diff options
25 files changed, 98 insertions, 46 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 28a08630e..7946fea59 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2119,10 +2119,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } -Node TheoryArrays::getNextDecisionRequest() { +Node TheoryArrays::getNextDecisionRequest( unsigned& priority ) { if(! d_decisionRequests.empty()) { Node n = d_decisionRequests.front(); d_decisionRequests.pop(); + priority = 2; return n; } else { return Node::null(); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index c1223474c..77c5928f0 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -255,7 +255,7 @@ class TheoryArrays : public Theory { private: public: - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); void presolve(); void shutdown() { } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 54853ceaf..dc0019383 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -417,7 +417,7 @@ void BoundedIntegers::assertNode( Node n ) { d_assertions[nlit] = n.getKind()!=NOT; } -Node BoundedIntegers::getNextDecisionRequest() { +Node BoundedIntegers::getNextDecisionRequest( unsigned& priority ) { Trace("bound-int-dec-debug") << "bi: Get next decision request?" << std::endl; for( unsigned i=0; i<d_ranges.size(); i++) { Node d = d_rms[d_ranges[i]]->getNextDecisionRequest(); @@ -435,6 +435,7 @@ Node BoundedIntegers::getNextDecisionRequest() { i--; } }else{ + priority = 1; Trace("bound-int-dec") << "Bounded Integers : Decide " << d << std::endl; return d; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index c3fb05641..0dfd7eafd 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -146,7 +146,7 @@ public: void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); } unsigned getBoundVarType( Node q, Node v ); unsigned getNumBoundVars( Node q ) { return d_set[q].size(); } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 54415d974..ecf4bb74d 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -229,6 +229,10 @@ CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c d_last_inst_si = false; } +CegInstantiation::~CegInstantiation(){ + delete d_conj; +} + bool CegInstantiation::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } @@ -345,7 +349,7 @@ void CegInstantiation::registerQuantifier( Node q ) { void CegInstantiation::assertNode( Node n ) { } -Node CegInstantiation::getNextDecisionRequest() { +Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { //enforce fairness if( d_conj->isAssigned() ){ d_conj->initializeGuard( d_quantEngine ); @@ -363,6 +367,7 @@ Node CegInstantiation::getNextDecisionRequest() { bool value; if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) { Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl; + priority = 0; return req_dec[i]; }else{ Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl; @@ -377,10 +382,12 @@ Node CegInstantiation::getNextDecisionRequest() { d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + priority = 1; return lit; } }else{ Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; + priority = 1; return lit; } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index c8b41c035..7f36f4d25 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -154,6 +154,7 @@ private: Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); + ~CegInstantiation(); public: bool needsCheck( Theory::Effort e ); unsigned needsModel( Theory::Effort e ); @@ -163,7 +164,7 @@ public: void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); void assertNode( Node n ); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } /** print solution for synthesis conjectures */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ac6e1edbe..895a0c93c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -592,12 +592,13 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool return Node::null(); } -Node InstStrategyCbqi::getNextDecisionRequest(){ +Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ std::map< Node, bool > proc; for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); Node d = getNextDecisionRequestProc( q, proc ); if( !d.isNull() ){ + priority = 0; return d; } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c9f62243f..2cd5f6e1c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -107,7 +107,7 @@ public: void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); /** get next decision request */ - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); }; //generalized counterexample guided quantifier instantiation diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 3ff21aa6e..b4264135c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -61,7 +61,7 @@ public: virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) {} virtual void propagate( Theory::Effort level ){} - virtual Node getNextDecisionRequest() { return TNode::null(); } + virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); } /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; public: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e97a76ce6..0b4f3c0c7 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -179,8 +179,8 @@ void TheoryQuantifiers::check(Effort e) { getQuantifiersEngine()->check( e ); } -Node TheoryQuantifiers::getNextDecisionRequest(){ - return getQuantifiersEngine()->getNextDecisionRequest(); +Node TheoryQuantifiers::getNextDecisionRequest( unsigned& priority ){ + return getQuantifiersEngine()->getNextDecisionRequest( priority ); } void TheoryQuantifiers::assertUniversal( Node n ){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index ba5a75d86..308514b92 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -63,7 +63,7 @@ public: void presolve(); void ppNotifyAssertions( std::vector< Node >& assertions ); void check(Effort e); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); Node getValue(TNode n); void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown() { } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 95b01bc7b..22bfa948f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -767,14 +767,17 @@ void QuantifiersEngine::propagate( Theory::Effort level ){ } } -Node QuantifiersEngine::getNextDecisionRequest(){ +Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ + unsigned min_priority; + Node dec; for( unsigned i=0; i<d_modules.size(); i++ ){ - Node n = d_modules[i]->getNextDecisionRequest(); - if( !n.isNull() ){ - return n; + Node n = d_modules[i]->getNextDecisionRequest( priority ); + if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){ + dec = n; + min_priority = priority; } } - return Node::null(); + return dec; } quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ff6a8a36c..fc2b27e02 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -294,7 +294,7 @@ public: /** propagate */ void propagate( Theory::Effort level ); /** get next decision request */ - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); private: /** reduceQuantifier, return true if reduced */ bool reduceQuantifier( Node q ); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 426daf622..ea025e3a2 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -683,6 +683,7 @@ void TheorySep::check(Effort e) { }else{ //this typically should not happen, should never happen for complete base theories Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl; + Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " << lem << "!!!" << std::endl; } } }else{ @@ -700,6 +701,7 @@ void TheorySep::check(Effort e) { //must witness finite data points-to for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){ TypeNode data_type = d_loc_to_data_type[it->first]; + //if the data type is finite if( data_type.isInterpretedFinite() ){ computeLabelModel( it->second ); Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " << data_type << std::endl; @@ -708,18 +710,29 @@ void TheorySep::check(Effort e) { Node l = d_label_model[it->second].d_heap_locs_model[j][0]; Trace("sep-process-debug") << " location : " << l << std::endl; if( d_pto_model[l].isNull() ){ - Node ll = d_tmodel[l]; - Assert( !ll.isNull() ); - Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl; - Node dsk = NodeManager::currentNM()->mkSkolem( "dsk", data_type, "pto-data for implicit location" ); - // if location is in the heap, then something must point to it - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::MEMBER, ll, it->second ), - NodeManager::currentNM()->mkNode( kind::SEP_STAR, - NodeManager::currentNM()->mkNode( kind::SEP_PTO, ll, dsk ), - d_true ) ); - Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl; - d_out->lemma( lem ); - addedLemma = true; + needAddLemma = true; + Node ll; + std::map< Node, Node >::iterator itm = d_tmodel.find( l ); + if( itm!=d_tmodel.end() ) { + ll = itm->second; + }else{ + //try to assign arbitrary skolem? + } + if( !ll.isNull() ){ + Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl; + Node dsk = NodeManager::currentNM()->mkSkolem( "dsk", data_type, "pto-data for implicit location" ); + // if location is in the heap, then something must point to it + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::MEMBER, ll, it->second ), + NodeManager::currentNM()->mkNode( kind::SEP_STAR, + NodeManager::currentNM()->mkNode( kind::SEP_PTO, ll, dsk ), + d_true ) ); + Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl; + d_out->lemma( lem ); + addedLemma = true; + }else{ + //This should only happen if we are in an unbounded fragment + Trace("sep-warn") << "TheorySep : WARNING : no term corresponding to location " << l << " in heap!!!" << std::endl; + } }else{ Trace("sep-process-debug") << " points-to data witness : " << d_pto_model[l] << std::endl; } @@ -727,7 +740,6 @@ void TheorySep::check(Effort e) { } } if( !addedLemma && needAddLemma ){ - Trace("sep-process") << "WARNING : could not find sep refinement lemma!!!" << std::endl; Assert( false ); d_out->setIncomplete(); } @@ -741,7 +753,7 @@ bool TheorySep::needsCheckLastEffort() { return hasFacts(); } -Node TheorySep::getNextDecisionRequest() { +Node TheorySep::getNextDecisionRequest( unsigned& priority ) { for( unsigned i=0; i<d_neg_guards.size(); i++ ){ Node g = d_neg_guards[i]; bool success = true; @@ -754,6 +766,7 @@ Node TheorySep::getNextDecisionRequest() { Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q ); bool value; if( d_valuation.hasSatValue( cel, value ) ){ + Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl; success = value; }else{ Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl; @@ -765,6 +778,7 @@ Node TheorySep::getNextDecisionRequest() { bool value; if( !d_valuation.hasSatValue( g, value ) ) { Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl; + priority = 0; return g; } } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index a3bb1bd7b..35b7fe5e9 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -118,7 +118,7 @@ class TheorySep : public Theory { private: public: - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); void presolve(); void shutdown() { } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5a99f8e30..ade5428ca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3802,7 +3802,7 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { //// Finite Model Finding -Node TheoryStrings::getNextDecisionRequest() { +Node TheoryStrings::getNextDecisionRequest( unsigned& priority ) { if( options::stringFMF() && !d_conflict ){ Node in_var_lsum = d_input_var_lsum.get(); //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl; @@ -3852,6 +3852,7 @@ Node TheoryStrings::getNextDecisionRequest() { } Node lit = d_cardinality_lits[ decideCard ]; Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit << std::endl; + priority = 1; return lit; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6665f9e50..457afb15a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -502,7 +502,7 @@ private: context::CDO< int > d_curr_cardinality; public: //for finite model finding - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); //ppRewrite Node ppRewrite(TNode atom); public: diff --git a/src/theory/theory.h b/src/theory/theory.h index 28552ed79..ffcec7c0c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -604,8 +604,12 @@ public: /** * Return a decision request, if the theory has one, or the NULL node * otherwise. + * If returning non-null node, hould set priority to + * 0 if decision is necessary for model-soundness, + * 1 if decision is necessary for completeness, + * >1 otherwise. */ - virtual Node getNextDecisionRequest() { return Node(); } + virtual Node getNextDecisionRequest( unsigned& priority ) { return Node(); } /** * Statically learn from assertion "in," which has been asserted diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c3e853ec0..9de8fa0dd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -739,21 +739,25 @@ void TheoryEngine::propagate(Theory::Effort effort) { Node TheoryEngine::getNextDecisionRequest() { // Definition of the statement that is to be run by every theory + unsigned min_priority; + Node dec; #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \ - Node n = theoryOf(THEORY)->getNextDecisionRequest(); \ - if(! n.isNull()) { \ - return n; \ + unsigned priority; \ + Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \ + if(! n.isNull() && ( dec.isNull() || priority<min_priority ) ) { \ + dec = n; \ + min_priority = priority; \ } \ } // Request decision from each theory using the statement above CVC4_FOR_EACH_THEORY; - return TNode(); + return dec; } bool TheoryEngine::properConflict(TNode conflict) const { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ae935798e..4cdc5e240 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -205,9 +205,9 @@ void TheoryUF::propagate(Effort effort) { //} } -Node TheoryUF::getNextDecisionRequest(){ +Node TheoryUF::getNextDecisionRequest( unsigned& priority ){ if (d_thss != NULL && !d_conflict) { - return d_thss->getNextDecisionRequest(); + return d_thss->getNextDecisionRequest( priority ); }else{ return Node::null(); } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 3a83decec..0900b4c90 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -194,7 +194,7 @@ public: void computeCareGraph(); void propagate(Effort effort); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); EqualityStatus getEqualityStatus(TNode a, TNode b); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 4713c7dcf..edb92bb1b 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1962,7 +1962,7 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){ } /** get next decision request */ -Node StrongSolverTheoryUF::getNextDecisionRequest(){ +Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){ //request the combined cardinality as a decision literal, if not already asserted if( options::ufssFairness() ){ int comCard = 0; @@ -1972,6 +1972,7 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){ com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null(); if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){ Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl; + priority = 1; return com_lit; } comCard++; @@ -1984,6 +1985,7 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Node n = it->second->getNextDecisionRequest(); if( !n.isNull() ){ + priority = 1; return n; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 40026522d..4130a7d41 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -399,7 +399,7 @@ public: /** propagate */ void propagate( Theory::Effort level ); /** get next decision request */ - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ void preRegisterTerm( TNode n ); /** notify restart */ diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 203352af3..2d35aef51 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ dup-nemp.smt2 \ emp2-quant-unsat.smt2 \ dispose-1.smt2 \ - finite-witness-sat.smt2 + finite-witness-sat.smt2 \ + sep-fmf-priority.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/sep-fmf-priority.smt2 b/test/regress/regress0/sep/sep-fmf-priority.smt2 new file mode 100644 index 000000000..fe3af1b35 --- /dev/null +++ b/test/regress/regress0/sep/sep-fmf-priority.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) + +(declare-sort Loc 0) +(declare-const l Loc) +(declare-const x Loc) + +(assert (wand (pto x x) false)) +(assert (forall ((x Loc) (y Loc)) (not (pto x y)))) + +(check-sat) |