From 5208b64a6ba4589a2b19c0e45c97a51774955a72 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 Apr 2020 12:59:24 -0700 Subject: [PATCH] expose only necessary methods of lar_solver Signed-off-by: Lev Nachmanson --- src/math/lp/gomory.cpp | 2 +- src/math/lp/hnf_cutter.cpp | 23 +- src/math/lp/int_branch.cpp | 2 +- src/math/lp/int_branch.h | 2 + src/math/lp/int_cube.cpp | 2 +- src/math/lp/int_gcd_test.cpp | 9 +- src/math/lp/int_gcd_test.h | 2 +- src/math/lp/int_solver.cpp | 4 - src/math/lp/lar_solver.cpp | 6 - src/math/lp/lar_solver.h | 428 +++++++++++----------------- src/math/lp/lp_bound_propagator.cpp | 6 +- src/math/lp/lp_core_solver_base.h | 3 +- src/math/lp/nla_core.cpp | 10 +- src/math/lp/nla_core.h | 6 +- src/math/lp/random_updater_def.h | 8 +- src/smt/theory_lra.cpp | 6 +- 16 files changed, 217 insertions(+), 302 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 135eafff2b8..a481f1668a9 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -282,7 +282,7 @@ class create_cut { void dump(std::ostream& out) { out << "applying cut at:\n"; print_linear_combination_indices_only, mpq>(m_row, out); out << std::endl; for (auto & p : m_row) { - lia.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out); + lia.lra.print_column_info(p.var(), out); } out << "inf_col = " << m_inf_col << std::endl; } diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 71e888d3962..c7728474a2d 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -155,10 +155,12 @@ namespace lp { bool hnf_cutter::overflow() const { return m_overflow; } - lia_move hnf_cutter::create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector & x0) { - // we suppose that x0 has at least one non integer element - (void)x0; - + lia_move hnf_cutter::create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper +#ifdef Z3DEBUG + , const vector & x0 + // we suppose that x0 has at least one non integer element +#endif + ) { init_matrix_A(); svector basis_rows; mpq big_number = m_abs_max.expt(3); @@ -179,7 +181,10 @@ namespace lp { hnf h(m_A, d); vector b = create_b(basis_rows); +#ifdef Z3DEBUG lp_assert(m_A * x0 == b); +#endif + find_h_minus_1_b(h.W(), b); int cut_row = find_cut_row_index(b); @@ -238,11 +243,13 @@ namespace lp { tout << lra.constraints(); ); #ifdef Z3DEBUG - vector x0 = transform_to_local_columns(lra.m_mpq_lar_core_solver.m_r_x); -#else - vector x0; + vector x0 = transform_to_local_columns(lra.r_x()); +#endif + lia_move r = create_cut(lia.m_t, lia.m_k, lia.m_ex, lia.m_upper +#ifdef Z3DEBUG + , x0 #endif - lia_move r = create_cut(lia.m_t, lia.m_k, lia.m_ex, lia.m_upper, x0); + ); if (r == lia_move::cut) { TRACE("hnf_cut", diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index c9ab221eb1b..803dd6f9dbd 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -56,7 +56,7 @@ namespace lp { } bool int_branch::left_branch_is_more_narrow_than_right(unsigned j) { - switch (lra.m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) { + switch (lra.get_column_type(j)) { case column_type::fixed: return false; case column_type::boxed: { diff --git a/src/math/lp/int_branch.h b/src/math/lp/int_branch.h index 0eab13f026d..c52b99f671e 100644 --- a/src/math/lp/int_branch.h +++ b/src/math/lp/int_branch.h @@ -17,6 +17,8 @@ Revision History: --*/ #pragma once +#include "math/lp/lar_solver.h" +#include "math/lp/int_solver.h" #include "math/lp/lia_move.h" namespace lp { diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index 347da215504..f3bc575af6a 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -27,7 +27,7 @@ namespace lp { lia_move int_cube::operator()() { lia.settings().stats().m_cube_calls++; TRACE("cube", - for (unsigned j = 0; j < lra.A_r().column_count(); j++) + for (unsigned j = 0; j < lra.number_of_vars(); j++) lia.display_column(tout, j); tout << lra.constraints(); ); diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index f5f7d101557..53d13dbfe6b 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -56,7 +56,7 @@ namespace lp { } bool int_gcd_test::gcd_test() { - auto & A = lra.A_r(); // getting the matrix + const auto & A = lra.A_r(); // getting the matrix for (unsigned i = 0; i < A.row_count(); i++) if (!gcd_test_for_row(A, i)) return false; @@ -71,10 +71,9 @@ namespace lp { return r; } - bool int_gcd_test::gcd_test_for_row(static_matrix> & A, unsigned i) { + bool int_gcd_test::gcd_test_for_row(const static_matrix> & A, unsigned i) { auto const& row = A.m_rows[i]; - auto & lcs = lra.m_mpq_lar_core_solver; - unsigned basic_var = lcs.m_r_basis[i]; + unsigned basic_var = lra.r_basis()[i]; if (!lia.column_is_int(basic_var) || lia.get_value(basic_var).is_int()) return true; @@ -154,7 +153,7 @@ namespace lp { unsigned j; for (const auto & c : row) { j = c.var(); - TRACE("ext_gcd_test", tout << "col = "; lra.m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout);); + TRACE("ext_gcd_test", tout << "col = "; lra.print_column_info(j, tout);); const mpq & a = c.coeff(); if (lra.column_is_fixed(j)) continue; diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h index c8fc2c27422..0734dc8aff0 100644 --- a/src/math/lp/int_gcd_test.h +++ b/src/math/lp/int_gcd_test.h @@ -38,7 +38,7 @@ namespace lp { unsigned m_delay; bool gcd_test(); - bool gcd_test_for_row(static_matrix> & A, unsigned i); + bool gcd_test_for_row(const static_matrix> & A, unsigned i); bool ext_gcd_test(const row_strip & row, mpq const & least_coeff, mpq const & lcm_den, diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index b0432e123ce..98f87f4c415 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -126,17 +126,13 @@ int_solver::int_solver(lar_solver& lar_slv) : // this will allow to enable and disable tracking of the pivot rows struct check_return_helper { lar_solver& lra; - lar_core_solver& lrac; bool m_track_pivoted_rows; check_return_helper(lar_solver& ls) : lra(ls), - lrac(ls.m_mpq_lar_core_solver), m_track_pivoted_rows(lra.get_track_pivoted_rows()) { - TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;); lra.set_track_pivoted_rows(false); } ~check_return_helper() { - TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;); lra.set_track_pivoted_rows(m_track_pivoted_rows); } }; diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index cf201351d57..1c9254caf3c 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -7,8 +7,6 @@ namespace lp { ////////////////// 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;} static_matrix & lar_solver::A_d() { return m_mpq_lar_core_solver.m_d_A;} static_matrix const & lar_solver::A_d() const { return m_mpq_lar_core_solver.m_d_A;} @@ -965,10 +963,6 @@ bool lar_solver::try_to_set_fixed(column_info & ci) { return false; } -column_type lar_solver::get_column_type(unsigned j) const{ - return m_mpq_lar_core_solver.m_column_types[j]; -} - bool lar_solver::all_constrained_variables_are_registered(const vector>& left_side) { for (auto it : left_side) { if (! var_is_registered(it.second)) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 66dc8fa7a58..beb241134f3 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -46,7 +46,8 @@ Revision History: namespace lp { - +class int_branch; +class int_solver; class lar_solver : public column_namer { struct term_hasher { std::size_t operator()(const lar_term &t) const @@ -72,9 +73,6 @@ class lar_solver : public column_namer { return a == b; } }; - - - //////////////////// fields ////////////////////////// lp_settings m_settings; @@ -82,12 +80,9 @@ class lar_solver : public column_namer { stacked_value m_simplex_strategy; // such can be found at the initialization step: u < l stacked_value m_crossed_bounds_column; -public: lar_core_solver m_mpq_lar_core_solver; -private: int_solver * m_int_solver; bool m_need_register_terms; -public: var_register m_var_register; var_register m_term_register; stacked_vector m_columns_to_ul_pairs; @@ -108,100 +103,43 @@ class lar_solver : public column_namer { vector m_backup_x; // end of fields - const vector & terms() const { return m_terms; } - lar_term const& term(unsigned i) const { return *m_terms[i]; } - constraint_set const& constraints() const { return m_constraints; } - void set_int_solver(int_solver * int_slv) { m_int_solver = int_slv; } - int_solver * get_int_solver() { return m_int_solver; } ////////////////// methods //////////////////////////////// - static_matrix> & A_r(); - static_matrix> const & A_r() const; static_matrix & A_d(); static_matrix const & A_d() const; static bool valid_index(unsigned j) { return static_cast(j) >= 0;} - bool column_is_int(unsigned j) const; - bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } - const impq& get_column_value(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j]; } - void set_column_value(unsigned j, const impq& v) { - m_mpq_lar_core_solver.m_r_x[j] = v; + inline void set_column_value(unsigned j, const impq& v) { + m_mpq_lar_core_solver.m_r_solver.update_x(j, v); } unsigned external_to_column_index(unsigned) const; - - // NSB code review: function seems misnamed. 'j' can be a term index. Columns are not term indices. - const mpq& get_column_value_rational(unsigned j) const { - if (tv::is_term(j)) { - j = m_var_register.external_to_local(j); - } - return m_mpq_lar_core_solver.m_r_x[j].x; - } - - bool column_is_fixed(unsigned j) const; - bool column_is_free(unsigned j) const; - const lar_term & get_term(unsigned j) const; bool row_has_a_big_num(unsigned i) const; -public: - // init region bool strategy_is_undecided() const; - - var_index add_var(unsigned ext_j, bool is_integer); - var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&); - void register_new_ext_var_index(unsigned ext_v, bool is_int); - - bool external_is_used(unsigned) const; - bool term_is_int(const lar_term * t) const; - bool term_is_int(const vector> & coeffs) const; - - bool var_is_int(var_index v) const; - void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); - void add_new_var_to_core_fields_for_doubles(bool register_in_basis); - void add_new_var_to_core_fields_for_mpq(bool register_in_basis); - mpq adjust_bound_for_int(lpvar j, lconstraint_kind&, const mpq&); // terms bool all_vars_are_registered(const vector> & coeffs); - - var_index add_term(const vector> & coeffs, unsigned ext_i); - var_index add_term_undecided(const vector> & coeffs); - bool term_coeffs_are_ok(const vector> & coeffs); void push_term(lar_term* t); void add_row_for_term(const lar_term * term, unsigned term_ext_index); - void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index); - void add_basic_var_to_core_fields(); - - constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); - - void activate(constraint_index ci); - - constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ; - - bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side); - bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs); - // columns - bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); } - column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } - bool is_fixed(column_index const& j) const { return column_is_fixed(j); } const impq& get_value(column_index const& j) const { return get_column_value(j); } @@ -214,15 +152,12 @@ class lar_solver : public column_namer { void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); 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) { + inline void set_infeasible_column(unsigned j) { set_status(lp_status::INFEASIBLE); m_crossed_bounds_column = j; } - 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; void decide_on_strategy_and_adjust_initial_state(); @@ -235,22 +170,9 @@ class lar_solver : public column_namer { // this fills the last row of A_d and sets the basis column: -1 in the last column of the row void fill_last_row_of_A_d(static_matrix & A, const lar_term* ls); - //end of init region - - lp_settings & settings(); - - lp_settings const & settings() const; - void clear(); - lar_solver(); - - void set_track_pivoted_rows(bool v); - - bool get_track_pivoted_rows() const; - - virtual ~lar_solver(); bool use_lu() const; @@ -270,81 +192,21 @@ class lar_solver : public column_namer { void substitute_basis_var_in_terms_for_row(unsigned i); void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp); - - unsigned adjust_column_index_to_term_index(unsigned j) const; - - unsigned map_term_index_to_column_index(unsigned j) const; - - var_index local_to_external(var_index idx) const { return tv::is_term(idx)? - m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx); } - - unsigned number_of_vars() const { return m_var_register.size(); } - - var_index external_to_local(unsigned j) const { - var_index local_j; - if (m_var_register.external_is_used(j, local_j) || - m_term_register.external_is_used(j, local_j)) { - return local_j; - } - else { - return -1; - } - } - - bool column_has_upper_bound(unsigned j) const { - return m_mpq_lar_core_solver.m_r_solver.column_has_upper_bound(j); - } - - bool column_has_lower_bound(unsigned j) const { - return m_mpq_lar_core_solver.m_r_solver.column_has_lower_bound(j); - } - - const impq& get_upper_bound(column_index j) const { - return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j]; - } - - const impq& get_lower_bound(column_index j) const { - return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j]; - } - void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset); - void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp); - - - bool term_is_used_as_row(unsigned term) const; - - void propagate_bounds_on_terms(lp_bound_propagator & bp); - - - // goes over touched rows and tries to induce bounds - void propagate_bounds_for_touched_rows(lp_bound_propagator & bp); - - lp_status get_status() const; - - void set_status(lp_status s); - - lp_status find_feasible_solution(); - - lp_status solve(); - - void fill_explanation_from_crossed_bounds_column(explanation & evidence) const; - unsigned get_total_iterations() const; // see http://research.microsoft.com/projects/z3/smt07.pdf // This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find // Attention, after a call to this method the non-basic variables don't necesserarly stick to their bounds anymore vector get_list_of_all_var_indices() const; - void push(); static void clean_popped_elements(unsigned n, u_set& set); static void shrink_inf_set_after_pop(unsigned n, u_set & set); - void pop(unsigned k); bool maximize_term_on_tableau(const lar_term & term, impq &term_max); @@ -358,13 +220,8 @@ class lar_solver : public column_namer { bool maximize_term_on_corrected_r_solver(lar_term & term, impq &term_max); // starting from a given feasible state look for the maximum of the term - // return true if found and false if unbounded - lp_status maximize_term(unsigned j_or_term, impq &term_max); - - - - const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; } - + // return true if found and false if unbounded + void pop_core_solver_params(); void pop_core_solver_params(unsigned k); @@ -391,10 +248,6 @@ class lar_solver : public column_namer { void adjust_x_of_column(unsigned j); - bool row_is_correct(unsigned i) const; - - bool ax_is_correct() const; - bool tableau_with_costs() const; bool costs_are_used() const; @@ -409,13 +262,7 @@ class lar_solver : public column_namer { void detect_rows_with_changed_bounds_for_column(unsigned j); void detect_rows_with_changed_bounds(); - inline bool is_base(unsigned j) const { - return m_mpq_lar_core_solver.m_r_heading[j] >= 0; - } - bool move_non_basic_columns_to_bounds(); - - bool move_non_basic_column_to_bounds(unsigned j); void set_value_for_nbasic_column(unsigned j, const impq & new_val); void update_x_and_inf_costs_for_columns_with_changed_bounds(); @@ -430,7 +277,6 @@ class lar_solver : public column_namer { bool x_is_correct() const; - bool var_is_registered(var_index vj) const; void fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls); @@ -443,8 +289,6 @@ class lar_solver : public column_namer { bool try_to_set_fixed(column_info & ci); - column_type get_column_type(unsigned j) const; - bool all_constrained_variables_are_registered(const vector>& left_side); bool all_constraints_hold() const; @@ -465,50 +309,19 @@ class lar_solver : public column_namer { mpq sum_of_right_sides_of_explanation(explanation &) const; - bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const; - - bool has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const; - - bool has_value(var_index var, mpq& value) const; - - void get_infeasibility_explanation(explanation &) const; void get_infeasibility_explanation_for_inf_sign( explanation & exp, const vector> & inf_row, int inf_sign) const; - void get_model(std::unordered_map & variable_values) const; - - void get_rid_of_inf_eps(); - - void get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const; - - std::string get_variable_name(var_index vi) const; - - void set_variable_name(var_index vi, std::string); - - // ********** print region start - - std::ostream& print_terms(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_indices_only(const lar_base_constraint * c, std::ostream & out) const; - - std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const; - std::ostream& print_values(std::ostream& out) const; mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const; void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list); - void random_update(unsigned sz, var_index const * vars); void pivot_fixed_vars_from_basis(); - void pop(); bool column_represents_row_in_tableau(unsigned j); void make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j); void remove_last_row_and_column_from_tableau(unsigned j); @@ -526,48 +339,74 @@ class lar_solver : public column_namer { return get_column_value(j).is_int(); } - bool column_is_real(unsigned j) const { - return !column_is_int(j); - } bool model_is_int_feasible() const; - const impq & column_lower_bound(unsigned j) const { - return m_mpq_lar_core_solver.lower_bound(j); - } - - const impq & column_upper_bound(unsigned j) const { - return m_mpq_lar_core_solver.upper_bound(j); - } - - bool column_is_bounded(unsigned j) const { - return m_mpq_lar_core_solver.column_is_bounded(j); - } - - std::pair add_equality(lpvar j, lpvar k); - - void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { - const ul_pair & ul = m_columns_to_ul_pairs[j]; - lc = ul.lower_bound_witness(); - uc = ul.upper_bound_witness(); - } indexed_vector & get_column_in_lu_mode(unsigned j) { m_column_buffer.clear(); m_column_buffer.resize(A_r().row_count()); m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); return m_column_buffer; } - bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const; - - const row_strip & get_row(unsigned i) { - return A_r().m_rows[i]; - } - unsigned get_base_column_in_row(unsigned row_index) const { return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index); } + lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; } + void catch_up_in_updating_int_solver(); + var_index to_column(unsigned ext_j) const; + void fix_terms_with_rounded_columns(); + void update_delta_for_terms(const impq & delta, unsigned j, const vector&); + void fill_vars_to_terms(vector> & vars_to_terms); + bool remove_from_basis(unsigned); + lar_term get_term_to_maximize(unsigned ext_j) const; + bool sum_first_coords(const lar_term& t, mpq & val) const; + void collect_rounded_rows_to_fix(); + void register_normalized_term(const lar_term&, lpvar); + void deregister_normalized_term(const lar_term&); + bool inside_bounds(lpvar, const impq&) const; +public: + lp_status maximize_term(unsigned j_or_term, impq &term_max); + inline + core_solver_pretty_printer pp(std::ostream& out) { return + core_solver_pretty_printer(m_mpq_lar_core_solver.m_r_solver, out); } + void get_infeasibility_explanation(explanation &) const; + inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } + inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } + void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp); + constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side); + void activate(constraint_index ci); + void random_update(unsigned sz, var_index const * vars); + void propagate_bounds_on_terms(lp_bound_propagator & bp); + void propagate_bounds_for_touched_rows(lp_bound_propagator & bp); + bool is_fixed(column_index const& j) const { return column_is_fixed(j); } + inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } + bool external_is_used(unsigned) const; + void pop(unsigned k); + 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) ; + 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(); } + inline var_index local_to_external(var_index idx) const { + return tv::is_term(idx)? + m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx); + } + bool column_corresponds_to_term(unsigned) const; + inline unsigned row_count() const { return A_r().row_count(); } + bool var_is_registered(var_index vj) const; + bool try_to_patch(lpvar, const mpq&, const std::function& blocker,const std::function& change_report); + inline bool column_has_upper_bound(unsigned j) const { + return m_mpq_lar_core_solver.m_r_solver.column_has_upper_bound(j); + } + + inline bool column_has_lower_bound(unsigned j) const { + return m_mpq_lar_core_solver.m_r_solver.column_has_lower_bound(j); + } + inline constraint_index get_column_upper_bound_witness(unsigned j) const { if (tv::is_term(j)) { j = m_var_register.external_to_local(j); @@ -575,18 +414,75 @@ class lar_solver : public column_namer { return m_columns_to_ul_pairs()[j].upper_bound_witness(); } - constraint_index get_column_lower_bound_witness(unsigned j) const { + inline + const impq& get_upper_bound(column_index j) const { + return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j]; + } + + inline + const impq& get_lower_bound(column_index j) const { + return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j]; + } +bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const; + bool has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const; + bool has_value(var_index var, mpq& value) const; +bool fetch_normalized_term_column(const lar_term& t, std::pair& ) const; + unsigned map_term_index_to_column_index(unsigned j) const; + bool column_is_fixed(unsigned j) const; + bool column_is_free(unsigned j) const; + unsigned adjust_column_index_to_term_index(unsigned j) const; + lp_settings & settings(); + lp_settings const & settings() const; + column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; } + const impq & get_lower_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_lower_bounds()[j]; } + const impq & get_upper_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_upper_bounds()[j]; } + std::ostream& print_terms(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_indices_only(const lar_base_constraint * c, std::ostream & out) const; + std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const; + std::ostream& print_values(std::ostream& out) const; + void get_model(std::unordered_map & variable_values) const; + void get_rid_of_inf_eps(); + void get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const; + std::string get_variable_name(var_index vi) const; + void set_variable_name(var_index vi, std::string); + unsigned number_of_vars() const { return m_var_register.size(); } + inline bool is_base(unsigned j) const { return m_mpq_lar_core_solver.m_r_heading[j] >= 0; } + inline const impq & column_lower_bound(unsigned j) const { + return m_mpq_lar_core_solver.lower_bound(j); + } + + inline const impq & column_upper_bound(unsigned j) const { + return m_mpq_lar_core_solver.upper_bound(j); + } + + inline bool column_is_bounded(unsigned j) const { + return m_mpq_lar_core_solver.column_is_bounded(j); + } + + std::pair add_equality(lpvar j, lpvar k); + + inline void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { + const ul_pair & ul = m_columns_to_ul_pairs[j]; + lc = ul.lower_bound_witness(); + uc = ul.upper_bound_witness(); + } + inline constraint_set const& constraints() const { return m_constraints; } + void push(); + void pop(); + inline constraint_index get_column_lower_bound_witness(unsigned j) const { if (tv::is_term(j)) { j = m_var_register.external_to_local(j); } return m_columns_to_ul_pairs()[j].lower_bound_witness(); } - tv column2tv(column_index const& c) const { + inline tv column2tv(column_index const& c) const { return tv::raw(adjust_column_index_to_term_index(c)); } - std::ostream& print_column_info(unsigned j, std::ostream& out) const { + inline std::ostream& print_column_info(unsigned j, std::ostream& out) const { m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); if (tv::is_term(j)) { print_term_as_indices(get_term(j), out) << "\n"; @@ -597,51 +493,75 @@ class lar_solver : public column_namer { } return out; } - + + inline std::ostream& print_column_bound_info(unsigned j, std::ostream& out) const { + return m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, out); + } + bool has_int_var() const; - bool has_inf_int() const { + inline bool has_inf_int() const { for (unsigned j = 0; j < column_count(); j++) { if (column_is_int(j) && ! column_value_is_int(j)) return true; } return false; } - - bool r_basis_has_inf_int() const { + inline const vector & terms() const { return m_terms; } + inline lar_term const& term(unsigned i) const { return *m_terms[i]; } + inline void set_int_solver(int_solver * int_slv) { m_int_solver = int_slv; } + inline int_solver * get_int_solver() { return m_int_solver; } + const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; } + lp_status find_feasible_solution(); + bool move_non_basic_columns_to_bounds(); + bool move_non_basic_column_to_bounds(unsigned j); + inline bool r_basis_has_inf_int() const { for (unsigned j : r_basis()) { if (column_is_int(j) && ! column_value_is_int(j)) return true; } return false; } - - lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; } - bool column_corresponds_to_term(unsigned) const; - void catch_up_in_updating_int_solver(); - var_index to_column(unsigned ext_j) const; - bool tighten_term_bounds_by_delta(tv const& t, const impq&); void round_to_integer_solution(); - void fix_terms_with_rounded_columns(); - void update_delta_for_terms(const impq & delta, unsigned j, const vector&); - void fill_vars_to_terms(vector> & vars_to_terms); - unsigned column_count() const { return A_r().column_count(); } - unsigned row_count() const { return A_r().row_count(); } + inline const row_strip & get_row(unsigned i) { return A_r().m_rows[i]; } + bool row_is_correct(unsigned i) const; + bool ax_is_correct() const; + bool get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq &rs, constraint_index& ci, bool &upper_bound) const; + bool var_is_int(var_index v) const; + const vector & r_heading() const { return m_mpq_lar_core_solver.m_r_heading; } const vector & r_basis() const { return m_mpq_lar_core_solver.r_basis(); } const vector & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); } - bool get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq &rs, constraint_index& ci, bool &upper_bound) const; - bool remove_from_basis(unsigned); - lar_term get_term_to_maximize(unsigned ext_j) const; - void set_cut_strategy(unsigned cut_frequency); - bool sum_first_coords(const lar_term& t, mpq & val) const; - void collect_rounded_rows_to_fix(); - void register_existing_terms(); - void register_normalized_term(const lar_term&, lpvar); - void deregister_normalized_term(const lar_term&); - bool fetch_normalized_term_column(const lar_term& t, std::pair& ) const; - bool try_to_patch(lpvar, const mpq&, const std::function& blocker,const std::function& change_report); - bool inside_bounds(lpvar, const impq&) const; - void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } - void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } + inline bool column_is_real(unsigned j) const { return !column_is_int(j); } + lp_status get_status() const; + void set_status(lp_status s); + lp_status solve(); + 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(); + void set_track_pivoted_rows(bool v); + bool get_track_pivoted_rows() const; + virtual ~lar_solver(); + const vector& r_x() const { return m_mpq_lar_core_solver.m_r_x; } + bool column_is_int(unsigned j) const; + bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } + inline static_matrix & A_r() { return m_mpq_lar_core_solver.m_r_A; } + inline const static_matrix & A_r() const { return m_mpq_lar_core_solver.m_r_A; } + const impq& get_column_value(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j]; } + inline + var_index external_to_local(unsigned j) const { + var_index local_j; + if (m_var_register.external_is_used(j, local_j) || + m_term_register.external_is_used(j, local_j)) { + return local_j; + } + else { + return -1; + } + } + + friend int_solver; + friend int_branch; + }; } diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp index 2242d63e5be..c07a60adbb6 100644 --- a/src/math/lp/lp_bound_propagator.cpp +++ b/src/math/lp/lp_bound_propagator.cpp @@ -7,13 +7,13 @@ namespace lp { lp_bound_propagator::lp_bound_propagator(lar_solver & ls): m_lar_solver(ls) {} column_type lp_bound_propagator::get_column_type(unsigned j) const { - return m_lar_solver.m_mpq_lar_core_solver.m_column_types()[j]; + return m_lar_solver.get_column_type(j); } const impq & lp_bound_propagator::get_lower_bound(unsigned j) const { - return m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]; + return m_lar_solver.get_lower_bound(j); } const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { - return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; + return m_lar_solver.get_upper_bound(j); } void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { j = m_lar_solver.adjust_column_index_to_term_index(j); diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index dc5bc0dd52e..06883bcd58c 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -557,7 +557,7 @@ class lp_core_solver_base { return true; } - void print_column_bound_info(unsigned j, std::ostream & out) const { + std::ostream& print_column_bound_info(unsigned j, std::ostream & out) const { out << column_name(j) << " type = " << column_type_to_string(m_column_types[j]) << std::endl; switch (m_column_types[j]) { case column_type::fixed: @@ -573,6 +573,7 @@ class lp_core_solver_base { default: break; } + return out; } std::ostream& print_column_info(unsigned j, std::ostream & out) const { diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 1b655a26402..1a4a7a0431c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -147,7 +147,7 @@ void core::pop(unsigned n) { rational core::product_value(const monic& m) const { rational r(1); for (auto j : m.vars()) { - r *= m_lar_solver.get_column_value_rational(j); + r *= m_lar_solver.get_column_value(j).x; } return r; } @@ -155,7 +155,7 @@ rational core::product_value(const monic& m) const { // return true iff the monic value is equal to the product of the values of the factors bool core::check_monic(const monic& m) const { SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); - bool ret = product_value(m) == m_lar_solver.get_column_value_rational(m.var()); + bool ret = product_value(m) == m_lar_solver.get_column_value(m.var()).x; CTRACE("nla_solver_check_monic", !ret, print_monic(m, tout) << '\n';); return ret; } @@ -1523,14 +1523,14 @@ lbool core::test_check( } std::ostream& core::print_terms(std::ostream& out) const { - for (unsigned i = 0; i< m_lar_solver.m_terms.size(); i++) { + for (unsigned i = 0; i< m_lar_solver.terms().size(); i++) { unsigned ext = lp::tv::mask_term(i); if (!m_lar_solver.var_is_registered(ext)) { out << "term is not registered\n"; continue; } - const lp::lar_term & t = *m_lar_solver.m_terms[i]; + const lp::lar_term & t = *m_lar_solver.terms()[i]; out << "term:"; print_term(t, out) << std::endl; lpvar j = m_lar_solver.external_to_local(ext); print_var(j, out); @@ -1631,7 +1631,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) { } } - for (unsigned j = 0; j < m_lar_solver.column_count(); ++j) { + for (unsigned j = 0; j < m_lar_solver.number_of_vars(); ++j) { if (m_lar_solver.column_has_lower_bound(j) || m_lar_solver.column_has_upper_bound(j)) { out << j << ": ["; if (m_lar_solver.column_has_lower_bound(j)) out << m_lar_solver.get_lower_bound(j); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 2f2f15efe29..7027727e9d2 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -128,13 +128,13 @@ class core { bool ineq_holds(const ineq& n) const; bool lemma_holds(const lemma& l) const; bool is_monic_var(lpvar j) const { return m_emons.is_monic_var(j); } - rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); } + const rational& val(lpvar j) const { return m_lar_solver.get_column_value(j).x; } - rational var_val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); } + const rational& var_val(const monic& m) const { return m_lar_solver.get_column_value(m.var()).x; } rational mul_val(const monic& m) const { rational r(1); - for (lpvar v : m.vars()) r *= m_lar_solver.get_column_value_rational(v); + for (lpvar v : m.vars()) r *= m_lar_solver.get_column_value(v).x; return r; } diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h index a2c6ffc8ebc..aca4e1d6582 100644 --- a/src/math/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -43,9 +43,7 @@ bool random_updater::shift_var(unsigned j) { if (ret) { const auto & A = m_lar_solver.A_r(); for (const auto& c : A.m_columns[j]) { - unsigned row_index = c.var(); - unsigned changed_basic = m_lar_solver.get_core_solver().m_r_basis[row_index]; - m_var_set.erase(changed_basic); + m_var_set.erase(m_lar_solver.r_basis()[c.var()]); } } return ret; @@ -62,8 +60,8 @@ void random_updater::update() { if (!m_lar_solver.is_base(j)) { shift_var(j); } else { - unsigned row = m_lar_solver.get_core_solver().m_r_heading[j]; - for (auto & row_c : m_lar_solver.get_core_solver().m_r_A.m_rows[row]) { + unsigned row_index = m_lar_solver.r_heading()[j]; + for (auto & row_c : m_lar_solver.get_row(row_index)) { unsigned cj = row_c.var(); if (!m_lar_solver.is_base(cj) && !m_lar_solver.column_is_fixed(cj) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6f02cb84024..65f5d1059e7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3815,11 +3815,9 @@ class theory_lra::imp { out << lp().constraints(); lp().print_terms(out); // the tableau - auto pp = lp ::core_solver_pretty_printer( - lp().m_mpq_lar_core_solver.m_r_solver, out); - pp.print(); + lp().pp(out).print(); for (unsigned j = 0; j < lp().number_of_vars(); j++) { - lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); + lp().print_column_info(j, out); } } if (m_nla) {