mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

fix bug in add-overflow propagation, move to use viable to mind for bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-23 13:38:51 -08:00
parent 9fefa0040f
commit 9275930f50
3 changed files with 27 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1133,13 +1133,13 @@ namespace polysat {
} }
/** /**
* x <= x + y & x <= n => y = 0 or y >= N - n * x >= x + y & x <= n => y = 0 or y >= N - n
* x < x + y & x <= n => y >= N - n * x > x + y & x <= n => y >= N - n
* -x >= -x - y & x <= n => y = 0 or y >= N - n * -x <= -x - y & x <= n => y = 0 or y >= N - n
* -x > -x - y & x <= n => y >= N - n * -x < -x - y & x <= n => y >= N - n
*/ */
bool saturation::try_add_overflow_bound(pvar x, conflict& core, inequality const& axb_l_y) { bool saturation::try_add_overflow_bound(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] x <= x + y & x <= n => y = 0 or y >= 2^N - n"); set_rule("[x] x >= x + y & x <= n => y = 0 or y >= 2^N - n");
signed_constraint y_eq_0, x_ge_bound; signed_constraint y_eq_0, x_ge_bound;
auto& m = s.var2pdd(x); auto& m = s.var2pdd(x);
pdd y = m.zero(); pdd y = m.zero();
@ -1155,16 +1155,15 @@ namespace polysat {
if (!axb_l_y.is_strict()) if (!axb_l_y.is_strict())
m_lemma.insert_eval(y_eq_0); m_lemma.insert_eval(y_eq_0);
m_lemma.insert_eval(~x_ge_bound); m_lemma.insert_eval(~x_ge_bound);
verbose_stream() << "ADD overflow bound " << axb_l_y << "\n";
return propagate(x, core, axb_l_y, s.uge(y, m.two_to_N() - bound)); return propagate(x, core, axb_l_y, s.uge(y, m.two_to_N() - bound));
} }
/** /**
* Match one of the patterns: * Match one of the patterns:
* x <= x + y * x >= x + y
* x < x + y * x > x + y
* -x >= -x - y * -x <= -x - y
* -x > -x - y * -x < -x - y
*/ */
bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y) { bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y) {
auto& m = s.var2pdd(x); auto& m = s.var2pdd(x);
@ -1172,12 +1171,12 @@ namespace polysat {
pdd a = X; pdd a = X;
if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1) if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1)
return false; return false;
if (i.lhs() == X) { if (i.rhs() == X) {
i.rhs().factor(x, 1, a, y); i.lhs().factor(x, 1, a, y);
if (a.is_one()) if (a.is_one())
return true; return true;
} }
if (i.rhs() == -X) { if (i.lhs() == -X) {
i.rhs().factor(x, 1, a, y); i.rhs().factor(x, 1, a, y);
if ((-a).is_one()) { if ((-a).is_one()) {
y = -y; y = -y;
@ -1187,71 +1186,12 @@ namespace polysat {
return false; return false;
} }
/**
* Just search core for literal of the form x <= bound
* TODO
* - more general bounnds obtained from forbidden interval extraction: x + k1 <= x + k2
* such that the forbidden interval includes -1.
* - in other words, use viable set to probe for bounds instead of literals
* - not just core, but query over all assigned literals?
* - look for optimal bounds, not just the first?
* - General comment: integrate with indexing: only assigned literals containing x are useful.
* - then index on patterns or features of literals?
*/
bool saturation::has_upper_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_le_bound) { bool saturation::has_upper_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_le_bound) {
return s.m_viable.has_upper_bound(x, bound, x_le_bound);
bool found = s.m_viable.has_upper_bound(x, bound, x_le_bound);
verbose_stream() << "found " << found << "\n";
auto& m = s.var2pdd(x);
pdd y = s.var(x);
for (auto const& c : core) {
if (!c->is_ule())
continue;
auto i = inequality::from_ule(c);
if (!is_x_l_Y(x, i, y))
continue;
if (!y.is_val())
continue;
bound = y.val();
if (i.is_strict() && bound == 0)
continue;
if (i.is_strict())
bound = bound - 1;
if (bound == m.max_value())
continue;
x_le_bound = c;
return true;
}
return false;
} }
bool saturation::has_lower_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_ge_bound) { bool saturation::has_lower_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_ge_bound) {
return s.m_viable.has_lower_bound(x, bound, x_ge_bound);
bool found = s.m_viable.has_lower_bound(x, bound, x_ge_bound);
verbose_stream() << "found " << found << "\n";
auto& m = s.var2pdd(x);
pdd y = s.var(x);
for (auto const& c : core) {
if (!c->is_ule())
continue;
auto i = inequality::from_ule(c);
if (!is_Y_l_x(x, i, y))
continue;
if (!y.is_val())
continue;
bound = y.val();
if (i.is_strict() && bound == m.max_value())
continue;
if (i.is_strict())
bound = bound + 1;
if (bound == 0)
continue;
x_ge_bound = c;
return true;
}
return false;
} }
/* /*

19
src/math/polysat/viable.cpp
View file

@ -643,40 +643,45 @@ namespace polysat {
return query<query_t::max_viable>(v, hi); return query<query_t::max_viable>(v, hi);
} }
// TBD: generalize to multiple intervals?
// Multiple intervals could be used to constrain upper/lower bounds, not just the last one.
bool viable::has_upper_bound(pvar v, rational& out_hi, signed_constraint& out_c) { bool viable::has_upper_bound(pvar v, rational& out_hi, signed_constraint& out_c) {
entry const* first = m_units[v]; entry const* first = m_units[v];
entry const* e = first; entry const* e = first;
do { do {
if (!e->refined) { if (!e->refined) {
verbose_stream() << "has-upper-bound " << e->src << " " << e->interval << "\n";
auto const& lo = e->interval.lo(); auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi(); auto const& hi = e->interval.hi();
if (lo.is_val() && hi.is_val() && lo.val() > hi.val()) { if (lo.is_val() && hi.is_val() && lo.val() > hi.val()) {
out_c = e->src; out_c = e->src;
out_hi = lo.val() - 1; out_hi = lo.val() - 1;
// verbose_stream() << "Upper bound v" << v << " " << out_hi << " " << out_c << "\n";
return true; return true;
} }
} }
e = e->next(); e = e->next();
} }
while (e != first); while (e != first);
return false; return false;
} }
bool viable::has_lower_bound(pvar v, rational& out_hi, signed_constraint& out_c) { bool viable::has_lower_bound(pvar v, rational& out_lo, signed_constraint& out_c) {
entry const* first = m_units[v]; entry const* first = m_units[v];
entry const* e = first; entry const* e = first;
do { do {
if (!e->refined) { if (!e->refined) {
verbose_stream() << "has-upper-bound " << e->src << " " << e->interval << "\n"; auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi();
if (lo.is_val() && hi.is_val() && (lo.val() == 0 || lo.val() > hi.val())) {
out_c = e->src;
out_lo = hi.val();
// verbose_stream() << "Lower bound " << v << " " << out_lo << " " << out_c << "\n";
return true;
}
} }
e = e->next(); e = e->next();
} }
while (e != first); while (e != first);
return false;
return false; return false;
} }

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

@ -195,7 +195,7 @@ namespace polysat {
* Query for an lower bound literal for v together with justification. * Query for an lower bound literal for v together with justification.
* @return true if a non-trivial lower bound is found, return justifying constraint. * @return true if a non-trivial lower bound is found, return justifying constraint.
*/ */
bool has_lower_bound(pvar v, rational& out_hi, signed_constraint& out_c); bool has_lower_bound(pvar v, rational& out_lo, signed_constraint& out_c);
/** /**
* Find a next viable value for variable. * Find a next viable value for variable.