Bug fixes related to parametric datatypes + theory combination + quantifiers. Add...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 1653ab636fb0cd90c2362822b365a7c259429a83..eb8b239736573ab96d4c5b701a4f038f5e002763 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -540,8 +540,9 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       if( tst==d_true ){
         n_ret = sel;
       }else{
-        mkExpDefSkolem( selector, n[0].getType(), n.getType() );
-        Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
+        TypeNode ndt = n[0].getType();
+        mkExpDefSkolem( selector, ndt, n.getType() );
+        Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ndt][ selector ], n[0]  );
         if( tst==NodeManager::currentNM()->mkConst( false ) ){
           n_ret = sk;
         }else{
@@ -994,10 +995,10 @@ void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels )
 }
 
 void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
-  if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){
+  if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
     std::stringstream ss;
     ss << sel << "_uf";
-    d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+    d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
                                   NodeManager::currentNM()->mkFunctionType( dt, rt ) );
   }
 }
@@ -1299,7 +1300,8 @@ void TheoryDatatypes::computeCareGraph(){
             TNode y = f2[k];
             Assert(d_equalityEngine.hasTerm(x));
             Assert(d_equalityEngine.hasTerm(y));
-            if( areDisequal(x, y) ){
+            //need to consider types for parametric selectors
+            if( x.getType()!=y.getType() || areDisequal(x, y) ){
               somePairIsDisequal = true;
               break;
             }else if( !d_equalityEngine.areEqual( x, y ) ){

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index b826780fcc0396e3f4742da922fb2facd3b26289..4bf04e08cd1453b9d169910378b75b4400571a59 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -183,7 +183,7 @@ private:
   /** counter for forcing assignments (ensures fairness) */
   unsigned d_dtfCounter;
   /** expand definition skolem functions */
-  std::map< Node, Node > d_exp_def_skolem;
+  std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem;
   /** sygus utilities */
   SygusSplit * d_sygus_split;
   SygusSymBreak * d_sygus_sym_break;

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index bb514f41bfd1bef4cedcd67f49b6ed3760423c9e..8c67eb95eaf2ef451cb6d790ce700b97d6273710 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -691,10 +691,13 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 if( max_zero[i] ){
                   //no terms available, will report incomplete instantiation
                   terms.push_back( Node::null() );
+                  Trace("inst-alg-rd") << "  null" << std::endl;
                 }else if( r==0 ){
                   terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+                  Trace("inst-alg-rd") << "  " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl;
                 }else{
                   terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
+                  Trace("inst-alg-rd") << "  " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl;
                 }
               }
               if( d_quantEngine->addInstantiation( f, terms, false ) ){

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1cbfbd99b8d350380aacfc913e74911457cc40c6..c796333b3a1347f918c365fbd2354cc78de700d7 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -508,9 +508,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe
       if( it!=d_var_rel_dom.end() ){
         for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
           for( unsigned j=0; j<it2->second.size(); j++ ){
-            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->second << "." << it2->second[j] << "?" << std::endl;
+            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->first << "." << it2->second[j] << "?" << std::endl;
             if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
-              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl;
               return false;
             }
           }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ef301c2cf04d0dbf1180be8369ab7c826cd5463c..51c72d7bbc471bdcd771a012df23823970172e03 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -126,9 +126,10 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
 }
 
 Node TermDb::getMatchOperator( Node n ) {
-  //return n.getOperator();
   Kind k = n.getKind();
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
+  //datatype operators may be parametric, always assume they are
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
+      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
@@ -241,10 +242,11 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ
   if( itv != visited.end() ){
     return itv->second;
   }
-  Assert( n.getKind()!=BOUND_VARIABLE );
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
   Node ret;
-  if( !qy->hasTerm( n ) ){
+  if( n.getKind()==BOUND_VARIABLE ){
+    return n;
+  }else if( !qy->hasTerm( n ) ){
     //term is not known to be equal to a representative in equality engine, evaluate it
     if( n.getKind()==FORALL ){
       ret = Node::null();

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index b51313debceb29e01745c3909caf41095d4e8d03..6b5e0d1ed1e075d33405945dc1973613e2314c78 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -78,7 +78,8 @@ TESTS =       \
        pure_dt_cbqi.smt2 \
        florian-case-ax.smt2 \
        double-pattern.smt2 \
-       qcf-rel-dom-opt.smt2
+       qcf-rel-dom-opt.smt2 \
+       parametric-lists.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine

diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2
new file mode 100644 (file)
index 0000000..c117934
--- /dev/null
+++ b/test/regress/regress0/quantifiers/parametric-lists.smt2
@@ -0,0 +1,42 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil))))
+(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair
+(declare-fun mapper ((List Int)) (List KV))
+(assert
+  (forall
+    ((input (List Int)))
+     (ite
+        (= input (as nil (List Int)))
+        (= (as nil (List KV)) (mapper input))
+        (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input))
+     )
+  )                                                                                                                            
+)
+(declare-fun reduce ((List KV)) Int)
+(assert
+  (forall
+    ((inputk (List KV)))
+    (ite
+      (= inputk (as nil (List KV)))
+      (= 0 (reduce inputk))
+      (= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk))
+    )
+  )
+)
+(declare-fun sum ((List Int)) Int)
+(assert
+  (forall
+    ((input (List Int)))
+    (ite
+      (= input (as nil (List Int)))
+      (= 0 (sum input))
+      (= (+ (head input) (sum (tail input))) (sum input))
+    )
+  )
+)
+(assert
+  (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int)))))))
+)
+(check-sat)
+