pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)

28 files changed, 217 insertions, 203 deletions

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index a789a0d0b..f5152f0d2 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -50,7 +50,7 @@ PreprocessingPassResult BoolToBV::applyInternal(
     for (size_t i = 0; i < size; ++i)
     {
       Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
-      assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion));
+      assertionsToPreprocess->replace(i, rewrite(newAssertion));
     }
   }
   else
@@ -59,7 +59,7 @@ PreprocessingPassResult BoolToBV::applyInternal(
     for (size_t i = 0; i < size; ++i)
     {
       assertionsToPreprocess->replace(
-          i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i])));
+          i, rewrite(lowerIte((*assertionsToPreprocess)[i])));
     }
   }
 
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index 597481678..cea5bf37c 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -53,7 +53,7 @@ PreprocessingPassResult BvAbstraction::applyInternal(
   bv_theory->applyAbstraction(assertions, new_assertions);
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
-    assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
+    assertionsToPreprocess->replace(i, rewrite(new_assertions[i]));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index b3c34087d..e49cc5c44 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -37,28 +37,24 @@ namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
-namespace {
-
-bool is_bv_const(Node n)
+bool BVGauss::is_bv_const(Node n)
 {
   if (n.isConst()) { return true; }
-  return Rewriter::rewrite(n).getKind() == kind::CONST_BITVECTOR;
+  return rewrite(n).getKind() == kind::CONST_BITVECTOR;
 }
 
-Node get_bv_const(Node n)
+Node BVGauss::get_bv_const(Node n)
 {
   Assert(is_bv_const(n));
-  return Rewriter::rewrite(n);
+  return rewrite(n);
 }
 
-Integer get_bv_const_value(Node n)
+Integer BVGauss::get_bv_const_value(Node n)
 {
   Assert(is_bv_const(n));
   return get_bv_const(n).getConst<BitVector>().getValue();
 }
 
-}  // namespace
-
 /**
  * Determines if an overflow may occur in given 'expr'.
  *
@@ -75,7 +71,7 @@ Integer get_bv_const_value(Node n)
  * will be handled via the default case, which is not incorrect but also not
  * necessarily the minimum.
  */
-unsigned BVGauss::getMinBwExpr(Node expr)
+uint32_t BVGauss::getMinBwExpr(Node expr)
 {
   std::vector<Node> visit;
   /* Maps visited nodes to the determined minimum bit-width required. */
@@ -454,7 +450,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
       Assert(is_bv_const(eq[0]));
       eqrhs = eq[0];
     }
-    if (getMinBwExpr(Rewriter::rewrite(urem[0])) == 0)
+    if (getMinBwExpr(rewrite(urem[0])) == 0)
     {
       Trace("bv-gauss-elim")
           << "Minimum required bit-width exceeds given bit-width, "
@@ -504,7 +500,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
         NodeBuilder nb_nonconsts(NodeManager::currentNM(), k);
         for (const Node& nn : n)
         {
-          Node nnrw = Rewriter::rewrite(nn);
+          Node nnrw = rewrite(nn);
           if (is_bv_const(nnrw))
           {
             nb_consts << nnrw;
@@ -519,7 +515,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
         unsigned nc = nb_consts.getNumChildren();
         if (nc > 1)
         {
-          n0 = Rewriter::rewrite(nb_consts.constructNode());
+          n0 = rewrite(nb_consts.constructNode());
         }
         else if (nc == 1)
         {
@@ -532,7 +528,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
         /* n1 is a mult with non-const operands */
         if (nb_nonconsts.getNumChildren() > 1)
         {
-          n1 = Rewriter::rewrite(nb_nonconsts.constructNode());
+          n1 = rewrite(nb_nonconsts.constructNode());
         }
         else
         {
diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 8fafcb741..0078770fb 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -93,14 +93,29 @@ class BVGauss : public PreprocessingPass
     NONE
   };
 
-  static Result gaussElim(Integer prime,
-                          std::vector<Integer>& rhs,
-                          std::vector<std::vector<Integer>>& lhs);
+  Result gaussElim(Integer prime,
+                   std::vector<Integer>& rhs,
+                   std::vector<std::vector<Integer>>& lhs);
 
-  static Result gaussElimRewriteForUrem(const std::vector<Node>& equations,
-                                        std::unordered_map<Node, Node>& res);
+  Result gaussElimRewriteForUrem(const std::vector<Node>& equations,
+                                 std::unordered_map<Node, Node>& res);
 
-  static unsigned getMinBwExpr(Node expr);
+  uint32_t getMinBwExpr(Node expr);
+
+  /**
+   * Return true if given node is a bit-vector value (after rewriting).
+   */
+  bool is_bv_const(Node n);
+  /**
+   * Return the bit-vector value resulting from rewriting node 'n'.
+   * Asserts that given node can be rewritten to a bit-vector value.
+   */
+  Node get_bv_const(Node n);
+  /**
+   * Return the Integer value representing the given bit-vector value.
+   * Asserts that given node can be rewritten to a bit-vector value.
+   */
+  Integer get_bv_const_value(Node n);
 };
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 45df7478c..ff0657dcd 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -94,7 +94,7 @@ PreprocessingPassResult BvIntroPow2::applyInternal(
     Node res = pow2Rewrite(cur, cache);
     if (res != cur)
     {
-      res = Rewriter::rewrite(res);
+      res = rewrite(res);
       assertionsToPreprocess->replace(i, res);
     }
   }
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index cd58a3faf..0d0131e3e 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -53,7 +53,7 @@ PreprocessingPassResult BVToBool::applyInternal(
   liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
-    assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
+    assertionsToPreprocess->replace(i, rewrite(new_assertions[i]));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }
@@ -281,7 +281,7 @@ void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
   for (unsigned i = 0; i < assertions.size(); ++i)
   {
     Node new_assertion = liftNode(assertions[i]);
-    new_assertions.push_back(Rewriter::rewrite(new_assertion));
+    new_assertions.push_back(rewrite(new_assertion));
     Trace("bv-to-bool") << "  " << assertions[i] << " => " << new_assertions[i]
                         << "\n";
   }
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 65c9bb012..cc631f4bc 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -60,7 +60,7 @@ Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k)
   Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar);
   Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k));
   Node result = d_nm->mkNode(kind::AND, lower, upper);
-  return Rewriter::rewrite(result);
+  return rewrite(result);
 }
 
 Node BVToInt::maxInt(uint64_t k)
@@ -256,7 +256,7 @@ Node BVToInt::eliminationPass(Node n)
 Node BVToInt::bvToInt(Node n)
 {
   // make sure the node is re-written before processing it.
-  n = Rewriter::rewrite(n);
+  n = rewrite(n);
   n = makeBinary(n);
   n = eliminationPass(n);
   // binarize again, in case the elimination pass introduced
@@ -946,7 +946,7 @@ PreprocessingPassResult BVToInt::applyInternal(
   {
     Node bvNode = (*assertionsToPreprocess)[i];
     Node intNode = bvToInt(bvNode);
-    Node rwNode = Rewriter::rewrite(intNode);
+    Node rwNode = rewrite(intNode);
     Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl;
     Trace("bv-to-int-debug") << "int node: " << intNode << std::endl;
     Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl;
@@ -966,7 +966,7 @@ void BVToInt::addFinalizeRangeAssertions(
   vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
   // conjoin all range assertions and add the conjunction
   // as a new assertion
-  Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range));
+  Node rangeAssertions = rewrite(d_nm->mkAnd(vec_range));
   assertionsToPreprocess->push_back(rangeAssertions);
   Trace("bv-to-int-debug") << "range constraints: "
                            << rangeAssertions.toString() << std::endl;
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index 6040b3669..24edf1509 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -36,7 +36,7 @@ ForeignTheoryRewrite::ForeignTheoryRewrite(
 Node ForeignTheoryRewrite::simplify(Node n)
 {
   std::vector<Node> toVisit;
-  n = Rewriter::rewrite(n);
+  n = rewrite(n);
   toVisit.push_back(n);
   // traverse n and rewrite until fixpoint
   while (!toVisit.empty())
@@ -143,7 +143,7 @@ PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     assertionsToPreprocess->replace(
-        i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i])));
+        i, rewrite(simplify((*assertionsToPreprocess)[i])));
   }
 
   return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 2405702b0..7e8f3ffab 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -153,7 +153,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
             << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
         Trace("fmf-fun-def") << "  to " << std::endl;
         Node new_q = nm->mkNode(FORALL, bvl, bd);
-        new_q = Rewriter::rewrite(new_q);
+        new_q = rewrite(new_q);
         assertionsToPreprocess->replace(i, new_q);
         Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
         fd_assertions.push_back(i);
@@ -187,7 +187,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
     Assert(constraints.empty());
     if (n != assertions[i])
     {
-      n = Rewriter::rewrite(n);
+      n = rewrite(n);
       Trace("fmf-fun-def-rewrite")
           << "FMF fun def : rewrite " << assertions[i] << std::endl;
       Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
@@ -232,7 +232,7 @@ Node FunDefFmf::simplifyFormula(
     for (unsigned i = 0; i < constraints.size(); i++)
     {
       constraints[i] = nm->mkNode(FORALL, n[0], constraints[i]);
-      constraints[i] = Rewriter::rewrite(constraints[i]);
+      constraints[i] = rewrite(constraints[i]);
     }
     if (c != n[1])
     {
@@ -365,7 +365,7 @@ Node FunDefFmf::simplifyFormula(
     if (constraints.size() > 1)
     {
       cons = nm->mkNode(AND, constraints);
-      cons = Rewriter::rewrite(cons);
+      cons = rewrite(cons);
       constraints.clear();
       constraints.push_back(cons);
     }
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index e990f8868..cd8ecc73f 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -94,7 +94,7 @@ Node GlobalNegate::simplify(const std::vector<Node>& assertions,
   }
 
   Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
-  body = Rewriter::rewrite(body);
+  body = rewrite(body);
   Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl;
   return body;
 }
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 27dcf651b..515cc4a32 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -315,7 +315,7 @@ PreprocessingPassResult HoElim::applyInternal(
     Node res = eliminateLambdaComplete(prev, newLambda);
     if (res != prev)
     {
-      res = theory::Rewriter::rewrite(res);
+      res = rewrite(res);
       Assert(!expr::hasFreeVar(res));
       assertionsToPreprocess->replace(i, res);
     }
@@ -361,7 +361,7 @@ PreprocessingPassResult HoElim::applyInternal(
   if (!axioms.empty())
   {
     Node conj = nm->mkAnd(axioms);
-    conj = theory::Rewriter::rewrite(conj);
+    conj = rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
     assertionsToPreprocess->conjoin(0, conj);
   }
@@ -374,7 +374,7 @@ PreprocessingPassResult HoElim::applyInternal(
     Node res = eliminateHo(prev);
     if (res != prev)
     {
-      res = theory::Rewriter::rewrite(res);
+      res = rewrite(res);
       Assert(!expr::hasFreeVar(res));
       assertionsToPreprocess->replace(i, res);
     }
@@ -456,7 +456,7 @@ PreprocessingPassResult HoElim::applyInternal(
   if (!axioms.empty())
   {
     Node conj = nm->mkAnd(axioms);
-    conj = theory::Rewriter::rewrite(conj);
+    conj = rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
     assertionsToPreprocess->conjoin(0, conj);
   }
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 41d52d1ae..46c75b560 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -203,7 +203,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
       // Mark the substitution and continue
       Node result = builder;
 
-      result = Rewriter::rewrite(result);
+      result = rewrite(result);
       cache[current] = result;
     }
     else
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 7578bcad6..97e56c58c 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -64,7 +64,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
-    assertions->replace(i, Rewriter::rewrite((*assertions)[i]));
+    assertions->replace(i, rewrite((*assertions)[i]));
   }
 
   return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp
index 81fbf1ea1..c2693e927 100644
--- a/src/preprocessing/passes/learned_rewrite.cpp
+++ b/src/preprocessing/passes/learned_rewrite.cpp
@@ -233,7 +233,7 @@ Node LearnedRewrite::rewriteLearned(Node n,
 {
   NodeManager* nm = NodeManager::currentNM();
   Trace("learned-rewrite-rr-debug") << "Rewrite " << n << std::endl;
-  Node nr = Rewriter::rewrite(n);
+  Node nr = rewrite(n);
   Kind k = nr.getKind();
   if (k == INTS_DIVISION || k == INTS_MODULUS || k == DIVISION)
   {
@@ -278,7 +278,7 @@ Node LearnedRewrite::rewriteLearned(Node n,
       children.insert(children.end(), n.begin(), n.end());
       Node ret = nm->mkNode(nk, children);
       nr = returnRewriteLearned(nr, ret, LearnedRewriteId::NON_ZERO_DEN);
-      nr = Rewriter::rewrite(nr);
+      nr = rewrite(nr);
       k = nr.getKind();
     }
   }
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index a5720e758..3ef4b7e9f 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -43,11 +43,58 @@ using namespace cvc5::theory;
 namespace {
 
 /**
+ * Trace nodes back to their assertions using CircuitPropagator's
+ * BackEdgesMap.
+ */
+void traceBackToAssertions(booleans::CircuitPropagator* propagator,
+                           const std::vector<Node>& nodes,
+                           std::vector<TNode>& assertions)
+{
+  const booleans::CircuitPropagator::BackEdgesMap& backEdges =
+      propagator->getBackEdges();
+  for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
+  {
+    booleans::CircuitPropagator::BackEdgesMap::const_iterator j =
+        backEdges.find(*i);
+    // term must appear in map, otherwise how did we get here?!
+    Assert(j != backEdges.end());
+    // if term maps to empty, that means it's a top-level assertion
+    if (!(*j).second.empty())
+    {
+      traceBackToAssertions(propagator, (*j).second, assertions);
+    }
+    else
+    {
+      assertions.push_back(*i);
+    }
+  }
+}
+
+}  // namespace
+
+MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "miplib-trick")
+{
+  if (!options::incrementalSolving())
+  {
+    NodeManager::currentNM()->subscribeEvents(this);
+  }
+}
+
+MipLibTrick::~MipLibTrick()
+{
+  if (!options::incrementalSolving())
+  {
+    NodeManager::currentNM()->unsubscribeEvents(this);
+  }
+}
+
+/**
  * Remove conjuncts in toRemove from conjunction n. Return # of removed
  * conjuncts.
  */
-size_t removeFromConjunction(Node& n,
-                             const std::unordered_set<unsigned long>& toRemove)
+size_t MipLibTrick::removeFromConjunction(
+    Node& n, const std::unordered_set<unsigned long>& toRemove)
 {
   Assert(n.getKind() == kind::AND);
   Node trueNode = NodeManager::currentNM()->mkConst(true);
@@ -109,7 +156,7 @@ size_t removeFromConjunction(Node& n,
       {
         n = b;
       }
-      n = Rewriter::rewrite(n);
+      n = rewrite(n);
       return removals;
     }
   }
@@ -118,53 +165,6 @@ size_t removeFromConjunction(Node& n,
   return 0;
 }
 
-/**
- * Trace nodes back to their assertions using CircuitPropagator's
- * BackEdgesMap.
- */
-void traceBackToAssertions(booleans::CircuitPropagator* propagator,
-                           const std::vector<Node>& nodes,
-                           std::vector<TNode>& assertions)
-{
-  const booleans::CircuitPropagator::BackEdgesMap& backEdges =
-      propagator->getBackEdges();
-  for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
-  {
-    booleans::CircuitPropagator::BackEdgesMap::const_iterator j =
-        backEdges.find(*i);
-    // term must appear in map, otherwise how did we get here?!
-    Assert(j != backEdges.end());
-    // if term maps to empty, that means it's a top-level assertion
-    if (!(*j).second.empty())
-    {
-      traceBackToAssertions(propagator, (*j).second, assertions);
-    }
-    else
-    {
-      assertions.push_back(*i);
-    }
-  }
-}
-
-}  // namespace
-
-MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "miplib-trick")
-{
-  if (!options::incrementalSolving())
-  {
-    NodeManager::currentNM()->subscribeEvents(this);
-  }
-}
-
-MipLibTrick::~MipLibTrick()
-{
-  if (!options::incrementalSolving())
-  {
-    NodeManager::currentNM()->unsubscribeEvents(this);
-  }
-}
-
 void MipLibTrick::nmNotifyNewVar(TNode n)
 {
   if (n.getType().isBoolean())
@@ -530,12 +530,12 @@ PreprocessingPassResult MipLibTrick::applyInternal(
                   nm->integerType(),
                   "a variable introduced due to scrubbing a miplib encoding",
                   NodeManager::SKOLEM_EXACT_NAME);
-              Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
-              Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
+              Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero));
+              Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one));
               TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
               TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr);
 
-              Node n = Rewriter::rewrite(geq.andNode(leq));
+              Node n = rewrite(geq.andNode(leq));
               assertionsToPreprocess->push_back(n);
               TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
               CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get();
@@ -575,8 +575,8 @@ PreprocessingPassResult MipLibTrick::applyInternal(
                 kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]);
           }
           Debug("miplib") << "vars[] " << var << endl
-                          << "    eq " << Rewriter::rewrite(sum) << endl;
-          Node newAssertion = var.eqNode(Rewriter::rewrite(sum));
+                          << "    eq " << rewrite(sum) << endl;
+          Node newAssertion = var.eqNode(rewrite(sum));
           if (top_level_substs.hasSubstitution(newAssertion[0]))
           {
             // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
@@ -599,7 +599,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
                 << " (threshold is " << options::arithMLTrickSubstitutions()
                 << ")" << endl;
           }
-          newAssertion = Rewriter::rewrite(newAssertion);
+          newAssertion = rewrite(newAssertion);
           Debug("miplib") << "  " << newAssertion << endl;
 
           assertionsToPreprocess->push_back(newAssertion);
@@ -642,7 +642,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
       }
       Debug("miplib") << "had: " << assertion[i] << endl;
       assertionsToPreprocess->replace(
-          i, Rewriter::rewrite(top_level_substs.apply(assertion)));
+          i, rewrite(top_level_substs.apply(assertion)));
       Debug("miplib") << "now: " << assertion << endl;
     }
   }
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index c63885cf0..537d27a0a 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -49,6 +49,9 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener
     Statistics();
   };
 
+  size_t removeFromConjunction(
+      Node& n, const std::unordered_set<unsigned long>& toRemove);
+
   Statistics d_statistics;
 
   std::vector<Node> d_boolVars;
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index afd21fb7a..27f34f177 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -64,7 +64,7 @@ Node NlExtPurify::purifyNlTerms(TNode n,
         && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
     {
       // don't do it if it rewrites to a constant
-      Node nr = Rewriter::rewrite(n);
+      Node nr = rewrite(n);
       if (nr.isConst())
       {
         // return the rewritten constant
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index ca61c9197..6c93eba15 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -210,7 +210,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
                                                Node orig)
 {
   Assert(assertion.getKind() == kind::GEQ);
-  Assert(assertion == Rewriter::rewrite(assertion));
+  Assert(assertion == rewrite(assertion));
 
   // assume assertion is rewritten
   Node l = assertion[0];
@@ -264,7 +264,7 @@ void PseudoBooleanProcessor::learnInternal(Node assertion,
     case kind::LEQ:
     case kind::LT:
     {
-      Node rw = Rewriter::rewrite(assertion);
+      Node rw = rewrite(assertion);
       if (assertion == rw)
       {
         if (assertion.getKind() == kind::GEQ)
@@ -320,7 +320,7 @@ void PseudoBooleanProcessor::addSub(Node from, Node to)
 {
   if (!d_subCache.hasSubstitution(from))
   {
-    Node rw_to = Rewriter::rewrite(to);
+    Node rw_to = rewrite(to);
     d_subCache.addSubstitution(from, rw_to);
   }
 }
@@ -386,7 +386,7 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq)
 
 Node PseudoBooleanProcessor::applyReplacements(Node pre)
 {
-  Node assertion = Rewriter::rewrite(pre);
+  Node assertion = rewrite(pre);
 
   Node result = d_subCache.apply(assertion);
   if (Debug.isOn("pbs::rewrites") && result != assertion)
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index c0bb0ea7f..f80c4383c 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -45,7 +45,7 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal(
     if (!trn.isNull())
     {
       Node next = trn.getNode();
-      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
+      assertionsToPreprocess->replace(i, rewrite(next));
       Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
       Trace("quantifiers-preprocess")
           << "   ...got " << (*assertionsToPreprocess)[i] << endl;
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 3cfc29ed6..9e2170ffd 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -57,7 +57,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
           || n.getKind() == kind::GEQ || n.getKind() == kind::LT
           || n.getKind() == kind::GT || n.getKind() == kind::LEQ)
       {
-        ret = Rewriter::rewrite(n);
+        ret = rewrite(n);
         Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
         if (!ret.isConst())
         {
@@ -81,13 +81,12 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
                     Rational(c.getConst<Rational>().getDenominator())));
               }
             }
-            Node cc =
-                coeffs.empty()
-                    ? Node::null()
-                    : (coeffs.size() == 1
-                           ? coeffs[0]
-                           : Rewriter::rewrite(NodeManager::currentNM()->mkNode(
-                                 kind::MULT, coeffs)));
+            Node cc = coeffs.empty()
+                          ? Node::null()
+                          : (coeffs.size() == 1
+                                 ? coeffs[0]
+                                 : rewrite(NodeManager::currentNM()->mkNode(
+                                     kind::MULT, coeffs)));
             std::vector<Node> sum;
             for (std::map<Node, Node>::iterator itm = msum.begin();
                  itm != msum.end();
@@ -105,7 +104,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
               {
                 if (!cc.isNull())
                 {
-                  c = Rewriter::rewrite(
+                  c = rewrite(
                       NodeManager::currentNM()->mkNode(kind::MULT, c, cc));
                 }
               }
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index 4704f1cb5..0e7aafcc3 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -34,7 +34,7 @@ PreprocessingPassResult Rewrite::applyInternal(
   AssertionPipeline* assertionsToPreprocess)
 {
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
-    assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i]));
+    assertionsToPreprocess->replace(i, rewrite((*assertionsToPreprocess)[i]));
   }
 
   return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 4322e60d5..37bf0fd8b 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -113,7 +113,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
     Node next = preSkolemEmp(prev, pol, visited);
     if (next != prev)
     {
-      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
+      assertionsToPreprocess->replace(i, rewrite(next));
       Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
       Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i]
                               << endl;
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 7b93f43cf..c139f0a86 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -52,7 +52,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
       Node next = si->simplify(prev, model_replace_f, visited);
       if (next != prev)
       {
-        next = theory::Rewriter::rewrite(next);
+        next = rewrite(next);
         assertionsToPreprocess->replace(i, next);
         Trace("sort-infer-preprocess")
             << "*** Preprocess SortInferencePass " << prev << endl;
@@ -64,7 +64,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
     si->getNewAssertions(newAsserts);
     for (const Node& na : newAsserts)
     {
-      Node nar = theory::Rewriter::rewrite(na);
+      Node nar = rewrite(na);
       Trace("sort-infer-preprocess")
           << "*** Preprocess SortInferencePass : new constraint " << nar
           << endl;
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 09d24d900..24d25e354 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -47,8 +47,7 @@ PreprocessingPassResult StaticLearning::applyInternal(
     }
     else
     {
-      assertionsToPreprocess->replace(
-          i, theory::Rewriter::rewrite(learned.constructNode()));
+      assertionsToPreprocess->replace(i, rewrite(learned.constructNode()));
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 6ab3a9bd2..80d6dd0e8 100644
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -49,7 +49,7 @@ PreprocessingPassResult StringsEagerPp::applyInternal(
     }
     if (prev != rew)
     {
-      assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew));
+      assertionsToPreprocess->replace(i, rewrite(rew));
     }
   }
 
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 8194f9f52..8abd77a27 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -65,7 +65,7 @@ PreprocessingPassResult SygusInference::applyInternal(
           prev.substitute(funs.begin(), funs.end(), sols.begin(), sols.end());
       if (curr != prev)
       {
-        curr = theory::Rewriter::rewrite(curr);
+        curr = rewrite(curr);
         Trace("sygus-infer-debug")
             << "...rewrote " << prev << " to " << curr << std::endl;
         assertionsToPreprocess->replace(i, curr);
@@ -127,7 +127,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
     std::map<TypeNode, unsigned> type_count;
     Node pas = as;
     // rewrite
-    pas = theory::Rewriter::rewrite(pas);
+    pas = rewrite(pas);
     Trace("sygus-infer") << "assertion : " << pas << std::endl;
     if (pas.getKind() == FORALL)
     {
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index c8ddfc2fa..c59aa86ef 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -231,7 +231,7 @@ void UnconstrainedSimplifier::processUnconstrained()
               // Special case: condition is unconstrained, then and else are
               // different, and total cardinality of the type is 2, then the
               // result is unconstrained
-              Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
+              Node test = rewrite(parent[1].eqNode(parent[2]));
               if (test == nm->mkConst<bool>(false))
               {
                 ++d_numUnconstrainedElim;
@@ -530,7 +530,7 @@ void UnconstrainedSimplifier::processUnconstrained()
             {
               // TODO(#2377): could build ITE here
               Node test = other.eqNode(nm->mkConst<Rational>(0));
-              if (Rewriter::rewrite(test) != nm->mkConst<bool>(false))
+              if (rewrite(test) != nm->mkConst<bool>(false))
               {
                 break;
               }
@@ -573,7 +573,7 @@ void UnconstrainedSimplifier::processUnconstrained()
               Node test = nm->mkNode(extractOp, children);
               BitVector one(1, unsigned(1));
               test = test.eqNode(nm->mkConst<BitVector>(one));
-              if (Rewriter::rewrite(test) != nm->mkConst<bool>(true))
+              if (rewrite(test) != nm->mkConst<bool>(true))
               {
                 done = true;
                 break;
@@ -753,8 +753,7 @@ void UnconstrainedSimplifier::processUnconstrained()
             }
             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             current = parent;
-            Node test =
-                Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
+            Node test = rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
             if (test == nm->mkConst<bool>(false))
             {
               break;
@@ -861,7 +860,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
     for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
     {
       Node a = assertions[i];
-      Node as = Rewriter::rewrite(d_substitutions.apply(a));
+      Node as = rewrite(d_substitutions.apply(a));
       // replace the assertion
       assertionsToPreprocess->replace(i, as);
     }
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 8f6fa7b14..68758f766 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -48,6 +48,8 @@ class TestPPWhiteBVGauss : public TestSmt
     d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
         d_smtEngine.get(), d_smtEngine->getEnv(), nullptr));
 
+    d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));
+
     d_zero = bv::utils::mkZero(16);
 
     d_p = bv::utils::mkConcat(
@@ -147,7 +149,7 @@ class TestPPWhiteBVGauss : public TestSmt
     std::cout << "Input: " << std::endl;
     print_matrix_dbg(rhs, lhs);
 
-    ret = BVGauss::gaussElim(prime, resrhs, reslhs);
+    ret = d_bv_gauss->gaussElim(prime, resrhs, reslhs);
 
     std::cout << "BVGauss::Result: "
               << (ret == BVGauss::Result::INVALID
@@ -199,6 +201,7 @@ class TestPPWhiteBVGauss : public TestSmt
   }
 
   std::unique_ptr<PreprocessingPassContext> d_preprocContext;
+  std::unique_ptr<BVGauss> d_bv_gauss;
 
   Node d_p;
   Node d_x;
@@ -262,7 +265,7 @@ TEST_F(TestPPWhiteBVGauss, elim_mod)
          {Integer(2), Integer(3), Integer(5)},
          {Integer(4), Integer(0), Integer(5)}};
   std::cout << "matrix 0, modulo 0" << std::endl;  // throws
-  ASSERT_DEATH(BVGauss::gaussElim(Integer(0), rhs, lhs), "prime > 0");
+  ASSERT_DEATH(d_bv_gauss->gaussElim(Integer(0), rhs, lhs), "prime > 0");
   std::cout << "matrix 0, modulo 1" << std::endl;
   testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
   std::cout << "matrix 0, modulo 2" << std::endl;
@@ -931,7 +934,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
   std::unordered_map<Node, Node> res;
-  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
   ASSERT_EQ(res[d_x], d_three32);
@@ -1037,7 +1040,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
   std::unordered_map<Node, Node> res;
-  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
   ASSERT_EQ(res[d_x], d_three32);
@@ -1075,7 +1078,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1199,7 +1202,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1321,7 +1324,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1419,7 +1422,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
       d_eight);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1562,7 +1565,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
       d_thirty);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -1713,7 +1716,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
       d_thirty);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 1);
 
@@ -1820,7 +1823,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
       kind::EQUAL, d_nodeManager->mkNode(kind::BITVECTOR_UREM, w, d_p), d_two);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 3);
 
@@ -1915,7 +1918,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -2086,7 +2089,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
       d_nine);
 
   std::vector<Node> eqs = {eq1, eq2};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
   ASSERT_EQ(res.size(), 2);
 
@@ -2224,7 +2227,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
       d_five);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
 
@@ -2285,7 +2288,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
       bv::utils::mkConcat(d_zero, d_nine));
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
 
@@ -2353,7 +2356,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
       bv::utils::mkConcat(d_zero, d_nine));
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+  ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::INVALID);
 }
 
@@ -2627,15 +2630,15 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw1)
 {
-  ASSERT_EQ(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(bv::utils::mkConst(32, 11)), 4);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(d_p), 4);
-  ASSERT_EQ(BVGauss::getMinBwExpr(d_x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_x), 16);
 
   Node extp = bv::utils::mkExtract(d_p, 4, 0);
-  ASSERT_EQ(BVGauss::getMinBwExpr(extp), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(extp), 4);
   Node extx = bv::utils::mkExtract(d_x, 4, 0);
-  ASSERT_EQ(BVGauss::getMinBwExpr(extx), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(extx), 5);
 
   Node zextop8 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
@@ -2647,132 +2650,132 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
 
   Node zext40p = d_nodeManager->mkNode(zextop8, d_p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext40p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40p), 4);
   Node zext40x = d_nodeManager->mkNode(zextop8, d_x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext40x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40x), 16);
 
   Node zext48p = d_nodeManager->mkNode(zextop16, d_p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p), 4);
   Node zext48x = d_nodeManager->mkNode(zextop16, d_x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x), 16);
 
   Node p8 = d_nodeManager->mkConst<BitVector>(BitVector(8, 11u));
   Node x8 = d_nodeManager->mkVar("x8", d_nodeManager->mkBitVectorType(8));
 
   Node zext48p8 = d_nodeManager->mkNode(zextop40, p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p8), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p8), 4);
   Node zext48x8 = d_nodeManager->mkNode(zextop40, x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x8), 8);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x8), 8);
 
   Node mult1p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extp, extp);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult1p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1p), 5);
   Node mult1x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extx, extx);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult1x), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1x), 0);
 
   Node mult2p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult2p), 7);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2p), 7);
   Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2x), 32);
 
   NodeBuilder nbmult3p(kind::BITVECTOR_MULT);
   nbmult3p << zext48p << zext48p << zext48p;
   Node mult3p = nbmult3p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3p), 11);
   NodeBuilder nbmult3x(kind::BITVECTOR_MULT);
   nbmult3x << zext48x << zext48x << zext48x;
   Node mult3x = nbmult3x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3x), 48);
 
   NodeBuilder nbmult4p(kind::BITVECTOR_MULT);
   nbmult4p << zext48p << zext48p8 << zext48p;
   Node mult4p = nbmult4p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4p), 11);
   NodeBuilder nbmult4x(kind::BITVECTOR_MULT);
   nbmult4x << zext48x << zext48x8 << zext48x;
   Node mult4x = nbmult4x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4x), 40);
 
   Node concat1p = bv::utils::mkConcat(d_p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat1p), 52);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1p), 52);
   Node concat1x = bv::utils::mkConcat(d_x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat1x), 64);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1x), 64);
 
   Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat2p), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2p), 4);
   Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2x), 16);
 
   Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1p), 1);
   Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1x), 48);
 
   Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2p), 1);
   Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2x), 48);
 
   Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1p), 1);
   Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1x), 1);
 
   Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2p), 1);
   Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2x), 16);
 
   Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3p), 1);
   Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3x), 8);
 
   Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extp, extp);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1p), 5);
   Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extx, extx);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1x), 0);
 
   Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40p, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2p), 5);
   Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40x, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2x), 17);
 
   Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48p8, zext48p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3p), 5);
   Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48x8, zext48x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3x), 17);
 
   NodeBuilder nbadd4p(kind::BITVECTOR_ADD);
   nbadd4p << zext48p << zext48p << zext48p;
   Node add4p = nbadd4p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4p), 6);
   NodeBuilder nbadd4x(kind::BITVECTOR_ADD);
   nbadd4x << zext48x << zext48x << zext48x;
   Node add4x = nbadd4x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4x), 18);
 
   NodeBuilder nbadd5p(kind::BITVECTOR_ADD);
   nbadd5p << zext48p << zext48p8 << zext48p;
   Node add5p = nbadd5p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5p), 6);
   NodeBuilder nbadd5x(kind::BITVECTOR_ADD);
   nbadd5x << zext48x << zext48x8 << zext48x;
   Node add5x = nbadd5x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5x), 18);
 
   NodeBuilder nbadd6p(kind::BITVECTOR_ADD);
   nbadd6p << zext48p << zext48p << zext48p << zext48p;
   Node add6p = nbadd6p;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6p), 6);
   NodeBuilder nbadd6x(kind::BITVECTOR_ADD);
   nbadd6x << zext48x << zext48x << zext48x << zext48x;
   Node add6x = nbadd6x;
-  ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6x), 18);
 
   Node not1p = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40p);
-  ASSERT_EQ(BVGauss::getMinBwExpr(not1p), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1p), 40);
   Node not1x = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40x);
-  ASSERT_EQ(BVGauss::getMinBwExpr(not1x), 40);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1x), 40);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw2)
@@ -2786,7 +2789,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw2)
   Node zext1 = d_nodeManager->mkNode(zextop15, d_p);
   Node ext = bv::utils::mkExtract(zext1, 7, 0);
   Node zext2 = d_nodeManager->mkNode(zextop5, ext);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 4);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 4);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
@@ -2805,7 +2808,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
   Node ext2 = bv::utils::mkExtract(z, 4, 0);
   Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
@@ -2821,7 +2824,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
   Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
   Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
@@ -2856,7 +2859,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
@@ -2888,7 +2891,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2);
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
@@ -2994,7 +2997,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 0);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 0);
 }
 
 TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
@@ -3098,8 +3101,8 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
       d_nodeManager->mkNode(
           kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
 
-  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 19);
-  ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 19);
+  ASSERT_EQ(d_bv_gauss->getMinBwExpr(Rewriter::rewrite(plus7)), 17);
 }
 }  // namespace test
 }  // namespace cvc5