mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

infeas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-03 13:00:52 -08:00
parent 0077ddf33c
commit 970347e797
1 changed files with 29 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/math/lp/int_solver.cpp
View file

@ -336,59 +336,52 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
l = u = zero_of_type<impq>(); l = u = zero_of_type<impq>();
m = mpq(1); m = mpq(1);
if (has_lower(j)) { if (has_lower(j))
set_lower(l, inf_l, lower_bound(j) - xj); set_lower(l, inf_l, lower_bound(j) - xj);
}
if (has_upper(j)) { if (has_upper(j))
set_upper(u, inf_u, upper_bound(j) - xj); set_upper(u, inf_u, upper_bound(j) - xj);
}
unsigned row_index;
lp_assert(settings().use_tableau()); lp_assert(settings().use_tableau());
const auto & A = lra.A_r(); const auto & A = lra.A_r();
for (auto c : A.column(j)) {
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index];
TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";);
if (column_is_int(i) && !a.is_int())
m = lcm(m, denominator(a));
}
TRACE("random_update", tout << "m = " << m << "\n";); TRACE("random_update", tout << "m = " << m << "\n";);
auto delta = [](mpq const& x, impq const& y, impq const& z) {
if (x.is_one())
return y - z;
if (x.is_minus_one())
return z - y;
return (y - z) / x;
};
for (auto c : A.column(j)) { for (auto c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break; unsigned row_index = c.var();
row_index = c.var();
const mpq & a = c.coeff(); const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index]; unsigned i = lrac.m_r_basis[row_index];
impq const & xi = get_value(i); impq const & xi = get_value(i);
#define SET_BOUND(_fn_, a, b, x, y, z) \ if (column_is_int(i) && !a.is_int())
if (x.is_one()) \ m = lcm(m, denominator(a));
_fn_(a, b, y - z); \
else if (x.is_minus_one()) \
_fn_(a, b, z - y); \
else if (z == y) \
_fn_(a, b, zero_of_type<impq>()); \
else \
{ _fn_(a, b, (y - z)/x); } \
if (!inf_l && !inf_u) {
if (l > u)
break;
if (l == u)
continue;
}
if (a.is_neg()) { if (a.is_neg()) {
if (has_lower(i)) { if (has_lower(i))
SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_lower_bounds()[i]); set_lower(l, inf_l, delta(a, xi, lrac.m_r_lower_bounds()[i]));
} if (has_upper(i))
if (has_upper(i)) { set_upper(u, inf_u, delta(a, xi, lrac.m_r_upper_bounds()[i]));
SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_upper_bounds()[i]);
}
} }
else { else {
if (has_upper(i)) { if (has_upper(i))
SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_upper_bounds()[i]); set_lower(l, inf_l, delta(a, xi, lrac.m_r_upper_bounds()[i]));
} if (has_lower(i))
if (has_lower(i)) { set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i]));
SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_lower_bounds()[i]);
}
} }
} }