From 719603f1856add4bff1c70e9533c33554144ecc9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 9 Mar 2020 13:07:05 -0700 Subject: [PATCH] register inner terms with null var Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 6 +++--- src/math/lp/var_register.h | 10 ++++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 1144279ca..9e917728b 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1708,13 +1708,13 @@ bool lar_solver::all_vars_are_registered(const vector> // do not register this term if ext_i == -1 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 (ext_i + 1) - m_term_register.add_var(ext_i, term_is_int(coeffs)); + m_term_register.add_var(ext_i, term_is_int(coeffs)); lp_assert(all_vars_are_registered(coeffs)); if (strategy_is_undecided()) return add_term_undecided(coeffs); lar_term * t = new lar_term(coeffs); push_term(t); + SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = m_terms_start_index + adjusted_term_index; if (use_tableau() && !coeffs.empty()) { @@ -2370,7 +2370,7 @@ std::pair lar_solver::add_equality(lpvar j, 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, -1); // -1 to not register the term: only external terms are registered + unsigned term_index = add_term(coeffs, -1); // -1 is the external null var return std::pair( add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index a97a039b4..0295da67d 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -50,11 +50,13 @@ public: } unsigned add_var(unsigned user_var, bool is_int) { - auto t = m_external_to_local.find(user_var); - if (t != m_external_to_local.end()) { - return t->second; + if (user_var + 1) { // user_var != -1 + auto t = m_external_to_local.find(user_var); + if (t != m_external_to_local.end()) { + return t->second; + } } - + m_local_to_external.push_back(ext_var_info(user_var, is_int)); return m_external_to_local[user_var] = size() - 1 + m_local_offset; }