From dd963729849ca7f1001373c56e800bd62781fe98 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Sep 2016 10:43:28 -0500 Subject: [PATCH] Refactor setIncomplete in quantifiers. --- src/theory/quantifiers/ambqi_builder.cpp | 7 ++- src/theory/quantifiers/ambqi_builder.h | 2 +- src/theory/quantifiers/full_model_check.cpp | 8 +-- src/theory/quantifiers/full_model_check.h | 2 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 59 ++++++++++++------- src/theory/quantifiers/inst_strategy_cbqi.h | 5 +- .../quantifiers/instantiation_engine.cpp | 16 +---- src/theory/quantifiers/instantiation_engine.h | 2 +- src/theory/quantifiers/local_theory_ext.h | 2 + src/theory/quantifiers/model_builder.cpp | 7 +-- src/theory/quantifiers/model_builder.h | 11 ++-- src/theory/quantifiers/model_engine.cpp | 33 +++++++---- src/theory/quantifiers/model_engine.h | 3 + src/theory/quantifiers/quant_split.cpp | 5 ++ src/theory/quantifiers/quant_split.h | 1 + src/theory/quantifiers/quant_util.cpp | 2 +- src/theory/quantifiers/quant_util.h | 4 +- src/theory/quantifiers/rewrite_engine.cpp | 5 ++ src/theory/quantifiers/rewrite_engine.h | 1 + src/theory/quantifiers_engine.cpp | 43 ++++++++++---- 20 files changed, 138 insertions(+), 80 deletions(-) diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 97116dee4..2ccc17e55 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -836,7 +836,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //--------------------model checking--------------------------------------- //do exhaustive instantiation -bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { +int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl; if (effort==0) { FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs(); @@ -868,9 +868,10 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in d_addedLemmas += lem; Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl; } - return quantValid; + return quantValid ? 1 : 0; + }else{ + return 1; } - return true; } bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 3669d38b7..0adaef638 100644 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -93,7 +93,7 @@ public: //process build model void processBuildModel(TheoryModel* m, bool fullModel); //do exhaustive instantiation - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); }; } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index be608aeaa..72057e734 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -589,7 +589,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { } -bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { +int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; Assert( !d_qe->inConflict() ); if( optUseModel() ){ @@ -723,15 +723,15 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){ //something went wrong, resort to exhaustive instantiation - return false; + return 0; } } } } } - return true; + return 1; }else{ - return false; + return 0; } } diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 411b7a5eb..7d21b4185 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -139,7 +139,7 @@ public: void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 82f45916c..9ee62964b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -285,6 +285,15 @@ bool InstStrategyCbqi::checkComplete() { } } +bool InstStrategyCbqi::checkCompleteFor( Node q ) { + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); + if( it!=d_do_cbqi.end() ){ + return it->second>0; + }else{ + return false; + } +} + Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){ std::map< Node, Node >::iterator it = visited.find( n ); if( it==visited.end() ){ @@ -334,7 +343,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ - if( !options::cbqiAll() ){ + if( d_do_cbqi[q]==2 ){ //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); @@ -512,43 +521,49 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ } bool InstStrategyCbqi::doCbqi( Node q ){ - std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ - bool ret = true; + int ret = 2; if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ for( unsigned i=0; igetTermDatabase()->getInstConstantBody( q ); - int ncbqiv = hasNonCbqiVariable( q ); - if( ncbqiv==1 ){ - //all variables imply this will be handled regardless of body (e.g. for EPR) - ret = true; - }else if( ncbqiv==0 ){ - std::map< Node, bool > visited; - ret = !hasNonCbqiOperator( q[1], visited ); - }else{ - ret = false; + if( ret!=0 ){ + //if quantifier has a non-handled variable, then do not use cbqi + //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR + int ncbqiv = hasNonCbqiVariable( q ); + if( ncbqiv==0 || ncbqiv==1 ){ + std::map< Node, bool > visited; + if( hasNonCbqiOperator( q[1], visited ) ){ + if( ncbqiv==1 ){ + //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR) + // so, try but not exclusively + ret = 1; + }else{ + //cannot be handled + ret = 0; + } } + }else{ + // unhandled variable type + ret = 0; + } + if( ret==0 && options::cbqiAll() ){ + //try but not exclusively + ret = 1; } } } Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; - return ret; + return ret!=0; }else{ - return it->second; + return it->second!=0; } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 18f4f4a31..eab267747 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -48,8 +48,8 @@ protected: std::map< Node, bool > d_active_quant; /** whether we have instantiated quantified formulas */ //NodeSet d_added_inst; - /** whether to do cbqi for this quantified formula */ - std::map< Node, bool > d_do_cbqi; + /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */ + std::map< Node, int > d_do_cbqi; /** register ce lemma */ bool registerCbqiLemma( Node q ); virtual void registerCounterexampleLemma( Node q, Node lem ); @@ -103,6 +103,7 @@ public: void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); + bool checkCompleteFor( Node q ); void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); /** get next decision request */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index db597d031..f46d08f08 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -151,19 +151,9 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } } -bool InstantiationEngine::checkComplete() { - if( !options::finiteModelFind() ){ - for( unsigned i=0; igetModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ @@ -470,10 +470,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = riter.isIncomplete(); - return true; + return riter.isIncomplete() ? -1 : 1; }else{ - return false; + return 0; } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index e4f9529a8..9b89e5ef6 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -38,13 +38,14 @@ public: virtual ~QModelBuilder() throw() {} // is quantifier active? virtual bool isQuantifierActive( Node f ); - //do exhaustive instantiation - virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } + //do exhaustive instantiation + // 0 : failed, but resorting to true exhaustive instantiation may work + // >0 : success + // <0 : failed + virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } //whether to construct model virtual bool optUseModel(); /** number of lemmas generated while building model */ - //is the exhaustive instantiation incomplete? - bool d_incomplete_check; int d_addedLemmas; int d_triedLemmas; /** exist instantiation ? */ @@ -142,7 +143,7 @@ public: // is quantifier active? bool isQuantifierActive( Node f ); //do exhaustive instantiation - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); //temporary stats int d_numQuantSat; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 7658f2b6b..7f560b74c 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -99,7 +99,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ } if( addedLemmas==0 ){ - Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; + Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; //CVC4 will answer SAT or unknown if( Trace.isOn("fmf-consistent") ){ Trace("fmf-consistent") << std::endl; @@ -113,6 +113,10 @@ bool ModelEngine::checkComplete() { return !d_incomplete_check; } +bool ModelEngine::checkCompleteFor( Node q ) { + return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end(); +} + void ModelEngine::registerQuantifier( Node f ){ if( Trace.isOn("fmf-warn") ){ bool canHandle = true; @@ -195,17 +199,18 @@ int ModelEngine::checkModel(){ // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; egetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i, true ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + Node q = fm->getAssertedQuantifier( i, true ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( considerQuantifiedFormula( f ) ){ - exhaustiveInstantiate( f, e ); + if( considerQuantifiedFormula( q ) ){ + exhaustiveInstantiate( q, e ); if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ break; } }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl; } } if( d_addedLemmas>0 ){ @@ -260,12 +265,16 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); mb->d_triedLemmas = 0; mb->d_addedLemmas = 0; - mb->d_incomplete_check = false; - if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ); + if( retEi!=0 ){ + if( retEi<0 ){ + Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; + d_incomplete_quants.push_back( f ); + }else{ + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + } d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; - d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ @@ -309,7 +318,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.isIncomplete(); + if( riter.isIncomplete() ){ + d_incomplete_quants.push_back( f ); + } } } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 12f18aa08..8575792b4 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -42,6 +42,8 @@ private: //temporary statistics //is the exhaustive instantiation incomplete? bool d_incomplete_check; + // set of quantified formulas for which check was incomplete + std::vector< Node > d_incomplete_quants; int d_addedLemmas; int d_triedLemmas; int d_totalLemmas; @@ -54,6 +56,7 @@ public: void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); + bool checkCompleteFor( Node q ); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 35b3e1f9e..df8533135 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -73,6 +73,11 @@ bool QuantDSplit::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty(); } +bool QuantDSplit::checkCompleteFor( Node q ) { + // true if we split q + return d_added_split.find( q )!=d_added_split.end(); +} + /* Call during quantifier engine's check */ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { //add lemmas ASAP (they are a reduction) diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index d36824998..3e3b08814 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -43,6 +43,7 @@ public: /* Called for new quantifiers */ void registerQuantifier( Node q ) {} void assertNode( Node n ) {} + bool checkCompleteFor( Node q ); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "QuantDSplit"; } }; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c3ddfacff..f4284a8ab 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -429,7 +429,7 @@ void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& vi for( unsigned i=0; i SAT + return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); +} + Node RewriteEngine::getInstConstNode( Node n, Node q ) { std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); if( it==d_inst_const_node[q].end() ){ diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 8d0678724..ef3337e53 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -56,6 +56,7 @@ public: void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); + bool checkCompleteFor( Node q ); /** Identify this module */ std::string identify() const { return "RewriteEngine"; } }; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e48c6eafe..fbfdb856e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -219,7 +219,6 @@ void QuantifiersEngine::finishInit(){ d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); d_modules.push_back( d_sg_gen ); } - //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules if( !options::finiteModelFind() || options::fmfInstEngine() ){ d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); @@ -395,13 +394,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_conflict = false; d_hasAddedLemma = false; bool setIncomplete = false; - if( e==Theory::EFFORT_LAST_CALL ){ - //sources of incompleteness - if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ - Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl; - setIncomplete = true; - } - } bool usedModelBuilder = false; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; @@ -544,20 +536,49 @@ void QuantifiersEngine::check( Theory::Effort e ){ } }else if( quant_e==QEFFORT_MODEL ){ if( e==Theory::EFFORT_LAST_CALL ){ + //sources of incompleteness if( !d_recorded_inst.empty() ){ + Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; setIncomplete = true; } //if we have a chance not to set incomplete if( !setIncomplete ){ setIncomplete = false; //check if we should set the incomplete flag - for( unsigned i=0; icheckComplete() ){ - Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl; + for( unsigned i=0; icheckComplete() ){ + Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl; setIncomplete = true; break; } } + if( !setIncomplete ){ + //look at individual quantified formulas, one module must claim completeness for each one + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ + bool hasCompleteM = false; + Node q = d_model->getAssertedQuantifier( i ); + QuantifiersModule * qmd = getOwner( q ); + if( qmd!=NULL ){ + hasCompleteM = qmd->checkCompleteFor( q ); + }else{ + for( unsigned j=0; jcheckCompleteFor( q ) ){ + qmd = d_modules[j]; + hasCompleteM = true; + break; + } + } + } + if( !hasCompleteM ){ + Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl; + setIncomplete = true; + break; + }else{ + Assert( qmd!=NULL ); + Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl; + } + } + } } //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL if( !setIncomplete ){ -- 2.30.2