diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-16 17:18:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-16 17:18:05 -0500 |
commit | 54abd196cb43422c77a74cb139f3aaebaa695639 (patch) | |
tree | 2a65e959b8d17d06fc953320ae15575133b95d17 /src/theory | |
parent | 9c4d548af9a14c18a6d69b41bba3e36054d37c0c (diff) |
Remove equality inference option for quantifiers (#3282)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 43 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_query.h | 29 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 8 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 3 |
6 files changed, 17 insertions, 111 deletions
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()<ei->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<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; - /** equality inference class */ - std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; /** all triggers will be stored in this trie */ std::unique_ptr<inst::TriggerTrie> 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; |