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/theory_state.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/theory_state.h')
| -rw-r--r-- | src/theory/theory_state.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 7c2a044bf..891016f0a 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -60,6 +60,8 @@ class TheoryState * returns true if the representative of a and b are distinct constants. */ virtual bool areDisequal(TNode a, TNode b) const; + /** get list of members in the equivalence class of a */ + virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const; /** get equality engine */ eq::EqualityEngine* getEqualityEngine() const; //-------------------------------------- end equality information |