From 54abd196cb43422c77a74cb139f3aaebaa695639 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Sep 2019 17:18:05 -0500 Subject: [PATCH] Remove equality inference option for quantifiers (#3282) --- src/options/quantifiers_options.toml | 9 ---- src/theory/quantifiers/equality_query.cpp | 43 ++----------------- src/theory/quantifiers/equality_query.h | 29 ++++++------- src/theory/quantifiers_engine.cpp | 27 ------------ src/theory/quantifiers_engine.h | 8 ---- src/theory/theory_engine.cpp | 18 -------- src/theory/theory_engine.h | 3 -- .../quantifiers/infer-arith-trigger-eq.smt2 | 2 - 8 files changed, 17 insertions(+), 122 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4398711b7..89ccd90b2 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -215,15 +215,6 @@ header = "options/quantifiers_options.h" read_only = true help = "consider ground terms within bodies of quantified formulas for matching" -[[option]] - name = "inferArithTriggerEq" - category = "regular" - long = "infer-arith-trigger-eq" - type = "bool" - default = "false" - read_only = true - help = "infer equalities for trigger terms based on solving arithmetic equalities" - [[option]] name = "strictTriggers" category = "regular" diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 22d6a3782..bb0306c06 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -32,8 +32,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ - +EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( + context::Context* c, QuantifiersEngine* qe) + : d_qe(qe), d_eqi_counter(c), d_reset_count(0) +{ } EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ @@ -42,43 +44,6 @@ EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ d_int_rep.clear(); d_reset_count++; - return processInferences( e ); -} - -bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { - if( options::inferArithTriggerEq() ){ - eq::EqualityEngine* ee = getEngine(); - //updated implementation - EqualityInference * ei = d_qe->getEqualityInference(); - while( d_eqi_counter.get()getNumPendingMerges() ){ - Node eq = ei->getPendingMerge( d_eqi_counter.get() ); - Node eq_exp = ei->getPendingMergeExplanation( d_eqi_counter.get() ); - Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; - Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl; - Assert( ee->hasTerm( eq[0] ) ); - Assert( ee->hasTerm( eq[1] ) ); - if( areDisequal( eq[0], eq[1] ) ){ - Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl; - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl; - if( !d_qe->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - //this should really never happen (implies arithmetic is incomplete when sharing is enabled) - Assert( false ); - } - Trace("term-db-lemma") << " add split on : " << eq << std::endl; - } - eq = Rewriter::rewrite(eq); - Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate()); - d_qe->addLemma(split); - return false; - }else{ - ee->assertEquality( eq, true, eq_exp ); - d_eqi_counter = d_eqi_counter.get() + 1; - } - } - Assert( ee->consistent() ); - } return true; } diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 1000b97e9..7766a335a 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -27,22 +27,19 @@ namespace theory { namespace quantifiers { /** EqualityQueryQuantifiersEngine class -* This is a wrapper class around an equality engine that is used for -* queries required by algorithms in the quantifiers theory. -* It uses an equality engine, as determined by the quantifiers engine it points -* to. -* -* The main extension of this class wrt EqualityQuery is the function -* getInternalRepresentative, which is used by instantiation-based methods -* that are agnostic with respect to choosing terms within an equivalence class. -* Examples of such methods are finite model finding and enumerative -* instantiation. -* Method getInternalRepresentative returns the "best" representative based on -* the internal heuristic, -* which is currently based on choosing the term that was previously chosen as a -* representative -* earliest. -*/ + * + * This is a wrapper class around an equality engine that is used for + * queries required by algorithms in the quantifiers theory. It uses an equality + * engine, as determined by the quantifiers engine it points to. + * + * The main extension of this class wrt EqualityQuery is the function + * getInternalRepresentative, which is used by instantiation-based methods + * that are agnostic with respect to choosing terms within an equivalence class. + * Examples of such methods are finite model finding and enumerative + * instantiation. Method getInternalRepresentative returns the "best" + * representative based on the internal heuristic, which is currently based on + * choosing the term that was previously chosen as a representative earliest. + */ class EqualityQueryQuantifiersEngine : public EqualityQuery { public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a6ec1c077..507d938b4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -188,7 +188,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te) : d_te(te), d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), - d_eq_inference(nullptr), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_rel_dom(nullptr), @@ -237,9 +236,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify()); } - if( options::inferArithTriggerEq() ){ - d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); - } d_util.push_back(d_instantiate.get()); @@ -328,10 +324,6 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() const { return d_eq_query.get(); } -quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const -{ - return d_eq_inference.get(); -} quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const { return d_rel_dom.get(); @@ -1040,25 +1032,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); - if( d_eq_inference ){ - d_eq_inference->eqNotifyNewClass( t ); - } -} - -void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) { - if( d_eq_inference ){ - d_eq_inference->eqNotifyMerge( t1, t2 ); - } -} - -void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) { - -} - -void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - //if( d_qcf ){ - // d_qcf->assertDisequal( t1, t2 ); - //} } bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0a534d090..e1fc742af 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -25,7 +25,6 @@ #include "expr/attribute.h" #include "expr/term_canonize.h" #include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" @@ -106,8 +105,6 @@ public: inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities //---------------------- utilities (TODO move these utilities #1163) - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() const; //---------------------- end utilities @@ -228,9 +225,6 @@ public: void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); /** use model equality engine */ bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ @@ -316,8 +310,6 @@ public: //------------- quantifiers utilities /** equality query class */ std::unique_ptr d_eq_query; - /** equality inference class */ - std::unique_ptr d_eq_inference; /** all triggers will be stored in this trie */ std::unique_ptr d_tr_trie; /** extended model object */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b8f6bf15c..8348c24d5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -260,24 +260,6 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ } } -void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ - if (d_logicInfo.isQuantified()) { - d_quantEngine->eqNotifyPreMerge( t1, t2 ); - } -} - -void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ - if (d_logicInfo.isQuantified()) { - d_quantEngine->eqNotifyPostMerge( t1, t2 ); - } -} - -void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ - if (d_logicInfo.isQuantified()) { - d_quantEngine->eqNotifyDisequal( t1, t2, reason ); - } -} - TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveTermFormulas& iteRemover, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 23d3282de..587d3693c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -174,15 +174,12 @@ class TheoryEngine { void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); } void eqNotifyPreMerge(TNode t1, TNode t2) override { - d_te.eqNotifyPreMerge(t1, t2); } void eqNotifyPostMerge(TNode t1, TNode t2) override { - d_te.eqNotifyPostMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override { - d_te.eqNotifyDisequal(t1, t2, reason); } };/* class TheoryEngine::NotifyClass */ NotifyClass d_masterEENotify; diff --git a/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 index 08d922a65..c19a18f73 100644 --- a/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 +++ b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --infer-arith-trigger-eq -; EXPECT: unsat (set-info :smt-lib-version 2.6) (set-logic UFLIA) (set-info :status unsat) -- 2.30.2