From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 5 Nov 2021 16:54:30 +0000 (-0500)
Subject: Remove many static calls to rewrite (#7580)
X-Git-Tag: cvc5-1.0.0~883
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a82b7fb2760e705aba57516fc32041214e701559;p=cvc5.git

Remove many static calls to rewrite (#7580)

This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.

It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).
---

diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index e8c1ff07f..cee38d83a 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -111,7 +111,7 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
             {
               // rewrite, this ensures that e.g. the propositional value of
               // quantified formulas can be queried
-              n = theory::Rewriter::rewrite(n);
+              n = rewrite(n);
               Node vn = m->getValue(n);
               Assert(vn.isConst());
               if (vn.getConst<bool>() == cpol)
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index fdcfb063b..5b225ef30 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -1713,7 +1713,7 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){
 //     c->explainForConflict(nb);
 //   }
 //   Node ret = safeConstructNary(nb);
-//   Node rew = Rewriter::rewrite(ret);
+//   Node rew = rewrite(ret);
 //   if(rew.getNumChildren() < ret.getNumChildren()){
 //     //Debug("approx::") << "explainSet " << ret << " " << rew << endl;
 //   }
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 8f10d7611..b42b97d59 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -102,7 +102,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
         newn = n;
       }else if(n.getNumChildren() > 0){
         newn = applyReduceVariablesInItes(n);
-        newn = Rewriter::rewrite(newn);
+        newn = rewrite(newn);
         Assert(Polynomial::isMember(newn));
       }else{
         newn = n;
@@ -385,7 +385,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){
   //Node n = 
   Node n = applySubstitutions(binor);
   if(n != binor){
-    n = Rewriter::rewrite(n);
+    n = rewrite(n);
 
     if(!(n.getKind() == kind::OR &&
 	 n.getNumChildren() == 2 &&
diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index 31017dea6..eb02339bb 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -58,13 +58,11 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
 
     // Prioritize trying a simple rounding of the real solution first,
     // it that fails, fall back on original branch and bound strategy.
-    Node ub =
-        Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1)));
-    Node lb =
-        Rewriter::rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1)));
+    Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1)));
+    Node lb = rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1)));
     Node right = nm->mkNode(OR, ub, lb);
     Node rawEq = nm->mkNode(EQUAL, var, mkRationalNode(nearest));
-    Node eq = Rewriter::rewrite(rawEq);
+    Node eq = rewrite(rawEq);
     // Also preprocess it before we send it out. This is important since
     // arithmetic may prefer eliminating equalities.
     TrustNode teq;
@@ -121,7 +119,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
   }
   else
   {
-    Node ub = Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor)));
+    Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor)));
     Node lb = ub.notNode();
     if (proofsEnabled())
     {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 4aee9e981..ae782eed2 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -355,7 +355,7 @@ bool ArithCongruenceManager::propagate(TNode x){
     return true;
   }
 
-  Node rewritten = Rewriter::rewrite(x);
+  Node rewritten = rewrite(x);
 
   //Need to still propagate this!
   if(rewritten.getKind() == kind::CONST_BOOLEAN){
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index b847c63ae..995526f49 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -100,7 +100,7 @@ class ArithCongruenceManager : protected EnvObj
   /* This maps the node a theory engine will request on an explain call to
    * to its corresponding PropUnit.
    * This is node is potentially both the propagation or
-   * Rewriter::rewrite(propagation).
+   * rewrite(propagation).
    */
   typedef context::CDHashMap<Node, size_t> ExplainMap;
   ExplainMap d_explanationMap;
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 670f38c40..4b0667aaa 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -115,13 +115,13 @@ std::size_t InferenceManager::numWaitingLemmas() const
 
 bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 {
-  Node rewritten = Rewriter::rewrite(lem);
+  Node rewritten = rewrite(lem);
   return TheoryInferenceManager::hasCachedLemma(rewritten, p);
 }
 
 bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 {
-  Node rewritten = Rewriter::rewrite(lem);
+  Node rewritten = rewrite(lem);
   return TheoryInferenceManager::cacheLemma(rewritten, p);
 }
 
@@ -130,7 +130,7 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
   if (options().arith.nlExtEntailConflicts)
   {
     Node ch_lemma = lem.d_node.negate();
-    ch_lemma = Rewriter::rewrite(ch_lemma);
+    ch_lemma = rewrite(ch_lemma);
     Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
                                << ch_lemma << "..." << std::endl;
 
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 4c79564e3..e41639c58 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -30,7 +30,8 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-FactoringCheck::FactoringCheck(ExtState* data) : d_data(data)
+FactoringCheck::FactoringCheck(Env& env, ExtState* data)
+    : EnvObj(env), d_data(data)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -94,7 +95,7 @@ void FactoringCheck::check(const std::vector<Node>& asserts,
                     children.pop_back();
                   }
                   children[i] = itm->first[i];
-                  val = Rewriter::rewrite(val);
+                  val = rewrite(val);
                   factor_to_mono[itm->first[i]].push_back(val);
                   factor_to_mono_orig[itm->first[i]].push_back(itm->first);
                 }
@@ -122,7 +123,7 @@ void FactoringCheck::check(const std::vector<Node>& asserts,
             continue;
           }
           Node sum = nm->mkNode(Kind::PLUS, itf->second);
-          sum = Rewriter::rewrite(sum);
+          sum = rewrite(sum);
           Trace("nl-ext-factor")
               << "* Factored sum for " << x << " : " << sum << std::endl;
 
@@ -153,7 +154,7 @@ void FactoringCheck::check(const std::vector<Node>& asserts,
           Trace("nl-ext-factor")
               << "...factored polynomial : " << polyn << std::endl;
           Node conc_lit = nm->mkNode(atom.getKind(), polyn, d_zero);
-          conc_lit = Rewriter::rewrite(conc_lit);
+          conc_lit = rewrite(conc_lit);
           if (!polarity)
           {
             conc_lit = conc_lit.negate();
diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index 9ae94f22d..1aa8c17aa 100644
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -30,10 +31,10 @@ namespace nl {
 
 struct ExtState;
 
-class FactoringCheck
+class FactoringCheck : protected EnvObj
 {
  public:
-  FactoringCheck(ExtState* data);
+  FactoringCheck(Env& env, ExtState* data);
 
   /** check factoring
    *
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index bb6a2a5c3..1f50b3112 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -68,8 +68,8 @@ bool hasNewMonomials(Node n, const std::vector<Node>& existing)
 }
 }  // namespace
 
-MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data)
-    : d_data(data), d_cdb(d_data->d_mdb)
+MonomialBoundsCheck::MonomialBoundsCheck(Env& env, ExtState* data)
+    : EnvObj(env), d_data(data), d_cdb(d_data->d_mdb)
 {
 }
 
@@ -300,7 +300,8 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
           Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
           Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
           Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
-          Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer));
+          Node infer_mv =
+              d_data->d_model.computeAbstractModelValue(rewrite(infer));
           Trace("nl-ext-bound-debug")
               << "       ...infer model value is " << infer_mv << std::endl;
           if (infer_mv == d_data->d_false)
@@ -311,7 +312,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
                     mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero),
                 d_ci_exp[x][coeff][rhs]);
             Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer);
-            Node iblem_rw = Rewriter::rewrite(iblem);
+            Node iblem_rw = rewrite(iblem);
             bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms);
             Trace("nl-ext-bound-lemma")
                 << "*** Bound inference lemma : " << iblem_rw
@@ -478,7 +479,7 @@ void MonomialBoundsCheck::checkResBounds()
         {
           Node rhs_a = itcar->first;
           Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a);
-          rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
+          rhs_a_res_base = rewrite(rhs_a_res_base);
           if (hasNewMonomials(rhs_a_res_base, d_data->d_ms))
           {
             continue;
@@ -501,7 +502,7 @@ void MonomialBoundsCheck::checkResBounds()
               Node rhs_b = itcbr->first;
               Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b);
               rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
-              rhs_b_res = Rewriter::rewrite(rhs_b_res);
+              rhs_b_res = rewrite(rhs_b_res);
               if (hasNewMonomials(rhs_b_res, d_data->d_ms))
               {
                 continue;
@@ -554,7 +555,7 @@ void MonomialBoundsCheck::checkResBounds()
                          "(pre-rewrite) "
                          ": "
                       << rblem << std::endl;
-                  rblem = Rewriter::rewrite(rblem);
+                  rblem = rewrite(rblem);
                   Trace("nl-ext-rbound-lemma")
                       << "Resolution bound lemma : " << rblem << std::endl;
                   d_data->d_im.addPendingLemma(
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index 3a21e7f58..caf0dd437 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -17,6 +17,7 @@
 #define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/ext/constraint.h"
 
 namespace cvc5 {
@@ -26,10 +27,10 @@ namespace nl {
 
 struct ExtState;
 
-class MonomialBoundsCheck
+class MonomialBoundsCheck : protected EnvObj
 {
  public:
-  MonomialBoundsCheck(ExtState* data);
+  MonomialBoundsCheck(Env& env, ExtState* data);
 
   void init();
 
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index b077dcfd0..a16ffdd02 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -29,7 +29,8 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-MonomialCheck::MonomialCheck(ExtState* data) : d_data(data)
+MonomialCheck::MonomialCheck(Env& env, ExtState* data)
+    : EnvObj(env), d_data(data)
 {
   d_order_points.push_back(d_data->d_neg_one);
   d_order_points.push_back(d_data->d_zero);
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index 3cf239bf5..a0b81bfb9 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -17,6 +17,7 @@
 #define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
 
@@ -27,10 +28,10 @@ namespace nl {
 
 struct ExtState;
 
-class MonomialCheck
+class MonomialCheck : protected EnvObj
 {
  public:
-  MonomialCheck(ExtState* data);
+  MonomialCheck(Env& env, ExtState* data);
 
   void init(const std::vector<Node>& xts);
 
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index dcd6398b5..e786eca37 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -28,8 +28,8 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-SplitZeroCheck::SplitZeroCheck(ExtState* data)
-    : d_data(data), d_zero_split(d_data->d_env.getUserContext())
+SplitZeroCheck::SplitZeroCheck(Env& env, ExtState* data)
+    : EnvObj(env), d_data(data), d_zero_split(d_data->d_env.getUserContext())
 {
 }
 
@@ -40,7 +40,7 @@ void SplitZeroCheck::check()
     Node v = d_data->d_ms_vars[i];
     if (d_zero_split.insert(v))
     {
-      Node eq = Rewriter::rewrite(v.eqNode(d_data->d_zero));
+      Node eq = rewrite(v.eqNode(d_data->d_zero));
       Node lem = eq.orNode(eq.negate());
       CDProof* proof = nullptr;
       if (d_data->isProofEnabled())
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index c50737d51..8b6280878 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -16,8 +16,9 @@
 #ifndef CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 #define CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 
-#include "expr/node.h"
 #include "context/cdhashset.h"
+#include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -26,10 +27,10 @@ namespace nl {
 
 struct ExtState;
 
-class SplitZeroCheck
+class SplitZeroCheck : protected EnvObj
 {
  public:
-  SplitZeroCheck(ExtState* data);
+  SplitZeroCheck(Env& env, ExtState* data);
 
   /** check split zero
    *
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index d2a5e628a..ebdca33dd 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -29,7 +29,10 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-TangentPlaneCheck::TangentPlaneCheck(ExtState* data) : d_data(data) {}
+TangentPlaneCheck::TangentPlaneCheck(Env& env, ExtState* data)
+    : EnvObj(env), d_data(data)
+{
+}
 
 void TangentPlaneCheck::check(bool asWaitingLemmas)
 {
@@ -90,7 +93,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
               {
                 Node do_extend = nm->mkNode(
                     (p == 1 || p == 3) ? Kind::GT : Kind::LT, curr_v, pt_v);
-                do_extend = Rewriter::rewrite(do_extend);
+                do_extend = rewrite(do_extend);
                 if (do_extend == d_data->d_true)
                 {
                   for (unsigned q = 0; q < 2; q++)
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index c9b7a3c7f..2832518ad 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -19,6 +19,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -27,10 +28,10 @@ namespace nl {
 
 struct ExtState;
 
-class TangentPlaneCheck
+class TangentPlaneCheck : protected EnvObj
 {
  public:
-  TangentPlaneCheck(ExtState* data);
+  TangentPlaneCheck(Env& env, ExtState* data);
 
   /** check tangent planes
    *
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 76d964934..b773f6baf 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -198,7 +198,7 @@ Node IAndSolver::convertToBvK(unsigned k, Node n) const
   NodeManager* nm = NodeManager::currentNM();
   Node iToBvOp = nm->mkConst(IntToBitVector(k));
   Node bn = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvOp, n);
-  return Rewriter::rewrite(bn);
+  return rewrite(bn);
 }
 
 Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const
@@ -206,14 +206,14 @@ Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const
   NodeManager* nm = NodeManager::currentNM();
   Node iAndOp = nm->mkConst(IntAnd(k));
   Node ret = nm->mkNode(IAND, iAndOp, x, y);
-  ret = Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
 Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const
 {
   Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y)));
-  ret = Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
@@ -221,7 +221,7 @@ Node IAndSolver::mkINot(unsigned k, Node x) const
 {
   NodeManager* nm = NodeManager::currentNM();
   Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x);
-  ret = Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
@@ -236,7 +236,7 @@ Node IAndSolver::valueBasedLemma(Node i)
 
   NodeManager* nm = NodeManager::currentNM();
   Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY);
-  valC = Rewriter::rewrite(valC);
+  valC = rewrite(valC);
 
   Node lem = nm->mkNode(
       IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC));
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 9cd74883b..92c7d3ddd 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -65,6 +65,11 @@ inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw)
 }
 }  // namespace
 
+ICPSolver::ICPSolver(Env& env, InferenceManager& im)
+    : EnvObj(env), d_im(im), d_state(d_mapper)
+{
+}
+
 std::vector<Node> ICPSolver::collectVariables(const Node& n) const
 {
   std::unordered_set<TNode> tmp;
@@ -79,7 +84,7 @@ std::vector<Node> ICPSolver::collectVariables(const Node& n) const
 
 std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
 {
-  Node tmp = Rewriter::rewrite(n);
+  Node tmp = rewrite(n);
   if (tmp.isConst())
   {
     return {};
@@ -271,7 +276,7 @@ std::vector<Node> ICPSolver::generateLemmas() const
       {
         Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
         Trace("nl-icp") << premise << " => " << c << std::endl;
-        Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
+        Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
         if (lemma.isConst())
         {
           Assert(lemma == nm->mkConst<bool>(true));
@@ -291,7 +296,7 @@ std::vector<Node> ICPSolver::generateLemmas() const
       {
         Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
         Trace("nl-icp") << premise << " => " << c << std::endl;
-        Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
+        Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
         if (lemma.isConst())
         {
           Assert(lemma == nm->mkConst<bool>(true));
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index c1b4b6dde..8b0fbf583 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -23,6 +23,7 @@
 #endif /* CVC5_POLY_IMP */
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/bound_inference.h"
 #include "theory/arith/nl/icp/candidate.h"
 #include "theory/arith/nl/icp/contraction_origins.h"
@@ -53,8 +54,19 @@ namespace icp {
  * These contractions can yield to a conflict (if the interval of some variable
  * becomes empty) or shrink the search space for a variable.
  */
-class ICPSolver
+class ICPSolver : protected EnvObj
 {
+ public:
+  ICPSolver(Env& env, InferenceManager& im);
+  /** Reset this solver for the next theory call */
+  void reset(const std::vector<Node>& assertions);
+
+  /**
+   * Performs a full ICP check.
+   */
+  void check();
+
+ private:
   /**
    * This encapsulates the state of the ICP solver that is local to a single
    * theory call. It contains the variable bounds and candidates derived from
@@ -126,24 +138,14 @@ class ICPSolver
    * is constructed.
    */
   std::vector<Node> generateLemmas() const;
-
- public:
-  ICPSolver(InferenceManager& im) : d_im(im), d_state(d_mapper) {}
-  /** Reset this solver for the next theory call */
-  void reset(const std::vector<Node>& assertions);
-
-  /**
-   * Performs a full ICP check.
-   */
-  void check();
 };
 
 #else /* CVC5_POLY_IMP */
 
-class ICPSolver
+class ICPSolver : protected EnvObj
 {
  public:
-  ICPSolver(InferenceManager& im) {}
+  ICPSolver(Env& env, InferenceManager& im) : EnvObj(env) {}
   void reset(const std::vector<Node>& assertions);
   void check();
 };
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index a970abc45..56bdd652a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -49,15 +49,15 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_extTheoryCb(state.getEqualityEngine()),
       d_extTheory(env, d_extTheoryCb, d_im),
       d_model(),
-      d_trSlv(d_im, d_model, d_env),
+      d_trSlv(d_env, d_im, d_model),
       d_extState(d_im, d_model, d_env),
-      d_factoringSlv(&d_extState),
-      d_monomialBoundsSlv(&d_extState),
-      d_monomialSlv(&d_extState),
-      d_splitZeroSlv(&d_extState),
-      d_tangentPlaneSlv(&d_extState),
+      d_factoringSlv(d_env, &d_extState),
+      d_monomialBoundsSlv(d_env, &d_extState),
+      d_monomialSlv(d_env, &d_extState),
+      d_splitZeroSlv(d_env, &d_extState),
+      d_tangentPlaneSlv(d_env, &d_extState),
       d_cadSlv(d_env, d_im, d_model),
-      d_icpSlv(d_im),
+      d_icpSlv(d_env, d_im),
       d_iandSlv(env, d_im, state, d_model),
       d_pow2Slv(env, d_im, state, d_model)
 {
@@ -455,7 +455,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS
         {
           for (const Node& eq : shared_term_value_splits)
           {
-            Node req = Rewriter::rewrite(eq);
+            Node req = rewrite(eq);
             Node literal = d_containing.getValuation().ensureLiteral(req);
             d_containing.getOutputChannel().requirePhase(literal, true);
             Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index 597a0df96..c91284be7 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -188,7 +188,7 @@ Node Pow2Solver::valueBasedLemma(Node i)
 
   NodeManager* nm = NodeManager::currentNM();
   Node valC = nm->mkNode(POW2, valX);
-  valC = Rewriter::rewrite(valC);
+  valC = rewrite(valC);
 
   Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC));
   return lem;
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 73279a782..17b5d259c 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -35,8 +35,8 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
-ExponentialSolver::ExponentialSolver(TranscendentalState* tstate)
-    : d_data(tstate)
+ExponentialSolver::ExponentialSolver(Env& env, TranscendentalState* tstate)
+    : EnvObj(env), d_data(tstate)
 {
 }
 
@@ -217,7 +217,7 @@ void ExponentialSolver::doTangentLemma(TNode e,
                         nm->mkNode(Kind::GEQ, e, poly_approx));
   Trace("nl-ext-exp") << "*** Tangent plane lemma (pre-rewrite): " << lem
                       << std::endl;
-  lem = Rewriter::rewrite(lem);
+  lem = rewrite(lem);
   Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
@@ -261,13 +261,13 @@ std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e,
   if (bounds.first.isNull())
   {
     // pick c-1
-    bounds.first = Rewriter::rewrite(
+    bounds.first = rewrite(
         NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
   }
   if (bounds.second.isNull())
   {
     // pick c+1
-    bounds.second = Rewriter::rewrite(
+    bounds.second = rewrite(
         NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one));
   }
   return bounds;
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index db540c40e..05bbb141a 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -19,6 +19,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -40,10 +41,10 @@ struct TranscendentalState;
  * It's main functionality are methods that implement lemma schemas below,
  * which return a set of lemmas that should be sent on the output channel.
  */
-class ExponentialSolver
+class ExponentialSolver : protected EnvObj
 {
  public:
-  ExponentialSolver(TranscendentalState* tstate);
+  ExponentialSolver(Env& env, TranscendentalState* tstate);
   ~ExponentialSolver();
 
   /**
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 6fdd4cc15..ed37ee91c 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -50,7 +50,10 @@ inline Node mkValidPhase(TNode a, TNode pi)
 }
 }  // namespace
 
-SineSolver::SineSolver(TranscendentalState* tstate) : d_data(tstate) {}
+SineSolver::SineSolver(Env& env, TranscendentalState* tstate)
+    : EnvObj(env), d_data(tstate)
+{
+}
 
 SineSolver::~SineSolver() {}
 
@@ -109,7 +112,7 @@ void SineSolver::checkInitialRefine()
         d_tf_initial_refine[t] = true;
         Node symn = nm->mkNode(Kind::SINE,
                                nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0]));
-        symn = Rewriter::rewrite(symn);
+        symn = rewrite(symn);
         // Can assume it is its own master since phase is split over 0,
         // hence  -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
         d_data->d_trMaster[symn] = symn;
@@ -381,7 +384,7 @@ void SineSolver::doTangentLemma(
 
   Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem
                        << std::endl;
-  lem = Rewriter::rewrite(lem);
+  lem = rewrite(lem);
   Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 83de35f52..96bfa6009 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -19,6 +19,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace cvc5 {
@@ -39,10 +40,10 @@ namespace transcendental {
  * It's main functionality are methods that implement lemma schemas below,
  * which return a set of lemmas that should be sent on the output channel.
  */
-class SineSolver
+class SineSolver : protected EnvObj
 {
  public:
-  SineSolver(TranscendentalState* tstate);
+  SineSolver(Env& env, TranscendentalState* tstate);
   ~SineSolver();
 
   /**
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 978823a22..5b6db69b8 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -37,10 +37,13 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
-TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
-                                           NlModel& m,
-                                           Env& env)
-    : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
+TranscendentalSolver::TranscendentalSolver(Env& env,
+                                           InferenceManager& im,
+                                           NlModel& m)
+    : EnvObj(env),
+      d_tstate(im, m, env),
+      d_expSlv(env, &d_tstate),
+      d_sineSlv(env, &d_tstate)
 {
   d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
 }
@@ -98,7 +101,7 @@ bool TranscendentalSolver::preprocessAssertionsCheckModel(
     if (!subs.empty())
     {
       pa = arithSubstitute(pa, subs);
-      pa = Rewriter::rewrite(pa);
+      pa = rewrite(pa);
     }
     if (!pa.isConst() || !pa.getConst<bool>())
     {
@@ -330,11 +333,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
       Assert(v_pab.isConst());
       Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
       Trace("nl-trans") << "...compare : " << comp << std::endl;
-      Node compr = Rewriter::rewrite(comp);
+      Node compr = rewrite(comp);
       Trace("nl-trans") << "...got : " << compr << std::endl;
       if (compr == d_tstate.d_true)
       {
-        poly_approx_c = Rewriter::rewrite(v_pab);
+        poly_approx_c = rewrite(v_pab);
         // beyond the bounds
         if (r == 0)
         {
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 649ff2080..c1a617b38 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/transcendental/exponential_solver.h"
 #include "theory/arith/nl/transcendental/sine_solver.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
@@ -47,10 +48,10 @@ namespace transcendental {
  * It's main functionality are methods that implement lemma schemas below,
  * which return a set of lemmas that should be sent on the output channel.
  */
-class TranscendentalSolver
+class TranscendentalSolver : protected EnvObj
 {
  public:
-  TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env);
+  TranscendentalSolver(Env& env, InferenceManager& im, NlModel& m);
   ~TranscendentalSolver();
 
   /** init last call
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index afbb9b70f..5c43189ea 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -106,7 +106,7 @@ Node OperatorElim::eliminateOperators(Node node,
     case COTANGENT:
     {
       // these are eliminated by rewriting
-      return Rewriter::rewrite(node);
+      return rewrite(node);
       break;
     }
     case TO_INTEGER:
@@ -148,8 +148,8 @@ Node OperatorElim::eliminateOperators(Node node,
         // not eliminating total operators
         return node;
       }
-      Node den = Rewriter::rewrite(node[1]);
-      Node num = Rewriter::rewrite(node[0]);
+      Node den = rewrite(node[1]);
+      Node num = rewrite(node[0]);
       Node rw = nm->mkNode(k, num, den);
       Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
       Node lem;
@@ -160,7 +160,7 @@ Node OperatorElim::eliminateOperators(Node node,
         if (num.isConst() || rat == 0)
         {
           // just rewrite
-          return Rewriter::rewrite(node);
+          return rewrite(node);
         }
         if (rat > 0)
         {
@@ -239,8 +239,8 @@ Node OperatorElim::eliminateOperators(Node node,
         // not eliminating total operators
         return node;
       }
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
+      Node num = rewrite(node[0]);
+      Node den = rewrite(node[1]);
       if (den.isConst())
       {
         // No need to eliminate here, can eliminate via rewriting later.
@@ -260,8 +260,8 @@ Node OperatorElim::eliminateOperators(Node node,
     }
     case DIVISION:
     {
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
+      Node num = rewrite(node[0]);
+      Node den = rewrite(node[1]);
       Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
@@ -277,8 +277,8 @@ Node OperatorElim::eliminateOperators(Node node,
     case INTS_DIVISION:
     {
       // partial function: integer div
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
+      Node num = rewrite(node[0]);
+      Node den = rewrite(node[1]);
       Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
@@ -295,8 +295,8 @@ Node OperatorElim::eliminateOperators(Node node,
     case INTS_MODULUS:
     {
       // partial function: mod
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
+      Node num = rewrite(node[0]);
+      Node den = rewrite(node[1]);
       Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp
index 4c72eb909..aa186edd6 100644
--- a/src/theory/arith/pp_rewrite_eq.cpp
+++ b/src/theory/arith/pp_rewrite_eq.cpp
@@ -40,7 +40,7 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom)
   Assert(atom[0].getType().isReal());
   Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
   Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
-  Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+  Node rewritten = rewrite(leq.andNode(geq));
   Debug("arith::preprocess")
       << "arith::preprocess() : returning " << rewritten << std::endl;
   // don't need to rewrite terms since rewritten is not a non-standard op
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 269ca083b..c5f0620f9 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -331,8 +331,10 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
   {
     return d_internal->getEqualityStatus(a,b);
   }
-  Node aval = Rewriter::rewrite(a.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
-  Node bval = Rewriter::rewrite(b.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
+  Node aval =
+      rewrite(a.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
+  Node bval =
+      rewrite(b.substitute(d_arithModelCache.begin(), d_arithModelCache.end()));
   if (aval == bval)
   {
     return EQUALITY_TRUE_IN_MODEL;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 732ed962e..f49a295c7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1005,7 +1005,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
       // ax + p = c -> (ax + p) -ax - c = -ax
       // x = (p - ax - c) * -1/a
       // Add the substitution if not recursive
-      Assert(elim == Rewriter::rewrite(elim));
+      Assert(elim == rewrite(elim));
 
       if (right.size() > options().arith.ppAssertMaxSubSize)
       {
@@ -1408,7 +1408,7 @@ TrustNode TheoryArithPrivate::dioCutting()
     Comparison leq = Comparison::mkComparison(LEQ, p, c);
     Comparison geq = Comparison::mkComparison(GEQ, p, c);
     Node lemma = NodeManager::currentNM()->mkNode(OR, leq.getNode(), geq.getNode());
-    Node rewrittenLemma = Rewriter::rewrite(lemma);
+    Node rewrittenLemma = rewrite(lemma);
     Debug("arith::dio::ex") << "dioCutting found the plane: " << plane.getNode() << endl;
     Debug("arith::dio::ex") << "resulting in the cut: " << lemma << endl;
     Debug("arith::dio::ex") << "rewritten " << rewrittenLemma << endl;
@@ -1499,7 +1499,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
     bool isDistinct = simpleKind == DISTINCT;
     Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
     Assert(!isSetup(eq));
-    Node reEq = Rewriter::rewrite(eq);
+    Node reEq = rewrite(eq);
     Debug("arith::distinct::const") << "Assertion: " << assertion << std::endl;
     Debug("arith::distinct::const") << "Eq       : " << eq << std::endl;
     Debug("arith::distinct::const") << "reEq     : " << reEq << std::endl;
@@ -1962,7 +1962,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D
   Assert(k == kind::LEQ || k == kind::GEQ);
 
   Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs));
-  Node rewritten = Rewriter::rewrite(comparison);
+  Node rewritten = rewrite(comparison);
   if(!(Comparison::isNormalAtom(rewritten))){
     return make_pair(NullConstraint, added);
   }
@@ -2061,11 +2061,12 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C
   return replayGetConstraint(lhs, k, rhs, ci.getKlass() == BranchCutKlass);
 }
 
-// Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv, Kind k){
+// Node denseVectorToLiteral(const ArithVariables& vars, const DenseVector& dv,
+// Kind k){
 //   NodeManager* nm = NodeManager::currentNM();
 //   Node sumLhs = toSumNode(vars, dv.lhs);
 //   Node ineq = nm->mkNode(k, sumLhs, mkRationalNode(dv.rhs) );
-//   Node lit = Rewriter::rewrite(ineq);
+//   Node lit = rewrite(ineq);
 //   return lit;
 // }
 
@@ -2590,7 +2591,7 @@ Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
       Rational fl(maybe_value.value().floor());
       NodeManager* nm = NodeManager::currentNM();
       Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl));
-      Node norm = Rewriter::rewrite(leq);
+      Node norm = rewrite(leq);
       return norm;
     }
   }
@@ -2609,7 +2610,7 @@ Node TheoryArithPrivate::cutToLiteral(ApproximateSimplex* approx, const CutInfo&
 
     NodeManager* nm = NodeManager::currentNM();
     Node ineq = nm->mkNode(k, sum, rhs);
-    return Rewriter::rewrite(ineq);
+    return rewrite(ineq);
   }
   return Node::null();
 }
@@ -2640,7 +2641,7 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
         const ConstraintCPVec& exp = cut->getExplanation();
         Node asLemma = Constraint::externalExplainByAssertions(exp);
 
-        Node implied = Rewriter::rewrite(cutConstraint);
+        Node implied = rewrite(cutConstraint);
         anythingnew = anythingnew || !isSatLiteral(implied);
 
         Node implication = asLemma.impNode(implied);
@@ -2923,7 +2924,7 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel)
       ++d_statistics.d_panicBranches;
       TrustNode branch = branchIntegerVariable(canBranch);
       Assert(branch.getNode().getKind() == kind::OR);
-      Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
+      Node rwbranch = rewrite(branch.getNode()[0]);
       if (!isSatLiteral(rwbranch))
       {
         d_approxCuts.push_back(branch);
@@ -3548,10 +3549,9 @@ bool TheoryArithPrivate::splitDisequalities(){
         TrustNode lemma = front->split();
         ++(d_statistics.d_statDisequalitySplits);
 
-        Debug("arith::lemma")
-            << "Now " << Rewriter::rewrite(lemma.getNode()) << endl;
+        Debug("arith::lemma") << "Now " << rewrite(lemma.getNode()) << endl;
         outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ);
-        //cout << "Now " << Rewriter::rewrite(lemma) << endl;
+        // cout << "Now " << rewrite(lemma) << endl;
         splitSomething = true;
       }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
         Debug("arith::eq") << "can drop as less than lb" << front << endl;
@@ -3692,7 +3692,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
 
     //Currently if the flag is set this came from an equality detected by the
     //equality engine in the the difference manager.
-    Node normalized = Rewriter::rewrite(toProp);
+    Node normalized = rewrite(toProp);
 
     ConstraintP constraint = d_constraintDatabase.lookup(normalized);
     if(constraint == NullConstraint){
@@ -4600,7 +4600,7 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith
   if(!successful) { return make_pair(false, Node::null()); }
 
   if(dp.getKind() == CONST_RATIONAL){
-    Node eval = Rewriter::rewrite(lit);
+    Node eval = rewrite(lit);
     Assert(eval.getKind() == kind::CONST_BOOLEAN);
     // if true, true is an acceptable explaination
     // if false, the node is uninterpreted and eval can be forgotten
diff --git a/src/theory/decision_strategy.cpp b/src/theory/decision_strategy.cpp
index 7c932177a..5162b667d 100644
--- a/src/theory/decision_strategy.cpp
+++ b/src/theory/decision_strategy.cpp
@@ -114,7 +114,7 @@ Node DecisionStrategyFmf::getLiteral(unsigned n)
     Node lit = mkLiteral(d_literals.size());
     if (!lit.isNull())
     {
-      lit = Rewriter::rewrite(lit);
+      lit = rewrite(lit);
     }
     d_literals.push_back(lit);
   }
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index d38fcf3e3..8b4880feb 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -58,7 +58,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem,
   if (checkCache)
   {
     // check if it is unique up to rewriting
-    Node lemr = Rewriter::rewrite(lem);
+    Node lemr = rewrite(lem);
     if (hasCachedLemma(lemr, p))
     {
       return false;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 2c6419de1..db62da53b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -947,7 +947,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
               }else{
                 rsg = lhs.eqNode( rhs );
               }
-              rsg = Rewriter::rewrite( rsg );
+              rsg = rewrite(rsg);
               d_conjectures.push_back( rsg );
               d_eq_conjectures[lhs].push_back( rhs );
               d_eq_conjectures[rhs].push_back( lhs );
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index b0dd61d33..fa4ff7007 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -85,7 +85,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
 
 Result ExprMiner::doCheck(Node query)
 {
-  Node queryr = Rewriter::rewrite(query);
+  Node queryr = rewrite(query);
   if (queryr.isConst())
   {
     if (!queryr.getConst<bool>())
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 4be13ba5f..b51090f78 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -152,7 +152,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
     }
   }
   Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
-  curr = Rewriter::rewrite(curr);
+  curr = rewrite(curr);
   return nm->mkNode(LAMBDA, boundVarList, curr);
 }
 
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 78a09641b..6f31273f0 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -54,7 +54,7 @@ void FunDefEvaluator::assertDefinition(Node q)
 Node FunDefEvaluator::evaluateDefinitions(Node n) const
 {
   // should do standard rewrite before this call
-  Assert(Rewriter::rewrite(n) == n);
+  Assert(rewrite(n) == n);
   Trace("fd-eval") << "FunDefEvaluator: evaluateDefinitions " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, unsigned> funDefCount;
@@ -217,7 +217,7 @@ Node FunDefEvaluator::evaluateDefinitions(Node n) const
           if (childChanged)
           {
             ret = nm->mkNode(cur.getKind(), children);
-            ret = Rewriter::rewrite(ret);
+            ret = rewrite(ret);
           }
           Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
           visited[cur] = ret;
diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp
index a2a8b8145..32822a23f 100644
--- a/src/theory/quantifiers/ho_term_database.cpp
+++ b/src/theory/quantifiers/ho_term_database.cpp
@@ -119,7 +119,7 @@ bool HoTermDb::resetInternal(Theory::Effort effort)
       std::map<Node, Node>::iterator itpe = d_hoPurifyToEq.find(pp.first);
       if (itpe == d_hoPurifyToEq.end())
       {
-        eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
+        eq = rewrite(pp.first.eqNode(pp.second));
         d_hoPurifyToEq[pp.first] = eq;
       }
       else
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 5a0cf8724..e93d0a105 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -71,7 +71,7 @@ bool CegisCoreConnective::processInitialize(Node conj,
   }
   Trace("sygus-ccore-init") << "  body : " << body << std::endl;
 
-  TransitionInference ti;
+  TransitionInference ti(d_env);
   ti.process(body, conj[0][0]);
 
   if (!ti.isComplete())
@@ -130,7 +130,7 @@ bool CegisCoreConnective::processInitialize(Node conj,
       sc = sc[1];
     }
     Node scb = TermUtil::simpleNegate(sc);
-    TransitionInference tisc;
+    TransitionInference tisc(d_env);
     tisc.process(scb, conj[0][0]);
     Node scTrans = ti.getTransitionRelation();
     Trace("sygus-ccore-init")
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 7af1ef45b..388a4d31f 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -30,7 +30,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
+SygusEvalUnfold::SygusEvalUnfold(Env& env, TermDbSygus* tds)
+    : EnvObj(env), d_tds(tds)
+{
+}
 
 void SygusEvalUnfold::registerEvalTerm(Node n)
 {
@@ -96,7 +99,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
       TNode at = a;
       TNode vt = v;
       Node vn = n.substitute(at, vt);
-      vn = Rewriter::rewrite(vn);
+      vn = rewrite(vn);
       unsigned start = d_node_mv_args_proc[n][vn];
       // get explanation in terms of testers
       std::vector<Node> antec_exp;
@@ -319,7 +322,7 @@ Node SygusEvalUnfold::unfold(Node en,
   Trace("sygus-eval-unfold-debug")
       << "Applied sygus args : " << ret << std::endl;
   // rewrite
-  ret = Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
   return ret;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
index c30d4dae7..32e58f6ce 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -19,7 +19,9 @@
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
 
 #include <map>
+
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/sygus_invariance.h"
 
 namespace cvc5 {
@@ -37,10 +39,10 @@ class TermDbSygus;
  * unfold" applications of eval based on the model values of evaluation heads
  * in refinement lemmas.
  */
-class SygusEvalUnfold
+class SygusEvalUnfold : protected EnvObj
 {
  public:
-  SygusEvalUnfold(TermDbSygus* tds);
+  SygusEvalUnfold(Env& env, TermDbSygus* tds);
   ~SygusEvalUnfold() {}
   /** register evaluation term
    *
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index e402bfb9e..6167f7474 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -87,7 +87,7 @@ Node SygusReconstruct::reconstructSolution(Node sol,
       {
         continue;
       }
-      Node builtin = Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz));
+      Node builtin = rewrite(datatypes::utils::sygusToBuiltin(sz));
       // if enumerated term does not contain free variables, then its
       // corresponding obligation can be solved immediately
       if (sz.isConst())
@@ -208,8 +208,7 @@ TypeBuiltinSetMap SygusReconstruct::matchNewObs(Node t, Node sz)
   matches.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
 
   // try to match the builtin term with the pattern sz
-  if (expr::match(
-          Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)), t, matches))
+  if (expr::match(rewrite(datatypes::utils::sygusToBuiltin(sz)), t, matches))
   {
     // the bound variables z generated by the enumerators are reused across
     // enumerated terms, so we need to replace them with our own skolems
@@ -497,11 +496,10 @@ void SygusReconstruct::printPool(
 
     for (const Node& sygusTerm : pair.second)
     {
-      Trace("sygus-rcons") << "    "
-                           << Rewriter::rewrite(
-                                  datatypes::utils::sygusToBuiltin(sygusTerm))
-                                  .toString()
-                           << std::endl;
+      Trace("sygus-rcons")
+          << "    "
+          << rewrite(datatypes::utils::sygusToBuiltin(sygusTerm)).toString()
+          << std::endl;
     }
 
     Trace("sygus-rcons") << "  ]" << std::endl;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 9c5b8a606..e7d0ef58b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -57,10 +57,10 @@ SynthConjecture::SynthConjecture(Env& env,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(options(), logicInfo(), d_tds),
+      d_verify(env, d_tds),
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
-      d_templInfer(new SygusTemplateInfer),
+      d_templInfer(new SygusTemplateInfer(env)),
       d_ceg_proc(new SynthConjectureProcess),
       d_ceg_gc(new CegGrammarConstructor(env, d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(env, d_tds)),
diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index db09b45ed..5b26efef5 100644
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -32,14 +32,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SynthVerify::SynthVerify(const Options& opts,
-                         const LogicInfo& logicInfo,
-                         TermDbSygus* tds)
-    : d_tds(tds), d_subLogicInfo(logicInfo)
+SynthVerify::SynthVerify(Env& env, TermDbSygus* tds)
+    : EnvObj(env), d_tds(tds), d_subLogicInfo(logicInfo())
 {
   // determine the options to use for the verification subsolvers we spawn
   // we start with the provided options
-  d_subOptions.copyValues(opts);
+  d_subOptions.copyValues(options());
   // limit the number of instantiation rounds on subcalls
   d_subOptions.quantifiers.instMaxRounds =
       d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
@@ -124,7 +122,7 @@ Result SynthVerify::verify(Node query,
       Node squery =
           query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end());
       Trace("cegqi-debug") << "...squery : " << squery << std::endl;
-      squery = Rewriter::rewrite(squery);
+      squery = rewrite(squery);
       Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
       Assert(options::sygusRecFun()
              || (squery.isConst() && squery.getConst<bool>()));
diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h
index 948a70787..87a653c05 100644
--- a/src/theory/quantifiers/sygus/synth_verify.h
+++ b/src/theory/quantifiers/sygus/synth_verify.h
@@ -21,6 +21,7 @@
 #include <memory>
 
 #include "options/options.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "util/result.h"
 
@@ -31,12 +32,10 @@ namespace quantifiers {
 /**
  * Class for verifying queries corresponding to synthesis conjectures
  */
-class SynthVerify
+class SynthVerify : protected EnvObj
 {
  public:
-  SynthVerify(const Options& opts,
-              const LogicInfo& logicInfo,
-              TermDbSygus* tds);
+  SynthVerify(Env& env, TermDbSygus* tds);
   ~SynthVerify();
   /**
    * Verification call, which takes into account specific aspects of the
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index eeec13508..ab9d5f845 100644
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -26,6 +26,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+SygusTemplateInfer::SygusTemplateInfer(Env& env) : EnvObj(env), d_ti(env) {}
+
 void SygusTemplateInfer::initialize(Node q)
 {
   Assert(d_quant.isNull());
diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h
index f7053df46..64bd3662f 100644
--- a/src/theory/quantifiers/sygus/template_infer.h
+++ b/src/theory/quantifiers/sygus/template_infer.h
@@ -21,6 +21,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/transition_inference.h"
 
 namespace cvc5 {
@@ -31,10 +32,10 @@ namespace quantifiers {
  * This class infers templates for an invariant-to-synthesize based on the
  * template mode. It uses the transition inference to choose a template.
  */
-class SygusTemplateInfer
+class SygusTemplateInfer : protected EnvObj
 {
  public:
-  SygusTemplateInfer() {}
+  SygusTemplateInfer(Env& env);
   ~SygusTemplateInfer() {}
   /**
    * Initialize this class for synthesis conjecture q. If applicable, the
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 2e528b213..352ce9d88 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -56,7 +56,7 @@ TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs)
       d_qstate(qs),
       d_syexp(new SygusExplain(this)),
       d_funDefEval(new FunDefEvaluator(env)),
-      d_eval_unfold(new SygusEvalUnfold(this))
+      d_eval_unfold(new SygusEvalUnfold(env, this))
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -981,7 +981,7 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
 {
   if (args.empty())
   {
-    return Rewriter::rewrite( bn );
+    return rewrite(bn);
   }
   Assert(isRegistered(tn));
   SygusTypeInfo& ti = getTypeInfo(tn);
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index e456c954f..7d93955c7 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -124,7 +124,7 @@ void TransitionInference::getConstantSubstitution(
                         const_var.end(),
                         const_subs.begin(),
                         const_subs.end());
-      sn = Rewriter::rewrite(sn);
+      sn = rewrite(sn);
     }
     else
     {
@@ -177,7 +177,7 @@ void TransitionInference::getConstantSubstitution(
         TNode ts = s;
         for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
         {
-          const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts));
+          const_subs[k] = rewrite(const_subs[k].substitute(v, ts));
         }
         Trace("cegqi-inv-debug2")
             << "...substitution : " << v << " -> " << s << std::endl;
@@ -258,7 +258,7 @@ void TransitionInference::process(Node n)
     for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
     {
       Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
-      disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+      disjuncts[j] = rewrite(disjuncts[j].substitute(
           vars.begin(), vars.end(), svars.begin(), svars.end()));
       Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
     }
@@ -269,7 +269,7 @@ void TransitionInference::process(Node n)
       // transition
       Assert(terms.find(true) != terms.end());
       Node next = terms[true];
-      next = Rewriter::rewrite(next.substitute(
+      next = rewrite(next.substitute(
           vars.begin(), vars.end(), svars.begin(), svars.end()));
       Trace("cegqi-inv-debug")
           << "transition next predicate : " << next << std::endl;
@@ -292,7 +292,7 @@ void TransitionInference::process(Node n)
       for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
       {
         Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
-        disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
+        disjuncts[j] = rewrite(disjuncts[j].substitute(
             rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
         Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
       }
@@ -503,7 +503,7 @@ TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
   // check if it satisfies the pre/post condition
   Node cc = fwd ? getPostCondition() : getPreCondition();
   Assert(!cc.isNull());
-  Node ccr = Rewriter::rewrite(cc.substitute(
+  Node ccr = rewrite(cc.substitute(
       d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
   if (ccr.isConst())
   {
@@ -519,7 +519,7 @@ TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
   Assert(!c.isNull());
 
   Assert(d_vars.size() == dt.d_curr.size());
-  Node cr = Rewriter::rewrite(c.substitute(
+  Node cr = rewrite(c.substitute(
       d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
   if (cr.isConst())
   {
@@ -548,7 +548,7 @@ TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
     Assert(it->second.find(pv) != it->second.end());
     Node pvs = it->second[pv];
     Assert(d_vars.size() == dt.d_curr.size());
-    Node pvsr = Rewriter::rewrite(pvs.substitute(
+    Node pvsr = rewrite(pvs.substitute(
         d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
     next.push_back(pvsr);
   }
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index d6dec6f71..32d9e22e7 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -23,7 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
-
+#include "smt/env_obj.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/single_inv_partition.h"
@@ -111,10 +111,10 @@ enum TraceIncStatus
  * The invariant-to-synthesize can either be explicitly given, via a call
  * to initialize( f, vars ), or otherwise inferred if this method is not called.
  */
-class TransitionInference
+class TransitionInference : protected EnvObj
 {
  public:
-  TransitionInference() : d_complete(false) {}
+  TransitionInference(Env& env) : EnvObj(env), d_complete(false) {}
   /** Process the conjecture n
    *
    * This initializes this class with information related to viewing it as a
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 8c395a958..9cae1f843 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -112,7 +112,6 @@ SetEnumerator& SetEnumerator::operator++()
   }
 
   Assert(d_currentSet.isConst());
-  Assert(d_currentSet == Rewriter::rewrite(d_currentSet));
 
   Trace("set-type-enum") << "SetEnumerator::operator++ d_elementsSoFar = "
                          << d_elementsSoFar << std::endl;
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index b0f2a2472..83062ce48 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -212,7 +212,7 @@ Node SortInference::simplify(Node n,
   std::map<Node, Node> var_bound;
   TypeNode tnn;
   Node ret = simplifyNode(n, var_bound, tnn, model_replace_f, visited);
-  ret = theory::Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
@@ -806,7 +806,7 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
                                 .eqNode(nm->mkNode(kind::APPLY_UF, f, v2))
                                 .negate(),
                             v1.eqNode(v2)));
-  ret = theory::Rewriter::rewrite( ret );
+  ret = rewrite(ret);
   return ret;
 }
 
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 9396e3e87..1e30b1623 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -605,7 +605,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
     {
       // if constant, compare
       Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need)));
-      cmp = Rewriter::rewrite(cmp);
+      cmp = rewrite(cmp);
       needsSplit = !cmp.getConst<bool>();
     }
     else
@@ -686,7 +686,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       }
       Node len = nm->mkNode(STRING_LENGTH, cols[i][0]);
       Node cons = nm->mkNode(GEQ, len, k_node);
-      cons = Rewriter::rewrite(cons);
+      cons = rewrite(cons);
       ei->d_cardinalityLemK.set(int_k + 1);
       if (!cons.isConst() || !cons.getConst<bool>())
       {
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 2de9bda96..6e2f60c6d 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -209,7 +209,8 @@ bool ExtfSolver::doReduction(int effort, Node n)
         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
     Trace("strings-red-lemma") << "...from " << n << std::endl;
     Trace("strings-red-lemma")
-        << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
+        << "Reduction_" << effort << " rewritten : " << rewrite(nnlem)
+        << std::endl;
     d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
@@ -297,7 +298,7 @@ void ExtfSolver::checkExtfEval(int effort)
           << ", exp " << exp << std::endl;
       einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
       // inference is rewriting the substituted node
-      Node nrc = Rewriter::rewrite(sn);
+      Node nrc = rewrite(sn);
       // if rewrites to a constant, then do the inference and mark as reduced
       if (nrc.isConst())
       {
@@ -332,7 +333,7 @@ void ExtfSolver::checkExtfEval(int effort)
           {
             Trace("strings-extf-debug")
                 << "  rewrite " << nrs << "..." << std::endl;
-            Node nrsr = Rewriter::rewrite(nrs);
+            Node nrsr = rewrite(nrs);
             // ensure the symbolic form is not rewritable
             if (nrsr != nrs)
             {
@@ -544,7 +545,7 @@ void ExtfSolver::checkExtfInference(Node n,
         {
           children[index] = nrc;
           Node conc = nm->mkNode(STRING_CONTAINS, children);
-          conc = Rewriter::rewrite(pol ? conc : conc.negate());
+          conc = rewrite(pol ? conc : conc.negate());
           // check if it already (does not) hold
           if (d_state.hasTerm(conc))
           {
@@ -605,7 +606,7 @@ void ExtfSolver::checkExtfInference(Node n,
           Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
           Node concOrig =
               nm->mkNode(STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
-          Node conc = Rewriter::rewrite(concOrig);
+          Node conc = rewrite(concOrig);
           // For termination concerns, we only do the inference if the contains
           // does not rewrite (and thus does not introduce new terms).
           if (conc == concOrig)
@@ -654,7 +655,7 @@ void ExtfSolver::checkExtfInference(Node n,
   // If it's not a predicate, see if we can solve the equality n = c, where c
   // is the constant that extended term n is equal to.
   Node inferEq = nr.eqNode(in.d_const);
-  Node inferEqr = Rewriter::rewrite(inferEq);
+  Node inferEqr = rewrite(inferEq);
   Node inferEqrr = inferEqr;
   if (inferEqr.getKind() == EQUAL)
   {
@@ -663,7 +664,7 @@ void ExtfSolver::checkExtfInference(Node n,
   }
   if (inferEqrr != inferEqr)
   {
-    inferEqrr = Rewriter::rewrite(inferEqrr);
+    inferEqrr = rewrite(inferEqrr);
     Trace("strings-extf-infer")
         << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
         << " with explanation " << in.d_exp << std::endl;
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a4f100c19..ead18e823 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -141,7 +141,7 @@ bool InferenceManager::sendInference(const std::vector<Node>& exp,
   {
     eq = d_false;
   }
-  else if (Rewriter::rewrite(eq) == d_true)
+  else if (rewrite(eq) == d_true)
   {
     // if trivial, return
     return false;
@@ -234,7 +234,7 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
 bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
 {
   Node eq = a.eqNode(b);
-  eq = Rewriter::rewrite(eq);
+  eq = rewrite(eq);
   if (eq.isConst())
   {
     return false;
@@ -243,7 +243,7 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
   InferInfo iiSplit(infer);
   iiSplit.d_sim = this;
   iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
-  eq = Rewriter::rewrite(eq);
+  eq = rewrite(eq);
   addPendingPhaseRequirement(eq, preq);
   addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
   return true;
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 28ab63d05..dfb246954 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -100,8 +100,7 @@ Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
   {
     exp.push_back(te.eqNode(lengthTerm));
   }
-  return Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
+  return rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
 }
 
 Node SolverState::getLength(Node t, std::vector<Node>& exp)
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 688f232a1..61fe786d6 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -372,7 +372,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
   if (n.getKind() != STRING_CONCAT && !n.isConst())
   {
     Node lsumb = nm->mkNode(STRING_LENGTH, n);
-    lsum = Rewriter::rewrite(lsumb);
+    lsum = rewrite(lsumb);
     // can register length term if it does not rewrite
     if (lsum == lsumb)
     {
@@ -381,7 +381,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
     }
   }
   Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
-  Node eq = Rewriter::rewrite(sk.eqNode(n));
+  Node eq = rewrite(sk.eqNode(n));
   d_proxyVar[n] = sk;
   // If we are introducing a proxy for a constant or concat term, we do not
   // need to send lemmas about its length, since its length is already
@@ -410,7 +410,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
       }
     }
     lsum = nm->mkNode(PLUS, nodeVec);
-    lsum = Rewriter::rewrite(lsum);
+    lsum = rewrite(lsum);
   }
   else if (n.isConst())
   {
@@ -418,7 +418,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
   }
   Assert(!lsum.isNull());
   d_proxyVarToLength[sk] = lsum;
-  Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
+  Node ceq = rewrite(skl.eqNode(lsum));
 
   Node ret = nm->mkNode(AND, eq, ceq);
 
@@ -538,16 +538,16 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
   Node n_len_eq_z = n_len.eqNode(d_zero);
   Node n_len_eq_z_2 = n.eqNode(emp);
   Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
-  Node case_emptyr = Rewriter::rewrite(case_empty);
+  Node case_emptyr = rewrite(case_empty);
   if (!case_emptyr.isConst())
   {
     // prefer trying the empty case first
     // notice that requirePhase must only be called on rewritten literals that
     // occur in the CNF stream.
-    n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
+    n_len_eq_z = rewrite(n_len_eq_z);
     Assert(!n_len_eq_z.isConst());
     reqPhase[n_len_eq_z] = true;
-    n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
+    n_len_eq_z_2 = rewrite(n_len_eq_z_2);
     Assert(!n_len_eq_z_2.isConst());
     reqPhase[n_len_eq_z_2] = true;
   }
@@ -576,7 +576,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
       return Node::null();
     }
     Node eq = n.eqNode(pn);
-    eq = Rewriter::rewrite(eq);
+    eq = rewrite(eq);
     if (std::find(exp.begin(), exp.end(), eq) == exp.end())
     {
       exp.push_back(eq);
@@ -643,7 +643,7 @@ void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
     return;
   }
   Trace("strings-subs-proxy") << "Input : " << n << std::endl;
-  Node ns = Rewriter::rewrite(n);
+  Node ns = rewrite(n);
   if (ns.getKind() == EQUAL)
   {
     for (size_t i = 0; i < 2; i++)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 53365e1b6..9b65a3e1c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -538,9 +538,11 @@ bool TheoryEngine::properConflict(TNode conflict) const {
                                 << conflict[i] << endl;
         return false;
       }
-      if (conflict[i] != Rewriter::rewrite(conflict[i])) {
-        Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
-                                << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
+      if (conflict[i] != rewrite(conflict[i]))
+      {
+        Debug("properConflict")
+            << "Bad conflict is due to atom not in normal form: " << conflict[i]
+            << " vs " << rewrite(conflict[i]) << endl;
         return false;
       }
     }
@@ -555,9 +557,11 @@ bool TheoryEngine::properConflict(TNode conflict) const {
                               << conflict << endl;
       return false;
     }
-    if (conflict != Rewriter::rewrite(conflict)) {
-      Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
-                              << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
+    if (conflict != rewrite(conflict))
+    {
+      Debug("properConflict")
+          << "Bad conflict is due to atom not in normal form: " << conflict
+          << " vs " << rewrite(conflict) << endl;
       return false;
     }
   }
@@ -905,7 +909,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
              && assertion[0].getKind() == kind::EQUAL));
 
   // Normalize
-  Node normalizedLiteral = Rewriter::rewrite(assertion);
+  Node normalizedLiteral = rewrite(assertion);
 
   // See if it rewrites false directly -> conflict
   if (normalizedLiteral.isConst()) {
@@ -1212,7 +1216,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
     }
 
     // Rewrite the equality
-    Node eqNormalized = Rewriter::rewrite(atoms[i]);
+    Node eqNormalized = rewrite(atoms[i]);
 
     Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
                            << " with nf " << eqNormalized << endl;
@@ -1721,7 +1725,7 @@ TrustNode TheoryEngine::getExplanation(
           continue;
         }
         // otherwise should hold by rewriting
-        Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp));
+        Assert(rewrite(tConc) == rewrite(tExp));
         // tExp
         // ---- MACRO_SR_PRED_TRANSFORM
         // tConc
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index fdd1d07c8..4ed01b618 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -259,7 +259,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
   resourceManager()->spendResource(id);
   Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
   // shouldn't send trivially true or false lemmas
-  Assert(!Rewriter::rewrite(tlem.getProven()).isConst());
+  Assert(!rewrite(tlem.getProven()).isConst());
   d_numCurrentLemmas++;
   d_out.trustedLemma(tlem, p);
   return true;
@@ -327,7 +327,7 @@ TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 
 bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 {
-  Node rewritten = Rewriter::rewrite(lem);
+  Node rewritten = rewrite(lem);
   return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
 }
 
@@ -535,7 +535,7 @@ bool TheoryInferenceManager::hasSentFact() const
 
 bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 {
-  Node rewritten = Rewriter::rewrite(lem);
+  Node rewritten = rewrite(lem);
   if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
   {
     return false;
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 71fe48de8..f711dfdd1 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1204,7 +1204,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
     retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
     if (childrenConst)
     {
-      retNode = Rewriter::rewrite(retNode);
+      retNode = rewrite(retNode);
     }
   }
   d_normalizedCache[r] = retNode;
@@ -1304,7 +1304,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
                                     << " returned " << hni << std::endl;
       Assert(hni.isConst());
       Assert(hni.getType().isSubtypeOf(args[0].getType()));
-      hni = Rewriter::rewrite(args[0].eqNode(hni));
+      hni = rewrite(args[0].eqNode(hni));
       Node hnv = m->getRepresentative(hn);
       Trace("model-builder-debug2") << "      get rep val : " << hn
                                     << " returned " << hnv << std::endl;
@@ -1321,7 +1321,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
         Assert(largs.size() == apply_args.size());
         hnv = hnv[1].substitute(
             largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
-        hnv = Rewriter::rewrite(hnv);
+        hnv = rewrite(hnv);
       }
       Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
                   .isNull());
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 043b0b37c..ee1e35b77 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -274,7 +274,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
     if (tid != THEORY_BOOL)
     {
       Node ppRewritten = ppTheoryRewrite(current, newLemmas);
-      Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
+      Assert(rewrite(ppRewritten) == ppRewritten);
       if (isProofEnabled() && ppRewritten != current)
       {
         TrustNode trn =
@@ -378,7 +378,7 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
     return preprocessWithProof(term, lems);
   }
   // should be in rewritten form here
-  Assert(term == Rewriter::rewrite(term));
+  Assert(term == rewrite(term));
   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
   // do not rewrite inside quantifiers
   Node newTerm = term;
@@ -406,7 +406,7 @@ Node TheoryPreprocessor::rewriteWithProof(Node term,
                                           TConvProofGenerator* pg,
                                           bool isPre)
 {
-  Node termr = Rewriter::rewrite(term);
+  Node termr = rewrite(term);
   // store rewrite step if tracking proofs and it rewrites
   if (isProofEnabled())
   {
@@ -429,7 +429,7 @@ Node TheoryPreprocessor::preprocessWithProof(Node term,
   // recorded in d_tpg are functional. In other words, there should not
   // be steps from the same term to multiple rewritten forms, which would be
   // the case if we registered a preprocessing step for a non-rewritten term.
-  Assert(term == Rewriter::rewrite(term));
+  Assert(term == rewrite(term));
   Trace("tpp-debug2") << "preprocessWithProof " << term
                       << ", #lems = " << lems.size() << std::endl;
   // We never call ppRewrite on equalities here, since equalities have a
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 83862e8bb..a25a2f470 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1533,7 +1533,7 @@ void CardinalityExtension::check(Theory::Effort level)
                 for( unsigned j=0; j<itel->second.size(); j++ ){
                   Node b = itel->second[j];
                   if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
-                    Node eq = Rewriter::rewrite( a.eqNode( b ) );
+                    Node eq = rewrite(a.eqNode(b));
                     Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                     Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
                     d_im.lemma(lem, InferenceId::UF_CARD_SPLIT);
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index e23262746..2702d6d24 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -259,8 +259,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
         // witness via assertions.
         if (!d_state.areDisequal(itf->second[j], itf->second[k]))
         {
-          Node deq =
-              Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
+          Node deq = rewrite(itf->second[j].eqNode(itf->second[k]).negate());
           // either add to model, or add lemma
           if (isCollectModel)
           {
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index da75d0eea..94ba490c5 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -163,9 +163,10 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
-    : ContextNotifyObj(context),
-      d_assertionsToRerun(context),
+SymmetryBreaker::SymmetryBreaker(Env& env, std::string name)
+    : EnvObj(env),
+      ContextNotifyObj(userContext()),
+      d_assertionsToRerun(userContext()),
       d_rerunningAssertions(false),
       d_phi(),
       d_phiSet(),
@@ -206,7 +207,7 @@ void SymmetryBreaker::rerunAssertionsIfNecessary() {
 }
 
 Node SymmetryBreaker::norm(TNode phi) {
-  Node n = Rewriter::rewrite(phi);
+  Node n = rewrite(phi);
   return normInternal(n, 0);
 }
 
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 67eabb6ba..7dca823dd 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -58,8 +58,8 @@ namespace cvc5 {
 namespace theory {
 namespace uf {
 
-class SymmetryBreaker : public context::ContextNotifyObj {
-
+class SymmetryBreaker : protected EnvObj, public context::ContextNotifyObj
+{
   class Template {
     Node d_template;
     NodeBuilder d_assertions;
@@ -158,12 +158,12 @@ public:
   }
 
  public:
-  SymmetryBreaker(context::Context* context, std::string name = "");
+  SymmetryBreaker(Env& env, std::string name = "");
 
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);
 
-};/* class SymmetryBreaker */
+}; /* class SymmetryBreaker */
 
 }  // namespace uf
 }  // namespace theory
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 5e9cb0a1d..a7b8d7ad7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -48,7 +48,7 @@ TheoryUF::TheoryUF(Env& env,
       d_thss(nullptr),
       d_ho(nullptr),
       d_functionsTerms(context()),
-      d_symb(userContext(), instanceName),
+      d_symb(env, instanceName),
       d_rewriter(logicInfo().isHigherOrder()),
       d_state(env, valuation),
       d_im(env, *this, d_state, "theory::uf::" + instanceName, false),