mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

compile

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-02 08:40:44 -08:00
parent 4c4f916917
commit 57d3abbf64
1 changed files with 49 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

95
src/test/polysat.cpp
View file

@ -1120,7 +1120,7 @@ namespace polysat {
s.check(); s.check();
} }
} }
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later) // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
// static void test_mixed_vars() { // static void test_mixed_vars() {
@ -1136,7 +1136,7 @@ namespace polysat {
}; // class test_polysat }; // class test_polysat
// Here we deal with linear constraints of the form // Here we deal with linear constraints of the form
// //
// a1*x + b1 <= a2*x + b2 (mod m = 2^bw) // a1*x + b1 <= a2*x + b2 (mod m = 2^bw)
@ -1144,7 +1144,7 @@ namespace polysat {
// and their negation. // and their negation.
class test_fi { class test_fi {
static bool is_violated(rational const& a1, rational const& b1, rational const& a2, rational const& b2, static bool is_violated(rational const& a1, rational const& b1, rational const& a2, rational const& b2,
rational const& val, bool negated, rational const& m) { rational const& val, bool negated, rational const& m) {
rational const lhs = (a1*val + b1) % m; rational const lhs = (a1*val + b1) % m;
@ -1197,52 +1197,55 @@ namespace polysat {
return true; return true;
} }
public: public:
static void exhaustive(unsigned bw = 0) { static void exhaustive(unsigned bw = 0) {
if (bw == 0) { if (bw == 0) {
exhaustive(1); exhaustive(1);
exhaustive(2); exhaustive(2);
exhaustive(3); exhaustive(3);
exhaustive(4); exhaustive(4);
exhaustive(5); exhaustive(5);
} else { }
std::cout << "test_fi::exhaustive for bw=" << bw << std::endl; else {
rational const m = rational::power_of_two(bw); std::cout << "test_fi::exhaustive for bw=" << bw << std::endl;
for (rational p(1); p < m; ++p) { rational const m = rational::power_of_two(bw);
for (rational r(1); r < m; ++r) { for (rational p(1); p < m; ++p) {
// TODO: remove this condition to test the cases other than disequal_lin! (also start p,q from 0) for (rational r(1); r < m; ++r) {
if (p == r) // TODO: remove this condition to test the cases other than disequal_lin! (also start p,q from 0)
continue; if (p == r)
for (rational q(0); q < m; ++q) continue;
for (rational s(0); s < m; ++s) for (rational q(0); q < m; ++q)
for (rational v(0); v < m; ++v) for (rational s(0); s < m; ++s)
for (bool negated : {true, false}) for (rational v(0); v < m; ++v)
check_one(p, q, r, s, v, negated, bw); for (bool negated : {true, false})
check_one(p, q, r, s, v, negated, bw);
}
} }
} }
} }
static void randomized(unsigned num_rounds = 100'000, unsigned bw = 16) { static void randomized(unsigned num_rounds = 100000, unsigned bw = 16) {
std::cout << "test_fi::randomized for bw=" << bw << " (" << num_rounds << " rounds)" << std::endl; std::cout << "test_fi::randomized for bw=" << bw << " (" << num_rounds << " rounds)" << std::endl;
rational const m = rational::power_of_two(bw); rational const m = rational::power_of_two(bw);
VERIFY(bw <= 32 && "random_gen generates 32-bit numbers"); VERIFY(bw <= 32 && "random_gen generates 32-bit numbers");
random_gen rng; random_gen rng;
unsigned round = num_rounds; unsigned round = num_rounds;
while (round) { while (round) {
// rational a1 = (rational(rng()) % (m - 1)) + 1; // rational a1 = (rational(rng()) % (m - 1)) + 1;
// rational a2 = (rational(rng()) % (m - 1)) + 1; // rational a2 = (rational(rng()) % (m - 1)) + 1;
rational a1 = rational(rng()) % m; rational a1 = rational(rng()) % m;
rational a2 = rational(rng()) % m; rational a2 = rational(rng()) % m;
if (a1.is_zero() || a2.is_zero() || a1 == a2) if (a1.is_zero() || a2.is_zero() || a1 == a2)
continue; continue;
rational b1 = rational(rng()) % m; rational b1 = rational(rng()) % m;
rational b2 = rational(rng()) % m; rational b2 = rational(rng()) % m;
rational val = rational(rng()) % m; rational val = rational(rng()) % m;
bool useful = bool useful =
check_one(a1, b1, a2, b2, val, true, bw) check_one(a1, b1, a2, b2, val, true, bw)
|| check_one(a1, b1, a2, b2, val, false, bw); || check_one(a1, b1, a2, b2, val, false, bw);
if (useful) if (useful)
round--; round--;
}
} }
}; // class test_fi }; // class test_fi