From c392592831ffefd67ac0c30c192a4e86a35ea225 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 21 Jan 2026 19:55:36 -0800 Subject: [PATCH] [WIP] Find and update std::optional usage in code base (#8272) * Initial plan * Add try_get_value for std::map and use it in var_register.h and dioph_eq.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add try_get_value overload for unordered_map with custom hash and use in lar_solver.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove redundant try_get_value template overload Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove std::map include and try_get_value overload from lp_utils.h Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/math/lp/dioph_eq.cpp | 6 ++--- src/math/lp/lar_solver.cpp | 51 ++++++++++++++++++++------------------ src/math/lp/lp_utils.h | 4 +-- src/math/lp/var_register.h | 33 +++++++++++------------- 4 files changed, 47 insertions(+), 47 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 39744ea83..57db6e79f 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1000,11 +1000,11 @@ namespace lp { void find_changed_terms_and_more_changed_rows() { for (unsigned j : m_changed_f_columns) { - const auto it = m_columns_to_terms.find(j); - if (it != m_columns_to_terms.end()) - for (unsigned k : it->second) { + if (auto terms = try_get_value(m_columns_to_terms, j)) { + for (unsigned k : *terms) { mark_term_change(k); } + } if (!m_var_register.external_is_used(j)) continue; for (const auto& p : m_e_matrix.column(this->lar_solver_to_local(j))) { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 23b219a8a..7d4732bd2 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -332,34 +332,38 @@ namespace lp { if (!column_has_term(be.m_j)) { if (coeff_map.size() != 1) return false; - auto it = coeff_map.find(be.m_j); - if (it == coeff_map.end()) return false; - mpq ratio = it->second; - if (ratio < zero_of_type()) { - kind = static_cast(-kind); + if (auto ratio_opt = try_get_value(coeff_map, be.m_j)) { + mpq ratio = *ratio_opt; + if (ratio < zero_of_type()) { + kind = static_cast(-kind); + } + rs_of_evidence /= ratio; + } else { + return false; } - rs_of_evidence /= ratio; } else { lar_term const& t = get_term(be.m_j); auto first_coeff = t.begin(); unsigned j = (*first_coeff).j(); - auto it = coeff_map.find(j); - if (it == coeff_map.end()) + if (auto ratio_opt = try_get_value(coeff_map, j)) { + mpq ratio = *ratio_opt / (*first_coeff).coeff(); + for (auto p : t) { + if (auto coeff_opt = try_get_value(coeff_map, p.j())) { + if (p.coeff() * ratio != *coeff_opt) + return false; + } else { + return false; + } + } + if (ratio < zero_of_type()) { + kind = static_cast(-kind); + } + rs_of_evidence /= ratio; + // rs_of_evidence += t->m_v * ratio; + } else { return false; - mpq ratio = it->second / (*first_coeff).coeff(); - for (auto p : t) { - it = coeff_map.find(p.j()); - if (it == coeff_map.end()) - return false; - if (p.coeff() * ratio != it->second) - return false; } - if (ratio < zero_of_type()) { - kind = static_cast(-kind); - } - rs_of_evidence /= ratio; - // rs_of_evidence += t->m_v * ratio; } return kind == be.kind() && rs_of_evidence == be.m_bound; @@ -2716,10 +2720,9 @@ namespace lp { bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair& a_j) const { TRACE(lar_solver_terms, print_term_as_indices(c, tout << "looking for term ") << "\n";); SASSERT(c.is_normalized()); - auto it = m_imp->m_normalized_terms_to_columns.find(c); - if (it != m_imp->m_normalized_terms_to_columns.end()) { - TRACE(lar_solver_terms, tout << "got " << it->second << "\n";); - a_j = it->second; + if (auto result = try_get_value(m_imp->m_normalized_terms_to_columns, c)) { + TRACE(lar_solver_terms, tout << "got " << *result << "\n";); + a_j = *result; return true; } TRACE(lar_solver_terms, tout << "have not found\n";); diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index 874bf1539..302ee803b 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -52,8 +52,8 @@ std::ostream& print_vector(const C * t, unsigned size, std::ostream & out) { } -template -std::optional try_get_value(const std::unordered_map & map, const A& key) { +template , typename KeyEqual = std::equal_to> +std::optional try_get_value(const std::unordered_map & map, const A& key) { const auto it = map.find(key); if (it == map.end()) return std::nullopt; diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 49771ae47..dcfc60092 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -18,6 +18,7 @@ Revision History: --*/ #pragma once #include "math/lp/lp_types.h" +#include "math/lp/lp_utils.h" namespace lp { @@ -53,9 +54,8 @@ public: unsigned add_var(unsigned user_var, bool is_int) { if (user_var != UINT_MAX) { - auto t = m_external_to_local.find(user_var); - if (t != m_external_to_local.end()) { - return t->second; + if (auto local = try_get_value(m_external_to_local, user_var)) { + return *local; } } @@ -96,29 +96,26 @@ public: } bool external_is_used(unsigned ext_j) const { - auto it = m_external_to_local.find(ext_j); - return it != m_external_to_local.end(); + return try_get_value(m_external_to_local, ext_j).has_value(); } bool external_is_used(unsigned ext_j, unsigned & local_j ) const { - auto it = m_external_to_local.find(ext_j); - if ( it == m_external_to_local.end()) { - local_j = UINT_MAX; - return false; + if (auto local = try_get_value(m_external_to_local, ext_j)) { + local_j = *local; + return true; } - local_j = it->second; - return true; + local_j = UINT_MAX; + return false; } bool external_is_used(unsigned ext_j, unsigned & local_j, bool & is_int ) const { - auto it = m_external_to_local.find(ext_j); - if ( it == m_external_to_local.end()){ - local_j = UINT_MAX; - return false; + if (auto local = try_get_value(m_external_to_local, ext_j)) { + local_j = *local; + is_int = m_local_to_external[local_j].is_integer(); + return true; } - local_j = it->second; - is_int = m_local_to_external[local_j].is_integer(); - return true; + local_j = UINT_MAX; + return false; } bool has_int_var() const {