diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 13:27:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-28 13:27:27 -0600 |
| commit | 3234db430074e278258e6d687c07146a59769a92 (patch) | |
| tree | 17db55e1ff335c3998e1c4e172d174dc9f6e3b21 /src/theory/ee_manager_distributed.h | |
| parent | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (diff) | |
Use standard equality engine information in quantifiers state (#5824)
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
Diffstat (limited to 'src/theory/ee_manager_distributed.h')
| -rw-r--r-- | src/theory/ee_manager_distributed.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index c7c1e7f4c..9578706d9 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -52,8 +52,9 @@ class EqEngineManagerDistributed : public EqEngineManager * per theories and connects them to a master equality engine. */ void initializeTheories() override; - /** get the core equality engine */ - eq::EqualityEngine* getCoreEqualityEngine() override; + /** Notify model */ + void notifyModel(bool incomplete) override; + private: /** notify class for master equality engine */ class MasterNotifyClass : public theory::eq::EqualityEngineNotify |