From 4f2eb0b4eb43086555ba16f07e0eb73daa4cf59b Mon Sep 17 00:00:00 2001 From: Lev Date: Sat, 29 Dec 2018 03:03:30 -0800 Subject: [PATCH] remove an unused field Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 03a4b4098..827b9c2b5 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -29,7 +29,6 @@ namespace nla { typedef lp::lconstraint_kind llc; struct solver::imp { - typedef lp::lar_base_constraint lpcon; //fields @@ -40,7 +39,6 @@ struct solver::imp { // this field is used for the push/pop operations unsigned_vector m_monomials_counts; lp::lar_solver& m_lar_solver; - std::unordered_map> m_monomials_containing_var; // m_var_to_its_monomial[m_monomials[i].var()] = i std::unordered_map m_var_to_its_monomial; @@ -1000,28 +998,12 @@ struct solver::imp { return false; } - void map_monomial_vars_to_monomial_indices(unsigned i) { - const monomial& m = m_monomials[i]; - for (lpvar j : m.vars()) { - auto it = m_monomials_containing_var.find(j); - if (it == m_monomials_containing_var.end()) { - unsigned_vector ms; - ms.push_back(i); - m_monomials_containing_var[j] = ms; - } - else { - it->second.push_back(i); - } - } - } - void map_vars_to_monomials() { for (unsigned i = 0; i < m_monomials.size(); i++) { const monomial& m = m_monomials[i]; lpvar v = m.var(); SASSERT(m_var_to_its_monomial.find(v) == m_var_to_its_monomial.end()); m_var_to_its_monomial[v] = i; - map_monomial_vars_to_monomial_indices(i); } } @@ -1184,7 +1166,6 @@ struct solver::imp { m_var_to_its_monomial.clear(); m_vars_equivalence.clear(); m_rm_table.clear(); - m_monomials_containing_var.clear(); m_expl->clear(); m_lemma->clear(); }