Move equality query utility into quantifiers model (#6186)

This simplifies the initialization of quantifiers engine.

This PR also makes general improvements to EqualityQuery.

10 files changed, 74 insertions, 74 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 4a1a21798..4cc912e45 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -18,6 +18,7 @@
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -193,7 +194,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
       if( !nh.isNull() ){
         if (options::instMaxLevel() != -1)
         {
-          nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
+          nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index);
           //don't consider this if already the instantiation is ineligible
           if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
           {
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index b94076c9f..48e5682f2 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -17,6 +17,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -27,8 +28,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
-    QuantifiersState& qs, FirstOrderModel* m)
+EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m)
     : d_qstate(qs),
       d_model(m),
       d_eqi_counter(qs.getSatContext()),
@@ -36,18 +36,16 @@ EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
 {
 }
 
-EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
-}
+EqualityQuery::~EqualityQuery() {}
 
-bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
+bool EqualityQuery::reset(Theory::Effort e)
+{
   d_int_rep.clear();
   d_reset_count++;
   return true;
 }
 
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
-                                                               Node q,
-                                                               int index)
+Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
 {
   Assert(q.isNull() || q.getKind() == FORALL);
   Node r = d_qstate.getRepresentative(a);
@@ -74,7 +72,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
   if (options::quantRepMode() == options::QuantRepMode::EE)
   {
-    int score = getRepScore(r, q, index, v_tn);
+    int32_t score = getRepScore(r, q, index, v_tn);
     if (score >= 0)
     {
       return r;
@@ -94,10 +92,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   Trace("internal-rep-select")
       << "Choose representative for equivalence class : " << eqc
       << ", type = " << v_tn << std::endl;
-  int r_best_score = -1;
+  int32_t r_best_score = -1;
   for (const Node& n : eqc)
   {
-    int score = getRepScore(n, q, index, v_tn);
+    int32_t score = getRepScore(n, q, index, v_tn);
     if (score != -2)
     {
       if (r_best.isNull()
@@ -143,7 +141,11 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
 
 //helper functions
 
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
+Node EqualityQuery::getInstance(
+    Node n,
+    const std::vector<Node>& eqc,
+    std::unordered_map<TNode, Node, TNodeHashFunction>& cache)
+{
   if(cache.find(n) != cache.end()) {
     return cache[n];
   }
@@ -161,10 +163,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
 }
 
 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore(Node n,
-                                                Node q,
-                                                int index,
-                                                TypeNode v_tn)
+int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
 {
   if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
     return -2;
@@ -174,21 +173,16 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
     //score prefer lowest instantiation level
     if( n.hasAttribute(InstLevelAttribute()) ){
       return n.getAttribute(InstLevelAttribute());
-    }else{
-      return options::instLevelInputOnly() ? -1 : 0;
-    }
-  }else{
-    if (options::quantRepMode() == options::QuantRepMode::FIRST)
-    {
-      //score prefers earliest use of this term as a representative
-      return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
-    }
-    else
-    {
-      Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
-      return quantifiers::TermUtil::getTermDepth( n );
     }
+    return options::instLevelInputOnly() ? -1 : 0;
+  }
+  else if (options::quantRepMode() == options::QuantRepMode::FIRST)
+  {
+    // score prefers earliest use of this term as a representative
+    return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
   }
+  Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
+  return quantifiers::TermUtil::getTermDepth(n);
 }
 
 } /* CVC4::theory::quantifiers namespace */
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 */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 001c2f62a..fd84dc500 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -23,10 +23,8 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory::quantifiers::fmcheck;
 
 namespace CVC4 {
 namespace theory {
@@ -51,6 +49,7 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
       d_qe(nullptr),
       d_qreg(qr),
       d_treg(tr),
+      d_eq_query(qs, this),
       d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {
@@ -59,6 +58,11 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
 //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
 void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
 
+Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
+{
+  return d_eq_query.getInternalRepresentative(a, q, index);
+}
+
 void FirstOrderModel::assertQuantifier( Node n ){
   if( n.getKind()==FORALL ){
     d_forall_asserts.push_back( n );
@@ -163,6 +167,8 @@ bool FirstOrderModel::isModelBasis(TNode n)
   return n.getAttribute(ModelBasisAttribute());
 }
 
+EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; }
+
 /** needs check */
 bool FirstOrderModel::checkNeeded() {
   return d_forall_asserts.size()>0;
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index c2660d933..b86abd960 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -18,7 +18,7 @@
 #define CVC4__FIRST_ORDER_MODEL_H
 
 #include "context/cdlist.h"
-#include "expr/attribute.h"
+#include "theory/quantifiers/equality_query.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
 
@@ -33,13 +33,6 @@ class QuantifiersState;
 class TermRegistry;
 class QuantifiersRegistry;
 
-namespace fmcheck {
-  class FirstOrderModelFmc;
-}/* CVC4::theory::quantifiers::fmcheck namespace */
-
-struct IsStarAttributeId {};
-typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
-
 // TODO (#1301) : document and refactor this class
 class FirstOrderModel : public TheoryModel
 {
@@ -52,6 +45,17 @@ class FirstOrderModel : public TheoryModel
   //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
   /** finish initialize */
   void finishInit(QuantifiersEngine* qe);
+  /** get internal representative
+   *
+   * Choose a term that is equivalent to a in the current context that is the
+   * best term for instantiating the index^th variable of quantified formula q.
+   * If no legal term can be found, we return null. This can occur if:
+   * - a's type is not a subtype of the type of the index^th variable of q,
+   * - a is in an equivalent class with all terms that are restricted not to
+   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
+   * guided instantiation.
+   */
+  Node getInternalRepresentative(Node a, Node q, size_t index);
 
   /** assert quantifier */
   void assertQuantifier( Node n );
@@ -127,6 +131,8 @@ class FirstOrderModel : public TheoryModel
    * Has the term been marked as a model basis term?
    */
   static bool isModelBasis(TNode n);
+  /** Get the equality query */
+  EqualityQuery* getEqualityQuery();
 
  protected:
   //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
@@ -135,6 +141,8 @@ class FirstOrderModel : public TheoryModel
   QuantifiersRegistry& d_qreg;
   /** Reference to the term registry */
   TermRegistry& d_treg;
+  /** equality query class */
+  EqualityQuery d_eq_query;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** 
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 252261b9c..9577e296b 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 
+#include "expr/attribute.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/rewriter.h"
 
@@ -24,6 +25,15 @@ namespace theory {
 namespace quantifiers {
 namespace fmcheck {
 
+/**
+ * Marks that a term represents the entire domain of quantified formula for
+ * the finite model finding fmc algorithm.
+ */
+struct IsStarAttributeId
+{
+};
+using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
+
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
                                        QuantifiersRegistry& qr,
                                        TermRegistry& tr,
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 257926737..789a7bd7c 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -166,7 +166,7 @@ int ModelEngine::checkModel(){
       Trace("model-engine-debug") << std::endl;
       Trace("model-engine-debug") << "   Term reps : ";
       for( size_t i=0; i<it->second.size(); i++ ){
-        Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
         if (r.isNull())
         {
           // there was an invalid equivalence class
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 6c8d826cb..be6101b81 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       // pick the best possible representative for instantiation, based on past
       // use and simplicity of term
-      terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
+      terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i);
     }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if (terms[i].isNull())
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7d5c4cf19..68962de72 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,7 +62,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_treg(tr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(qm),
-      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)),
       d_instantiate(
           new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
       d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
@@ -70,7 +69,7 @@ QuantifiersEngine::QuantifiersEngine(
       d_quants_red(qstate.getUserContext())
 {
   // initialize the utilities
-  d_util.push_back(d_eq_query.get());
+  d_util.push_back(d_model->getEqualityQuery());
   // quantifiers registry must come before the remaining utilities
   d_util.push_back(&d_qreg);
   d_util.push_back(tr.getTermDatabase());
@@ -711,10 +710,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
 }
 
-Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
-  return d_eq_query->getInternalRepresentative(a, q, index);
-}
-
 Node QuantifiersEngine::getNameForQuant(Node q) const
 {
   return d_qreg.getNameForQuant(q);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 625bac40a..4d3029ca9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -40,7 +40,6 @@ namespace inst {
 class TriggerTrie;
 }
 namespace quantifiers {
-class EqualityQueryQuantifiersEngine;
 class FirstOrderModel;
 class Instantiate;
 class QModelBuilder;
@@ -148,17 +147,6 @@ public:
  /** mark relevant quantified formula, this will indicate it should be checked
   * before the others */
  void markRelevant(Node q);
- /** get internal representative
-  *
-  * Choose a term that is equivalent to a in the current context that is the
-  * best term for instantiating the index^th variable of quantified formula q.
-  * If no legal term can be found, we return null. This can occur if:
-  * - a's type is not a subtype of the type of the index^th variable of q,
-  * - a is in an equivalent class with all terms that are restricted not to
-  * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
-  * guided instantiation.
-  */
- Node getInternalRepresentative(Node a, Node q, int index);
  /**
   * Get quantifiers name, which returns a variable corresponding to the name of
   * quantified formula q if q has a name, or otherwise returns q itself.
@@ -249,8 +237,6 @@ public:
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** equality query class */
-  std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
   /** instantiate utility */
   std::unique_ptr<quantifiers::Instantiate> d_instantiate;
   /** skolemize utility */