mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

speed up freedom interval computation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-28 15:21:39 -08:00
parent 75d1e8e929
commit ff5bdd6f1f
3 changed files with 86 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -464,7 +464,7 @@ void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
impq & val = lcs.m_r_x[j];
bool val_is_int = val.is_int();
if (patch_only_int_vals && !val_is_int)
return;
return;
bool inf_l, inf_u;
impq l, u;
@ -473,11 +473,13 @@ void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
return;
}
bool m_is_one = m.is_one();
if (m.is_one() && val_is_int)
if (m.is_one() && val_is_int) {
return;
}
// check whether value of j is already a multiple of m.
if (val_is_int && (val.x / m).is_int())
if (val_is_int && (val.x / m).is_int()) {
return;
}
TRACE("patch_int",
tout << "TARGET j" << j << " -> [";
if (inf_l) tout << "-oo"; else tout << l;
@ -488,25 +490,21 @@ void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {
TRACE("patch_int",
tout << "patching with l: " << l << '\n';);
TRACE("patch_int", tout << "patching with l: " << l << '\n';);
m_lar_solver->set_value_for_nbasic_column(j, l);
}
else {
TRACE("patch_int",
tout << "not patching " << l << "\n";);
TRACE("patch_int", tout << "not patching " << l << "\n";);
}
}
else if (!inf_u) {
u = impq(m_is_one ? floor(u) : m * floor(u / m));
m_lar_solver->set_value_for_nbasic_column(j, u);
TRACE("patch_int",
tout << "patching with u: " << u << '\n';);
TRACE("patch_int", tout << "patching with u: " << u << '\n';);
}
else {
m_lar_solver->set_value_for_nbasic_column(j, impq(0));
TRACE("patch_int",
tout << "patching with 0\n";);
TRACE("patch_int", tout << "patching with 0\n";);
}
}
@ -758,39 +756,69 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
m = mpq(1);
if (has_low(j)) {
set_lower(l, inf_l, lower_bound(j));
set_lower(l, inf_l, lower_bound(j) - xj);
}
if (has_upper(j)) {
set_upper(u, inf_u, upper_bound(j));
set_upper(u, inf_u, upper_bound(j) - xj);
}
mpq a; // the coefficient in the column
unsigned row_index;
lp_assert(settings().use_tableau());
const auto & A = m_lar_solver->A_r();
unsigned rounds = 0;
for (const auto &c : A.column(j)) {
row_index = c.var();
const mpq & a = c.coeff();
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
impq const & xi = get_value(i);
if (column_is_int(i) && column_is_int(j) && !a.is_int())
m = lcm(m, denominator(a));
}
if (column_is_int(j) && m.is_one())
return false;
for (const auto &c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break;
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
impq const & xi = get_value(i);
#define SET_BOUND(_fn_, a, b, x, y, z) \
if (x.is_one()) \
_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 (a.is_neg()) {
if (has_low(i))
set_lower(l, inf_l, xj + (xi - lcs.m_r_lower_bounds()[i]) / a);
if (has_upper(i))
set_upper(u, inf_u, xj + (xi - lcs.m_r_upper_bounds()[i]) / a);
if (has_low(i)) {
SET_BOUND(set_lower, l, inf_l, a, xi, lcs.m_r_lower_bounds()[i]);
}
if (has_upper(i)) {
SET_BOUND(set_upper, u, inf_u, a, xi, lcs.m_r_upper_bounds()[i]);
}
}
else {
if (has_upper(i))
set_lower(l, inf_l, xj + (xi - lcs.m_r_upper_bounds()[i]) / a);
if (has_low(i))
set_upper(u, inf_u, xj + (xi - lcs.m_r_lower_bounds()[i]) / a);
if (has_upper(i)) {
SET_BOUND(set_lower, l, inf_l, a, xi, lcs.m_r_upper_bounds()[i]);
}
if (has_low(i)) {
SET_BOUND(set_upper, u, inf_u, a, xi, lcs.m_r_lower_bounds()[i]);
}
}
if (!inf_l && !inf_u && l >= u) break;
++rounds;
// patch always fails in this case
if (!inf_l && !inf_u && rounds > 2 && u - l < m && (xj.x + u.x) % m > (xj.x + l.x) % m) break;
}
l += xj;
u += xj;
TRACE("freedom_interval",
tout << "freedom variable for:\n";
tout << m_lar_solver->get_variable_name(j);

5
src/smt/theory_lra.cpp
View file

@ -1074,9 +1074,10 @@ public:
default:
break;
}
auto vi = get_lpvar(b->get_var());
if (vi == lp::null_lpvar)
auto vi = register_theory_var_in_lar_solver(b->get_var());
if (vi == lp::null_lpvar) {
return l_undef;
}
return m_solver->compare_values(vi, k, b->get_value()) ? l_true : l_false;
}

33
src/util/mpq.h
View file

@ -225,18 +225,31 @@ public:
void add(mpq const & a, mpq const & b, mpq & c) {
STRACE("mpq", tout << "[mpq] " << to_string(a) << " + " << to_string(b) << " == ";);
if (is_int(a) && is_int(b)) {
if (is_zero(b)) {
set(c, a);
}
else if (is_zero(a)) {
set(c, b);
}
else if (is_int(a) && is_int(b)) {
mpz_manager<SYNCH>::add(a.m_num, b.m_num, c.m_num);
reset_denominator(c);
}
else
else {
rat_add(a, b, c);
}
STRACE("mpq", tout << to_string(c) << "\n";);
}
void add(mpq const & a, mpz const & b, mpq & c) {
STRACE("mpq", tout << "[mpq] " << to_string(a) << " + " << to_string(b) << " == ";);
if (is_int(a)) {
if (is_zero(b)) {
set(c, a);
}
else if (is_zero(a)) {
set(c, b);
}
else if (is_int(a)) {
mpz_manager<SYNCH>::add(a.m_num, b, c.m_num);
reset_denominator(c);
}
@ -312,6 +325,9 @@ public:
else if (is_minus_one(b)) {
sub(a, c, d);
}
else if (is_zero(b) || is_zero(c)) {
set(d, a);
}
else {
if (SYNCH) {
mpq tmp;
@ -334,6 +350,9 @@ public:
else if (is_minus_one(b)) {
sub(a, c, d);
}
else if (is_zero(b) || is_zero(c)) {
set(d, a);
}
else {
if (SYNCH) {
mpq tmp;
@ -409,6 +428,10 @@ public:
void div(mpq const & a, mpq const & b, mpq & c) {
STRACE("mpq", tout << "[mpq] " << to_string(a) << " / " << to_string(b) << " == ";);
if (is_zero(a) || is_one(b)) {
set(c, a);
return;
}
if (&b == &c) {
mpz tmp; // it is not safe to use c.m_num at this point.
mul(a.m_num, b.m_den, tmp);
@ -431,6 +454,10 @@ public:
void div(mpq const & a, mpz const & b, mpq & c) {
STRACE("mpq", tout << "[mpq] " << to_string(a) << " / " << to_string(b) << " == ";);
if (is_zero(a) || is_one(b)) {
set(c, a);
return;
}
set(c.m_num, a.m_num);
mul(a.m_den, b, c.m_den);
if (mpz_manager<SYNCH>::is_neg(b)) {