mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Try bounds propagation for the example case

Browse source
This commit is contained in:
Jakob Rath 2022-12-23 18:15:05 +01:00
parent 993996c8a5
commit fda93c97f5
1 changed files with 39 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1264,39 +1264,70 @@ namespace polysat {
* v85 := 12
* -v85*v33 - 1 <= 2^128-2
* Then -v85*v33 <= 2^128-1
* Then v33*v85 >= -2^128+1
* Then v33*v85 >= -2^128+1 (requires lhs != 0, rhs != 0)
* Then v85 >= ceil(-2^128+1 / 2^128-1)
*/
bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) {
set_rule("[x] ax + b <= n1, x >= n2, b >= n2, b <= n1, b <= ax => a <= (n1 - n3)/n2");
verbose_stream() << "try-add-mul-bound " << a_l_b << "\n";
verbose_stream() << "try-add-mul-bound v" << x << " " << a_l_b << "\n";
auto& m = s.var2pdd(x);
pdd const X = s.var(x);
pdd a = s.var(x);
pdd b = a, y = a;
rational b_val, y_val, x_bound;
pdd b = a, c = a, y = a;
rational b_val, c_val, y_val, x_bound;
signed_constraint x_ge_bound, x_le_bound, b_bound, ax_bound;
if (is_AxB_l_Y(x, a_l_b, a, b, y) && y.is_val() && s.try_eval(b, b_val)) {
verbose_stream() << " a " << a << " b " << b << " := " << dd::val_pp(m, b_val, false) << " y " << y << "\n";
SASSERT(!a.is_zero());
y_val = y.val();
if (has_upper_bound(x, core, x_bound, x_ge_bound) && x_ge_bound != a_l_b.as_signed_constraint()) {
// define c := -b
c = -b;
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()) {
// ax + b <= y & b_val <= b <= y & ax + b >= b & ... => ax <= y - b_val
if (b_val < y_val) {
y = y - b_val;
}
// ax - b <= y & b <= b_val, y + b_val < N => ax <= y + b_val
// ax - c <= y
// ==> ax <= y + c if int(y) + int(c) <= 2^N i.e. ~Omega^+(y, c) ... y+c >= c or y+c >= y
// ==> (-a)x >= -y-c if ax != 0 and y+c != 0
// ==> -a >= ceil(int(-y-c) / int(x)) TODO: double-check if ceil works here or if floor is needed
else if (c_val + y_val <= m.max_value()) {
auto bound = ceil((m.two_to_N() - y_val - c_val) / x_bound);
m_lemma.reset();
m_lemma.insert_eval(~x_le_bound); // x <= x_bound
m_lemma.insert_eval(~s.ule(c, c_val)); // c <= c_val
m_lemma.insert_eval(~s.ult(y, y + c)); // ~Omega^+(y, c) <=> y < y + c
m_lemma.insert_try_eval(s.eq(a*X)); // ax != 0
m_lemma.insert_try_eval(s.eq(y+c)); // y + c != 0
auto conclusion = s.uge(-a, bound); // ==> -a >= bound
verbose_stream() << "XX: " << conclusion << "\n";
if (propagate(x, core, a_l_b, conclusion)) {
// std::abort();
return true;
}
}
#if 0
// ax - b <= y & b <= b_val & y + b_val < N => ax <= y + b_val // ??? conclusion seems to add b on LHS and -b on RHS
else if (s.try_eval((-b), b_val) && b_val <= y_val && b_val + y_val <= m.max_value()) {
y = y + b_val;
b_bound = s.ule(-b, b_val);
auto bound = ceil((m.two_to_N() - y_val - b_val) / x_bound);
b = bound;
m_lemma.reset();
m_lemma.insert(~x_ge_bound);
m_lemma.insert_eval(~b_bound); // -b <= b_val
// TODO m_lemma.insert_eval(s.ule(y, y - b)); // -2^N < y - b < 2^N
verbose_stream() << "XX: " << b_bound << " " << s.uge(-a, b) << "\n";
verbose_stream() << "XX: " << b_bound << " " << s.uge(-a, b) << "\n";
//
if (propagate(x, core, a_l_b, s.uge(-a, b)))
if (propagate(x, core, a_l_b, s.uge(-a, b))) {
// std::abort();
return true;
}
}
#endif
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()) {