Miscellaneous elimination of dependencies on quantifiers engine (#6238)

This should be the last PR before quantifiers engine will not be passed to quantifiers modules.

12 files changed, 36 insertions, 51 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index fd6a087ca..38b9c739e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -29,7 +29,6 @@
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -185,11 +184,12 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
 
 CegInstantiator::CegInstantiator(Node q,
                                  QuantifiersState& qs,
+                                 TermRegistry& tr,
                                  InstStrategyCegqi* parent)
     : d_quant(q),
       d_qstate(qs),
+      d_treg(tr),
       d_parent(parent),
-      d_qe(parent->getQuantifiersEngine()),
       d_is_nested_quant(false),
       d_effort(CEG_INST_EFFORT_NONE)
 {
@@ -1437,7 +1437,7 @@ void CegInstantiator::processAssertions() {
 }
 
 Node CegInstantiator::getModelValue( Node n ) {
-  return d_qe->getModel()->getValue( n );
+  return d_treg.getModel()->getValue(n);
 }
 
 Node CegInstantiator::getBoundVariable(TypeNode tn)
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 217584de8..bca62f2ef 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -24,15 +24,13 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class Instantiator;
 class InstantiatorPreprocess;
 class InstStrategyCegqi;
 class QuantifiersState;
+class TermRegistry;
 
 /**
  * Descriptions of the types of constraints that a term was solved for in.
@@ -209,7 +207,10 @@ class CegInstantiator {
    * The instantiator will be constructing instantiations for quantified formula
    * q, parent is the owner of this object.
    */
-  CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent);
+  CegInstantiator(Node q,
+                  QuantifiersState& qs,
+                  TermRegistry& tr,
+                  InstStrategyCegqi* parent);
   virtual ~CegInstantiator();
   /** check
    * This adds instantiations based on the state of d_vars in current context
@@ -233,8 +234,6 @@ class CegInstantiator {
                                    std::vector<Node>& ce_vars,
                                    std::vector<Node>& auxLems);
   //------------------------------interface for instantiators
-  /** get quantifiers engine */
-  QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
   /** push stack variable
    * This adds a new variable to solve for in the stack
    * of variables we are processing. This stack is only
@@ -251,7 +250,7 @@ class CegInstantiator {
    * instantiation, specified by sf.
    *
    * This function returns true if a call to
-   * QuantifiersEngine::addInstantiation(...)
+   * Instantiate::addInstantiation(...)
    * was successfully made in a recursive call.
    *
    * The solved form sf is reverted to its original state if
@@ -349,10 +348,10 @@ class CegInstantiator {
   Node d_quant;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** The parent of this instantiator */
   InstStrategyCegqi* d_parent;
-  /** quantified formula associated with this instantiator */
-  QuantifiersEngine* d_qe;
 
   //-------------------------------globally cached
   /** cache from nodes to the set of variables it contains
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 8318c5f4c..3690cbcac 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -16,9 +16,6 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -26,7 +23,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -511,7 +507,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
       d_cinst.find(q);
   if( it==d_cinst.end() ){
-    d_cinst[q].reset(new CegInstantiator(q, d_qstate, this));
+    d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this));
     return d_cinst[q].get();
   }
   return it->second.get();
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index 6968a0dee..b277ec180 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -24,10 +24,8 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
+
 class QuantifiersState;
 class TermRegistry;
 
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 0c8c9399b..a45029074 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -111,7 +111,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
-    d_rel_dom.reset(new RelevantDomain(qe, qr));
+    d_rel_dom.reset(new RelevantDomain(qs, qr, tr));
     d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 456a7a8fc..8210c5e8a 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -19,8 +19,8 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
@@ -72,8 +72,10 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
   }
 }
 
-RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr)
-    : d_qe(qe), d_qreg(qr)
+RelevantDomain::RelevantDomain(QuantifiersState& qs,
+                               QuantifiersRegistry& qr,
+                               TermRegistry& tr)
+    : d_qs(qs), d_qreg(qr), d_treg(tr)
 {
   d_is_computed = false;
 }
@@ -111,7 +113,7 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    FirstOrderModel* fm = d_qe->getModel();
+    FirstOrderModel* fm = d_treg.getModel();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node q = fm->getAssertedQuantifier( i );
       Node icf = d_qreg.getInstConstantBody(q);
@@ -120,7 +122,7 @@ void RelevantDomain::compute(){
     }
 
     Trace("rel-dom-debug") << "account for ground terms" << std::endl;
-    TermDb * db = d_qe->getTermDatabase();
+    TermDb* db = d_treg.getTermDatabase();
     for (unsigned k = 0; k < db->getNumOperators(); k++)
     {
       Node op = db->getOperator(k);
@@ -145,7 +147,7 @@ void RelevantDomain::compute(){
         RDomain * r = it2->second;
         RDomain * rp = r->getParent();
         if( r==rp ){
-          r->removeRedundantTerms(d_qe->getState());
+          r->removeRedundantTerms(d_qs);
           for( unsigned i=0; i<r->d_terms.size(); i++ ){
             Trace("rel-dom") << r->d_terms[i] << " ";
           }
@@ -160,7 +162,7 @@ void RelevantDomain::compute(){
 
 void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) {
   Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
-  Node op = d_qe->getTermDatabase()->getMatchOperator( n );
+  Node op = d_treg.getTermDatabase()->getMatchOperator(n);
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( !op.isNull() ){
       RDomain * rf = getRDomain( op, i );
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index cfc543c9b..8fbd70f3e 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -24,7 +24,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QuantifiersState;
 class QuantifiersRegistry;
+class TermRegistry;
 
 /** Relevant Domain
  *
@@ -42,7 +44,9 @@ class QuantifiersRegistry;
 class RelevantDomain : public QuantifiersUtil
 {
  public:
-  RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr);
+  RelevantDomain(QuantifiersState& qs,
+                 QuantifiersRegistry& qr,
+                 TermRegistry& tr);
   virtual ~RelevantDomain();
   /** Reset. */
   bool reset(Theory::Effort e) override;
@@ -117,10 +121,12 @@ class RelevantDomain : public QuantifiersUtil
    * each relevant domain object.
    */
   std::map< RDomain *, int > d_ri_map;
-  /** Quantifiers engine associated with this utility. */
-  QuantifiersEngine* d_qe;
-  /** The quantifiers registry */
+  /** Reference to the quantifiers state object */
+  QuantifiersState& d_qs;
+  /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** have we computed the relevant domain on this full effort check? */
   bool d_is_computed;
   /** relevant domain literal
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index 5185e549f..de136d546 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -28,9 +28,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 /** This file contains techniques that compute
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 800ba6261..c8582cce5 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {}
+SygusQePreproc::SygusQePreproc() {}
 
 Node SygusQePreproc::preprocess(Node q)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 3629164ee..4cfa8a624 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -19,9 +19,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 /**
@@ -37,17 +34,13 @@ namespace quantifiers {
 class SygusQePreproc
 {
  public:
-  SygusQePreproc(QuantifiersEngine* qe);
+  SygusQePreproc();
   ~SygusQePreproc() {}
   /**
    * Preprocess. Returns a lemma of the form q = nq where nq is obtained
    * by the quantifier elimination technique outlined above.
    */
   Node preprocess(Node q);
-
- private:
-  /** Pointer to quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f4d50118e..1d71af6b4 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -32,9 +32,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr, qe),
-      d_conj(nullptr),
-      d_sqp(qe)
+    : QuantifiersModule(qs, qim, qr, tr, qe), d_conj(nullptr), d_sqp()
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(qs, qim, qr, tr, d_statistics)));
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 6506a6123..bafaa8bdd 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -30,9 +30,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class QuantifiersState;
@@ -67,7 +64,6 @@ class DbList
  * lazily for performance reasons.
  */
 class TermDb : public QuantifiersUtil {
-  friend class ::CVC4::theory::QuantifiersEngine;
   using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
   using NodeList = context::CDList<Node>;
   using NodeSet = context::CDHashSet<Node, NodeHashFunction>;