mirror of
https://github.com/Z3Prover/z3
synced 2025-06-26 15:53:41 +00:00
add notes and unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
6478e789e9
commit
dc55fbf30d
2 changed files with 138 additions and 13 deletions
|
|
@ -12,7 +12,8 @@ Author:
|
||||||
|
|
||||||
Notes:
|
Notes:
|
||||||
|
|
||||||
Rewrite rules to simplify expressions
|
Rewrite rules to simplify expressions.
|
||||||
|
In the following let k, k1, k2 be values.
|
||||||
|
|
||||||
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
|
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
|
||||||
- k1 <= k2 ==> 1 <= 0 if k1 > k2
|
- k1 <= k2 ==> 1 <= 0 if k1 > k2
|
||||||
|
|
@ -21,9 +22,16 @@ Notes:
|
||||||
- k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2.
|
- k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2.
|
||||||
- k <= p ==> p - k <= - k - 1
|
- k <= p ==> p - k <= - k - 1
|
||||||
|
|
||||||
TODO:
|
TODO: clause simplifications:
|
||||||
- p <= p + q ==> p <= -q - 1
|
|
||||||
- p + k <= p ==> p + k <= k - 1 for k > 0
|
- p + k <= p ==> p + k <= k or p = 0 for k != 0
|
||||||
|
- p*q = 0 ==> p = 0 or q = 0 applies to any factoring
|
||||||
|
- 2*p <= 2*q ==> (p >= 2^n-1 & q < 2^n-1) or (p >= 2^n-1 = q >= 2^n-1 & p <= q)
|
||||||
|
==> (p >= 2^n-1 => q < 2^n-1 or p <= q) &
|
||||||
|
(p < 2^n-1 => p <= q) &
|
||||||
|
(p < 2^n-1 => q < 2^n-1)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
|
|
||||||
|
|
@ -54,6 +62,10 @@ namespace polysat {
|
||||||
m_lhs = 0, m_rhs = 0;
|
m_lhs = 0, m_rhs = 0;
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
if (m_lhs == m_rhs) {
|
||||||
|
m_lhs = m_rhs = 0;
|
||||||
|
return;
|
||||||
|
}
|
||||||
if (m_lhs.is_val() && m_rhs.is_val()) {
|
if (m_lhs.is_val() && m_rhs.is_val()) {
|
||||||
if (m_lhs.val() <= m_rhs.val())
|
if (m_lhs.val() <= m_rhs.val())
|
||||||
m_lhs = m_rhs = 0;
|
m_lhs = m_rhs = 0;
|
||||||
|
|
@ -75,6 +87,7 @@ namespace polysat {
|
||||||
if (x.is_neg())
|
if (x.is_neg())
|
||||||
x = mod(x, m_lhs.manager().two_to_N());
|
x = mod(x, m_lhs.manager().two_to_N());
|
||||||
m_lhs *= x;
|
m_lhs *= x;
|
||||||
|
SASSERT(m_lhs.leading_coefficient().is_power_of_two());
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -725,7 +725,7 @@ namespace polysat {
|
||||||
void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
|
void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
|
||||||
SASSERT(k < 6);
|
SASSERT(k < 6);
|
||||||
unsigned i = k % 3;
|
unsigned i = k % 3;
|
||||||
unsigned j = i % 2;
|
unsigned j = k % 2;
|
||||||
if (i == 1)
|
if (i == 1)
|
||||||
std::swap(a, b);
|
std::swap(a, b);
|
||||||
else if (i == 2)
|
else if (i == 2)
|
||||||
|
|
@ -734,6 +734,40 @@ namespace polysat {
|
||||||
std::swap(b, c);
|
std::swap(b, c);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void permute_args(unsigned n, pdd& a, pdd& b, pdd& c, pdd& d) {
|
||||||
|
SASSERT(n < 24);
|
||||||
|
switch (n % 4) {
|
||||||
|
case 1:
|
||||||
|
std::swap(a, b);
|
||||||
|
break;
|
||||||
|
case 2:
|
||||||
|
std::swap(a, c);
|
||||||
|
break;
|
||||||
|
case 3:
|
||||||
|
std::swap(a, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
switch (n % 3) {
|
||||||
|
case 1:
|
||||||
|
std::swap(b, c);
|
||||||
|
break;
|
||||||
|
case 2:
|
||||||
|
std::swap(b, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
switch (n % 2) {
|
||||||
|
case 1:
|
||||||
|
std::swap(c, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// xy < xz and !Omega(x*y) => y < z
|
// xy < xz and !Omega(x*y) => y < z
|
||||||
static void test_ineq_axiom1(unsigned bw = 32) {
|
static void test_ineq_axiom1(unsigned bw = 32) {
|
||||||
auto const bound = rational::power_of_two(bw-1);
|
auto const bound = rational::power_of_two(bw-1);
|
||||||
|
|
@ -798,9 +832,84 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
|
|
||||||
// xy < b & a <= x & !Omega(x*y) => a*y < b
|
// xy < b & a <= x & !Omega(x*y) => a*y < b
|
||||||
|
static void test_ineq_axiom3(unsigned bw = 32) {
|
||||||
|
auto const bound = rational::power_of_two(bw - 1);
|
||||||
|
for (unsigned i = 0; i < 24; ++i) {
|
||||||
|
scoped_solver s(__func__);
|
||||||
|
auto x = s.var(s.add_var(bw));
|
||||||
|
auto y = s.var(s.add_var(bw));
|
||||||
|
auto a = s.var(s.add_var(bw));
|
||||||
|
auto b = s.var(s.add_var(bw));
|
||||||
|
permute_args(i, x, y, a, b);
|
||||||
|
s.add_ult(x * y, b);
|
||||||
|
s.add_ule(a, x);
|
||||||
|
s.add_ult(x, bound);
|
||||||
|
s.add_ult(y, bound);
|
||||||
|
s.add_ule(b, a * y);
|
||||||
|
s.check();
|
||||||
|
s.expect_unsat();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// xy <= b & a <= x & !Omega(x*y) => a*y <= b
|
// xy <= b & a <= x & !Omega(x*y) => a*y <= b
|
||||||
|
static void test_ineq_axiom4(unsigned bw = 32) {
|
||||||
|
auto const bound = rational::power_of_two(bw - 1);
|
||||||
|
for (unsigned i = 0; i < 24; ++i) {
|
||||||
|
scoped_solver s(__func__);
|
||||||
|
auto x = s.var(s.add_var(bw));
|
||||||
|
auto y = s.var(s.add_var(bw));
|
||||||
|
auto a = s.var(s.add_var(bw));
|
||||||
|
auto b = s.var(s.add_var(bw));
|
||||||
|
permute_args(i, x, y, a, b);
|
||||||
|
s.add_ule(x * y, b);
|
||||||
|
s.add_ule(a, x);
|
||||||
|
s.add_ult(x, bound);
|
||||||
|
s.add_ult(y, bound);
|
||||||
|
s.add_ult(b, a * y);
|
||||||
|
s.check();
|
||||||
|
s.expect_unsat();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// a < xy & x <= b & !Omega(x*y) => a < b*y
|
// a < xy & x <= b & !Omega(x*y) => a < b*y
|
||||||
// a <= xy & x <= b & !omega(x*y) => a <= b*y
|
static void test_ineq_axiom5(unsigned bw = 32) {
|
||||||
|
auto const bound = rational::power_of_two(bw - 1);
|
||||||
|
for (unsigned i = 0; i < 24; ++i) {
|
||||||
|
scoped_solver s(__func__);
|
||||||
|
auto x = s.var(s.add_var(bw));
|
||||||
|
auto y = s.var(s.add_var(bw));
|
||||||
|
auto a = s.var(s.add_var(bw));
|
||||||
|
auto b = s.var(s.add_var(bw));
|
||||||
|
permute_args(i, x, y, a, b);
|
||||||
|
s.add_ult(a, x * y);
|
||||||
|
s.add_ule(x, b);
|
||||||
|
s.add_ult(x, bound);
|
||||||
|
s.add_ult(y, bound);
|
||||||
|
s.add_ule(b * y, a);
|
||||||
|
s.check();
|
||||||
|
s.expect_unsat();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// a <= xy & x <= b & !Omega(x*y) => a <= b*y
|
||||||
|
static void test_ineq_axiom6(unsigned bw = 32) {
|
||||||
|
auto const bound = rational::power_of_two(bw - 1);
|
||||||
|
for (unsigned i = 0; i < 24; ++i) {
|
||||||
|
scoped_solver s(__func__);
|
||||||
|
auto x = s.var(s.add_var(bw));
|
||||||
|
auto y = s.var(s.add_var(bw));
|
||||||
|
auto a = s.var(s.add_var(bw));
|
||||||
|
auto b = s.var(s.add_var(bw));
|
||||||
|
permute_args(i, x, y, a, b);
|
||||||
|
s.add_ule(a, x * y);
|
||||||
|
s.add_ule(x, b);
|
||||||
|
s.add_ult(x, bound);
|
||||||
|
s.add_ult(y, bound);
|
||||||
|
s.add_ult(b * y, a);
|
||||||
|
s.check();
|
||||||
|
s.expect_unsat();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
// 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
|
||||||
|
|
@ -930,15 +1039,11 @@ void tst_polysat() {
|
||||||
polysat::test_subst();
|
polysat::test_subst();
|
||||||
|
|
||||||
|
|
||||||
// polysat::test_ineq_axiom1();
|
|
||||||
// return;
|
|
||||||
|
|
||||||
// not working
|
// not working
|
||||||
// polysat::test_fixed_point_arith_div_mul_inverse();
|
// polysat::test_fixed_point_arith_div_mul_inverse();
|
||||||
|
|
||||||
// polysat::test_monot_bounds_simple(8);
|
// polysat::test_monot_bounds_simple(8);
|
||||||
|
|
||||||
|
|
||||||
// working
|
// working
|
||||||
polysat::test_fixed_point_arith_mul_div_inverse();
|
polysat::test_fixed_point_arith_mul_div_inverse();
|
||||||
|
|
||||||
|
|
@ -965,6 +1070,13 @@ void tst_polysat() {
|
||||||
polysat::test_monot_bounds(2);
|
polysat::test_monot_bounds(2);
|
||||||
polysat::test_cjust();
|
polysat::test_cjust();
|
||||||
|
|
||||||
|
polysat::test_ineq_axiom1();
|
||||||
|
polysat::test_ineq_axiom2();
|
||||||
|
polysat::test_ineq_axiom3();
|
||||||
|
polysat::test_ineq_axiom4();
|
||||||
|
polysat::test_ineq_axiom5();
|
||||||
|
polysat::test_ineq_axiom6();
|
||||||
|
|
||||||
// inefficient conflicts:
|
// inefficient conflicts:
|
||||||
// Takes time: polysat::test_monot_bounds_full();
|
// Takes time: polysat::test_monot_bounds_full();
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue