diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 13:05:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-18 13:05:04 -0500 |
commit | 944cb8e5381c47ccc49955a19609921399bb9437 (patch) | |
tree | 788411c7f26ceedc7f75e2eb9d591ebb6860b5fd /src/theory | |
parent | ab9742939d7706e10ea3d70c73275e97a5235f03 (diff) |
Quantifiers engine stores a pointer to the master equality engine (#4908)
This is work towards a configurable approach to theory combination.
Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 |
4 files changed, 22 insertions, 10 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eafcc1e85..9fdf7e7aa 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -176,6 +176,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te) : d_te(te), + d_masterEqualityEngine(nullptr), d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), @@ -274,6 +275,11 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, QuantifiersEngine::~QuantifiersEngine() {} +void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee) +{ + d_masterEqualityEngine = mee; +} + context::Context* QuantifiersEngine::getSatContext() { return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext(); @@ -1258,7 +1264,7 @@ QuantifiersEngine::Statistics::~Statistics(){ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const { - return d_te->getMasterEqualityEngine(); + return d_masterEqualityEngine; } Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index dd86c0db9..eca108587 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -49,6 +49,7 @@ class QuantifiersEnginePrivate; // TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { + friend class ::CVC4::TheoryEngine; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDList<Node> NodeList; typedef context::CDList<bool> BoolList; @@ -102,6 +103,10 @@ public: inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities private: + //---------------------- private initialization + /** Set the master equality engine */ + void setMasterEqualityEngine(eq::EqualityEngine* mee); + //---------------------- end private initialization /** * Maps quantified formulas to the module that owns them, if any module has * specifically taken ownership of it. @@ -316,6 +321,8 @@ public: private: /** reference to theory engine object */ TheoryEngine* d_te; + /** Pointer to the master equality engine */ + eq::EqualityEngine* d_masterEqualityEngine; /** vector of utilities for quantifiers */ std::vector<QuantifiersUtil*> d_util; /** vector of modules for quantifiers */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 07c160058..e86a09112 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -159,6 +159,13 @@ void TheoryEngine::finishInit() { d_aloc_curr_model_builder = true; } + // set the core equality engine on quantifiers engine + if (d_logicInfo.isQuantified()) + { + d_quantEngine->setMasterEqualityEngine( + d_eeDistributed->getMasterEqualityEngine()); + } + // finish initializing the theories for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { Theory* t = d_theoryTable[theoryId]; @@ -545,7 +552,7 @@ void TheoryEngine::check(Theory::Effort effort) { if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { // case where we are about to answer SAT, the master equality engine, // if it exists, must be consistent. - eq::EqualityEngine* mee = getMasterEqualityEngine(); + eq::EqualityEngine* mee = d_eeDistributed->getMasterEqualityEngine(); if (mee != NULL) { AlwaysAssert(mee->consistent()); @@ -1807,12 +1814,6 @@ SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase() return &d_sharedTerms; } -theory::eq::EqualityEngine* TheoryEngine::getMasterEqualityEngine() -{ - Assert(d_eeDistributed != nullptr); - return d_eeDistributed->getMasterEqualityEngine(); -} - void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index aa23aa29b..bedd54130 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -738,8 +738,6 @@ public: SharedTermsDatabase* getSharedTermsDatabase(); - theory::eq::EqualityEngine* getMasterEqualityEngine(); - SortInference* getSortInference() { return &d_sortInfer; } /** Prints the assertions to the debug stream */ |