diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:49:51 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:50:08 -0500 |
commit | fa5df1aad69f8ad62686b9418070a1baf74b4a77 (patch) | |
tree | ad780365050498223b2a3fceb703556713cb49d0 /src/theory/quantifiers_engine.cpp | |
parent | 599329b76da2e95f18479a19c1bbbc3e3228b100 (diff) |
Add quantifiers options related to model and master equality engine.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 65 |
1 files changed, 54 insertions, 11 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b369e30b7..db0efd988 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -91,6 +91,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_curr_effort_level = QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; + d_useModelEe = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -383,7 +384,21 @@ void QuantifiersEngine::ppNotifyAssertions( void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_statistics.d_time); - if( !getMasterEqualityEngine()->consistent() ){ + d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL ); + // if we want to use the model's equality engine, build the model now + if( d_useModelEe && !d_model->isBuilt() ){ + Trace("quant-engine-debug") << "Build the model." << std::endl; + if( !d_te->getModelBuilder()->buildModel( d_model ) ){ + //we are done if model building was unsuccessful + flushLemmas(); + if( d_hasAddedLemma ){ + Trace("quant-engine-debug") << "...failed." << std::endl; + return; + } + } + } + + if( !getActiveEqualityEngine()->consistent() ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } @@ -505,7 +520,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ d_curr_effort_level = quant_e; - bool success = true; //build the model if any module requested it if( needsModelE==quant_e && !d_model->isBuilt() ){ // theory engine's model builder is quantifier engine's builder if it has one @@ -513,11 +527,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Build model..." << std::endl; if( !d_te->getModelBuilder()->buildModel( d_model ) ){ //we are done if model building was unsuccessful - Trace("quant-engine-debug") << "...failed." << std::endl; - success = false; + Trace("quant-engine-debug") << "...added lemmas." << std::endl; + flushLemmas(); } } - if( success ){ + if( !d_hasAddedLemma ){ //check each module for( unsigned i=0; i<qm.size(); i++ ){ Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl; @@ -527,9 +541,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ break; } } + //flush all current lemmas + flushLemmas(); } - //flush all current lemmas - flushLemmas(); //if we have added one, stop if( d_hasAddedLemma ){ break; @@ -1084,7 +1098,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); + terms[i] = getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() ); @@ -1178,6 +1192,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; body = Rewriter::rewrite(body); + + if( d_useModelEe && options::instNoModelTrue() ){ + Node val_body = d_model->getValue( body ); + if( val_body==d_term_db->d_true ){ + Trace("inst-add-debug") << " --> True in model." << std::endl; + ++(d_statistics.d_inst_duplicate_model_true); + return false; + } + } + Node lem; if( rlv_cond.empty() ){ lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); @@ -1571,6 +1595,7 @@ QuantifiersEngine::Statistics::Statistics() d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0), + d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), @@ -1596,6 +1621,7 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_inst_duplicate); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true); smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); @@ -1623,6 +1649,7 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true); smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); @@ -1640,11 +1667,27 @@ QuantifiersEngine::Statistics::~Statistics(){ } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ - return getTheoryEngine()->getMasterEqualityEngine(); + return d_te->getMasterEqualityEngine(); +} + +eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() { + if( d_useModelEe ){ + return d_model->d_equalityEngine; + }else{ + return d_te->getMasterEqualityEngine(); + } +} + +Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ + bool prevModelEe = d_useModelEe; + d_useModelEe = false; + Node ret = d_eq_query->getInternalRepresentative( a, q, index ); + d_useModelEe = prevModelEe; + return ret; } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { - eq::EqualityEngine* ee = getMasterEqualityEngine(); + eq::EqualityEngine* ee = getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ @@ -1922,7 +1965,7 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getMasterEqualityEngine(); + return d_qe->getActiveEqualityEngine(); } void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ |