From f5b62015fc10d1d065b53a4c9b2d0646df5fee98 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 25 Mar 2020 16:02:36 -0700 Subject: [PATCH] change the return type of ival.var() to tv Signed-off-by: Lev Nachmanson --- src/math/lp/general_matrix.h | 2 +- src/math/lp/gomory.cpp | 4 ++-- src/math/lp/hnf_cutter.cpp | 2 +- src/math/lp/int_cube.cpp | 4 ++-- src/math/lp/lar_solver.cpp | 26 +++++++++++++------------- src/math/lp/lar_solver.h | 8 ++++---- src/math/lp/lar_term.h | 9 +++++---- src/math/lp/nla_core.cpp | 28 ++++++++++++++-------------- src/math/lp/static_matrix.h | 4 ++-- src/smt/theory_lra.cpp | 26 +++++++++++++------------- 10 files changed, 57 insertions(+), 56 deletions(-) diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index f6f93c705..0a5b5286e 100644 --- a/src/math/lp/general_matrix.h +++ b/src/math/lp/general_matrix.h @@ -109,7 +109,7 @@ public: auto & row = m_data[adjust_row(i)]; lp_assert(row_is_initialized_correctly(row)); for (const auto & p : c) { - unsigned j = adjust_column(column_fix(p.var())); + unsigned j = adjust_column(column_fix(p.var().index())); row[j] = sign * p.coeff(); } } diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 0d7db428d..37b201497 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -191,7 +191,7 @@ class create_cut { void dump_coeff(std::ostream & out, const T& c) const { out << "( * "; dump_coeff_val(out, c.coeff()); - out << " " << var_name(c.var()) << ")"; + out << " " << var_name(c.var().index()) << ")"; } std::ostream& dump_row_coefficients(std::ostream & out) const { @@ -221,7 +221,7 @@ class create_cut { dump_declaration(out, p.var()); } for (const auto& p : m_t) { - unsigned v = p.var(); + unsigned v = p.var().index(); if (lp::tv::is_term(v)) { dump_declaration(out, v); } diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 5b675fa64..7c8dd42d7 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -50,7 +50,7 @@ namespace lp { m_constraints_for_explanation.push_back(ci); for (const auto &p : *t) { - m_var_register.add_var(p.var(), true); // hnf only deals with integral variables for now + m_var_register.add_var(p.var().index(), true); // hnf only deals with integral variables for now mpq t = abs(ceil(p.coeff())); if (t > m_abs_max) m_abs_max = t; diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index 87db17f70..1f918bc7c 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -86,7 +86,7 @@ namespace lp { bool seen_minus = false; bool seen_plus = false; for(const auto & p : t) { - if (!lia.column_is_int(p.var())) + if (!lia.column_is_int(p.var().index())) 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 (const auto & p : t) - if (lia.column_is_int(p.var())) + if (lia.column_is_int(p.var().index())) delta += abs(p.coeff()); delta *= mpq(1, 2); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index b36244a66..0d7889041 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -115,13 +115,13 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, } else { lar_term & t = *m_terms[tv::unmask_term(be.m_j)]; auto first_coeff = t.begin(); - unsigned j = (*first_coeff).var(); + unsigned j = (*first_coeff).var().index(); 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.var()); + it = coeff_map.find(p.var().index()); if (it == coeff_map.end()) return false; if (p.coeff() * ratio != it->second) @@ -421,7 +421,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) { lp_assert(jset.is_empty()); for (const auto & p : term) { - unsigned j = p.var(); + unsigned j = p.var().index(); rslv.m_costs[j] = zero_of_type(); int i = rslv.m_basis_heading[j]; if (i < 0) @@ -452,7 +452,7 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { lp_assert(reduced_costs_are_zeroes_for_r_solver()); rslv.m_costs.resize(A_r().column_count(), zero_of_type()); for (const auto & p : term) { - unsigned j = p.var(); + unsigned j = p.var().index(); rslv.m_costs[j] = p.coeff(); if (rslv.m_basis_heading[j] < 0) rslv.m_d[j] += p.coeff(); @@ -679,7 +679,7 @@ void lar_solver::substitute_terms_in_linear_expression(const vector> & A, lp_assert(A.m_rows[last_row].size() == 0); for (auto t : *ls) { lp_assert(!is_zero(t.coeff())); - var_index j = t.var(); + var_index j = t.var().index(); A.set(last_row, j, - t.coeff()); } unsigned basis_j = A.column_count() - 1; @@ -1145,7 +1145,7 @@ bool lar_solver::has_value(var_index var, mpq& value) const { lar_term const& t = get_term(var); value = 0; for (auto const& cv : t) { - impq const& r = get_column_value(cv.var()); + impq const& r = get_column_value(cv.var().index()); if (!numeric_traits::is_zero(r.y)) return false; value += r.x * cv.coeff(); } @@ -1304,7 +1304,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c out << " - "; else if (val != numeric_traits::one()) out << T_to_string(val); - out << this->get_variable_name(p.var()); + out << this->get_variable_name(p.var().index()); } return out; } @@ -1331,7 +1331,7 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v var_index var = vars[i]; if (tv::is_term(var)) { // handle the term for (auto it : *m_terms[tv::unmask_term(var)]) { - column_list.push_back(it.var()); + column_list.push_back(it.var().index()); } } else { column_list.push_back(var); @@ -1527,7 +1527,7 @@ bool lar_solver::model_is_int_feasible() const { bool lar_solver::term_is_int(const lar_term * t) const { for (auto const p : *t) - if (! (column_is_int(p.var()) && p.coeff().is_int())) + if (! (column_is_int(p.var().index()) && p.coeff().is_int())) return false; return true; } @@ -1938,7 +1938,7 @@ void lar_solver::fill_last_row_of_A_d(static_matrix & A, const l for (auto t : *ls) { lp_assert(!is_zero(t.coeff())); - var_index j = t.var(); + var_index j = t.var().index(); A.set(last_row, j, -t.coeff().get_double()); } @@ -2239,7 +2239,7 @@ void lar_solver::fix_terms_with_rounded_columns() { bool need_to_fix = false; const lar_term & t = *m_terms[i]; for (const auto & p : t) { - if (m_incorrect_columns.contains(p.var())) { + if (m_incorrect_columns.contains(p.var().index())) { need_to_fix = true; break; } @@ -2256,7 +2256,7 @@ void lar_solver::fix_terms_with_rounded_columns() { bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const { val = zero_of_type(); for (const auto & c : t) { - const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()]; + const auto & x = m_mpq_lar_core_solver.m_r_x[c.var().index()]; if (!is_zero(x.y)) return false; val += x.x * c.coeff(); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index ad3a28f11..cf52c2ca8 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, p.var()); + hash_combine(seed, p.var().index()); hash_combine(seed, p.coeff()); if (i++ > 10) break; @@ -578,9 +578,9 @@ public: void subs_term_columns(lar_term& t) { vector> columns_to_subs; for (const auto & m : t) { - unsigned tj = adjust_column_index_to_term_index(m.var()); - if (tj == m.var()) continue; - columns_to_subs.push_back(std::make_pair(m.var(), tj)); + unsigned tj = adjust_column_index_to_term_index(m.var().index()); + if (tj == m.var().index()) continue; + columns_to_subs.push_back(std::make_pair(m.var().index(), tj)); } for (const auto & p : columns_to_subs) { t.subst_index(p.first, p.second); diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index a5d716ebb..3e7dc7ef8 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -123,7 +123,8 @@ public: const mpq & m_coeff; public: ival(unsigned var, const mpq & val) : m_var(var), m_coeff(val) { } - unsigned var() const { return m_var; } + unsigned raw() const { return m_var; } + tv var() const { return tv::raw(m_var); } const mpq & coeff() const { return m_coeff; } }; @@ -142,13 +143,13 @@ public: lpvar min_var = -1; mpq c; for (const auto & p : *this) { - if (p.var() < min_var) { - min_var = p.var(); + if (p.var().index() < min_var) { + min_var = p.var().index(); } } lar_term r; for (const auto & p : *this) { - if (p.var() == min_var) { + if (p.var().index() == min_var) { return p.coeff().is_one(); } } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index ebc18ec01..5497414ed 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -50,7 +50,7 @@ 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 (const auto & t : r) { - ret += t.coeff() * val(t.var()); + ret += t.coeff() * val(t.var().index()); } return ret; } @@ -58,7 +58,7 @@ rational core::value(const lp::lar_term& r) const { lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const { lp::lar_term r; for (const auto& p : t) { - lpvar j = p.var(); + lpvar j = p.var().index(); if (lp::tv::is_term(j)) j = m_lar_solver.map_term_index_to_column_index(j); r.add_monomial(p.coeff(), j); @@ -323,25 +323,25 @@ bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bou SASSERT(!a.is_zero()); unsigned c; // the index for the lower or the upper bound if (a.is_pos()) { - unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var()); + unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var().index()); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_lower_bound(p.var()).x; + bound = a * m_lar_solver.get_lower_bound(p.var().index()).x; e.add(c); return true; } // a.is_neg() - c = m_lar_solver.get_column_upper_bound_witness(p.var()); + c = m_lar_solver.get_column_upper_bound_witness(p.var().index()); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_upper_bound(p.var()).x; + bound = a * m_lar_solver.get_upper_bound(p.var().index()).x; e.add(c); 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 = lp::tv::is_term(p.var())? m_lar_solver.map_term_index_to_column_index(p.var()) : p.var(); + lpvar j = p.var().is_term()? m_lar_solver.map_term_index_to_column_index(p.var().index()) : p.var().index(); SASSERT(!a.is_zero()); unsigned c; // the index for the lower or the upper bound if (a.is_neg()) { @@ -681,7 +681,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 (const auto & p: in.m_term) - vars.insert(p.var()); + vars.insert(p.var().index()); } out << std::endl; for (lpvar j : vars) { @@ -864,9 +864,9 @@ bool core:: is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar return false; } if (i == static_cast(-1)) - i = p.var(); + i = p.var().index(); else - j = p.var(); + j = p.var().index(); } SASSERT(j != static_cast(-1)); sign = (seen_minus && seen_plus)? false : true; @@ -986,7 +986,7 @@ std::unordered_set core::collect_vars(const lemma& l) const { for (const auto& i : current_lemma().ineqs()) { for (const auto& p : i.term()) { - insert_j(p.var()); + insert_j(p.var().index()); } } for (const auto& p : current_expl()) { @@ -1628,9 +1628,9 @@ std::unordered_set core::get_vars_of_expr_with_opening_terms(const nex *e if (ls.column_corresponds_to_term(j)) { const auto& t = m_lar_solver.get_term(ls.local_to_external(j)); for (auto p : t) { - if (ret.find(p.var()) == ret.end()) { - added.push_back(p.var()); - ret.insert(p.var()); + if (ret.find(p.var().index()) == ret.end()) { + added.push_back(p.var().index()); + ret.insert(p.var().index()); } } } diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 295c7f01e..016775507 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -357,14 +357,14 @@ public: // 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.var()); + m_work_vector.set_value(-p.coeff(), p.var().index()); // 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.var(), basis_heading); + fill_last_row_with_pivoting_loop_block(p.var().index(), basis_heading); } lp_assert(m_work_vector.is_OK()); unsigned last_row = row_count() - 1; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bed099345..e07ed1577 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1503,7 +1503,7 @@ public: if (lp::tv::is_term(vi)) { const lp::lar_term& term = lp().get_term(vi); for (const auto & i: term) { - m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); + m_todo_terms.push_back(std::make_pair(i.var().index(), coeff * i.coeff())); } } else { @@ -1535,11 +1535,11 @@ public: if (lp::tv::is_term(wi)) { const lp::lar_term& term = lp().get_term(wi); for (const auto & i : term) { - if (m_variable_values.count(i.var()) > 0) { - result += m_variable_values[i.var()] * coeff * i.coeff(); + if (m_variable_values.count(i.var().index()) > 0) { + result += m_variable_values[i.var().index()] * coeff * i.coeff(); } else { - m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); + m_todo_terms.push_back(std::make_pair(i.var().index(), coeff * i.coeff())); } } } @@ -1931,7 +1931,7 @@ public: expr_ref t(m); expr_ref_vector ts(m); for (auto const& p : term) { - lpvar wi = p.var(); + lpvar wi = p.var().index(); if (lp::tv::is_term(wi)) { ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(wi)))); } @@ -1973,7 +1973,7 @@ public: lp().print_term(term, out << "bound: "); out << (upper?" <= ":" >= ") << k << "\n"; for (auto const& p : term) { - lpvar wi = p.var(); + lpvar wi = p.var().index(); out << p.coeff() << " * "; if (lp::tv::is_term(wi)) { lp().print_term(lp().get_term(wi), out) << "\n"; @@ -2771,7 +2771,7 @@ public: m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(vi); for (auto const& p : term) { - lpvar wi = p.var(); + lpvar wi = p.var().index(); if (lp::tv::is_term(wi)) { m_todo_vars.push_back(wi); } @@ -2796,7 +2796,7 @@ public: m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(vi); for (auto const& coeff : term) { - lpvar wi = coeff.var(); + lpvar wi = coeff.var().index(); if (lp::tv::is_term(wi)) { m_todo_vars.push_back(wi); } @@ -2886,7 +2886,7 @@ public: SASSERT(lp::tv::is_term(vi)); lp::lar_term const& term = m_solver->get_term(vi); for (auto const mono : term) { - lp::var_index wi = mono.var(); + lp::var_index wi = mono.var().index(); lp::constraint_index ci; rational value; bool is_strict; @@ -3349,7 +3349,7 @@ public: m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); for (auto const & arg : term) { - lpvar wi = arg.var(); + lpvar wi = arg.var().index(); c1 = arg.coeff() * wcoeff; if (lp::tv::is_term(wi)) { m_todo_terms.push_back(std::make_pair(wi, c1)); @@ -3621,16 +3621,16 @@ public: void term2coeffs(lp::lar_term const& term, u_map& coeffs, rational const& coeff) { for (const auto & ti : term) { theory_var w; - if (lp::tv::is_term(ti.var())) { + if (ti.var().is_term()) { //w = m_term_index2theory_var.get(lp::tv::unmask_term(ti.m_key), null_theory_var); //if (w == null_theory_var) // if extracting expressions directly from nested term - lp::lar_term const& term1 = lp().get_term(ti.var()); + lp::lar_term const& term1 = lp().get_term(ti.var().index()); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2); continue; } else { - w = lp().local_to_external(ti.var()); + w = lp().local_to_external(ti.var().index()); } rational c0(0); coeffs.find(w, c0);