diff options
-rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 97 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_gauss.h | 61 | ||||
-rw-r--r-- | test/unit/preprocessing/pass_bv_gauss_white.h | 324 |
3 files changed, 248 insertions, 234 deletions
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index fccdfa2f9..09d963ba3 100644 --- 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 862777a9b..93d61be9e 100644 --- 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 e027fb5e8..7f7af40b9 100644 --- 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); } }; |