mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

use std::map instead of std::unordered_map

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-13 18:10:05 -07:00
parent 8bf2418b16
commit 39cc3393b7
1 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/levelwise.cpp
View file

@ -2,6 +2,7 @@
#include "nlsat/nlsat_types.h" #include "nlsat/nlsat_types.h"
#include <vector> #include <vector>
#include <unordered_map> #include <unordered_map>
#include <map>
namespace nlsat { namespace nlsat {
// Local enums reused from previous scaffolding // Local enums reused from previous scaffolding
@ -60,21 +61,21 @@ namespace nlsat {
std::vector<property> greatest_to_refine() { std::vector<property> greatest_to_refine() {
// For each polynomial p, pick the property at current level m_i // Deterministic order: use ascending polynomial id as key
// with the highest score, excluding sgn_inv_irreducible. std::map<unsigned, property> best_by_poly;
std::unordered_map<poly*, property> best;
for (const auto& q : m_Q) { for (const auto& q : m_Q) {
if (q.level != m_i) if (q.level != m_i)
continue; continue;
if (q.prop == prop_enum::sgn_inv_irreducible) if (q.prop == prop_enum::sgn_inv_irreducible)
continue; continue;
auto it = best.find(q.p); unsigned pid = polynomial::manager::id(q.p);
if (it == best.end() || score(q.prop) > score(it->second.prop)) auto it = best_by_poly.find(pid);
best[q.p] = q; if (it == best_by_poly.end() || score(q.prop) > score(it->second.prop))
best_by_poly[pid] = q;
} }
std::vector<property> ret; std::vector<property> ret;
ret.reserve(best.size()); ret.reserve(best_by_poly.size());
for (auto const& kv : best) for (auto const& kv : best_by_poly)
ret.push_back(kv.second); ret.push_back(kv.second);
return ret; return ret;
} }