diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-18 14:13:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 14:13:17 -0700 |
| commit | 005b6458d3340dd805279eb4c442d2871d75c844 (patch) | |
| tree | 137249805212631349ae0f28b77193bbdd321af5 /src/theory/quantifiers_engine.cpp | |
| parent | 8e66e8dfb1a7f54c8982141bdbbc1dfe914e5900 (diff) | |
| parent | aa8da1ff4e7f119408dbf14074b9a5efcb06618b (diff) | |
Merge branch 'master' into regDisableProofs
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 8 |
1 files changed, 7 insertions, 1 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 ){ |