mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

extract multiple bounds for upper/lower bound

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-23 14:52:41 -08:00
parent 9275930f50
commit 50cbe2659a
4 changed files with 85 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1140,7 +1140,8 @@ namespace polysat {
*/ */
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;
vector<signed_constraint> x_ge_bound;
auto& m = s.var2pdd(x); auto& m = s.var2pdd(x);
pdd y = m.zero(); pdd y = m.zero();
if (!is_add_overflow(x, axb_l_y, y)) if (!is_add_overflow(x, axb_l_y, y))
@ -1154,7 +1155,8 @@ namespace polysat {
m_lemma.reset(); m_lemma.reset();
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); for (auto c : x_ge_bound)
m_lemma.insert_eval(~c);
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));
} }
@ -1186,11 +1188,11 @@ namespace polysat {
return false; return false;
} }
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, vector<signed_constraint>& x_le_bound) {
return s.m_viable.has_upper_bound(x, bound, x_le_bound); return s.m_viable.has_upper_bound(x, bound, x_le_bound);
} }
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, vector<signed_constraint>& x_ge_bound) {
return s.m_viable.has_lower_bound(x, bound, x_ge_bound); return s.m_viable.has_lower_bound(x, bound, x_ge_bound);
} }
@ -1250,8 +1252,16 @@ namespace polysat {
* -1195: v85 + 1 > 2^128+1 * -1195: v85 + 1 > 2^128+1
* v25 := 353 * v25 := 353
* v81 := -1 * v81 := -1
*
* -1*v85*v25 + v81 < v25
* a -1*v25 := -315 b v81 := -1 y v25 := 315
* & v25 <= 315
* & -v81 <= 1
*
* The example illustrates that fixing y_val produces a weaker bound.
* The result should be a forbidden interval around v25 based on bounds for
* v85 and v81.
* *
* Note that lower bound for v85 should use forbidden intervals which subsumes pattern matching against -1195.
*/ */
bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) { bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) {
@ -1260,17 +1270,18 @@ namespace polysat {
pdd const X = s.var(x); pdd const X = s.var(x);
pdd a = s.var(x); pdd a = s.var(x);
pdd b = a, c = a, y = a; pdd b = a, c = a, y = a;
rational b_val, c_val, y_val, x_bound; rational a_val, b_val, c_val, y_val, x_bound;
signed_constraint x_ge_bound, x_le_bound, b_bound, ax_bound; vector<signed_constraint> x_le_bound, x_ge_bound;
if (is_AxB_l_Y(x, a_l_b, a, b, y) && s.try_eval(y, y_val) && s.try_eval(b, b_val) && !y_val.is_zero() && !a.is_val()) { signed_constraint b_bound;
verbose_stream() << a_l_b << " a " << a << " b " << b << " := " << dd::val_pp(m, b_val, false) << " y " << y << "\n"; if (is_AxB_l_Y(x, a_l_b, a, b, y) && !a.is_val() && s.try_eval(y, y_val) && s.try_eval(b, b_val) && s.try_eval(a, a_val) && !y_val.is_zero()) {
IF_VERBOSE(2, verbose_stream() << "v" << x << ": " << a_l_b << " a " << a << " := " << dd::val_pp(m, a_val, false) << " b " << b << " := " << dd::val_pp(m, b_val, false) << " y " << y << " := " << dd::val_pp(m, y_val, false) << "\n");
SASSERT(!a.is_zero()); SASSERT(!a.is_zero());
// define c := -b // define c := -b
c = -b; c = -b;
VERIFY(s.try_eval(c, c_val)); VERIFY(s.try_eval(c, c_val));
if (has_upper_bound(x, core, x_bound, x_le_bound) && x_le_bound != a_l_b.as_signed_constraint()) { if (has_upper_bound(x, core, x_bound, x_le_bound) && !x_le_bound.contains(a_l_b.as_signed_constraint())) {
// ax - c <= y // ax - c <= y
// ==> ax <= y + c if int(y) + int(c) <= 2^N, y <= int(y), c <= int(c) // ==> ax <= y + c if int(y) + int(c) <= 2^N, y <= int(y), c <= int(c)
// ==> a not in [-floor(-int(y+c) / int(x), 0[ // ==> a not in [-floor(-int(y+c) / int(x), 0[
@ -1278,18 +1289,23 @@ namespace polysat {
if (c_val + y_val <= m.max_value()) { if (c_val + y_val <= m.max_value()) {
auto bound = floor((m.two_to_N() - y_val - c_val) / x_bound); auto bound = floor((m.two_to_N() - y_val - c_val) / x_bound);
m_lemma.reset(); m_lemma.reset();
m_lemma.insert_eval(~x_le_bound); // x <= x_bound for (auto c : x_le_bound)
m_lemma.insert_eval(~c); // x <= x_bound
m_lemma.insert_eval(~s.ule(c, c_val)); // c <= c_val m_lemma.insert_eval(~s.ule(c, c_val)); // c <= c_val
m_lemma.insert_eval(~s.ule(y, y_val)); // y <= y_val m_lemma.insert_eval(~s.ule(y, y_val)); // y <= y_val
auto conclusion = s.uge(-a, bound); // ==> -a >= bound auto conclusion = s.uge(-a, bound); // ==> -a >= bound
verbose_stream() << "XX: " << conclusion << "\n"; IF_VERBOSE(2,
if (propagate(x, core, a_l_b, conclusion)) { verbose_stream() << core << "\n";
verbose_stream() << "& " << X << " <= " << dd::val_pp(m, x_bound, false) << " := " << x_le_bound << "\n";
verbose_stream() << "& " << s.ule(c, c_val) << "\n";
verbose_stream() << "& " << s.ule(y, y_val) << "\n";
verbose_stream() << "==> " << -a << " >= " << dd::val_pp(m, bound, false) << "\n");
if (propagate(x, core, a_l_b, conclusion))
return true; return true;
}
} }
// verbose_stream() << "TODO bound 1 " << a_l_b << " " << x_ge_bound << " " << b << " " << b_val << " " << y << "\n"; // verbose_stream() << "TODO bound 1 " << a_l_b << " " << x_ge_bound << " " << b << " " << b_val << " " << y << "\n";
} }
if (has_lower_bound(x, core, x_bound, x_le_bound) && x_le_bound != a_l_b.as_signed_constraint()) { if (has_lower_bound(x, core, x_bound, x_le_bound) && !x_le_bound.contains(a_l_b.as_signed_constraint())) {
// verbose_stream() << "TODO bound 2 " << a_l_b << " " << x_le_bound << "\n"; // verbose_stream() << "TODO bound 2 " << a_l_b << " " << x_le_bound << "\n";
} }

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

@ -120,8 +120,9 @@ namespace polysat {
// i := x + y >= x or x + y > x // i := x + y >= x or x + y > x
bool is_add_overflow(pvar x, inequality const& i, pdd& y); bool is_add_overflow(pvar x, inequality const& i, pdd& y);
bool has_upper_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_ge_bound); bool has_upper_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_ge_bound);
bool has_lower_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_le_bound);
bool has_lower_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_le_bound);
// determine min/max parity of polynomial // determine min/max parity of polynomial
unsigned min_parity(pdd const& p); unsigned min_parity(pdd const& p);

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

@ -643,46 +643,69 @@ namespace polysat {
return query<query_t::max_viable>(v, hi); return query<query_t::max_viable>(v, hi);
} }
// TBD: generalize to multiple intervals? bool viable::has_upper_bound(pvar v, rational& out_hi, vector<signed_constraint>& out_c) {
// 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) {
entry const* first = m_units[v]; entry const* first = m_units[v];
entry const* e = first; entry const* e = first;
bool found = false;
out_c.reset();
do { do {
if (!e->refined) { found = false;
auto const& lo = e->interval.lo(); do {
auto const& hi = e->interval.hi(); if (!e->refined) {
if (lo.is_val() && hi.is_val() && lo.val() > hi.val()) { auto const& lo = e->interval.lo();
out_c = e->src; auto const& hi = e->interval.hi();
out_hi = lo.val() - 1; if (lo.is_val() && hi.is_val()) {
// verbose_stream() << "Upper bound v" << v << " " << out_hi << " " << out_c << "\n"; if (out_c.empty() && lo.val() > hi.val()) {
return true; out_c.push_back(e->src);
out_hi = lo.val() - 1;
found = true;
}
else if (!out_c.empty() && lo.val() <= out_hi && out_hi < hi.val()) {
out_c.push_back(e->src);
out_hi = lo.val() - 1;
found = true;
}
}
} }
e = e->next();
} }
e = e->next(); while (e != first);
} }
while (e != first); while (found);
return false; return !out_c.empty();
} }
bool viable::has_lower_bound(pvar v, rational& out_lo, signed_constraint& out_c) { // TBD: generalize to multiple intervals similar to upper bound
bool viable::has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c) {
entry const* first = m_units[v]; entry const* first = m_units[v];
entry const* e = first; entry const* e = first;
bool found = false;
out_c.reset();
do { do {
if (!e->refined) { found = false;
auto const& lo = e->interval.lo(); do {
auto const& hi = e->interval.hi(); if (!e->refined) {
if (lo.is_val() && hi.is_val() && (lo.val() == 0 || lo.val() > hi.val())) { auto const& lo = e->interval.lo();
out_c = e->src; auto const& hi = e->interval.hi();
out_lo = hi.val(); if (lo.is_val() && hi.is_val()) {
// verbose_stream() << "Lower bound " << v << " " << out_lo << " " << out_c << "\n"; if (out_c.empty() && (lo.val() == 0 || lo.val() > hi.val())) {
return true; out_c.push_back(e->src);
out_lo = hi.val();
found = true;
}
else if (!out_c.empty() && lo.val() <= out_lo && out_lo < hi.val()) {
out_c.push_back(e->src);
out_lo = hi.val();
found = true;
}
}
} }
e = e->next();
} }
e = e->next(); while (e != first);
} }
while (e != first); while (found);
return false; return !out_c.empty();
} }
template <query_t mode> template <query_t mode>

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

@ -189,13 +189,13 @@ namespace polysat {
* Query for an upper bound literal for v together with justification. * Query for an upper bound literal for v together with justification.
* @return true if a non-trivial upper bound is found, return justifying constraint. * @return true if a non-trivial upper bound is found, return justifying constraint.
*/ */
bool has_upper_bound(pvar v, rational& out_hi, signed_constraint& out_c); bool has_upper_bound(pvar v, rational& out_hi, vector<signed_constraint>& out_c);
/** /**
* 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_lo, signed_constraint& out_c); bool has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c);
/** /**
* Find a next viable value for variable. * Find a next viable value for variable.