From bdb9106f996c838f387c1602f29e9665feccea2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jan 2024 16:05:18 -0800 Subject: [PATCH] Api (#7097) * rename ul_pair to column Signed-off-by: Lev Nachmanson * t Signed-off-by: Lev Nachmanson * simple test passed * remove an assert * relax an assertion * remove an obsolete function Signed-off-by: Lev Nachmanson * access a term by the term column * remove the column index from colunm.h * remove an unused method * remove debug code * fix the build of lp_tst Signed-off-by: Lev Nachmanson --------- Signed-off-by: Lev Nachmanson Co-authored-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 1 - src/math/lp/{ul_pair.h => column.h} | 25 +- src/math/lp/emonics.cpp | 2 +- src/math/lp/general_matrix.h | 2 +- src/math/lp/gomory.cpp | 12 +- src/math/lp/hnf_cutter.cpp | 14 +- src/math/lp/hnf_cutter.h | 2 +- src/math/lp/int_branch.cpp | 2 +- src/math/lp/int_cube.cpp | 20 +- src/math/lp/int_solver.cpp | 6 +- src/math/lp/int_solver.h | 2 +- src/math/lp/lar_constraints.h | 12 +- src/math/lp/lar_solver.cpp | 536 +++++++++------------------- src/math/lp/lar_solver.h | 175 ++++----- src/math/lp/lar_term.h | 23 +- src/math/lp/lp_api.h | 6 +- src/math/lp/lp_bound_propagator.h | 21 +- src/math/lp/lp_settings.h | 5 +- src/math/lp/lp_types.h | 60 ---- src/math/lp/lp_utils.h | 9 +- src/math/lp/monic.h | 12 +- src/math/lp/monomial_bounds.cpp | 11 +- src/math/lp/nla_core.cpp | 72 ++-- src/math/lp/nla_core.h | 5 +- src/math/lp/nla_defs.h | 8 +- src/math/lp/nla_divisions.cpp | 17 +- src/math/lp/nla_grobner.cpp | 5 +- src/math/lp/nla_powers.cpp | 4 +- src/math/lp/nla_solver.cpp | 2 +- src/math/lp/nla_solver.h | 2 +- src/math/lp/nla_types.h | 2 +- src/math/lp/nra_solver.cpp | 38 +- src/math/lp/nra_solver.h | 2 +- src/math/lp/static_matrix.h | 4 +- src/math/lp/var_register.h | 11 +- src/sat/smt/arith_diagnostics.cpp | 7 +- src/sat/smt/arith_internalize.cpp | 9 +- src/sat/smt/arith_sls.cpp | 36 +- src/sat/smt/arith_sls.h | 4 +- src/sat/smt/arith_solver.cpp | 85 ++--- src/sat/smt/arith_solver.h | 14 +- src/smt/theory_lra.cpp | 159 ++++----- src/test/lp/gomory_test.h | 2 +- src/test/lp/lp.cpp | 110 +++--- src/test/lp/smt_reader.h | 4 +- 45 files changed, 587 insertions(+), 973 deletions(-) rename src/math/lp/{ul_pair.h => column.h} (75%) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index b4d587bec2d..20e45a2188a 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -291,7 +291,6 @@ public : int bound_sign = (is_lower_bound ? 1 : -1); int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; - SASSERT(!tv::is_term(bound_j)); u_dependency* ret = nullptr; for (auto const& r : lar->get_row(row_index)) { unsigned j = r.var(); diff --git a/src/math/lp/ul_pair.h b/src/math/lp/column.h similarity index 75% rename from src/math/lp/ul_pair.h rename to src/math/lp/column.h index 35407028125..4f3e689669f 100644 --- a/src/math/lp/ul_pair.h +++ b/src/math/lp/column.h @@ -37,17 +37,19 @@ inline std::ostream& operator<<(std::ostream& out, lconstraint_kind k) { return out << "??"; } -inline bool compare(const std::pair & a, const std::pair & b) { +inline bool compare(const std::pair & a, const std::pair & b) { return a.second < b.second; } - -class ul_pair { +class lar_term; // forward definition +class column { u_dependency* m_lower_bound_witness = nullptr; u_dependency* m_upper_bound_witness = nullptr; bool m_associated_with_row = false; + lpvar m_j; //the column index + lar_term* m_term = nullptr; public: - // TODO - seems more straight-forward to just expose ul_pair as a struct with direct access to attributes. - + lar_term* term() const { return m_term; } + u_dependency*& lower_bound_witness() { return m_lower_bound_witness; } u_dependency* lower_bound_witness() const { return m_lower_bound_witness; } u_dependency*& upper_bound_witness() { return m_upper_bound_witness; } @@ -56,20 +58,21 @@ class ul_pair { // equality is used by stackedvector operations. // this appears to be a low level reason - bool operator!=(const ul_pair & p) const { + bool operator!=(const column & p) const { return !(*this == p); } - bool operator==(const ul_pair & p) const { + bool operator==(const column & p) const { return m_lower_bound_witness == p.m_lower_bound_witness && m_upper_bound_witness == p.m_upper_bound_witness && m_associated_with_row == p.m_associated_with_row; } - // empty constructor - ul_pair() {} + column() = delete; + column(bool) = delete; - ul_pair(bool associated_with_row) : - m_associated_with_row(associated_with_row) {} + + column(bool associated_with_row, lar_term* term) : + m_associated_with_row(associated_with_row), m_term(term) {} bool associated_with_row() const { return m_associated_with_row; } }; diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 5d0e664f29a..e6e52e57b26 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -536,7 +536,7 @@ bool emonics::invariant() const { do { auto const& m = m_monics[c->m_index]; bool found = false; - for (lp::var_index w : m.rvars()) { + for (lp::lpvar w : m.rvars()) { auto w1 = m_ve.find(w); found |= v1.var() == w1.var(); } diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index a4f6693a211..fb1030e6b10 100644 --- a/src/math/lp/general_matrix.h +++ b/src/math/lp/general_matrix.h @@ -109,7 +109,7 @@ class general_matrix { auto & row = m_data[adjust_row(i)]; lp_assert(row_is_initialized_correctly(row)); for (lp::lar_term::ival p : c) { - unsigned j = adjust_column(column_fix(p.column().index())); + unsigned j = adjust_column(column_fix(p.j())); row[j] = sign * p.coeff(); } } diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index a7c72a76d15..7b4347af513 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -156,7 +156,7 @@ struct create_cut { template void dump_coeff(std::ostream & out, const T& c) const { - dump_coeff_val(out << "(* ", c.coeff()) << " " << var_name(c.column().index()) << ")"; + dump_coeff_val(out << "(* ", c.coeff()) << " " << var_name(c.j()) << ")"; } std::ostream& dump_row_coefficients(std::ostream & out) const { @@ -183,9 +183,8 @@ struct create_cut { for (const auto & p : m_row) dump_declaration(out, p.var()); for (lar_term::ival p : m_t) { - auto t = lia.lra.column2tv(p.column()); - if (t.is_term()) - dump_declaration(out, t.id()); + if (lia.lra.column_has_term(p.j())) + dump_declaration(out, p.j()); } } @@ -491,9 +490,8 @@ struct create_cut { return all_of(t, [&](auto ci) { return ci.coeff().is_small(); }); }; auto add_cut = [&](const lar_term& t, const mpq& k, u_dependency * dep) { - lp::lpvar term_index = lra.add_term(t.coeffs_as_vector(), UINT_MAX); - term_index = lra.map_term_index_to_column_index(term_index); - lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::GE, k, dep); + lp::lpvar j = lra.add_term(t.coeffs_as_vector(), UINT_MAX); + lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE, k, dep); }; auto _check_feasible = [&](void) { lra.find_feasible_solution(); diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 75095ca515e..b120b7aac0e 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -20,7 +20,7 @@ namespace lp { lra(lia.lra), m_settings(lia.settings()), m_abs_max(zero_of_type()), - m_var_register(false) {} + m_var_register() {} bool hnf_cutter::is_full() const { return @@ -50,7 +50,7 @@ namespace lp { m_constraints_for_explanation.push_back(ci); for (lar_term::ival p : *t) { - m_var_register.add_var(p.column().index(), true); // hnf only deals with integral variables for now + m_var_register.add_var(p.j(), true); // hnf only deals with integral variables for now mpq t = abs(ceil(p.coeff())); if (t > m_abs_max) m_abs_max = t; @@ -227,12 +227,12 @@ branch y_i >= ceil(y0_i) is impossible. svector hnf_cutter::vars() const { return m_var_register.vars(); } - void hnf_cutter::try_add_term_to_A_for_hnf(tv const &i) { + void hnf_cutter::try_add_term_to_A_for_hnf(lpvar j) { mpq rs; - const lar_term& t = lra.get_term(i); + const lar_term& t = lra.get_term(j); u_dependency* dep; bool upper_bound; - if (!is_full() && lra.get_equality_and_right_side_for_term_on_current_x(i, rs, dep, upper_bound)) { + if (!is_full() && lra.get_equality_and_right_side_for_term_on_current_x(j, rs, dep, upper_bound)) { add_term(&t, rs, dep, upper_bound); } } @@ -243,8 +243,8 @@ branch y_i >= ceil(y0_i) is impossible. bool hnf_cutter::init_terms_for_hnf_cut() { clear(); - for (unsigned i = 0; i < lra.terms().size() && !is_full(); i++) - try_add_term_to_A_for_hnf(tv::term(i)); + for (const lar_term* t: lra.terms()) + try_add_term_to_A_for_hnf(t->j()); return hnf_has_var_with_non_integral_value(); } diff --git a/src/math/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h index 74fb52327a9..07ddc7b12f0 100644 --- a/src/math/lp/hnf_cutter.h +++ b/src/math/lp/hnf_cutter.h @@ -50,7 +50,7 @@ class hnf_cutter { private: bool init_terms_for_hnf_cut(); bool hnf_has_var_with_non_integral_value() const; - void try_add_term_to_A_for_hnf(tv const& i); + void try_add_term_to_A_for_hnf(lpvar); unsigned terms_count() const { return m_terms.size(); } const mpq & abs_max() const { return m_abs_max; } diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 4ab97d3ed10..10211c4faf3 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -34,7 +34,7 @@ lia_move int_branch::create_branch_on_column(int j) { lia.m_t.clear(); lp_assert(j != -1); - lia.m_t.add_monomial(mpq(1), lra.column_to_reported_index(j)); + lia.m_t.add_monomial(mpq(1), j); if (lia.is_free(j)) { lia.m_upper = lia.random() % 2; lia.m_k = mpq(0); diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index 9ef9aa34161..c8488ca3737 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -55,21 +55,21 @@ namespace lp { lia.settings().stats().m_cube_success++; return lia_move::sat; } - +// i is the column index having the term bool int_cube::tighten_term_for_cube(unsigned i) { - if (!lra.term_is_used_as_row(i)) + if (!lra.column_associated_with_row(i)) return true; - const lar_term* t = lra.terms()[i]; - impq delta = get_cube_delta_for_term(*t); - TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta << "\n";); + const lar_term& t = lra.get_term(i); + impq delta = get_cube_delta_for_term(t); + TRACE("cube", lra.print_term_as_indices(t, tout); tout << ", delta = " << delta << "\n";); if (is_zero(delta)) return true; - return lra.tighten_term_bounds_by_delta(tv::term(i), delta); + return lra.tighten_term_bounds_by_delta(i, delta); } bool int_cube::tighten_terms_for_cube() { - for (unsigned i = 0; i < lra.terms().size(); i++) - if (!tighten_term_for_cube(i)) { + for (const lar_term* t: lra.terms()) + if (!tighten_term_for_cube(t->j())) { TRACE("cube", tout << "cannot tighten";); return false; } @@ -86,7 +86,7 @@ namespace lp { bool seen_minus = false; bool seen_plus = false; for(lar_term::ival p : t) { - if (!lia.column_is_int(p.column())) + if (!lia.column_is_int(p.j())) goto usual_delta; const mpq & c = p.coeff(); if (c == one_of_type()) { @@ -104,7 +104,7 @@ namespace lp { usual_delta: mpq delta = zero_of_type(); for (lar_term::ival p : t) - if (lia.column_is_int(p.column())) + if (lia.column_is_int(p.j())) delta += abs(p.coeff()); delta *= mpq(1, 2); diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 5c480cbb331..f547ba274fb 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -228,7 +228,7 @@ namespace lp { bool int_solver::cut_indices_are_columns() const { for (lar_term::ival p : m_t) { - if (p.column().index() >= lra.A_r().column_count()) + if (p.j() >= lra.A_r().column_count()) return false; } return true; @@ -271,7 +271,7 @@ namespace lp { return lra.settings(); } - bool int_solver::column_is_int(column_index const& j) const { + bool int_solver::column_is_int(lpvar j) const { return lra.column_is_int(j); } @@ -296,7 +296,7 @@ namespace lp { } bool int_solver::is_term(unsigned j) const { - return lra.column_corresponds_to_term(j); + return lra.column_has_term(j); } unsigned int_solver::column_count() const { diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 5f8e3eeb52b..524f8fb2832 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -83,7 +83,7 @@ class int_solver { bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; const impq & upper_bound(unsigned j) const; - bool column_is_int(column_index const& j) const; + bool column_is_int(lpvar j) const; const impq & get_value(unsigned j) const; bool at_lower(unsigned j) const; bool at_upper(unsigned j) const; diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index f0c9373249d..b9069625f5c 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -16,7 +16,7 @@ Copyright (c) 2017 Microsoft Corporation #include "util/region.h" #include "util/stacked_value.h" #include "math/lp/lp_utils.h" -#include "math/lp/ul_pair.h" +#include "math/lp/column.h" #include "math/lp/lar_term.h" #include "math/lp/column_namer.h" namespace lp { @@ -46,7 +46,7 @@ class lar_base_constraint { public: - virtual vector> coeffs() const = 0; + virtual vector> coeffs() const = 0; lar_base_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) : m_kind(kind), m_right_side(right_side), m_active(false), m_j(j), m_dep(dep) {} virtual ~lar_base_constraint() = default; @@ -69,8 +69,8 @@ class lar_var_constraint: public lar_base_constraint { lar_var_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) : lar_base_constraint(j, kind, dep, right_side) {} - vector> coeffs() const override { - vector> ret; + vector> coeffs() const override { + vector> ret; ret.push_back(std::make_pair(one_of_type(), column())); return ret; } @@ -84,7 +84,7 @@ class lar_term_constraint: public lar_base_constraint { lar_term_constraint(unsigned j, const lar_term* t, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) : lar_base_constraint(j, kind, dep, right_side), m_term(t) {} - vector> coeffs() const override { return m_term->coeffs_as_vector(); } + vector> coeffs() const override { return m_term->coeffs_as_vector(); } unsigned size() const override { return m_term->size();} }; @@ -168,7 +168,7 @@ class constraint_set { m_region.pop_scope(k); } - constraint_index add_var_constraint(var_index j, lconstraint_kind k, mpq const& rhs) { + constraint_index add_var_constraint(lpvar j, lconstraint_kind k, mpq const& rhs) { return add(new (m_region) lar_var_constraint(j, k, mk_dep(), rhs)); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index d14a7489e79..ef61c220953 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -23,8 +23,7 @@ namespace lp { lar_solver::lar_solver() : m_mpq_lar_core_solver(m_settings, *this), - m_var_register(false), - m_term_register(true), + m_var_register(), m_constraints(m_dependencies, *this) {} // start or ends tracking the rows that were changed by solve() @@ -52,9 +51,9 @@ namespace lp { std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostream& out) const { out << "implied bound\n"; unsigned v = be.m_j; - if (tv::is_term(v)) { - out << "it is a term number " << tv::unmask_term(be.m_j) << std::endl; - print_term(*m_terms[tv::unmask_term(v)], out); + if (column_has_term(v)) { + out << "term for column " << v << std::endl; + print_term(*m_columns[v].term(), out); } else { out << get_variable_name(v); @@ -95,7 +94,7 @@ namespace lp { if (strict) kind = static_cast((static_cast(kind) / 2)); - if (!tv::is_term(be.m_j)) { + if (!column_has_term(be.m_j)) { if (coeff_map.size() != 1) return false; auto it = coeff_map.find(be.m_j); @@ -109,13 +108,13 @@ namespace lp { else { lar_term const& t = get_term(be.m_j); auto first_coeff = t.begin(); - unsigned j = (*first_coeff).column(); + unsigned j = (*first_coeff).j(); auto it = coeff_map.find(j); if (it == coeff_map.end()) return false; mpq ratio = it->second / (*first_coeff).coeff(); for (auto p : t) { - it = coeff_map.find(p.column()); + it = coeff_map.find(p.j()); if (it == coeff_map.end()) return false; if (p.coeff() * ratio != it->second) @@ -139,43 +138,6 @@ namespace lp { return false; } - void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { - // todo : create a map from term basic vars to the rows where they are used - unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i]; - for (unsigned k = 0; k < m_terms.size(); k++) { - if (term_is_used_as_row(k)) - continue; - if (!m_terms[k]->contains(basis_j)) - continue; - m_terms[k]->subst_in_row(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); - } - } - - // Returns the column index without changes, - // but in the case the column was created as - // the slack variable to a term return the term index. - // It is the same index that was returned by add_var(), or - // by add_term() - unsigned lar_solver::column_to_reported_index(unsigned j) const { - if (tv::is_term(j)) - return j; - unsigned ext_var_or_term = m_var_register.local_to_external(j); - if (tv::is_term(ext_var_or_term)) - j = ext_var_or_term; - return j; - } - - unsigned lar_solver::map_term_index_to_column_index(unsigned j) const { - SASSERT(tv::is_term(j)); - return m_var_register.external_to_local(j); - } - - // here i is just the term index - bool lar_solver::term_is_used_as_row(unsigned i) const { - SASSERT(i < m_terms.size()); - return m_var_register.external_is_used(tv::mask_term(i)); - } - lp_status lar_solver::get_status() const { return m_status; } void lar_solver::set_status(lp_status s) { @@ -189,8 +151,6 @@ namespace lp { stats().m_max_cols = A_r().column_count(); if (A_r().row_count() > stats().m_max_rows) stats().m_max_rows = A_r().row_count(); - if (strategy_is_undecided()) - decide_on_strategy_and_adjust_initial_state(); flet f(settings().simplex_strategy(), simplex_strategy_enum::tableau_rows); m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true; auto ret = solve(); @@ -257,7 +217,7 @@ namespace lp { m_crossed_bounds_column = null_lpvar; m_crossed_bounds_deps = nullptr; m_trail.pop_scope(k); - unsigned n = m_columns_to_ul_pairs.size(); + unsigned n = m_columns.size(); m_var_register.shrink(n); lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); @@ -276,9 +236,7 @@ namespace lp { unsigned m = A_r().row_count(); clean_popped_elements(m, m_touched_rows); clean_inf_heap_of_r_solver_after_pop(); - lp_assert( - m_settings.simplex_strategy() == simplex_strategy_enum::undecided || - m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + SASSERT(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); m_constraints.pop(k); m_simplex_strategy.pop(k); @@ -296,9 +254,6 @@ namespace lp { bool lar_solver::maximize_term_on_tableau(const lar_term& term, impq& term_max) { flet f(m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only, false); - if (settings().simplex_strategy() == simplex_strategy_enum::undecided) - decide_on_strategy_and_adjust_initial_state(); - m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::FEASIBLE); m_mpq_lar_core_solver.solve(); lp_status st = m_mpq_lar_core_solver.m_r_solver.get_status(); @@ -325,7 +280,7 @@ namespace lp { TRACE("lar_solver_improve_bounds", tout << "d[" << j << "] = " << d_j << "\n"; this->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, tout);); - const ul_pair& ul = m_columns_to_ul_pairs[j]; + const column& ul = m_columns[j]; u_dependency * bound_dep; if (d_j.is_pos()) bound_dep = ul.upper_bound_witness(); @@ -411,7 +366,7 @@ namespace lp { auto& d = rslv.m_d; auto& costs = rslv.m_costs; for (lar_term::ival p : term) { - unsigned j = p.column(); + unsigned j = p.j(); costs[j] = zero_of_type(); int i = rslv.m_basis_heading[j]; if (i < 0) @@ -433,7 +388,7 @@ namespace lp { move_non_basic_columns_to_bounds(); rslv.m_costs.resize(A_r().column_count(), zero_of_type()); for (lar_term::ival p : term) { - unsigned j = p.column(); + unsigned j = p.j(); rslv.m_costs[j] = p.coeff(); if (rslv.m_basis_heading[j] < 0) rslv.m_d[j] += p.coeff(); @@ -540,28 +495,28 @@ namespace lp { lp_assert(is_base(j)); unsigned i = row_of_basic_column(j); for (const auto & c : A_r().m_rows[i]) - if (j != c.var() && !is_fixed(c.var())) + if (j != c.var() && !column_is_fixed(c.var())) return m_mpq_lar_core_solver.m_r_solver.remove_from_basis_core(c.var(), j); return false; } - lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const { - if (tv::is_term(j_or_term)) { - return get_term(j_or_term); + lar_term lar_solver::get_term_to_maximize(unsigned j) const { + if (column_has_term(j)) { + return * m_columns[j].term(); } - if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) { + if (j < m_mpq_lar_core_solver.m_r_x.size()) { lar_term r; - r.add_monomial(one_of_type(), j_or_term); + r.add_monomial(one_of_type(), j); return r; } return lar_term(); // return an empty term } - lp_status lar_solver::maximize_term(unsigned j_or_term, + lp_status lar_solver::maximize_term(unsigned j, impq& term_max) { TRACE("lar_solver", print_values(tout);); SASSERT(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); - lar_term term = get_term_to_maximize(j_or_term); + lar_term term = get_term_to_maximize(j); if (term.is_empty()) return lp_status::UNBOUNDED; impq prev_value = term.apply(m_mpq_lar_core_solver.m_r_x); auto backup = m_mpq_lar_core_solver.m_r_x; @@ -607,13 +562,6 @@ namespace lp { return lp_status::FEASIBLE; } - - - const lar_term& lar_solver::get_term(unsigned j) const { - lp_assert(tv::is_term(j)); - return *m_terms[tv::unmask_term(j)]; - } - void lar_solver::pop_core_solver_params() { pop_core_solver_params(1); } @@ -624,17 +572,17 @@ namespace lp { - void lar_solver::set_upper_bound_witness(var_index j, u_dependency* dep) { - m_trail.push(vector_value_trail(m_columns_to_ul_pairs, j)); - m_columns_to_ul_pairs[j].upper_bound_witness() = dep; + void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep) { + m_trail.push(vector_value_trail(m_columns, j)); + m_columns[j].upper_bound_witness() = dep; } - void lar_solver::set_lower_bound_witness(var_index j, u_dependency* dep) { - m_trail.push(vector_value_trail(m_columns_to_ul_pairs, j)); - m_columns_to_ul_pairs[j].lower_bound_witness() = dep; + void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep) { + m_trail.push(vector_value_trail(m_columns, j)); + m_columns[j].lower_bound_witness() = dep; } - void lar_solver::register_monoid_in_map(std::unordered_map& coeffs, const mpq& a, unsigned j) { + void lar_solver::register_monoid_in_map(std::unordered_map& coeffs, const mpq& a, unsigned j) { auto it = coeffs.find(j); if (it == coeffs.end()) coeffs[j] = a; @@ -643,19 +591,19 @@ namespace lp { } - void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, - vector>& left_side) const { - std::unordered_map coeffs; + void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, + vector>& left_side) const { + std::unordered_map coeffs; for (auto& t : left_side_with_terms) { unsigned j = t.second; - if (!tv::is_term(j)) { + if (!column_has_term(j)) { register_monoid_in_map(coeffs, t.first, j); } else { - const lar_term& term = *m_terms[tv::unmask_term(t.second)]; + const lar_term& term = *m_columns[t.second].term(); for (auto p : term) - register_monoid_in_map(coeffs, t.first * p.coeff(), p.column()); + register_monoid_in_map(coeffs, t.first * p.coeff(), p.j()); } } @@ -675,16 +623,16 @@ namespace lp { unsigned num = A_r().column_count(); unsigned_vector to_remove; for (unsigned j : m_fixed_base_var_set) { - if (j >= num || !is_base(j) || !is_fixed(j)) { + if (j >= num || !is_base(j) || !column_is_fixed(j)) { to_remove.push_back(j); continue; } - lp_assert(is_base(j) && is_fixed(j)); + lp_assert(is_base(j) && column_is_fixed(j)); auto const& r = basic2row(j); for (auto const& c : r) { unsigned j_entering = c.var(); - if (!is_fixed(j_entering)) { + if (!column_is_fixed(j_entering)) { pivot(j_entering, j); to_remove.push_back(j); lp_assert(is_base(j_entering)); @@ -839,15 +787,12 @@ namespace lp { return r; } - bool lar_solver::var_is_registered(var_index vj) const { - if (tv::is_term(vj)) { - return tv::unmask_term(vj) < m_terms.size(); - } - return vj < A_r().column_count(); + bool lar_solver::var_is_registered(lpvar vj) const { + return vj < A_r().column_count(); } - bool lar_solver::all_constrained_variables_are_registered(const vector>& left_side) { + bool lar_solver::all_constrained_variables_are_registered(const vector>& left_side) { for (auto it : left_side) { if (!var_is_registered(it.second)) return false; @@ -858,7 +803,7 @@ namespace lp { bool lar_solver::all_constraints_hold() const { if (m_settings.get_cancel_flag()) return true; - std::unordered_map var_map; + std::unordered_map var_map; get_model_do_not_care_about_diff_vars(var_map); for (auto const& c : m_constraints.active()) { @@ -874,7 +819,7 @@ namespace lp { return true; } - bool lar_solver::constraint_holds(const lar_base_constraint& constr, std::unordered_map& var_map) const { + bool lar_solver::constraint_holds(const lar_base_constraint& constr, std::unordered_map& var_map) const { mpq left_side_val = get_left_side_val(constr, var_map); switch (constr.kind()) { case LE: return left_side_val <= constr.rhs(); @@ -889,7 +834,7 @@ namespace lp { } - void lar_solver::register_in_map(std::unordered_map& coeffs, const lar_base_constraint& cn, const mpq& a) { + void lar_solver::register_in_map(std::unordered_map& coeffs, const lar_base_constraint& cn, const mpq& a) { for (auto& it : cn.coeffs()) { unsigned j = it.second; auto p = coeffs.find(j); @@ -904,7 +849,7 @@ namespace lp { } bool lar_solver::the_left_sides_sum_to_zero(const vector>& evidence) const { - std::unordered_map coeff_map; + std::unordered_map coeff_map; for (auto const & [coeff, con_ind] : evidence) { lp_assert(m_constraints.valid_index(con_ind)); register_in_map(coeff_map, m_constraints[con_ind], coeff); @@ -966,13 +911,13 @@ namespace lp { return ret; } - bool lar_solver::has_lower_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const { + bool lar_solver::has_lower_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const { - if (var >= m_columns_to_ul_pairs.size()) { + if (var >= m_columns.size()) { // TBD: bounds on terms could also be used, caller may have to track these. return false; } - const ul_pair& ul = m_columns_to_ul_pairs[var]; + const column& ul = m_columns[var]; ci = ul.lower_bound_witness(); if (ci != nullptr) { auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var]; @@ -985,13 +930,13 @@ namespace lp { } } - bool lar_solver::has_upper_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const { + bool lar_solver::has_upper_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const { - if (var >= m_columns_to_ul_pairs.size()) { + if (var >= m_columns.size()) { // TBD: bounds on terms could also be used, caller may have to track these. return false; } - const ul_pair& ul = m_columns_to_ul_pairs[var]; + const column& ul = m_columns[var]; ci = ul.upper_bound_witness(); if (ci != nullptr) { auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; @@ -1004,12 +949,12 @@ namespace lp { } } - bool lar_solver::has_value(var_index var, mpq& value) const { - if (tv::is_term(var)) { + bool lar_solver::has_value(lpvar var, mpq& value) const { + if (column_has_term(var)) { lar_term const& t = get_term(var); value = 0; for (lar_term::ival cv : t) { - impq const& r = get_column_value(cv.column()); + impq const& r = get_column_value(cv.j()); if (!numeric_traits::is_zero(r.y)) return false; value += r.x * cv.coeff(); } @@ -1049,7 +994,7 @@ namespace lp { unsigned j = it.second; int adj_sign = coeff.is_pos() ? inf_sign : -inf_sign; - const ul_pair& ul = m_columns_to_ul_pairs[j]; + const column& ul = m_columns[j]; u_dependency* bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); svector deps; @@ -1062,7 +1007,7 @@ namespace lp { } // (x, y) != (x', y') => (x + delta*y) != (x' + delta*y') - void lar_solver::get_model(std::unordered_map& variable_values) const { + void lar_solver::get_model(std::unordered_map& variable_values) const { variable_values.clear(); if (!init_model()) return; @@ -1070,7 +1015,7 @@ namespace lp { unsigned n = m_mpq_lar_core_solver.m_r_x.size(); for (unsigned j = 0; j < n; j++) - variable_values[j] = get_value(column_index(j)); + variable_values[j] = get_value(j); TRACE("lar_solver_model", tout << "delta = " << m_delta << "\nmodel:\n"; for (auto p : variable_values) tout << this->get_variable_name(p.first) << " = " << p.second << "\n";); @@ -1108,7 +1053,7 @@ namespace lp { return true; } - void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map& variable_values) const { + void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map& variable_values) const { mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1)); for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++) { const impq& rp = m_mpq_lar_core_solver.m_r_x[i]; @@ -1116,32 +1061,13 @@ namespace lp { } } - mpq lar_solver::get_value(column_index const& j) const { + mpq lar_solver::get_value(lpvar j) const { SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE); VERIFY(m_columns_with_changed_bounds.empty()); numeric_pair const& rp = get_column_value(j); return from_model_in_impq_to_mpq(rp); } - mpq lar_solver::get_tv_value(tv const& t) const { - if (t.is_var()) - return get_value(t.column()); -#if 0 - unsigned term_j = 0; - if (m_var_register.term_is_used(t.id(), term_j)) - return get_value(column_index(term_j)); -#endif - mpq r(0); - for (lar_term::ival p : get_term(t)) - r += p.coeff() * get_value(p.column()); - return r; - } - //fetches the cached value of the term or the variable by the given index - const impq& lar_solver::get_tv_ivalue(tv const& t) const { - unsigned j = t.is_var()? (unsigned)t.column(): this->map_term_index_to_column_index(t.index()); - return this->get_column_value(j); - } - void lar_solver::get_rid_of_inf_eps() { bool y_is_zero = true; for (unsigned j = 0; j < number_of_vars(); j++) { @@ -1162,13 +1088,13 @@ namespace lp { } } - void lar_solver::set_variable_name(var_index vi, std::string name) { + void lar_solver::set_variable_name(lpvar vi, std::string name) { m_var_register.set_name(vi, name); } - std::string lar_solver::get_variable_name(var_index j) const { - if (tv::is_term(j)) - return std::string("_t") + T_to_string(tv::unmask_term(j)); + std::string lar_solver::get_variable_name(lpvar j) const { + if (column_has_term(j)) + return std::string("_t") + T_to_string(j); if (j >= m_var_register.size()) return std::string("_s") + T_to_string(j); @@ -1180,7 +1106,7 @@ namespace lp { return std::string("j") + T_to_string(m_var_register.local_to_external(j)); } else { - std::string s = column_corresponds_to_term(j) ? "t" : "j"; + std::string s = column_has_term(j) ? "t" : "j"; return s + T_to_string(j); } } @@ -1225,7 +1151,7 @@ namespace lp { out << " - "; else if (val != numeric_traits::one()) out << T_to_string(val); - out << this->get_variable_name(p.column()); + out << this->get_variable_name(p.j()); } return out; } @@ -1235,10 +1161,10 @@ namespace lp { return out; } - mpq lar_solver::get_left_side_val(const lar_base_constraint& cns, const std::unordered_map& var_map) const { + mpq lar_solver::get_left_side_val(const lar_base_constraint& cns, const std::unordered_map& var_map) const { mpq ret = cns.get_free_coeff_of_left_side(); for (auto& it : cns.coeffs()) { - var_index j = it.second; + lpvar j = it.second; auto vi = var_map.find(j); lp_assert(vi != var_map.end()); ret += it.first * vi->second; @@ -1247,13 +1173,13 @@ namespace lp { } - void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const* vars, vector& column_list) { + void lar_solver::fill_var_set_for_random_update(unsigned sz, lpvar const* vars, vector& column_list) { TRACE("lar_solver_rand", tout << "sz = " << sz << "\n";); for (unsigned i = 0; i < sz; i++) { - var_index var = vars[i]; - if (tv::is_term(var)) { - if (term_is_used_as_row(tv::unmask_term(var))) { - column_list.push_back(map_term_index_to_column_index(var)); + lpvar var = vars[i]; + if (column_has_term(var)) { + if (m_columns[var].associated_with_row()) { + column_list.push_back(var); } } else { @@ -1262,7 +1188,7 @@ namespace lp { } } - void lar_solver::random_update(unsigned sz, var_index const* vars) { + void lar_solver::random_update(unsigned sz, lpvar const* vars) { vector column_list; fill_var_set_for_random_update(sz, vars, column_list); random_updater ru(*this, column_list); @@ -1280,7 +1206,7 @@ namespace lp { } bool lar_solver::column_represents_row_in_tableau(unsigned j) { - return m_columns_to_ul_pairs[j].associated_with_row(); + return m_columns[j].associated_with_row(); } void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { @@ -1430,7 +1356,7 @@ namespace lp { bool lar_solver::term_is_int(const lar_term* t) const { for (auto const p : *t) - if (!(column_is_int(p.column()) && p.coeff().is_int())) + if (!(column_is_int(p.j()) && p.coeff().is_int())) return false; return true; } @@ -1442,14 +1368,9 @@ namespace lp { return true; } - bool lar_solver::var_is_int(var_index v) const { - if (tv::is_term(v)) { - lar_term const& t = get_term(v); - return term_is_int(&t); - } - else { - return column_is_int(v); - } + bool lar_solver::var_is_int(lpvar v) const { + SASSERT(!column_has_term(v) || term_is_int(&get_term(v)) == column_is_int(v)); + return column_is_int(v); } bool lar_solver::column_is_int(unsigned j) const { @@ -1466,34 +1387,26 @@ namespace lp { // below is the initialization functionality of lar_solver - bool lar_solver::strategy_is_undecided() const { - return m_settings.simplex_strategy() == simplex_strategy_enum::undecided; - } - - var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::string& name) { - var_index j = add_var(ext_j, is_int); + lpvar lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::string& name) { + lpvar j = add_var(ext_j, is_int); m_var_register.set_name(j, name); return j; } - unsigned lar_solver::external_to_column_index(unsigned ext_j) const { - unsigned j = external_to_local(ext_j); - if (j == null_lpvar) - return j; - - if (tv::is_term(j)) - return map_term_index_to_column_index(j); - - return j; - } - struct lar_solver::undo_add_column : public trail { lar_solver& s; undo_add_column(lar_solver& s) : s(s) {} void undo() override { + auto& col = s.m_columns.back(); + if (col.term() != nullptr) { + if (s.m_need_register_terms) + s.deregister_normalized_term(*col.term()); + delete col.term(); + s.m_terms.pop_back(); + } s.remove_last_column_from_tableau(); - s.m_columns_to_ul_pairs.pop_back(); - unsigned j = s.m_columns_to_ul_pairs.size(); + s.m_columns.pop_back(); + unsigned j = s.m_columns.size(); if (s.m_columns_with_changed_bounds.contains(j)) s.m_columns_with_changed_bounds.remove(j); if (s.m_incorrect_columns.contains(j)) @@ -1501,29 +1414,14 @@ namespace lp { } }; - struct lar_solver::undo_add_term : public trail { - lar_solver& s; - undo_add_term(lar_solver& s):s(s) {} - void undo() override { - auto* t = s.m_terms.back(); - if (s.m_need_register_terms) - s.deregister_normalized_term(*t); - delete t; - s.m_terms.pop_back(); - s.m_term_register.shrink(s.m_terms.size()); - } - }; - - var_index lar_solver::add_var(unsigned ext_j, bool is_int) { + lpvar lar_solver::add_var(unsigned ext_j, bool is_int) { TRACE("add_var", tout << "adding var " << ext_j << (is_int ? " int" : " nonint") << std::endl;); - var_index local_j; - SASSERT(!m_term_register.external_is_used(ext_j)); - lp_assert(!tv::is_term(ext_j)); + lpvar local_j; if (m_var_register.external_is_used(ext_j, local_j)) return local_j; - lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count()); + lp_assert(m_columns.size() == A_r().column_count()); local_j = A_r().column_count(); - m_columns_to_ul_pairs.push_back(ul_pair(false)); // not associated with a row + m_columns.push_back(column(false, nullptr)); // false - not associated with a row, nullptr for term m_trail.push(undo_add_column(*this)); while (m_usage_in_terms.size() <= ext_j) m_usage_in_terms.push_back(0); @@ -1536,17 +1434,17 @@ namespace lp { return m_var_register.has_int_var(); } - void lar_solver::register_new_ext_var_index(unsigned ext_v, bool is_int) { + void lar_solver::register_new_external_var(unsigned ext_v, bool is_int) { lp_assert(!m_var_register.external_is_used(ext_v)); m_var_register.add_var(ext_v, is_int); } bool lar_solver::external_is_used(unsigned v) const { - return m_var_register.external_is_used(v) || m_term_register.external_is_used(v); + return m_var_register.external_is_used(v); } void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) { - register_new_ext_var_index(ext_j, is_int); + register_new_external_var(ext_j, is_int); m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); add_new_var_to_core_fields_for_mpq(false); // false for not adding a row } @@ -1578,7 +1476,7 @@ namespace lp { } #if Z3DEBUG_CHECK_UNIQUE_TERMS - bool lar_solver::term_coeffs_are_ok(const vector>& coeffs) { + bool lar_solver::term_coeffs_are_ok(const vector>& coeffs) { for (const auto& p : coeffs) if (column_is_real(p.second)) @@ -1603,50 +1501,40 @@ namespace lp { } #endif - void lar_solver::push_term(lar_term* t) { - m_terms.push_back(t); - m_trail.push(undo_add_term(*this)); - } - + // terms - bool lar_solver::all_vars_are_registered(const vector>& coeffs) { + bool lar_solver::all_vars_are_registered(const vector>& coeffs) { return all_of(coeffs, [&](const auto& p) { return p.second < m_var_register.size(); }); } void lar_solver::subst_known_terms(lar_term* t) { std::set seen_terms; for (auto p : *t) { - auto j = p.column(); - if (this->column_corresponds_to_term(j)) + auto j = p.j(); + if (this->column_has_term(j)) seen_terms.insert(j); } while (!seen_terms.empty()) { unsigned j = *seen_terms.begin(); seen_terms.erase(j); - auto tj = this->m_var_register.local_to_external(j); - auto& ot = this->get_term(tj); + const lar_term& ot = this->get_term(j); for (auto p : ot) - if (this->column_corresponds_to_term(p.column())) - seen_terms.insert(p.column()); + if (this->column_has_term(p.j())) + seen_terms.insert(p.j()); t->subst_by_term(ot, j); } } - // do not register in m_var_register this term if ext_i == UINT_MAX - var_index lar_solver::add_term(const vector>& coeffs, unsigned ext_i) { - TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); + // if UINT_MAX == null_lpvar then the term does not correspond and external variable + lpvar lar_solver::add_term(const vector>& coeffs, unsigned ext_i) { + TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); SASSERT(!m_var_register.external_is_used(ext_i)); SASSERT(all_vars_are_registered(coeffs)); lar_term* t = new lar_term(coeffs); subst_known_terms(t); - m_term_register.add_var(ext_i, term_is_int(t)); - push_term(t); - if (strategy_is_undecided()) - return tv::mask_term(m_terms.size() - 1); - SASSERT(m_terms.size() == m_term_register.size()); - unsigned adjusted_term_index = m_terms.size() - 1; - var_index ret = tv::mask_term(adjusted_term_index); - if (!coeffs.empty()) - add_row_from_term_no_constraint(m_terms.back(), ret); + SASSERT(t->is_empty() == false); + m_terms.push_back(t); + lpvar ret = A_r().column_count(); + add_row_from_term_no_constraint(t, ext_i); lp_assert(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) @@ -1654,26 +1542,15 @@ namespace lp { return ret; } - /** - * \brief ensure there is a column index corresponding to vi - * If vi is already a column, just return vi - * If vi is for a term, then create a row that uses the term. - */ - var_index lar_solver::ensure_column(var_index vi) { - if (lp::tv::is_term(vi)) - return to_column(vi); - else - return vi; - } - - - void lar_solver::add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index) { + void lar_solver::add_row_from_term_no_constraint(lar_term* term, unsigned ext_index) { TRACE("dump_terms", print_term(*term, tout) << std::endl;); - register_new_ext_var_index(term_ext_index, term_is_int(term)); + register_new_external_var(ext_index, term_is_int(term)); // j will be a new variable unsigned j = A_r().column_count(); - ul_pair ul(true); // to mark this column as associated_with_row - m_columns_to_ul_pairs.push_back(ul); + SASSERT(ext_index == null_lpvar || external_to_local(ext_index) == j); + column ul(true, term); // true - to mark this column as associated_with_row + term->j() = j; // point from the term to the column + m_columns.push_back(ul); m_trail.push(undo_add_column(*this)); add_basic_var_to_core_fields(); @@ -1684,7 +1561,7 @@ namespace lp { m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1)); for (lar_term::ival c : *term) { - unsigned j = c.column(); + unsigned j = c.j(); while (m_usage_in_terms.size() <= j) m_usage_in_terms.push_back(0); m_usage_in_terms[j] = m_usage_in_terms[j] + 1; @@ -1700,13 +1577,13 @@ namespace lp { return !column_is_int(j) || 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 lar_solver::add_var_bound_check_on_equal(lpvar j, lconstraint_kind kind, const mpq& right_side, lpvar& 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 lar_solver::add_var_bound(lpvar j, lconstraint_kind kind, const mpq& right_side) { constraint_index ci = mk_var_bound(j, kind, right_side); activate(ci); return ci; @@ -1756,7 +1633,7 @@ namespace lp { // SASSERT(column_is_fixed(k)); if (j != k && column_is_fixed(k)) { SASSERT(column_is_int(j) == column_is_int(k)); - equal_to_j = column_to_reported_index(k); + equal_to_j = k; TRACE("lar_solver", tout << "found equal column k = " << k << ", external = " << equal_to_j << "\n";); } @@ -1796,10 +1673,10 @@ namespace lp { } - constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq& right_side) { + constraint_index lar_solver::mk_var_bound(lpvar j, lconstraint_kind kind, const mpq& right_side) { TRACE("lar_solver", tout << "j = " << get_variable_name(j) << " " << lconstraint_kind_string(kind) << " " << right_side << std::endl;); constraint_index ci; - if (!tv::is_term(j)) { // j is a var + if (!column_has_term(j)) { mpq rs = adjust_bound_for_int(j, kind, right_side); lp_assert(bound_is_integer_for_integer_column(j, rs)); ci = m_constraints.add_var_constraint(j, kind, rs); @@ -1811,9 +1688,7 @@ namespace lp { return ci; } - bool lar_solver::compare_values(var_index j, lconstraint_kind k, const mpq& rhs) { - if (tv::is_term(j)) - j = to_column(j); + bool lar_solver::compare_values(lpvar j, lconstraint_kind k, const mpq& rhs) { return compare_values(get_column_value(j), k, rhs); } @@ -1897,7 +1772,7 @@ namespace lp { void lar_solver::add_constraint_to_validate(lar_solver& ls, constraint_index ci) { auto const& c = m_constraints[ci]; TRACE("lar_solver_validate", tout << "adding constr with column = "<< c.column() << "\n"; m_constraints.display(tout, c); tout << std::endl;); - vector> coeffs; + vector> coeffs; for (auto p : c.coeffs()) { lpvar jext = p.second; lpvar j = ls.external_to_local(jext); @@ -1910,7 +1785,7 @@ namespace lp { lpvar column_ext = c.column(); unsigned j = ls.external_to_local(column_ext); - var_index tv; + lpvar tv; if (j == UINT_MAX) { tv = ls.add_term(coeffs, column_ext); } @@ -1959,37 +1834,10 @@ namespace lp { } } - constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side) { - lp_assert(tv::is_term(j)); - unsigned adjusted_term_index = tv::unmask_term(j); - // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); - unsigned term_j; - lar_term const* term = m_terms[adjusted_term_index]; - if (m_var_register.external_is_used(j, term_j)) { - mpq rs = adjust_bound_for_int(term_j, kind, right_side); - lp_assert(bound_is_integer_for_integer_column(term_j, rs)); - return m_constraints.add_term_constraint(term_j, term, kind, rs); - } - else { - return add_constraint_from_term_and_create_new_column_row(j, term, kind, right_side); - } - } - - 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 lar_solver::add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side) { mpq rs = adjust_bound_for_int(j, kind, right_side); - lp_assert(bound_is_integer_for_integer_column(j, rs)); - return m_constraints.add_term_constraint(j, term, kind, rs); - } - - void lar_solver::decide_on_strategy_and_adjust_initial_state() { - lp_assert(strategy_is_undecided()); - - m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; - - adjust_initial_state(); + SASSERT(bound_is_integer_for_integer_column(j, rs)); + return m_constraints.add_term_constraint(j, m_columns[j].term(), kind, rs); } struct scoped_backup { @@ -2001,31 +1849,7 @@ namespace lp { m_s.restore_x(); } }; - - - void lar_solver::adjust_initial_state() { - switch (m_settings.simplex_strategy()) { - case simplex_strategy_enum::tableau_rows: - adjust_initial_state_for_tableau_rows(); - break; - case simplex_strategy_enum::tableau_costs: - UNREACHABLE(); // not implemented - case simplex_strategy_enum::undecided: - adjust_initial_state_for_tableau_rows(); - break; - } - } - - - void lar_solver::adjust_initial_state_for_tableau_rows() { - for (unsigned i = 0; i < m_terms.size(); i++) { - if (m_var_register.external_is_used(tv::mask_term(i))) - continue; - add_row_from_term_no_constraint(m_terms[i], tv::mask_term(i)); - } - } - - + void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { SASSERT(column_has_upper_bound(j)); if (column_has_lower_bound(j)) { @@ -2046,7 +1870,7 @@ namespace lp { } } - void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { + void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j)); lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed); @@ -2111,7 +1935,7 @@ namespace lp { } } - void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { + void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j)); lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); @@ -2164,7 +1988,7 @@ namespace lp { } } - void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { + void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j)); lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); mpq y_of_bound(0); @@ -2217,7 +2041,7 @@ namespace lp { } } - void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { + void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) { lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j)); mpq y_of_bound(0); @@ -2252,22 +2076,14 @@ namespace lp { UNREACHABLE(); } insert_to_columns_with_changed_bounds(j); - } - - bool lar_solver::column_corresponds_to_term(unsigned j) const { - return tv::is_term(m_var_register.local_to_external(j)); - } + } - var_index lar_solver::to_column(unsigned ext_j) const { + lpvar lar_solver::to_column(unsigned ext_j) const { return m_var_register.external_to_local(ext_j); } - bool lar_solver::tighten_term_bounds_by_delta(tv const& t, const impq& delta) { - SASSERT(t.is_term()); - unsigned tj = t.index(); - unsigned j; - if (!m_var_register.external_is_used(tj, j)) - return true; // the term is not a column so it has no bounds + bool lar_solver::tighten_term_bounds_by_delta(lpvar j, const impq& delta) { + SASSERT(column_has_term(j)); auto& slv = m_mpq_lar_core_solver.m_r_solver; TRACE("cube", tout << "delta = " << delta << std::endl; m_int_solver->display_column(tout, j); ); @@ -2280,15 +2096,15 @@ namespace lp { TRACE("cube", tout << "can tighten";); if (slv.column_has_upper_bound(j)) { if (!is_zero(delta.y) || !is_zero(slv.m_upper_bounds[j].y)) - add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x); + add_var_bound(j, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x); else - add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x); + add_var_bound(j, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x); } if (slv.column_has_lower_bound(j)) { if (!is_zero(delta.y) || !is_zero(slv.m_lower_bounds[j].y)) - add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x); + add_var_bound(j, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x); else - add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x); + add_var_bound(j, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x); } return true; } @@ -2297,7 +2113,7 @@ namespace lp { void lar_solver::round_to_integer_solution() { for (unsigned j = 0; j < column_count(); j++) { if (!column_is_int(j)) continue; - if (column_corresponds_to_term(j)) continue; + if (column_has_term(j)) continue; impq& v = m_mpq_lar_core_solver.m_r_x[j]; if (v.is_int()) continue; @@ -2322,20 +2138,20 @@ namespace lp { void lar_solver::fix_terms_with_rounded_columns() { - for (unsigned i = 0; i < m_terms.size(); i++) { - if (!term_is_used_as_row(i)) + for (const lar_term* t : m_terms) { + lpvar j = t->j(); + if (!m_columns[j].associated_with_row()) continue; bool need_to_fix = false; - const lar_term& t = *m_terms[i]; - for (lar_term::ival p : t) { - if (m_incorrect_columns.contains(p.column())) { + + for (lar_term::ival p : * t) { + if (m_incorrect_columns.contains(p.j())) { need_to_fix = true; break; } } if (need_to_fix) { - lpvar j = m_var_register.external_to_local(tv::mask_term(i)); - impq v = t.apply(m_mpq_lar_core_solver.m_r_x); + impq v = t->apply(m_mpq_lar_core_solver.m_r_x); m_mpq_lar_core_solver.m_r_solver.update_x(j, v); } } @@ -2347,7 +2163,7 @@ namespace lp { bool lar_solver::sum_first_coords(const lar_term& t, mpq& val) const { val = zero_of_type(); for (lar_term::ival c : t) { - const auto& x = m_mpq_lar_core_solver.m_r_x[c.column()]; + const auto& x = m_mpq_lar_core_solver.m_r_x[c.j()]; if (!is_zero(x.y)) return false; val += x.x * c.coeff(); @@ -2355,18 +2171,14 @@ namespace lp { return true; } - bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq& rs, u_dependency*& ci, bool& upper_bound) const { - lp_assert(t.is_term()); - unsigned j; - bool is_int; - if (!m_var_register.external_is_used(t.index(), j, is_int)) - return false; // the term does not have a bound because it does not correspond to a column - if (!is_int) // todo - allow for the next version of hnf + bool lar_solver::get_equality_and_right_side_for_term_on_current_x(lpvar j, mpq& rs, u_dependency*& ci, bool& upper_bound) const { + lp_assert(column_has_term(j)); + if (!column_is_int(j)) // todo - allow for the next version of hnf return false; bool rs_is_calculated = false; mpq b; bool is_strict; - const lar_term& term = get_term(t); + const lar_term& term = get_term(j); if (has_upper_bound(j, ci, b, is_strict) && !is_strict) { lp_assert(b.is_int()); if (!sum_first_coords(term, rs)) @@ -2433,9 +2245,8 @@ namespace lp { void lar_solver::register_existing_terms() { if (!m_need_register_terms) { TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";); - for (unsigned k = 0; k < m_terms.size(); k++) { - lpvar j = m_var_register.external_to_local(tv::mask_term(k)); - register_normalized_term(*m_terms[k], j); + for (const lar_term* t : m_terms) { + register_normalized_term(*t, t->j()); } } m_need_register_terms = true; @@ -2455,44 +2266,19 @@ namespace lp { return false; } - lar_term lar_solver::unfold_nested_subterms(lar_term const& term) { - lar_term result; - vector> todo; - for (auto const & [j,c] : term.coeffs()) - todo.push_back({j, c}); - while (!todo.empty()) { - auto [j, c] = todo.back(); - todo.pop_back(); - auto tv = column2tv(j); - if (tv.is_term()) { - for (auto const& [j, c2] : get_term(tv).coeffs()) - todo.push_back({j, c*c2}); - } - else - result.add_monomial(c, j); - } - return result; - } - - std::pair lar_solver::add_equality(lpvar j, lpvar k) { - vector> coeffs; - if (tv::is_term(j)) - j = map_term_index_to_column_index(j); - - if (tv::is_term(k)) - k = map_term_index_to_column_index(k); - + vector> coeffs; + coeffs.push_back(std::make_pair(mpq(1), j)); coeffs.push_back(std::make_pair(mpq(-1), k)); - unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var + unsigned ej = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var if (get_column_value(j) != get_column_value(k)) set_status(lp_status::UNKNOWN); return std::pair( - add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), - add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); + add_var_bound(ej, lconstraint_kind::LE, mpq(0)), + add_var_bound(ej, lconstraint_kind::GE, mpq(0))); } bool lar_solver::inside_bounds(lpvar j, const impq& val) const { @@ -2511,7 +2297,7 @@ namespace lp { SASSERT(m_crossed_bounds_deps == nullptr); set_status(lp_status::INFEASIBLE); m_crossed_bounds_column = j; - const auto& ul = this->m_columns_to_ul_pairs[j]; + const auto& ul = this->m_columns[j]; u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness(); SASSERT(bdep != nullptr); m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index b1abb21f797..4d71d0181da 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -59,7 +59,7 @@ class lar_solver : public column_namer { size_t seed = 0; int i = 0; for (const auto p : t) { - hash_combine(seed, (unsigned)p.column()); + hash_combine(seed, (unsigned)p.j()); hash_combine(seed, p.coeff()); if (i++ > 10) break; @@ -86,8 +86,7 @@ class lar_solver : public column_namer { int_solver* m_int_solver = nullptr; bool m_need_register_terms = false; var_register m_var_register; - var_register m_term_register; - svector m_columns_to_ul_pairs; + svector m_columns; constraint_set m_constraints; // the set of column indices j such that bounds have changed for j indexed_uint_set m_columns_with_changed_bounds; @@ -119,16 +118,13 @@ class lar_solver : public column_namer { ////////////////// nested structs ///////////////////////// struct undo_add_column; - struct undo_add_term; ////////////////// methods //////////////////////////////// static bool valid_index(unsigned j) { return static_cast(j) >= 0; } - const lar_term& get_term(unsigned j) const; bool row_has_a_big_num(unsigned i) const; // init region - bool strategy_is_undecided() const; - void register_new_ext_var_index(unsigned ext_v, bool is_int); + void register_new_external_var(unsigned ext_v, bool is_int); bool term_is_int(const lar_term* t) const; bool term_is_int(const vector>& coeffs) const; void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); @@ -136,10 +132,9 @@ class lar_solver : public column_namer { mpq adjust_bound_for_int(lpvar j, lconstraint_kind&, const mpq&); // terms - bool all_vars_are_registered(const vector>& coeffs); - bool term_coeffs_are_ok(const vector>& coeffs); - void push_term(lar_term* t); - void add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index); + bool all_vars_are_registered(const vector>& coeffs); + bool term_coeffs_are_ok(const vector>& coeffs); + void add_row_from_term_no_constraint(lar_term* term, unsigned term_ext_index); void add_basic_var_to_core_fields(); bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs); @@ -168,27 +163,20 @@ class lar_solver : public column_namer { void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); private: void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; } - void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); 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); + constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side); void set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep); - 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(); - void adjust_initial_state(); - void adjust_initial_state_for_tableau_rows(); bool sizes_are_correct() const; bool implied_bound_is_correctly_explained(implied_bound const& be, const vector>& explanation) const; - void substitute_basis_var_in_terms_for_row(unsigned i); - template unsigned calculate_implied_bounds_for_row(unsigned row_index, lp_bound_propagator& bp) { if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation || row_has_a_big_num(row_index)) @@ -214,10 +202,10 @@ class lar_solver : public column_namer { void pop_core_solver_params(); void pop_core_solver_params(unsigned k); - void set_upper_bound_witness(var_index j, u_dependency* ci); - void set_lower_bound_witness(var_index j, u_dependency* ci); - void substitute_terms_in_linear_expression(const vector>& left_side_with_terms, - vector>& left_side) const; + void set_upper_bound_witness(lpvar j, u_dependency* ci); + void set_lower_bound_witness(lpvar j, u_dependency* ci); + void substitute_terms_in_linear_expression(const vector>& left_side_with_terms, + vector>& left_side) const; bool use_tableau_costs() const; bool tableau_with_costs() const; @@ -231,11 +219,11 @@ class lar_solver : public column_namer { void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); void solve_with_core_solver(); numeric_pair get_basic_var_value_from_row(unsigned i); - bool all_constrained_variables_are_registered(const vector>& left_side); + bool all_constrained_variables_are_registered(const vector>& left_side); bool all_constraints_hold() const; - bool constraint_holds(const lar_base_constraint& constr, std::unordered_map& var_map) const; - static void register_in_map(std::unordered_map& coeffs, const lar_base_constraint& cn, const mpq& a); - static void register_monoid_in_map(std::unordered_map& coeffs, const mpq& a, unsigned j); + bool constraint_holds(const lar_base_constraint& constr, std::unordered_map& var_map) const; + static void register_in_map(std::unordered_map& coeffs, const lar_base_constraint& cn, const mpq& a); + static void register_monoid_in_map(std::unordered_map& coeffs, const mpq& a, unsigned j); bool the_left_sides_sum_to_zero(const vector>& evidence) const; bool explanation_is_correct(explanation&) const; bool inf_explanation_is_correct() const; @@ -244,8 +232,8 @@ class lar_solver : public column_namer { explanation& exp, const vector>& inf_row, int inf_sign) 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); + 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, lpvar const* vars, vector& column_list); 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); @@ -259,7 +247,7 @@ class lar_solver : public column_namer { bool bound_is_integer_for_integer_column(unsigned j, const mpq& right_side) const; inline lar_core_solver& get_core_solver() { return m_mpq_lar_core_solver; } - var_index to_column(unsigned ext_j) const; + lpvar to_column(unsigned ext_j) const; void fix_terms_with_rounded_columns(); bool remove_from_basis(unsigned); lar_term get_term_to_maximize(unsigned ext_j) const; @@ -299,8 +287,6 @@ class lar_solver : public column_namer { template void remove_non_fixed_from_table(T&); - unsigned external_to_column_index(unsigned) const; - bool inside_bounds(lpvar, const impq&) const; inline void set_column_value(unsigned j, const impq& v) { @@ -311,7 +297,7 @@ class lar_solver : public column_namer { set_column_value(j, v); } - var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&); + lpvar add_named_var(unsigned ext_j, bool is_integer, const std::string&); lp_status maximize_term(unsigned j_or_term, impq& term_max); @@ -348,7 +334,7 @@ class lar_solver : public column_namer { mpq const& a = r.coeff(); int a_sign = is_pos(a) ? 1 : -1; int sign = j_sign * a_sign; - const ul_pair& ul = m_columns_to_ul_pairs[j]; + const column& ul = m_columns[j]; auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); lp_assert(witness); for (auto ci : flatten(witness)) @@ -367,10 +353,10 @@ class lar_solver : public column_namer { #ifdef Z3DEBUG bool fixed_base_removed_correctly() const; #endif - constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq& right_side); - void activate_check_on_equal(constraint_index, var_index&); + constraint_index mk_var_bound(lpvar j, lconstraint_kind kind, const mpq& right_side); + void activate_check_on_equal(constraint_index, lpvar&); void activate(constraint_index); - void random_update(unsigned sz, var_index const* vars); + void random_update(unsigned sz, lpvar const* vars); void add_column_rows_to_touched_rows(lpvar j); template void propagate_bounds_for_touched_rows(lp_bound_propagator& bp) { @@ -404,34 +390,24 @@ class lar_solver : public column_namer { } } - 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); unsigned num_scopes() const { return m_trail.get_num_scopes(); } - bool compare_values(var_index j, lconstraint_kind kind, const mpq& right_side); - var_index add_term(const vector>& coeffs, unsigned ext_i); + bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side); + lpvar add_term(const vector>& coeffs, unsigned ext_i); void register_existing_terms(); - var_index ensure_column(var_index vi); - 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&); + constraint_index add_var_bound(lpvar, lconstraint_kind, const mpq&); + constraint_index add_var_bound_check_on_equal(lpvar, lconstraint_kind, const mpq&, lpvar&); - var_index add_var(unsigned ext_j, bool is_integer); + lpvar 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; - const lar_term& column_to_term(unsigned j) const { - SASSERT(column_corresponds_to_term(j)); - return get_term(column2tv(to_column_index(j))); + inline lpvar local_to_external(lpvar idx) const { + return m_var_register.local_to_external(idx); } - - lar_term unfold_nested_subterms(lar_term const& term); - + inline bool column_associated_with_row(lpvar j) const { return m_columns[j].associated_with_row(); } inline unsigned row_count() const { return A_r().row_count(); } - bool var_is_registered(var_index vj) const; + bool var_is_registered(lpvar vj) const; void clear_inf_heap() { m_mpq_lar_core_solver.m_r_solver.inf_heap().clear(); } @@ -518,33 +494,28 @@ class lar_solver : public column_namer { u_dependency_manager& dep_manager() { return m_dependencies; } inline u_dependency* get_column_upper_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].upper_bound_witness(); + return m_columns[j].upper_bound_witness(); } - inline const impq& get_upper_bound(column_index j) const { + inline const impq& get_upper_bound(lpvar 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 { + inline const impq& get_lower_bound(lpvar j) const { return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j]; } - inline mpq bound_span_x(column_index j) const { + inline mpq bound_span_x(lpvar j) const { return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j].x - m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j].x; } - bool has_lower_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const; - bool has_upper_bound(var_index var, u_dependency*& ci, mpq& value, bool& is_strict) const; - bool has_value(var_index var, mpq& value) const; + bool has_lower_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const; + bool has_upper_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const; + bool has_value(lpvar 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; bool column_is_feasible(unsigned j) const { return m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j);} - unsigned column_to_reported_index(unsigned j) const; lp_settings& settings(); lp_settings const& settings() const; statistics& stats(); @@ -552,8 +523,6 @@ class lar_solver : public column_namer { void updt_params(params_ref const& p); column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; } const vector& get_column_types() const { return m_mpq_lar_core_solver.m_column_types(); } - 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); @@ -566,14 +535,12 @@ class lar_solver : public column_namer { } bool init_model() const; mpq from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_delta * v.y; } - mpq get_value(column_index const& j) const; - mpq get_tv_value(tv const& t) const; - const impq& get_tv_ivalue(tv const& t) const; - void get_model(std::unordered_map& variable_values) const; + mpq get_value(lpvar j) 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 override; - void set_variable_name(var_index vi, std::string); + void get_model_do_not_care_about_diff_vars(std::unordered_map& variable_values) const; + std::string get_variable_name(lpvar vi) const override; + void set_variable_name(lpvar vi, std::string); inline 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 { @@ -595,7 +562,7 @@ class lar_solver : public column_namer { std::pair add_equality(lpvar j, lpvar k); u_dependency* get_bound_constraint_witnesses_for_column(unsigned j) { - const ul_pair& ul = m_columns_to_ul_pairs[j]; + const column& ul = m_columns[j]; return m_dependencies.mk_join(ul.lower_bound_witness(), ul.upper_bound_witness()); } template @@ -613,22 +580,15 @@ class lar_solver : public column_namer { void pop(); inline u_dependency* 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(); - } - - inline tv column2tv(column_index const& c) const { - return tv::raw(column_to_reported_index(c)); + return m_columns[j].lower_bound_witness(); } - + inline bool column_has_term(lpvar j) const { return m_columns[j].term() != nullptr; } 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)) { + if (column_has_term(j)) { print_term_as_indices(get_term(j), out) << "\n"; - } else if (column_corresponds_to_term(j)) { + } else if (column_has_term(j)) { const lar_term& t = get_term(m_var_register.local_to_external(j)); print_term_as_indices(t, out) << "\n"; } @@ -651,13 +611,12 @@ class lar_solver : public column_namer { return false; } 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; } inline const int_solver* get_int_solver() const { return m_int_solver; } - inline const lar_term& get_term(tv const& t) const { - lp_assert(t.is_term()); - return *m_terms[t.id()]; + inline const lar_term& get_term(lpvar j) const { + return *m_columns[j].term(); } lp_status find_feasible_solution(); void move_non_basic_columns_to_bounds(); @@ -675,8 +634,8 @@ class lar_solver : public column_namer { inline const column_strip& get_column(unsigned i) const { return A_r().m_columns[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, u_dependency*& ci, bool& upper_bound) const; - bool var_is_int(var_index v) const; + bool get_equality_and_right_side_for_term_on_current_x(lpvar j, mpq& rs, u_dependency*& ci, bool& upper_bound) const; + bool var_is_int(lpvar v) const; inline const vector& r_heading() const { return m_mpq_lar_core_solver.m_r_heading; } inline const vector& r_basis() const { return m_mpq_lar_core_solver.r_basis(); } inline const vector& r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); } @@ -687,7 +646,7 @@ class lar_solver : public column_namer { 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&); + bool tighten_term_bounds_by_delta(lpvar j, const impq&); lar_solver(); void track_touched_rows(bool v); bool touched_rows_are_tracked() const; @@ -698,18 +657,16 @@ class lar_solver : public column_namer { 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; } // columns - bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); } - const impq& get_column_value(column_index const& 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)) { + const impq& get_column_value(lpvar j) const { return m_mpq_lar_core_solver.m_r_x[j]; } + inline lpvar external_to_local(unsigned j) const { + lpvar local_j; + if (m_var_register.external_is_used(j, local_j)) { return local_j; } else { return -1; } } - unsigned usage_in_terms(column_index j) const { + unsigned usage_in_terms(lpvar j) const { if (j >= m_usage_in_terms.size()) return 0; return m_usage_in_terms[j]; diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index a96d3ad5a11..6547377d365 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -26,8 +26,12 @@ namespace lp { class lar_term { typedef unsigned lpvar; u_map m_coeffs; + // the column index related to the term + lpvar m_j = -1; public: - lar_term() {} + // the column index related to the term + lpvar j() const { return m_j; } + lpvar& j() { return m_j; } void add_monomial(const mpq& c, unsigned j) { if (c.is_zero()) return; @@ -62,10 +66,11 @@ class lar_term { mpq a = it->get_data().m_value; this->m_coeffs.erase(term_column); for (auto p : t) { - this->add_monomial(a * p.coeff(), p.column()); + this->add_monomial(a * p.coeff(), p.j()); } } - + // constructors + lar_term() {} lar_term(const vector>& coeffs) { for (auto const& p : coeffs) { add_monomial(p.first, p.second); @@ -150,11 +155,11 @@ class lar_term { } class ival { - unsigned m_var; + lpvar m_var; const mpq & m_coeff; public: - ival(unsigned var, const mpq & val) : m_var(var), m_coeff(val) { } - column_index column() const { return column_index(m_var); } + ival(lpvar var, const mpq & val) : m_var(var), m_coeff(val) { } + lpvar j() const { return m_var; } const mpq & coeff() const { return m_coeff; } }; @@ -173,13 +178,13 @@ class lar_term { lpvar min_var = -1; mpq c; for (ival p : *this) { - if (p.column() < min_var) { - min_var = p.column(); + if (p.j() < min_var) { + min_var = p.j(); } } lar_term r; for (ival p : *this) { - if (p.column() == min_var) { + if (p.j() == min_var) { return p.coeff().is_one(); } } diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 021501ecd25..325bc980bc8 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -31,7 +31,7 @@ namespace lp_api { class bound { Literal m_bv; theory_var m_var; - lp::lpvar m_vi; + lp::lpvar m_column_index; bool m_is_int; rational m_value; bound_kind m_bound_kind; @@ -41,7 +41,7 @@ namespace lp_api { bound(Literal bv, theory_var v, lp::lpvar vi, bool is_int, rational const& val, bound_kind k, lp::constraint_index ct, lp::constraint_index cf) : m_bv(bv), m_var(v), - m_vi(vi), + m_column_index(vi), m_is_int(is_int), m_value(val), m_bound_kind(k) { @@ -53,7 +53,7 @@ namespace lp_api { theory_var get_var() const { return m_var; } - lp::tv tv() const { return lp::tv::raw(m_vi); } + lp::lpvar column_index() const { return m_column_index; } Literal get_lit() const { return m_bv; } diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index c6fa5796da0..daeac3b18ed 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -147,8 +147,6 @@ class lp_bound_propagator { void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { - j = lp().column_to_reported_index(j); - lconstraint_kind kind = is_low ? GE : LE; if (strict) kind = static_cast(kind / 2); @@ -222,14 +220,11 @@ class lp_bound_propagator { return out; } - bool add_eq_on_columns(const explanation& exp, lpvar j, lpvar k, bool is_fixed) { - lp_assert(j != k && is_int(j) == is_int(k)); - lp_assert(ival(j) == ival(k)); + bool add_eq_on_columns(const explanation& exp, lpvar je, lpvar ke, bool is_fixed) { + lp_assert(je != ke && is_int(je) == is_int(ke)); + lp_assert(ival(je) == ival(ke)); - unsigned je = lp().column_to_reported_index(j); - unsigned ke = lp().column_to_reported_index(k); TRACE("eq", - tout << "reporting eq " << j << ", " << k << "\n"; tout << "reported idx " << je << ", " << ke << "\n"; print_expl(tout, exp); tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";); @@ -246,12 +241,12 @@ class lp_bound_propagator { // column to theory_var unsigned col_to_imp(unsigned j) const { - return lp().local_to_external(lp().column_to_reported_index(j)); + return lp().local_to_external(j); } // theory_var to column unsigned imp_to_col(unsigned j) const { - return lp().external_to_column_index(j); + return lp().external_to_local(j); } bool is_int(lpvar j) const { @@ -261,7 +256,7 @@ class lp_bound_propagator { void explain_fixed_in_row(unsigned row, explanation& ex) { TRACE("eq", tout << lp().get_row(row) << std::endl); for (const auto& c : lp().get_row(row)) - if (lp().is_fixed(c.var())) + if (lp().column_is_fixed(c.var())) explain_fixed_column(c.var(), ex); } @@ -269,7 +264,7 @@ class lp_bound_propagator { unsigned base = UINT_MAX; TRACE("eq", tout << lp().get_row(row) << std::endl); for (const auto& c : lp().get_row(row)) { - if (lp().is_fixed(c.var())) { + if (lp().column_is_fixed(c.var())) { explain_fixed_column(c.var(), ex); } else if (lp().is_base(c.var())) { @@ -288,7 +283,7 @@ class lp_bound_propagator { #ifdef Z3DEBUG bool all_fixed_in_row(unsigned row) const { for (const auto& c : lp().get_row(row)) - if (!lp().is_fixed(c.var())) + if (!lp().column_is_fixed(c.var())) return false; return true; } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a0cb485b5f6..08fd365055a 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -53,9 +53,8 @@ inline std::ostream& operator<<(std::ostream& out, column_type const& t) { } enum class simplex_strategy_enum { - undecided = 3, - tableau_rows = 0, - tableau_costs = 1 + tableau_rows, + tableau_costs }; std::string column_type_to_string(column_type t); diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h index f770fe956a0..5883495fad3 100644 --- a/src/math/lp/lp_types.h +++ b/src/math/lp/lp_types.h @@ -30,72 +30,12 @@ namespace nla { namespace lp { -typedef unsigned var_index; typedef unsigned constraint_index; typedef unsigned row_index; enum lconstraint_kind { LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0, NE = 3 }; typedef unsigned lpvar; const lpvar null_lpvar = UINT_MAX; const constraint_index null_ci = UINT_MAX; - - -class column_index { - unsigned m_index; - friend class lar_solver; - friend class lar_term; - friend nla::core; - - operator unsigned() const { return m_index; } - -public: - column_index(unsigned j): m_index(j) {} - unsigned index() const { return m_index; } - bool is_null() const { return m_index == null_lpvar; } -}; - - -// index that comes from term or variable. -class tv { - unsigned m_index; - static const unsigned EF = UINT_MAX >> 1; - tv(unsigned i): m_index(i) {} -public: - static tv term(unsigned i) { SASSERT(0 == (i & left_most_bit)); return tv(mask_term(i)); } - static tv var(unsigned i) { SASSERT(0 == (i & left_most_bit)); return tv(i); } - static tv raw(unsigned i) { return tv(i); } - - // retrieve the identifier associated with tv - unsigned id() const { return unmask_term(m_index); } - column_index column() const { SASSERT(is_var()); return column_index(id()); } - - // retrieve the raw index. - unsigned index() const { return m_index; } - - bool is_term() const { return 0 != (m_index & left_most_bit); } - bool is_var() const { return 0 == (m_index & left_most_bit); } - - // utilities useful where tv isn't already encapsulating id's. - static inline unsigned unmask_term(unsigned j) { return j & EF; } - static inline bool is_term(unsigned j) { return j & left_most_bit; } - static inline unsigned mask_term(unsigned j) { return j | left_most_bit; } - - // used by var_register. could we encapsulate even this? - static const unsigned left_most_bit = ~EF; - - std::string to_string() const { - std::ostringstream strm; - strm << (is_term() ? "t" : "j") << id(); - return strm.str(); - } - - bool is_null() const { return m_index == UINT_MAX; } - -}; - - } -inline std::ostream& operator<<(std::ostream& out, lp::tv const& t) { - return out << (t.is_term() ? "t":"j") << t.id() << "\n"; -} diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index 3c1383cb39e..d6943bf50a4 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -116,12 +116,9 @@ template std::ostream& print_linear_combination_of_column_indices_only(const vector> & coeffs, std::ostream & out) { return print_linear_combination_customized( coeffs, - [](unsigned j) {std::stringstream ss; - if (tv::is_term(j)) { - ss << "t" << tv::unmask_term(j); - } else { - ss << "j" << j; - } + [](unsigned j) { + std::stringstream ss; + ss << "j" << j; return ss.str();}, out); } diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index 19137cd3143..b5113416629 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -21,15 +21,15 @@ namespace nla { class mon_eq { // fields - lp::var_index m_v; - svector m_vs; + lp::lpvar m_v; + svector m_vs; public: // constructors - mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs): + mon_eq(lp::lpvar v, unsigned sz, lp::lpvar const* vs): m_v(v), m_vs(sz, vs) { std::sort(m_vs.begin(), m_vs.end()); } - mon_eq(lp::var_index v, const svector &vs): + mon_eq(lp::lpvar v, const svector &vs): m_v(v), m_vs(vs) { std::sort(m_vs.begin(), m_vs.end()); } @@ -37,7 +37,7 @@ class mon_eq { unsigned var() const { return m_v; } unsigned size() const { return m_vs.size(); } - const svector& vars() const { return m_vs; } + const svector& vars() const { return m_vs; } bool empty() const { return m_vs.empty(); } bool is_sorted() const { for (unsigned i = 0; i + 1 < size(); i++) @@ -49,7 +49,7 @@ class mon_eq { return std::binary_search(m_vs.begin(), m_vs.end(), j); } protected: - svector& vars1() { return m_vs; } + svector& vars1() { return m_vs; } }; // support the congruence diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 9c99fa8c325..f2a1b0287d0 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -376,7 +376,7 @@ namespace nla { // propagate fixed equality auto exp = get_explanation(dep); - c().add_fixed_equality(c().lra.column_to_reported_index(m.var()), rational(0), exp); + c().add_fixed_equality(m.var(), rational(0), exp); } void monomial_bounds::propagate_fixed(monic const& m, rational const& k) { @@ -386,22 +386,21 @@ namespace nla { // propagate fixed equality auto exp = get_explanation(dep); - c().add_fixed_equality(c().lra.column_to_reported_index(m.var()), k, exp); + c().add_fixed_equality(m.var(), k, exp); } void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) { vector> coeffs; coeffs.push_back({-k, w}); coeffs.push_back({rational::one(), m.var()}); - lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX); + lp::lpvar j = c().lra.add_term(coeffs, UINT_MAX); auto* dep = explain_fixed(m, k); - term_index = c().lra.map_term_index_to_column_index(term_index); TRACE("nla_solver", tout << "propagate nonfixed " << m << " = " << k << " " << w << "\n";); - c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep); + c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, mpq(0), dep); if (k == 1) { lp::explanation exp = get_explanation(dep); - c().add_equality(c().lra.column_to_reported_index(m.var()), c().lra.column_to_reported_index(w), exp); + c().add_equality(m.var(), w, exp); } } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e2db006fa7c..675bf502231 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -68,21 +68,10 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const rational core::value(const lp::lar_term& r) const { rational ret(0); for (lp::lar_term::ival t : r) - ret += t.coeff() * val(t.column()); + ret += t.coeff() * val(t.j()); return ret; } -lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const { - lp::lar_term r; - for (lp::lar_term::ival p : t) { - lpvar j = p.column(); - if (lp::tv::is_term(j)) - j = lra.map_term_index_to_column_index(j); - r.add_monomial(p.coeff(), j); - } - return r; -} - bool core::ineq_holds(const ineq& n) const { return compare_holds(value(n.term()), n.cmp(), n.rs()); } @@ -139,10 +128,7 @@ bool core::canonize_sign(const factorization& f) const { void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) { m_add_buffer.resize(sz); for (unsigned i = 0; i < sz; i++) { - lpvar j = vs[i]; - if (lp::tv::is_term(j)) - j = lra.map_term_index_to_column_index(j); - m_add_buffer[i] = j; + m_add_buffer[i] = vs[i]; } m_emons.add(v, m_add_buffer); m_monics_with_changed_bounds.insert(v); @@ -326,25 +312,25 @@ bool core::explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& boun const rational& a = p.coeff(); SASSERT(!a.is_zero()); if (a.is_pos()) { - auto* dep = lra.get_column_lower_bound_witness(p.column()); + auto* dep = lra.get_column_lower_bound_witness(p.j()); if (!dep) return false; - bound = a * lra.get_lower_bound(p.column()).x; + bound = a * lra.get_lower_bound(p.j()).x; lra.push_explanation(dep, e); return true; } // a.is_neg() - auto* dep = lra.get_column_upper_bound_witness(p.column()); + auto* dep = lra.get_column_upper_bound_witness(p.j()); if (!dep) return false; - bound = a * lra.get_upper_bound(p.column()).x; + bound = a * lra.get_upper_bound(p.j()).x; lra.push_explanation(dep, e); return true; } bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const { const rational& a = p.coeff(); - lpvar j = p.column(); + lpvar j = p.j(); SASSERT(!a.is_zero()); if (a.is_neg()) { auto *dep = lra.get_column_lower_bound_witness(j); @@ -602,7 +588,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const { print_ineq(in, out); if (i + 1 < l.ineqs().size()) out << " or "; for (lp::lar_term::ival p: in.term()) - vars.insert(p.column()); + vars.insert(p.j()); } out << std::endl; for (lpvar j : vars) { @@ -701,13 +687,13 @@ unsigned core::random() { return lp_settings().random_next(); } void core::collect_equivs() { const lp::lar_solver& s = lra; - for (unsigned i = 0; i < s.terms().size(); i++) { - if (!s.term_is_used_as_row(i)) + for (const auto * t : s.terms()) { + if (!s.column_associated_with_row(t->j())) continue; - lpvar j = s.external_to_local(lp::tv::mask_term(i)); + lpvar j = t->j(); if (var_is_fixed_to_zero(j)) { - TRACE("nla_solver_mons", s.print_term_as_indices(*s.terms()[i], tout << "term = ") << "\n";); - add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); + TRACE("nla_solver_mons", s.print_term_as_indices(*t, tout << "term = ") << "\n";); + add_equivalence_maybe(t, s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); } } m_emons.ensure_canonized(); @@ -732,9 +718,9 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar & return false; } if (i == null_lpvar) - i = p.column(); + i = p.j(); else - j = p.column(); + j = p.j(); } SASSERT(j != null_lpvar); sign = (seen_minus && seen_plus)? false : true; @@ -871,7 +857,7 @@ std::unordered_set core::collect_vars(const lemma& l) const { for (const auto& i : l.ineqs()) { for (lp::lar_term::ival p : i.term()) { - insert_j(p.column()); + insert_j(p.j()); } } for (auto p : l.expl()) { @@ -1629,17 +1615,9 @@ lbool core::test_check() { } std::ostream& core::print_terms(std::ostream& out) const { - for (unsigned i = 0; i < lra.terms().size(); i++) { - unsigned ext = lp::tv::mask_term(i); - if (!lra.var_is_registered(ext)) { - out << "term is not registered\n"; - continue; - } - - const lp::lar_term & t = *lra.terms()[i]; - out << "term:"; print_term(t, out) << std::endl; - lpvar j = lra.external_to_local(ext); - print_var(j, out); + for (const auto * t: lra.terms()) { + out << "term:"; print_term(*t, out) << std::endl; + print_var(t->j(), out); } return out; } @@ -1673,12 +1651,12 @@ std::unordered_set core::get_vars_of_expr_with_opening_terms(const nex *e } for (unsigned i = 0; i < added.size(); ++i) { lpvar j = added[i]; - if (ls.column_corresponds_to_term(j)) { - const auto& t = lra.get_term(lp::tv::raw(ls.local_to_external(j))); + if (ls.column_has_term(j)) { + const auto& t = lra.get_term(j); for (auto p : t) { - if (ret.find(p.column()) == ret.end()) { - added.push_back(p.column()); - ret.insert(p.column()); + if (ret.find(p.j()) == ret.end()) { + added.push_back(p.j()); + ret.insert(p.j()); } } } @@ -1729,8 +1707,6 @@ void core::set_active_vars_weights(nex_creator& nc) { } bool core::influences_nl_var(lpvar j) const { - if (lp::tv::is_term(j)) - j = lp::tv::unmask_term(j); if (is_nl_var(j)) return true; for (const auto & c : lra.A_r().m_columns[j]) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 253306bcd5f..eb1f8b4369f 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -135,7 +135,6 @@ class core { rational value(const lp::lar_term& r) const; - lp::lar_term subs_terms_to_columns(const lp::lar_term& t) const; 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); } @@ -284,10 +283,10 @@ class core { } const rational& get_upper_bound(unsigned j) const; const rational& get_lower_bound(unsigned j) const; - bool has_lower_bound(lp::var_index var, u_dependency*& ci, lp::mpq& value, bool& is_strict) const { + bool has_lower_bound(lp::lpvar var, u_dependency*& ci, lp::mpq& value, bool& is_strict) const { return lra.has_lower_bound(var, ci, value, is_strict); } - bool has_upper_bound(lp::var_index var, u_dependency*& ci, lp::mpq& value, bool& is_strict) const { + bool has_upper_bound(lp::lpvar var, u_dependency*& ci, lp::mpq& value, bool& is_strict) const { return lra.has_upper_bound(var, ci, value, is_strict); } diff --git a/src/math/lp/nla_defs.h b/src/math/lp/nla_defs.h index e9807eaeb4f..b576036143d 100644 --- a/src/math/lp/nla_defs.h +++ b/src/math/lp/nla_defs.h @@ -17,7 +17,7 @@ namespace nla { typedef lp::constraint_index lpci; typedef lp::lconstraint_kind llc; typedef lp::explanation expl_set; - typedef lp::var_index lpvar; + typedef unsigned lpvar; struct from_index_dummy{}; class signed_var { @@ -54,12 +54,12 @@ inline std::ostream& operator<<(std::ostream& out, signed_var const& sv) { retur * where m_vs = [v1, v2, .., vn] */ class monic_coeff { - svector m_vs; + svector m_vs; rational m_coeff; public: - monic_coeff(const svector& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {} + monic_coeff(const svector& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {} rational const& coeff() const { return m_coeff; } - const svector & vars() const { return m_vs; } + const svector & vars() const { return m_vs; } }; template bool has_zero(const T& product) { for (const rational & t : product) { diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp index 7d52cd0bab8..6c3bb178c66 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/src/math/lp/nla_divisions.cpp @@ -19,15 +19,9 @@ Module Name: namespace nla { void divisions::add_idivision(lpvar q, lpvar x, lpvar y) { - auto& lra = m_core.lra; + const auto& lra = m_core.lra; if (x == null_lpvar || y == null_lpvar || q == null_lpvar) return; - if (lp::tv::is_term(x)) - x = lra.map_term_index_to_column_index(x); - if (lp::tv::is_term(y)) - y = lra.map_term_index_to_column_index(y); - if (lp::tv::is_term(q)) - q = lra.map_term_index_to_column_index(q); m_idivisions.push_back({q, x, y}); m_core.trail().push(push_back_vector(m_idivisions)); } @@ -36,13 +30,6 @@ namespace nla { auto& lra = m_core.lra; if (x == null_lpvar || y == null_lpvar || q == null_lpvar) return; - if (lp::tv::is_term(x)) - x = lra.map_term_index_to_column_index(x); - if (lp::tv::is_term(y)) - y = lra.map_term_index_to_column_index(y); - if (lp::tv::is_term(q)) - q = lra.map_term_index_to_column_index(q); - m_rdivisions.push_back({ q, x, y }); m_core.trail().push(push_back_vector(m_rdivisions)); } @@ -50,7 +37,7 @@ namespace nla { void divisions::add_bounded_division(lpvar q, lpvar x, lpvar y) { if (x == null_lpvar || y == null_lpvar || q == null_lpvar) return; - if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(q)) + if (m_core.lra.column_has_term(x) || m_core.lra.column_has_term(y) || m_core.lra.column_has_term(q)) return; m_bounded_divisions.push_back({ q, x, y }); m_core.trail().push(push_back_vector(m_bounded_divisions)); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index f9974b41cd6..4beb7eaff7e 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -406,9 +406,8 @@ namespace nla { coeffs.push_back({lc*coeff, m_mon2var.find(vars)->second}); } - lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX); - term_index = c().lra.map_term_index_to_column_index(term_index); - c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, offset, e.dep()); + lp::lpvar j = c().lra.add_term(coeffs, UINT_MAX); + c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, offset, e.dep()); c().m_check_feasible = true; return true; } diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp index f389aad93c7..4e521bb0130 100644 --- a/src/math/lp/nla_powers.cpp +++ b/src/math/lp/nla_powers.cpp @@ -80,12 +80,12 @@ namespace nla { lbool powers::check(lpvar r, lpvar x, lpvar y, vector& lemmas) { TRACE("nla", tout << r << " == " << x << "^" << y << "\n"); + core& c = m_core; if (x == null_lpvar || y == null_lpvar || r == null_lpvar) return l_undef; - if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(r)) + if (c.lra.column_has_term(x) || c.lra.column_has_term(y) || c.lra.column_has_term(r)) return l_undef; - core& c = m_core; if (c.use_nra_model()) return l_undef; diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 23d4016bdb4..f55eec6a6f7 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -83,7 +83,7 @@ namespace nla { nlsat::anum_manager& solver::am() { return m_core->m_nra.am(); } - nlsat::anum const& solver::am_value(lp::var_index v) const { + nlsat::anum const& solver::am_value(lp::lpvar v) const { SASSERT(use_nra_model()); return m_core->m_nra.value(v); } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 1e47362fdf4..53e62b4f074 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -46,7 +46,7 @@ namespace nla { bool use_nra_model() const; core& get_core(); nlsat::anum_manager& am(); - nlsat::anum const& am_value(lp::var_index v) const; + nlsat::anum const& am_value(lp::lpvar v) const; scoped_anum& tmp1(); scoped_anum& tmp2(); vector const& lemmas() const; diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index cb62c5a3003..f0f79665223 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -22,7 +22,7 @@ namespace nla { typedef lp::lconstraint_kind llc; typedef lp::constraint_index lpci; typedef lp::explanation expl_set; - typedef lp::var_index lpvar; + typedef lp::lpvar lpvar; const lpvar null_lpvar = UINT_MAX; diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index e035fc34f5d..9c9db4e4114 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -71,12 +71,11 @@ struct solver::imp { } } - for (unsigned i = lra.terms().size(); i-- > 0; ) { - auto const& t = lra.term(i); - for (auto const iv : t) { - auto v = iv.column().index(); + for (const auto *t : lra.terms() ) { + for (auto const iv : *t) { + auto v = iv.j(); var2occurs.reserve(v + 1); - var2occurs[v].terms.push_back(i); + var2occurs[v].terms.push_back(t->j()); } } @@ -99,17 +98,15 @@ struct solver::imp { todo.push_back(w); for (auto ti : var2occurs[v].terms) { - for (auto iv : lra.term(ti)) - todo.push_back(iv.column().index()); - auto vi = lp::tv::mask_term(ti); - todo.push_back(lra.map_term_index_to_column_index(vi)); + for (auto iv : lra.get_term(ti)) + todo.push_back(iv.j()); + todo.push_back(ti); } - if (lra.column_corresponds_to_term(v)) { + if (lra.column_has_term(v)) { m_term_set.insert(v); - lp::tv ti = lp::tv::raw(lra.column_to_reported_index(v)); - for (auto kv : lra.get_term(ti)) - todo.push_back(kv.column().index()); + for (auto kv : lra.get_term(v)) + todo.push_back(kv.j()); } if (m_nla_core.is_monic_var(v)) { @@ -517,16 +514,16 @@ struct solver::imp { - bool is_int(lp::var_index v) { + bool is_int(lp::lpvar v) { return lra.var_is_int(v); } - polynomial::var lp2nl(lp::var_index v) { + polynomial::var lp2nl(lp::lpvar v) { polynomial::var r; if (!m_lp2nl.find(v, r)) { r = m_nlsat->mk_var(is_int(v)); m_lp2nl.insert(v, r); - if (!m_term_set.contains(v) && lra.column_corresponds_to_term(v)) { + if (!m_term_set.contains(v) && lra.column_has_term(v)) { m_term_set.insert(v); } } @@ -534,14 +531,13 @@ struct solver::imp { } // void add_term(unsigned term_column) { - lp::tv ti = lp::tv::raw(lra.column_to_reported_index(term_column)); - const lp::lar_term& t = lra.get_term(ti); + const lp::lar_term& t = lra.get_term(term_column); // code that creates a polynomial equality between the linear coefficients and // variable representing the term. svector vars; rational den(1); for (lp::lar_term::ival kv : t) { - vars.push_back(lp2nl(kv.column().index())); + vars.push_back(lp2nl(kv.j())); den = lcm(den, denominator(kv.coeff())); } vars.push_back(lp2nl(term_column)); @@ -559,7 +555,7 @@ struct solver::imp { m_nlsat->mk_clause(1, &lit, nullptr); } - nlsat::anum const& value(lp::var_index v) { + nlsat::anum const& value(lp::lpvar v) { polynomial::var pv; if (m_lp2nl.find(v, pv)) return m_nlsat->value(pv); @@ -636,7 +632,7 @@ std::ostream& solver::display(std::ostream& out) const { return m_imp->display(out); } -nlsat::anum const& solver::value(lp::var_index v) { +nlsat::anum const& solver::value(lp::lpvar v) { return m_imp->value(v); } diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h index 747b4cee394..90f022ba6dc 100644 --- a/src/math/lp/nra_solver.h +++ b/src/math/lp/nra_solver.h @@ -55,7 +55,7 @@ namespace nra { /* \brief Access model. */ - nlsat::anum const& value(lp::var_index v); + nlsat::anum const& value(lp::lpvar v); nlsat::anum_manager& am(); diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index ffbd48021cd..9d6bb859964 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -346,14 +346,14 @@ class static_matrix // we use the form -it + 1 = 0 m_work_vector.set_value(one_of_type(), bj); for (auto p : row) { - m_work_vector.set_value(-p.coeff(), p.column().index()); + m_work_vector.set_value(-p.coeff(), p.j()); // but take care of the basis 1 later } // now iterate with pivoting fill_last_row_with_pivoting_loop_block(bj, basis_heading); for (auto p : row) { - fill_last_row_with_pivoting_loop_block(p.column().index(), basis_heading); + fill_last_row_with_pivoting_loop_block(p.j(), basis_heading); } unsigned last_row = row_count() - 1; diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 3b326788ba7..bd7e6efe830 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -41,10 +41,7 @@ class ext_var_info { class var_register { vector m_local_to_external; std::unordered_map m_external_to_local; - unsigned m_locals_mask; - unsigned m_locals_mask_inverted; public: - var_register(bool mask_locals): m_locals_mask(mask_locals? tv::left_most_bit: 0), m_locals_mask_inverted(~m_locals_mask) {} void set_name(unsigned j, std::string name) { m_local_to_external[j].set_name(name); @@ -63,7 +60,7 @@ class var_register { } m_local_to_external.push_back(ext_var_info(user_var, is_int)); - unsigned local = ( size() - 1 ) | m_locals_mask; + unsigned local = size() - 1; if (user_var != UINT_MAX) m_external_to_local[user_var] = local; @@ -79,7 +76,7 @@ class var_register { // returns UINT_MAX if unsigned local_to_external(unsigned local_var) const { - unsigned k = local_var & m_locals_mask_inverted; + unsigned k = local_var; if (k >= m_local_to_external.size()) return UINT_MAX; return m_local_to_external[k].external_j(); @@ -119,7 +116,7 @@ class var_register { local_j = UINT_MAX; return false; } - local_j = it->second & m_locals_mask_inverted; + local_j = it->second; is_int = m_local_to_external[local_j].is_integer(); return true; } @@ -129,7 +126,7 @@ class var_register { } bool local_is_int(unsigned j) const { - return m_local_to_external[j & m_locals_mask_inverted].is_integer(); + return m_local_to_external[j].is_integer(); } void shrink(unsigned shrunk_size) { diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 32e64e2b5d7..c408fbf96bc 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -45,8 +45,7 @@ namespace arith { } unsigned nv = get_num_vars(); for (unsigned v = 0; v < nv; ++v) { - auto t = get_tv(v); - auto vi = lp().external_to_column_index(v); + auto vi = lp().external_to_local(v); out << "v" << v << " "; if (is_bool(v)) { euf::enode* n = var2enode(v); @@ -57,10 +56,10 @@ namespace arith { } } else { - if (t.is_null()) + if (vi == lp::null_lpvar) out << "null"; else - out << (t.is_term() ? "t" : "j") << vi; + out << (lp().column_has_term(vi) ? "t" : "j") << vi; if (m_nla && m_nla->use_nra_model() && is_registered_var(v)) { scoped_anum an(m_nla->am()); m_nla->am().display(out << " = ", nl_value(v, an)); diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 00038cf8bdd..a389d13b889 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -507,11 +507,11 @@ namespace arith { } else { vi = lp().add_term(m_left_side, v); - SASSERT(lp::tv::is_term(vi)); + SASSERT(lp().column_has_term(vi)); TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; - lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";); + lp().print_term(lp().get_term(vi), tout) << "\n";); } } return v; @@ -541,8 +541,6 @@ namespace arith { rational const& r = m_columns[var]; if (!r.is_zero()) { auto vi = register_theory_var_in_lar_solver(var); - if (lp::tv::is_term(vi)) - vi = lp().map_term_index_to_column_index(vi); m_left_side.push_back(std::make_pair(r, vi)); m_columns[var].reset(); } @@ -625,9 +623,6 @@ namespace arith { return lp().external_to_local(v); } - lp::tv solver::get_tv(theory_var v) const { - return lp::tv::raw(get_lpvar(v)); - } /** \brief We must redefine this method, because theory of arithmetic contains diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp index 4fe153289de..2168299803b 100644 --- a/src/sat/smt/arith_sls.cpp +++ b/src/sat/smt/arith_sls.cpp @@ -59,18 +59,10 @@ namespace arith { int64_t val = 0; lp::lar_term const& term = s.lp().get_term(t); for (lp::lar_term::ival const& arg : term) { - auto t2 = s.lp().column2tv(arg.column()); - auto w = s.lp().local_to_external(t2.id()); + auto t2 = arg.j(); + auto w = s.lp().local_to_external(t2); val += to_numeral(arg.coeff()) * m_vars[w].m_best_value; } - if (v == 52) { - verbose_stream() << "update v" << v << " := " << val << "\n"; - for (lp::lar_term::ival const& arg : term) { - auto t2 = s.lp().column2tv(arg.column()); - auto w = s.lp().local_to_external(t2.id()); - verbose_stream() << "v" << w << " := " << m_vars[w].m_best_value << " * " << to_numeral(arg.coeff()) << "\n"; - } - } m_vars[v].m_best_value = val; } @@ -81,12 +73,12 @@ namespace arith { continue; int64_t new_value = m_vars[v].m_best_value; s.ensure_column(v); - lp::column_index vj = s.lp().to_column_index(v); - SASSERT(!vj.is_null()); - if (!s.lp().is_base(vj.index())) { + lp::lpvar vj = s.lp().external_to_local(v); + SASSERT(vj != lp::null_lpvar); + if (!s.lp().is_base(vj)) { rational new_value_(new_value, rational::i64()); lp::impq val(new_value_, rational::zero()); - s.lp().set_value_for_nbasic_column(vj.index(), val); + s.lp().set_value_for_nbasic_column(vj, val); } } @@ -460,18 +452,18 @@ namespace arith { return 0; } - void sls::add_args(sat::bool_var bv, ineq& ineq, lp::tv t, theory_var v, int64_t sign) { - if (t.is_term()) { + void sls::add_args(sat::bool_var bv, ineq& ineq, lp::lpvar t, theory_var v, int64_t sign) { + if (s.lp().column_has_term(t)) { lp::lar_term const& term = s.lp().get_term(t); m_terms.push_back({t,v}); for (lp::lar_term::ival arg : term) { - auto t2 = s.lp().column2tv(arg.column()); - auto w = s.lp().local_to_external(t2.id()); + auto t2 = arg.j(); + auto w = s.lp().local_to_external(t2); add_arg(bv, ineq, sign * to_numeral(arg.coeff()), w); } } else - add_arg(bv, ineq, sign, s.lp().local_to_external(t.id())); + add_arg(bv, ineq, sign, s.lp().local_to_external(t)); } void sls::init_bool_var(sat::bool_var bv) { @@ -480,7 +472,7 @@ namespace arith { api_bound* b = nullptr; s.m_bool_var2bound.find(bv, b); if (b) { - auto t = b->tv(); + auto t = b->column_index(); rational bound = b->get_value(); bool should_minus = false; sls::ineq_kind op; @@ -503,8 +495,8 @@ namespace arith { if (e && m.is_eq(e, l, r) && s.a.is_int_real(l)) { theory_var u = s.get_th_var(l); theory_var v = s.get_th_var(r); - lp::tv tu = s.get_tv(u); - lp::tv tv = s.get_tv(v); + lp::lpvar tu = s.get_column(u); + lp::lpvar tv = s.get_column(v); auto& ineq = new_ineq(sls::ineq_kind::EQ, 0); add_args(bv, ineq, tu, u, 1); add_args(bv, ineq, tv, v, -1); diff --git a/src/sat/smt/arith_sls.h b/src/sat/smt/arith_sls.h index 09a56c84efd..55d39b25205 100644 --- a/src/sat/smt/arith_sls.h +++ b/src/sat/smt/arith_sls.h @@ -105,7 +105,7 @@ namespace arith { config m_config; scoped_ptr_vector m_bool_vars; vector m_vars; - svector> m_terms; + svector> m_terms; bool m_dscore_mode = false; @@ -140,7 +140,7 @@ namespace arith { void add_vars(); sls::ineq& new_ineq(ineq_kind op, int64_t const& bound); void add_arg(sat::bool_var bv, ineq& ineq, int64_t const& c, var_t v); - void add_args(sat::bool_var bv, ineq& ineq, lp::tv t, euf::theory_var v, int64_t sign); + void add_args(sat::bool_var bv, ineq& ineq, lp::lpvar j, euf::theory_var v, int64_t sign); void init_bool_var(sat::bool_var v); void init_bool_var_assignment(sat::bool_var v); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index b2a466779b1..3086d75f43f 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -370,7 +370,7 @@ namespace arith { void solver::refine_bound(theory_var v, const lp::implied_bound& be) { lpvar vi = be.m_j; - if (lp::tv::is_term(vi)) + if (lp().column_has_term(vi)) return; expr_ref w(var2expr(v), m); if (a.is_add(w) || a.is_numeral(w) || m.is_ite(w)) @@ -418,7 +418,7 @@ namespace arith { ++m_stats.m_assert_upper; inf_rational value = b.get_value(is_true); if (propagate_eqs() && value.is_rational()) - propagate_eqs(b.tv(), ci, k, b, value.get_rational()); + propagate_eqs(b.column_index(), ci, k, b, value.get_rational()); #if 0 if (propagation_mode() != BP_NONE) lp().add_column_rows_to_touched_rows(b.tv().id()); @@ -426,30 +426,29 @@ namespace arith { } - void solver::propagate_eqs(lp::tv t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) { + void solver::propagate_eqs(lp::lpvar t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) { u_dependency* dep; auto& dm = lp().dep_manager(); - if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), dep, value)) { + if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t, dep, value)) { fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value); } - else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), dep, value)) { + else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t, dep, value)) { fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value); } } - bool solver::set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower) { - if (tv.is_term()) { - lpvar ti = tv.id(); + bool solver::set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower) { + if (lp().column_has_term(tv)) { auto& vec = is_lower ? m_lower_terms : m_upper_terms; - if (vec.size() <= ti) { - vec.resize(ti + 1, constraint_bound(UINT_MAX, rational())); + if (vec.size() <= tv) { + vec.resize(tv + 1, constraint_bound(UINT_MAX, rational())); } - constraint_bound& b = vec[ti]; + constraint_bound& b = vec[tv]; if (b.first == UINT_MAX || (is_lower ? b.second < v : b.second > v)) { - TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";); - m_history.push_back(vec[ti]); - ctx.push(history_trail(vec, ti, m_history)); + TRACE("arith", tout << "tighter bound " << tv << "\n";); + m_history.push_back(vec[tv]); + ctx.push(history_trail(vec, tv, m_history)); b.first = ci; b.second = v; } @@ -461,10 +460,10 @@ namespace arith { rational b; u_dependency* dep = nullptr; if (is_lower) { - return lp().has_lower_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v; + return lp().has_lower_bound(tv, dep, b, is_strict) && !is_strict && b == v; } else { - return lp().has_upper_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v; + return lp().has_upper_bound(tv, dep, b, is_strict) && !is_strict && b == v; } } } @@ -772,7 +771,7 @@ namespace arith { bool solver::has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, true); } bool solver::has_bound(lpvar vi, u_dependency*& dep, rational const& bound, bool is_lower) { - if (lp::tv::is_term(vi)) { + if (lp().column_has_term(vi)) { theory_var v = lp().local_to_external(vi); rational val; TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";); @@ -782,9 +781,8 @@ namespace arith { } auto& vec = is_lower ? m_lower_terms : m_upper_terms; - lpvar ti = lp::tv::unmask_term(vi); - if (vec.size() > ti) { - auto& [ci, coeff] = vec[ti]; + if (vec.size() > vi) { + auto& [ci, coeff] = vec[vi]; if (ci == UINT_MAX) return false; dep = lp().dep_manager().mk_leaf(ci); @@ -876,11 +874,16 @@ namespace arith { lp::impq solver::get_ivalue(theory_var v) const { SASSERT(is_registered_var(v)); - return m_solver->get_tv_ivalue(get_tv(v)); + return m_solver->get_column_value(get_column(v)); } + lp::lpvar solver::get_column(theory_var v) const { + SASSERT(is_registered_var(v)); + return m_solver->external_to_local(v); + } + rational solver::get_value(theory_var v) const { - return is_registered_var(v) ? m_solver->get_tv_value(get_tv(v)) : rational::zero(); + return is_registered_var(v) ? m_solver->get_value(get_column(v)) : rational::zero(); } void solver::random_update() { @@ -895,18 +898,18 @@ namespace arith { if (is_bool(v)) continue; ensure_column(v); - lp::column_index vj = lp().to_column_index(v); - SASSERT(!vj.is_null()); + lp::lpvar vj = lp().external_to_local(v); + SASSERT(vj != lp::null_lpvar); theory_var other = m_model_eqs.insert_if_not_there(v); if (is_equal(v, other)) continue; - if (!lp().is_fixed(vj)) - vars.push_back(vj.index()); + if (!lp().column_is_fixed(vj)) + vars.push_back(vj); else if (!m_tmp_var_set.contains(other)) { - lp::column_index other_j = lp().to_column_index(other); - if (!lp().is_fixed(other_j)) { + lp::lpvar other_j = lp().external_to_local(other); + if (!lp().column_is_fixed(other_j)) { m_tmp_var_set.insert(other); - vars.push_back(other_j.index()); + vars.push_back(other_j); } } } @@ -1068,14 +1071,14 @@ namespace arith { nlsat::anum const& solver::nl_value(theory_var v, scoped_anum& r) const { SASSERT(m_nla); SASSERT(m_nla->use_nra_model()); - auto t = get_tv(v); - if (!t.is_term()) { - m_nla->am().set(r, m_nla->am_value(t.id())); + auto t = get_column(v); + if (!lp().column_has_term(t)) { + m_nla->am().set(r, m_nla->am_value(t)); } else { m_todo_terms.push_back(std::make_pair(t, rational::one())); - TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";); - TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; + TRACE("nl_value", tout << "v" << v << " " << t << "\n";); + TRACE("nl_value", tout << "v" << v << " := w" << t << "\n"; lp().print_term(lp().get_term(t), tout) << "\n";); m_nla->am().set(r, 0); @@ -1090,14 +1093,14 @@ namespace arith { m_nla->am().set(r1, c1.to_mpq()); m_nla->am().add(r, r1, r); for (lp::lar_term::ival arg : term) { - auto wi = lp().column2tv(arg.column()); + auto wi = arg.j(); c1 = arg.coeff() * wcoeff; - if (wi.is_term()) { + if (lp().column_has_term(wi)) { m_todo_terms.push_back(std::make_pair(wi, c1)); } else { m_nla->am().set(r1, c1.to_mpq()); - m_nla->am().mul(m_nla->am_value(wi.id()), r1, r1); + m_nla->am().mul(m_nla->am_value(wi), r1, r1); m_nla->am().add(r1, r, r); } } @@ -1393,17 +1396,17 @@ namespace arith { TRACE("arith", lp().print_term(term, tout) << "\n";); for (lp::lar_term::ival ti : term) { theory_var w; - auto tv = lp().column2tv(ti.column()); - if (tv.is_term()) { + auto tv = ti.j(); + if (lp().column_has_term(tv)) { lp::lar_term const& term1 = lp().get_term(tv); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2); continue; } else { - w = lp().local_to_external(tv.id()); + w = lp().local_to_external(tv); SASSERT(w >= 0); - TRACE("arith", tout << (tv.id()) << ": " << w << "\n";); + TRACE("arith", tout << tv << ": " << w << "\n";); } rational c0(0); coeffs.find(w, c0); diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index af9df0798fc..755611474bd 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -38,7 +38,7 @@ namespace euf { namespace arith { typedef ptr_vector> lp_bounds; - typedef lp::var_index lpvar; + typedef lp::lpvar lpvar; typedef euf::theory_var theory_var; typedef euf::theory_id theory_id; typedef euf::enode enode; @@ -245,7 +245,7 @@ namespace arith { symbol m_farkas; std_vector m_implied_bounds; lp::lp_bound_propagator m_bp; - mutable vector> m_todo_terms; + mutable vector> m_todo_terms; // lemmas lp::explanation m_explanation; @@ -306,7 +306,7 @@ namespace arith { bool reflect(expr* n) const; lpvar get_lpvar(theory_var v) const; - lp::tv get_tv(theory_var v) const; + lp::lpvar get_column(theory_var v) const; // axioms void mk_div_axiom(expr* p, expr* q); @@ -348,7 +348,7 @@ namespace arith { iterator end, bool& found_compatible); - void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value); + void propagate_eqs(lp::lpvar t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value); void propagate_basic_bounds(unsigned qhead); void propagate_bounds_with_lp_solver(); void propagate_bound(literal lit, api_bound& b); @@ -362,9 +362,9 @@ namespace arith { api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound); lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true); void fixed_var_eh(theory_var v1, u_dependency* dep, rational const& bound); - bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } - bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); } - bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower); + bool set_upper_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } + bool set_lower_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); } + bool set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower); typedef std::pair constraint_bound; vector m_lower_terms; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4c9e02738ef..f0a96ddd1ba 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -47,7 +47,7 @@ #include "util/scoped_timer.h" #include "util/distribution.h" -typedef lp::var_index lpvar; +typedef lp::lpvar lpvar; namespace smt { @@ -790,10 +790,6 @@ class theory_lra::imp { return v == null_theory_var ? lp::null_lpvar : lp().external_to_local(v); } - lp::tv get_tv(theory_var v) const { - return lp::tv::raw(get_lpvar(v)); - } - theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) { theory_var v = mk_var(term); TRACE("arith_internalize", tout << "v" << v << " " << bpp(term) << "\n";); @@ -812,11 +808,11 @@ class theory_lra::imp { } else { vi = lp().add_term(m_left_side, v); - SASSERT(lp::tv::is_term(vi)); + SASSERT(lp().column_has_term(vi)); TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; - lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";); + lp().print_term(lp().get_term(vi), tout) << "\n";); } } @@ -1432,15 +1428,15 @@ class theory_lra::imp { register_theory_var_in_lar_solver(v); } - mutable vector> m_todo_terms; - + mutable vector> m_todo_terms; + lp::impq get_ivalue(theory_var v) const { SASSERT(is_registered_var(v)); - return lp().get_tv_ivalue(get_tv(v)); + return lp().get_column_value(get_lpvar(v)); } rational get_value(theory_var v) const { - return is_registered_var(v) ? lp().get_tv_value(get_tv(v)) : rational::zero(); + return is_registered_var(v) ? lp().get_value(get_lpvar(v)) : rational::zero(); } bool m_model_is_initialized{ false }; @@ -1467,8 +1463,8 @@ class theory_lra::imp { continue; } ensure_column(v); - lp::column_index vj = lp().to_column_index(v); - SASSERT(!vj.is_null()); + lp::lpvar vj = lp().external_to_local(v); + SASSERT(vj != lp::null_lpvar); theory_var other = m_model_eqs.insert_if_not_there(v); if (other == v) { continue; @@ -1476,14 +1472,14 @@ class theory_lra::imp { enode * n2 = get_enode(other); if (n1->get_root() == n2->get_root()) continue; - if (!lp().is_fixed(vj)) { - vars.push_back(vj.index()); + if (!lp().column_is_fixed(vj)) { + vars.push_back(vj); } else if (!m_tmp_var_set.contains(other) ) { - lp::column_index other_j = lp().to_column_index(other); - if (!lp().is_fixed(other_j)) { + lp::lpvar other_j = lp().external_to_local(other); + if (!lp().column_is_fixed(other_j)) { m_tmp_var_set.insert(other); - vars.push_back(other_j.index()); + vars.push_back(other_j); } } } @@ -1794,12 +1790,12 @@ class theory_lra::imp { expr_ref t(m); expr_ref_vector ts(m); for (lp::lar_term::ival p : term) { - auto ti = lp().column2tv(p.column()); - if (ti.is_term()) { + auto ti = p.j(); + if (lp().column_has_term(ti)) { ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(ti)))); } else { - ts.push_back(multerm(p.coeff(), var2expr(ti.id()))); + ts.push_back(multerm(p.coeff(), var2expr(ti))); } } if (ts.size() == 1) { @@ -1836,13 +1832,13 @@ class theory_lra::imp { lp().print_term(term, out << "bound: "); out << (upper?" <= ":" >= ") << k << "\n"; for (lp::lar_term::ival p : term) { - auto ti = lp().column2tv(p.column()); + auto ti = p.j(); out << p.coeff() << " * "; - if (ti.is_term()) { + if (lp().column_has_term(ti)) { lp().print_term(lp().get_term(ti), out) << "\n"; } else { - out << "v" << lp().local_to_external(ti.id()) << "\n"; + out << "v" << lp().local_to_external(ti) << "\n"; } } for (auto ev : ex) { @@ -2324,7 +2320,7 @@ class theory_lra::imp { void refine_bound(theory_var v, const lp::implied_bound& be) { lpvar vi = be.m_j; - if (lp::tv::is_term(vi)) + if (lp().column_has_term(vi)) return; expr_ref w(get_enode(v)->get_expr(), m); if (a.is_add(w) || a.is_numeral(w) || m.is_ite(w)) @@ -2747,27 +2743,27 @@ class theory_lra::imp { ++m_stats.m_bounds_propagations; } - svector m_todo_vars; + svector m_todo_vars; void add_use_lists(api_bound* b) { theory_var v = b->get_var(); lpvar vi = register_theory_var_in_lar_solver(v); - if (!lp::tv::is_term(vi)) { + if (!lp().column_has_term(vi)) { return; } - m_todo_vars.push_back(lp::tv::raw(vi)); + m_todo_vars.push_back(vi); while (!m_todo_vars.empty()) { auto ti = m_todo_vars.back(); - SASSERT(ti.is_term()); + SASSERT(lp().column_has_term(ti)); m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(ti); for (auto p : term) { - lp::tv wi = lp().column2tv(p.column()); - if (wi.is_term()) { + lp::lpvar wi = p.j(); + if (lp().column_has_term(wi)) { m_todo_vars.push_back(wi); } else { - unsigned w = lp().local_to_external(wi.id()); + unsigned w = lp().local_to_external(wi); m_use_list.reserve(w + 1, ptr_vector()); m_use_list[w].push_back(b); } @@ -2778,22 +2774,22 @@ class theory_lra::imp { void del_use_lists(api_bound* b) { theory_var v = b->get_var(); lpvar vi = get_lpvar(v); - if (!lp::tv::is_term(vi)) { + if (!lp().column_has_term(vi)) { return; } - m_todo_vars.push_back(lp::tv::raw(vi)); + m_todo_vars.push_back(vi); while (!m_todo_vars.empty()) { auto ti = m_todo_vars.back(); - SASSERT(ti.is_term()); + SASSERT(lp().column_has_term(ti)); m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(ti); for (auto coeff : term) { - auto wi = lp().column2tv(coeff.column()); - if (wi.is_term()) { + auto wi = coeff.j(); + if (lp().column_has_term(wi)) { m_todo_vars.push_back(wi); } else { - unsigned w = lp().local_to_external(wi.id()); + unsigned w = lp().local_to_external(wi); SASSERT(m_use_list[w].back() == b); m_use_list[w].pop_back(); } @@ -2872,20 +2868,20 @@ class theory_lra::imp { reset_evidence(); r.reset(); theory_var v = b.get_var(); - auto ti = get_tv(v); - SASSERT(ti.is_term()); + lp::lpvar ti = get_lpvar(v); + SASSERT(lp().column_has_term(ti)); lp::lar_term const& term = lp().get_term(ti); for (auto const mono : term) { - auto wi = lp().column2tv(mono.column()); + auto wi = mono.j(); u_dependency* ci = nullptr; rational value; bool is_strict; - if (wi.is_term()) { + if (lp().column_has_term(wi)) { return false; } if (mono.coeff().is_neg() == is_lub) { // -3*x ... <= lub based on lower bound for x. - if (!lp().has_lower_bound(wi.id(), ci, value, is_strict)) { + if (!lp().has_lower_bound(wi, ci, value, is_strict)) { return false; } if (is_strict) { @@ -2893,7 +2889,7 @@ class theory_lra::imp { } } else { - if (!lp().has_upper_bound(wi.id(), ci, value, is_strict)) { + if (!lp().has_upper_bound(wi, ci, value, is_strict)) { return false; } if (is_strict) { @@ -2933,7 +2929,7 @@ class theory_lra::imp { } inf_rational value = b.get_value(is_true); if (propagate_eqs() && value.is_rational()) - propagate_eqs(b.tv(), ci, k, b, value.get_rational()); + propagate_eqs(b.column_index(), ci, k, b, value.get_rational()); return true; #if 0 if (should_propagate()) @@ -2978,13 +2974,13 @@ class theory_lra::imp { vector m_lower_terms; vector m_upper_terms; - void propagate_eqs(lp::tv t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) { + void propagate_eqs(lp::lpvar t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) { u_dependency* ci2 = nullptr; auto pair = [&]() { return lp().dep_manager().mk_join(lp().dep_manager().mk_leaf(ci1), ci2); }; - if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), ci2, value)) { + if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t, ci2, value)) { fixed_var_eh(b.get_var(), t, pair(), value); } - else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), ci2, value)) { + else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t, ci2, value)) { fixed_var_eh(b.get_var(), t, pair(), value); } } @@ -2998,24 +2994,23 @@ class theory_lra::imp { bool proofs_enabled() const { return m.proofs_enabled(); } - bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } + bool set_upper_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } - bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); } + bool set_lower_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); } vector m_history; - bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower) { - if (tv.is_term()) { - lpvar ti = tv.id(); + bool set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower) { + if (lp().column_has_term(tv)) { auto& vec = is_lower ? m_lower_terms : m_upper_terms; - if (vec.size() <= ti) { - vec.resize(ti + 1, constraint_bound(UINT_MAX, rational())); + if (vec.size() <= tv) { + vec.resize(tv + 1, constraint_bound(UINT_MAX, rational())); } - constraint_bound& b = vec[ti]; + constraint_bound& b = vec[tv]; if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) { - TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";); - m_history.push_back(vec[ti]); - ctx().push_trail(history_trail(vec, ti, m_history)); + TRACE("arith", tout << "tighter bound " << tv << "\n";); + m_history.push_back(vec[tv]); + ctx().push_trail(history_trail(vec, tv, m_history)); b.first = ci; b.second = v; } @@ -3027,10 +3022,10 @@ class theory_lra::imp { rational b; u_dependency* dep = nullptr; if (is_lower) { - return lp().has_lower_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v; + return lp().has_lower_bound(tv, dep, b, is_strict) && !is_strict && b == v; } else { - return lp().has_upper_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v; + return lp().has_upper_bound(tv, dep, b, is_strict) && !is_strict && b == v; } } } @@ -3052,7 +3047,7 @@ class theory_lra::imp { bool has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, true); } bool has_bound(lpvar vi, u_dependency*& dep, rational const& bound, bool is_lower) { - if (lp::tv::is_term(vi)) { + if (lp().column_has_term(vi)) { theory_var v = lp().local_to_external(vi); rational val; TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";); @@ -3062,9 +3057,8 @@ class theory_lra::imp { } auto& vec = is_lower ? m_lower_terms : m_upper_terms; - lpvar ti = lp::tv::unmask_term(vi); - if (vec.size() > ti) { - auto const& [ci, coeff] = vec[ti]; + if (vec.size() > vi) { + auto const& [ci, coeff] = vec[vi]; if (ci == UINT_MAX) return false; dep = lp().dep_manager().mk_leaf(ci); @@ -3145,7 +3139,7 @@ class theory_lra::imp { ctx().assign_eq(x, y, eq_justification(js)); } - void fixed_var_eh(theory_var v, lp::tv t, u_dependency* dep, rational const& bound) { + void fixed_var_eh(theory_var v, lp::lpvar t, u_dependency* dep, rational const& bound) { theory_var w = null_theory_var; enode* x = get_enode(v); if (m_value2var.find(bound, w)) @@ -3314,14 +3308,14 @@ class theory_lra::imp { nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const { SASSERT(use_nra_model()); - auto t = get_tv(v); - if (!t.is_term()) - m_nla->am().set(r, m_nla->am_value(t.id())); + auto t = get_lpvar(v); + if (!lp().column_has_term(t)) + m_nla->am().set(r, m_nla->am_value(t)); else { m_todo_terms.push_back({t, rational::one()}); - TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";); - TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; + TRACE("nl_value", tout << "v" << v << " " << t << "\n";); + TRACE("nl_value", tout << "v" << v << " := w" << t << "\n"; lp().print_term(lp().get_term(t), tout) << "\n";); m_nla->am().set(r, 0); @@ -3336,14 +3330,14 @@ class theory_lra::imp { m_nla->am().set(r1, c1.to_mpq()); m_nla->am().add(r, r1, r); for (lp::lar_term::ival arg : term) { - auto wi = lp().column2tv(arg.column()); + auto wi = arg.j(); c1 = arg.coeff() * wcoeff; - if (wi.is_term()) { + if (lp().column_has_term(wi)) { m_todo_terms.push_back({wi, c1}); } else { m_nla->am().set(r1, c1.to_mpq()); - m_nla->am().mul(m_nla->am_value(wi.id()), r1, r1); + m_nla->am().mul(m_nla->am_value(wi), r1, r1); m_nla->am().add(r1, r, r); } } @@ -3619,17 +3613,17 @@ class theory_lra::imp { TRACE("arith", lp().print_term(term, tout) << "\n";); for (lp::lar_term::ival ti : term) { theory_var w; - auto tv = lp().column2tv(ti.column()); - if (tv.is_term()) { + auto tv = ti.j(); + if (lp().column_has_term(tv)) { lp::lar_term const& term1 = lp().get_term(tv); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2); continue; } else { - w = lp().local_to_external(tv.id()); + w = lp().local_to_external(tv); SASSERT(w >= 0); - TRACE("arith", tout << (tv.id()) << ": " << w << "\n";); + TRACE("arith", tout << tv << ": " << w << "\n";); } rational c0(0); coeffs.find(w, c0); @@ -3686,9 +3680,9 @@ class theory_lra::imp { } app_ref mk_obj(theory_var v) { - auto t = get_tv(v); + auto t = get_lpvar(v); bool is_int = a.is_int(get_enode(v)->get_expr()); - if (t.is_term()) { + if (lp().column_has_term(t)) { return mk_term(lp().get_term(t), is_int); } else { @@ -3744,11 +3738,10 @@ class theory_lra::imp { } unsigned nv = th.get_num_vars(); for (unsigned v = 0; v < nv; ++v) { - auto t = get_tv(v); - auto vi = lp().external_to_column_index(v); + auto vi = get_lpvar(v); if (!ctx().is_relevant(get_enode(v))) out << "irr: "; out << "v" << v << " "; - if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << vi; + if (vi == lp::null_lpvar) out << "null"; else out << (lp().column_has_term(vi) ? "t":"j") << vi; if (use_nra_model() && is_registered_var(v)) m_nla->am().display(out << " = ", nl_value(v, m_nla->tmp1())); else if (can_get_value(v)) out << " = " << get_value(v); if (is_int(v)) out << ", int"; diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index c64c0103653..9ac675d1a35 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -189,7 +189,7 @@ struct gomory_test { void print_term(lar_term & t, std::ostream & out) { vector> row; for (auto p : t) - row.push_back(std::make_pair(p.coeff(), p.column().index())); + row.push_back(std::make_pair(p.coeff(), p.j())); print_row(out, row); } diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 088a7dac0a7..84077b98e20 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -786,25 +786,25 @@ void test_term() { lar_solver solver; unsigned _x = 0; unsigned _y = 1; - var_index x = solver.add_named_var(_x, true, "x"); - var_index y = solver.add_named_var(_y, true, "y"); + lpvar x = solver.add_named_var(_x, true, "x"); + lpvar y = solver.add_named_var(_y, true, "y"); enable_trace("lar_solver"); enable_trace("cube"); - vector> pairs; - pairs.push_back(std::pair(mpq(2), x)); - pairs.push_back(std::pair(mpq(1), y)); + vector> pairs; + pairs.push_back(std::pair(mpq(2), x)); + pairs.push_back(std::pair(mpq(1), y)); int ti = 0; unsigned x_plus_y = solver.add_term(pairs, ti++); solver.add_var_bound(x_plus_y, lconstraint_kind::GE, mpq(5, 3)); solver.add_var_bound(x_plus_y, lconstraint_kind::LE, mpq(14, 3)); pairs.pop_back(); - pairs.push_back(std::pair(mpq(-1), y)); + pairs.push_back(std::pair(mpq(-1), y)); unsigned x_minus_y = solver.add_term(pairs, ti++); solver.add_var_bound(x_minus_y, lconstraint_kind::GE, mpq(5, 3)); solver.add_var_bound(x_minus_y, lconstraint_kind::LE, mpq(14, 3)); auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; - std::unordered_map model; + std::unordered_map model; if (status != lp_status::OPTIMAL) { std::cout << "non optimal" << std::endl; return; @@ -834,24 +834,24 @@ void test_term() { void test_evidence_for_total_inf_simple(argument_parser &args_parser) { lar_solver solver; - var_index x = solver.add_var(0, false); - var_index y = solver.add_var(1, false); + lpvar x = solver.add_var(0, false); + lpvar y = solver.add_var(1, false); solver.add_var_bound(x, LE, mpq(-1)); solver.add_var_bound(y, GE, mpq(0)); - vector> ls; + vector> ls; - ls.push_back(std::pair(mpq(1), x)); - ls.push_back(std::pair(mpq(1), y)); + ls.push_back(std::pair(mpq(1), x)); + ls.push_back(std::pair(mpq(1), y)); unsigned j = solver.add_term(ls, 1); solver.add_var_bound(j, GE, mpq(1)); ls.pop_back(); - ls.push_back(std::pair(-mpq(1), y)); + ls.push_back(std::pair(-mpq(1), y)); j = solver.add_term(ls, 2); solver.add_var_bound(j, GE, mpq(0)); auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; - std::unordered_map model; + std::unordered_map model; lp_assert(solver.get_status() == lp_status::INFEASIBLE); } void test_bound_propagation_one_small_sample1() { @@ -873,20 +873,20 @@ void test_bound_propagation_one_small_sample1() { unsigned a = ls.add_var(0, false); unsigned b = ls.add_var(1, false); unsigned c = ls.add_var(2, false); - vector> coeffs; - coeffs.push_back(std::pair(mpq(1), a)); - coeffs.push_back(std::pair(mpq(-1), c)); + vector> coeffs; + coeffs.push_back(std::pair(mpq(1), a)); + coeffs.push_back(std::pair(mpq(-1), c)); ls.add_term(coeffs, -1); coeffs.pop_back(); - coeffs.push_back(std::pair(mpq(-1), b)); + coeffs.push_back(std::pair(mpq(-1), b)); ls.add_term(coeffs, -1); coeffs.clear(); - coeffs.push_back(std::pair(mpq(1), a)); - coeffs.push_back(std::pair(mpq(-1), b)); + coeffs.push_back(std::pair(mpq(1), a)); + coeffs.push_back(std::pair(mpq(-1), b)); // ls.add_constraint(coeffs, LE, zero_of_type()); // coeffs.clear(); - // coeffs.push_back(std::pair(mpq(1), b)); - // coeffs.push_back(std::pair(mpq(-1), c)); + // coeffs.push_back(std::pair(mpq(1), b)); + // coeffs.push_back(std::pair(mpq(-1), c)); // ls.add_constraint(coeffs, LE, zero_of_type()); // vector ev; // ls.add_var_bound(a, LE, mpq(1)); @@ -942,9 +942,9 @@ void test_bound_propagation_one_row() { lar_solver ls; unsigned x0 = ls.add_var(0, false); unsigned x1 = ls.add_var(1, false); - vector> c; - c.push_back(std::pair(mpq(1), x0)); - c.push_back(std::pair(mpq(-1), x1)); + vector> c; + c.push_back(std::pair(mpq(1), x0)); + c.push_back(std::pair(mpq(-1), x1)); // todo : restore test // ls.add_constraint(c, EQ, one_of_type()); // vector ev; @@ -957,9 +957,9 @@ void test_bound_propagation_one_row_with_bounded_vars() { lar_solver ls; unsigned x0 = ls.add_var(0, false); unsigned x1 = ls.add_var(1, false); - vector> c; - c.push_back(std::pair(mpq(1), x0)); - c.push_back(std::pair(mpq(-1), x1)); + vector> c; + c.push_back(std::pair(mpq(1), x0)); + c.push_back(std::pair(mpq(-1), x1)); // todo: restore test // ls.add_constraint(c, EQ, one_of_type()); // vector ev; @@ -974,9 +974,9 @@ void test_bound_propagation_one_row_mixed() { lar_solver ls; unsigned x0 = ls.add_var(0, false); unsigned x1 = ls.add_var(1, false); - vector> c; - c.push_back(std::pair(mpq(1), x0)); - c.push_back(std::pair(mpq(-1), x1)); + vector> c; + c.push_back(std::pair(mpq(1), x0)); + c.push_back(std::pair(mpq(-1), x1)); // todo: restore test // ls.add_constraint(c, EQ, one_of_type()); // vector ev; @@ -991,16 +991,16 @@ void test_bound_propagation_two_rows() { unsigned x = ls.add_var(0, false); unsigned y = ls.add_var(1, false); unsigned z = ls.add_var(2, false); - vector> c; - c.push_back(std::pair(mpq(1), x)); - c.push_back(std::pair(mpq(2), y)); - c.push_back(std::pair(mpq(3), z)); + vector> c; + c.push_back(std::pair(mpq(1), x)); + c.push_back(std::pair(mpq(2), y)); + c.push_back(std::pair(mpq(3), z)); // todo: restore test // ls.add_constraint(c, GE, one_of_type()); // c.clear(); - // c.push_back(std::pair(mpq(3), x)); - // c.push_back(std::pair(mpq(2), y)); - // c.push_back(std::pair(mpq(y), z)); + // c.push_back(std::pair(mpq(3), x)); + // c.push_back(std::pair(mpq(2), y)); + // c.push_back(std::pair(mpq(y), z)); // ls.add_constraint(c, GE, one_of_type()); // ls.add_var_bound(x, LE, mpq(2)); // vector ev; @@ -1016,10 +1016,10 @@ void test_total_case_u() { unsigned x = ls.add_var(0, false); unsigned y = ls.add_var(1, false); unsigned z = ls.add_var(2, false); - vector> c; - c.push_back(std::pair(mpq(1), x)); - c.push_back(std::pair(mpq(2), y)); - c.push_back(std::pair(mpq(3), z)); + vector> c; + c.push_back(std::pair(mpq(1), x)); + c.push_back(std::pair(mpq(2), y)); + c.push_back(std::pair(mpq(3), z)); // todo: restore test // ls.add_constraint(c, LE, one_of_type()); // ls.add_var_bound(x, GE, zero_of_type()); @@ -1044,10 +1044,10 @@ void test_total_case_l() { unsigned x = ls.add_var(0, false); unsigned y = ls.add_var(1, false); unsigned z = ls.add_var(2, false); - vector> c; - c.push_back(std::pair(mpq(1), x)); - c.push_back(std::pair(mpq(2), y)); - c.push_back(std::pair(mpq(3), z)); + vector> c; + c.push_back(std::pair(mpq(1), x)); + c.push_back(std::pair(mpq(2), y)); + c.push_back(std::pair(mpq(3), z)); // todo: restore test // ls.add_constraint(c, GE, one_of_type()); // ls.add_var_bound(x, LE, one_of_type()); @@ -1611,15 +1611,15 @@ void test_maximize_term() { int_solver i_solver(solver); // have to create it too unsigned _x = 0; unsigned _y = 1; - var_index x = solver.add_var(_x, false); - var_index y = solver.add_var(_y, true); - vector> term_ls; - term_ls.push_back(std::pair(mpq(1), x)); - term_ls.push_back(std::pair(mpq(-1), y)); + lpvar x = solver.add_var(_x, false); + lpvar y = solver.add_var(_y, true); + vector> term_ls; + term_ls.push_back(std::pair(mpq(1), x)); + term_ls.push_back(std::pair(mpq(-1), y)); unsigned term_x_min_y = solver.add_term(term_ls, -1); term_ls.clear(); - term_ls.push_back(std::pair(mpq(2), x)); - term_ls.push_back(std::pair(mpq(2), y)); + term_ls.push_back(std::pair(mpq(2), x)); + term_ls.push_back(std::pair(mpq(2), y)); unsigned term_2x_pl_2y = solver.add_term(term_ls, -1); solver.add_var_bound(term_x_min_y, LE, zero_of_type()); @@ -1627,7 +1627,7 @@ void test_maximize_term() { solver.find_feasible_solution(); lp_assert(solver.get_status() == lp_status::OPTIMAL); std::cout << solver.constraints(); - std::unordered_map model; + std::unordered_map model; solver.get_model(model); for (auto p : model) { std::cout << "v[" << p.first << "] = " << p.second << std::endl; @@ -1918,4 +1918,4 @@ void test_patching() { test_patching_alpha(rational(x1, x2), rational(a1, a2)); } -} \ No newline at end of file +} diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 7843d5714d2..7a0ea5ff989 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -28,7 +28,7 @@ Revision History: #include #include #include -#include "math/lp/ul_pair.h" +#include "math/lp/column.h" #include "math/lp/lar_constraints.h" #include #include @@ -383,7 +383,7 @@ namespace lp { } void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc, unsigned i) { - vector> ls; + vector> ls; for (auto & it : fc.m_coeffs) { ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false))); }