From 9d6a0bda98ac2c3e3c59f55f349e029d623b264a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 1 Dec 2016 11:37:44 -0600 Subject: [PATCH] Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 and 763. --- src/theory/quantifiers/quant_split.cpp | 76 +++++++++++----------- test/regress/regress0/push-pop/Makefile.am | 3 +- test/regress/regress0/push-pop/bug765.smt2 | 30 +++++++++ 3 files changed, 71 insertions(+), 38 deletions(-) create mode 100644 test/regress/regress0/push-pop/bug765.smt2 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; isecond ){ - 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 vars; - for( unsigned k=0; kmkBoundVar( 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; isecond ){ + 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 vars; + for( unsigned k=0; kmkBoundVar( 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) -- 2.30.2