mirror of
https://github.com/Z3Prover/z3
synced 2025-06-22 22:03:39 +00:00
unit test notes
This commit is contained in:
Jakob Rath
parent
49590e0e01
commit
67c778a6da
1 changed files with 139 additions and 168 deletions
|
|
@ -125,49 +125,49 @@ namespace polysat {
|
|||
*/
|
||||
|
||||
/// Creates two separate conflicts (from narrowing) before solving loop is started.
|
||||
static void test_add_conflicts() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
s.add_eq(a + 1);
|
||||
s.add_eq(a + 2);
|
||||
s.add_eq(b + 1);
|
||||
s.add_eq(b + 2);
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
static void test_add_conflicts() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
s.add_eq(a + 1);
|
||||
s.add_eq(a + 2);
|
||||
s.add_eq(b + 1);
|
||||
s.add_eq(b + 2);
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
/// Has constraints which must be inserted into other watchlist to discover UNSAT
|
||||
static void test_wlist() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
auto c = s.var(s.add_var(3));
|
||||
auto d = s.var(s.add_var(3));
|
||||
s.add_eq(d + c + b + a + 1);
|
||||
s.add_eq(d + c + b + a);
|
||||
s.add_eq(d + c + b);
|
||||
s.add_eq(d + c);
|
||||
s.add_eq(d);
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
static void test_wlist() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
auto c = s.var(s.add_var(3));
|
||||
auto d = s.var(s.add_var(3));
|
||||
s.add_eq(d + c + b + a + 1);
|
||||
s.add_eq(d + c + b + a);
|
||||
s.add_eq(d + c + b);
|
||||
s.add_eq(d + c);
|
||||
s.add_eq(d);
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
/// Has a constraint in cjust[a] where a does not occur.
|
||||
static void test_cjust() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
auto c = s.var(s.add_var(3));
|
||||
// 1. Decide a = 0.
|
||||
s.add_eq(a*a + b + 7); // 2. Propagate b = 1
|
||||
s.add_eq(b*b + c*c*c*(b+7) + c + 5); // 3. Propagate c = 2
|
||||
s.add_eq(b*b + c*c); // 4. Conflict
|
||||
// Resolution fails because second constraint has c*c*c
|
||||
// => cjust[a] += b*b + c*c
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
static void test_cjust() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
auto b = s.var(s.add_var(3));
|
||||
auto c = s.var(s.add_var(3));
|
||||
// 1. Decide a = 0.
|
||||
s.add_eq(a*a + b + 7); // 2. Propagate b = 1
|
||||
s.add_eq(b*b + c*c*c*(b+7) + c + 5); // 3. Propagate c = 2
|
||||
s.add_eq(b*b + c*c); // 4. Conflict
|
||||
// Resolution fails because second constraint has c*c*c
|
||||
// => cjust[a] += b*b + c*c
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
/**
|
||||
* most basic linear equation solving.
|
||||
|
|
@ -207,7 +207,7 @@ namespace polysat {
|
|||
static void test_l4() {
|
||||
scoped_solver s(__func__);
|
||||
auto a = s.var(s.add_var(3));
|
||||
s.add_eq(4*a + 2);
|
||||
s.add_eq(4*a + 2); // always false due to parity
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
|
@ -223,7 +223,6 @@ namespace polysat {
|
|||
s.expect_sat({{a, 4}, {b, 4}});
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* This one is unsat because a*a*(a*a - 1)
|
||||
* is 0 for all values of a.
|
||||
|
|
@ -268,9 +267,9 @@ namespace polysat {
|
|||
|
||||
|
||||
// Unique solution: u = 5
|
||||
static void test_ineq_basic1() {
|
||||
static void test_ineq_basic1(unsigned bw = 32) {
|
||||
scoped_solver s(__func__);
|
||||
auto u = s.var(s.add_var(4));
|
||||
auto u = s.var(s.add_var(bw));
|
||||
s.add_ule(u, 5);
|
||||
s.add_ule(5, u);
|
||||
s.check();
|
||||
|
|
@ -278,9 +277,9 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// Unsatisfiable
|
||||
static void test_ineq_basic2() {
|
||||
static void test_ineq_basic2(unsigned bw = 32) {
|
||||
scoped_solver s(__func__);
|
||||
auto u = s.var(s.add_var(4));
|
||||
auto u = s.var(s.add_var(bw));
|
||||
s.add_ult(u, 5);
|
||||
s.add_ule(5, u);
|
||||
s.check();
|
||||
|
|
@ -288,11 +287,11 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// Solutions with u = v = w
|
||||
static void test_ineq_basic3() {
|
||||
static void test_ineq_basic3(unsigned bw = 32) {
|
||||
scoped_solver s(__func__);
|
||||
auto u = s.var(s.add_var(4));
|
||||
auto v = s.var(s.add_var(4));
|
||||
auto w = s.var(s.add_var(4));
|
||||
auto u = s.var(s.add_var(bw));
|
||||
auto v = s.var(s.add_var(bw));
|
||||
auto w = s.var(s.add_var(bw));
|
||||
s.add_ule(u, v);
|
||||
s.add_ule(v, w);
|
||||
s.add_ule(w, u);
|
||||
|
|
@ -303,11 +302,11 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// Unsatisfiable
|
||||
static void test_ineq_basic4() {
|
||||
static void test_ineq_basic4(unsigned bw = 32) {
|
||||
scoped_solver s(__func__);
|
||||
auto u = s.var(s.add_var(4));
|
||||
auto v = s.var(s.add_var(4));
|
||||
auto w = s.var(s.add_var(4));
|
||||
auto u = s.var(s.add_var(bw));
|
||||
auto v = s.var(s.add_var(bw));
|
||||
auto w = s.var(s.add_var(bw));
|
||||
s.add_ule(u, v);
|
||||
s.add_ult(v, w);
|
||||
s.add_ule(w, u);
|
||||
|
|
@ -1393,93 +1392,65 @@ namespace polysat {
|
|||
void tst_polysat() {
|
||||
using namespace polysat;
|
||||
|
||||
// test_polysat::test_add_conflicts(); // ok
|
||||
// test_polysat::test_wlist(); // ok
|
||||
// test_polysat::test_cjust(); // uses viable_fallback; weak lemmas
|
||||
// test_polysat::test_subst(); // TODO: assert + resource limit
|
||||
// test_polysat::test_pop_conflict(); // ok now (had bad conflict/pop interaction)
|
||||
|
||||
test_polysat::test_fi_zero();
|
||||
test_polysat::test_fi_nonzero();
|
||||
test_polysat::test_fi_nonmax();
|
||||
test_polysat::test_fi_disequal_mild();
|
||||
// test_polysat::test_l1(); // ok
|
||||
// test_polysat::test_l2(); // TODO: loops
|
||||
// test_polysat::test_l3(); // ok
|
||||
// test_polysat::test_l4(); // ok now (had assertion failure in conflict::insert)
|
||||
// test_polysat::test_l5(); // inefficient conflicts (needs equality reasoning)
|
||||
|
||||
// test_polysat::test_p1(); // ok (conflict @0 by viable_fallback)
|
||||
// test_polysat::test_p2(); // ok (viable_fallback finds the correct value)
|
||||
// test_polysat::test_p3(); // TODO: resource limit
|
||||
|
||||
// test_polysat::test_ineq_basic1(); // ok
|
||||
// test_polysat::test_ineq_basic2(); // TODO: assert / boolean conflict
|
||||
// test_polysat::test_ineq_basic3(); // ok
|
||||
// test_polysat::test_ineq_basic4(); // TODO: resource limit
|
||||
// test_polysat::test_ineq_basic5(); // works, but only because variable order changes after the conflict
|
||||
// TODO: non-asserting lemma
|
||||
// possible variable selection heuristic: start with the most restricted interval?
|
||||
// (if we have a restricted and non-restricted variable; we should probably pick the restricted one first. hoping that we can propagate and uncover restrictions on the other variable.)
|
||||
// test_polysat::test_ineq_basic6(); // same as ineq_basic5
|
||||
|
||||
#if 0
|
||||
// looks like a fishy conflict lemma?
|
||||
test_polysat::test_monot_bounds();
|
||||
return;
|
||||
|
||||
test_polysat::test_quot_rem_incomplete();
|
||||
test_polysat::test_quot_rem_fixed();
|
||||
//return;
|
||||
|
||||
test_polysat::test_band();
|
||||
return;
|
||||
|
||||
test_polysat::test_quot_rem();
|
||||
return;
|
||||
|
||||
test_polysat::test_ineq_axiom1();
|
||||
test_polysat::test_ineq_axiom2();
|
||||
test_polysat::test_ineq_axiom3();
|
||||
test_polysat::test_ineq_axiom4();
|
||||
test_polysat::test_ineq_axiom5();
|
||||
test_polysat::test_ineq_axiom6();
|
||||
return;
|
||||
|
||||
#endif
|
||||
|
||||
// test_polysat::test_var_minimize(); // works but var_minimized isn't used (UNSAT before lemma is created)
|
||||
|
||||
// test_polysat::test_ineq1(); // TODO: resource limit
|
||||
// test_polysat::test_ineq2(); // TODO: resource limit
|
||||
// test_polysat::test_monot(); // TODO: resource limit
|
||||
// test_polysat::test_monot_bounds(2); // weak conflicts
|
||||
// test_polysat::test_monot_bounds(8);
|
||||
// test_polysat::test_monot_bounds(); // TODO: resource limit
|
||||
// test_polysat::test_monot_bounds_full(); // TODO: triggers assertion in watchlist invariant
|
||||
// test_polysat::test_monot_bounds_simple(8); // undef
|
||||
// test_polysat::test_fixed_point_arith_div_mul_inverse(); // undef
|
||||
|
||||
test_polysat::test_add_conflicts();
|
||||
test_polysat::test_wlist();
|
||||
test_polysat::test_l1();
|
||||
test_polysat::test_l2();
|
||||
test_polysat::test_l3();
|
||||
test_polysat::test_l4();
|
||||
test_polysat::test_l5();
|
||||
test_polysat::test_p1();
|
||||
test_polysat::test_p2();
|
||||
test_polysat::test_p3();
|
||||
// test_polysat::test_ineq_axiom1();
|
||||
// test_polysat::test_ineq_axiom2();
|
||||
// test_polysat::test_ineq_axiom3();
|
||||
// test_polysat::test_ineq_axiom4();
|
||||
// test_polysat::test_ineq_axiom5();
|
||||
// test_polysat::test_ineq_axiom6();
|
||||
// test_polysat::test_ineq_non_axiom1(); // assertion but looks otherwise ok
|
||||
// test_polysat::test_ineq_non_axiom4(32, 5); // assertions/undef
|
||||
|
||||
test_polysat::test_ineq_basic1();
|
||||
test_polysat::test_ineq_basic2();
|
||||
test_polysat::test_ineq_basic3();
|
||||
test_polysat::test_ineq_basic4();
|
||||
test_polysat::test_ineq_basic5();
|
||||
test_polysat::test_ineq_basic6();
|
||||
// test_polysat::test_quot_rem_incomplete();
|
||||
// test_polysat::test_quot_rem_fixed();
|
||||
// test_polysat::test_band();
|
||||
// test_polysat::test_quot_rem();
|
||||
|
||||
test_polysat::test_cjust();
|
||||
test_polysat::test_subst();
|
||||
|
||||
test_polysat::test_var_minimize();
|
||||
|
||||
test_polysat::test_ineq1();
|
||||
test_polysat::test_ineq2();
|
||||
test_polysat::test_monot();
|
||||
test_polysat::test_monot_bounds(2);
|
||||
|
||||
return;
|
||||
|
||||
test_polysat::test_ineq_axiom1();
|
||||
test_polysat::test_ineq_axiom2();
|
||||
test_polysat::test_ineq_axiom3();
|
||||
test_polysat::test_ineq_axiom4();
|
||||
test_polysat::test_ineq_axiom5();
|
||||
test_polysat::test_ineq_axiom6();
|
||||
|
||||
test_fi::exhaustive();
|
||||
test_fi::randomized();
|
||||
return;
|
||||
|
||||
#if 0
|
||||
test_polysat::test_ineq_non_axiom4(32, 5);
|
||||
#endif
|
||||
|
||||
// inefficient conflicts:
|
||||
// Takes time: test_polysat::test_monot_bounds_full();
|
||||
|
||||
test_polysat::test_monot_bounds_simple(8);
|
||||
test_polysat::test_fixed_point_arith_div_mul_inverse();
|
||||
// test_polysat::test_fi_zero(); // ok
|
||||
// test_polysat::test_fi_nonzero(); // ok
|
||||
// test_polysat::test_fi_nonmax(); // ok (viable_fallback chooses value for second variable)
|
||||
// test_polysat::test_fi_disequal_mild(); // ok
|
||||
|
||||
// test_fi::exhaustive();
|
||||
// test_fi::randomized();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue