summaryrefslogtreecommitdiff
path: root/test/unit/preprocessing/pass_bv_gauss_white.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/preprocessing/pass_bv_gauss_white.h')
-rw-r--r--test/unit/preprocessing/pass_bv_gauss_white.h324
1 files changed, 162 insertions, 162 deletions
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);
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback