From a59745c2f2509ba3537fd391b5c2e8eda0516eeb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Feb 2020 09:13:40 -0800 Subject: [PATCH] isolate constraints in a constraint_set Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_solver.cpp | 8 +- src/math/lp/lar_constraints.h | 152 +++++++++++++++++++++++++++++----- src/math/lp/lar_solver.cpp | 144 +++++++------------------------- src/math/lp/lar_solver.h | 33 ++++---- src/math/lp/nla_core.cpp | 10 +-- src/math/lp/nra_solver.cpp | 4 +- src/smt/theory_lra.cpp | 14 ++-- 7 files changed, 192 insertions(+), 173 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 3db3e3c00..62516c91b 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -238,7 +238,7 @@ lia_move int_solver::find_cube() { TRACE("cube", for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) display_column(tout, j); - m_lar_solver->print_constraints(tout); + tout << m_lar_solver->constraints(); ); m_lar_solver->push(); @@ -357,9 +357,9 @@ lia_move int_solver::make_hnf_cut() { settings().stats().m_hnf_cutter_calls++; TRACE("hnf_cut", tout << "settings().stats().m_hnf_cutter_calls = " << settings().stats().m_hnf_cutter_calls << "\n"; for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_lar_solver->print_constraint(i, tout); + m_lar_solver->constraints().display(tout, i); } - m_lar_solver->print_constraints(tout); + tout << m_lar_solver->constraints(); ); #ifdef Z3DEBUG vector x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x); @@ -373,7 +373,7 @@ lia_move int_solver::make_hnf_cut() { m_lar_solver->print_term(m_t, tout << "cut:"); tout << " <= " << m_k << std::endl; for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_lar_solver->print_constraint(i, tout); + m_lar_solver->constraints().display(tout, i); } ); lp_assert(current_solution_is_inf_on_cut()); diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 931f46687..96c23038f 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -19,14 +19,17 @@ Revision History: --*/ #pragma once -#include "util/vector.h" #include -#include #include #include + +#include "util/vector.h" +#include "util/region.h" #include "math/lp/lp_utils.h" #include "math/lp/ul_pair.h" #include "math/lp/lar_term.h" +#include "math/lp/column_namer.h" +#include "math/lp/stacked_value.h" namespace lp { inline lconstraint_kind flip_kind(lconstraint_kind t) { return static_cast( - static_cast(t)); @@ -57,8 +60,9 @@ struct lar_base_constraint { virtual mpq get_free_coeff_of_left_side() const { return zero_of_type();} }; -struct lar_var_constraint: public lar_base_constraint { +class lar_var_constraint: public lar_base_constraint { unsigned m_j; +public: vector> coeffs() const override { vector> ret; ret.push_back(std::make_pair(one_of_type(), m_j)); @@ -69,32 +73,136 @@ struct lar_var_constraint: public lar_base_constraint { }; -struct lar_term_constraint: public lar_base_constraint { +class lar_term_constraint: public lar_base_constraint { const lar_term * m_term; - vector> coeffs() const override { - return m_term->coeffs_as_vector(); - } +public: + vector> coeffs() const override { return m_term->coeffs_as_vector(); } unsigned size() const override { return m_term->size();} lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { } - // mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} - }; -class lar_constraint : public lar_base_constraint { +class constraint_set { + region m_region; + column_namer& m_namer; + vector m_constraints; + stacked_value m_constraint_count; + + constraint_index add(lar_base_constraint* c) { + constraint_index ci = m_constraints.size(); + m_constraints.push_back(c); + return ci; + } + + std::ostream& print_left_side_of_constraint(const lar_base_constraint & c, std::ostream & out) const { + m_namer.print_linear_combination_of_column_indices(c.coeffs(), out); + mpq free_coeff = c.get_free_coeff_of_left_side(); + if (!is_zero(free_coeff)) + out << " + " << free_coeff; + return out; + } + + std::ostream& print_left_side_of_constraint_indices_only(const lar_base_constraint & c, std::ostream & out) const { + print_linear_combination_of_column_indices_only(c.coeffs(), out); + mpq free_coeff = c.get_free_coeff_of_left_side(); + if (!is_zero(free_coeff)) + out << " + " << free_coeff; + return out; + } + + std::ostream& print_left_side_of_constraint(const lar_base_constraint & c, std::function& var_str, std::ostream & out) const { + print_linear_combination_customized(c.coeffs(), var_str, out); + mpq free_coeff = c.get_free_coeff_of_left_side(); + if (!is_zero(free_coeff)) + out << " + " << free_coeff; + return out; + } + + std::ostream& out_of_bounds(std::ostream& out, constraint_index ci) const { + return out << "constraint " << T_to_string(ci) << " is not found" << std::endl; + } + public: - vector> m_coeffs; - lar_constraint(const vector> & left_side, lconstraint_kind kind, const mpq & right_side) - : lar_base_constraint(kind, right_side), m_coeffs(left_side) {} + constraint_set(column_namer& cn): + m_namer(cn) {} + + ~constraint_set() { + for (auto* c : m_constraints) + c->~lar_base_constraint(); + } + + void push() { + m_constraint_count = m_constraints.size(); + m_constraint_count.push(); + m_region.push_scope(); + } + + void pop(unsigned k) { + m_constraint_count.pop(k); + for (unsigned i = m_constraints.size(); i-- > m_constraint_count; ) + m_constraints[i]->~lar_base_constraint(); + m_constraints.shrink(m_constraint_count); + m_region.pop_scope(k); + } + + constraint_index add_var_constraint(var_index j, lconstraint_kind k, mpq const& rhs) { + return add(new (m_region) lar_var_constraint(j, k, rhs)); + } + + constraint_index add_term_constraint(const lar_term* t, lconstraint_kind k, mpq const& rhs) { + return add(new (m_region) lar_term_constraint(t, k, rhs)); + } + + lar_base_constraint const& operator[](constraint_index ci) const { return *m_constraints[ci]; } + + // TBD: would like to make this opaque + // and expose just active constraints + // constraints need not be active. + unsigned size() const { return m_constraints.size(); } + vector::const_iterator begin() const { return m_constraints.begin(); } + vector::const_iterator end() const { return m_constraints.end(); } + + std::ostream& display(std::ostream& out) const { + out << "number of constraints = " << m_constraints.size() << std::endl; + for (auto const* c : *this) { + display(out, *c); + } + return out; + } + + std::ostream& display(std::ostream& out, constraint_index ci) const { + return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display(out, (*this)[ci]); + } + + std::ostream& display(std::ostream& out, lar_base_constraint const& c) const { + print_left_side_of_constraint(c, out); + return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl; + } + + std::ostream& display_indices_only(std::ostream& out, constraint_index ci) const { + return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display_indices_only(out, (*this)[ci]); + } + + std::ostream& display_indices_only(std::ostream& out, lar_base_constraint const& c) const { + print_left_side_of_constraint_indices_only(c, out); + return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl; + } + + std::ostream& display(std::ostream& out, std::function var_str, constraint_index ci) const { + return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display(out, var_str, (*this)[ci]); + } + + std::ostream& display(std::ostream& out, std::function& var_str, lar_base_constraint const& c) const { + print_left_side_of_constraint(c, var_str, out); + return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl; + } + + - lar_constraint(const lar_base_constraint & c) { - lp_assert(false); // should not be called : todo! - } - - unsigned size() const override { - return static_cast(m_coeffs.size()); - } - - vector> coeffs() const override { return m_coeffs; } }; + +inline std::ostream& operator<<(std::ostream& out, constraint_set const& cs) { + return cs.display(out); +} + } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index c18ee75ba..3ab51c9cc 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -6,13 +6,6 @@ namespace lp { -unsigned lar_solver::constraint_count() const { - return m_constraints.size(); -} -const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const { - return *(m_constraints[ci]); -} - ////////////////// methods //////////////////////////////// static_matrix> & lar_solver::A_r() { return m_mpq_lar_core_solver.m_r_A;} static_matrix> const & lar_solver::A_r() const { return m_mpq_lar_core_solver.m_r_A;} @@ -34,6 +27,7 @@ lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_terms_start_index(1000000), m_var_register(0), m_term_register(m_terms_start_index), + m_constraints(*this), m_need_register_terms(false) {} @@ -47,8 +41,6 @@ bool lar_solver::get_track_pivoted_rows() const { lar_solver::~lar_solver(){ - for (auto c : m_constraints) - delete c; for (auto t : m_terms) delete t; @@ -107,7 +99,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, for (auto & it : explanation) { mpq coeff = it.first; constraint_index con_ind = it.second; - const auto & constr = *m_constraints[con_ind]; + const auto & constr = m_constraints[con_ind]; lconstraint_kind kind = coeff.is_pos() ? constr.m_kind : flip_kind(constr.m_kind); register_in_map(coeff_map, constr, coeff); if (kind == GT || kind == LT) @@ -329,6 +321,7 @@ vector lar_solver::get_list_of_all_var_indices() const { ret.push_back(j); return ret; } + void lar_solver::push() { m_simplex_strategy = m_settings.simplex_strategy(); m_simplex_strategy.push(); @@ -337,8 +330,7 @@ void lar_solver::push() { m_mpq_lar_core_solver.push(); m_term_count = m_terms.size(); m_term_count.push(); - m_constraint_count = m_constraints.size(); - m_constraint_count.push(); + m_constraints.push(); } void lar_solver::clean_popped_elements(unsigned n, int_set& set) { @@ -383,11 +375,7 @@ void lar_solver::pop(unsigned k) { (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - m_constraint_count.pop(k); - for (unsigned i = m_constraint_count; i < m_constraints.size(); i++) - delete m_constraints[i]; - - m_constraints.resize(m_constraint_count); + m_constraints.pop(k); m_term_count.pop(k); for (unsigned i = m_term_count; i < m_terms.size(); i++) { if (m_need_register_terms) @@ -402,14 +390,7 @@ void lar_solver::pop(unsigned k) { lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); set_status(lp_status::UNKNOWN); } - -vector lar_solver::get_all_constraint_indices() const { - vector ret; - constraint_index i = 0; - while ( i < m_constraints.size()) - ret.push_back(i++); - return ret; -} + bool lar_solver::maximize_term_on_tableau(const lar_term & term, impq &term_max) { @@ -934,9 +915,6 @@ bool lar_solver::var_is_registered(var_index vj) const { return true; } -unsigned lar_solver::constraint_stack_size() const { - return m_constraint_count.stack_size(); -} void lar_solver::fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls) { lp_assert(A.row_count() > 0); @@ -1003,16 +981,18 @@ bool lar_solver::all_constraints_hold() const { std::unordered_map var_map; get_model_do_not_care_about_diff_vars(var_map); - for (unsigned i = 0; i < m_constraints.size(); i++) { - if (!constraint_holds(*m_constraints[i], var_map)) { + unsigned i = 0; + for (auto const* c : m_constraints) { + if (!constraint_holds(*c, var_map)) { TRACE("lar_solver", tout << "i = " << i << "; "; - print_constraint(m_constraints[i], tout) << "\n"; - for(auto p : m_constraints[i]->coeffs()) { + m_constraints.display(tout, *c) << "\n"; + for (auto p : c->coeffs()) { m_mpq_lar_core_solver.m_r_solver.print_column_info(p.second, tout); }); return false; } + ++i; } return true; } @@ -1038,8 +1018,8 @@ bool lar_solver::the_relations_are_of_same_type(const vectorm_kind : - flip_kind(m_constraints[con_ind]->m_kind); + m_constraints[con_ind].m_kind : + flip_kind(m_constraints[con_ind].m_kind); if (kind == GT || kind == LT) strict = true; if (kind == GE || kind == GT) @@ -1074,7 +1054,7 @@ bool lar_solver::the_left_sides_sum_to_zero(const vector> & evidence) { - mpq ret = numeric_traits::zero(); - for (auto & it : evidence) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lp_assert(con_ind < m_constraints.size()); - const lar_constraint & constr = *m_constraints[con_ind]; - ret += constr.m_right_side * coeff; - } - return !numeric_traits::is_zero(ret); -} bool lar_solver::explanation_is_correct(explanation& explanation) const { return true; @@ -1139,7 +1108,7 @@ mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const { mpq coeff = it.first; constraint_index con_ind = it.second; lp_assert(con_ind < m_constraints.size()); - ret += (m_constraints[con_ind]->m_right_side - m_constraints[con_ind]->get_free_coeff_of_left_side()) * coeff; + ret += (m_constraints[con_ind].m_right_side - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff; } return ret; } @@ -1318,41 +1287,19 @@ std::string lar_solver::get_variable_name(var_index j) const { // ********** print region start std::ostream& lar_solver::print_constraint(constraint_index ci, std::ostream & out) const { - if (ci >= m_constraints.size()) { - out << "constraint " << T_to_string(ci) << " is not found"; - out << std::endl; - return out; - } - - return print_constraint(m_constraints[ci], out); + return m_constraints.display(out, ci); } std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std::ostream & out) const { - if (ci >= m_constraints.size()) { - out << "constraint " << T_to_string(ci) << " is not found"; - out << std::endl; - return out; - } - - return print_constraint_indices_only(m_constraints[ci], out); + return m_constraints.display_indices_only(out, ci); } std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const { - if (ci >= m_constraints.size()) { - out << "constraint " << T_to_string(ci) << " is not found"; - out << std::endl; - return out; - } - - return print_constraint_indices_only_customized(m_constraints[ci], var_str, out); + return m_constraints.display(out, var_str, ci); } std::ostream& lar_solver::print_constraints(std::ostream& out) const { - out << "number of constraints = " << m_constraints.size() << std::endl; - for (auto c : m_constraints) { - print_constraint(c, out); - } - return out; + return out << m_constraints; } std::ostream& lar_solver::print_terms(std::ostream& out) const { @@ -1362,22 +1309,6 @@ std::ostream& lar_solver::print_terms(std::ostream& out) const { return out; } -std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const { - print_linear_combination_of_column_indices(c->coeffs(), out); - mpq free_coeff = c->get_free_coeff_of_left_side(); - if (!is_zero(free_coeff)) - out << " + " << free_coeff; - return out; -} - -std::ostream& lar_solver::print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const { - print_linear_combination_of_column_indices_only(c->coeffs(), out); - mpq free_coeff = c->get_free_coeff_of_left_side(); - if (!is_zero(free_coeff)) - out << " + " << free_coeff; - return out; -} - std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const { if (term.size() == 0){ out << "0"; @@ -1419,21 +1350,6 @@ mpq lar_solver::get_left_side_val(const lar_base_constraint & cns, const std::u return ret; } -std::ostream& lar_solver::print_constraint(const lar_base_constraint * c, std::ostream & out) const { - print_left_side_of_constraint(c, out); - return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; -} - -std::ostream& lar_solver::print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const { - print_left_side_of_constraint_indices_only(c, out); - return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; -} - -std::ostream& lar_solver::print_constraint_indices_only_customized(const lar_base_constraint * c, - std::function var_str, std::ostream & out) const { - print_linear_combination_customized(c->coeffs(), var_str, out); - return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; -} void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { for (unsigned i = 0; i < sz; i++) { @@ -1867,15 +1783,14 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;); - constraint_index ci = m_constraints.size(); + constraint_index ci; if (!is_term(j)) { // j is a var lp_assert(bound_is_integer_for_integer_column(j, right_side)); - auto vc = new lar_var_constraint(j, kind, right_side); - m_constraints.push_back(vc); + ci = m_constraints.add_var_constraint(j, kind, right_side); update_column_type_and_bound(j, kind, right_side, ci); } else { - add_var_bound_on_constraint_for_term(j, kind, right_side, ci); + ci = add_var_bound_on_constraint_for_term(j, kind, right_side); } lp_assert(sizes_are_correct()); return ci; @@ -1908,28 +1823,31 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); } -void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { +constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) { lp_assert(is_term(j)); unsigned adjusted_term_index = adjust_term_index(j); // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; + constraint_index ci; if (m_var_register.external_is_used(j, term_j)) { - m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); + ci = m_constraints.add_term_constraint(m_terms[adjusted_term_index], kind, right_side); update_column_type_and_bound(term_j, kind, right_side, ci); } else { - add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); + ci = add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); } + return ci; } -void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, +constraint_index lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, lconstraint_kind kind, const mpq & right_side) { add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; + constraint_index ci = m_constraints.add_term_constraint(term, kind, right_side); update_column_type_and_bound(j, kind, right_side, m_constraints.size()); - m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + return ci; } void lar_solver::decide_on_strategy_and_adjust_initial_state() { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 588befcd7..dd711b2c5 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -25,15 +25,15 @@ Revision History: #include #include #include -#include "math/lp/lar_constraints.h" -#include -#include "math/lp/lar_core_solver.h" #include +#include +#include +#include "math/lp/lar_constraints.h" +#include "math/lp/lar_core_solver.h" #include "math/lp/numeric_pair.h" #include "math/lp/scaler.h" #include "math/lp/lp_primal_core_solver.h" #include "math/lp/random_updater.h" -#include #include "math/lp/stacked_value.h" #include "math/lp/stacked_vector.h" #include "math/lp/implied_bound.h" @@ -91,8 +91,11 @@ public: var_register m_var_register; var_register m_term_register; stacked_vector m_columns_to_ul_pairs; + constraint_set m_constraints; +#if 0 vector m_constraints; stacked_value m_constraint_count; +#endif // the set of column indices j such that bounds have changed for j int_set m_columns_with_changed_bound; int_set m_rows_with_changed_bounds; @@ -112,7 +115,7 @@ public: unsigned terms_start_index() const { return m_terms_start_index; } const vector & terms() const { return m_terms; } lar_term const& term(unsigned i) const { return *m_terms[i]; } - const vector& constraints() const { + constraint_set const& constraints() const { return m_constraints; } void set_int_solver(int_solver * int_slv) { @@ -121,8 +124,7 @@ public: int_solver * get_int_solver() { return m_int_solver; } - unsigned constraint_count() const; - const lar_base_constraint& get_constraint(unsigned ci) const; + const lar_base_constraint& get_constraint(unsigned ci) const { return m_constraints[ci]; } ////////////////// methods //////////////////////////////// static_matrix> & A_r(); static_matrix> const & A_r() const; @@ -204,15 +206,15 @@ public: 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 add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); + + constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side); void set_infeasible_column(unsigned j) { set_status(lp_status::INFEASIBLE); m_infeasible_column = j; } - void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, + constraint_index add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, lconstraint_kind kind, const mpq & right_side); unsigned row_of_basic_column(unsigned) const; @@ -342,8 +344,6 @@ public: void pop(unsigned k); - vector get_all_constraint_indices() const; - bool maximize_term_on_tableau(const lar_term & term, impq &term_max); @@ -432,8 +432,6 @@ public: bool var_is_registered(var_index vj) const; - unsigned constraint_stack_size() const; - void fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls); template @@ -491,6 +489,7 @@ public: void set_variable_name(var_index vi, std::string); // ********** print region start + private: std::ostream& print_constraint(constraint_index ci, std::ostream & out) const; std::ostream& print_constraints(std::ostream& out) const ; @@ -500,18 +499,14 @@ public: std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const; std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function var_str, std::ostream & out) const; + public: std::ostream& print_terms(std::ostream& out) const; - std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const; - - std::ostream& print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const; - std::ostream& print_term(lar_term const& term, std::ostream & out) const; static std::ostream& print_term_as_indices(lar_term const& term, std::ostream & out); - std::ostream& print_constraint(const lar_base_constraint * c, std::ostream & out) const; std::ostream& print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const; std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f87497067..bc5ccce84 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -286,9 +286,7 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& unsigned i = 0; for (auto &p : exp) { out << "(" << p.second << ")"; - m_lar_solver.print_constraint_indices_only_customized(p.second, - [this](lpvar j) { return var_str(j);}, - out); + m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.second); if (++i < exp.size()) out << " "; } @@ -520,8 +518,8 @@ void core:: fill_explanation_and_lemma_sign(const monic& a, const monic & b, rat TRACE("nla_solver", tout << "used constraints: "; for (auto &p : current_expl()) - m_lar_solver.print_constraint(p.second, tout); tout << "\n"; - ); + m_lar_solver.constraints().display(tout, p.second); tout << "\n"; + ); SASSERT(current_ineqs().size() == 0); mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero()); TRACE("nla_solver", print_lemma(tout);); @@ -1258,7 +1256,7 @@ bool core::done() const { } lbool core::incremental_linearization(bool constraint_derived) { - TRACE("nla_solver_details", print_terms(tout); m_lar_solver.print_constraints(tout);); + TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints();); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 830dfd12e..4cf1fb082 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -92,7 +92,7 @@ typedef nla::variable_map_type variable_map_type; vector core; // add linear inequalities from lra_solver - for (unsigned i = 0; i < s.constraint_count(); ++i) { + for (unsigned i = 0; i < s.constraints().size(); ++i) { add_constraint(i); } @@ -154,7 +154,7 @@ typedef nla::variable_map_type variable_map_type; } void add_constraint(unsigned idx) { - auto& c = s.get_constraint(idx); + auto& c = s.constraints()[idx]; auto& pm = m_nlsat->pm(); auto k = c.m_kind; auto rhs = c.m_right_side; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3ebca8673..3437366b4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -841,7 +841,7 @@ class theory_lra::imp { m_constraint_sources.setx(index, inequality_source, null_source); m_inequalities.setx(index, lit, null_literal); ++m_stats.m_add_rows; - TRACE("arith", lp().print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); + TRACE("arith", lp().constraints().display(tout, index) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); } void add_def_constraint(lp::constraint_index index) { @@ -1288,7 +1288,7 @@ public: add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero())); add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r))); SASSERT(!is_infeasible()); - TRACE("arith", lp().print_constraints(tout << term << "\n");); + TRACE("arith", tout << term << "\n" << lp().constraints();); } void mk_idiv_mod_axioms(expr * p, expr * q) { @@ -2029,7 +2029,7 @@ public: } expr_ref constraint2fml(lp::constraint_index ci) { - lp::lar_base_constraint const& c = *lp().constraints()[ci]; + lp::lar_base_constraint const& c = lp().constraints()[ci]; expr_ref fml(m); expr_ref_vector ts(m); rational rhs = c.m_right_side; @@ -2063,7 +2063,7 @@ public: } } for (auto const& ev : ex) { - lp().print_constraint(ev.second, out << ev.first << ": "); + lp().constraints().display(out << ev.first << ": ", ev.second); } expr_ref_vector fmls(m); for (auto const& ev : ex) { @@ -3242,7 +3242,7 @@ public: } lbool make_feasible() { - TRACE("pcs", lp().print_constraints(tout);); + TRACE("pcs", tout << lp().constraints();); auto status = lp().find_feasible_solution(); TRACE("arith_verbose", display(tout);); switch (status) { @@ -3787,7 +3787,7 @@ public: void display(std::ostream & out) { if (m_solver) { - lp().print_constraints(out); + out << lp().constraints(); lp().print_terms(out); // the tableau auto pp = lp ::core_solver_pretty_printer( @@ -3842,7 +3842,7 @@ public: } } for (auto const& ev : evidence) { - lp().print_constraint(ev.second, out << ev.first << ": "); + lp().constraints().display(out << ev.first << ": ", ev.second); } }