mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

extract_bilinear_form: handle case where top variable is different on LHS and RHS

Browse source
This commit is contained in:
Jakob Rath 2023-03-04 17:19:58 +01:00
parent d5271df888
commit 235c465ae2
2 changed files with 61 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1567,43 +1567,70 @@ namespace polysat {
return x; return x;
} }
bool saturation::eval_round(rational const& M, pdd const& p, rational& r) {
if (!s.try_eval(p, r))
return false;
r = round(M, r);
return true;
}
/** /**
* write as q := a*y + b * Write as q := a*y + b
*
* If y == null_var, chooses some variable y from q (if one exists).
*/ */
bool saturation::extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b) { bool saturation::extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b) {
auto & m = q.manager(); auto& m = q.manager();
auto M = m.two_to_N(); rational const& M = m.two_to_N();
if (q.is_val()) { if (q.is_val()) {
a = 0; a = 0;
b = round(M, q.val()); b = round(M, q.val());
return true; return true;
} }
y = q.var(); if (y == null_var) {
if (q.hi().is_var() && q.hi().var() == y) // choose the top variable
return false; y = q.var();
if (!s.try_eval(q.hi(), a)) if (q.hi().is_var() && q.hi().var() == y)
return false; return false;
if (!s.try_eval(q.lo(), b)) if (!eval_round(M, q.hi(), a))
return false; return false;
if (!eval_round(M, q.lo(), b))
a = round(M, a); return false;
b = round(M, b); return true;
return true; }
else {
// factor according to given variable
SASSERT(y != null_var);
switch (q.degree(y)) {
case 0:
if (!eval_round(M, q, b))
return false;
a = 0;
return true;
case 1: {
pdd a1(m), b1(m);
q.factor(y, 1, a1, b1);
if (!eval_round(M, a1, a))
return false;
if (!eval_round(M, b1, b))
return false;
return true;
}
default:
return false;
}
}
} }
/** /**
* write as p := a*x*y + b*x + c*y + d * Write as p := a*x*y + b*x + c*y + d
*
* If y == null_var, chooses some variable y != x from p (if one exists).
*/ */
bool saturation::extract_bilinear_form(pvar x, pdd const& p, pvar& y, rational& a, rational& b, rational& c, rational& d) { bool saturation::extract_bilinear_form(pvar x, pdd const& p, pvar& y, rational& a, rational& b, rational& c, rational& d) {
auto & m = s.var2pdd(x); auto& m = s.var2pdd(x);
auto M = m.two_to_N(); rational const& M = m.two_to_N();
auto eval_round = [&](pdd const& p, rational& r) {
if (!s.try_eval(p, r))
return false;
r = round(M, r);
return true;
};
switch (p.degree(x)) { switch (p.degree(x)) {
case 0: case 0:
if (!s.try_eval(p, d)) if (!s.try_eval(p, d))
@ -1617,20 +1644,20 @@ namespace polysat {
return false; return false;
if (a == 0) { if (a == 0) {
c = 0; c = 0;
return eval_round(r, d); return eval_round(M, r, d);
} }
SASSERT(y != null_var); SASSERT(y != null_var);
switch (r.degree(y)) { switch (r.degree(y)) {
case 0: case 0:
if (!eval_round(r, d)) if (!eval_round(M, r, d))
return false; return false;
c = 0; c = 0;
return true; return true;
case 1: case 1:
r.factor(y, 1, u, v); r.factor(y, 1, u, v);
if (!eval_round(u, c)) if (!eval_round(M, u, c))
return false; return false;
if (!eval_round(v, d)) if (!eval_round(M, v, d))
return false; return false;
return true; return true;
default: default:
@ -1766,7 +1793,6 @@ namespace polysat {
} }
void saturation::fix_values(pvar x, pvar y, pdd const& p) { void saturation::fix_values(pvar x, pvar y, pdd const& p) {
pdd q = p, r = p;
if (p.degree(x) == 0) if (p.degree(x) == 0)
fix_values(y, p); fix_values(y, p);
else { else {
@ -1846,17 +1872,14 @@ namespace polysat {
if (p.degree(x) == 0 && q.degree(x) == 0) if (p.degree(x) == 0 && q.degree(x) == 0)
return false; return false;
pvar y1 = null_var, y2 = null_var, y; pvar y = null_var;
rational a1, a2, b1, b2, c1, c2, d1, d2; rational a1, a2, b1, b2, c1, c2, d1, d2;
if (!extract_bilinear_form(x, p, y1, a1, b1, c1, d1)) if (!extract_bilinear_form(x, p, y, a1, b1, c1, d1))
return false; return false;
if (!extract_bilinear_form(x, q, y2, a2, b2, c2, d2)) if (!extract_bilinear_form(x, q, y, a2, b2, c2, d2))
return false; return false;
if (y1 != null_var && y2 != null_var && y1 != y2) if (y == null_var)
return false; return false;
if (y1 == null_var && y2 == null_var)
return false;
y = (y1 == null_var) ? y2 : y1;
if (!s.is_assigned(y)) if (!s.is_assigned(y))
return false; return false;
rational y0 = s.get_value(y); rational y0 = s.get_value(y);
@ -1872,8 +1895,8 @@ namespace polysat {
VERIFY(x_min != x_max); VERIFY(x_min != x_max);
SASSERT(0 <= x_min && x_min <= m.max_value()); SASSERT(0 <= x_min && x_min <= m.max_value());
SASSERT(0 <= x_max && x_max <= m.max_value()); SASSERT(0 <= x_max && x_max <= m.max_value());
rational M = m.two_to_N(); rational const& M = m.two_to_N();
x_max = x_max == 0 ? M - 1 : x_max - 1; x_max = x_max == 0 ? m.max_value() : x_max - 1;
if (x_min == x_max) if (x_min == x_max)
return false; return false;
if (x_min > x_max) if (x_min > x_max)

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

@ -73,6 +73,7 @@ namespace polysat {
bool try_div_monotonicity(conflict& core); bool try_div_monotonicity(conflict& core);
rational round(rational const& M, rational const& x); rational round(rational const& M, rational const& x);
bool eval_round(rational const& M, pdd const& p, rational& r);
bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b); bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b);
bool extract_bilinear_form(pvar x, pdd const& p, pvar& y, rational& a, rational& b, rational& c, rational& d); bool extract_bilinear_form(pvar x, pdd const& p, pvar& y, rational& a, rational& b, rational& c, rational& d);
bool adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M, rational const& a, rational const& b, rational const& c, rational& d, rational* x_split); bool adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M, rational const& a, rational const& b, rational const& c, rational& d, rational* x_split);