Miscellaneous elimination of dependencies on quantifiers engine (#6238)

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

1 files changed, 9 insertions, 7 deletions

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 );