1 files changed, 10 insertions, 8 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 02f1b8509..9f6617d5a 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
 
 using namespace std;
@@ -196,7 +198,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     }else{
       //compute attributes
       QAttributes qa;
-      TermDb::computeQuantAttributes( in, qa );
+      QuantAttributes::computeQuantAttributes( in, qa );
       if( !qa.isRewriteRule() ){
         for( int op=0; op<COMPUTE_LAST; op++ ){
           if( doOperation( in, op, qa ) ){
@@ -504,10 +506,10 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
   std::map< Node, Node > cache;
   std::map< Node, Node > icache;
   if( qa.isFunDef() ){
-    Node h = TermDb::getFunDefHead( q );
+    Node h = QuantAttributes::getFunDefHead( q );
     Assert( !h.isNull() );
     // if it is a function definition, rewrite the body independently
-    Node fbody = TermDb::getFunDefBody( q );
+    Node fbody = QuantAttributes::getFunDefBody( q );
     Assert( !body.isNull() );
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
     Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false );
@@ -745,7 +747,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
   }else if( n.getKind()==EQUAL ){
     for( unsigned i=0; i<2; i++ ){
       if( n[i].getKind()==BOUND_VARIABLE ){
-        if( !TermDb::containsTerm( n[1-i], n[i] ) ){
+        if( !TermUtil::containsTerm( n[1-i], n[i] ) ){
           return true;
         }
       }
@@ -843,7 +845,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
 }
 
 bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
-  if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
+  if( TermUtil::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
     return false;
   }else{
     return true;
@@ -973,7 +975,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
             if( lit.getKind()==GEQ || lit.getKind()==GT ){
               //compute variables in itm->first, these are not eligible for elimination
               std::vector< Node > bvs;
-              TermDb::getBoundVars( itm->first, bvs );
+              TermUtil::getBoundVars( itm->first, bvs );
               for( unsigned j=0; j<bvs.size(); j++ ){
                 Trace("var-elim-ineq-debug") << "...ineligible " << bvs[j] << " since it is contained in monomial." << std::endl;
                 num_bounds[bvs[j]][true].clear();
@@ -1410,7 +1412,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
       NodeBuilder<> tb(kind::OR);
       for( unsigned i=0; i<body.getNumChildren(); i++ ){
         Node trm = body[i];
-        if( TermDb::containsTerms( body[i], args ) ){
+        if( TermUtil::containsTerms( body[i], args ) ){
           tb << trm;
         }else{
           body_split << trm;
@@ -1791,7 +1793,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
       Node sub;
       std::vector< unsigned > sub_vars;
       //return skolemized body
-      return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
+      return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
     }
   }else{
     //check if it contains a quantifier as a subterm