diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 0ef575d5b..e87c75898 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -82,6 +82,10 @@ namespace { // NOTE: the result should not depend on the initial value of is_positive; // the purpose of is_positive is to allow flipping the sign as part of a rewrite rule. void simplify_impl(bool& is_positive, pdd& lhs, pdd& rhs) { + scoped_set_log_enabled _log(false); + SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2()); + unsigned const N = lhs.power_of_2(); + // 0 <= p --> 0 <= 0 if (lhs.is_zero()) { rhs = 0; @@ -125,6 +129,7 @@ namespace { unsigned const rhs_vars = rhs.free_vars().size(); unsigned const diff_vars = (lhs - rhs).free_vars().size(); if (diff_vars < lhs_vars || diff_vars < rhs_vars) { + LOG("reduce number of varables"); // verbose_stream() << "IN: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n"; if (lhs_vars <= rhs_vars) rhs = lhs - rhs - 1; @@ -134,19 +139,60 @@ namespace { } } -#if 0 - // TODO: maybe enable this later to make some constraints more readable + // -p + k <= k --> p <= k + if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) { + LOG("-p + k <= k --> p <= k"); + lhs = rhs - lhs; + } + + // k <= p + k --> p <= -k-1 + if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) { + LOG("k <= p + k --> p <= -k-1"); + pdd k = lhs; + lhs = rhs - lhs; + rhs = -k - 1; + } + + // k <= -p --> p-1 <= -k-1 + if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) { + LOG("k <= -p --> p-1 <= -k-1"); + pdd k = lhs; + lhs = -(rhs + 1); + rhs = -k - 1; + } + + // -p <= k --> -k-1 <= p-1 + // if (rhs.is_val() && lhs.leading_coefficient() > rational::power_of_two(N - 1) && !lhs.offset().is_zero()) { + if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) { + LOG("-p <= k --> -k-1 <= p-1"); + pdd k = rhs; + rhs = -(lhs + 1); + lhs = -k - 1; + } + + // NOTE: do not use pdd operations in conditions when comparing pdd values. + // e.g.: "lhs.offset() == (rhs + 1).val()" is problematic with the following evaluation: + // 1. return reference into pdd_manager::m_values from lhs.offset() + // 2. compute rhs+1, which may reallocate pdd_manager::m_values + // 3. now the reference returned from lhs.offset() may be invalid + pdd const rhs_plus_one = rhs + 1; + // p - k <= -k - 1 --> k <= p - // ALTERNATIVE: p > k-1 to keep the polynomial on the lhs? allows us to have boolean conflicts between x <= k and x > k ? (otherwise it is x <= k and k+1 <= x.) - if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == (rhs + 1).val()) { - // verbose_stream() << "IN: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n"; - std::abort(); + // TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken. + if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) { + LOG("p - k <= -k - 1 --> k <= p"); pdd k = -(rhs + 1); rhs = lhs + k; lhs = k; - // verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n"; } -#endif + + pdd const lhs_minus_one = lhs - 1; + + // k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q + if (lhs.is_val() && rhs.leading_coefficient() == rational::power_of_two(N-1) && rhs.offset() == lhs_minus_one.val()) { + LOG("k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q"); + rhs = (lhs - 1) - rhs; + } // -1 <= p --> p + 1 <= 0 if (lhs.is_max()) { @@ -227,9 +273,34 @@ namespace polysat { SASSERT(rhs.is_zero()); } } + SASSERT(is_simplified(lhs, rhs)); // rewriting should be idempotent #endif } + bool ule_constraint::is_simplified(pdd const& lhs0, pdd const& rhs0) { + bool const pos0 = true; + bool pos1 = pos0; + pdd lhs1 = lhs0; + pdd rhs1 = rhs0; + simplify_impl(pos1, lhs1, rhs1); + bool const is_simplified = (pos1 == pos0 && lhs1 == lhs0 && rhs1 == rhs0); + if (!is_simplified) { + LOG("Not simplified: " << lhs0 << " <= " << rhs0); + LOG(" --> " << lhs1 << " <= " << rhs1); + } + DEBUG_CODE({ + // check that simplification doesn't depend on initial sign + bool pos2 = !pos0; + pdd lhs2 = lhs0; + pdd rhs2 = rhs0; + simplify_impl(pos2, lhs2, rhs2); + SASSERT_EQ(pos2, !pos1); + SASSERT_EQ(lhs2, lhs1); + SASSERT_EQ(rhs2, rhs1); + }); + return is_simplified; + } + std::ostream& ule_constraint::display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs) { out << lhs; if (rhs.is_zero() && status == l_true) out << " == "; diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index d721b420c..80bb7d71b 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -26,7 +26,6 @@ namespace polysat { pdd m_rhs; ule_constraint(pdd const& l, pdd const& r); - static void simplify(bool& is_positive, pdd& lhs, pdd& rhs); static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); } static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); } static lbool eval(pdd const& lhs, pdd const& rhs); @@ -46,6 +45,9 @@ namespace polysat { bool is_eq() const override { return m_rhs.is_zero(); } void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; unsigned power_of_2() const { return m_lhs.power_of_2(); } + + static void simplify(bool& is_positive, pdd& lhs, pdd& rhs); + static bool is_simplified(pdd const& lhs, pdd const& rhs); // return true if lhs <= rhs is not simplified further. this is meant to be used in assertions. }; struct ule_pp { @@ -53,6 +55,7 @@ namespace polysat { pdd lhs; pdd rhs; ule_pp(lbool status, pdd const& lhs, pdd const& rhs): status(status), lhs(lhs), rhs(rhs) {} + ule_pp(lbool status, ule_constraint const& ule): status(status), lhs(ule.lhs()), rhs(ule.rhs()) {} }; inline std::ostream& operator<<(std::ostream& out, ule_pp const& u) { return ule_constraint::display(out, u.status, u.lhs, u.rhs); } diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index b82f5593b..b0f8042cb 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1952,6 +1952,113 @@ namespace polysat { //s.expect_unsat(); } + static void test_fi_pow2_a() { + scoped_solver s(__func__); + auto const x = s.var(s.add_var(256)); + rational const a = rational::power_of_two(253); + s.add_eq(a*x); // x[3:] == 0 + s.add_eq(a*x, a*3); // x[3:] == 3 + s.check(); + s.expect_unsat(); + } + + static void test_fi_pow2_b() { + scoped_solver s(__func__); + auto const x = s.var(s.add_var(256)); + rational const a = rational::power_of_two(253) + 2; + // s.add_eq(a*x); + // s.add_eq(a*x, 6); + s.add_ule(a*x, 1); + s.add_ule(a*x - 6, 1); + s.check(); + s.expect_unsat(); + } + + static void test_fi_pow2_c() { + scoped_solver s(__func__); + auto const x = s.var(s.add_var(256)); + s.add_eq(rational::power_of_two(253)*x); // 2^253*x == 0 ... lowest three bits are zero + s.add_diseq(rational::power_of_two(254)*x); // 2^254*x != 0 ... lowest two bits aren't zero + s.check(); + s.expect_unsat(); + } + + // Test rewrite rules for ule_constraints. + // Since we recognize some syntactic patterns in constraints, + // make sure that equivalent forms are rewritten to the same result. + static void test_ule_simplify() { + scoped_solver s(__func__); + unsigned const N = 64; + auto const x = s.var(s.add_var(N)); + scoped_set_log_enabled _log(true); + test_ule_simplify(s, true, x, rational::power_of_two(16)); + test_ule_simplify(s, true, x, rational::power_of_two(48) + rational::power_of_two(23)); + test_ule_simplify(s, true, x, rational::power_of_two(63)); + test_ule_simplify(s, true, rational::power_of_two(16), x); + test_ule_simplify(s, true, rational::power_of_two(48) + rational::power_of_two(23), x); + test_ule_simplify(s, true, rational::power_of_two(63), x); + test_ule_simplify(s, true, rational(1), x, false, x, rational(0)); + test_ule_simplify(s, true, rational::power_of_two(16) * (x - 1234), rational(0)); // 2^k * x = m * 2^k + test_ule_simplify(s, true, rational::power_of_two(63) * (x - 1234), rational(0)); // 2^k * x = m * 2^k + test_ule_simplify(s, true, rational::power_of_two(N - 1), x * rational::power_of_two(N - 1 - 5)); // bit(x, 5) + test_ule_simplify(s, true, rational::power_of_two(N - 1), x * rational::power_of_two(N - 1)); // bit(x, 0) + for (unsigned i = 0; i < N; ++i) { + scoped_set_log_enabled _logg(false); + test_ule_simplify(s, true, x, rational::power_of_two(i)); + if (i == 0) + test_ule_simplify(s, true, rational::power_of_two(i), x, false, x, rational(0)); // special case for 1 <= x ==> x > 0 + else + test_ule_simplify(s, true, rational::power_of_two(i), x); + test_ule_simplify(s, true, rational::power_of_two(N - 1), x * rational::power_of_two(N - 1 - i)); // bit(x, i) + } + } + + static void test_ule_simplify(solver& s, bool is_positive, rational const& p, pdd const& q) { + test_ule_simplify(s, is_positive, q.manager().mk_val(p), q); + } + + static void test_ule_simplify(solver& s, bool is_positive, pdd const& p, rational const& q) { + test_ule_simplify(s, is_positive, p, p.manager().mk_val(q)); + } + + // The argument is the expected form of the constraint. + // Checks if equivalent forms are rewritten by ule_constraint::simplify to the expected form. + static void test_ule_simplify(solver& s, bool const is_positive, pdd const& p, pdd const& q) { + LOG_H2("Constraint " << ule_pp(to_lbool(is_positive), p, q)); + inequality const i = inequality::from_ule(is_positive ? s.ule(p, q) : ~s.ule(p, q)); + bool ok = true; + for (unsigned j = 0; j < 6; ++j) { + inequality const i2 = i.rewrite_equiv(j); + pdd lhs = i2.is_strict() ? i2.rhs() : i2.lhs(); + pdd rhs = i2.is_strict() ? i2.lhs() : i2.rhs(); + bool pos = !i2.is_strict(); + { + scoped_set_log_enabled _log(false); + ule_constraint::simplify(pos, lhs, rhs); + } + LOG(rpad(50, i2) << " --> " << ule_pp(to_lbool(pos), lhs, rhs)); + ok = ok && (lhs == p) && (rhs == q) && (pos == is_positive); + } + VERIFY(ok); + } + + // test expected rewrite before checking equivalent forms + static void test_ule_simplify(solver& s, bool is_positive, pdd p, pdd q, bool expect_pos, pdd const& expect_p, pdd const& expect_q) { + { + scoped_set_log_enabled _log(false); + ule_constraint::simplify(is_positive, p, q); + } + SASSERT_EQ(is_positive, expect_pos); + SASSERT_EQ(p, expect_p); + SASSERT_EQ(q, expect_q); + test_ule_simplify(s, is_positive, p, q); + } + + static void test_ule_simplify(solver& s, bool is_positive, rational const& p, pdd q, bool expect_pos, pdd const& expect_p, rational const& expect_q) { + test_ule_simplify(s, is_positive, q.manager().mk_val(p), q, expect_pos, expect_p, expect_p.manager().mk_val(expect_q)); + } + + }; // class test_polysat } // namespace polysat @@ -1966,11 +2073,16 @@ static void STD_CALL polysat_on_ctrl_c(int) { void tst_polysat() { using namespace polysat; -#if 0 // Enable this block to run a single unit test with detailed output. +#if 1 // Enable this block to run a single unit test with detailed output. collect_test_records = false; test_max_conflicts = 50; - //test_polysat::test_bench13_mulovfl_ineq(); - test_polysat::test_ineq_axiom3(32, 3); // TODO: assertion + test_polysat::test_ule_simplify(); + // test_polysat::test_fi_pow2_a(); + // test_polysat::test_fi_pow2_b(); + // test_polysat::test_fi_pow2_c(); + // test_polysat::test_monot(); + // test_polysat::test_bench13_mulovfl_ineq(); + // test_polysat::test_ineq_axiom3(32, 3); // TODO: assertion // test_polysat::test_ineq_axiom6(32, 0); // TODO: assertion // test_polysat::test_band5(); // TODO: assertion when clause simplification (merging p>q and p=q) is enabled // test_polysat::test_bench27_viable1(); // TODO: refinement @@ -1988,6 +2100,7 @@ void tst_polysat() { signal(SIGINT, polysat_on_ctrl_c); set_default_debug_action(debug_action::throw_exception); set_log_enabled(false); + set_verbosity_level(0); } #if 0