mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Revisit ule_constraint simplifications and add unit test for this

Browse source 
If we can be certain of simplification results,
it is easier to recognize patterns for fixed bits and similar.
This commit is contained in:
Jakob Rath 2023-08-17 17:46:34 +02:00
parent 6593754cd6
commit f8c9ed1d90
3 changed files with 199 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

87
src/math/polysat/ule_constraint.cpp
View file

@ -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 << " == ";

5
src/math/polysat/ule_constraint.h
View file

@ -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); }

119
src/test/polysat.cpp
View file

@ -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