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.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/combination_engine.h')
-rw-r--r-- | src/theory/combination_engine.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 4413da603..765a49d68 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -49,15 +49,8 @@ class CombinationEngine /** Finish initialization */ void finishInit(); - //-------------------------- equality engine /** Get equality engine theory information for theory with identifier tid. */ const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; - /** - * Get the "core" equality engine. This is the equality engine that - * quantifiers should use. - */ - eq::EqualityEngine* getCoreEqualityEngine(); - //-------------------------- end equality engine //-------------------------- model /** * Reset the model maintained by this class. This resets all local information |