diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 8cbd83801..a425460f9 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -95,7 +95,6 @@ public: unsigned size() const override { return m_term->size();} }; - class constraint_set { region m_region; column_namer& m_namer; @@ -151,20 +150,16 @@ public: m_constraint_count = m_constraints.size(); m_constraint_count.push(); m_region.push_scope(); -#if 1 m_active_lim = m_active.size(); m_active_lim.push(); -#endif } void pop(unsigned k) { -#if 1 m_active_lim.pop(k); for (unsigned i = m_active.size(); i-- > m_active_lim; ) { m_constraints[m_active[i]]->deactivate(); } m_active.shrink(m_active_lim); -#endif m_constraint_count.pop(k); for (unsigned i = m_constraints.size(); i-- > m_constraint_count; ) m_constraints[i]->~lar_base_constraint(); @@ -181,17 +176,10 @@ public: return add(new (m_region) lar_term_constraint(j, t, k, rhs)); } -#if 0 - bool is_active(constraint_index ci) const { return true; } - - void activate(constraint_index ci) {} - -#else // future behavior uses activation bit. bool is_active(constraint_index ci) const { return m_constraints[ci]->is_active(); } void activate(constraint_index ci) { auto& c = *m_constraints[ci]; if (!c.is_active()) { c.activate(); m_active.push_back(ci); } } -#endif lar_base_constraint const& operator[](constraint_index ci) const { return *m_constraints[ci]; } @@ -283,9 +271,6 @@ public: print_left_side_of_constraint(c, var_str, out); return out << " " << lconstraint_kind_string(c.kind()) << " " << c.rhs() << std::endl; } - - - }; inline std::ostream& operator<<(std::ostream& out, constraint_set const& cs) { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 4b915d769..dd97aa957 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -18,14 +18,16 @@ void clear() {lp_assert(false); // not implemented } -lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), - m_crossed_bounds_column(-1), - m_mpq_lar_core_solver(m_settings, *this), - m_int_solver(nullptr), - m_need_register_terms(false), - m_var_register(false), - m_term_register(true), - m_constraints(*this) +lar_solver::lar_solver(const std::function& report_equality_of_fixed_vars) : + m_status(lp_status::UNKNOWN), + m_crossed_bounds_column(-1), + m_mpq_lar_core_solver(m_settings, *this), + m_int_solver(nullptr), + 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) {} void lar_solver::set_track_pivoted_rows(bool v) { @@ -271,6 +273,7 @@ void lar_solver::pop(unsigned k) { m_columns_to_ul_pairs.pop(k); m_mpq_lar_core_solver.pop(k); + remove_non_fixed_from_fixed_var_table(); clean_popped_elements(n, m_columns_with_changed_bound); clean_popped_elements(n, m_incorrect_columns); @@ -1721,6 +1724,36 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c return ci; } +void lar_solver::remove_non_fixed_from_fixed_var_table() { + vector to_remove; + for (const auto& p : m_fixed_var_table) { + unsigned j = p.m_value; + if (j >= column_count() || column_is_fixed(j) == false) + to_remove.push_back(p.m_key); + } + for (const auto & p : to_remove) + m_fixed_var_table.erase(p); +} + +void lar_solver::register_in_fixed_var_table(unsigned j) { + SASSERT(column_is_fixed(j)); + const impq& bound = get_lower_bound(j); + if (bound.y.is_zero() == false) + return; + + value_sort_pair key(bound.x, column_is_int(j)); + unsigned k; + if (m_fixed_var_table.find(key, k) == false ) { + m_fixed_var_table.insert(key, 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)); +} + void lar_solver::activate(constraint_index ci) { auto const& c = m_constraints[ci]; update_column_type_and_bound(c.column(), c.kind(), c.rhs(), ci); @@ -1784,13 +1817,19 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq & } } -void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, +void lar_solver::update_column_type_and_bound(var_index j, + lconstraint_kind kind, + const mpq & right_side, constraint_index constr_index) { m_constraints.activate(constr_index); if (column_has_upper_bound(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); + if (column_is_fixed(j)) { + register_in_fixed_var_table(j); + } + } constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 8341a8c98..94bf3857a 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -49,6 +49,8 @@ namespace lp { class int_branch; class int_solver; class lar_solver : public column_namer { + typedef std::pair value_sort_pair; + typedef pair_hash, bool_hash> value_sort_pair_hash; struct term_hasher { std::size_t operator()(const lar_term &t) const { @@ -102,6 +104,12 @@ class lar_solver : public column_namer { m_normalized_terms_to_columns; vector m_backup_x; stacked_vector m_usage_in_terms; + // ((x[j], is_int(j))->j) for fixed j, used in equalities propagation + map> m_fixed_var_table; + std::function m_report_equality_of_fixed_vars; // end of fields ////////////////// methods //////////////////////////////// @@ -142,7 +150,8 @@ class lar_solver : public column_namer { 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 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) { set_status(lp_status::INFEASIBLE); @@ -281,6 +290,18 @@ class lar_solver : public column_namer { void register_normalized_term(const lar_term&, lpvar); void deregister_normalized_term(const lar_term&); public: + const map>& fixed_var_table() const { + return m_fixed_var_table; + } + map>& fixed_var_table() { + return m_fixed_var_table; + } unsigned external_to_column_index(unsigned) const; bool inside_bounds(lpvar, const impq&) const; inline void set_column_value(unsigned j, const impq& v) { @@ -572,7 +593,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(); + lar_solver(const std::function & report_equality_of_fixed_vars); void set_track_pivoted_rows(bool v); bool get_track_pivoted_rows() const; virtual ~lar_solver(); diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index a51b0fe41..e28410b06 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -325,19 +325,9 @@ public: if (y == null_lpvar) { // x is an implied fixed var at k. value_sort_pair key(k, is_int(x)); - int x2; - if (m_imp.m_fixed_var_table.find(key, x2) && - x2 < static_cast(m_imp.get_num_vars()) - && - lp().column_is_fixed(x2 = imp_to_col(x2)) && // change x2 - get_lower_bound_rational(x2) == k && - // We must check whether x2 is an integer. - // The table m_fixed_var_table is not restored during backtrack. So, it may - // contain invalid (key -> value) pairs. - // So, we must check whether x2 is really equal to k (previous test) - // AND has the same sort of x. - is_int(x) == is_int(x2) && - !is_equal(x, x2)) { + unsigned x2; + if (lp().fixed_var_table().find(key, x2) && !is_equal(x, x2)) { + SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k && is_int(x) == is_int(x2)); explanation ex; constraint_index lc, uc; lp().get_bound_constraint_witnesses_for_column(x2, lc, uc); diff --git a/src/math/lp/mps_reader.h b/src/math/lp/mps_reader.h index f165b08b3..550b968b5 100644 --- a/src/math/lp/mps_reader.h +++ b/src/math/lp/mps_reader.h @@ -883,7 +883,7 @@ public: } lar_solver * create_lar_solver() { - lar_solver * solver = new lar_solver(); + lar_solver * solver = new lar_solver([](unsigned, unsigned) { }); fill_lar_solver(solver); return solver; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 54c0d2aab..90ec8f33d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -327,42 +327,7 @@ class theory_lra::imp { bool is_real(enode* n) const { return a.is_real(n->get_owner()); } enode* get_enode(theory_var v) const { return th.get_enode(v); } enode* get_enode(expr* e) const { return ctx().get_enode(e); } - expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } - - void init_solver() { - if (m_solver) return; - - reset_variable_values(); - m_solver = alloc(lp::lar_solver); - - // initialize 0, 1 variables: - get_one(true); - get_one(false); - get_zero(true); - get_zero(false); - - smt_params_helper lpar(ctx().get_params()); - lp().settings().set_resource_limit(m_resource_limit); - lp().settings().simplex_strategy() = static_cast(lpar.arith_simplex_strategy()); - lp().settings().bound_propagation() = BP_NONE != propagation_mode(); - lp().settings().enable_hnf() = lpar.arith_enable_hnf(); - lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names(); - lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows()); - lp().settings().report_frequency = lpar.arith_rep_freq(); - lp().settings().print_statistics = lpar.arith_print_stats(); - - // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts - unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; - lp().set_cut_strategy(branch_cut_ratio); - - lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; - lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); - m_lia = alloc(lp::int_solver, *m_solver.get()); - get_one(true); - get_zero(true); - get_one(false); - get_zero(false); - } + expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } lpvar add_const(int c, lpvar& var, bool is_int) { if (var != UINT_MAX) { @@ -371,7 +336,7 @@ class theory_lra::imp { app_ref cnst(a.mk_numeral(rational(c), is_int), m); mk_enode(cnst); theory_var v = mk_var(cnst); - var = lp().add_var(v, true); + 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))); @@ -933,10 +898,6 @@ class theory_lra::imp { } } - rational val; - if (a.is_numeral(term, val)) { - m_fixed_var_table.insert(value_sort_pair(val, is_int(v)), v); - } return v; } } @@ -976,8 +937,7 @@ public: if (m_solver) return; reset_variable_values(); - m_solver = alloc(lp::lar_solver); - + m_solver = alloc(lp::lar_solver, [&](unsigned j, unsigned k) { report_equality_of_fixed_vars(j, k); }); // initialize 0, 1 variables: get_one(true); get_one(false); @@ -3055,10 +3015,6 @@ public: typedef std::pair constraint_bound; vector m_lower_terms; vector m_upper_terms; - typedef std::pair value_sort_pair; - typedef pair_hash, bool_hash> value_sort_pair_hash; - typedef map > value2var; - value2var m_fixed_var_table; void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) { if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) { @@ -3191,62 +3147,61 @@ public: } unsigned get_num_vars() const { return th.get_num_vars(); } + + void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) { + lp::constraint_index ci1, ci2, ci3, ci4; + theory_var v1 = lp().local_to_external(vi1); + theory_var v2 = lp().local_to_external(vi2); + if (is_equal(v1, v2)) + return; + SASSERT(is_int(v1) == is_int(v2)); + + lp::mpq bound; + TRACE("arith", + bool hlb = has_lower_bound(vi2, ci3, bound); // has_lower_bound in turn trace "arith" + tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;); + if (!(has_lower_bound(vi2, ci3, bound) + && + has_upper_bound(vi2, ci4, bound) + && + has_lower_bound(vi1, ci1, bound) + && + has_upper_bound(vi1, ci2, bound))) { + TRACE("arith", tout << "strange\n";); + return; + } + ++m_stats.m_fixed_eqs; + reset_evidence(); + set_evidence(ci1, m_core, m_eqs); + set_evidence(ci2, m_core, m_eqs); + set_evidence(ci3, m_core, m_eqs); + set_evidence(ci4, m_core, m_eqs); + enode* x = get_enode(v1); + enode* y = get_enode(v2); + justification* js = + ctx().mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); + + TRACE("arith", + for (unsigned i = 0; i < m_core.size(); ++i) { + ctx().display_detailed_literal(tout, m_core[i]); + tout << "\n"; + } + for (unsigned i = 0; i < m_eqs.size(); ++i) { + tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n"; + } + tout << " ==> "; + tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n"; + ); + + // parameters are TBD. + // SASSERT(validate_eq(x, y)); + ctx().assign_eq(x, y, eq_justification(js)); + } void fixed_var_eh(theory_var v1, rational const& bound) { - // IF_VERBOSE(0, verbose_stream() << "fix " << mk_bounded_pp(get_owner(v1), m) << " " << bound << "\n"); - - theory_var v2; - value_sort_pair key(bound, is_int(v1)); - if (m_fixed_var_table.find(key, v2)) { - if (static_cast(v2) < th.get_num_vars() && !is_equal(v1, v2) && is_int(v1) == is_int(v2)) { - auto vi1 = register_theory_var_in_lar_solver(v1); - auto vi2 = register_theory_var_in_lar_solver(v2); - lp::constraint_index ci1, ci2, ci3, ci4; - - TRACE("arith", - bool hlb = has_lower_bound(vi2, ci3, bound); // has_lower_bound in turn trace "arith" - tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;); - if (has_lower_bound(vi2, ci3, bound) && has_upper_bound(vi2, ci4, bound)) { - VERIFY (has_lower_bound(vi1, ci1, bound)); - VERIFY (has_upper_bound(vi1, ci2, bound)); - ++m_stats.m_fixed_eqs; - reset_evidence(); - set_evidence(ci1, m_core, m_eqs); - set_evidence(ci2, m_core, m_eqs); - set_evidence(ci3, m_core, m_eqs); - set_evidence(ci4, m_core, m_eqs); - enode* x = get_enode(v1); - enode* y = get_enode(v2); - justification* js = - ctx().mk_justification( - ext_theory_eq_propagation_justification( - get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); - - TRACE("arith", - for (unsigned i = 0; i < m_core.size(); ++i) { - ctx().display_detailed_literal(tout, m_core[i]); - tout << "\n"; - } - for (unsigned i = 0; i < m_eqs.size(); ++i) { - tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n"; - } - tout << " ==> "; - tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n"; - ); - - // parameters are TBD. - // SASSERT(validate_eq(x, y)); - ctx().assign_eq(x, y, eq_justification(js)); - } - } - else { - // bounds on v2 were changed. - m_fixed_var_table.insert(key, v1); - } - } - else { - m_fixed_var_table.insert(key, v1); - } + // no op } lbool make_feasible() {