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, 32 deletions

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index b82b9ae64..a3f895f54 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -29,11 +29,7 @@ namespace quantifiers {
 
 /** EqualityQueryQuantifiersEngine class
  *
- * This is a wrapper class around an equality engine that is used for
- * queries required by algorithms in the quantifiers theory. It uses an equality
- * engine, as determined by the quantifiers engine it points to.
- *
- * The main extension of this class wrt EqualityQuery is the function
+ * The main method of this class is the function
  * getInternalRepresentative, which is used by instantiation-based methods
  * that are agnostic with respect to choosing terms within an equivalence class.
  * Examples of such methods are finite model finding and enumerative
@@ -41,7 +37,7 @@ namespace quantifiers {
  * representative based on the internal heuristic, which is currently based on
  * choosing the term that was previously chosen as a representative earliest.
  */
-class EqualityQueryQuantifiersEngine : public EqualityQuery
+class EqualityQueryQuantifiersEngine : public QuantifiersUtil
 {
  public:
   EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
@@ -52,32 +48,6 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
   void registerQuantifier(Node q) override {}
   /** identify */
   std::string identify() const override { return "EqualityQueryQE"; }
-  /** does the equality engine have term a */
-  bool hasTerm(Node a) override;
-  /** get the representative of a */
-  Node getRepresentative(Node a) override;
-  /** are a and b equal? */
-  bool areEqual(Node a, Node b) override;
-  /** are a and b disequal? */
-  bool areDisequal(Node a, Node b) override;
-  /** get equality engine
-  * This may either be the master equality engine or the model's equality
-  * engine.
-  */
-  eq::EqualityEngine* getEngine() override;
-  /** get list of members in the equivalence class of a */
-  void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
-  /** get congruent term
-  * If possible, returns a term n such that:
-  * (1) n is a term in the equality engine from getEngine().
-  * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
-  * of args[i] for i=1...k
-  * Otherwise, returns the null node.
-  *
-  * Notice that f should be a "match operator", returned by
-  * TermDb::getMatchOperator.
-  */
-  TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
   /** gets the current best representative in the equivalence
    * class of a, based on some heuristic. Currently, the default heuristic
    * chooses terms that were previously chosen as representatives
@@ -97,6 +67,8 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
  private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
+  /** the quantifiers state */
+  QuantifiersState& d_qstate;
   /** quantifiers equality inference */
   context::CDO< unsigned > d_eqi_counter;
   /** internal representatives */