Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 and 763.

3 files changed, 71 insertions, 38 deletions

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index df8533135..5f73fe6d0 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -85,46 +85,48 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
     std::vector< Node > lemmas;
     for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
       Node q = it->first;
-      if( d_added_split.find( q )==d_added_split.end() ){
-        d_added_split.insert( q );
-        std::vector< Node > bvs;
-        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-          if( (int)i!=it->second ){
-            bvs.push_back( q[0][i] );
-          }
-        }
-        std::vector< Node > disj;
-        disj.push_back( q.negate() );
-        TNode svar = q[0][it->second];
-        TypeNode tn = svar.getType();
-        if( tn.isDatatype() ){
-          std::vector< Node > cons;
-          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-          for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-            std::vector< Node > vars;
-            for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-              TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
-              Node v = NodeManager::currentNM()->mkBoundVar( tns );
-              vars.push_back( v );
+      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        if( d_added_split.find( q )==d_added_split.end() ){
+          d_added_split.insert( q );
+          std::vector< Node > bvs;
+          for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+            if( (int)i!=it->second ){
+              bvs.push_back( q[0][i] );
             }
-            std::vector< Node > bvs_cmb;
-            bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
-            bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
-            vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
-            Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
-            TNode ct = c;
-            Node body = q[1].substitute( svar, ct );
-            if( !bvs_cmb.empty() ){
-              body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
+          }
+          std::vector< Node > disj;
+          disj.push_back( q.negate() );
+          TNode svar = q[0][it->second];
+          TypeNode tn = svar.getType();
+          if( tn.isDatatype() ){
+            std::vector< Node > cons;
+            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+            for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+              std::vector< Node > vars;
+              for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
+                TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
+                Node v = NodeManager::currentNM()->mkBoundVar( tns );
+                vars.push_back( v );
+              }
+              std::vector< Node > bvs_cmb;
+              bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
+              bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
+              vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
+              Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
+              TNode ct = c;
+              Node body = q[1].substitute( svar, ct );
+              if( !bvs_cmb.empty() ){
+                body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
+              }
+              cons.push_back( body );
             }
-            cons.push_back( body );
+            Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons );
+            disj.push_back( conc );
+          }else{
+            Assert( false );
           }
-          Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons );
-          disj.push_back( conc );
-        }else{
-          Assert( false );
+          lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
         }
-        lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
       }
     }
 
@@ -133,7 +135,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
       Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
       d_quantEngine->addLemma( lemmas[i], false );
     }
-    d_quant_to_reduce.clear();
+    //d_quant_to_reduce.clear();
   }
 }
 
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 8f1126ef5..99619a6aa 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -45,7 +45,8 @@ BUG_TESTS = \
   bug674.smt2 \
   inc-double-u.smt2 \
   fmf-fun-dbu.smt2 \
-  inc-define.smt2
+  inc-define.smt2 \
+  bug765.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/bug765.smt2 b/test/regress/regress0/push-pop/bug765.smt2
new file mode 100644
index 000000000..fb4aac85a
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug765.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes () (
+    (Color (red) (white) (blue))
+) )
+
+(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) )
+(declare-fun ColorFromString (String) Color)
+(assert (forall ((c Color)) (= c (ColorFromString (ColorToString c)))))
+
+(declare-datatypes () (
+    (CP (cp (c1 Color) (c2 Color)))
+) )
+
+(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (ColorToString (c1 cp)) "," (ColorToString (c2 cp)) ")"))
+(declare-fun CPFromString (String) CP)
+(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
+
+(declare-fun cpx() CP)
+(assert (= cpx (CPFromString "cp(white,red)")))
+
+; EXPECT: sat
+(check-sat)
+
+(declare-fun cpy() CP)
+(assert (= cpy (CPFromString "cp(red,blue)")))
+
+; EXPECT: sat
+(check-sat)