mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Update saturation inferences

Browse source
This commit is contained in:
Jakob Rath 2022-11-28 18:02:18 +01:00
parent 7468b2326c
commit 3d79cddf33
4 changed files with 226 additions and 342 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -57,7 +57,7 @@ TODO:
namespace polysat { namespace polysat {
class conflict_resolver { class conflict_resolver {
inf_saturate m_saturate; saturation m_saturate;
ex_polynomial_superposition m_poly_sup; ex_polynomial_superposition m_poly_sup;
free_variable_elimination m_free_variable_elimination; free_variable_elimination m_free_variable_elimination;

516
src/math/polysat/saturation.cpp
View file

@ -28,279 +28,166 @@ TODO: when we check that 'x' is "unary":
#include "math/polysat/log.h" #include "math/polysat/log.h"
namespace polysat { namespace polysat {
bool inf_saturate::perform(pvar v, conflict& core) { saturation::saturation(solver& s) : s(s), m_lemma(s) {}
for (auto c1 : core) {
if (!c1->is_ule()) bool saturation::perform(pvar v, conflict& core) {
for (auto c : core) {
if (!c->is_ule())
continue; continue;
if (c1.is_currently_true(s)) if (c.is_currently_true(s))
continue; continue;
auto c = c1.as_inequality(); auto i = inequality::from_ule(c);
if (try_ugt_x(v, core, c)) if (try_ugt_x(v, core, i))
return true; return true;
if (try_ugt_y(v, core, c)) if (try_ugt_y(v, core, i))
return true; return true;
if (try_ugt_z(v, core, c)) if (try_ugt_z(v, core, i))
return true; return true;
if (try_y_l_ax_and_x_l_z(v, core, c)) if (try_y_l_ax_and_x_l_z(v, core, i))
return true; return true;
if (try_tangent(v, core, c)) if (try_tangent(v, core, i))
return true; return true;
} }
return false; return false;
} }
signed_constraint inf_saturate::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) { signed_constraint saturation::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
if (is_strict) if (is_strict)
return s.ult(lhs, rhs); return s.ult(lhs, rhs);
else else
return s.ule(lhs, rhs); return s.ule(lhs, rhs);
} }
/** bool saturation::propagate(conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint const c) {
* Propagate c. It is added to reason and core all other literals in reason are false in current stack.
* The lemmas outlined in the rules are valid and therefore c is implied.
*/
bool inf_saturate::propagate(char const* inf_name, conflict& core, inequality const& _crit1, inequality const& _crit2, signed_constraint& c) {
auto crit1 = _crit1.as_signed_constraint(); auto crit1 = _crit1.as_signed_constraint();
auto crit2 = _crit2.as_signed_constraint(); auto crit2 = _crit2.as_signed_constraint();
m_new_constraints.push_back(crit1); m_lemma.insert(~crit1);
m_new_constraints.push_back(crit2); if (crit1 != crit2)
SASSERT(!crit1.is_currently_true(s)); m_lemma.insert(~crit2);
LOG("critical " << m_rule << " " << crit1); LOG("critical " << m_rule << " " << crit1);
LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c)); LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s));
// ensure new core is a conflict SASSERT(all_of(m_lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
// TODO: don't we need to check the m_new_constraints too? or maybe that is implicit in the rules (should check it)
if (!c.is_currently_false(s) && c.bvalue(s) != l_false) // Ensure lemma is a conflict lemma
if (c.bvalue(s) != l_false && !c.is_currently_false(s))
return false; return false;
if (c.bvalue(s) == l_true) // TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs.
return false; // if (c.bvalue(s) == l_true)
// return false;
SASSERT(c.bvalue(s) != l_true);
// avoid loops m_lemma.insert(c);
// NOTE: core.add_lemma(m_lemma.build()); // TODO: log with name m_rule
// it is not enough to only check whether ~c is already in the core. return true;
// One example had c: 0 != 0, so c was ignored when inserting it to the core.
// (But the side conditions in m_new_constraints were useful.)
bool inserting = false;
if (!c.is_always_false() && !core.contains(~c))
inserting = true;
else
for (auto d : m_new_constraints)
if (!d.is_always_true() && !core.contains(d)) {
inserting = true;
break;
}
if (!inserting)
return false;
// TODO: add as a side lemma instead of changing the conflict
core.remove_all();
for (auto d : m_new_constraints)
core.insert_eval(d);
if (c.bvalue(s) != l_false) // conflict is due to the evaluation of c, so it depends on the variable values
core.insert_vars(c);
core.insert_eval(~c);
core.logger().log(inf_name);
LOG("Core " << core);
return true;
} }
bool inf_saturate::propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs) { bool saturation::propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs) {
signed_constraint c = ineq(is_strict, lhs, rhs); signed_constraint c = ineq(is_strict, lhs, rhs);
return propagate(inf_name, core, crit1, crit2, c); return propagate(core, crit1, crit2, c);
} }
/// Add premises for Ω*(x, y) void saturation::insert_omega(pdd const& x, pdd const& y) {
void inf_saturate::push_omega_bisect(pdd const& x, rational x_max, pdd const& y, rational y_max) { m_lemma.insert(s.umul_ovfl(x, y));
rational x_val, y_val;
auto& pddm = x.manager();
rational bound = pddm.max_value();
VERIFY(s.try_eval(x, x_val));
VERIFY(s.try_eval(y, y_val));
SASSERT(x_val * y_val <= bound);
rational x_lo = x_val, x_hi = x_max, y_lo = y_val, y_hi = y_max;
SASSERT(x_lo <= x_hi && y_lo <= y_hi);
rational two(2);
while (x_lo < x_hi || y_lo < y_hi) {
rational x_mid = div(x_hi + x_lo + 1, two);
rational y_mid = div(y_hi + y_lo + 1, two);
if (x_mid * y_mid > bound) {
x_hi = x_lo < x_hi ? x_mid - 1 : x_lo;
y_hi = y_lo < y_hi ? y_mid - 1 : y_lo;
}
else
x_lo = x_mid, y_lo = y_mid;
}
SASSERT(x_hi == x_lo && y_hi == y_lo);
SASSERT(x_lo * y_lo <= bound);
SASSERT((x_lo + 1) * (y_lo + 1) > bound);
if ((x_lo + 1) * y_lo <= bound) {
x_hi = x_max;
while (x_lo < x_hi) {
rational x_mid = div(x_hi + x_lo + 1, two);
if (x_mid * y_lo > bound)
x_hi = x_mid - 1;
else
x_lo = x_mid;
}
}
else if (x_lo * (y_lo + 1) <= bound) {
y_hi = y_max;
while (y_lo < y_hi) {
rational y_mid = div(y_hi + y_lo + 1, two);
if (y_mid * x_lo > bound)
y_hi = y_mid - 1;
else
y_lo = y_mid;
}
}
SASSERT(x_lo * y_lo <= bound);
SASSERT((x_lo + 1) * y_lo > bound || x_val == x_max);
SASSERT(x_lo * (y_lo + 1) > bound || y_val == y_max);
// inequalities are justified by current assignments to x, y
// conflict resolution should be able to pick up this as a valid justification.
// or we resort to the same extension as in the original mul_overflow code
// where we add explicit equality propagations from the current assignment.
auto c1 = s.ule(x, pddm.mk_val(x_lo));
auto c2 = s.ule(y, pddm.mk_val(y_lo));
m_new_constraints.insert(c1);
m_new_constraints.insert(c2);
LOG("bounded " << bound << " : " << x << " " << x_max << " " << y << " " << y_max << " " << c1 << " " << c2);
}
rational inf_saturate::max_value(pdd const& x) {
if (x.is_var())
return s.m_viable.max_viable(x.var());
else if (x.is_val())
return x.val();
else
return x.manager().max_value();
}
void inf_saturate::push_omega(pdd const& x, pdd const& y) {
m_new_constraints.insert(~s.umul_ovfl(x, y));
/*
// determine worst case upper bounds for x, y
// then extract premises for a non-worst-case bound.
auto& pddm = x.manager();
rational x_max = max_value(x);
rational y_max = max_value(y);
LOG("pushing " << x << " " << y);
if (x_max * y_max > pddm.max_value())
push_omega_bisect(x, x_max, y, y_max);
else {
for (auto const& c : s.m_viable.get_constraints(y.var()))
m_new_constraints.insert(c);
for (auto const& c : s.m_viable.get_constraints(x.var()))
m_new_constraints.insert(c);
}
*/
} }
/* /*
* Match [v] .. <= v * Match [v] .. <= v
*/ */
bool inf_saturate::is_l_v(pvar v, inequality const& i) { bool saturation::is_l_v(pvar v, inequality const& i) {
return i.rhs == s.var(v); return i.rhs() == s.var(v);
} }
/* /*
* Match [v] v <= ... * Match [v] v <= ...
*/ */
bool inf_saturate::is_g_v(pvar v, inequality const& i) { bool saturation::is_g_v(pvar v, inequality const& i) {
return i.lhs == s.var(v); return i.lhs() == s.var(v);
} }
/* /*
* Match [x] x <= y * Match [x] x <= y
*/ */
bool inf_saturate::is_x_l_Y(pvar x, inequality const& c, pdd& y) { bool saturation::is_x_l_Y(pvar x, inequality const& i, pdd& y) {
y = c.rhs; y = i.rhs();
return is_g_v(x, c); return is_g_v(x, i);
} }
/* /*
* Match [x] y <= a*x * Match [x] y <= a*x
*/ */
bool inf_saturate::is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y) { bool saturation::is_Y_l_Ax(pvar x, inequality const& i, pdd& a, pdd& y) {
y = d.lhs; y = i.lhs();
return is_xY(x, d.rhs, a); return is_xY(x, i.rhs(), a);
} }
bool inf_saturate::verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y) { bool saturation::verify_Y_l_Ax(pvar x, inequality const& i, pdd const& a, pdd const& y) {
return d.lhs == y && d.rhs == a * s.var(x); return i.lhs() == y && i.rhs() == a * s.var(x);
} }
/** /**
* Match [coeff*x] coeff*x*Y * Match [coeff*x] coeff*x*Y where x is a variable
*/ */
bool saturation::is_coeffxY(pdd const& x, pdd const& p, pdd& y) {
bool inf_saturate::is_coeffxY(pdd const& x, pdd const& p, pdd& y) { pdd xy = x.manager().zero();
pdd xy = x;
return x.is_unary() && p.try_div(x.hi().val(), xy) && xy.factor(x.var(), 1, y); return x.is_unary() && p.try_div(x.hi().val(), xy) && xy.factor(x.var(), 1, y);
} }
/** /**
* determine whether values of x * y is non-overflowing. * Determine whether values of x * y is non-overflowing.
*/ */
bool inf_saturate::is_non_overflow(pdd const& x, pdd const& y) { bool saturation::is_non_overflow(pdd const& x, pdd const& y) {
rational x_val, y_val; rational x_val, y_val;
auto& pddm = x.manager(); rational bound = x.manager().two_to_N();
rational bound = rational::power_of_two(pddm.power_of_2()); return s.try_eval(x, x_val) && s.try_eval(y, y_val) && x_val * y_val < bound;
return s.try_eval(x, x_val) && s.try_eval(y, y_val) && x_val * y_val < bound;
} }
/** /**
* Match [v] v*x <= z*x with x a variable * Match [v] v*x <= z*x with x a variable
*/ */
bool inf_saturate::is_Xy_l_XZ(pvar v, inequality const& c, pdd& x, pdd& z) { bool saturation::is_Xy_l_XZ(pvar v, inequality const& i, pdd& x, pdd& z) {
return is_xY(v, c.lhs, x) && is_coeffxY(x, c.rhs, z); return is_xY(v, i.lhs(), x) && is_coeffxY(x, i.rhs(), z);
} }
bool inf_saturate::verify_Xy_l_XZ(pvar v, inequality const& c, pdd const& x, pdd const& z) { bool saturation::verify_Xy_l_XZ(pvar v, inequality const& i, pdd const& x, pdd const& z) {
return c.lhs == s.var(v) * x && c.rhs == z * x; return i.lhs() == s.var(v) * x && i.rhs() == z * x;
} }
/** /**
* Match [z] yx <= zx with x a variable * Match [z] yx <= zx with x a variable
*/ */
bool inf_saturate::is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y) { bool saturation::is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y) {
return is_xY(z, c.rhs, x) && is_coeffxY(x, c.lhs, y); return is_xY(z, c.rhs(), x) && is_coeffxY(x, c.lhs(), y);
} }
bool inf_saturate::verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y) { bool saturation::verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y) {
return c.lhs == y * x && c.rhs == s.var(z) * x; return c.lhs() == y * x && c.rhs() == s.var(z) * x;
} }
/** /**
* Match [x] xY <= xZ * Match [x] xY <= xZ
*/ */
bool inf_saturate::is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z) { bool saturation::is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z) {
return is_xY(x, c.lhs, y) && is_xY(x, c.rhs, z); return is_xY(x, c.lhs(), y) && is_xY(x, c.rhs(), z);
} }
/** /**
* Match xy = x * Y * Match xy = x * Y
*/ */
bool inf_saturate::is_xY(pvar x, pdd const& xy, pdd& y) { bool saturation::is_xY(pvar x, pdd const& xy, pdd& y) {
return xy.degree(x) == 1 && xy.factor(x, 1, y); return xy.degree(x) == 1 && xy.factor(x, 1, y);
} }
/** /**
* Implement the inferences * Implement the inferences
* [x] zx > yx ==> Ω*(x,y) \/ z > y * [x] yx < zx ==> Ω*(x,y) \/ y < z
* [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0 * [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0
*/ */
bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& xy_l_xz) { bool saturation::try_ugt_x(pvar v, conflict& core, inequality const& xy_l_xz) {
set_rule("zx <= yx"); set_rule("[x] yx <= zx");
pdd x = s.var(v); pdd x = s.var(v);
pdd y = x; pdd y = x;
pdd z = x; pdd z = x;
@ -308,34 +195,26 @@ namespace polysat {
return false; return false;
if (!is_non_overflow(x, y)) if (!is_non_overflow(x, y))
return false; return false;
if (!xy_l_xz.is_strict && s.get_value(v).is_zero()) if (!xy_l_xz.is_strict() && s.get_value(v).is_zero())
return false; return false;
m_lemma.reset();
m_new_constraints.reset(); insert_omega(x, y);
if (!xy_l_xz.is_strict) if (!xy_l_xz.is_strict())
m_new_constraints.push_back(~s.eq(x)); m_lemma.insert_eval(s.eq(x));
push_omega(x, y); return propagate(core, xy_l_xz, xy_l_xz, xy_l_xz.is_strict(), y, z);
return propagate("ugt_x", core, xy_l_xz, xy_l_xz, xy_l_xz.is_strict, y, z);
} }
/// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x /**
/// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx * [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) { * [y] z' <= y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx
SASSERT(is_l_v(v, le_y)); * [y] z' < y /\ yx <= zx ==> Ω*(x,y) \/ z'x < zx
SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z)); * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx TODO: could strengthen the conclusion to z'x + 1 < zx
pdd const y = s.var(v); */
if (!is_non_overflow(x, y)) bool saturation::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) {
return false;
pdd const& z_prime = le_y.lhs;
m_new_constraints.reset();
push_omega(x, y);
return propagate("ugt_y", core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x);
}
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) {
set_rule("[y] z' <= y & yx <= zx"); set_rule("[y] z' <= y & yx <= zx");
pdd x = s.var(v); auto& m = s.var2pdd(v);
pdd z = x; pdd x = m.zero();
pdd z = m.zero();
if (!is_Xy_l_XZ(v, yx_l_zx, x, z)) if (!is_Xy_l_XZ(v, yx_l_zx, x, z))
return false; return false;
for (auto si : s.m_search) { for (auto si : s.m_search) {
@ -343,23 +222,77 @@ namespace polysat {
continue; continue;
if (si.is_resolved()) if (si.is_resolved())
continue; continue;
auto dd = s.lit2cnstr(si.lit()); auto d = s.lit2cnstr(si.lit());
if (!dd->is_ule()) if (!d->is_ule())
continue; continue;
auto le_y = dd.as_inequality(); auto l_y = inequality::from_ule(d);
if (is_l_v(v, le_y) && try_ugt_y(v, core, le_y, yx_l_zx, x, z)) if (is_l_v(v, l_y) && try_ugt_y(v, core, l_y, yx_l_zx, x, z))
return true; return true;
} }
return false; return false;
} }
bool saturation::try_ugt_y(pvar v, conflict& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
SASSERT(is_l_v(v, l_y));
SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z));
pdd const y = s.var(v);
if (!is_non_overflow(x, y))
return false;
pdd const& z_prime = l_y.lhs();
m_lemma.reset();
insert_omega(x, y);
return propagate(core, l_y, yx_l_zx, yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x);
}
/// [x] y <= ax /\ x <= z (non-overflow case) /**
/// ==> Ω*(a, z) \/ y <= az * [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax) { * [z] z <= y' /\ yx < zx ==> Ω*(x,y') \/ yx < y'x
* [z] z < y' /\ yx <= zx ==> Ω*(x,y') \/ yx < y'x
* [z] z < y' /\ yx < zx ==> Ω*(x,y') \/ yx < y'x TODO: could strengthen the conclusion to yx + 1 < y'x
*/
bool saturation::try_ugt_z(pvar z, conflict& core, inequality const& yx_l_zx) {
set_rule("[z] z <= y' && yx <= zx");
auto& m = s.var2pdd(z);
pdd y = m.zero();
pdd x = m.zero();
if (!is_YX_l_zX(z, yx_l_zx, x, y))
return false;
for (auto si : s.m_search) {
if (!si.is_boolean())
continue;
if (si.is_resolved())
continue;
auto d = s.lit2cnstr(si.lit());
if (!d->is_ule())
continue;
auto z_l_y = inequality::from_ule(d);
if (is_g_v(z, z_l_y) && try_ugt_z(z, core, z_l_y, yx_l_zx, x, y))
return true;
}
return false;
}
bool saturation::try_ugt_z(pvar z, conflict& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
SASSERT(is_g_v(z, z_l_y));
SASSERT(verify_YX_l_zX(z, yx_l_zx, x, y));
pdd const& y_prime = z_l_y.rhs();
if (!is_non_overflow(x, y_prime))
return false;
m_lemma.reset();
insert_omega(x, y_prime);
return propagate(core, yx_l_zx, z_l_y, z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x);
}
/**
* [x] y <= ax /\ x <= z (non-overflow case)
* ==> Ω*(a, z) \/ y <= az
* ... (other combinations of <, <=)
*/
bool saturation::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax) {
set_rule("[x] y <= ax & x <= z"); set_rule("[x] y <= ax & x <= z");
pdd y = s.var(x); auto& m = s.var2pdd(x);
pdd a = y; pdd y = m.zero();
pdd a = m.zero();
if (!is_Y_l_Ax(x, y_l_ax, a, y)) if (!is_Y_l_Ax(x, y_l_ax, a, y))
return false; return false;
if (a.is_one()) if (a.is_one())
@ -369,89 +302,55 @@ namespace polysat {
continue; continue;
if (si.is_resolved()) if (si.is_resolved())
continue; continue;
auto dd = s.lit2cnstr(si.lit()); auto d = s.lit2cnstr(si.lit());
if (!dd->is_ule()) if (!d->is_ule())
continue; continue;
auto x_l_z = dd.as_inequality(); auto x_l_z = inequality::from_ule(d);
if (is_g_v(x, x_l_z) && try_y_l_ax_and_x_l_z(x, core, y_l_ax, x_l_z, a, y)) if (is_g_v(x, x_l_z) && try_y_l_ax_and_x_l_z(x, core, y_l_ax, x_l_z, a, y))
return true; return true;
} }
return false; return false;
} }
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax, inequality const& x_l_z, pdd const& a, pdd const& y) { bool saturation::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax, inequality const& x_l_z, pdd const& a, pdd const& y) {
SASSERT(is_g_v(x, x_l_z)); SASSERT(is_g_v(x, x_l_z));
SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y)); SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
pdd z = x_l_z.rhs; pdd const& z = x_l_z.rhs();
if (!is_non_overflow(a, z)) if (!is_non_overflow(a, z))
return false; return false;
m_new_constraints.reset(); m_lemma.reset();
push_omega(a, z); insert_omega(a, z);
return propagate("y_l_ax_and_x_l_z", core, y_l_ax, x_l_z, x_l_z.is_strict || y_l_ax.is_strict, y, a * z); return propagate(core, y_l_ax, x_l_z, x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z);
} }
/**
/// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx * [x] p(x) <= q(x) where value(p) > value(q)
/// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x * ==> q <= value(q) => p <= value(q)
bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& yx_l_zx) { *
set_rule("[z] z <= y' && zx > yx"); * for strict?
pdd y = s.var(z); * p(x) < q(x) where value(p) >= value(q)
pdd x = y; * ==> value(p) <= p => value(p) < q
if (!is_YX_l_zX(z, yx_l_zx, x, y)) */
return false; bool saturation::try_tangent(pvar v, conflict& core, inequality const& c) {
for (auto si : s.m_search) {
if (!si.is_boolean())
continue;
if (si.is_resolved())
continue;
auto dd = s.lit2cnstr(si.lit());
if (!dd->is_ule())
continue;
auto z_l_y = dd.as_inequality();
if (is_g_v(z, z_l_y) && try_ugt_z(z, core, z_l_y, yx_l_zx, x, y))
return true;
}
return false;
}
bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
SASSERT(is_g_v(z, z_l_y));
SASSERT(verify_YX_l_zX(z, yx_l_zx, x, y));
pdd const& y_prime = z_l_y.rhs;
if (!is_non_overflow(x, y_prime))
return false;
m_new_constraints.reset();
push_omega(x, y_prime);
// yx <= y'x
return propagate("ugt_z", core, yx_l_zx, z_l_y, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x);
}
// [x] p(x) <= q(x) where value(p) > value(q)
// ==> q <= value(q) => p <= value(q)
//
// for strict?
// p(x) < q(x) where value(p) >= value(q)
// ==> value(p) <= p => value(p) < q
bool inf_saturate::try_tangent(pvar v, conflict& core, inequality const& c) {
set_rule("[x] p(x) <= q(x) where value(p) > value(q)"); set_rule("[x] p(x) <= q(x) where value(p) > value(q)");
if (c.is_strict) // if (c.is_strict())
// return false;
if (!c.as_signed_constraint()->contains_var(v))
return false; return false;
if (!c.src->contains_var(v)) if (c.lhs().is_val() || c.rhs().is_val())
return false;
if (c.lhs.is_val() || c.rhs.is_val())
return false; return false;
pdd q_l(c.lhs), e_l(c.lhs), q_r(c.rhs), e_r(c.rhs); auto& m = s.var2pdd(v);
pdd q_l(m), e_l(m), q_r(m), e_r(m);
bool is_linear = true; bool is_linear = true;
is_linear &= c.lhs.degree(v) <= 1; is_linear &= c.lhs().degree(v) <= 1;
is_linear &= c.rhs.degree(v) <= 1; is_linear &= c.rhs().degree(v) <= 1;
if (c.lhs.degree(v) == 1) { if (c.lhs().degree(v) == 1) {
c.lhs.factor(v, 1, q_l, e_l); c.lhs().factor(v, 1, q_l, e_l);
is_linear &= q_l.is_val(); is_linear &= q_l.is_val();
} }
if (c.rhs.degree(v) == 1) { if (c.rhs().degree(v) == 1) {
c.rhs.factor(v, 1, q_r, e_r); c.rhs().factor(v, 1, q_r, e_r);
is_linear &= q_r.is_val(); is_linear &= q_r.is_val();
} }
if (is_linear) if (is_linear)
@ -460,29 +359,28 @@ namespace polysat {
if (!c.as_signed_constraint().is_currently_false(s)) if (!c.as_signed_constraint().is_currently_false(s))
return false; return false;
rational l_val, r_val; rational l_val, r_val;
if (!s.try_eval(c.lhs, l_val)) if (!s.try_eval(c.lhs(), l_val))
return false; return false;
if (!s.try_eval(c.rhs, r_val)) if (!s.try_eval(c.rhs(), r_val))
return false; return false;
SASSERT(c.is_strict || l_val > r_val); SASSERT(c.is_strict() || l_val > r_val);
SASSERT(!c.is_strict || l_val >= r_val); SASSERT(!c.is_strict() || l_val >= r_val);
m_new_constraints.reset(); m_lemma.reset();
m_new_constraints.push_back(c.as_signed_constraint()); if (c.is_strict()) {
if (c.is_strict) { auto d = s.ule(l_val, c.lhs());
auto d = s.ule(l_val, c.lhs);
if (d.bvalue(s) == l_false) // it is a different value conflict that contains v if (d.bvalue(s) == l_false) // it is a different value conflict that contains v
return false; return false;
m_new_constraints.push_back(d); m_lemma.insert_eval(~d);
auto conseq = s.ult(r_val, c.rhs); auto conseq = s.ult(r_val, c.rhs());
return propagate("tangent (strict)", core, c, c, conseq); return propagate(core, c, c, conseq);
} }
else { else {
auto d = s.ule(c.rhs, r_val); auto d = s.ule(c.rhs(), r_val);
if (d.bvalue(s) == l_false) // it is a different value conflict that contains v if (d.bvalue(s) == l_false) // it is a different value conflict that contains v
return false; return false;
m_new_constraints.push_back(d); m_lemma.insert_eval(~d);
auto conseq = s.ule(c.lhs, r_val); auto conseq = s.ule(c.lhs(), r_val);
return propagate("tangent (non-strict)", core, c, c, conseq); return propagate(core, c, c, conseq);
} }
} }

48
src/math/polysat/saturation.h
View file

@ -12,38 +12,26 @@ Author:
--*/ --*/
#pragma once #pragma once
#include "math/polysat/clause_builder.h"
#include "math/polysat/conflict.h" #include "math/polysat/conflict.h"
namespace polysat { namespace polysat {
class solver; /**
* Introduce lemmas that derive new (simpler) constraints from the current conflict and partial model.
*/
class saturation {
class inference_engine {
friend class conflict;
protected:
solver& s; solver& s;
public: clause_builder m_lemma;
inference_engine(solver& s) :s(s) {}
virtual ~inference_engine() {}
/** Try to apply an inference rule.
* Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
* Returns true if a new constraint was added to the core.
*/
virtual bool perform(pvar v, conflict& core) = 0;
};
class inf_saturate : public inference_engine {
vector<signed_constraint> m_new_constraints;
char const* m_rule = nullptr; char const* m_rule = nullptr;
void set_rule(char const* r) { m_rule = r; } void set_rule(char const* r) { m_rule = r; }
void push_omega(pdd const& x, pdd const& y); void insert_omega(pdd const& x, pdd const& y);
void push_omega_bisect(pdd const& x, rational x_max, pdd const& y, rational y_max);
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs); signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c); bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs); bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs);
bool try_ugt_x(pvar v, conflict& core, inequality const& c); bool try_ugt_x(pvar v, conflict& core, inequality const& c);
@ -52,14 +40,14 @@ namespace polysat {
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c); bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y); bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
bool try_ugt_z(pvar z, conflict& core, inequality const& c); bool try_ugt_z(pvar z, conflict& core, inequality const& c);
bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x); bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
bool try_tangent(pvar v, conflict& core, inequality const& c); bool try_tangent(pvar v, conflict& core, inequality const& c);
// c := lhs ~ v // c := lhs ~ v
// where ~ is < or <= // where ~ is < or <=
bool is_l_v(pvar v, inequality const& c); bool is_l_v(pvar v, inequality const& c);
// c := v ~ rhs // c := v ~ rhs
@ -74,11 +62,11 @@ namespace polysat {
// c := Y ~ Ax // c := Y ~ Ax
bool is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y); bool is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y);
bool verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y); bool verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y);
// c := Y*X ~ z*X // c := Y*X ~ z*X
bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y); bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);
bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y); bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y);
// c := xY <= xZ // c := xY <= xZ
bool is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z); bool is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z);
@ -92,11 +80,9 @@ namespace polysat {
// p := coeff*x*y where coeff_x = coeff*x, x a variable // p := coeff*x*y where coeff_x = coeff*x, x a variable
bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y); bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
rational max_value(pdd const& x);
public: public:
inf_saturate(solver& s) : inference_engine(s) {} saturation(solver& s);
bool perform(pvar v, conflict& core) override; bool perform(pvar v, conflict& core);
}; };
/* /*

2
src/math/polysat/solver.h
View file

@ -133,7 +133,7 @@ namespace polysat {
friend class assignments_pp; friend class assignments_pp;
friend class ex_polynomial_superposition; friend class ex_polynomial_superposition;
friend class free_variable_elimination; friend class free_variable_elimination;
friend class inf_saturate; friend class saturation;
friend class constraint_manager; friend class constraint_manager;
friend class scoped_solverv; friend class scoped_solverv;
friend class test_polysat; friend class test_polysat;