diff options
-rw-r--r-- | src/options/quantifiers_options.toml | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 36 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 6 |
8 files changed, 26 insertions, 94 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b62468cdd..4b130158c 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -493,15 +493,6 @@ header = "options/quantifiers_options.h" help = "allow theory combination to happen once initially, before quantifier strategies are run" [[option]] - name = "quantModelEe" - category = "regular" - long = "quant-model-ee" - type = "bool" - default = "false" - read_only = true - help = "use equality engine of model for last call effort" - -[[option]] name = "instMaxLevel" category = "regular" long = "inst-max-level=N" @@ -824,14 +815,6 @@ header = "options/quantifiers_options.h" help = "do not consider instances of quantified formulas that are currently entailed" [[option]] - name = "instNoModelTrue" - category = "regular" - long = "inst-no-model-true" - type = "bool" - default = "false" - help = "do not consider instances of quantified formulas that are currently true in model, if it is available" - -[[option]] name = "qcfEagerTest" category = "regular" long = "qcf-eager-test" diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 94e60513c..feaa0f223 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -182,7 +182,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getActiveEqualityEngine(); + return d_qe->getMasterEqualityEngine(); } void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index c9048fc95..77b61e9dd 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -242,17 +242,6 @@ bool Instantiate::addInstantiation( // construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; - if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue()) - { - Node val_body = d_qe->getModel()->getValue(body); - if (val_body.isConst() && val_body.getConst<bool>()) - { - Trace("inst-add-debug") << " --> True in model." << std::endl; - ++(d_statistics.d_inst_duplicate_model_true); - return false; - } - } - Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body); lem = Rewriter::rewrite(lem); @@ -845,14 +834,12 @@ Instantiate::Statistics::Statistics() : d_instantiations("Instantiate::Instantiations_Total", 0), d_inst_duplicate("Instantiate::Duplicate_Inst", 0), d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0), - d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0), - d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0) + d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0) { smtStatisticsRegistry()->registerStat(&d_instantiations); smtStatisticsRegistry()->registerStat(&d_inst_duplicate); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true); } Instantiate::Statistics::~Statistics() @@ -861,7 +848,6 @@ Instantiate::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); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 16ff1f2c3..cb40bbbbc 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -305,7 +305,6 @@ class Instantiate : public QuantifiersUtil IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; - IntStat d_inst_duplicate_model_true; Statistics(); ~Statistics(); }; /* class Instantiate::Statistics */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index a8eda10bb..cb1207912 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -32,7 +32,7 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const { - return d_quantEngine->getActiveEqualityEngine(); + return d_quantEngine->getMasterEqualityEngine(); } bool QuantifiersModule::areEqual(TNode n1, TNode n2) const diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7caa103a0..6e5dca4ef 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -249,7 +249,7 @@ void TermDb::addTerm(Node n, void TermDb::computeArgReps( TNode n ) { if (d_arg_reps.find(n) == d_arg_reps.end()) { - eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); for (const TNode& nc : n) { TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc; @@ -272,7 +272,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { { ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); } - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); for (const Node& ff : ops) { for (const TNode& n : d_op_map[ff]) @@ -307,7 +307,7 @@ void TermDb::computeUfTerms( TNode f ) { unsigned nonCongruentCount = 0; unsigned alreadyCongruentCount = 0; unsigned relevantCount = 0; - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); NodeManager* nm = NodeManager::currentNM(); for (const Node& ff : ops) { @@ -503,8 +503,8 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { f = getOperatorRepresentative( f ); } computeUfTerms( f ); - Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r) - || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r) + Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r) + || d_quantEngine->getMasterEqualityEngine()->getRepresentative(r) == r); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ @@ -905,22 +905,18 @@ void TermDb::setTermInactive( Node n ) { bool TermDb::hasTermCurrent( Node n, bool useMode ) { if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); - }else{ - //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE - if (options::termDbMode() == options::TermDbMode::ALL) - { - return true; - } - else if (options::termDbMode() == options::TermDbMode::RELEVANT) - { - return d_has_map.find( n )!=d_has_map.end(); - } - else - { - Assert(false); - return false; - } } + //some assertions are not sent to EE + if (options::termDbMode() == options::TermDbMode::ALL) + { + return true; + } + else if (options::termDbMode() == options::TermDbMode::RELEVANT) + { + return d_has_map.find( n )!=d_has_map.end(); + } + Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode(); + return false; } bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) @@ -966,7 +962,7 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); if( it==d_term_elig_eqc.end() ){ Node h; - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while (!eqc_i.isFinished()) { @@ -1021,7 +1017,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_func_map_rel_dom.clear(); d_consistent_ee = true; - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); Assert(ee->consistent()); // if higher-order, add equalities for the purification terms now diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bb5950c5e..eafcc1e85 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -223,7 +223,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; - d_useModelEe = false; //don't add true lemma d_lemmas_produced_c[d_term_util->d_true] = true; @@ -513,22 +512,9 @@ void QuantifiersEngine::ppNotifyAssertions( void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_statistics.d_time); - 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.get())) - { - //we are done if model building was unsuccessful - flushLemmas(); - if( d_hasAddedLemma ){ - Trace("quant-engine-debug") << "...failed." << std::endl; - return; - } - } - } - - if( !getActiveEqualityEngine()->consistent() ){ + + if (!getMasterEqualityEngine()->consistent()) + { Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } @@ -1275,20 +1261,8 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const return d_te->getMasterEqualityEngine(); } -eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const -{ - if( d_useModelEe ){ - return d_model->getEqualityEngine(); - } - 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; + return d_eq_query->getInternalRepresentative(a, q, index); } bool QuantifiersEngine::getSynthSolutions( @@ -1298,7 +1272,7 @@ bool QuantifiersEngine::getSynthSolutions( } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { - eq::EqualityEngine* ee = getActiveEqualityEngine(); + eq::EqualityEngine* ee = getMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index a4d858b16..dd86c0db9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -74,8 +74,6 @@ public: //---------------------- utilities /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() const; - /** get the active equality engine */ - eq::EqualityEngine* getActiveEqualityEngine() const; /** get equality query */ EqualityQuery* getEqualityQuery() const; /** get the model builder */ @@ -228,8 +226,6 @@ public: void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); - /** use model equality engine */ - bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); /** get internal representative @@ -364,8 +360,6 @@ public: context::CDO<bool> d_conflict_c; /** has added lemma this round */ bool d_hasAddedLemma; - /** whether to use model equality engine */ - bool d_useModelEe; //------------- end temporary information during check private: /** list of all quantifiers seen */ |