From e5cc613bf1dfc0fd4f13b57ae3b550bfce3e903c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 21 Oct 2020 14:12:05 +0100 Subject: [PATCH] remove some dup map lookups (mentioned in perf sanitizer paper) --- src/smt/theory_lra.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5f35dd5d3..e4999d6c2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1438,11 +1438,12 @@ public: if (v == null_theory_var || !lp().external_is_used(v)) { return rational::zero(); } - + auto t = get_tv(v); - if (m_variable_values.count(t.index()) > 0) - return m_variable_values[t.index()]; - + auto I = m_variable_values.find(t.index()); + if (I != m_variable_values.end()) + return I->second; + if (!t.is_term() && lp().is_fixed(t.id())) return lp().column_lower_bound(t.id()).x; if (!t.is_term()) @@ -1458,8 +1459,9 @@ public: const lp::lar_term& term = lp().get_term(t2); for (const auto & i : term) { auto tv = lp().column2tv(i.column()); - if (m_variable_values.count(tv.index()) > 0) { - result += m_variable_values[tv.index()] * coeff * i.coeff(); + auto I = m_variable_values.find(tv.index()); + if (I != m_variable_values.end()) { + result += I->second * coeff * i.coeff(); } else { m_todo_terms.push_back(std::make_pair(tv, coeff * i.coeff())); @@ -1467,10 +1469,10 @@ public: } } else { - result += m_variable_values[t2.index()] * coeff; + result += m_variable_values.at(t2.index()) * coeff; } } - m_variable_values[t.index()] = result; + m_variable_values.emplace(t.index(), result); return result; }