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/combination_engine.cpp | |
| 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/combination_engine.cpp')
| -rw-r--r-- | src/theory/combination_engine.cpp | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 5e242659f..71eac49a0 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -77,21 +77,11 @@ const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const return d_eemanager->getEeTheoryInfo(tid); } -eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine() -{ - return d_eemanager->getCoreEqualityEngine(); -} - void CombinationEngine::resetModel() { d_mmanager->resetModel(); } void CombinationEngine::postProcessModel(bool incomplete) { - // should have a consistent core equality engine - eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine(); - if (mee != nullptr) - { - AlwaysAssert(mee->consistent()); - } + d_eemanager->notifyModel(incomplete); // postprocess with the model d_mmanager->postProcessModel(incomplete); } |