From 4182943e7accc8a0e05f6dfdf9db7db06e94c6cd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 29 Sep 2015 15:17:03 +0200 Subject: [PATCH] Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions. --- src/theory/quantifiers/inst_strategy_cbqi.cpp | 33 ++++++++++++++- src/theory/quantifiers/inst_strategy_cbqi.h | 5 +++ .../quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 4 ++ src/theory/quantifiers/term_database.h | 2 + src/theory/quantifiers_engine.cpp | 10 +++-- src/theory/uf/theory_uf.cpp | 3 ++ src/theory/uf/theory_uf_strong_solver.cpp | 42 ++++++++++++------- src/theory/uf/theory_uf_strong_solver.h | 6 ++- test/regress/regress0/push-pop/Makefile.am | 3 +- .../regress0/push-pop/fmf-fun-dbu.smt2 | 15 +++++++ test/regress/regress0/sygus/Makefile.am | 3 +- .../regress/regress0/sygus/clock-inc-tuple.sy | 14 +++++++ 13 files changed, 118 insertions(+), 24 deletions(-) create mode 100644 test/regress/regress0/push-pop/fmf-fun-dbu.smt2 create mode 100644 test/regress/regress0/sygus/clock-inc-tuple.sy diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 8e6673fb9..1f4d398be 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -39,6 +39,7 @@ d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_v d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_true = NodeManager::currentNM()->mkConst( true ); + d_is_nested_quant = false; } void CegInstantiator::computeProgVars( Node n ){ @@ -1202,8 +1203,13 @@ void CegInstantiator::processAssertions() { //collect all assertions from theory for( context::CDList::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { Node lit = (*it).assertion; - d_curr_asserts[tid].push_back( lit ); - Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ + d_curr_asserts[tid].push_back( lit ); + Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + }else{ + Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; + } if( lit.getKind()==EQUAL ){ std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit ); if( itae!=d_aux_eq.end() ){ @@ -1338,6 +1344,25 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st subs_rhs.push_back( r ); } +void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==FORALL ){ + d_is_nested_quant = true; + }else{ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( TermDb::isBoolConnective( n.getKind() ) ){ + for( unsigned i=0; i& lems, std::vector< Node >& ce_vars ) { Assert( d_vars.empty() ); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); @@ -1367,6 +1392,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } lems[i] = rlem; } + //collect atoms from lem[0]: we will only do bounds coming from original body + d_is_nested_quant = false; + std::map< Node, bool > visited; + collectCeAtoms( lems[0], visited ); } //old implementation diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 9b3b15dc5..9fe938f16 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -65,7 +65,12 @@ private: std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables std::vector< Node > d_vars; + //atoms of the CE lemma + bool d_is_nested_quant; + std::vector< Node > d_ce_atoms; private: + //collect atoms + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); //for adding instantiations during check void computeProgVars( Node n ); //solved form, involves substitution with coefficients diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b7d82bc9e..9e13ef5eb 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1649,7 +1649,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT ); + return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() ); } bool MatchGen::isHandledUfTerm( TNode n ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 366c7ce07..2c9430876 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1549,6 +1549,10 @@ bool TermDb::isComm( Kind k ) { k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; } +bool TermDb::isBoolConnective( Kind k ) { + return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT; +} + void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 682a9f8e0..1b0b72bf9 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -394,6 +394,8 @@ public: static bool isAssoc( Kind k ); /** is comm */ static bool isComm( Kind k ); + /** is bool connective */ + static bool isBoolConnective( Kind k ); //for sygus private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f1c47a21a..2c2e4ea5b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -298,7 +298,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { } void QuantifiersEngine::presolve() { - Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl; + Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; for( unsigned i=0; ipresolve(); } @@ -306,9 +306,11 @@ void QuantifiersEngine::presolve() { d_presolve = false; //add all terms to database if( options::incrementalSolving() ){ + Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl; for( unsigned i=0; itheoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); - } + //if( options::finiteModelFind() ){ + // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); + //} d_quants[f] = true; return true; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 073399894..858761078 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -265,6 +265,9 @@ void TheoryUF::presolve() { d_out->lemma(*i); } } + if( d_thss ){ + d_thss->presolve(); + } Debug("uf") << "uf: end presolve()" << endl; } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 2a33b8b36..29e726da7 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -706,6 +706,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel } } +void StrongSolverTheoryUF::SortModel::presolve() { + d_initialized = false; + d_aloc_cardinality = 0; +} + void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){ } @@ -719,11 +724,14 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){ if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){ Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl; return cn; + }else{ + Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl; } } } Trace("uf-ss-dec") << "UFSS : no decisions for " << d_type << "." << std::endl; Trace("uf-ss-dec-debug") << " aloc_cardinality = " << d_aloc_cardinality << ", cardinality = " << d_cardinality << ", hasCard = " << d_hasCard << std::endl; + Assert( d_hasCard ); return Node::null(); } @@ -834,6 +842,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int if( !d_conflict ){ Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = "; Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; + Assert( c>0 ); Node cl = getCardinalityLiteral( c ); d_cardinality_assertions[ cl ] = val; if( val ){ @@ -878,10 +887,12 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int if( !d_hasCard ){ bool needsCard = true; for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){ - if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){ - Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl; - needsCard = false; - break; + if( it->first<=d_aloc_cardinality.get() ){ + if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){ + Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl; + needsCard = false; + break; + } } } if( needsCard ){ @@ -1702,6 +1713,14 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ } } +void StrongSolverTheoryUF::presolve() { + d_aloc_com_card.set( 0 ); + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + it->second->presolve(); + it->second->initialize( d_out ); + } +} + /** propagate */ void StrongSolverTheoryUF::propagate( Theory::Effort level ){ //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ @@ -1779,14 +1798,14 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ } } -void StrongSolverTheoryUF::registerQuantifier( Node f ){ - Debug("uf-ss-register") << "Register quantifier " << f << std::endl; +//void StrongSolverTheoryUF::registerQuantifier( Node f ){ +// Debug("uf-ss-register") << "Register quantifier " << f << std::endl; //must ensure the quantifier does not quantify over arithmetic //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ // TypeNode tn = f[0][i].getType(); // preRegisterType( tn, true ); //} -} +//} StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ @@ -1798,15 +1817,10 @@ StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ it = d_rep_model.find( tn ); } if( it!=d_rep_model.end() ){ - //initialize the type if necessary - //if( d_rep_model_init.find( tn )==d_rep_model_init.end() ){ - ////initialize the model - //it->second->initialize( d_out ); - //d_rep_model_init[tn] = true; - //} return it->second; + }else{ + return NULL; } - return NULL; } void StrongSolverTheoryUF::notifyRestart(){ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 3619a8ba7..3e612ff1f 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -268,6 +268,8 @@ public: bool areDisequal( Node a, Node b ); /** check */ void check( Theory::Effort level, OutputChannel* out ); + /** presolve */ + void presolve(); /** propagate */ void propagate( Theory::Effort level, OutputChannel* out ); /** get next decision request */ @@ -365,6 +367,8 @@ public: public: /** check */ void check( Theory::Effort level ); + /** presolve */ + void presolve(); /** propagate */ void propagate( Theory::Effort level ); /** get next decision request */ @@ -372,7 +376,7 @@ public: /** preregister a term */ void preRegisterTerm( TNode n ); /** preregister a quantifier */ - void registerQuantifier( Node f ); + //void registerQuantifier( Node f ); /** notify restart */ void notifyRestart(); public: diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 6d50cc39f..bcf6403b7 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -43,7 +43,8 @@ BUG_TESTS = \ bug654-dd.smt2 \ bug-fmf-fun-skolem.smt2 \ bug674.smt2 \ - inc-double-u.smt2 + inc-double-u.smt2 \ + fmf-fun-dbu.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 new file mode 100644 index 000000000..125d5fcc9 --- /dev/null +++ b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental --fmf-fun --no-check-models +(set-logic UFDTLIA) +(set-option :produce-models true) +(set-info :smt-lib-version 2.5) +(declare-datatypes () ((List (Nil) (Cons (Cons$head Int) (Cons$tail List))))) +(define-fun-rec all-z ((x List)) Bool (=> (is-Cons x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x))))) +(define-fun-rec len ((x List)) Int (ite (is-Nil x) 0 (+ 1 (len (Cons$tail x))))) +(declare-fun root() List) +; EXPECT: sat +(assert (and (all-z root) (<= 1 (len root)))) +(check-sat) +; EXPECT: sat +(assert (= root (Cons 0 Nil))) +(check-sat) + diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 6bd732c76..a1f91a6ce 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -44,7 +44,8 @@ TESTS = commutative.sy \ uminus_one.sy \ sygus-dt.sy \ dt-no-syntax.sy \ - list-head-x.sy + list-head-x.sy \ + clock-inc-tuple.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy new file mode 100644 index 000000000..09bdb8b4d --- /dev/null +++ b/test/regress/regress0/sygus/clock-inc-tuple.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth + +(set-logic ALL_SUPPORTED) +(declare-var m Int) +(declare-var s Int) +(declare-var inc Int) +(declare-datatypes () ( (tuple2 (tuple2 (_m Int) (_s Int))) )) + +(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2) +(constraint (=> +(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) +(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc))))) +(check-synth) -- 2.30.2