diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 12:11:09 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 12:11:15 +0200 |
commit | c3992de261f0fa968f50349de1bdc3f9bef6ce6b (patch) | |
tree | 38308f6cdf2c502482bef56a9530e63f32376cb2 /src/theory/quantifiers_engine.cpp | |
parent | 41c09b51a7000fe5eb6b702d4ef9a1644129410b (diff) |
Refactor model builder from model engine to quant engine. Work on fairness strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 78 |
1 files changed, 69 insertions, 9 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index d17899cf2..09cae8eca 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,8 +25,6 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -//#include "theory/rewriterules/efficient_e_matching.h" -//#include "theory/rewriterules/rr_trigger.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/quant_conflict_find.h" @@ -35,6 +33,9 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/qinterval_builder.h" +#include "theory/quantifiers/ambqi_builder.h" using namespace std; using namespace CVC4; @@ -45,7 +46,7 @@ using namespace CVC4::theory::inst; eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { - return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); + return d_quantEngine->getMasterEqualityEngine(); } bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { @@ -80,7 +81,9 @@ d_lemmas_produced_c(u){ //d_rr_tr_trie = new rrinst::TriggerTrie; //d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; - + + bool needsBuilder = false; + Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object @@ -135,6 +138,7 @@ d_lemmas_produced_c(u){ } d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); + needsBuilder = true; }else{ d_model_engine = NULL; d_bint = NULL; @@ -151,12 +155,36 @@ d_lemmas_produced_c(u){ }else{ d_ceg_inst = NULL; } + + if( needsBuilder ){ + Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; + if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || + options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){ + Trace("quant-engine-debug") << "...make fmc builder." << std::endl; + d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); + }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ + Trace("quant-engine-debug") << "...make interval builder." << std::endl; + d_builder = new quantifiers::QIntervalBuilder( c, this ); + }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; + d_builder = new quantifiers::AbsMbqiBuilder( c, this ); + }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){ + Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl; + d_builder = new quantifiers::QModelBuilderInstGen( c, this ); + }else{ + Trace("quant-engine-debug") << "...make default model builder." << std::endl; + d_builder = new quantifiers::QModelBuilderDefault( c, this ); + } + }else{ + d_builder = NULL; + } //options d_total_inst_count_debug = 0; } QuantifiersEngine::~QuantifiersEngine(){ + delete d_builder; delete d_rr_engine; delete d_bint; delete d_model_engine; @@ -168,6 +196,8 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_tr_trie; delete d_term_db; delete d_eq_query; + delete d_sg_gen; + delete d_ceg_inst; for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } @@ -199,7 +229,7 @@ void QuantifiersEngine::finishInit(){ } } -QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { +QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ return NULL; @@ -214,7 +244,7 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { if( mo!=NULL ){ Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl; } - d_owner[q] = m; + d_owner[q] = m; } } @@ -247,6 +277,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; + Trace("quant-engine-ee") << "Equality engine : " << std::endl; + debugPrintEqualityEngine( "quant-engine-ee" ); + if( !getMasterEqualityEngine()->consistent() ){ Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; return; @@ -628,8 +661,8 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b } } } - //also check model engine (it may contain instantiations internally) - if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){ + //also check model builder (it may contain instantiations internally) + if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){ return true; } return false; @@ -881,7 +914,34 @@ QuantifiersEngine::Statistics::~Statistics(){ } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ - return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine(); + return getTheoryEngine()->getMasterEqualityEngine(); +} + +void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { + eq::EqualityEngine* ee = getMasterEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + bool firstTime = true; + Trace(c) << " " << r; + Trace(c) << " : { "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( r!=n ){ + if( firstTime ){ + Trace(c) << std::endl; + firstTime = false; + } + Trace(c) << " " << n << std::endl; + } + ++eqc_i; + } + if( !firstTime ){ Trace(c) << " "; } + Trace(c) << "}" << std::endl; + ++eqcs_i; + } + Trace(c) << std::endl; } void EqualityQueryQuantifiersEngine::reset(){ |