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/quantifiers_engine.h | |
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/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 7 |
1 files changed, 7 insertions, 0 deletions
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 */ |