diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
commit | af86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32 (patch) | |
tree | d86858d67279e940a225e7ca693172685532d6d7 /src/theory/quantifiers_engine.cpp | |
parent | aaf1bbbdc6e42910e07db64441885ee3476d86df (diff) |
Promote InstStrategyCbqi to quantifier module. Cleanup unused code.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 71 |
1 files changed, 40 insertions, 31 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 913d9b0c6..9ae3b1d40 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -40,6 +40,7 @@ #include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/quant_equality_engine.h" #include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/inst_strategy_cbqi.h" using namespace std; using namespace CVC4; @@ -128,15 +129,18 @@ d_presolve_cache_wic(u){ d_sg_gen = NULL; } //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules - if( !options::finiteModelFind() || options::fmfInstEngine() || options::cbqi() ){ + if( !options::finiteModelFind() || options::fmfInstEngine() ){ d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); - if( options::cbqi() && options::cbqiModel() ){ - needsBuilder = true; - } }else{ d_inst_engine = NULL; } + //counterexample-based instantiation (initialized during finishInit) + d_i_cbqi = NULL; + if( options::cbqi() && options::cbqiModel() ){ + needsBuilder = true; + } + //finite model finding if( options::finiteModelFind() ){ if( options::fmfBoundInt() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); @@ -243,9 +247,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_fun_def_engine; delete d_uee; delete d_fs; - for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { - delete (*i).second; - } + delete d_i_cbqi; } EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { @@ -270,6 +272,18 @@ Valuation& QuantifiersEngine::getValuation(){ void QuantifiersEngine::finishInit(){ Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl; + //counterexample-based quantifier instantiation + if( options::cbqi() ){ + if( options::cbqiSplx() ){ + d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this ); + d_modules.push_back( d_i_cbqi ); + }else{ + d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); + d_modules.push_back( d_i_cbqi ); + } + }else{ + d_i_cbqi = NULL; + } for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->finishInit(); } @@ -449,12 +463,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_LAST_CALL && quant_e==QEFFORT_MODEL ){ //if we have a chance not to set incomplete if( !setIncomplete ){ - setIncomplete = true; + setIncomplete = false; //check if we should set the incomplete flag for( unsigned i=0; i<qm.size(); i++ ){ - if( qm[i]->checkComplete() ){ - Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl; - setIncomplete = false; + if( !qm[i]->checkComplete() ){ + Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl; + setIncomplete = true; break; } } @@ -571,7 +585,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ } Node ceBody = d_term_db->getInstConstantBody( f ); //generate the phase requirements - d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); + //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); //also register it with the strong solver //if( options::finiteModelFind() ){ // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); @@ -1043,23 +1057,6 @@ void QuantifiersEngine::flushLemmas(){ } } -void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ - if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){ - // doing literal-based matching (consider polarity of literals) - for( int i=0; i<(int)nodes.size(); i++ ){ - Node prev = nodes[i]; - if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ - bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); - nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) ); - } - //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ - // Node req = qe->getPhaseReqEquality( f, trNodes[i] ); - // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req ); - //} - } - } -} - void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool printed = false; for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ @@ -1113,7 +1110,11 @@ QuantifiersEngine::Statistics::Statistics(): d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0) + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), + d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), + d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), + d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), + d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -1126,7 +1127,11 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); StatisticsRegistry::registerStat(&d_red_alpha_equiv); - StatisticsRegistry::registerStat(&d_red_lte_partial_inst); + StatisticsRegistry::registerStat(&d_red_lte_partial_inst); + StatisticsRegistry::registerStat(&d_instantiations_user_patterns); + StatisticsRegistry::registerStat(&d_instantiations_auto_gen); + StatisticsRegistry::registerStat(&d_instantiations_guess); + StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); } QuantifiersEngine::Statistics::~Statistics(){ @@ -1142,6 +1147,10 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); + StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns); + StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen); + StatisticsRegistry::unregisterStat(&d_instantiations_guess); + StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ |