Eliminate equality query dependence on quantifiers engine (#5831)

This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 08741ef0f424ae74f00bbb6c58a86fa5999a6f11..c60c98d7098a41ec6408641911bd3ef3d5035ba2 100644 (file)
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -19,9 +19,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -32,9 +29,10 @@ namespace theory {
 namespace quantifiers {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
-    QuantifiersState& qs, QuantifiersEngine* qe)
-    : d_qe(qe),
-      d_qstate(qs),
+    QuantifiersState& qs, TermDb* tdb, FirstOrderModel* m)
+    : d_qstate(qs),
+      d_tdb(tdb),
+      d_model(m),
       d_eqi_counter(qs.getSatContext()),
       d_reset_count(0)
 {
@@ -58,8 +56,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   if( options::finiteModelFind() ){
     if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
       //map back from values assigned by model, if any
-      if( d_qe->getModel() ){
-        Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r);
+      if (d_model != nullptr)
+      {
+        Node tr = d_model->getRepSet()->getTermForRepresentative(r);
         if (!tr.isNull())
         {
           r = tr;
@@ -173,7 +172,10 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
     return -2;
   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
     return -2;
-  }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
+  }
+  else if (options::lteRestrictInstClosure()
+           && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false)))
+  {
     return -1;
   }else if( options::instMaxLevel()!=-1 ){
     //score prefer lowest instantiation level

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index a3f895f541e5656cd59a7f3ad62ec3f7e31395e3..9944bf7039a85fa2e30604c3e6b31828f04e7950 100644 (file)
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -27,6 +27,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class TermDb;
+class FirstOrderModel;
+
 /** EqualityQueryQuantifiersEngine class
  *
  * The main method of this class is the function
@@ -40,7 +43,9 @@ namespace quantifiers {
 class EqualityQueryQuantifiersEngine : public QuantifiersUtil
 {
  public:
-  EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
+  EqualityQueryQuantifiersEngine(QuantifiersState& qs,
+                                 TermDb* tdb,
+                                 FirstOrderModel* m);
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
   bool reset(Theory::Effort e) override;
@@ -65,10 +70,12 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
   Node getInternalRepresentative(Node a, Node q, int index);
 
  private:
-  /** pointer to theory engine */
-  QuantifiersEngine* d_qe;
   /** the quantifiers state */
   QuantifiersState& d_qstate;
+  /** Pointer to the term database */
+  TermDb* d_tdb;
+  /** Pointer to the model */
+  FirstOrderModel* d_model;
   /** quantifiers equality inference */
   context::CDO< unsigned > d_eqi_counter;
   /** internal representatives */

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 8f587c09d9a5337999846d902d2edc9ce7d892e4..db977c53d89dc1ec7441417d2c1139217545a2df 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -118,7 +118,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
       // terms in rep_set are now constants which mapped to terms through
       // TheoryModel. Thus, should introduce a constant and a term.
       // For now, we just add an arbitrary term.
-      Node var = d_qe->getModel()->getSomeDomainElement(tn);
+      Node var = getSomeDomainElement(tn);
       Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
                      << std::endl;
       d_rep_set.add(tn, var);

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 28397fd14db95428d59dd005416b5836b6a3cfef..921c5100fed2c92f09a7f6dd2b0207df2f82e8a0 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -40,12 +40,12 @@ QuantifiersEngine::QuantifiersEngine(
       d_qim(qim),
       d_te(nullptr),
       d_decManager(nullptr),
-      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
       d_term_util(new quantifiers::TermUtil),
       d_term_db(new quantifiers::TermDb(qstate, qim, this)),
+      d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
@@ -62,7 +62,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_presolve_cache_wic(qstate.getUserContext())
 {
   //---- utilities
-  d_util.push_back(d_eq_query.get());
   // term util must come before the other utilities
   d_util.push_back(d_term_util.get());
   d_util.push_back(d_term_db.get());
@@ -116,6 +115,9 @@ QuantifiersEngine::QuantifiersEngine(
     d_model.reset(
         new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
   }
+  d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
+      qstate, d_term_db.get(), d_model.get()));
+  d_util.insert(d_util.begin(), d_eq_query.get());
 }
 
 QuantifiersEngine::~QuantifiersEngine() {}

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 74f4325857ef88f7f58ed2a12b2ee6fb9d8e38ab..f38a43757a85705d69fe7ad88e953c30246f9bf1 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -343,8 +343,6 @@ public:
   /** vector of modules for quantifiers */
   std::vector<QuantifiersModule*> d_modules;
   //------------- quantifiers utilities
-  /** equality query class */
-  std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
   /** all triggers will be stored in this trie */
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
@@ -355,6 +353,8 @@ public:
   std::unique_ptr<quantifiers::TermUtil> d_term_util;
   /** term database */
   std::unique_ptr<quantifiers::TermDb> d_term_db;
+  /** equality query class */
+  std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
   /** sygus term database */
   std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
   /** quantifiers attributes */