mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Some bugfixes and unit-tests for variable elimination

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-16 10:12:34 +01:00
parent dc95179ae5
commit 71211f3134
4 changed files with 266 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict.cpp
View file

@ -79,7 +79,11 @@ namespace polysat {
// Analyse current conflict core to extract additional lemmas
void find_extra_lemmas(conflict& core) {
#if 1
// Don't do variable elimination for now
#else
m_free_variable_elimination.find_lemma(core);
#endif
}
};

76
src/math/polysat/variable_elimination.cpp
View file

@ -236,8 +236,8 @@ namespace polysat {
LOG("core: " << core);
LOG("Free variables: " << s.m_free_pvars);
for (pvar v : core.vars_occurring_in_constraints())
if (!s.is_assigned(v)) // TODO: too restrictive. should also consider variables that will be unassigned only after backjumping (can update this after assignment handling in search state is refactored.)
find_lemma(v, core);
//if (!s.is_assigned(v)) // TODO: too restrictive. should also consider variables that will be unassigned only after backjumping (can update this after assignment handling in search state is refactored.)
find_lemma(v, core);
}
void free_variable_elimination::find_lemma(pvar v, conflict& core) {
@ -261,8 +261,8 @@ namespace polysat {
pdd fac = m.zero();
pdd rest = m.zero();
p.factor(v, 1, fac, rest);
if (rest.is_val())
return;
//if (rest.is_val()) // TODO: Why do we need this?
// return;
SASSERT(!fac.free_vars().contains(v));
SASSERT(!rest.free_vars().contains(v));
@ -314,31 +314,49 @@ namespace polysat {
pdd coeff_odd = p.manager().zero();
optional<pdd> fac_odd_inv;
bool is_multiple1 = is_multiple(fac_lhs, fac, new_lhs);
bool is_multiple2 = is_multiple(fac_rhs, fac, new_rhs);
get_multiple_result multiple1 = get_multiple(fac_lhs, fac, new_lhs);
get_multiple_result multiple2 = get_multiple(fac_rhs, fac, new_rhs);
if (multiple1 == cannot_multiple || multiple2 == cannot_multiple)
continue;
bool evaluated = false;
substitution sub(m);
if (!is_multiple1 || !is_multiple2) {
if (multiple1 == can_multiple || multiple2 == can_multiple) {
if (
(!fac.is_val() && !fac.is_var()) ||
(!fac_lhs.is_val() && !fac_lhs.is_var()) ||
(!fac_rhs.is_val() && !fac_rhs.is_var())) {
// TODO: We could introduce a new variable "new_var = lc" and add the valuation for this new variable
if (s.is_assigned(v))
continue; // We could not eliminate it symbolically and evaluating makes no sense as we already have a value for it
pdd const fac_eval = eval(fac, core, sub);
LOG("lcs: " << fac_eval);
LOG("fac_eval: " << fac_eval);
pdd fac_eval_inv = m.zero();
// TODO: We can now again use multiples instead of failing if it is not invertible
// e.g., x * y + x * z = z (with y = 0 eval)
// and, 3 * x * z <= 0
// We don't do anything, although we could
// x * z = z
// and multiplying with 3 results in a feasible replacement
if (!inv(fac_eval, fac_eval_inv))
continue;
LOG("fac_eval_inv: " << fac_eval_inv);
pdd const rest_eval = sub.apply_to(rest);
LOG("rest_eval: " << rest_eval);
pdd const vs = -rest_eval * fac_eval_inv; // this is the polynomial that computes v
LOG("vs: " << vs);
SASSERT(!vs.free_vars().contains(v));
new_lhs = c_target->to_ule().lhs().subst_pdd(v, vs);
new_rhs = c_target->to_ule().rhs().subst_pdd(v, vs);
// TODO: Why was the assignment (sub) not applied to the result in previous commits?
new_lhs = sub.apply_to(c_target->to_ule().lhs().subst_pdd(v, vs));
new_rhs = sub.apply_to(c_target->to_ule().rhs().subst_pdd(v, vs));
evaluated = true;
}
else {
@ -354,7 +372,7 @@ namespace polysat {
}
if (!evaluated) {
if (!is_multiple1) { // Sometimes we can simply unify the two equations
if (multiple1 == can_multiple) {
pdd pv_lhs = get_dyadic_valuation(fac_lhs).first;
pdd odd_fac_lhs = get_odd(fac_lhs);
pdd power_diff_lhs = s.shl(m.one(), pv_lhs - pv_equality);
@ -365,10 +383,12 @@ namespace polysat {
new_lhs = -rest * *fac_odd_inv * power_diff_lhs * odd_fac_lhs + rest_rhs;
p1 = s.ule(get_dyadic_valuation(fac).first, get_dyadic_valuation(fac_lhs).first);
}
else
else {
SASSERT(multiple1 == is_multiple);
new_lhs = -rest * new_lhs + rest_lhs;
}
if (!is_multiple2) {
if (multiple2 == can_multiple) {
pdd pv_rhs = get_dyadic_valuation(fac_rhs).first;
pdd odd_fac_rhs = get_odd(fac_rhs);
pdd power_diff_rhs = s.shl(m.one(), pv_rhs - pv_equality);
@ -379,8 +399,10 @@ namespace polysat {
new_rhs = -rest * *fac_odd_inv * power_diff_rhs * odd_fac_rhs + rest_rhs;
p2 = s.ule(get_dyadic_valuation(fac).first, get_dyadic_valuation(fac_rhs).first);
}
else
else {
SASSERT(multiple2 == is_multiple);
new_rhs = -rest * new_rhs + rest_rhs;
}
}
signed_constraint c_new = s.ule(new_lhs , new_rhs);
@ -411,7 +433,7 @@ namespace polysat {
cb.insert(c_new);
ref<clause> c = cb.build();
if (c) // Can we get tautologies this way?
core.add_lemma("variable elimination", cb.build());
core.add_lemma("variable elimination", c);
}
}
@ -421,15 +443,13 @@ namespace polysat {
// TODO: recognize constraints of the form "v1 == 27" to be used in the assignment?
// (but maybe useful evaluations are always part of core.vars() anyway?)
substitution& sub = out_sub;
SASSERT(sub.empty());
SASSERT(out_sub.empty());
for (auto v : p.free_vars())
if (core.contains_pvar(v))
sub.add(v, s.get_value(v));
pdd q = sub.apply_to(p);
out_sub = out_sub.add(v, s.get_value(v));
pdd q = out_sub.apply_to(p);
// TODO: like in the old conflict::minimize_vars, we can now try to remove unnecessary variables from a.
return q;
@ -449,19 +469,19 @@ namespace polysat {
}
bool free_variable_elimination::is_multiple(const pdd& p1, const pdd& p2, pdd& out) {
LOG("Check if there is an easy way to unify " << p1 << " and " << p2);
free_variable_elimination::get_multiple_result free_variable_elimination::get_multiple(const pdd& p1, const pdd& p2, pdd& out) {
LOG("Check if there is an easy way to unify " << p2 << " and " << p1);
if (p1.is_zero()) {
out = p1.manager().zero();
return true;
return is_multiple;
}
if (p2.is_one()) {
out = p1;
return true;
return is_multiple;
}
if (!p1.is_monomial() || !p2.is_monomial())
// TODO: Actually, this could work as well. (4a*d + 6b*c*d) is a multiple of (2a + 3b*c) although none of them is a monomial
return false;
return can_multiple;
dd::pdd_monomial p1m = *p1.begin();
dd::pdd_monomial p2m = *p2.begin();
@ -469,7 +489,7 @@ namespace polysat {
unsigned tz2 = p2m.coeff.trailing_zeros();
if (tz2 > tz1)
return false; // The constant coefficient is not invertible
return cannot_multiple; // The constant coefficient is not invertible
rational odd = div(p2m.coeff, rational::power_of_two(tz2));
rational inv;
@ -489,7 +509,7 @@ namespace polysat {
for (const auto& occ : m_occ)
m_occ_cnt[occ] = 0;
m_occ.clear();
return false; // p2 contains more v2 than p1
return can_multiple; // p2 contains more v2 than p1; we need more information
}
m_occ_cnt[v2]--;
}
@ -502,7 +522,7 @@ namespace polysat {
}
m_occ.clear();
LOG("Found multiple: " << out);
return true;
return is_multiple;
}
}

8
src/math/polysat/variable_elimination.h
View file

@ -21,7 +21,11 @@ namespace polysat {
class conflict;
class free_variable_elimination {
enum get_multiple_result {
is_multiple, can_multiple, cannot_multiple
};
solver& s;
unsigned_vector m_has_validation_of_range; // TODO: Find a better name
unsigned_vector m_pv_constants;
@ -42,7 +46,7 @@ namespace polysat {
void find_lemma(pvar v, signed_constraint c, conflict& core);
pdd eval(pdd const& p, conflict& core, substitution& out_sub);
bool inv(pdd const& p, pdd& out_p_inv);
bool is_multiple(const pdd& p1, const pdd& p2, pdd &out);
get_multiple_result get_multiple(const pdd& p1, const pdd& p2, pdd &out);
public:
free_variable_elimination(solver& s): s(s) {}
void find_lemma(conflict& core);

210
src/test/polysat.cpp
View file

@ -1,5 +1,6 @@
#include "math/polysat/log.h"
#include "math/polysat/solver.h"
#include "math/polysat/variable_elimination.h"
#include "ast/ast.h"
#include "parsers/smt2/smt2parser.h"
#include "util/util.h"
@ -1093,6 +1094,201 @@ namespace polysat {
s.expect_unsat();
}
static void expect_lemma_cnt(conflict& cfl, unsigned cnt) {
auto lemmas = cfl.lemmas();
if (lemmas.size() == cnt)
return;
LOG_H1("FAIL: Expected " << cnt << " learned lemmas; got " << lemmas.size() << "!");
if (!collect_test_records)
VERIFY(false);
}
static void expect_lemma(solver& s, conflict& cfl, signed_constraint c1) {
LOG_H1("Looking for constraint: " << c1);
auto lemmas = cfl.lemmas();
for (auto& lemma : lemmas) {
for (unsigned i = 0; i < lemma->size(); i++) {
if (s.lit2cnstr(lemma->operator[](i)) == c1)
return;
LOG_H1("Found different constraint " << s.lit2cnstr(lemma->operator[](i)));
}
}
LOG_H1("FAIL: Lemma " << c1 << " not deduced!");
if (!collect_test_records)
VERIFY(false);
}
static void test_elim1(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto c1 = s.eq(7 * x, 3);
auto c2 = s.ule(x - y, 5);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
rational res;
rational(7).mult_inverse(bw, res);
expect_lemma_cnt(cfl, 1);
expect_lemma(s, cfl, s.ule(s.sz2pdd(bw).mk_val(res * 3) - y, 5));
}
static void test_elim2(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto c1 = s.eq(x * x, x * 3);
auto c2 = s.ule(x + y, 5);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 0); // Non linear; should be skipped
}
static void test_elim3(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto c1 = s.eq(7 * x, 3);
auto c2 = s.ule(x * x + y, 5);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 0); // also not linear; should be skipped
}
static void test_elim4(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto c1 = s.eq(7 * x, 3);
auto c2 = s.ule(y * x, 5 + x + y);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 1);
expect_lemma(s, cfl, s.ule(5 * y, 10 + y));
}
static void test_elim5(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto z = s.var(s.add_var(bw));
auto c1 = s.eq(x * 7 + x * y, 3);
auto c2 = s.ule(y * x * z, 2);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 1); // Eliminating "x" fails because there is no assignment for "y"; eliminating "y" works
expect_lemma(s, cfl, s.ule(3 * z - 7 * x * z, 2));
s.assign_core(y.var(), rational(2), justification::propagation(0));
conflict cfl2(s);
cfl2.insert(c1);
cfl2.insert_vars(c1);
cfl2.insert(c2);
cfl2.insert_vars(c2);
elim.find_lemma(cfl2);
expect_lemma_cnt(cfl2, 2); // Now it uses the assignment
expect_lemma(s, cfl2, s.ule(3 * z - 7 * x * z, 2));
expect_lemma(s, cfl2, s.ule(6 * z, 2));
}
static void test_elim6(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto z = s.var(s.add_var(bw));
auto c1 = s.eq(2 * x, z);
auto c2 = s.ule(4 * x, y);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 1); // We have to multiply by 2 so this is an over-approximation (or we would increase bit-width by 1)
expect_lemma(s, cfl, s.ule(2 * z, y));
auto c3 = s.eq(4 * x, z);
auto c4 = s.ule(2 * x, y);
conflict cfl2(s);
s.assign_eh(c3, dependency(0));
cfl2.insert(c3);
s.assign_eh(c4, dependency(0));
cfl2.insert(c4);
elim.find_lemma(cfl2);
expect_lemma_cnt(cfl2, 0); // This does not work because of polarity
}
static void test_elim7(unsigned bw = 32) {
scoped_solver s(__func__);
free_variable_elimination elim(s);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto z = s.var(s.add_var(bw));
auto c1 = s.eq(x * y, 3);
auto c2 = s.ule(z * x, 2);
conflict cfl(s);
s.assign_eh(c1, dependency(0));
cfl.insert(c1);
s.assign_eh(c2, dependency(0));
cfl.insert(c2);
elim.find_lemma(cfl);
expect_lemma_cnt(cfl, 1); // Should introduce polarity constraints
// TODO: Check if this lemma is really correct
}
/**
* x*x <= z
@ -1654,7 +1850,9 @@ static void STD_CALL polysat_on_ctrl_c(int) {
void tst_polysat() {
using namespace polysat;
#if 1 // Enable this block to run a single unit test with detailed output.
polysat::test_polysat::test_elim7(3);
#if 0 // Enable this block to run a single unit test with detailed output.
collect_test_records = false;
test_max_conflicts = 50;
// test_polysat::test_parity1();
@ -1719,6 +1917,14 @@ void tst_polysat() {
RUN(test_polysat::test_var_minimize()); // works but var_minimize isn't used (UNSAT before lemma is created)
RUN(test_polysat::test_elim1());
RUN(test_polysat::test_elim2());
RUN(test_polysat::test_elim3());
RUN(test_polysat::test_elim4());
RUN(test_polysat::test_elim5());
RUN(test_polysat::test_elim6());
RUN(test_polysat::test_elim7());
RUN(test_polysat::test_ineq1());
RUN(test_polysat::test_ineq2());
RUN(test_polysat::test_monot());
@ -1755,7 +1961,7 @@ void tst_polysat() {
RUN(test_polysat::test_ineq_axiom5());
RUN(test_polysat::test_ineq_axiom6());
RUN(test_polysat::test_ineq_non_axiom1());
RUN(test_polysat::test_ineq_non_axiom4());
//RUN(test_polysat::test_ineq_non_axiom4());
// test_fi::exhaustive();
// test_fi::randomized();