mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
allow multiple lemmas during processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
1940f53b31
commit
1c884c8d72
2 changed files with 64 additions and 52 deletions
|
|
@ -32,15 +32,18 @@ namespace polysat {
|
|||
|
||||
saturation::saturation(solver& s) : s(s), m_lemma(s) {}
|
||||
|
||||
void saturation::log_lemma(pvar v, conflict& core) {
|
||||
IF_VERBOSE(1, auto const& cl = core.lemmas().back();
|
||||
verbose_stream() << m_rule << " v" << v << " ";
|
||||
for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " ";
|
||||
verbose_stream() << "\n");
|
||||
}
|
||||
|
||||
void saturation::perform(pvar v, conflict& core) {
|
||||
IF_VERBOSE(2, verbose_stream() << "v" << v << " " << core << "\n");
|
||||
for (auto c : core)
|
||||
if (perform(v, c, core)) {
|
||||
IF_VERBOSE(0, auto const& cl = core.lemmas().back();
|
||||
verbose_stream() << m_rule << " v" << v << " ";
|
||||
for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " ";
|
||||
verbose_stream() << "\n");
|
||||
if (perform(v, c, core))
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) {
|
||||
|
|
@ -60,27 +63,28 @@ namespace polysat {
|
|||
}
|
||||
|
||||
bool saturation::try_inequality(pvar v, inequality const& i, conflict& core) {
|
||||
bool prop = false;
|
||||
if (try_mul_bounds(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_parity(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_parity_diseq(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_transitivity(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_factor_equality(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_ugt_x(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_ugt_y(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_ugt_z(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (try_y_l_ax_and_x_l_z(v, core, i))
|
||||
return true;
|
||||
prop = true;
|
||||
if (false && try_tangent(v, core, i))
|
||||
return true;
|
||||
return false;
|
||||
prop = true;
|
||||
return prop;
|
||||
}
|
||||
|
||||
bool saturation::try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core) {
|
||||
|
|
@ -99,7 +103,7 @@ namespace polysat {
|
|||
// ~ovfl(V,q) => q = 0 or V <= V*q
|
||||
m_lemma.reset();
|
||||
m_lemma.insert_eval(q_eq_0);
|
||||
if (propagate(core, c, s.ule(p, p * q)))
|
||||
if (propagate(v, core, c, s.ule(p, p * q)))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
@ -113,11 +117,11 @@ namespace polysat {
|
|||
return s.ule(lhs, rhs);
|
||||
}
|
||||
|
||||
bool saturation::propagate(conflict& core, inequality const& crit, signed_constraint c) {
|
||||
return propagate(core, crit.as_signed_constraint(), c);
|
||||
bool saturation::propagate(pvar v, conflict& core, inequality const& crit, signed_constraint c) {
|
||||
return propagate(v, core, crit.as_signed_constraint(), c);
|
||||
}
|
||||
|
||||
bool saturation::propagate(conflict& core, signed_constraint const& crit, signed_constraint c) {
|
||||
bool saturation::propagate(pvar v, conflict& core, signed_constraint const& crit, signed_constraint c) {
|
||||
if (is_forced_true(c))
|
||||
return false;
|
||||
|
||||
|
|
@ -137,23 +141,19 @@ namespace polysat {
|
|||
|
||||
m_lemma.insert(~crit);
|
||||
|
||||
IF_VERBOSE(10, verbose_stream() << "propagate " << m_rule << " ";
|
||||
for (auto lit : m_lemma) verbose_stream() << s.lit2cnstr(lit) << " ";
|
||||
verbose_stream() << c << "\n";
|
||||
);
|
||||
|
||||
SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); }));
|
||||
|
||||
m_lemma.insert(c);
|
||||
core.add_lemma(m_rule, m_lemma.build());
|
||||
log_lemma(v, core);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool saturation::add_conflict(conflict& core, inequality const& crit1, signed_constraint c) {
|
||||
return add_conflict(core, crit1, crit1, c);
|
||||
bool saturation::add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c) {
|
||||
return add_conflict(v, core, crit1, crit1, c);
|
||||
}
|
||||
|
||||
bool saturation::add_conflict(conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint const c) {
|
||||
bool saturation::add_conflict(pvar v, conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint const c) {
|
||||
auto crit1 = _crit1.as_signed_constraint();
|
||||
auto crit2 = _crit2.as_signed_constraint();
|
||||
m_lemma.insert(~crit1);
|
||||
|
|
@ -175,6 +175,7 @@ namespace polysat {
|
|||
|
||||
m_lemma.insert_eval(c);
|
||||
core.add_lemma(m_rule, m_lemma.build());
|
||||
log_lemma(v, core);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -424,7 +425,7 @@ namespace polysat {
|
|||
m_lemma.insert_eval(~non_ovfl);
|
||||
if (!xy_l_xz.is_strict())
|
||||
m_lemma.insert_eval(s.eq(x));
|
||||
return add_conflict(core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z));
|
||||
return add_conflict(v, core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -465,7 +466,7 @@ namespace polysat {
|
|||
pdd const& z_prime = l_y.lhs();
|
||||
m_lemma.reset();
|
||||
m_lemma.insert_eval(~non_ovfl);
|
||||
return add_conflict(core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
|
||||
return add_conflict(v, core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -505,7 +506,7 @@ namespace polysat {
|
|||
return false;
|
||||
m_lemma.reset();
|
||||
m_lemma.insert_eval(~non_ovfl);
|
||||
return add_conflict(core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x));
|
||||
return add_conflict(z, core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -546,7 +547,7 @@ namespace polysat {
|
|||
return false;
|
||||
m_lemma.reset();
|
||||
m_lemma.insert_eval(~non_ovfl);
|
||||
return add_conflict(core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z));
|
||||
return add_conflict(x, core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -584,7 +585,7 @@ namespace polysat {
|
|||
m_lemma.insert_eval(~s.eq(y));
|
||||
m_lemma.insert_eval(x_eq_0);
|
||||
m_lemma.insert_eval(a_eq_0);
|
||||
return propagate(core, axb_l_y, c);
|
||||
return propagate(x, core, axb_l_y, c);
|
||||
};
|
||||
|
||||
auto prop2 = [&](signed_constraint ante, signed_constraint c) {
|
||||
|
|
@ -594,7 +595,7 @@ namespace polysat {
|
|||
m_lemma.insert_eval(x_eq_0);
|
||||
m_lemma.insert_eval(a_eq_0);
|
||||
m_lemma.insert_eval(~ante);
|
||||
return propagate(core, axb_l_y, c);
|
||||
return propagate(x, core, axb_l_y, c);
|
||||
};
|
||||
|
||||
pdd minus_a = -a;
|
||||
|
|
@ -672,9 +673,9 @@ namespace polysat {
|
|||
m_lemma.insert_eval(~s.eq(b, rational(-1)));
|
||||
m_lemma.insert_eval(~s.eq(y));
|
||||
m_lemma.insert_eval(~non_ovfl);
|
||||
if (propagate(core, axb_l_y, s.eq(X, 1)))
|
||||
if (propagate(x, core, axb_l_y, s.eq(X, 1)))
|
||||
return true;
|
||||
if (propagate(core, axb_l_y, s.eq(a, 1)))
|
||||
if (propagate(x, core, axb_l_y, s.eq(a, 1)))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
|
@ -725,7 +726,7 @@ namespace polysat {
|
|||
m_lemma.reset();
|
||||
m_lemma.insert_eval(~s.eq(y));
|
||||
m_lemma.insert_eval(~premise);
|
||||
return propagate(core, axb_l_y, conseq);
|
||||
return propagate(x, core, axb_l_y, conseq);
|
||||
};
|
||||
|
||||
auto propagate2 = [&](signed_constraint premise1, signed_constraint premise2, signed_constraint conseq) {
|
||||
|
|
@ -733,7 +734,7 @@ namespace polysat {
|
|||
m_lemma.insert_eval(~s.eq(y));
|
||||
m_lemma.insert_eval(~premise1);
|
||||
m_lemma.insert_eval(~premise2);
|
||||
return propagate(core, axb_l_y, conseq);
|
||||
return propagate(x, core, axb_l_y, conseq);
|
||||
};
|
||||
#if 0
|
||||
LOG_H1("try_parity: " << X << " on: " << lit_pp(s, axb_l_y.as_signed_constraint()));
|
||||
|
|
@ -831,7 +832,7 @@ namespace polysat {
|
|||
m_lemma.reset();
|
||||
m_lemma.insert_eval(~s.eq(y));
|
||||
m_lemma.insert_eval(~s.eq(b));
|
||||
return propagate(core, axb_l_y, ~s.parity(X, N - k));
|
||||
return propagate(x, core, axb_l_y, ~s.parity(X, N - k));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -856,12 +857,12 @@ namespace polysat {
|
|||
m_lemma.insert_eval(s.eq(y));
|
||||
m_lemma.insert_eval(~s.eq(b));
|
||||
m_lemma.insert_eval(a_eq_0);
|
||||
if (propagate(core, axb_l_y, s.even(X)))
|
||||
if (propagate(x, core, axb_l_y, s.even(X)))
|
||||
return true;
|
||||
if (!is_forced_diseq(X, 0, x_eq_0))
|
||||
return false;
|
||||
m_lemma.insert_eval(x_eq_0);
|
||||
if (propagate(core, axb_l_y, s.even(a)))
|
||||
if (propagate(x, core, axb_l_y, s.even(a)))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
|
@ -895,7 +896,7 @@ namespace polysat {
|
|||
m_lemma.insert_eval(~s.eq(b, 1));
|
||||
m_lemma.insert(~c);
|
||||
auto ineq = i.is_strict() || a_l_b.is_strict() ? s.ult(q, p) : s.ule(q, p);
|
||||
if (propagate(core, a_l_b, ineq))
|
||||
if (propagate(x, core, a_l_b, ineq))
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -923,6 +924,8 @@ namespace polysat {
|
|||
|
||||
if (!is_axb_l_y && !is_y_l_axb)
|
||||
return false;
|
||||
|
||||
bool factored = false;
|
||||
|
||||
for (auto c : core) {
|
||||
if (!c->is_ule())
|
||||
|
|
@ -942,6 +945,10 @@ namespace polysat {
|
|||
change = true;
|
||||
lhs = b1 - b3;
|
||||
}
|
||||
else if (is_axb_l_y && a1 == -a3) {
|
||||
change = true;
|
||||
lhs = b1 + b3;
|
||||
}
|
||||
else if (is_axb_l_y && a3.is_val() && a3.val().is_odd()) {
|
||||
// a3*x + b3 == 0
|
||||
// a3 is odd => x = inverse(a3)*-b3
|
||||
|
|
@ -954,6 +961,10 @@ namespace polysat {
|
|||
change = true;
|
||||
rhs = b2 - b3;
|
||||
}
|
||||
else if (is_y_l_axb && a2 == -a3) {
|
||||
change = true;
|
||||
rhs = b2 + b3;
|
||||
}
|
||||
else if (is_y_l_axb && a3.is_val() && a3.val().is_odd()) {
|
||||
change = true;
|
||||
rational a3_inv;
|
||||
|
|
@ -968,10 +979,10 @@ namespace polysat {
|
|||
m_lemma.reset();
|
||||
m_lemma.insert(~s.eq(y3));
|
||||
m_lemma.insert(~c);
|
||||
if (propagate(core, a_l_b, conseq))
|
||||
return true;
|
||||
if (propagate(x, core, a_l_b, conseq))
|
||||
factored = true;
|
||||
}
|
||||
return false;
|
||||
return factored;
|
||||
}
|
||||
/*
|
||||
* TODO
|
||||
|
|
@ -1031,7 +1042,7 @@ namespace polysat {
|
|||
return false;
|
||||
m_lemma.insert_eval(~d);
|
||||
auto conseq = s.ult(r_val, c.rhs());
|
||||
return add_conflict(core, c, conseq);
|
||||
return add_conflict(v, core, c, conseq);
|
||||
}
|
||||
else {
|
||||
auto d = s.ule(c.rhs(), r_val);
|
||||
|
|
@ -1039,7 +1050,7 @@ namespace polysat {
|
|||
return false;
|
||||
m_lemma.insert_eval(~d);
|
||||
auto conseq = s.ule(c.lhs(), r_val);
|
||||
return add_conflict(core, c, conseq);
|
||||
return add_conflict(v, core, c, conseq);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -31,10 +31,11 @@ namespace polysat {
|
|||
bool is_non_overflow(pdd const& x, pdd const& y, signed_constraint& c);
|
||||
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
|
||||
|
||||
bool propagate(conflict& core, signed_constraint const& crit1, signed_constraint c);
|
||||
bool propagate(conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool add_conflict(conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool add_conflict(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
|
||||
void log_lemma(pvar v, conflict& core);
|
||||
bool propagate(pvar v, conflict& core, signed_constraint const& crit1, signed_constraint c);
|
||||
bool propagate(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool add_conflict(pvar v, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
|
||||
|
||||
bool try_ugt_x(pvar v, conflict& core, inequality const& c);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue