Move equality query utility into quantifiers model (#6186)

This simplifies the initialization of quantifiers engine.

This PR also makes general improvements to EqualityQuery.

1 files changed, 12 insertions, 12 deletions

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 6dec66b5c..887c54f42 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -21,15 +21,15 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 class FirstOrderModel;
+class QuantifiersState;
 
-/** EqualityQueryQuantifiersEngine class
+/** EqualityQuery class
  *
  * The main method of this class is the function
  * getInternalRepresentative, which is used by instantiation-based methods
@@ -39,18 +39,18 @@ class FirstOrderModel;
  * 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 QuantifiersUtil
+class EqualityQuery : public QuantifiersUtil
 {
  public:
-  EqualityQueryQuantifiersEngine(QuantifiersState& qs,
-                                 FirstOrderModel* m);
-  virtual ~EqualityQueryQuantifiersEngine();
+  EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
+  virtual ~EqualityQuery();
+
   /** reset */
   bool reset(Theory::Effort e) override;
   /* Called for new quantifiers */
   void registerQuantifier(Node q) override {}
   /** identify */
-  std::string identify() const override { return "EqualityQueryQE"; }
+  std::string identify() const override { return "EqualityQuery"; }
   /** 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
@@ -65,7 +65,7 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
    * Node::null() if all terms in the equivalence class of a
    * are ineligible.
    */
-  Node getInternalRepresentative(Node a, Node q, int index);
+  Node getInternalRepresentative(Node a, Node q, size_t index);
 
  private:
   /** the quantifiers state */
@@ -77,16 +77,16 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
   /** internal representatives */
   std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
-  std::map< Node, int > d_rep_score;
+  std::map<Node, int32_t> d_rep_score;
   /** the number of times reset( e ) has been called */
-  int d_reset_count;
+  size_t d_reset_count;
   /** processInferences : will merge equivalence classes in master equality engine, if possible */
   bool processInferences( Theory::Effort e );
   /** node contains */
   Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
-  int getRepScore( Node n, Node f, int index, TypeNode v_tn );
-}; /* EqualityQueryQuantifiersEngine */
+  int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn);
+}; /* EqualityQuery */
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */