From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 18 Feb 2021 03:15:39 +0000 (-0600)
Subject: Eliminate non-static members in term util (#5919)
X-Git-Tag: cvc5-1.0.0~2267
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0bd5ef36d2b773912c3049f8f3fed62eaf0fa68b;p=cvc5.git

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.
---

diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index 6b0063ce0..04ac14c11 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/sygus_simple_sym.h"
 
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace std;
@@ -24,7 +25,7 @@ namespace theory {
 namespace datatypes {
 
 SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
-    : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil())
+    : d_tds(qe->getTermDatabaseSygus())
 {
 }
 
@@ -430,7 +431,7 @@ bool SygusSimpleSymBreak::considerConst(
   {
     Kind ok;
     int offset;
-    if (d_tutil->hasOffsetArg(pk, arg, offset, ok))
+    if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok))
     {
       Trace("sygus-sb-simple-debug")
           << pk << " has offset arg " << ok << " " << offset << std::endl;
@@ -443,7 +444,8 @@ bool SygusSimpleSymBreak::considerConst(
         if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
         {
           int status;
-          Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status);
+          Node co = quantifiers::TermUtil::mkTypeValueOffset(
+              c.getType(), c, offset, status);
           Trace("sygus-sb-simple-debug")
               << c << " with offset " << offset << " is " << co
               << ", status=" << status << std::endl;
@@ -476,7 +478,7 @@ bool SygusSimpleSymBreak::considerConst(
   bool ret = true;
   Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
                           << ", arg = " << arg << "?" << std::endl;
-  if (d_tutil->isIdempotentArg(c, pk, arg))
+  if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg))
   {
     if (pdt[pc].getNumArgs() == 2)
     {
@@ -493,7 +495,7 @@ bool SygusSimpleSymBreak::considerConst(
   }
   else
   {
-    Node sc = d_tutil->isSingularArg(c, pk, arg);
+    Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg);
     if (!sc.isNull())
     {
       if (pti.hasConst(sc))
@@ -509,9 +511,9 @@ bool SygusSimpleSymBreak::considerConst(
   {
     ReqTrie rt;
     Assert(rt.empty());
-    Node max_c = d_tutil->getTypeMaxValue(c.getType());
-    Node zero_c = d_tutil->getTypeValue(c.getType(), 0);
-    Node one_c = d_tutil->getTypeValue(c.getType(), 1);
+    Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType());
+    Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0);
+    Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1);
     if (pk == XOR || pk == BITVECTOR_XOR)
     {
       if (c == max_c)
diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h
index a16e7a513..c2940512a 100644
--- a/src/theory/datatypes/sygus_simple_sym.h
+++ b/src/theory/datatypes/sygus_simple_sym.h
@@ -20,7 +20,6 @@
 #include <map>
 #include "expr/dtype.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -89,8 +88,6 @@ class SygusSimpleSymBreak
  private:
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
-  /** Pointer to the quantifiers term utility */
-  quantifiers::TermUtil* d_tutil;
   /** return the index of the first argument position of c that has type tn */
   int getFirstArgOccurrence(const DTypeConstructor& c, TypeNode tn);
   /**
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).
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ebec7a110..1c01eae65 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,7 +45,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
-      d_term_util(new quantifiers::TermUtil),
       d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
       d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
@@ -166,10 +165,6 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
 {
   return d_sygus_tdb.get();
 }
-quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
-{
-  return d_term_util.get();
-}
 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
 {
   return d_quant_attr.get();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2fbf6b70f..f8f92f2e9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -90,8 +90,6 @@ class QuantifiersEngine {
   quantifiers::TermDb* getTermDatabase() const;
   /** get term database sygus */
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
-  /** get term utilities */
-  quantifiers::TermUtil* getTermUtil() const;
   /** get quantifiers attributes */
   quantifiers::QuantAttributes* getQuantAttributes() const;
   /** get instantiate utility */
@@ -294,8 +292,6 @@ public:
   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
   /** model builder */
   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
-  /** term utilities */
-  std::unique_ptr<quantifiers::TermUtil> d_term_util;
   /** term database */
   std::unique_ptr<quantifiers::TermDb> d_term_db;
   /** equality query class */