mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
testing inference based on complementary bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
56bda59de9
commit
824c10711c
3 changed files with 88 additions and 88 deletions
|
|
@ -1454,8 +1454,8 @@ namespace polysat {
|
|||
*/
|
||||
|
||||
bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) {
|
||||
// if (try_add_mul_bound2(x, core, a_l_b))
|
||||
// return true;
|
||||
if (try_add_mul_bound2(x, core, a_l_b))
|
||||
return true;
|
||||
|
||||
set_rule("[x] ax + b <= y, ... => a >= u_a");
|
||||
auto& m = s.var2pdd(x);
|
||||
|
|
@ -1687,35 +1687,15 @@ namespace polysat {
|
|||
bool saturation::try_add_mul_bound2(pvar x, conflict& core, inequality const& a_l_b) {
|
||||
set_rule("[x] mul-bound2 ax + b <= y, ... => a >= u_a");
|
||||
|
||||
// enable for dev
|
||||
return false;
|
||||
|
||||
auto& m = s.var2pdd(x);
|
||||
pdd p = a_l_b.lhs(), q = a_l_b.rhs();
|
||||
if (p.degree(x) > 1 || q.degree(x) > 1)
|
||||
return false;
|
||||
if (p.degree(x) == 0 && q.degree(x) == 0)
|
||||
return false;
|
||||
vector<signed_constraint> bounds;
|
||||
rational x_min, x_max;
|
||||
if (!s.m_viable.has_max_forbidden(x, x_min, x_max, bounds))
|
||||
return false;
|
||||
|
||||
VERIFY(x_min != x_max);
|
||||
// From forbidden interval [x_min, x_max[ compute
|
||||
// allowed range: [x_max, x_min - 1]
|
||||
SASSERT(0 <= x_min && x_min <= m.max_value());
|
||||
SASSERT(0 <= x_max && x_max <= m.max_value());
|
||||
rational M = m.two_to_N();
|
||||
rational hi = x_min == 0 ? M - 1 : x_min - 1;
|
||||
x_min = x_max;
|
||||
x_max = hi;
|
||||
SASSERT(x_min != x_max);
|
||||
if (x_min > x_max)
|
||||
x_min -= M;
|
||||
SASSERT(x_min <= x_max);
|
||||
|
||||
if (x_max == 0) {
|
||||
SASSERT(x_min == 0);
|
||||
return false;
|
||||
}
|
||||
|
||||
pvar y1 = null_var, y2 = null_var, y;
|
||||
rational a1, a2, b1, b2, c1, c2, d1, d2;
|
||||
|
|
@ -1728,8 +1708,29 @@ namespace polysat {
|
|||
if (y1 == null_var && y2 == null_var)
|
||||
return false;
|
||||
y = (y1 == null_var) ? y2 : y1;
|
||||
rational y0 = s.get_value(y);
|
||||
rational y0 = s.get_value(y);
|
||||
|
||||
vector<signed_constraint> bounds;
|
||||
rational x_min, x_max;
|
||||
if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_min, x_max, bounds))
|
||||
return false;
|
||||
|
||||
VERIFY(x_min != x_max);
|
||||
// [x_min, x_max[ is allowed interval.
|
||||
// compute [x_min, x_max - 1]
|
||||
|
||||
// From forbidden interval [x_min, x_max[ compute
|
||||
// allowed range: [x_max, x_min - 1]
|
||||
SASSERT(0 <= x_min && x_min <= m.max_value());
|
||||
SASSERT(0 <= x_max && x_max <= m.max_value());
|
||||
rational M = m.two_to_N();
|
||||
x_max = x_max == 0 ? M - 1 : x_max - 1;
|
||||
if (x_min == x_max)
|
||||
return false;
|
||||
if (x_min > x_max)
|
||||
x_min -= M;
|
||||
SASSERT(x_min <= x_max);
|
||||
|
||||
IF_VERBOSE(2,
|
||||
s.m_viable.display(verbose_stream(), x) << "\n";
|
||||
verbose_stream() << "x_min " << x_min << " x_max " << x_max << "\n";
|
||||
|
|
@ -1782,8 +1783,10 @@ namespace polysat {
|
|||
return false;
|
||||
|
||||
m_lemma.reset();
|
||||
for (auto c : bounds)
|
||||
m_lemma.insert(~c);
|
||||
for (auto const& c : bounds)
|
||||
m_lemma.insert_eval(~c);
|
||||
// m_lemma.insert_eval(~s.ule(x_min, s.var(x)));
|
||||
// m_lemma.insert_eval(~s.ule(s.var(x), x_max));
|
||||
fix_values(x, y, p);
|
||||
fix_values(x, y, q);
|
||||
if (y_max != M - 1) {
|
||||
|
|
|
|||
|
|
@ -726,73 +726,70 @@ namespace polysat {
|
|||
return !out_c.empty();
|
||||
}
|
||||
|
||||
bool viable::has_max_forbidden(pvar v, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c) {
|
||||
bool viable::has_max_forbidden(pvar v, signed_constraint const& c, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c) {
|
||||
out_c.reset();
|
||||
entry const* first = m_units[v];
|
||||
entry const* e = first;
|
||||
bool found = false;
|
||||
if (!e)
|
||||
return false;
|
||||
|
||||
auto covers_all = [&](rational const& lo1, rational const& hi1, rational const lo2, rational const& hi2) {
|
||||
SASSERT(lo1 != hi1);
|
||||
if (lo1 < hi1) {
|
||||
return lo2 <= hi1 && lo1 <= hi2;
|
||||
}
|
||||
else
|
||||
// hi1 < lo1
|
||||
return hi1 <= hi2 && hi2 <= lo2 && lo2 <= lo1;
|
||||
};
|
||||
|
||||
auto overlap_left = [&](rational const& lo1, rational const& hi1, rational const lo2, rational const& hi2) {
|
||||
if (lo2 < hi2)
|
||||
return lo2 <= hi1 && hi1 <= hi2;
|
||||
else
|
||||
// hi2 < lo2
|
||||
return lo1 < lo2 && (hi1 <= hi2 || lo2 <= hi1);
|
||||
};
|
||||
|
||||
do {
|
||||
found = false;
|
||||
do {
|
||||
if (e->refined)
|
||||
goto next;
|
||||
|
||||
auto const& lo = e->interval.lo();
|
||||
auto const& hi = e->interval.hi();
|
||||
if (!lo.is_val() || !hi.is_val())
|
||||
goto next;
|
||||
if (out_c.contains(e->src))
|
||||
goto next;
|
||||
if (out_c.empty()) {
|
||||
out_c.push_back(e->src);
|
||||
out_lo = lo.val();
|
||||
out_hi = hi.val();
|
||||
found = true;
|
||||
}
|
||||
else if (covers_all(out_lo, out_hi, lo.val(), hi.val()))
|
||||
return false;
|
||||
// [lo, hi0, hi[
|
||||
// [lo, hi0, 0, hi[
|
||||
else if (overlap_left(lo.val(), hi.val(), out_lo, out_hi)) {
|
||||
out_c.push_back(e->src);
|
||||
out_lo = lo.val();
|
||||
found = true;
|
||||
}
|
||||
// [lo, lo0, hi[
|
||||
// [lo, 0, lo0, hi[
|
||||
else if (overlap_left(out_lo, out_hi, lo.val(), hi.val())) {
|
||||
out_c.push_back(e->src);
|
||||
out_hi = hi.val();
|
||||
found = true;
|
||||
}
|
||||
next:
|
||||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
if (e->src == c)
|
||||
break;
|
||||
e = e->next();
|
||||
}
|
||||
while (found);
|
||||
return !out_c.empty();
|
||||
while (e != first);
|
||||
|
||||
if (e->src != c)
|
||||
return false;
|
||||
entry const* e0 = e;
|
||||
|
||||
|
||||
do {
|
||||
entry const* n = e->next();
|
||||
while (n != first) {
|
||||
entry const* n1 = n->next();
|
||||
if (n1 == e)
|
||||
break;
|
||||
if (!e->interval.currently_contains(n1->interval.lo_val()))
|
||||
if (e->interval.hi_val() != n1->interval.lo_val())
|
||||
break;
|
||||
n = n1;
|
||||
}
|
||||
|
||||
if (e == e0) {
|
||||
out_hi = n->interval.lo_val();
|
||||
if (!n->interval.lo().is_val())
|
||||
out_c.push_back(s.eq(n->interval.lo(), out_hi));
|
||||
}
|
||||
else if (n == e0) {
|
||||
out_lo = e->interval.hi_val();
|
||||
if (!e->interval.hi().is_val())
|
||||
out_c.push_back(s.eq(e->interval.hi(), out_lo));
|
||||
}
|
||||
else if (!e->interval.is_full()) {
|
||||
auto const& hi = e->interval.hi();
|
||||
auto const& next_lo = n->interval.lo();
|
||||
auto const& next_hi = n->interval.hi();
|
||||
auto lhs = hi - next_lo;
|
||||
auto rhs = next_hi - next_lo;
|
||||
signed_constraint c = s.m_constraints.ult(lhs, rhs);
|
||||
out_c.push_back(c);
|
||||
}
|
||||
if (e != e0) {
|
||||
for (auto sc : e->side_cond)
|
||||
out_c.push_back(sc);
|
||||
out_c.push_back(e->src);
|
||||
}
|
||||
e = n;
|
||||
}
|
||||
while (e != e0);
|
||||
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "has-max-forbidden " << e->src << "\n";
|
||||
verbose_stream() << "v" << v << " " << out_lo << " " << out_hi << " " << out_c << "\n";
|
||||
display(verbose_stream(), v) << "\n");
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -201,7 +201,7 @@ namespace polysat {
|
|||
/**
|
||||
* Query for a maximal interval based on fixed bounds where v is forbidden.
|
||||
*/
|
||||
bool has_max_forbidden(pvar v, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c);
|
||||
bool has_max_forbidden(pvar v, signed_constraint const& c, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c);
|
||||
|
||||
/**
|
||||
* Find a next viable value for variable.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue