diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 3ffd388e3..165171117 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -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()); \ + 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); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 386166a3c..814d12df2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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; } diff --git a/src/util/mpq.h b/src/util/mpq.h index 8c08fe988..f6554a640 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -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::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::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::is_neg(b)) {