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.

1 files changed, 4 insertions, 9 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a51c0ecdc..e3d7909b7 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -24,7 +24,9 @@
 namespace CVC4 {
 namespace theory {
 
-class EqualityQuery;
+namespace quantifiers {
+class QuantifiersState;
+}
 
 namespace inst {
 
@@ -50,13 +52,6 @@ public:
    * not already initialized in this match.
    */
   void add(InstMatch& m);
-  /** merge with match m
-   *
-   * This method returns true if the merge was successful, that is, all jointly
-   * initialized fields of this class and m are equivalent modulo the equalities
-   * given by q.
-   */
-  bool merge( EqualityQuery* q, InstMatch& m );
   /** is this complete, i.e. are all fields non-null? */
   bool isComplete();
   /** is this empty, i.e. are all fields the null node? */
@@ -87,7 +82,7 @@ public:
    * This method returns true if the i^th field was previously uninitialized,
    * or is equivalent to n modulo the equalities given by q.
    */
-  bool set(EqualityQuery* q, size_t i, TNode n);
+  bool set(quantifiers::QuantifiersState& qs, size_t i, TNode n);
 };
 
 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {