Fix BVGauss unit tests. (#3142)

pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.

This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index fccdfa2f936a13e50f6cbb2c6c49eda38e0a22ad..09d963ba38fb6f623e44d1fc86e862023321d802 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -37,47 +37,6 @@ namespace passes {
 
 namespace {
 
-/**
- *  Represents the result of Gaussian Elimination where the solution
- *  of the given equation system is
- *
- *   INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b,
- *               where ci, b and p are
- *                 - bit-vector constants
- *                 - extracts or zero extensions on bit-vector constants
- *                 - of arbitrary nesting level
- *               and p is co-prime to all bit-vector constants for which
- *               a multiplicative inverse has to be computed.
- *
- *   UNIQUE  ... determined for all unknowns, e.g., x = 4
- *
- *   PARTIAL ... e.g., x = 4 - 2z
- *
- *   NONE    ... no solution
- *
- *   Given a matrix A representing an equation system, the resulting
- *   matrix B after applying GE represents, e.g.:
- *
- *   B = 1 0 0 2 <-    UNIQUE
- *       0 1 0 3 <-
- *       0 0 1 1 <-
- *
- *   B = 1 0 2 4 <-    PARTIAL
- *       0 1 3 2 <-
- *       0 0 1 1
- *
- *   B = 1 0 0 1       NONE
- *       0 1 1 2
- *       0 0 0 2 <-
- */
-enum class Result
-{
-  INVALID,
-  UNIQUE,
-  PARTIAL,
-  NONE
-};
-
 bool is_bv_const(Node n)
 {
   if (n.isConst()) { return true; }
@@ -96,6 +55,8 @@ Integer get_bv_const_value(Node n)
   return get_bv_const(n).getConst<BitVector>().getValue();
 }
 
+}  // namespace
+
 /**
  * Determines if an overflow may occur in given 'expr'.
  *
@@ -112,7 +73,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 getMinBwExpr(Node expr)
+unsigned BVGauss::getMinBwExpr(Node expr)
 {
   std::vector<Node> visit;
   /* Maps visited nodes to the determined minimum bit-width required. */
@@ -280,10 +241,9 @@ unsigned getMinBwExpr(Node expr)
  * form) is stored in 'rhs' and 'lhs', i.e., the given matrix is overwritten
  * with the resulting matrix.
  */
-Result gaussElim(
-    Integer prime,
-    std::vector<Integer>& rhs,
-    std::vector<std::vector<Integer>>& lhs)
+BVGauss::Result BVGauss::gaussElim(Integer prime,
+                                   std::vector<Integer>& rhs,
+                                   std::vector<std::vector<Integer>>& lhs)
 {
   Assert(prime > 0);
   Assert(lhs.size());
@@ -296,7 +256,7 @@ Result gaussElim(
     rhs = std::vector<Integer>(rhs.size(), Integer(0));
     lhs = std::vector<std::vector<Integer>>(
         lhs.size(), std::vector<Integer>(lhs[0].size(), Integer(0)));
-    return Result::UNIQUE;
+    return BVGauss::Result::UNIQUE;
   }
 
   size_t nrows = lhs.size();
@@ -361,7 +321,7 @@ Result gaussElim(
           Integer inv = lhs[j][pcol].modInverse(prime);
           if (inv == -1)
           {
-            return Result::INVALID; /* not coprime */
+            return BVGauss::Result::INVALID; /* not coprime */
           }
           for (size_t k = pcol; k < ncols; ++k)
           {
@@ -409,7 +369,7 @@ Result gaussElim(
       if (rhs[i] != 0)
       {
         /* no solution */
-        return Result::NONE;
+        return BVGauss::Result::NONE;
       }
       continue;
     }
@@ -426,9 +386,12 @@ Result gaussElim(
     }
   }
 
-  if (ispart) { return Result::PARTIAL; }
+  if (ispart)
+  {
+    return BVGauss::Result::PARTIAL;
+  }
 
-  return Result::UNIQUE;
+  return BVGauss::Result::UNIQUE;
 }
 
 /**
@@ -452,7 +415,7 @@ Result gaussElim(
  * to result (modulo prime). These mapped results are added as constraints
  * of the form 'unknown = mapped result' in applyInternal.
  */
-Result gaussElimRewriteForUrem(
+BVGauss::Result BVGauss::gaussElimRewriteForUrem(
     const std::vector<Node>& equations,
     std::unordered_map<Node, Node, NodeHashFunction>& res)
 {
@@ -493,7 +456,7 @@ Result gaussElimRewriteForUrem(
           << "Minimum required bit-width exceeds given bit-width, "
              "will not apply Gaussian Elimination."
           << std::endl;
-      return Result::INVALID;
+      return BVGauss::Result::INVALID;
     }
     rhs.push_back(get_bv_const_value(eqrhs));
 
@@ -613,7 +576,7 @@ Result gaussElimRewriteForUrem(
 
   if (nrows < 1)
   {
-    return Result::INVALID;
+    return BVGauss::Result::INVALID;
   }
 
   for (size_t i = 0; i < nrows; ++i)
@@ -631,13 +594,13 @@ Result gaussElimRewriteForUrem(
 
   if (lhs.size() > lhs[0].size())
   {
-    return Result::INVALID;
+    return BVGauss::Result::INVALID;
   }
 
   Trace("bv-gauss-elim") << "Applying Gaussian Elimination..." << std::endl;
-  Result ret = gaussElim(iprime, rhs, lhs);
+  BVGauss::Result ret = gaussElim(iprime, rhs, lhs);
 
-  if (ret != Result::NONE && ret != Result::INVALID)
+  if (ret != BVGauss::Result::NONE && ret != BVGauss::Result::INVALID)
   {
     std::vector<Node> vvars;
     for (const auto& p : vars) { vvars.push_back(p.first); }
@@ -645,7 +608,7 @@ Result gaussElimRewriteForUrem(
     Assert(nrows == lhs.size());
     Assert(nrows == rhs.size());
     NodeManager *nm = NodeManager::currentNM();
-    if (ret == Result::UNIQUE)
+    if (ret == BVGauss::Result::UNIQUE)
     {
       for (size_t i = 0; i < nvars; ++i)
       {
@@ -655,7 +618,7 @@ Result gaussElimRewriteForUrem(
     }
     else
     {
-      Assert(ret == Result::PARTIAL);
+      Assert(ret == BVGauss::Result::PARTIAL);
 
       for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows;
            ++pcol, ++prow)
@@ -712,10 +675,6 @@ Result gaussElimRewriteForUrem(
   return ret;
 }
 
-}  // namespace
-
-
-
 BVGauss::BVGauss(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-gauss")
 {
@@ -772,20 +731,20 @@ PreprocessingPassResult BVGauss::applyInternal(
     if (eq.second.size() <= 1) { continue; }
 
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    Result ret = gaussElimRewriteForUrem(eq.second, res);
+    BVGauss::Result ret = gaussElimRewriteForUrem(eq.second, res);
     Trace("bv-gauss-elim") << "result: "
-                           << (ret == Result::INVALID
+                           << (ret == BVGauss::Result::INVALID
                                    ? "INVALID"
-                                   : (ret == Result::UNIQUE
+                                   : (ret == BVGauss::Result::UNIQUE
                                           ? "UNIQUE"
-                                          : (ret == Result::PARTIAL
+                                          : (ret == BVGauss::Result::PARTIAL
                                                  ? "PARTIAL"
                                                  : "NONE")))
                            << std::endl;
-    if (ret != Result::INVALID)
+    if (ret != BVGauss::Result::INVALID)
     {
       NodeManager *nm = NodeManager::currentNM();
-      if (ret == Result::NONE)
+      if (ret == BVGauss::Result::NONE)
       {
         atpp.clear();
         atpp.push_back(nm->mkConst<bool>(false));

diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 862777a9bc52cef39dc398c8d31bae1722ebdc97..93d61be9e51c2d318cae6e9087292bfbdf4c0c25 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -30,7 +30,7 @@ namespace passes {
 class BVGauss : public PreprocessingPass
 {
  public:
-   BVGauss(PreprocessingPassContext* preprocContext);
+  BVGauss(PreprocessingPassContext* preprocContext);
 
  protected:
   /**
@@ -42,8 +42,63 @@ class BVGauss : public PreprocessingPass
    * succeed modulo a prime number, which is not necessarily the case if a
    * given set of equations is modulo a non-prime number.
    */
-   PreprocessingPassResult applyInternal(
-       AssertionPipeline* assertionsToPreprocess) override;
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  /* Note: The following functionality is only exposed for unit testing in
+   * pass_bv_gauss_white.h. */
+
+  /**
+   *  Represents the result of Gaussian Elimination where the solution
+   *  of the given equation system is
+   *
+   *   INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b,
+   *               where ci, b and p are
+   *                 - bit-vector constants
+   *                 - extracts or zero extensions on bit-vector constants
+   *                 - of arbitrary nesting level
+   *               and p is co-prime to all bit-vector constants for which
+   *               a multiplicative inverse has to be computed.
+   *
+   *   UNIQUE  ... determined for all unknowns, e.g., x = 4
+   *
+   *   PARTIAL ... e.g., x = 4 - 2z
+   *
+   *   NONE    ... no solution
+   *
+   *   Given a matrix A representing an equation system, the resulting
+   *   matrix B after applying GE represents, e.g.:
+   *
+   *   B = 1 0 0 2 <-    UNIQUE
+   *       0 1 0 3 <-
+   *       0 0 1 1 <-
+   *
+   *   B = 1 0 2 4 <-    PARTIAL
+   *       0 1 3 2 <-
+   *       0 0 1 1
+   *
+   *   B = 1 0 0 1       NONE
+   *       0 1 1 2
+   *       0 0 0 2 <-
+   */
+  enum class Result
+  {
+    INVALID,
+    UNIQUE,
+    PARTIAL,
+    NONE
+  };
+
+  static 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, NodeHashFunction>& res);
+
+  static unsigned getMinBwExpr(Node expr);
 };
 
 }  // namespace passes

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index e027fb5e8f1689103601bad25f326441d7004f80..7f7af40b98e8e8116448b2a0ed4b280fabcbeadc 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -17,8 +17,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "preprocessing/passes/bv_gauss.cpp"
-#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/passes/bv_gauss.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -31,6 +30,7 @@
 
 using namespace CVC4;
 using namespace CVC4::preprocessing;
+using namespace CVC4::preprocessing::passes;
 using namespace CVC4::theory;
 using namespace CVC4::smt;
 
@@ -51,13 +51,13 @@ static void print_matrix_dbg(std::vector<Integer> &rhs,
 static void testGaussElimX(Integer prime,
                            std::vector<Integer> rhs,
                            std::vector<std::vector<Integer>> lhs,
-                           passes::Result expected,
-                           std::vector<Integer> *rrhs = nullptr,
-                           std::vector<std::vector<Integer>> *rlhs = nullptr)
+                           BVGauss::Result expected,
+                           std::vector<Integer>* rrhs = nullptr,
+                           std::vector<std::vector<Integer>>* rlhs = nullptr)
 {
   size_t nrows = lhs.size();
   size_t ncols = lhs[0].size();
-  passes::Result ret;
+  BVGauss::Result ret;
   std::vector<Integer> resrhs = std::vector<Integer>(rhs);
   std::vector<std::vector<Integer>> reslhs =
       std::vector<std::vector<Integer>>(lhs);
@@ -65,21 +65,21 @@ static void testGaussElimX(Integer prime,
   std::cout << "Input: " << std::endl;
   print_matrix_dbg(rhs, lhs);
 
-  ret = passes::gaussElim(prime, resrhs, reslhs);
+  ret = BVGauss::gaussElim(prime, resrhs, reslhs);
 
-  std::cout << "passes::Result: "
-            << (ret == passes::Result::INVALID
+  std::cout << "BVGauss::Result: "
+            << (ret == BVGauss::Result::INVALID
                     ? "INVALID"
-                    : (ret == passes::Result::UNIQUE
+                    : (ret == BVGauss::Result::UNIQUE
                            ? "UNIQUE"
-                           : (ret == passes::Result::PARTIAL ? "PARTIAL"
-                                                                  : "NONE")))
+                           : (ret == BVGauss::Result::PARTIAL ? "PARTIAL"
+                                                              : "NONE")))
             << std::endl;
   print_matrix_dbg(resrhs, reslhs);
 
   TS_ASSERT_EQUALS(expected, ret);
 
-  if (expected == passes::Result::UNIQUE)
+  if (expected == BVGauss::Result::UNIQUE)
   {
     /* map result value to column index
      * e.g.:
@@ -121,7 +121,7 @@ static void testGaussElimT(Integer prime,
                            std::vector<Integer> rhs,
                            std::vector<std::vector<Integer>> lhs)
 {
-  TS_ASSERT_THROWS(passes::gaussElim(prime, rhs, lhs), T);
+  TS_ASSERT_THROWS(BVGauss::gaussElim(prime, rhs, lhs), T);
 }
 
 class TheoryBVGaussWhite : public CxxTest::TestSuite
@@ -321,27 +321,27 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     std::cout << "matrix 0, modulo 0" << std::endl;  // throws
     testGaussElimT<AssertionException>(Integer(0), rhs, lhs);
     std::cout << "matrix 0, modulo 1" << std::endl;
-    testGaussElimX(Integer(1), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 2" << std::endl;
-    testGaussElimX(Integer(2), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(2), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 3" << std::endl;
-    testGaussElimX(Integer(3), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(3), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 4" << std::endl;  // no inverse
-    testGaussElimX(Integer(4), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(4), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 5" << std::endl;
-    testGaussElimX(Integer(5), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(5), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 6" << std::endl;  // no inverse
-    testGaussElimX(Integer(6), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(6), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 8" << std::endl;  // no inverse
-    testGaussElimX(Integer(8), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(8), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 10" << std::endl;  // no inverse
-    testGaussElimX(Integer(10), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(10), rhs, lhs, BVGauss::Result::INVALID);
     std::cout << "matrix 0, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueDone()
@@ -361,7 +361,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(1), Integer(0)},
            {Integer(0), Integer(0), Integer(1)}};
     std::cout << "matrix 1, modulo 17" << std::endl;
-    testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUnique()
@@ -381,11 +381,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(3), Integer(1), Integer(-2)}};
     std::cout << "matrix 2, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 2, modulo 17" << std::endl;
-    testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 2, modulo 59" << std::endl;
-    testGaussElimX(Integer(59), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *      lhs       rhs         lhs     rhs   modulo 11
@@ -401,7 +401,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(-1), Integer(-1), Integer(-2)},
            {Integer(2), Integer(-1), Integer(2), Integer(-1)}};
     std::cout << "matrix 3, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero1()
@@ -421,7 +421,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(1), Integer(1)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 4, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -435,7 +435,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(4), Integer(5)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 5, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -449,7 +449,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(3), Integer(2), Integer(5)},
            {Integer(0), Integer(4), Integer(5)}};
     std::cout << "matrix 6, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero2()
@@ -469,7 +469,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(1), Integer(1), Integer(1)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 7, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -483,7 +483,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(5)},
            {Integer(3), Integer(2), Integer(5)}};
     std::cout << "matrix 8, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 11
@@ -497,7 +497,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(3), Integer(2), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 9, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero3()
@@ -517,7 +517,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(6)}};
     std::cout << "matrix 10, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 7
@@ -531,7 +531,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(6), Integer(0)}};
     std::cout << "matrix 11, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimUniqueZero4()
@@ -551,7 +551,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 12, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -565,7 +565,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 13, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -579,7 +579,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 14, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -593,7 +593,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 15, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -607,7 +607,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 16, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -621,7 +621,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 17, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -635,7 +635,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 18, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -649,7 +649,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(0), Integer(0), Integer(0)}};
     std::cout << "matrix 18, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -663,7 +663,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 19, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs  modulo 2
@@ -682,7 +682,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(2), rhs, lhs, passes::Result::UNIQUE, &resrhs, &reslhs);
+        Integer(2), rhs, lhs, BVGauss::Result::UNIQUE, &resrhs, &reslhs);
   }
 
   void testGaussElimUniquePartial()
@@ -700,7 +700,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(2), Integer(0), Integer(6)},
            {Integer(4), Integer(0), Integer(6)}};
     std::cout << "matrix 21, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs   modulo 7
@@ -712,7 +712,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(2), Integer(6), Integer(0)},
            {Integer(4), Integer(6), Integer(0)}};
     std::cout << "matrix 22, modulo 7" << std::endl;
-    testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE);
+    testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
   }
 
   void testGaussElimNone()
@@ -732,7 +732,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(3), Integer(1), Integer(-2)}};
     std::cout << "matrix 23, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs       modulo 59
@@ -746,7 +746,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(4), Integer(12)},
            {Integer(1), Integer(-4), Integer(-12)}};
     std::cout << "matrix 24, modulo 59" << std::endl;
-    testGaussElimX(Integer(59), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs       modulo 9
@@ -760,7 +760,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(4), Integer(5), Integer(6)},
            {Integer(2), Integer(7), Integer(12)}};
     std::cout << "matrix 25, modulo 9" << std::endl;
-    testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID);
+    testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
   }
 
   void testGaussElimNoneZero()
@@ -780,7 +780,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(3), Integer(5)},
            {Integer(0), Integer(0), Integer(5)}};
     std::cout << "matrix 26, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -794,7 +794,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(0), Integer(5)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 27, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs  modulo 11
@@ -808,7 +808,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(0)},
            {Integer(4), Integer(0), Integer(0)}};
     std::cout << "matrix 28, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
   }
 
   void testGaussElimPartial1()
@@ -826,7 +826,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(0), Integer(9)},
            {Integer(0), Integer(1), Integer(3)}};
     std::cout << "matrix 29, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -838,7 +838,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(3), Integer(0)},
            {Integer(0), Integer(0), Integer(1)}};
     std::cout << "matrix 30, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -850,7 +850,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     lhs = {{Integer(1), Integer(1), Integer(1)},
            {Integer(2), Integer(3), Integer(5)}};
     std::cout << "matrix 31, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs  modulo { 3, 5, 7, 11, 17, 31, 59 }
@@ -869,38 +869,38 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     resrhs = {Integer(1), Integer(4), Integer(0)};
     std::cout << "matrix 32, modulo 5" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(4)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(5), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(5), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 7" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(6)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(7), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(7), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 11" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(10)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(11), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(11), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 17" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(16)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(17), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(17), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
     std::cout << "matrix 32, modulo 59" << std::endl;
     reslhs = {{Integer(1), Integer(0), Integer(58)},
               {Integer(0), Integer(1), Integer(2)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(59), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(59), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
 
     /* -------------------------------------------------------------------
      *     lhs    rhs        lhs   rhs   modulo 3
@@ -919,7 +919,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
               {Integer(0), Integer(0), Integer(0)},
               {Integer(0), Integer(0), Integer(0)}};
     testGaussElimX(
-        Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs);
+        Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
   }
 
   void testGaussElimPartial2()
@@ -940,7 +940,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(0), Integer(0), Integer(2), Integer(2)},
            {Integer(0), Integer(0), Integer(1), Integer(0)}};
     std::cout << "matrix 34, modulo 11" << std::endl;
-    testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL);
+    testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
   }
   void testGaussElimRewriteForUremUnique1()
   {
@@ -984,8 +984,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
     TS_ASSERT(res[d_x] == d_three32);
     TS_ASSERT(res[d_y] == d_four32);
@@ -1083,8 +1083,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
     TS_ASSERT(res[d_x] == d_three32);
     TS_ASSERT(res[d_y] == d_four32);
@@ -1094,7 +1094,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial1()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1120,8 +1120,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1212,7 +1212,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial1a()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1236,8 +1236,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1328,7 +1328,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial2()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1351,8 +1351,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
                      d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1414,7 +1414,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial3()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1445,8 +1445,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_eight);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1535,7 +1535,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial4()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *     lhs    rhs          lhs    rhs  modulo 11
@@ -1579,8 +1579,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_thirty);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     Node x1 = d_nm->mkNode(
@@ -1677,7 +1677,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial5()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *     lhs    rhs         lhs   rhs  modulo 3
@@ -1721,8 +1721,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_thirty);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 1);
 
     Node x1 = d_nm->mkNode(kind::BITVECTOR_UREM,
@@ -1784,7 +1784,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremPartial6()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *    lhs    rhs  -->    lhs    rhs  modulo 11
@@ -1828,8 +1828,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_two);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 3);
 
     Node x1 = d_nm->mkNode(
@@ -1872,7 +1872,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremWithExprPartial()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -1919,8 +1919,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     x = Rewriter::rewrite(x);
@@ -2015,7 +2015,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNAryPartial()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      *   lhs   rhs        lhs   rhs  modulo 11
@@ -2082,8 +2082,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
                             d_nine);
 
     std::vector<Node> eqs = {eq1, eq2};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::PARTIAL);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::PARTIAL);
     TS_ASSERT(res.size() == 2);
 
     x_mul_xx = Rewriter::rewrite(x_mul_xx);
@@ -2178,7 +2178,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNotInvalid1()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * 3x / 2z = 4  modulo 11
@@ -2208,8 +2208,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n3, d_p), d_five);
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
 
     TS_ASSERT(res[n1] == d_four32);
@@ -2220,7 +2220,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremNotInvalid2()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * x*y = 4  modulo 11
@@ -2267,8 +2267,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         bv::utils::mkConcat(d_zero, d_nine));
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::UNIQUE);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::UNIQUE);
     TS_ASSERT(res.size() == 3);
 
     n1 = Rewriter::rewrite(n1);
@@ -2289,7 +2289,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   void testGaussElimRewriteForUremInvalid()
   {
     std::unordered_map<Node, Node, NodeHashFunction> res;
-    passes::Result ret;
+    BVGauss::Result ret;
 
     /* -------------------------------------------------------------------
      * x*y = 4  modulo 11
@@ -2332,8 +2332,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         bv::utils::mkConcat(d_zero, d_nine));
 
     std::vector<Node> eqs = {eq1, eq2, eq3};
-    ret = passes::gaussElimRewriteForUrem(eqs, res);
-    TS_ASSERT(ret == passes::Result::INVALID);
+    ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
+    TS_ASSERT(ret == BVGauss::Result::INVALID);
   }
 
   void testGaussElimRewriteUnique1()
@@ -2590,15 +2590,15 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
   void testGetMinBw1()
   {
-    TS_ASSERT(passes::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4);
 
-    TS_ASSERT(passes::getMinBwExpr(d_p) == 4);
-    TS_ASSERT(passes::getMinBwExpr(d_x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(d_p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(d_x) == 16);
 
     Node extp = bv::utils::mkExtract(d_p, 4, 0);
-    TS_ASSERT(passes::getMinBwExpr(extp) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(extp) == 4);
     Node extx = bv::utils::mkExtract(d_x, 4, 0);
-    TS_ASSERT(passes::getMinBwExpr(extx) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(extx) == 5);
 
     Node zextop8 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
     Node zextop16 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(16));
@@ -2606,132 +2606,132 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node zextop40 = d_nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
 
     Node zext40p = d_nm->mkNode(zextop8, d_p);
-    TS_ASSERT(passes::getMinBwExpr(zext40p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext40p) == 4);
     Node zext40x = d_nm->mkNode(zextop8, d_x);
-    TS_ASSERT(passes::getMinBwExpr(zext40x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext40x) == 16);
 
     Node zext48p = d_nm->mkNode(zextop16, d_p);
-    TS_ASSERT(passes::getMinBwExpr(zext48p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48p) == 4);
     Node zext48x = d_nm->mkNode(zextop16, d_x);
-    TS_ASSERT(passes::getMinBwExpr(zext48x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48x) == 16);
 
     Node p8 = d_nm->mkConst<BitVector>(BitVector(8, 11u));
     Node x8 = d_nm->mkVar("x8", d_nm->mkBitVectorType(8));
 
     Node zext48p8 = d_nm->mkNode(zextop40, p8);
-    TS_ASSERT(passes::getMinBwExpr(zext48p8) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48p8) == 4);
     Node zext48x8 = d_nm->mkNode(zextop40, x8);
-    TS_ASSERT(passes::getMinBwExpr(zext48x8) == 8);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext48x8) == 8);
 
     Node mult1p = d_nm->mkNode(kind::BITVECTOR_MULT, extp, extp);
-    TS_ASSERT(passes::getMinBwExpr(mult1p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult1p) == 5);
     Node mult1x = d_nm->mkNode(kind::BITVECTOR_MULT, extx, extx);
-    TS_ASSERT(passes::getMinBwExpr(mult1x) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult1x) == 0);
 
     Node mult2p = d_nm->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(mult2p) == 7);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult2p) == 7);
     Node mult2x = d_nm->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(mult2x) == 32);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult2x) == 32);
 
     NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT);
     nbmult3p << zext48p << zext48p << zext48p;
     Node mult3p = nbmult3p;
-    TS_ASSERT(passes::getMinBwExpr(mult3p) == 11);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult3p) == 11);
     NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT);
     nbmult3x << zext48x << zext48x << zext48x;
     Node mult3x = nbmult3x;
-    TS_ASSERT(passes::getMinBwExpr(mult3x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult3x) == 48);
 
     NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT);
     nbmult4p << zext48p  << zext48p8 << zext48p;
     Node mult4p = nbmult4p;
-    TS_ASSERT(passes::getMinBwExpr(mult4p) == 11);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult4p) == 11);
     NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT);
     nbmult4x << zext48x  << zext48x8 << zext48x;
     Node mult4x = nbmult4x;
-    TS_ASSERT(passes::getMinBwExpr(mult4x) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(mult4x) == 40);
 
     Node concat1p = bv::utils::mkConcat(d_p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(concat1p) == 52);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat1p) == 52);
     Node concat1x = bv::utils::mkConcat(d_x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(concat1x) == 64);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat1x) == 64);
 
     Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p);
-    TS_ASSERT(passes::getMinBwExpr(concat2p) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat2p) == 4);
     Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
-    TS_ASSERT(passes::getMinBwExpr(concat2x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(concat2x) == 16);
 
     Node udiv1p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(udiv1p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv1p) == 1);
     Node udiv1x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(udiv1x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv1x) == 48);
 
     Node udiv2p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8);
-    TS_ASSERT(passes::getMinBwExpr(udiv2p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv2p) == 1);
     Node udiv2x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8);
-    TS_ASSERT(passes::getMinBwExpr(udiv2x) == 48);
+    TS_ASSERT(BVGauss::getMinBwExpr(udiv2x) == 48);
 
     Node urem1p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(urem1p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem1p) == 1);
     Node urem1x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(urem1x) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem1x) == 1);
 
     Node urem2p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8);
-    TS_ASSERT(passes::getMinBwExpr(urem2p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem2p) == 1);
     Node urem2x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8);
-    TS_ASSERT(passes::getMinBwExpr(urem2x) == 16);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem2x) == 16);
 
     Node urem3p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(urem3p) == 1);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem3p) == 1);
     Node urem3x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(urem3x) == 8);
+    TS_ASSERT(BVGauss::getMinBwExpr(urem3x) == 8);
 
     Node add1p = d_nm->mkNode(kind::BITVECTOR_PLUS, extp, extp);
-    TS_ASSERT(passes::getMinBwExpr(add1p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add1p) == 5);
     Node add1x = d_nm->mkNode(kind::BITVECTOR_PLUS, extx, extx);
-    TS_ASSERT(passes::getMinBwExpr(add1x) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(add1x) == 0);
 
     Node add2p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(add2p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add2p) == 5);
     Node add2x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(add2x) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(add2x) == 17);
 
     Node add3p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p);
-    TS_ASSERT(passes::getMinBwExpr(add3p) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(add3p) == 5);
     Node add3x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x);
-    TS_ASSERT(passes::getMinBwExpr(add3x) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(add3x) == 17);
 
     NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS);
     nbadd4p << zext48p << zext48p << zext48p;
     Node add4p = nbadd4p;
-    TS_ASSERT(passes::getMinBwExpr(add4p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add4p) == 6);
     NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS);
     nbadd4x << zext48x << zext48x << zext48x;
     Node add4x = nbadd4x;
-    TS_ASSERT(passes::getMinBwExpr(add4x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add4x) == 18);
 
     NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS);
     nbadd5p << zext48p << zext48p8 << zext48p;
     Node add5p = nbadd5p;
-    TS_ASSERT(passes::getMinBwExpr(add5p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add5p) == 6);
     NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS);
     nbadd5x << zext48x << zext48x8 << zext48x;
     Node add5x = nbadd5x;
-    TS_ASSERT(passes::getMinBwExpr(add5x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add5x) == 18);
 
     NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS);
     nbadd6p << zext48p << zext48p << zext48p << zext48p;
     Node add6p = nbadd6p;
-    TS_ASSERT(passes::getMinBwExpr(add6p) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(add6p) == 6);
     NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS);
     nbadd6x << zext48x << zext48x << zext48x << zext48x;
     Node add6x = nbadd6x;
-    TS_ASSERT(passes::getMinBwExpr(add6x) == 18);
+    TS_ASSERT(BVGauss::getMinBwExpr(add6x) == 18);
 
     Node not1p = d_nm->mkNode(kind::BITVECTOR_NOT, zext40p);
-    TS_ASSERT(passes::getMinBwExpr(not1p) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(not1p) == 40);
     Node not1x = d_nm->mkNode(kind::BITVECTOR_NOT, zext40x);
-    TS_ASSERT(passes::getMinBwExpr(not1x) == 40);
+    TS_ASSERT(BVGauss::getMinBwExpr(not1x) == 40);
   }
 
   void testGetMinBw2()
@@ -2743,7 +2743,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node zext1 = d_nm->mkNode(zextop15, d_p);
     Node ext = bv::utils::mkExtract(zext1, 7, 0);
     Node zext2 = d_nm->mkNode(zextop5, ext);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 4);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 4);
   }
 
   void testGetMinBw3a()
@@ -2761,7 +2761,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node ext2 = bv::utils::mkExtract(z, 4, 0);
     Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
     Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 5);
   }
 
   void testGetMinBw3b()
@@ -2776,7 +2776,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
     Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
     Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
-    TS_ASSERT(passes::getMinBwExpr(zext2) == 5);
+    TS_ASSERT(BVGauss::getMinBwExpr(zext2) == 5);
   }
 
   void testGetMinBw4a()
@@ -2809,7 +2809,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
 
-    TS_ASSERT(passes::getMinBwExpr(plus) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus) == 6);
   }
 
   void testGetMinBw4b()
@@ -2839,7 +2839,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
 
-    TS_ASSERT(passes::getMinBwExpr(plus) == 6);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus) == 6);
   }
 
   void testGetMinBw5a()
@@ -2935,7 +2935,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         plus6,
         d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
 
-    TS_ASSERT(passes::getMinBwExpr(plus7) == 0);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus7) == 0);
   }
 
   void testGetMinBw5b()
@@ -3030,8 +3030,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
         plus6,
         d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
 
-    TS_ASSERT(passes::getMinBwExpr(plus7) == 19);
-    TS_ASSERT(passes::getMinBwExpr(Rewriter::rewrite(plus7)) == 17);
+    TS_ASSERT(BVGauss::getMinBwExpr(plus7) == 19);
+    TS_ASSERT(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)) == 17);
   }
 
 };