From c2e5cd78c8e5023ef60802f901efbe5e4d390110 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 11:51:06 -0700 Subject: [PATCH] change lar_terms to use column indices Signed-off-by: Nikolaj Bjorner --- src/math/lp/general_matrix.h | 2 +- src/math/lp/gomory.cpp | 10 +++++----- src/math/lp/hnf_cutter.cpp | 3 ++- src/math/lp/int_cube.cpp | 4 ++-- src/math/lp/int_solver.cpp | 2 +- src/math/lp/int_solver.h | 2 +- src/math/lp/lar_solver.cpp | 36 +++++++++++++---------------------- src/math/lp/lar_solver.h | 32 +++++++------------------------ src/math/lp/lar_term.h | 9 ++++----- src/math/lp/lp_types.h | 20 +++++++++++++++++++ src/math/lp/nla_core.cpp | 30 ++++++++++++++--------------- src/math/lp/static_matrix.h | 4 ++-- src/smt/theory_lra.cpp | 37 ++++++++++++++++-------------------- 13 files changed, 88 insertions(+), 103 deletions(-) diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h index 0a5b5286e..6a996ddfa 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().index())); + unsigned j = adjust_column(column_fix(p.column().index())); row[j] = sign * p.coeff(); } } diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 62bd4ba7e..135eafff2 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -191,7 +191,8 @@ 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().index()) << ")"; + auto t = lia.lra.column2tv(c.column()); + out << " " << var_name(t.id()) << ")"; } std::ostream& dump_row_coefficients(std::ostream & out) const { @@ -221,9 +222,9 @@ class create_cut { dump_declaration(out, p.var()); } for (const auto& p : m_t) { - unsigned v = p.var().index(); - if (lp::tv::is_term(v)) { - dump_declaration(out, v); + auto t = lia.lra.column2tv(p.column()); + if (t.is_term()) { + dump_declaration(out, t.id()); } } } @@ -349,7 +350,6 @@ public: // NSB code review: this is also used in nla_core. // but it isn't consistent: when theory_lra accesses lar_solver::get_term, the term that is returned uses // column indices, not terms. - lia.lra.subs_term_columns(m_t); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index cbc5eb4f8..687a5517c 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -50,7 +50,8 @@ namespace lp { m_constraints_for_explanation.push_back(ci); for (const auto &p : *t) { - m_var_register.add_var(p.var().index(), true); // hnf only deals with integral variables for now + auto tv = lia.lra.column2tv(p.column()); + m_var_register.add_var(tv.id(), 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 24609ec25..347da2155 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().index())) + if (!lia.column_is_int(p.column())) 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().index())) + if (lia.column_is_int(p.column())) 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 c56551b04..b0432e123 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -228,7 +228,7 @@ const lp_settings& int_solver::settings() const { return lra.settings(); } -bool int_solver::column_is_int(unsigned j) const { +bool int_solver::column_is_int(column_index const& j) const { return lra.column_is_int(j); } diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index a87472178..e4dbace0b 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -82,7 +82,7 @@ public: bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; const impq & upper_bound(unsigned j) const; - bool column_is_int(unsigned j) const; + bool column_is_int(column_index const& 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_solver.cpp b/src/math/lp/lar_solver.cpp index 99c79f5e3..4aca609d9 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 const& t = get_term(be.m_j); auto first_coeff = t.begin(); - unsigned j = (*first_coeff).var().index(); + unsigned j = (*first_coeff).column(); 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().index()); + it = coeff_map.find(p.column()); if (it == coeff_map.end()) return false; if (p.coeff() * ratio != it->second) @@ -231,6 +231,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & } // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } + // here i is just the term index bool lar_solver::term_is_used_as_row(unsigned i) const { SASSERT(i < m_terms.size()); @@ -246,7 +247,6 @@ void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) { } } - // goes over touched rows and tries to induce bounds void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { if (!use_tableau()) @@ -423,7 +423,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().index(); + unsigned j = p.column(); rslv.m_costs[j] = zero_of_type(); int i = rslv.m_basis_heading[j]; if (i < 0) @@ -454,7 +454,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().index(); + unsigned j = p.column(); rslv.m_costs[j] = p.coeff(); if (rslv.m_basis_heading[j] < 0) rslv.m_d[j] += p.coeff(); @@ -681,7 +681,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().index(); + var_index j = t.column(); A.set(last_row, j, - t.coeff()); } unsigned basis_j = A.column_count() - 1; @@ -1147,7 +1147,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().index()); + impq const& r = get_column_value(cv.column()); if (!numeric_traits::is_zero(r.y)) return false; value += r.x * cv.coeff(); } @@ -1306,7 +1306,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().index()); + out << this->get_variable_name(p.column()); } return out; } @@ -1530,7 +1530,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().index()) && p.coeff().is_int())) + if (! (column_is_int(p.column()) && p.coeff().is_int())) return false; return true; } @@ -1691,19 +1691,9 @@ bool lar_solver::term_coeffs_are_ok(const vector> & co } #endif void lar_solver::push_term(lar_term* t) { - // SASSERT(well_formed(*t)); m_terms.push_back(t); } -bool lar_solver::well_formed(lar_term const& t) const { - for (auto const& ti : t) { - if (!ti.var().is_term() && - column_corresponds_to_term(ti.var().index())) { - return false; - } - } - return true; -} // terms @@ -1956,7 +1946,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().index(); + var_index j = t.column(); A.set(last_row, j, -t.coeff().get_double()); } @@ -2257,7 +2247,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().index())) { + if (m_incorrect_columns.contains(p.column())) { need_to_fix = true; break; } @@ -2274,7 +2264,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().index()]; + const auto & x = m_mpq_lar_core_solver.m_r_x[c.column()]; 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 e28737a7a..afb6db79c 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -60,7 +60,7 @@ class lar_solver : public column_namer { size_t seed = 0; int i = 0; for (const auto p : t) { - hash_combine(seed, p.var().index()); + hash_combine(seed, (unsigned)p.column()); hash_combine(seed, p.coeff()); if (i++ > 10) break; @@ -125,15 +125,11 @@ public: static bool valid_index(unsigned j){ return static_cast(j) >= 0;} - bool column_is_int(unsigned j) const; - bool column_value_is_int(unsigned j) const { - return m_mpq_lar_core_solver.m_r_x[j].is_int(); - } - + bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); } - const impq& get_column_value(unsigned j) const { - return m_mpq_lar_core_solver.m_r_x[j]; - } + bool column_is_int(unsigned j) const; + bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } + const impq& get_column_value(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j]; } void set_column_value(unsigned j, const impq& v) { m_mpq_lar_core_solver.m_r_x[j] = v; @@ -583,23 +579,9 @@ public: return m_columns_to_ul_pairs()[j].lower_bound_witness(); } - // NSB code review - seems superfluous to translate back and forth because - // get_term(..) that is exposed over API does not ensure that columns that - // are based on terms are translated back to term indices. - // would be better to have consistent typing, either lar_term uses cv (and not tv) - // or they are created to use tv consistently. - void subs_term_columns(lar_term& t) { - svector> columns_to_subs; - for (const auto & m : t) { - 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); - } + tv column2tv(column_index const& c) const { + return tv::raw(adjust_column_index_to_term_index(c)); } - std::ostream& print_column_info(unsigned j, std::ostream& out) const { m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 1f44729c7..662ed0410 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -123,8 +123,7 @@ public: const mpq & m_coeff; public: ival(unsigned var, const mpq & val) : m_var(var), m_coeff(val) { } - unsigned raw() const { return m_var; } - tv var() const { return tv::raw(m_var); } + column_index column() const { return column_index(m_var); } const mpq & coeff() const { return m_coeff; } }; @@ -143,13 +142,13 @@ public: lpvar min_var = -1; mpq c; for (const auto & p : *this) { - if (p.var().index() < min_var) { - min_var = p.var().index(); + if (p.column() < min_var) { + min_var = p.column(); } } lar_term r; for (const auto & p : *this) { - if (p.var().index() == min_var) { + if (p.column() == min_var) { return p.coeff().is_one(); } } diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h index af41aa913..05193a9b4 100644 --- a/src/math/lp/lp_types.h +++ b/src/math/lp/lp_types.h @@ -21,6 +21,11 @@ Revision History: #include + +namespace nla { + class core; +} + namespace lp { typedef unsigned var_index; typedef unsigned constraint_index; @@ -62,8 +67,23 @@ public: } }; + +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; } +}; + } 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/nla_core.cpp b/src/math/lp/nla_core.cpp index c4392a60d..5e59dc431 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().index()); + ret += t.coeff() * val(t.column()); } 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().index(); + lpvar j = p.column(); 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().index()); + unsigned c = m_lar_solver.get_column_lower_bound_witness(p.column()); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_lower_bound(p.var().index()).x; + bound = a * m_lar_solver.get_lower_bound(p.column()).x; e.add(c); return true; } // a.is_neg() - c = m_lar_solver.get_column_upper_bound_witness(p.var().index()); + c = m_lar_solver.get_column_upper_bound_witness(p.column()); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_upper_bound(p.var().index()).x; + bound = a * m_lar_solver.get_upper_bound(p.column()).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 = p.var().is_term()? m_lar_solver.map_term_index_to_column_index(p.var().index()) : p.var().index(); + lpvar j = p.column(); SASSERT(!a.is_zero()); unsigned c; // the index for the lower or the upper bound if (a.is_neg()) { @@ -426,7 +426,6 @@ bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const { void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) { TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); if (!explain_ineq(t, cmp, rs)) { - m_lar_solver.subs_term_columns(t); current_lemma().push_back(ineq(cmp, t, rs)); CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); SASSERT(!ineq_holds(ineq(cmp, t, rs))); @@ -435,7 +434,6 @@ void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) { void core::mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs) { TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); - m_lar_solver.subs_term_columns(t); current_lemma().push_back(ineq(cmp, t, rs)); CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); SASSERT(!ineq_holds(ineq(cmp, t, rs))); @@ -681,7 +679,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().index()); + vars.insert(p.column()); } out << std::endl; for (lpvar j : vars) { @@ -864,9 +862,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().index(); + i = p.column(); else - j = p.var().index(); + j = p.column(); } SASSERT(j != static_cast(-1)); sign = (seen_minus && seen_plus)? false : true; @@ -987,7 +985,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().index()); + insert_j(p.column()); } } for (const auto& p : current_expl()) { @@ -1754,9 +1752,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(lp::tv::raw(ls.local_to_external(j))); for (auto p : t) { - if (ret.find(p.var().index()) == ret.end()) { - added.push_back(p.var().index()); - ret.insert(p.var().index()); + if (ret.find(p.column()) == ret.end()) { + added.push_back(p.column()); + ret.insert(p.column()); } } } diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 016775507..039de80ef 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().index()); + m_work_vector.set_value(-p.coeff(), p.column().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().index(), basis_heading); + fill_last_row_with_pivoting_loop_block(p.column().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 1c198fb85..e13194ef8 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1523,7 +1523,7 @@ public: if (t.is_term()) { const lp::lar_term& term = lp().get_term(t); 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(lp().column2tv(i.column()), coeff * i.coeff())); } } else { @@ -1555,11 +1555,12 @@ public: if (t2.is_term()) { const lp::lar_term& term = lp().get_term(t2); for (const auto & i : term) { - if (m_variable_values.count(i.var().index()) > 0) { - result += m_variable_values[i.var().index()] * coeff * i.coeff(); + auto tv = lp().column2tv(i.column()); + if (m_variable_values.count(tv.index()) > 0) { + result += m_variable_values[tv.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(tv, coeff * i.coeff())); } } } @@ -1955,7 +1956,7 @@ public: expr_ref t(m); expr_ref_vector ts(m); for (auto const& p : term) { - auto ti = p.var(); + auto ti = lp().column2tv(p.column()); if (ti.is_term()) { ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(ti)))); } @@ -1997,7 +1998,7 @@ public: lp().print_term(term, out << "bound: "); out << (upper?" <= ":" >= ") << k << "\n"; for (auto const& p : term) { - auto ti = p.var(); + auto ti = lp().column2tv(p.column()); out << p.coeff() << " * "; if (ti.is_term()) { lp().print_term(lp().get_term(ti), out) << "\n"; @@ -2798,7 +2799,7 @@ public: m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(ti); for (auto const& p : term) { - lp::tv wi = p.var(); + lp::tv wi = lp().column2tv(p.column()); if (wi.is_term()) { m_todo_vars.push_back(wi); } @@ -2824,7 +2825,7 @@ public: m_todo_vars.pop_back(); lp::lar_term const& term = lp().get_term(ti); for (auto const& coeff : term) { - auto wi = coeff.var(); + auto wi = lp().column2tv(coeff.column()); if (wi.is_term()) { m_todo_vars.push_back(wi); } @@ -2914,7 +2915,7 @@ public: SASSERT(ti.is_term()); lp::lar_term const& term = m_solver->get_term(ti); for (auto const mono : term) { - auto wi = mono.var(); + auto wi = lp().column2tv(mono.column()); lp::constraint_index ci; rational value; bool is_strict; @@ -3377,7 +3378,7 @@ public: m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); for (auto const & arg : term) { - auto wi = arg.var(); + auto wi = lp().column2tv(arg.column()); c1 = arg.coeff() * wcoeff; if (wi.is_term()) { m_todo_terms.push_back(std::make_pair(wi, c1)); @@ -3658,23 +3659,17 @@ public: TRACE("arith", lp().print_term(term, tout) << "\n";); for (const auto & ti : term) { theory_var w; - if (ti.var().is_term()) { - lp::lar_term const& term1 = lp().get_term(ti.var()); + auto tv = lp().column2tv(ti.column()); + if (tv.is_term()) { + lp::lar_term const& term1 = lp().get_term(tv); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2); continue; } - else if (lp().column_corresponds_to_term(ti.var().index())) { - lp::tv t = lp::tv::term(ti.var().index()); - lp::lar_term const& term1 = lp().get_term(t); - rational coeff2 = coeff * ti.coeff(); - term2coeffs(term1, coeffs, coeff2); - continue; - } else { - w = lp().local_to_external(ti.var().index()); + w = lp().local_to_external(tv.id()); SASSERT(w >= 0); - TRACE("arith", tout << (ti.var().index()) << ": " << w << "\n";); + TRACE("arith", tout << (tv.id()) << ": " << w << "\n";); } rational c0(0); coeffs.find(w, c0);