mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
Update viable tests
This commit is contained in:
Jakob Rath
parent
c954e82503
commit
b23c1b4016
2 changed files with 212 additions and 163 deletions
|
|
@ -1910,122 +1910,6 @@ namespace polysat {
|
|||
|
||||
}; // class test_polysat
|
||||
|
||||
|
||||
// Here we deal with linear constraints of the form
|
||||
//
|
||||
// a1*x + b1 <= a2*x + b2 (mod m = 2^bw)
|
||||
//
|
||||
// and their negation.
|
||||
|
||||
class test_fi {
|
||||
|
||||
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 lhs = (a1*val + b1) % m;
|
||||
rational const rhs = (a2*val + b2) % m;
|
||||
if (negated)
|
||||
return lhs <= rhs;
|
||||
else
|
||||
return lhs > rhs;
|
||||
}
|
||||
|
||||
// Returns true if the input is valid and the test did useful work
|
||||
static bool check_one(rational const& a1, rational const& b1, rational const& a2, rational const& b2, rational const& val, bool negated, unsigned bw) {
|
||||
rational const m = rational::power_of_two(bw);
|
||||
if (a1.is_zero() && a2.is_zero())
|
||||
return false;
|
||||
if (!is_violated(a1, b1, a2, b2, val, negated, m))
|
||||
return false;
|
||||
|
||||
scoped_solver s(__func__);
|
||||
auto x = s.var(s.add_var(bw));
|
||||
signed_constraint c = s.ule(a1*x + b1, a2*x + b2);
|
||||
if (negated)
|
||||
c.negate();
|
||||
viable& v = s.m_viable;
|
||||
v.intersect(x.var(), c);
|
||||
// Trigger forbidden interval refinement
|
||||
v.is_viable(x.var(), val);
|
||||
auto* e = v.m_units[x.var()];
|
||||
if (!e) {
|
||||
std::cout << "test_fi: no interval for a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " neg=" << negated << std::endl;
|
||||
// VERIFY(false);
|
||||
return false;
|
||||
}
|
||||
VERIFY(e);
|
||||
auto* first = e;
|
||||
SASSERT(e->next() == e); // the result is expected to be a single interval (although for this check it doesn't really matter if there's more...)
|
||||
do {
|
||||
rational const& lo = e->interval.lo_val();
|
||||
rational const& hi = e->interval.hi_val();
|
||||
for (rational x = lo; x != hi; x = (x + 1) % m) {
|
||||
// LOG("lo=" << lo << " hi=" << hi << " x=" << x);
|
||||
if (!is_violated(a1, b1, a2, b2, val, negated, m)) {
|
||||
std::cout << "test_fi: unsound for a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " neg=" << negated << std::endl;
|
||||
VERIFY(false);
|
||||
}
|
||||
}
|
||||
// TODO: now try to extend lo/hi one by one to find out how "bad" our interval really is.
|
||||
// (probably slow so maybe add a flag to enable/disable that.)
|
||||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
return true;
|
||||
}
|
||||
|
||||
public:
|
||||
static void exhaustive(unsigned bw = 0) {
|
||||
if (bw == 0) {
|
||||
exhaustive(1);
|
||||
exhaustive(2);
|
||||
exhaustive(3);
|
||||
exhaustive(4);
|
||||
exhaustive(5);
|
||||
}
|
||||
else {
|
||||
std::cout << "test_fi::exhaustive for bw=" << bw << std::endl;
|
||||
rational const m = rational::power_of_two(bw);
|
||||
for (rational p(1); p < m; ++p) {
|
||||
for (rational r(1); r < m; ++r) {
|
||||
// TODO: remove this condition to test the cases other than disequal_lin! (also start p,q from 0)
|
||||
if (p == r)
|
||||
continue;
|
||||
for (rational q(0); q < m; ++q)
|
||||
for (rational s(0); s < m; ++s)
|
||||
for (rational v(0); v < m; ++v)
|
||||
for (bool negated : {true, false})
|
||||
check_one(p, q, r, s, v, negated, bw);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static void randomized(unsigned num_rounds = 100000, unsigned bw = 16) {
|
||||
std::cout << "test_fi::randomized for bw=" << bw << " (" << num_rounds << " rounds)" << std::endl;
|
||||
rational const m = rational::power_of_two(bw);
|
||||
VERIFY(bw <= 32 && "random_gen generates 32-bit numbers");
|
||||
random_gen rng;
|
||||
unsigned round = num_rounds;
|
||||
while (round) {
|
||||
// rational a1 = (rational(rng()) % (m - 1)) + 1;
|
||||
// rational a2 = (rational(rng()) % (m - 1)) + 1;
|
||||
rational a1 = rational(rng()) % m;
|
||||
rational a2 = rational(rng()) % m;
|
||||
if (a1.is_zero() || a2.is_zero() || a1 == a2)
|
||||
continue;
|
||||
rational b1 = rational(rng()) % m;
|
||||
rational b2 = rational(rng()) % m;
|
||||
rational val = rational(rng()) % m;
|
||||
bool useful =
|
||||
check_one(a1, b1, a2, b2, val, true, bw)
|
||||
|| check_one(a1, b1, a2, b2, val, false, bw);
|
||||
if (useful)
|
||||
round--;
|
||||
}
|
||||
}
|
||||
|
||||
}; // class test_fi
|
||||
|
||||
} // namespace polysat
|
||||
|
||||
|
||||
|
|
@ -2154,9 +2038,6 @@ void tst_polysat() {
|
|||
RUN(test_polysat::test_ineq_non_axiom1());
|
||||
RUN(test_polysat::test_ineq_non_axiom4());
|
||||
|
||||
// test_fi::exhaustive();
|
||||
// test_fi::randomized();
|
||||
|
||||
if (collect_test_records)
|
||||
test_records.display(std::cout);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,64 +5,80 @@
|
|||
|
||||
namespace polysat {
|
||||
|
||||
class big_random_gen {
|
||||
unsigned m_bit_width;
|
||||
random_gen m_rng32_int;
|
||||
rational m_two_to_32 = rational::power_of_two(32);
|
||||
rational m_mod_value;
|
||||
|
||||
// create 32-bit random number
|
||||
unsigned rng32_unsigned() {
|
||||
return static_cast<unsigned>(m_rng32_int());
|
||||
}
|
||||
|
||||
public:
|
||||
big_random_gen(unsigned bit_width):
|
||||
m_bit_width(bit_width),
|
||||
m_mod_value(rational::power_of_two(bit_width)) {}
|
||||
|
||||
rational operator()() {
|
||||
rational x(rng32_unsigned());
|
||||
unsigned bw = m_bit_width;
|
||||
while (bw > 32) {
|
||||
x = x * m_two_to_32 + rng32_unsigned();
|
||||
bw -= 32;
|
||||
}
|
||||
return mod(x, m_mod_value);
|
||||
}
|
||||
};
|
||||
|
||||
struct solver_scopev {
|
||||
reslimit lim;
|
||||
};
|
||||
|
||||
class scoped_solverv : public solver_scopev, public solver {
|
||||
public:
|
||||
viable v;
|
||||
scoped_solverv(): solver(lim), v(*this) {}
|
||||
~scoped_solverv() {
|
||||
for (unsigned i = m_trail.size(); i-- > 0;) {
|
||||
switch (m_trail[i]) {
|
||||
case trail_instr_t::viable_add_i:
|
||||
v.pop_viable();
|
||||
break;
|
||||
case trail_instr_t::viable_rem_i:
|
||||
v.push_viable();
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
scoped_solverv(): solver(lim) {}
|
||||
viable& v() { return m_viable; }
|
||||
};
|
||||
|
||||
static void test1() {
|
||||
scoped_solverv s;
|
||||
auto xv = s.add_var(3);
|
||||
auto x = s.var(xv);
|
||||
s.v.push_var(3);
|
||||
viable& v = s.v();
|
||||
rational val;
|
||||
auto c = s.ule(x + 3, x + 5);
|
||||
s.v.intersect(xv, c);
|
||||
std::cout << s.v << "\n";
|
||||
std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.v.intersect(xv, s.ule(x, 2));
|
||||
std::cout << s.v << "\n";
|
||||
s.v.intersect(xv, s.ule(1, x));
|
||||
std::cout << s.v << "\n";
|
||||
std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.v.intersect(xv, s.ule(x, 3));
|
||||
std::cout << s.v << "\n";
|
||||
std::cout << s.v.find_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.v.intersect(xv, s.ule(3, x));
|
||||
std::cout << s.v << "\n";
|
||||
std::cout << s.v.find_viable(xv, val) << " " << val << "\n";
|
||||
s.add_ule(x + 3, x + 5);
|
||||
VERIFY_EQ(s.check_sat(), l_true);
|
||||
std::cout << v << "\n";
|
||||
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.add_ule(x, 2);
|
||||
VERIFY_EQ(s.check_sat(), l_true);
|
||||
std::cout << v << "\n";
|
||||
s.add_ule(1, x);
|
||||
VERIFY_EQ(s.check_sat(), l_true);
|
||||
std::cout << v << "\n";
|
||||
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.add_ule(x, 3);
|
||||
VERIFY_EQ(s.check_sat(), l_true);
|
||||
std::cout << v << "\n";
|
||||
std::cout << v.find_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
|
||||
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
|
||||
s.add_ule(3, x);
|
||||
VERIFY_EQ(s.check_sat(), l_false);
|
||||
std::cout << v << "\n";
|
||||
}
|
||||
|
||||
static void add_interval(scoped_solverv& s, pvar xv, pdd x, unsigned lo, unsigned len) {
|
||||
if (lo == 0)
|
||||
s.v.intersect(xv, s.ule(x, len - 1));
|
||||
s.v().intersect(xv, s.ule(x, len - 1));
|
||||
else if (lo + len == 8)
|
||||
s.v.intersect(xv, s.ule(lo, x));
|
||||
else
|
||||
s.v.intersect(xv, ~s.ule(x - ((lo + len)%8), x - lo));
|
||||
s.v().intersect(xv, s.ule(lo, x));
|
||||
else
|
||||
s.v().intersect(xv, ~s.ule(x - ((lo + len)%8), x - lo));
|
||||
}
|
||||
|
||||
static bool member(unsigned i, unsigned lo, unsigned len) {
|
||||
|
|
@ -80,7 +96,7 @@ namespace polysat {
|
|||
static void validate_intervals(scoped_solverv& s, pvar xv, vector<std::pair<unsigned, unsigned>> const& intervals) {
|
||||
for (unsigned i = 0; i < 8; ++i) {
|
||||
bool mem1 = member(i, intervals);
|
||||
bool mem2 = s.v.is_viable(xv, rational(i));
|
||||
bool mem2 = s.v().is_viable(xv, rational(i));
|
||||
if (mem1 != mem2)
|
||||
std::cout << "test violation: " << i << " member of all intervals " << mem1 << " viable: " << mem2 << "\n";
|
||||
VERIFY_EQ(mem1, mem2);
|
||||
|
|
@ -91,11 +107,10 @@ namespace polysat {
|
|||
scoped_solverv s;
|
||||
auto xv = s.add_var(3);
|
||||
auto x = s.var(xv);
|
||||
s.v.push_var(3);
|
||||
for (auto const& [lo, len] : intervals)
|
||||
add_interval(s, xv, x, lo, len);
|
||||
std::cout << intervals << "\n";
|
||||
//std::cout << s.v << "\n";
|
||||
//std::cout << s.v() << "\n";
|
||||
validate_intervals(s, xv, intervals);
|
||||
}
|
||||
|
||||
|
|
@ -290,13 +305,166 @@ namespace polysat {
|
|||
VERIFY(solver->check() == l_false);
|
||||
}
|
||||
|
||||
|
||||
class test_fi {
|
||||
|
||||
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 lhs = mod(a1*val + b1, M);
|
||||
rational const rhs = mod(a2*val + b2, M);
|
||||
if (negated)
|
||||
return lhs <= rhs;
|
||||
else
|
||||
return lhs > rhs;
|
||||
}
|
||||
|
||||
public:
|
||||
static bool check_one(unsigned a1, unsigned b1, unsigned a2, unsigned b2, unsigned val, unsigned bw) {
|
||||
return check_one(rational(a1), rational(b1), rational(a2), rational(b2), rational(val), bw);
|
||||
}
|
||||
|
||||
// Returns true if the input is valid and the test did useful work
|
||||
static bool check_one(rational const& a1, rational const& b1, rational const& a2, rational const& b2, rational const& val, unsigned bw) {
|
||||
// std::cout << "a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " bw=" << bw << "\n";
|
||||
rational const M = rational::power_of_two(bw);
|
||||
if (a1.is_zero() && a2.is_zero())
|
||||
return false;
|
||||
bool negated = false;
|
||||
if (!is_violated(a1, b1, a2, b2, val, negated, M))
|
||||
negated = !negated;
|
||||
SASSERT(is_violated(a1, b1, a2, b2, val, negated, M));
|
||||
|
||||
scoped_solverv s;
|
||||
auto x = s.var(s.add_var(bw));
|
||||
signed_constraint c = s.ule(a1*x + b1, a2*x + b2);
|
||||
if (negated)
|
||||
c.negate();
|
||||
if (c.is_always_true() || c.is_always_false())
|
||||
return false;
|
||||
bool expect_optimality =
|
||||
// refine-equal-lin should now find the optimal interval in all cases
|
||||
a1.is_zero() || a2.is_zero() || a1 == a2;
|
||||
SASSERT_EQ(c.vars().size(), 1);
|
||||
viable& v = s.v();
|
||||
v.intersect(x.var(), c);
|
||||
// Trigger forbidden interval refinement
|
||||
v.is_viable(x.var(), val);
|
||||
auto* e = v.m_units[x.var()];
|
||||
if (!e) {
|
||||
std::cout << "test_fi: no interval for a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " neg=" << negated << std::endl;
|
||||
VERIFY(false);
|
||||
return false;
|
||||
}
|
||||
VERIFY(e);
|
||||
auto* first = e;
|
||||
SASSERT(e->next() == e); // the result is expected to be a single interval (although for this check it doesn't really matter if there's more...)
|
||||
|
||||
auto check_is_violated = [&](rational const& x, bool expect_violated) -> bool {
|
||||
if (is_violated(a1, b1, a2, b2, x, negated, M) == expect_violated)
|
||||
return true;
|
||||
std::cout << "ERROR: a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " negated=" << negated << " bw=" << bw << "\n";
|
||||
return false;
|
||||
};
|
||||
|
||||
do {
|
||||
rational const& lo = e->interval.is_full() ? rational::zero() : e->interval.lo_val();
|
||||
rational const& hi = e->interval.is_full() ? M : e->interval.hi_val();
|
||||
rational const& len = e->interval.is_full() ? M : e->interval.current_len();
|
||||
unsigned max_offset = 1000;
|
||||
unsigned check_offset = len.is_unsigned() ? std::min(max_offset, len.get_unsigned() / 2) : max_offset;
|
||||
for (unsigned i = 0; i <= check_offset; ++i) {
|
||||
for (rational x : { lo + i, hi - (i + 1), val - i, val + i }) {
|
||||
x = mod(x, M);
|
||||
if (!e->interval.currently_contains(x))
|
||||
continue;
|
||||
VERIFY(check_is_violated(x, true));
|
||||
}
|
||||
}
|
||||
if (M > max_offset) {
|
||||
big_random_gen rng(bw);
|
||||
for (unsigned i = 0; i < 1000; ++i) {
|
||||
rational const x = mod(lo + mod(rng(), len), M);
|
||||
VERIFY(e->interval.currently_contains(x));
|
||||
VERIFY(check_is_violated(x, true));
|
||||
}
|
||||
}
|
||||
if (expect_optimality && !e->interval.is_full()) {
|
||||
VERIFY(check_is_violated(lo - 1, false));
|
||||
VERIFY(check_is_violated(hi, false));
|
||||
}
|
||||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
return true;
|
||||
}
|
||||
|
||||
public:
|
||||
static void exhaustive() {
|
||||
exhaustive(1);
|
||||
exhaustive(2);
|
||||
exhaustive(3);
|
||||
exhaustive(4);
|
||||
exhaustive(5);
|
||||
}
|
||||
|
||||
static void exhaustive(unsigned bw) {
|
||||
std::cout << "test_fi::exhaustive for bw=" << bw << std::endl;
|
||||
rational const m = rational::power_of_two(bw);
|
||||
for (rational p; p < m; ++p)
|
||||
for (rational r; r < m; ++r)
|
||||
for (rational q; q < m; ++q)
|
||||
for (rational s; s < m; ++s)
|
||||
for (rational v; v < m; ++v)
|
||||
check_one(p, q, r, s, v, bw);
|
||||
}
|
||||
|
||||
static void randomized(unsigned num_rounds, unsigned bw) {
|
||||
std::cout << "test_fi::randomized for bw=" << bw << " (" << num_rounds << " rounds)" << std::endl;
|
||||
big_random_gen rng(bw);
|
||||
unsigned round = num_rounds;
|
||||
while (round) {
|
||||
std::cout << "round " << round << "\n";
|
||||
rational a1 = rng();
|
||||
rational a2 = rng();
|
||||
rational b1 = rng();
|
||||
rational b2 = rng();
|
||||
rational val = rng();
|
||||
bool useful = check_one(a1, b1, a2, b2, val, bw);
|
||||
if (!a1.is_zero() && !a2.is_zero() && a1 != a2) {
|
||||
// make sure to trigger refine-equal-lin as well
|
||||
useful |= check_one(a1, b1, a1, b2, val, bw);
|
||||
useful |= check_one(rational::zero(), b1, a2, b2, val, bw);
|
||||
useful |= check_one(a1, b1, rational::zero(), b2, val, bw);
|
||||
}
|
||||
if (useful)
|
||||
round--;
|
||||
}
|
||||
}
|
||||
|
||||
}; // class test_fi
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
void tst_viable() {
|
||||
set_log_enabled(false);
|
||||
polysat::test1();
|
||||
polysat::test_univariate();
|
||||
polysat::test_univariate_minmax();
|
||||
polysat::test2(); // takes long
|
||||
polysat::test2();
|
||||
polysat::test_fi::exhaustive();
|
||||
polysat::test_fi::randomized(10000, 16);
|
||||
polysat::test_fi::randomized(1000, 256);
|
||||
#if 0
|
||||
// TODO: case where refine-equal-lin is still looping:
|
||||
polysat::test_fi::check_one(
|
||||
rational("359753528351133424343509264780402113166597651845926285955318862825137336"),
|
||||
rational("752856510718007431332405387553440539688023502087834331667662410998631117"),
|
||||
rational("359753528351133424343509264780402113166597651845926285955318862825137336"),
|
||||
rational("752856510698397765512447284907808137313109237627169307951559225462781625"),
|
||||
rational("453547182885518174546100861831801761371386469830527870060540275516786265"),
|
||||
256
|
||||
);
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue