Eliminate non-static members in term util (#5919)

This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.

This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.

16 files changed, 82 insertions, 192 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index d620da7b5..f107c56e5 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -870,10 +870,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
   {
     // redo, split integer/non-integer parts
     bool useCoeff = false;
-    Integer coeff = ci->getQuantifiersEngine()
-                        ->getTermUtil()
-                        ->d_one.getConst<Rational>()
-                        .getNumerator();
+    Integer coeff(1);
     for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
          ++it)
     {
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index b2fff012e..8b60152a8 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1246,6 +1246,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
     bool pol = lit.getKind()!=NOT;
     //arithmetic inequalities and disequalities
     if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
+      NodeManager* nm = NodeManager::currentNM();
       Assert(atom.getKind() != GEQ || atom[1].isConst());
       Node atom_lhs;
       Node atom_rhs;
@@ -1253,20 +1254,27 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
         atom_lhs = atom[0];
         atom_rhs = atom[1];
       }else{
-        atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+        atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
         atom_lhs = Rewriter::rewrite( atom_lhs );
-        atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero;
+        atom_rhs = nm->mkConst(Rational(0));
       }
       //must be an eligible term
       if( isEligible( atom_lhs ) ){
         //apply substitution to LHS of atom
         TermProperties atom_lhs_prop;
-        atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop );
+        atom_lhs = applySubstitution(nm->realType(),
+                                     atom_lhs,
+                                     vars,
+                                     subs,
+                                     prop,
+                                     non_basic,
+                                     atom_lhs_prop);
         if( !atom_lhs.isNull() ){
           if( !atom_lhs_prop.d_coeff.isNull() ){
-            atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
+            atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs);
+            atom_rhs = Rewriter::rewrite(atom_rhs);
           }
-          lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+          lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs);
           if( !pol ){
             lret = lret.negate();
           }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 3ade304e8..e8b9f5dea 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -783,7 +783,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
         Node tu = u;
         getBounds( q, v, rsi, tl, tu );
         Assert(!tl.isNull() && !tu.isNull());
-        if( ra==d_quantEngine->getTermUtil()->d_true ){
+        if (ra.isConst() && ra.getConst<bool>())
+        {
           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
           for( unsigned k=0; k<rr; k++ ){
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index 1d2da7e79..ab08df233 100644
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -67,11 +67,6 @@ quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
   return d_quantEngine->getTermDatabase();
 }
 
-quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
-{
-  return d_quantEngine->getTermUtil();
-}
-
 quantifiers::QuantifiersState& QuantifiersModule::getState()
 {
   return d_qstate;
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 4d0481484..af763265d 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -34,7 +34,6 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 class TermDb;
-class TermUtil;
 }  // namespace quantifiers
 
 /** QuantifiersModule class
@@ -160,8 +159,6 @@ class QuantifiersModule
   QuantifiersEngine* getQuantifiersEngine() const;
   /** get currently used term database */
   quantifiers::TermDb* getTermDatabase() const;
-  /** get currently used term utility object */
-  quantifiers::TermUtil* getTermUtil() const;
   /** get the quantifiers state */
   quantifiers::QuantifiersState& getState();
   /** get the quantifiers inference manager */
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 1748dea8e..b296a4421 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -544,7 +544,8 @@ void CegSingleInvSol::getEquivalentTerms(Kind k,
         }
         if( !eq.isNull() ){
           eq = Rewriter::rewrite( eq );
-          if( eq!=d_qe->getTermUtil()->d_true ){
+          if (!eq.isConst() || !eq.getConst<bool>())
+          {
             success = false;
             break;
           }
@@ -788,7 +789,7 @@ void CegSingleInvSol::registerType(TypeNode tn)
   TypeNode btn = dt.getSygusType();
   // for constant reconstruction
   Kind ck = getComparisonKind(btn);
-  Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
+  Node z = TermUtil::mkTypeValue(btn, 0);
 
   // iterate over constructors
   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 00a72cbcb..538d80e44 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
 
 using namespace CVC4::kind;
@@ -34,9 +33,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
+CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds,
                                              SynthConjecture* p)
-    : d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
+    : d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
 {
 }
 
@@ -138,7 +137,7 @@ Node CegGrammarConstructor::process(Node q,
       sfvl = preGrammarType.getDType().getSygusVarList();
       tn = preGrammarType;
       // normalize type, if user-provided
-      SygusGrammarNorm sygus_norm(d_qe);
+      SygusGrammarNorm sygus_norm(d_tds);
       tn = sygus_norm.normalizeSygusType(tn, sfvl);
     }else{
       sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
@@ -205,7 +204,6 @@ Node CegGrammarConstructor::process(Node q,
 
   std::vector<Node> qchildren;
   Node qbody_subs = q[1];
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
   {
     Node sf = q[0][i];
@@ -253,7 +251,7 @@ Node CegGrammarConstructor::process(Node q,
         Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
       }
     }
-    tds->registerSygusType(tn);
+    d_tds->registerSygusType(tn);
     Assert(tn.isDatatype());
     const DType& dt = tn.getDType();
     Assert(dt.isSygus());
@@ -282,7 +280,6 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
   std::stack<TNode> visit;
   TNode cur;
   visit.push(n);
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   do {
     cur = visit.top();
     visit.pop();
@@ -347,7 +344,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
           //   lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
           // where ef is the first order variable for the
           // function-to-synthesize.
-          SygusTypeInfo& ti = tds->getTypeInfo(ef.getType());
+          SygusTypeInfo& ti = d_tds->getTypeInfo(ef.getType());
           const std::vector<Node>& vars = ti.getVarList();
           Assert(!vars.empty());
           std::vector<Node> vs;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 6edfbebd5..67d5eb027 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -28,8 +28,6 @@
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
 /**
  * Attribute for associating a function-to-synthesize with a first order
  * variable whose type is a sygus datatype type that encodes its grammar.
@@ -53,6 +51,7 @@ typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
 namespace quantifiers {
 
 class SynthConjecture;
+class TermDbSygus;
 
 /**
  * Utility for constructing datatypes that correspond to syntactic restrictions,
@@ -61,7 +60,7 @@ class SynthConjecture;
 class CegGrammarConstructor
 {
 public:
- CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
+ CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
  ~CegGrammarConstructor() {}
  /** process
   *
@@ -169,8 +168,8 @@ public:
   Node convertToEmbedding(Node n);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine * d_qe;
+  /** The sygus term database we are using */
+  TermDbSygus* d_tds;
   /** parent conjecture
   * This contains global information about the synthesis conjecture.
   */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 644d50a95..7d757ca98 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 #include <numeric>  // for std::iota
 
@@ -68,10 +67,7 @@ bool OpPosTrie::getOrMakeType(TypeNode tn,
   return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
 }
 
-SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe)
-    : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
-{
-}
+SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {}
 
 SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
     : d_tn(src_tn),
@@ -287,7 +283,7 @@ std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
   if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
   {
     SygusRedundantCons src;
-    src.initialize(d_qe, tn);
+    src.initialize(d_tds, tn);
     std::vector<unsigned> rindices;
     src.getRedundant(rindices);
     if (!rindices.empty())
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 48a5dbe06..2827d2837 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -25,7 +25,6 @@
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers/term_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -128,7 +127,7 @@ class OpPosTrie
 class SygusGrammarNorm
 {
  public:
-  SygusGrammarNorm(QuantifiersEngine* qe);
+  SygusGrammarNorm(TermDbSygus* tds);
   ~SygusGrammarNorm() {}
   /** creates a normalized typenode from a given one.
    *
@@ -363,8 +362,6 @@ class SygusGrammarNorm
 
   }; /* class TransfChain */
 
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** sygus term database associated with this utility */
   TermDbSygus* d_tds;
   /** List of variable inputs of function-to-synthesize.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index e6b9b3593..6e36222b6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -19,7 +19,6 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -28,13 +27,12 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
+void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
 {
-  Assert(qe != nullptr);
+  Assert(tds != nullptr);
   Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
   d_type = tn;
   Assert(tn.isDatatype());
-  TermDbSygus* tds = qe->getTermDatabaseSygus();
   tds->registerSygusType(tn);
   const DType& dt = tn.getDType();
   Assert(dt.isSygus());
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 7fda6acbe..ace855ee1 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -24,9 +24,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class TermDbSygus;
@@ -48,7 +45,7 @@ class SygusRedundantCons
    * qe : pointer to the quantifiers engine,
    * tn : the (sygus) type to compute redundant constructors for
    */
-  void initialize(QuantifiersEngine* qe, TypeNode tn);
+  void initialize(TermDbSygus* tds, TypeNode tn);
   /** Get the indices of the redundant constructors of the register type */
   void getRedundant(std::vector<unsigned>& indices);
   /**
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 59edd3070..909a9aecc 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -53,7 +53,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_ceg_si(new CegSingleInv(qe)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess(qe)),
-      d_ceg_gc(new CegGrammarConstructor(qe, this)),
+      d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(qe, this)),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 728797d85..e800a52cf 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -939,8 +939,7 @@ bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
     if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL || 
         k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
       if( n[1].isConst() ){
-        if (n[1]
-            == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0))
+        if (n[1] == TermUtil::mkTypeValue(n[1].getType(), 0))
         {
           return true;
         }
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 97a731fb9..9cbf2cf53 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -35,18 +35,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermUtil::TermUtil()
-{
-  d_true = NodeManager::currentNM()->mkConst(true);
-  d_false = NodeManager::currentNM()->mkConst(false);
-  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(Rational(1));
-}
-
-TermUtil::~TermUtil(){
-
-}
-
 size_t TermUtil::getVariableNum(Node q, Node v)
 {
   Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
@@ -342,19 +330,7 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) {
          ( n.getKind()!=ITE || n.getType().isBoolean() );
 }
 
-Node TermUtil::getTypeValue(TypeNode tn, int val)
-{
-  std::unordered_map<int, Node>::iterator it = d_type_value[tn].find(val);
-  if (it == d_type_value[tn].end())
-  {
-    Node n = mkTypeValue(tn, val);
-    d_type_value[tn][val] = n;
-    return n;
-  }
-  return it->second;
-}
-
-Node TermUtil::mkTypeValue(TypeNode tn, int val)
+Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
 {
   Node n;
   if (tn.isInteger() || tn.isReal())
@@ -364,7 +340,8 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val)
   }
   else if (tn.isBitVector())
   {
-    unsigned int uv = val;
+    // cast to unsigned
+    uint32_t uv = static_cast<uint32_t>(val);
     BitVector bval(tn.getConst<BitVectorSize>(), uv);
     n = NodeManager::currentNM()->mkConst<BitVector>(bval);
   }
@@ -385,19 +362,6 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val)
   return n;
 }
 
-Node TermUtil::getTypeMaxValue(TypeNode tn)
-{
-  std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
-      d_type_max_value.find(tn);
-  if (it == d_type_max_value.end())
-  {
-    Node n = mkTypeMaxValue(tn);
-    d_type_max_value[tn] = n;
-    return n;
-  }
-  return it->second;
-}
-
 Node TermUtil::mkTypeMaxValue(TypeNode tn)
 {
   Node n;
@@ -412,39 +376,29 @@ Node TermUtil::mkTypeMaxValue(TypeNode tn)
   return n;
 }
 
-Node TermUtil::getTypeValueOffset(TypeNode tn,
-                                  Node val,
-                                  int offset,
-                                  int& status)
+Node TermUtil::mkTypeValueOffset(TypeNode tn,
+                                 Node val,
+                                 int32_t offset,
+                                 int32_t& status)
 {
-  std::unordered_map<int, Node>::iterator it =
-      d_type_value_offset[tn][val].find(offset);
-  if (it == d_type_value_offset[tn][val].end())
+  Node val_o;
+  Node offset_val = mkTypeValue(tn, offset);
+  status = -1;
+  if (!offset_val.isNull())
   {
-    Node val_o;
-    Node offset_val = getTypeValue(tn, offset);
-    status = -1;
-    if (!offset_val.isNull())
+    if (tn.isInteger() || tn.isReal())
     {
-      if (tn.isInteger() || tn.isReal())
-      {
-        val_o = Rewriter::rewrite(
-            NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
-        status = 0;
-      }
-      else if (tn.isBitVector())
-      {
-        val_o = Rewriter::rewrite(
-            NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
-        // TODO : enable?  watch for overflows
-      }
+      val_o = Rewriter::rewrite(
+          NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
+      status = 0;
+    }
+    else if (tn.isBitVector())
+    {
+      val_o = Rewriter::rewrite(
+          NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
     }
-    d_type_value_offset[tn][val][offset] = val_o;
-    d_type_value_offset_status[tn][val][offset] = status;
-    return val_o;
   }
-  status = d_type_value_offset_status[tn][val][offset];
-  return it->second;
+  return val_o;
 }
 
 Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
@@ -493,7 +447,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
   // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
   // ik!=BITVECTOR_UDIV );
   TypeNode tn = n.getType();
-  if (n == getTypeValue(tn, 0))
+  if (n == mkTypeValue(tn, 0))
   {
     if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS
         || ik == BITVECTOR_OR
@@ -511,7 +465,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
       return arg == 1;
     }
   }
-  else if (n == getTypeValue(tn, 1))
+  else if (n == mkTypeValue(tn, 1))
   {
     if (ik == MULT || ik == BITVECTOR_MULT)
     {
@@ -528,7 +482,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
       return arg == 1;
     }
   }
-  else if (n == getTypeMaxValue(tn))
+  else if (n == mkTypeMaxValue(tn))
   {
     if (ik == EQUAL || ik == BITVECTOR_AND || ik == BITVECTOR_XNOR)
     {
@@ -541,7 +495,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
 Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
 {
   TypeNode tn = n.getType();
-  if (n == getTypeValue(tn, 0))
+  if (n == mkTypeValue(tn, 0))
   {
     if (ik == AND || ik == MULT || ik == BITVECTOR_AND || ik == BITVECTOR_MULT)
     {
@@ -565,7 +519,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
       }
       else if (arg == 1)
       {
-        return getTypeMaxValue(tn);
+        return mkTypeMaxValue(tn);
       }
     }
     else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
@@ -586,25 +540,25 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
       }
       else if (arg == 2)
       {
-        return getTypeValue(NodeManager::currentNM()->stringType(), 0);
+        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
       }
     }
     else if (ik == STRING_STRIDOF)
     {
       if (arg == 0 || arg == 1)
       {
-        return getTypeValue(NodeManager::currentNM()->integerType(), -1);
+        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
       }
     }
   }
-  else if (n == getTypeValue(tn, 1))
+  else if (n == mkTypeValue(tn, 1))
   {
     if (ik == BITVECTOR_UREM_TOTAL)
     {
-      return getTypeValue(tn, 0);
+      return mkTypeValue(tn, 0);
     }
   }
-  else if (n == getTypeMaxValue(tn))
+  else if (n == mkTypeMaxValue(tn))
   {
     if (ik == OR || ik == BITVECTOR_OR)
     {
@@ -618,12 +572,12 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
       // negative arguments
       if (ik == STRING_SUBSTR || ik == STRING_CHARAT)
       {
-        return getTypeValue(NodeManager::currentNM()->stringType(), 0);
+        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
       }
       else if (ik == STRING_STRIDOF)
       {
         Assert(arg == 2);
-        return getTypeValue(NodeManager::currentNM()->integerType(), -1);
+        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
       }
     }
   }
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index e9e3c7e98..591b7f85f 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -21,7 +21,7 @@
 #include <unordered_set>
 
 #include "expr/attribute.h"
-#include "theory/type_enumerator.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -50,13 +50,6 @@ typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttri
 struct QuantIdNumAttributeId {};
 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
-class QuantifiersEngine;
-
-namespace inst{
-  class Trigger;
-  class HigherOrderTrigger;
-}
-
 namespace quantifiers {
 
 class TermDatabase;
@@ -65,14 +58,8 @@ class TermDatabase;
 class TermUtil
 {
  public:
-  TermUtil();
-  ~TermUtil();
-  /** boolean terms */
-  Node d_true;
-  Node d_false;
-  /** constants */
-  Node d_zero;
-  Node d_one;
+  TermUtil() {}
+  ~TermUtil() {}
 
   // for inst constant
  public:
@@ -114,33 +101,6 @@ public:
                                                Node n,
                                                std::vector<Node>& vars);
 
-public:
-  
-//general utilities
-  // TODO #1216 : promote these?
- private:
-  /** cache for getTypeValue */
-  std::unordered_map<TypeNode,
-                     std::unordered_map<int, Node>,
-                     TypeNodeHashFunction>
-      d_type_value;
-  /** cache for getTypeMaxValue */
-  std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_max_value;
-  /** cache for getTypeValueOffset */
-  std::unordered_map<TypeNode,
-                     std::unordered_map<Node,
-                                        std::unordered_map<int, Node>,
-                                        NodeHashFunction>,
-                     TypeNodeHashFunction>
-      d_type_value_offset;
-  /** cache for status of getTypeValueOffset*/
-  std::unordered_map<TypeNode,
-                     std::unordered_map<Node,
-                                        std::unordered_map<int, int>,
-                                        NodeHashFunction>,
-                     TypeNodeHashFunction>
-      d_type_value_offset_status;
-
  public:
   /** contains uninterpreted constant */
   static bool containsUninterpretedConstant( Node n );
@@ -205,41 +165,35 @@ public:
    *   <k>( ... t_{arg-1}, t_{arg+1}...)
    * always holds.
    */
-  bool isIdempotentArg(Node n, Kind ik, int arg);
+  static bool isIdempotentArg(Node n, Kind ik, int arg);
 
   /** is singular arg
    * Returns true if
    *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret
    * always holds for some constant ret, which is returned by this function.
    */
-  Node isSingularArg(Node n, Kind ik, unsigned arg);
+  static Node isSingularArg(Node n, Kind ik, unsigned arg);
 
-  /** get type value
+  /** get type value with simple value
    * This gets the Node that represents value val for Type tn
    * This is used to get simple values, e.g. -1,0,1,
    * in a uniform way per type.
    */
-  Node getTypeValue(TypeNode tn, int val);
-
-  /** get type value offset
+  static Node mkTypeValue(TypeNode tn, int32_t val);
+  /** make type value with simple offset
    * Returns the value of ( val + getTypeValue( tn, offset ) ),
    * where + is the additive operator for the type.
    * Stores the status (0: success, -1: failure) in status.
    */
-  Node getTypeValueOffset(TypeNode tn, Node val, int offset, int& status);
-
-  /** get the "max" value for type tn
+  static Node mkTypeValueOffset(TypeNode tn,
+                                Node val,
+                                int32_t offset,
+                                int32_t& status);
+  /** make the "max" value for type tn
    * For example,
    *   the max value for Bool is true,
    *   the max value for BitVector is 1..1.
    */
-  Node getTypeMaxValue(TypeNode tn);
-
-  /** make value, static version of get value */
-  static Node mkTypeValue(TypeNode tn, int val);
-  /** make value offset, static version of get value offset */
-  static Node mkTypeValueOffset(TypeNode tn, Node val, int offset, int& status);
-  /** make max value, static version of get max value */
   static Node mkTypeMaxValue(TypeNode tn);
   /**
    * Make const, returns pol ? mkTypeValue(tn,0) : mkTypeMaxValue(tn).