Move methods from term util to quantifiers registry (#5916)

Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.

Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.

1 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 1743cafe5..3cef2884f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -69,10 +69,10 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
   }
 }
 
-
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){
-   d_is_computed = false;
+RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr)
+    : d_qe(qe), d_qreg(qr)
+{
+  d_is_computed = false;
 }
 
 RelevantDomain::~RelevantDomain() {
@@ -111,7 +111,7 @@ void RelevantDomain::compute(){
     FirstOrderModel* fm = d_qe->getModel();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node q = fm->getAssertedQuantifier( i );
-      Node icf = d_qe->getTermUtil()->getInstConstantBody( q );
+      Node icf = d_qreg.getInstConstantBody(q);
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
       computeRelevantDomain( q, icf, true, true );
     }
@@ -204,12 +204,13 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
 
 void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
   if( n.getKind()==INST_CONSTANT ){
-    Node q = d_qe->getTermUtil()->getInstConstAttr( n );
+    Node q = TermUtil::getInstConstAttr(n);
     //merge the RDomains
     unsigned id = n.getAttribute(InstVarNumAttribute());
     Assert(q[0][id].getType() == n.getType());
     Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
-    Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl;
+    Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
+                           << std::endl;
     RDomain * rq = getRDomain( q, id );
     if( rf!=rq ){
       rq->merge( rf );
@@ -226,12 +227,11 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
     d_rel_dom_lit[hasPol][pol][n].d_merge = false;
     int varCount = 0;
     int varCh = -1;
-    TermUtil* tu = d_qe->getTermUtil();
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( n[i].getKind()==INST_CONSTANT ){
         // must get the quantified formula this belongs to, which may be
         // different from q
-        Node qi = tu->getInstConstAttr(n[i]);
+        Node qi = TermUtil::getInstConstAttr(n[i]);
         unsigned id = n[i].getAttribute(InstVarNumAttribute());
         d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
         varCount++;
@@ -262,7 +262,7 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
             bool hasNonVar = false;
             for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
               if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
-                  && tu->getInstConstAttr(it->first) == q)
+                  && TermUtil::getInstConstAttr(it->first) == q)
               {
                 if( var.isNull() ){
                   var = it->first;