mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

adjust overflow premises, add stubs for used constraints as premises

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-09 16:58:51 +02:00
parent ed60cdc403
commit 697723d53b
3 changed files with 74 additions and 135 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/clause_builder.h
View file

@ -48,6 +48,9 @@ namespace polysat {
void push(sat::literal lit);
void push(signed_constraint c);
void push(inequality const& i) {
NOT_IMPLEMENTED_YET();
}
using const_iterator = decltype(m_literals)::const_iterator;
const_iterator begin() const { return m_literals.begin(); }

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

@ -65,127 +65,15 @@ namespace polysat {
push_c(core, c, reason);
}
/// Find smallest upper bound for the variable x, i.e., a constraint 'x <= bound' where the rhs is constant.
bool inf_saturate::find_upper_bound(pvar x, signed_constraint& c, rational& bound) {
auto& bounds = s().m_cjust[x];
rational best_bound(-1);
pdd y = s().var(x);
for (auto& b : bounds) {
inequality bound = b.as_inequality();
if (is_x_l_Y(x, bound, y) && y.is_val()) {
rational value = y.val();
if (bound.is_strict) {
SASSERT(value > 0); // "x < 0" is always false and should have led to a conflict earlier
value = value - 1;
}
if (value < best_bound) {
best_bound = value;
c = b;
}
}
}
return best_bound != -1;
}
/// Add Ω*(x, y) to the conflict state.
///
/// @param[in] p bit width
bool inf_saturate::push_omega_mul(conflict_core& core, clause_builder & reason, unsigned level, pdd const& x, pdd const& y) {
LOG_H3("Omega^*(x, y)");
LOG("x = " << x);
LOG("y = " << y);
auto& pddm = x.manager();
unsigned p = pddm.power_of_2();
unsigned min_k = 0;
unsigned max_k = p - 1;
unsigned k = p / 2;
rational x_val;
if (!s().try_eval(x, x_val))
return false;
rational y_val;
if (!s().try_eval(y, y_val))
return false;
unsigned x_bits = x_val.bitsize();
LOG("eval x: " << x << " := " << x_val << " (x_bits: " << x_bits << ")");
SASSERT(x_val < rational::power_of_two(x_bits));
min_k = x_bits;
unsigned y_bits = y_val.bitsize();
LOG("eval y: " << y << " := " << y_val << " (y_bits: " << y_bits << ")");
SASSERT(y_val < rational::power_of_two(y_bits));
max_k = p - y_bits;
if (min_k > max_k) {
// In this case, we cannot choose k such that both literals are false.
// This means x*y overflows in the current model and the chosen rule is not applicable.
// (or maybe we are in the case where we need the msb-encoding for overflow).
return false;
}
SASSERT(min_k <= max_k); // if this assertion fails, we cannot choose k s.t. both literals are false
// TODO: could also choose other value for k (but between the bounds)
if (min_k == 0)
k = max_k;
else
k = min_k;
SASSERT(min_k <= k && k <= max_k);
// x < 2^k
auto c1 = s().m_constraints.ult(level, x, pddm.mk_val(rational::power_of_two(k)));
// y <= 2^{p-k}
auto c2 = s().m_constraints.ule(level, y, pddm.mk_val(rational::power_of_two(p - k)));
// bail-out explanation uses equality constraint based on current assignment to variables.
// TODO: extract stronger explanations.
// for example if they appear already in Gamma
// or if some strengthening appears in gamma
// or using the current value assignment
clause_builder bound(s());
bound.push(s().m_constraints.eq(level, x - pddm.mk_val(x_val)));
push_c(core, c1, bound);
bound.reset();
bound.push(s().m_constraints.eq(level, y - pddm.mk_val(y_val)));
push_c(core, c2, bound);
reason.push(c1);
reason.push(c2);
return true;
}
// special case viable sets used by variables.
bool inf_saturate::push_omega_viable(conflict_core& core, clause_builder& reason, unsigned level, pdd const& px, pdd const& py) {
if (!px.is_var() || !py.is_var())
return false;
pvar x = px.var();
pvar y = py.var();
rational x_max = s().m_viable.max_viable(x);
rational y_max = s().m_viable.max_viable(y);
/// Add premises for Ω*(x, y)
void inf_saturate::push_omega_bisect(clause_builder& reason, unsigned level, pdd const& px, rational x_max, pdd const& py, rational y_max) {
rational x_val, y_val;
auto& pddm = px.manager();
unsigned bit_size = pddm.power_of_2();
rational bound = rational::power_of_two(bit_size);
if (x_max * y_max < bound) {
// max values don't overflow, we can justify no-overflow using cjust for x, y
for (auto c : s().m_cjust[x])
reason.push(c);
for (auto c : s().m_cjust[y])
reason.push(c);
return true;
}
rational x_val = s().get_value(x);
rational y_val = s().get_value(y);
if (x_val * y_val >= bound)
return false;
VERIFY(s().try_eval(px, x_val));
VERIFY(s().try_eval(py, 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;
rational two(2);
@ -195,7 +83,7 @@ namespace polysat {
if (x_mid * y_mid >= bound)
x_hi = x_mid - 1, y_hi = y_mid - 1;
else
x_lo = x_mid, y_lo = y_mid;
x_lo = x_mid, y_lo = y_mid;
}
SASSERT(x_hi == x_lo && y_hi == y_lo);
SASSERT(x_lo * y_lo < bound);
@ -232,7 +120,32 @@ namespace polysat {
auto c2 = s().m_constraints.ule(level, py, pddm.mk_val(y_lo));
reason.push(c1);
reason.push(c2);
return true;
}
// special case viable sets used by variables.
void inf_saturate::push_omega(clause_builder& reason, unsigned level, pdd const& px, pdd const& py) {
auto& pddm = px.manager();
unsigned bit_size = pddm.power_of_2();
rational bound = rational::power_of_two(bit_size);
if (px.is_var() && py.is_var()) {
pvar x = px.var();
pvar y = py.var();
rational x_max = s().m_viable.max_viable(x);
rational y_max = s().m_viable.max_viable(y);
if (x_max * y_max < bound) {
// max values don't overflow, we can justify no-overflow using cjust for x, y
for (auto c : s().m_cjust[x])
reason.push(c);
for (auto c : s().m_cjust[y])
reason.push(c);
return;
}
else
push_omega_bisect(reason, level, px, x_max, py, y_max);
}
push_omega_bisect(reason, level, px, bound - 1, py, bound-1);
}
/*
@ -269,6 +182,19 @@ namespace polysat {
return d.lhs == y && d.rhs == a * s().var(x);
}
/**
* determine whether values of x * y is non-overflowing.
*/
bool inf_saturate::is_non_overflow(pdd const& x, pdd const& y) {
rational x_val, y_val;
if (!s().try_eval(x, x_val) || !s().try_eval(y, y_val))
return false;
auto& pddm = x.manager();
rational bound = rational::power_of_two(pddm.power_of_2());
return x_val * y_val < bound;
}
/**
* Match [v] v*x <= z*x
*/
@ -337,13 +263,14 @@ namespace polysat {
pdd z = x;
if (!is_xY_l_xZ(v, c, y, z))
return false;
if (!is_non_overflow(x, y))
return false;
unsigned const lvl = c.src->level();
clause_builder reason(s());
// Omega^*(x, y)
if (!push_omega_mul(core, reason, lvl, x, y))
return false;
clause_builder reason(s());
reason.push(c);
push_omega(reason, lvl, x, y);
push_l(core, lvl, c.is_strict, y, z, reason);
return true;
@ -357,15 +284,16 @@ namespace polysat {
SASSERT(is_l_v(v, le_y));
SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z));
if (!is_non_overflow(x, y))
return false;
unsigned const lvl = std::max(yx_l_zx.src->level(), le_y.src->level());
pdd const& z_prime = le_y.lhs;
clause_builder reason(s());
// Omega^*(x, y)
if (!push_omega_mul(core, reason, lvl, x, y))
return false;
reason.push(le_y);
reason.push(yx_l_zx);
push_omega(reason, lvl, x, y);
// z'x <= zx
push_l(core, lvl, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
@ -407,10 +335,13 @@ namespace polysat {
SASSERT(is_g_v(x, x_l_z));
SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
pdd z = x_l_z.rhs;
if (!is_non_overflow(a, z))
return false;
unsigned const lvl = std::max(x_l_z.src->level(), y_l_ax.src->level());
clause_builder reason(s());
if (!push_omega_mul(core, reason, lvl, a, z))
return false;
reason.push(x_l_z);
reason.push(y_l_ax);
push_omega(reason, lvl, a, z);
push_l(core, lvl, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
return true;
}
@ -437,10 +368,12 @@ namespace polysat {
SASSERT(verify_YX_l_zX(z, d, x, y));
unsigned const lvl = std::max(c.src->level(), d.src->level());
pdd const& y_prime = c.rhs;
clause_builder reason(s());
// Omega^*(x, y')
if (!push_omega_mul(core, reason, lvl, x, y_prime))
if (!is_non_overflow(x, y_prime))
return false;
clause_builder reason(s());
reason.push(c);
reason.push(d);
push_omega(reason, lvl, x, y_prime);
// yx <= y'x
push_l(core, lvl, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
return true;

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

@ -38,8 +38,8 @@ namespace polysat {
class inf_saturate : public inference_engine {
bool find_upper_bound(pvar x, signed_constraint& c, rational& bound);
bool push_omega_viable(conflict_core& core, clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
bool push_omega_mul(conflict_core& core, clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
void push_omega(clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
void push_omega_bisect(clause_builder& reason, unsigned level, pdd const& x, rational x_max, pdd const& y, rational y_max);
signed_constraint ineq(unsigned level, bool strict, pdd const& lhs, pdd const& rhs);
void push_c(conflict_core& core, signed_constraint const& c, clause_builder& reason);
void push_l(conflict_core& core, unsigned level, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
@ -83,6 +83,9 @@ namespace polysat {
// xy := x * Y
bool is_xY(pvar x, pdd const& xy, pdd& y);
// a * b does not overflow
bool is_non_overflow(pdd const& a, pdd const& b);
public:
bool perform(pvar v, conflict_core& core) override;