From dc55fbf30d6467745ef22fc18864528f81199bad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Sep 2021 05:04:07 -0700 Subject: [PATCH] add notes and unit tests Signed-off-by: Nikolaj Bjorner --- src/math/polysat/ule_constraint.cpp | 23 +++-- src/test/polysat.cpp | 128 ++++++++++++++++++++++++++-- 2 files changed, 138 insertions(+), 13 deletions(-) diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index c95c7d2eb..bef07c891 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -12,7 +12,8 @@ Author: 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 ==> 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 <= p ==> p - k <= - k - 1 - TODO: - - p <= p + q ==> p <= -q - 1 - - p + k <= p ==> p + k <= k - 1 for k > 0 +TODO: clause simplifications: + + - 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) + + --*/ @@ -53,7 +61,11 @@ namespace polysat { if (m_rhs.is_val() && m_rhs.val() == m_rhs.manager().max_value()) { m_lhs = 0, m_rhs = 0; return; - } + } + if (m_lhs == m_rhs) { + m_lhs = m_rhs = 0; + return; + } if (m_lhs.is_val() && m_rhs.is_val()) { if (m_lhs.val() <= m_rhs.val()) m_lhs = m_rhs = 0; @@ -75,6 +87,7 @@ namespace polysat { if (x.is_neg()) x = mod(x, m_lhs.manager().two_to_N()); m_lhs *= x; + SASSERT(m_lhs.leading_coefficient().is_power_of_two()); } } diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index dcb3f72c6..1b989b38b 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -725,7 +725,7 @@ namespace polysat { void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) { SASSERT(k < 6); unsigned i = k % 3; - unsigned j = i % 2; + unsigned j = k % 2; if (i == 1) std::swap(a, b); else if (i == 2) @@ -734,6 +734,40 @@ namespace polysat { 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 static void test_ineq_axiom1(unsigned bw = 32) { 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 + 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 + 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 + 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 @@ -930,14 +1039,10 @@ void tst_polysat() { polysat::test_subst(); -// polysat::test_ineq_axiom1(); -// return; // not working - // polysat::test_fixed_point_arith_div_mul_inverse(); - - //polysat::test_monot_bounds_simple(8); - + // polysat::test_fixed_point_arith_div_mul_inverse(); + // polysat::test_monot_bounds_simple(8); // working polysat::test_fixed_point_arith_mul_div_inverse(); @@ -965,6 +1070,13 @@ void tst_polysat() { polysat::test_monot_bounds(2); 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: // Takes time: polysat::test_monot_bounds_full();