diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index dd97aa957..7714f54ce 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -18,7 +18,7 @@ void clear() {lp_assert(false); // not implemented } -lar_solver::lar_solver(const std::function& report_equality_of_fixed_vars) : +lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_crossed_bounds_column(-1), m_mpq_lar_core_solver(m_settings, *this), @@ -26,9 +26,7 @@ lar_solver::lar_solver(const std::function& report_equ m_need_register_terms(false), m_var_register(false), m_term_register(true), - m_constraints(*this), - m_report_equality_of_fixed_vars(report_equality_of_fixed_vars) -{} + m_constraints(*this) {} void lar_solver::set_track_pivoted_rows(bool v) { m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; @@ -1718,6 +1716,12 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig return right_side.is_int(); } +constraint_index lar_solver::add_var_bound_check_on_equal(var_index j, lconstraint_kind kind, const mpq & right_side, var_index& equal_var) { + constraint_index ci = mk_var_bound(j, kind, right_side); + activate_check_on_equal(ci, equal_var); + return ci; +} + constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { constraint_index ci = mk_var_bound(j, kind, right_side); activate(ci); @@ -1735,10 +1739,11 @@ void lar_solver::remove_non_fixed_from_fixed_var_table() { m_fixed_var_table.erase(p); } -void lar_solver::register_in_fixed_var_table(unsigned j) { +void lar_solver::register_in_fixed_var_table(unsigned j, unsigned & equal_to_j) { SASSERT(column_is_fixed(j)); + equal_to_j = null_lpvar; const impq& bound = get_lower_bound(j); - if (bound.y.is_zero() == false) + if (!bound.y.is_zero()) return; value_sort_pair key(bound.x, column_is_int(j)); @@ -1748,10 +1753,16 @@ void lar_solver::register_in_fixed_var_table(unsigned j) { return; } SASSERT(column_is_fixed(k)); - if (j != k && column_is_int(j) == column_is_int(k)) - m_report_equality_of_fixed_vars( - column_to_reported_index(j), - column_to_reported_index(k)); + if (j != k && column_is_int(j) == column_is_int(k)) { + equal_to_j = column_to_reported_index(k); + TRACE("lar_solver", tout << "found equal column k = " << k << + ", external = " << equal_to_j << "\n";); + } +} + +void lar_solver::activate_check_on_equal(constraint_index ci, unsigned & equal_column) { + auto const& c = m_constraints[ci]; + update_column_type_and_bound_check_on_equal(c.column(), c.kind(), c.rhs(), ci, equal_column); } void lar_solver::activate(constraint_index ci) { @@ -1817,7 +1828,7 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq & } } -void lar_solver::update_column_type_and_bound(var_index j, +void lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) { @@ -1826,8 +1837,17 @@ void lar_solver::update_column_type_and_bound(var_index j, update_column_type_and_bound_with_ub(j, kind, right_side, constr_index); else update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); +} + +void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j, + lconstraint_kind kind, + const mpq & right_side, + constraint_index constr_index, + unsigned& equal_to_j) { + update_column_type_and_bound(j, kind, right_side, constr_index); + equal_to_j = null_lpvar; if (column_is_fixed(j)) { - register_in_fixed_var_table(j); + register_in_fixed_var_table(j, equal_to_j); } } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 94bf3857a..727a0ca7f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -109,7 +109,6 @@ class lar_solver : public column_namer { unsigned, value_sort_pair_hash, default_eq> m_fixed_var_table; - std::function m_report_equality_of_fixed_vars; // end of fields ////////////////// methods //////////////////////////////// @@ -143,14 +142,15 @@ class lar_solver : public column_namer { const impq& get_value(column_index const& j) const { return get_column_value(j); } - void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, unsigned&); + void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); - void register_in_fixed_var_table(var_index); + void register_in_fixed_var_table(unsigned, unsigned&); void remove_non_fixed_from_fixed_var_table(); constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side); inline void set_infeasible_column(unsigned j) { @@ -342,7 +342,8 @@ public: } // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); - void activate(constraint_index ci); + void activate_check_on_equal(constraint_index, var_index&); + void activate(constraint_index); void random_update(unsigned sz, var_index const * vars); template void propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { @@ -361,7 +362,9 @@ public: bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side); var_index add_term(const vector> & coeffs, unsigned ext_i); void register_existing_terms(); - constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ; + constraint_index add_var_bound(var_index, lconstraint_kind, const mpq &); + constraint_index add_var_bound_check_on_equal(var_index, lconstraint_kind, const mpq &, var_index&); + var_index add_var(unsigned ext_j, bool is_integer); void set_cut_strategy(unsigned cut_frequency); inline unsigned column_count() const { return A_r().column_count(); } @@ -593,7 +596,7 @@ public: void fill_explanation_from_crossed_bounds_column(explanation & evidence) const; bool term_is_used_as_row(unsigned term) const; bool tighten_term_bounds_by_delta(tv const& t, const impq&); - lar_solver(const std::function & report_equality_of_fixed_vars); + lar_solver(); void set_track_pivoted_rows(bool v); bool get_track_pivoted_rows() const; virtual ~lar_solver(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 90ec8f33d..ba9672291 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -338,8 +338,8 @@ class theory_lra::imp { theory_var v = mk_var(cnst); var = lp().add_var(v, is_int); lp().push(); - add_def_constraint(lp().add_var_bound(var, lp::GE, rational(c))); - add_def_constraint(lp().add_var_bound(var, lp::LE, rational(c))); + add_def_constraint_and_equality(var, lp::GE, rational(c)); + add_def_constraint_and_equality(var, lp::LE, rational(c)); TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";); return var; } @@ -770,6 +770,17 @@ class theory_lra::imp { bool is_infeasible() const { return lp().get_status() == lp::lp_status::INFEASIBLE; } + + void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, + const rational& bound) { + lpvar vi_equal; + lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal); + add_def_constraint(ci); + if (vi_equal != lp::null_lpvar) { + report_equality_of_fixed_vars(vi, vi_equal); + } + + } void internalize_eq(theory_var v1, theory_var v2) { app_ref term(m.mk_fresh_const("eq", a.mk_real()), m); @@ -780,12 +791,12 @@ class theory_lra::imp { st.coeffs().push_back(rational::minus_one()); theory_var z = internalize_linearized_def(term, st); lpvar vi = register_theory_var_in_lar_solver(z); - add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero())); + add_def_constraint_and_equality(vi, lp::LE, rational::zero()); if (is_infeasible()) { IF_VERBOSE(0, verbose_stream() << "infeasible\n";); // process_conflict(); // exit here? } - add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); + add_def_constraint_and_equality(vi, lp::GE, rational::zero()); if (is_infeasible()) { IF_VERBOSE(0, verbose_stream() << "infeasible\n";); // process_conflict(); // exit here? @@ -885,8 +896,8 @@ class theory_lra::imp { } if (m_left_side.empty()) { vi = lp().add_var(v, a.is_int(term)); - add_def_constraint(lp().add_var_bound(vi, lp::GE, rational(0))); - add_def_constraint(lp().add_var_bound(vi, lp::LE, rational(0))); + add_def_constraint_and_equality(vi, lp::GE, rational(0)); + add_def_constraint_and_equality(vi, lp::LE, rational(0)); } else { vi = lp().add_term(m_left_side, v); @@ -937,7 +948,7 @@ public: if (m_solver) return; reset_variable_values(); - m_solver = alloc(lp::lar_solver, [&](unsigned j, unsigned k) { report_equality_of_fixed_vars(j, k); }); + m_solver = alloc(lp::lar_solver); // initialize 0, 1 variables: get_one(true); get_one(false); @@ -1274,10 +1285,10 @@ public: theory_var z = internalize_def(term); lpvar zi = register_theory_var_in_lar_solver(z); lpvar vi = register_theory_var_in_lar_solver(v); - add_def_constraint(lp().add_var_bound(zi, lp::GE, rational::zero())); - add_def_constraint(lp().add_var_bound(zi, lp::LE, rational::zero())); - add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); - add_def_constraint(lp().add_var_bound(vi, lp::LT, abs(r))); + add_def_constraint_and_equality(zi, lp::GE, rational::zero()); + add_def_constraint_and_equality(zi, lp::LE, rational::zero()); + add_def_constraint_and_equality(vi, lp::GE, rational::zero()); + add_def_constraint_and_equality(vi, lp::LT, abs(r)); SASSERT(!is_infeasible()); TRACE("arith", tout << term << "\n" << lp().constraints();); }