Make BVInstantiatorUtil an EnvObj (#8633)

Eliminates 5 of the remaining 8 static calls to Rewriter::rewrite.

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index f5eff833a9f76d3bb043fb9b2a4c8970e479d6e4..156dbc5cc606bb9694fcb45a0f7001ec9b9402d7 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -860,8 +860,7 @@ class CVC5_EXPORT SolverEngine
   std::vector<Node> getExpandedAssertions();
 
   /**
-   * !!!!! temporary, until the environment is passsed to all classes that
-   * require it.
+   * Get the enviornment from this solver engine.
    */
   Env& getEnv();
   /* .......................................................................  */

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 50178ac6300fb0f68ea49fa949dd3ba8814a3642..f0be34902d96566de7e287c93e8a9981616f8e33 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -19,7 +19,6 @@
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 #include "util/random.h"
@@ -55,7 +54,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
 };
 
 BvInstantiator::BvInstantiator(Env& env, TypeNode tn, BvInverter* inv)
-    : Instantiator(env, tn), d_inverter(inv), d_inst_id_counter(0)
+    : Instantiator(env, tn), d_inverter(inv), d_util(env), d_inst_id_counter(0)
 {
   // The inverter utility d_inverter is global to all BvInstantiator classes.
   // This must be global since we need to:
@@ -563,7 +562,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
     if (options().quantifiers.cegqiBvLinearize && contains_pv[lhs]
         && contains_pv[rhs])
     {
-      Node result = utils::normalizePvEqual(pv, children, contains_pv);
+      Node result = d_util.normalizePvEqual(pv, children, contains_pv);
       if (!result.isNull())
       {
         Trace("cegqi-bv-nl")
@@ -584,11 +583,11 @@ Node BvInstantiator::rewriteTermForSolvePv(
       Node result;
       if (n.getKind() == BITVECTOR_MULT)
       {
-        result = utils::normalizePvMult(pv, children, contains_pv);
+        result = d_util.normalizePvMult(pv, children, contains_pv);
       }
       else
       {
-        result = utils::normalizePvPlus(pv, children, contains_pv);
+        result = d_util.normalizePvPlus(pv, children, contains_pv);
       }
       if (!result.isNull())
       {

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index fda9aa57c8df63ce463d7b9158fe9da44a8a943e..be990899a4d33ec9264aa3884a57875e4115ba77 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -19,7 +19,9 @@
 #define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
 
 #include <unordered_map>
+
 #include "theory/quantifiers/bv_inverter.h"
+#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 
 namespace cvc5::internal {
@@ -104,6 +106,8 @@ class BvInstantiator : public Instantiator
  private:
   /** pointer to the bv inverter class */
   BvInverter* d_inverter;
+  /** Utility class */
+  BvInstantiatorUtil d_util;
   //--------------------------------solved forms
   /** identifier counter, used to allocate ids to each solve form */
   unsigned d_inst_id_counter;

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index 4e4ee317ac11af5b4b58ae9b67ed4d953b6e7fd4..4f68c44d3edd043c8c3339e405ba5a6155242240 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -23,9 +23,10 @@ using namespace cvc5::internal::kind;
 namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
-namespace utils {
 
-Node getPvCoeff(TNode pv, TNode n)
+BvInstantiatorUtil::BvInstantiatorUtil(Env& env) : EnvObj(env) {}
+
+Node BvInstantiatorUtil::getPvCoeff(TNode pv, TNode n) const
 {
   bool neg = false;
   Node coeff;
@@ -59,9 +60,10 @@ Node getPvCoeff(TNode pv, TNode n)
   return coeff;
 }
 
-Node normalizePvMult(TNode pv,
-                     const std::vector<Node>& children,
-                     std::unordered_map<Node, bool>& contains_pv)
+Node BvInstantiatorUtil::normalizePvMult(
+    TNode pv,
+    const std::vector<Node>& children,
+    std::unordered_map<Node, bool>& contains_pv) const
 {
   bool neg, neg_coeff = false;
   bool found_pv = false;
@@ -111,7 +113,7 @@ Node normalizePvMult(TNode pv,
   {
     coeff = nm->mkNode(BITVECTOR_NEG, coeff);
   }
-  coeff = Rewriter::rewrite(coeff);
+  coeff = rewrite(coeff);
   unsigned size_coeff = bv::utils::getSize(coeff);
   Node zero = bv::utils::mkZero(size_coeff);
   if (coeff == zero)
@@ -136,11 +138,8 @@ Node normalizePvMult(TNode pv,
   return result;
 }
 
-#ifdef CVC5_ASSERTIONS
-namespace {
-bool isLinearPlus(TNode n,
-                  TNode pv,
-                  std::unordered_map<Node, bool>& contains_pv)
+bool BvInstantiatorUtil::isLinearPlus(
+    TNode n, TNode pv, std::unordered_map<Node, bool>& contains_pv) const
 {
   Node coeff;
   Assert(n.getAttribute(BvLinearAttribute()));
@@ -153,17 +152,16 @@ bool isLinearPlus(TNode n,
     Assert(!contains_pv[n[0][1]]);
   }
   Assert(!contains_pv[n[1]]);
-  coeff = utils::getPvCoeff(pv, n[0]);
+  coeff = getPvCoeff(pv, n[0]);
   Assert(!coeff.isNull());
   Assert(!contains_pv[coeff]);
   return true;
 }
-}  // namespace
-#endif
 
-Node normalizePvPlus(Node pv,
-                     const std::vector<Node>& children,
-                     std::unordered_map<Node, bool>& contains_pv)
+Node BvInstantiatorUtil::normalizePvPlus(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<Node, bool>& contains_pv) const
 {
   NodeManager* nm;
   NodeBuilder nb_c(BITVECTOR_ADD);
@@ -190,7 +188,7 @@ Node normalizePvPlus(Node pv,
     if (nc == pv
         || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
     {
-      Node coeff = utils::getPvCoeff(pv, nc);
+      Node coeff = getPvCoeff(pv, nc);
       Assert(!coeff.isNull());
       if (neg)
       {
@@ -202,7 +200,7 @@ Node normalizePvPlus(Node pv,
     else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear))
     {
       Assert(isLinearPlus(nc, pv, contains_pv));
-      Node coeff = utils::getPvCoeff(pv, nc[0]);
+      Node coeff = getPvCoeff(pv, nc[0]);
       Assert(!coeff.isNull());
       Node leaf = nc[1];
       if (neg)
@@ -223,15 +221,14 @@ Node normalizePvPlus(Node pv,
   if (nb_c.getNumChildren() > 0)
   {
     Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
-    coeffs = Rewriter::rewrite(coeffs);
-    result = pv_mult_coeffs =
-        utils::normalizePvMult(pv, {pv, coeffs}, contains_pv);
+    coeffs = rewrite(coeffs);
+    result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv);
   }
 
   if (nb_l.getNumChildren() > 0)
   {
     Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
-    leafs = Rewriter::rewrite(leafs);
+    leafs = rewrite(leafs);
     Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
     /* pv * 0 + t --> t */
     if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
@@ -249,9 +246,10 @@ Node normalizePvPlus(Node pv,
   return result;
 }
 
-Node normalizePvEqual(Node pv,
-                      const std::vector<Node>& children,
-                      std::unordered_map<Node, bool>& contains_pv)
+Node BvInstantiatorUtil::normalizePvEqual(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<Node, bool>& contains_pv) const
 {
   Assert(children.size() == 2);
 
@@ -275,13 +273,13 @@ Node normalizePvEqual(Node pv,
       if (child.getKind() == BITVECTOR_ADD)
       {
         Assert(isLinearPlus(child, pv, contains_pv));
-        coeffs[i] = utils::getPvCoeff(pv, child[0]);
+        coeffs[i] = getPvCoeff(pv, child[0]);
         leafs[i] = child[1];
       }
       else
       {
         Assert(child.getKind() == BITVECTOR_MULT || child == pv);
-        coeffs[i] = utils::getPvCoeff(pv, child);
+        coeffs[i] = getPvCoeff(pv, child);
       }
     }
     if (neg)
@@ -303,9 +301,9 @@ Node normalizePvEqual(Node pv,
   }
 
   Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
-  coeff = Rewriter::rewrite(coeff);
+  coeff = rewrite(coeff);
   std::vector<Node> mult_children = {pv, coeff};
-  Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv);
+  Node lhs = normalizePvMult(pv, mult_children, contains_pv);
 
   Node rhs;
   if (!leafs[0].isNull() && !leafs[1].isNull())
@@ -324,7 +322,7 @@ Node normalizePvEqual(Node pv,
   {
     rhs = bv::utils::mkZero(bv::utils::getSize(pv));
   }
-  rhs = Rewriter::rewrite(rhs);
+  rhs = rewrite(rhs);
 
   if (lhs == rhs)
   {
@@ -336,7 +334,6 @@ Node normalizePvEqual(Node pv,
   return result;
 }
 
-}  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5::internal

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 40a25ce877e97d286b4b3576af05f324a030b466..d17fee50d3cdc89e54e5be420f9a46f34177a52b 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -20,6 +20,7 @@
 
 #include "expr/attribute.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -30,76 +31,84 @@ struct BvLinearAttributeId
 };
 using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>;
 
-namespace utils {
+class BvInstantiatorUtil : protected EnvObj
+{
+ public:
+  BvInstantiatorUtil(Env& env);
+  /**
+   * Determine coefficient of pv in term n, where n has the form pv, -pv, pv *
+   * t, or -pv * t. Extracting the coefficient of multiplications only succeeds
+   * if the multiplication are normalized with normalizePvMult.
+   *
+   * If sucessful it returns
+   *   1    if n ==  pv,
+   *  -1    if n == -pv,
+   *   t    if n ==  pv * t,
+   *  -t    if n == -pv * t.
+   * If n is not a linear term, a null node is returned.
+   */
+  Node getPvCoeff(TNode pv, TNode n) const;
 
-/**
- * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t,
- * or -pv * t. Extracting the coefficient of multiplications only succeeds if
- * the multiplication are normalized with normalizePvMult.
- *
- * If sucessful it returns
- *   1    if n ==  pv,
- *  -1    if n == -pv,
- *   t    if n ==  pv * t,
- *  -t    if n == -pv * t.
- * If n is not a linear term, a null node is returned.
- */
-Node getPvCoeff(TNode pv, TNode n);
+  /**
+   * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks
+   * terms in which pv occurs.
+   * For example,
+   *
+   *  a * -pv * b * c
+   *
+   * is rewritten to
+   *
+   *  pv * -(a * b * c)
+   *
+   * Returns the normalized node if the resulting term is linear w.r.t. pv and
+   * a null node otherwise. If pv does not occur in children it returns a
+   * multiplication over children.
+   */
+  Node normalizePvMult(TNode pv,
+                       const std::vector<Node>& children,
+                       std::unordered_map<Node, bool>& contains_pv) const;
 
-/**
- * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks
- * terms in which pv occurs.
- * For example,
- *
- *  a * -pv * b * c
- *
- * is rewritten to
- *
- *  pv * -(a * b * c)
- *
- * Returns the normalized node if the resulting term is linear w.r.t. pv and
- * a null node otherwise. If pv does not occur in children it returns a
- * multiplication over children.
- */
-Node normalizePvMult(TNode pv,
-                     const std::vector<Node>& children,
-                     std::unordered_map<Node, bool>& contains_pv);
+  /**
+   * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks
+   * terms in which pv occurs.
+   * For example,
+   *
+   *  a * pv + b + c * -pv
+   *
+   * is rewritten to
+   *
+   *  pv * (a - c) + b
+   *
+   * Returns the normalized node if the resulting term is linear w.r.t. pv and
+   * a null node otherwise. If pv does not occur in children it returns an
+   * addition over children.
+   */
+  Node normalizePvPlus(Node pv,
+                       const std::vector<Node>& children,
+                       std::unordered_map<Node, bool>& contains_pv) const;
 
-/**
- * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks
- * terms in which pv occurs.
- * For example,
- *
- *  a * pv + b + c * -pv
- *
- * is rewritten to
- *
- *  pv * (a - c) + b
- *
- * Returns the normalized node if the resulting term is linear w.r.t. pv and
- * a null node otherwise. If pv does not occur in children it returns an
- * addition over children.
- */
-Node normalizePvPlus(Node pv,
-                     const std::vector<Node>& children,
-                     std::unordered_map<Node, bool>& contains_pv);
+  /**
+   * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
+   * marks terms in which pv occurs.
+   * For example, equality
+   *
+   *   -pv * a + b = c + pv
+   *
+   * rewrites to
+   *
+   *   pv * (-a - 1) = c - b.
+   */
+  Node normalizePvEqual(Node pv,
+                        const std::vector<Node>& children,
+                        std::unordered_map<Node, bool>& contains_pv) const;
 
-/**
- * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
- * marks terms in which pv occurs.
- * For example, equality
- *
- *   -pv * a + b = c + pv
- *
- * rewrites to
- *
- *   pv * (-a - 1) = c - b.
- */
-Node normalizePvEqual(Node pv,
-                      const std::vector<Node>& children,
-                      std::unordered_map<Node, bool>& contains_pv);
+ private:
+  /** Checks whether n is a linear plus */
+  bool isLinearPlus(TNode n,
+                    TNode pv,
+                    std::unordered_map<Node, bool>& contains_pv) const;
+};
 
-}  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5::internal

diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
index 92f21d31cf16bacd8b07b2661d5d5f38bc700a31..f61de869d51710f565200cef3ee2be9e5571f16f 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
@@ -29,7 +29,6 @@ using namespace theory;
 using namespace theory::bv;
 using namespace theory::bv::utils;
 using namespace theory::quantifiers;
-using namespace theory::quantifiers::utils;
 
 namespace test {
 
@@ -60,7 +59,7 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt
 };
 
 /**
- * getPvCoeff(x, n) should return
+ * util.getPvCoeff(x, n) should return
  *
  *  1           if n == x
  * -1           if n == -x
@@ -72,38 +71,45 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt
  */
 TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, getPvCoeff)
 {
+  Env& env = d_slvEngine->getEnv();
+  BvInstantiatorUtil util(env);
+
   Node x = mkVar(32);
   Node a = mkVar(32);
   Node one = mkOne(32);
   BvLinearAttribute is_linear;
 
   /* x -> 1 */
-  Node coeff_x = getPvCoeff(x, x);
+  Node coeff_x = util.getPvCoeff(x, x);
   ASSERT_EQ(coeff_x, one);
 
   /* -x -> -1 */
-  Node coeff_neg_x = getPvCoeff(x, mkNeg(x));
+  Node coeff_neg_x = util.getPvCoeff(x, mkNeg(x));
   ASSERT_EQ(coeff_neg_x, mkNeg(one));
 
   /* x * a -> null (since x * a not a normalized) */
   Node x_mult_a = mkMult(x, a);
-  Node coeff_x_mult_a = getPvCoeff(x, x_mult_a);
+  Node coeff_x_mult_a = util.getPvCoeff(x, x_mult_a);
   ASSERT_TRUE(coeff_x_mult_a.isNull());
 
   /* x * a -> a */
   x_mult_a.setAttribute(is_linear, true);
-  coeff_x_mult_a = getPvCoeff(x, x_mult_a);
+  coeff_x_mult_a = util.getPvCoeff(x, x_mult_a);
   ASSERT_EQ(coeff_x_mult_a, a);
 
   /* x * -a -> -a */
   Node x_mult_neg_a = mkMult(x, mkNeg(a));
   x_mult_neg_a.setAttribute(is_linear, true);
-  Node coeff_x_mult_neg_a = getPvCoeff(x, x_mult_neg_a);
+  Node coeff_x_mult_neg_a = util.getPvCoeff(x, x_mult_neg_a);
   ASSERT_EQ(coeff_x_mult_neg_a, mkNeg(a));
 }
 
 TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
 {
+  Env& env = d_slvEngine->getEnv();
+  BvInstantiatorUtil util(env);
+  Rewriter* rr = env.getRewriter();
+
   Node x = mkVar(32);
   Node neg_x = mkNeg(x);
   Node a = mkVar(32);
@@ -119,15 +125,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
   contains_x[neg_x] = true;
 
   /* x * -x -> null (since non linear) */
-  Node norm_xx = normalizePvMult(x, {x, neg_x}, contains_x);
+  Node norm_xx = util.normalizePvMult(x, {x, neg_x}, contains_x);
   ASSERT_TRUE(norm_xx.isNull());
 
   /* nothing to normalize -> create a * a */
-  Node norm_aa = normalizePvMult(x, {a, a}, contains_x);
-  ASSERT_EQ(norm_aa, Rewriter::rewrite(mkMult(a, a)));
+  Node norm_aa = util.normalizePvMult(x, {a, a}, contains_x);
+  ASSERT_EQ(norm_aa, rr->rewrite(mkMult(a, a)));
 
   /* normalize x * a -> x * a */
-  Node norm_xa = normalizePvMult(x, {x, a}, contains_x);
+  Node norm_xa = util.normalizePvMult(x, {x, a}, contains_x);
   ASSERT_TRUE(contains_x[norm_xa]);
   ASSERT_TRUE(norm_xa.getAttribute(is_linear));
   ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_MULT);
@@ -136,7 +142,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
   ASSERT_EQ(norm_xa[1], a);
 
   /* normalize a * x -> x * a */
-  Node norm_ax = normalizePvMult(x, {a, x}, contains_x);
+  Node norm_ax = util.normalizePvMult(x, {a, x}, contains_x);
   ASSERT_TRUE(contains_x[norm_ax]);
   ASSERT_TRUE(norm_ax.getAttribute(is_linear));
   ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_MULT);
@@ -145,7 +151,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
   ASSERT_EQ(norm_ax[1], a);
 
   /* normalize a * -x -> x * -a */
-  Node norm_neg_ax = normalizePvMult(x, {a, neg_x}, contains_x);
+  Node norm_neg_ax = util.normalizePvMult(x, {a, neg_x}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_ax]);
   ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_MULT);
@@ -154,55 +160,59 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
   ASSERT_EQ(norm_neg_ax[1], mkNeg(a));
 
   /* normalize 0 * x -> 0 */
-  Node norm_zx = normalizePvMult(x, {zero, x}, contains_x);
+  Node norm_zx = util.normalizePvMult(x, {zero, x}, contains_x);
   ASSERT_EQ(norm_zx, zero);
 
   /* normalize 1 * x -> x */
-  Node norm_ox = normalizePvMult(x, {one, x}, contains_x);
+  Node norm_ox = util.normalizePvMult(x, {one, x}, contains_x);
   ASSERT_EQ(norm_ox, x);
 
   /* normalize a * b * c * x * d -> x * (a * b * c * d) */
-  Node norm_abcxd = normalizePvMult(x, {a, b, c, x, d}, contains_x);
+  Node norm_abcxd = util.normalizePvMult(x, {a, b, c, x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_abcxd]);
   ASSERT_TRUE(norm_abcxd.getAttribute(is_linear));
   ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_abcxd.getNumChildren(), 2);
   ASSERT_EQ(norm_abcxd[0], x);
-  ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkMult({a, b, c, d})));
+  ASSERT_EQ(norm_abcxd[1], rr->rewrite(mkMult({a, b, c, d})));
 
   /* normalize a * b * c * -x * d -> x * -(a * b * c * d) */
-  Node norm_neg_abcxd = normalizePvMult(x, {a, b, c, neg_x, d}, contains_x);
+  Node norm_neg_abcxd =
+      util.normalizePvMult(x, {a, b, c, neg_x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_abcxd]);
   ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2);
   ASSERT_EQ(norm_neg_abcxd[0], x);
-  ASSERT_TRUE(norm_neg_abcxd[1]
-              == mkNeg(Rewriter::rewrite(mkMult({a, b, c, d}))));
+  ASSERT_TRUE(norm_neg_abcxd[1] == mkNeg(rr->rewrite(mkMult({a, b, c, d}))));
 
   /* normalize b * (x * a) -> x * (b * a) */
-  Node norm_bxa = normalizePvMult(x, {b, norm_ax}, contains_x);
+  Node norm_bxa = util.normalizePvMult(x, {b, norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_bxa]);
   ASSERT_TRUE(norm_bxa.getAttribute(is_linear));
   ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_bxa.getNumChildren(), 2);
   ASSERT_EQ(norm_bxa[0], x);
-  ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkMult(b, a)));
+  ASSERT_EQ(norm_bxa[1], rr->rewrite(mkMult(b, a)));
 
   /* normalize b * -(x * a) -> x * -(a * b) */
   Node neg_norm_ax = mkNeg(norm_ax);
   contains_x[neg_norm_ax] = true;
-  Node norm_neg_bxa = normalizePvMult(x, {b, neg_norm_ax}, contains_x);
+  Node norm_neg_bxa = util.normalizePvMult(x, {b, neg_norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_bxa]);
   ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2);
   ASSERT_EQ(norm_neg_bxa[0], x);
-  ASSERT_EQ(norm_neg_bxa[1], mkNeg(Rewriter::rewrite(mkMult(b, a))));
+  ASSERT_EQ(norm_neg_bxa[1], mkNeg(rr->rewrite(mkMult(b, a))));
 }
 
 TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
 {
+  Env& env = d_slvEngine->getEnv();
+  BvInstantiatorUtil util(env);
+  Rewriter* rr = env.getRewriter();
+
   Node one = mkOne(32);
   Node x = mkVar(32);
   Node neg_x = mkNeg(x);
@@ -219,15 +229,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   /* a + b * x -> null (since b * x not normalized) */
   Node mult_bx = mkMult(b, x);
   contains_x[mult_bx] = true;
-  Node norm_abx = normalizePvPlus(x, {a, mult_bx}, contains_x);
+  Node norm_abx = util.normalizePvPlus(x, {a, mult_bx}, contains_x);
   ASSERT_TRUE(norm_abx.isNull());
 
   /* nothing to normalize -> create a + a */
-  Node norm_aa = normalizePvPlus(x, {a, a}, contains_x);
-  ASSERT_EQ(norm_aa, Rewriter::rewrite(mkPlus(a, a)));
+  Node norm_aa = util.normalizePvPlus(x, {a, a}, contains_x);
+  ASSERT_EQ(norm_aa, rr->rewrite(mkPlus(a, a)));
 
   /* x + a -> x + a */
-  Node norm_xa = normalizePvPlus(x, {x, a}, contains_x);
+  Node norm_xa = util.normalizePvPlus(x, {x, a}, contains_x);
   ASSERT_TRUE(contains_x[norm_xa]);
   ASSERT_TRUE(norm_xa.getAttribute(is_linear));
   ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_ADD);
@@ -236,7 +246,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   ASSERT_EQ(norm_xa[1], a);
 
   /* a * x -> x * a */
-  Node norm_ax = normalizePvPlus(x, {a, x}, contains_x);
+  Node norm_ax = util.normalizePvPlus(x, {a, x}, contains_x);
   ASSERT_TRUE(contains_x[norm_ax]);
   ASSERT_TRUE(norm_ax.getAttribute(is_linear));
   ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_ADD);
@@ -245,7 +255,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   ASSERT_EQ(norm_ax[1], a);
 
   /* a + -x -> (x * -1) + a */
-  Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x);
+  Node norm_neg_ax = util.normalizePvPlus(x, {a, neg_x}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_ax]);
   ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_ADD);
@@ -255,30 +265,33 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   ASSERT_TRUE(norm_neg_ax[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_neg_ax[0]]);
   ASSERT_EQ(norm_neg_ax[0][0], x);
-  ASSERT_EQ(norm_neg_ax[0][1], Rewriter::rewrite(mkNeg(one)));
+  ASSERT_EQ(norm_neg_ax[0][1], rr->rewrite(mkNeg(one)));
   ASSERT_EQ(norm_neg_ax[1], a);
 
   /* -x + -a * x -> x * (-1 - a) */
-  Node norm_xax = normalizePvPlus(
-      x, {mkNeg(x), normalizePvMult(x, {mkNeg(a), x}, contains_x)}, contains_x);
+  Node norm_xax = util.normalizePvPlus(
+      x,
+      {mkNeg(x), util.normalizePvMult(x, {mkNeg(a), x}, contains_x)},
+      contains_x);
   ASSERT_TRUE(contains_x[norm_xax]);
   ASSERT_TRUE(norm_xax.getAttribute(is_linear));
   ASSERT_EQ(norm_xax.getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_xax.getNumChildren(), 2);
   ASSERT_EQ(norm_xax[0], x);
-  ASSERT_EQ(norm_xax[1], Rewriter::rewrite(mkPlus(mkNeg(one), mkNeg(a))));
+  ASSERT_EQ(norm_xax[1], rr->rewrite(mkPlus(mkNeg(one), mkNeg(a))));
 
   /* a + b + c + x + d -> x + (a + b + c + d) */
-  Node norm_abcxd = normalizePvPlus(x, {a, b, c, x, d}, contains_x);
+  Node norm_abcxd = util.normalizePvPlus(x, {a, b, c, x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_abcxd]);
   ASSERT_TRUE(norm_abcxd.getAttribute(is_linear));
   ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_abcxd.getNumChildren(), 2);
   ASSERT_EQ(norm_abcxd[0], x);
-  ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d})));
+  ASSERT_EQ(norm_abcxd[1], rr->rewrite(mkPlus({a, b, c, d})));
 
   /* a + b + c + -x + d -> (x * -1) + (a + b + c + d) */
-  Node norm_neg_abcxd = normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x);
+  Node norm_neg_abcxd =
+      util.normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_abcxd]);
   ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_ADD);
@@ -288,22 +301,22 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]);
   ASSERT_EQ(norm_neg_abcxd[0][0], x);
-  ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one)));
-  ASSERT_EQ(norm_neg_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d})));
+  ASSERT_EQ(norm_neg_abcxd[0][1], rr->rewrite(mkNeg(one)));
+  ASSERT_EQ(norm_neg_abcxd[1], rr->rewrite(mkPlus({a, b, c, d})));
 
   /* b + (x + a) -> x + (b + a) */
-  Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x);
+  Node norm_bxa = util.normalizePvPlus(x, {b, norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_bxa]);
   ASSERT_TRUE(norm_bxa.getAttribute(is_linear));
   ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_ADD);
   ASSERT_EQ(norm_bxa.getNumChildren(), 2);
   ASSERT_EQ(norm_bxa[0], x);
-  ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkPlus(b, a)));
+  ASSERT_EQ(norm_bxa[1], rr->rewrite(mkPlus(b, a)));
 
   /* b + -(x + a) -> (x * -1) + b - a */
   Node neg_norm_ax = mkNeg(norm_ax);
   contains_x[neg_norm_ax] = true;
-  Node norm_neg_bxa = normalizePvPlus(x, {b, neg_norm_ax}, contains_x);
+  Node norm_neg_bxa = util.normalizePvPlus(x, {b, neg_norm_ax}, contains_x);
   ASSERT_TRUE(contains_x[norm_neg_bxa]);
   ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear));
   ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_ADD);
@@ -313,17 +326,21 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]);
   ASSERT_EQ(norm_neg_abcxd[0][0], x);
-  ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one)));
-  ASSERT_EQ(norm_neg_bxa[1], Rewriter::rewrite((mkPlus(b, mkNeg(a)))));
+  ASSERT_EQ(norm_neg_abcxd[0][1], rr->rewrite(mkNeg(one)));
+  ASSERT_EQ(norm_neg_bxa[1], rr->rewrite((mkPlus(b, mkNeg(a)))));
 
   /* -x + x + a -> a */
-  Node norm_neg_xxa = normalizePvPlus(x, {neg_x, x, a}, contains_x);
+  Node norm_neg_xxa = util.normalizePvPlus(x, {neg_x, x, a}, contains_x);
   ASSERT_FALSE(contains_x[norm_neg_xxa]);
   ASSERT_EQ(norm_neg_xxa, a);
 }
 
 TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
 {
+  Env& env = d_slvEngine->getEnv();
+  BvInstantiatorUtil util(env);
+  Rewriter* rr = env.getRewriter();
+
   Node x = mkVar(32);
   Node neg_x = mkNeg(x);
   Node a = mkVar(32);
@@ -340,74 +357,75 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
   contains_x[neg_x] = true;
 
   /* x = a -> null (nothing to normalize) */
-  Node norm_xa = normalizePvEqual(x, {x, a}, contains_x);
+  Node norm_xa = util.normalizePvEqual(x, {x, a}, contains_x);
   ASSERT_TRUE(norm_xa.isNull());
 
   /* x = x -> true */
-  Node norm_xx = normalizePvEqual(x, {x, x}, contains_x);
+  Node norm_xx = util.normalizePvEqual(x, {x, x}, contains_x);
   ASSERT_EQ(norm_xx, ntrue);
 
   /* x = -x -> x * 2 = 0 */
-  Node norm_neg_xx = normalizePvEqual(x, {x, neg_x}, contains_x);
+  Node norm_neg_xx = util.normalizePvEqual(x, {x, neg_x}, contains_x);
   ASSERT_EQ(norm_neg_xx.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_neg_xx[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_xx[0].getNumChildren(), 2);
   ASSERT_TRUE(norm_neg_xx[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_neg_xx[0]]);
   ASSERT_EQ(norm_neg_xx[0][0], x);
-  ASSERT_EQ(norm_neg_xx[0][1], Rewriter::rewrite(mkConst(32, 2)));
+  ASSERT_EQ(norm_neg_xx[0][1], rr->rewrite(mkConst(32, 2)));
   ASSERT_EQ(norm_neg_xx[1], zero);
 
   /* a + x = x -> 0 = -a */
-  Node norm_axx = normalizePvEqual(
-      x, {normalizePvPlus(x, {a, x}, contains_x), x}, contains_x);
+  Node norm_axx = util.normalizePvEqual(
+      x, {util.normalizePvPlus(x, {a, x}, contains_x), x}, contains_x);
   ASSERT_EQ(norm_axx.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_axx[0], zero);
   ASSERT_EQ(norm_axx[1], mkNeg(a));
 
   /* a + -x = x -> x * -2 = a */
-  Node norm_neg_axx = normalizePvEqual(
-      x, {normalizePvPlus(x, {a, neg_x}, contains_x), x}, contains_x);
+  Node norm_neg_axx = util.normalizePvEqual(
+      x, {util.normalizePvPlus(x, {a, neg_x}, contains_x), x}, contains_x);
   ASSERT_EQ(norm_neg_axx.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_neg_axx[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_neg_axx[0].getNumChildren(), 2);
   ASSERT_TRUE(norm_neg_axx[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_neg_axx[0]]);
   ASSERT_EQ(norm_neg_axx[0][0], x);
-  ASSERT_EQ(norm_neg_axx[0][1], Rewriter::rewrite(mkNeg(mkConst(32, 2))));
+  ASSERT_EQ(norm_neg_axx[0][1], rr->rewrite(mkNeg(mkConst(32, 2))));
   ASSERT_EQ(norm_neg_axx[1], mkNeg(a));
 
   /* a * x = x -> x * (a - 1) = 0 */
-  Node norm_mult_axx = normalizePvEqual(
-      x, {normalizePvMult(x, {a, x}, contains_x), x}, contains_x);
+  Node norm_mult_axx = util.normalizePvEqual(
+      x, {util.normalizePvMult(x, {a, x}, contains_x), x}, contains_x);
   ASSERT_EQ(norm_mult_axx.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_mult_axx[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_mult_axx[0].getNumChildren(), 2);
   ASSERT_TRUE(norm_mult_axx[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_mult_axx[0]]);
   ASSERT_EQ(norm_mult_axx[0][0], x);
-  ASSERT_EQ(norm_mult_axx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one))));
+  ASSERT_EQ(norm_mult_axx[0][1], rr->rewrite(mkPlus(a, mkNeg(one))));
   ASSERT_EQ(norm_mult_axx[1], zero);
 
   /* a * x = x + b -> x * (a - 1) = b */
-  Node norm_axxb = normalizePvEqual(x,
-                                    {normalizePvMult(x, {a, x}, contains_x),
-                                     normalizePvPlus(x, {b, x}, contains_x)},
-                                    contains_x);
+  Node norm_axxb =
+      util.normalizePvEqual(x,
+                            {util.normalizePvMult(x, {a, x}, contains_x),
+                             util.normalizePvPlus(x, {b, x}, contains_x)},
+                            contains_x);
   ASSERT_EQ(norm_axxb.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_axxb[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_axxb[0].getNumChildren(), 2);
   ASSERT_TRUE(norm_axxb[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_axxb[0]]);
   ASSERT_EQ(norm_axxb[0][0], x);
-  ASSERT_EQ(norm_axxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one))));
+  ASSERT_EQ(norm_axxb[0][1], rr->rewrite(mkPlus(a, mkNeg(one))));
   ASSERT_EQ(norm_axxb[1], b);
 
   /* a * x + c = x -> x * (a - 1) = -c */
-  Node norm_axcx = normalizePvEqual(
+  Node norm_axcx = util.normalizePvEqual(
       x,
-      {normalizePvPlus(
-           x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x),
+      {util.normalizePvPlus(
+           x, {util.normalizePvMult(x, {a, x}, contains_x), c}, contains_x),
        x},
       contains_x);
   ASSERT_EQ(norm_axcx.getKind(), kind::EQUAL);
@@ -416,15 +434,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
   ASSERT_TRUE(norm_axcx[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_axcx[0]]);
   ASSERT_EQ(norm_axcx[0][0], x);
-  ASSERT_EQ(norm_axcx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one))));
+  ASSERT_EQ(norm_axcx[0][1], rr->rewrite(mkPlus(a, mkNeg(one))));
   ASSERT_EQ(norm_axcx[1], mkNeg(c));
 
   /* a * x + c = x + b -> x * (a - 1) = b - c*/
-  Node norm_axcxb = normalizePvEqual(
+  Node norm_axcxb = util.normalizePvEqual(
       x,
-      {normalizePvPlus(
-           x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x),
-       normalizePvPlus(x, {b, x}, contains_x)},
+      {util.normalizePvPlus(
+           x, {util.normalizePvMult(x, {a, x}, contains_x), c}, contains_x),
+       util.normalizePvPlus(x, {b, x}, contains_x)},
       contains_x);
   ASSERT_EQ(norm_axcxb.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_axcxb[0].getKind(), kind::BITVECTOR_MULT);
@@ -432,22 +450,22 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
   ASSERT_TRUE(norm_axcxb[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_axcxb[0]]);
   ASSERT_EQ(norm_axcxb[0][0], x);
-  ASSERT_EQ(norm_axcxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one))));
-  ASSERT_EQ(norm_axcxb[1], Rewriter::rewrite(mkPlus(b, mkNeg(c))));
+  ASSERT_EQ(norm_axcxb[0][1], rr->rewrite(mkPlus(a, mkNeg(one))));
+  ASSERT_EQ(norm_axcxb[1], rr->rewrite(mkPlus(b, mkNeg(c))));
 
   /* -(a + -x) = a * x -> x * (1 - a) = a */
-  Node norm_axax =
-      normalizePvEqual(x,
-                       {mkNeg(normalizePvPlus(x, {a, neg_x}, contains_x)),
-                        normalizePvMult(x, {a, x}, contains_x)},
-                       contains_x);
+  Node norm_axax = util.normalizePvEqual(
+      x,
+      {mkNeg(util.normalizePvPlus(x, {a, neg_x}, contains_x)),
+       util.normalizePvMult(x, {a, x}, contains_x)},
+      contains_x);
   ASSERT_EQ(norm_axax.getKind(), kind::EQUAL);
   ASSERT_EQ(norm_axax[0].getKind(), kind::BITVECTOR_MULT);
   ASSERT_EQ(norm_axax[0].getNumChildren(), 2);
   ASSERT_TRUE(norm_axax[0].getAttribute(is_linear));
   ASSERT_TRUE(contains_x[norm_axax[0]]);
   ASSERT_EQ(norm_axax[0][0], x);
-  ASSERT_EQ(norm_axax[0][1], Rewriter::rewrite(mkPlus(one, mkNeg(a))));
+  ASSERT_EQ(norm_axax[0][1], rr->rewrite(mkPlus(one, mkNeg(a))));
   ASSERT_EQ(norm_axax[1], a);
 }
 }  // namespace test