From e7439fc0daf1049f59540b9aeb890a52d86a77bd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 13 May 2015 10:13:16 +0200 Subject: [PATCH] Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus. --- .../quantifiers/instantiation_engine.cpp | 210 ++++++------------ src/theory/quantifiers/instantiation_engine.h | 19 +- src/theory/quantifiers/model_engine.cpp | 16 +- src/theory/quantifiers/model_engine.h | 2 + src/theory/quantifiers_engine.cpp | 35 ++- src/theory/quantifiers_engine.h | 2 + src/util/datatype.cpp | 2 +- 7 files changed, 117 insertions(+), 169 deletions(-) diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 3b31bad13..12d6bed8d 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -30,8 +30,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; -InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ), d_setIncomplete( setIncomplete ){ +InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) : +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ } @@ -101,14 +101,16 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); if( !ceLit.isNull() ){ //require any decision on cel to be phase=true - d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + //d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + d_quantEngine->addRequirePhase( ceLit, true ); Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma NodeBuilder<> nb(kind::OR); nb << f << ceLit; Node lem = nb; Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem, false, true ); + //d_quantEngine->getOutputChannel().lemma( lem, false, true ); + d_quantEngine->addLemma( lem, false ); addedLemma = true; } } @@ -123,6 +125,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ InstStrategy* is = d_instStrategies[i]; is->processResetInstantiationRound( effort ); } + //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; @@ -132,24 +135,21 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl; finished = true; //instantiate each quantifier - for( int q=0; qgetModel()->getNumAssertedQuantifiers(); q++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( q ); - Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl; - //if this quantifier is active - if( d_quant_active[ f ] ){ - //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e; - int e_use = e; - if( e_use>=0 ){ - Trace("inst-engine-debug") << "inst-engine : " << f << std::endl; - //check each instantiation strategy - for( size_t i=0; iidentify() << " " << e_use << std::endl; - int quantStatus = is->process( f, effort, e_use ); - Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; - if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ - finished = false; - } + for( unsigned i=0; igetRelevance( q )==-1 ? e - 1 : e; + int e_use = e; + if( e_use>=0 ){ + Trace("inst-engine-debug") << "inst-engine : " << q << std::endl; + //check each instantiation strategy + for( size_t i=0; iidentify() << " " << e_use << std::endl; + int quantStatus = is->process( q, effort, e_use ); + Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; + if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ + finished = false; } } } @@ -173,6 +173,32 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ return d_quantEngine->getInstWhenNeedsCheck( e ); } +void InstantiationEngine::reset_round( Theory::Effort e ) { + if( options::cbqi() ){ + //set inactive the quantified formulas whose CE literals are asserted false + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine + if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) && hasAddedCbqiLemma( q ) ){ + Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + bool value; + if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; + if( !value ){ + d_quantEngine->getModel()->setQuantifierActive( q, false ); + if( d_quantEngine->getValuation().isDecision( cel ) ){ + Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; + } + } + }else{ + Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; + } + } + } + } +} + void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ double clSet = 0; @@ -182,89 +208,23 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } ++(d_statistics.d_instantiation_rounds); bool quantActive = false; - Debug("quantifiers") << "quantifiers: check: asserted quantifiers size=" - << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; + d_quants.clear(); for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Debug("quantifiers") << "Process " << n << "..." << std::endl; - //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( !d_quantEngine->hasOwnership( n, this ) ){ - d_quant_active[n] = false; - Debug("quantifiers") << " Quantifier has owner." << std::endl; - }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ - d_quant_active[n] = false; - Debug("quantifiers") << " Quantifier is not active (from model)." << std::endl; - //it is not active if we have found the skolemized negation is unsat - }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); - bool active, value; - bool ceValue = false; - if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - active = value; - ceValue = true; - }else{ - active = true; - } - d_quant_active[n] = active; - if( active ){ - Debug("quantifiers") << " Active : " << n; - if( !TermDb::hasInstConstAttr(n) ){ - quantActive = true; - } - }else{ - Debug("quantifiers") << " NOT active : " << n; - if( d_quantEngine->getValuation().isDecision( cel ) ){ - Debug("quant-req-phase") << "Bad decision : " << cel << std::endl; - } - //note that the counterexample literal must not be a decision - Assert( !d_quantEngine->getValuation().isDecision( cel ) ); - } - if( d_quantEngine->getValuation().hasSatValue( n, value ) ){ - Debug("quantifiers") << ", value = " << value; - } - if( ceValue ){ - Debug("quantifiers") << ", ce is asserted"; - } - Debug("quantifiers") << std::endl; - }else{ - d_quant_active[n] = true; - if( !TermDb::hasInstConstAttr(n) ){ + if( d_quantEngine->hasOwnership( n, this ) && d_quantEngine->getModel()->isQuantifierActive( n ) ){ + if( !options::cbqi() || !TermDb::hasInstConstAttr(n) ){ quantActive = true; } - Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl; + d_quants.push_back( n ); } - Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl; - if( options::relevantTriggers() ){ - Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; - Debug("quantifiers") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; - } - Trace("inst-engine-debug") << "Process : " << n << " " << d_quant_active[n] << std::endl; } + Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; + Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl; if( quantActive ){ bool addedLemmas = doInstantiationRound( e ); - if( !addedLemmas && e==Theory::EFFORT_LAST_CALL ){ - //check if we need to set the incomplete flag - if( d_setIncomplete ){ - //check if we are complete for all active quantifiers - bool inc = false; - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( isIncomplete( f ) ){ - inc = true; - break; - } - } - if( inc ){ - Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl; - d_quantEngine->getOutputChannel().setIncomplete(); - }else{ - Debug("inst-engine") << "Instantiation strategies were complete..." << std::endl; - } - }else{ - Assert( options::finiteModelFind() ); - Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl; - } - } + Trace("inst-engine-debug") << "Add lemmas = " << addedLemmas << std::endl; + }else{ + d_quants.clear(); } if( Trace.isOn("inst-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); @@ -273,6 +233,15 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } } +bool InstantiationEngine::checkComplete() { + for( unsigned i=0; ihasOwnership( f, this ) ){ //Notice() << "do cbqi " << f << " ? " << std::endl; @@ -341,13 +310,10 @@ bool InstantiationEngine::doCbqi( Node f ){ } bool InstantiationEngine::isIncomplete( Node f ) { - if( d_i_lte ){ - //TODO : ensure completeness for local theory extensions - //return !d_i_lte->isLocalTheoryExt( f ); - return true; - }else{ - return true; - } + return true; + //TODO : ensure completeness for local theory extensions + //if( d_i_lte ){ + //return !d_i_lte->isLocalTheoryExt( f ); } @@ -361,39 +327,6 @@ bool InstantiationEngine::isIncomplete( Node f ) { - -void InstantiationEngine::debugSat( int reason ){ - if( reason==SAT_CBQI ){ - //Debug("quantifiers-sat") << "Decisions:" << std::endl; - //for( int i=1; i<=(int)d_quantEngine->getValuation().getDecisionLevel(); i++ ){ - // Debug("quantifiers-sat") << " " << i << ": " << d_quantEngine->getValuation().getDecision( i ) << std::endl; - //} - //for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) { - // if( (*i).second ) { - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - Assert( !cel.isNull() ); - bool value; - if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - if( !value ){ - AlwaysAssert(! d_quantEngine->getValuation().isDecision( cel ), - "bad decision on counterexample literal"); - } - } - } - if( d_setIncomplete ){ - Debug("quantifiers-sat") << "Cannot conclude SAT with nested quantifiers in recursive strategy." << std::endl; - //TODO : only when existentials with inst constants - d_quantEngine->getOutputChannel().setIncomplete(); - } - //} - Debug("quantifiers-sat") << "return SAT: Cbqi, no quantifier is active. " << std::endl; - }else if( reason==SAT_INST_STRATEGY ){ - Debug("quantifiers-sat") << "return SAT: No strategy chose to add an instantiation." << std::endl; - } -} - Node InstantiationEngine::getNextDecisionRequest(){ //propagate as decision all counterexample literals that are not asserted if( options::cbqi() ){ @@ -403,8 +336,7 @@ Node InstantiationEngine::getNextDecisionRequest(){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - //if not already set, propagate as decision - Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << cel << std::endl; + Debug("cbqi-prop-as-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 8a733ac1d..21056bc05 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -73,10 +73,8 @@ private: InstStrategyCegqi * d_i_cegqi; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** whether the instantiation engine should set incomplete if it cannot answer SAT */ - bool d_setIncomplete; - /** whether each quantifier is active */ - std::map< Node, bool > d_quant_active; + /** current processing quantified formulas */ + std::vector< Node > d_quants; /** whether we have added cbqi lemma */ std::map< Node, bool > d_added_cbqi_lemma; private: @@ -94,21 +92,16 @@ private: bool doInstantiationRound( Theory::Effort effort ); /** register literals of n, f is the quantifier it belongs to */ //void registerLiterals( Node n, Node f ); -private: - enum{ - SAT_CBQI, - SAT_INST_STRATEGY, - }; - /** debug sat */ - void debugSat( int reason ); public: - InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true ); + InstantiationEngine( QuantifiersEngine* qe ); ~InstantiationEngine(); /** initialize */ void finishInit(); - bool needsCheck( Theory::Effort e ); + bool needsCheck( Theory::Effort e ); + void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); + bool checkComplete(); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 1d6676464..ce780a29b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -35,7 +35,7 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), -d_incomplete_check(false), +d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), d_totalLemmas(0) @@ -55,6 +55,10 @@ unsigned ModelEngine::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_MODEL; } +void ModelEngine::reset_round( Theory::Effort e ) { + d_incomplete_check = true; +} + void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ int addedLemmas = 0; @@ -95,16 +99,16 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - //if the check was incomplete, we must set incomplete flag - if( d_incomplete_check ){ - d_quantEngine->getOutputChannel().setIncomplete(); - } }else{ //otherwise, the search will continue } } } +bool ModelEngine::checkComplete() { + return !d_incomplete_check; +} + void ModelEngine::registerQuantifier( Node f ){ if( Trace.isOn("fmf-warn") ){ bool canHandle = true; @@ -218,7 +222,7 @@ int ModelEngine::checkModel(){ if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ //set incomplete if( effort==0 ){ - d_quantEngine->getOutputChannel().setIncomplete(); + d_incomplete_check = true; } break; } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 6cdb47be2..c357c2876 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -49,7 +49,9 @@ public: public: bool needsCheck( Theory::Effort e ); unsigned needsModel( Theory::Effort e ); + void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); + bool checkComplete(); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 19e39d5b5..c940b3218 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -86,7 +86,7 @@ d_lemmas_produced_c(u){ d_hasAddedLemma = false; bool needsBuilder = false; - + Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object @@ -123,9 +123,9 @@ d_lemmas_produced_c(u){ }else{ d_sg_gen = NULL; } + //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules if( !options::finiteModelFind() || options::fmfInstEngine() ){ - //the instantiation must set incomplete flag unless finite model finding is turned on - d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() ); + d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); }else{ d_inst_engine = NULL; @@ -329,11 +329,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first FIXME: remove? - uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); - if( ufss && !ufss->minimize() ){ - return; - } + //if effort is last call, try to minimize model first + //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + //if( ufss && !ufss->minimize() ){ return; } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); @@ -381,6 +379,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; + }else{ + Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl; } //SAT case if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ @@ -390,12 +390,27 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_te->getModelBuilder()->buildModel( d_model, true ); Trace("quant-engine-debug") << "Done building the model." << std::endl; } - //check other sources of incompleteness bool setInc = false; - if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ + if( needsCheck ){ setInc = true; + for( unsigned i=0; icheckComplete() ){ + Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl; + setInc = false; + } + } + }else{ + Trace("quant-engine-debug") << "Do not set incomplete because check wasn't necessary." << std::endl; + } + //check other sources of incompleteness + if( !setInc ){ + if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ + Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl; + setInc = true; + } } if( setInc ){ + Trace("quant-engine-debug") << "Set incomplete flag." << std::endl; getOutputChannel().setIncomplete(); } //output debug stats diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1d8c1591c..6468d4650 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -60,6 +60,8 @@ public: virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ virtual void check( Theory::Effort e, unsigned quant_e ) = 0; + /* check was complete (e.g. no lemmas implies a model) */ + virtual bool checkComplete() { return false; } /* Called for new quantifiers */ virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) = 0; diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 948bad56c..5a7a6da89 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -140,7 +140,7 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_type = st; d_sygus_bvl = bvl; d_sygus_allow_const = allow_const || allow_all; - d_sygus_allow_const = allow_all; + d_sygus_allow_all = allow_all; } -- 2.30.2