mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 07:24:40 +00:00
Code Activity

Adopt C++17 structured bindings for map/pair iteration (#8159)

Browse source 
* Initial plan

* Adopt structured bindings for map iteration

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix DEBUG_CODE macro issue with structured bindings

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>
This commit is contained in:
Copilot 2026-01-11 17:44:12 -08:00 • committed by Nikolaj Bjorner
parent f15b0b2a56
commit d68837693c
10 changed files with 20 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_anf_simplifier.cpp
View file

@ -251,10 +251,10 @@ namespace sat {
TRACE(anf_simplifier,
tout << "kept:\n";
for (clause* cp : clauses) tout << *cp << "\n";
for (auto b : bins) tout << b.first << " " << b.second << "\n";
for (auto [l1, l2] : bins) tout << l1 << " " << l2 << "\n";
tout << "removed:\n";
for (clause* cp : oclauses) tout << *cp << "\n";
for (auto b : obins) tout << b.first << " " << b.second << "\n";);
for (auto [l1, l2] : obins) tout << l1 << " " << l2 << "\n";);
}
void anf_simplifier::set_relevant(solver::bin_clause const& b) {

6
src/sat/sat_simplifier.cpp
View file

@ -1766,10 +1766,10 @@ namespace sat {
m_elim_todo.reset();
std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt());
TRACE(sat_simplifier,
for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") ";
for (auto& [v, c] : tmp) tout << "(" << v << ", " << c << ") ";
tout << "\n";);
for (auto& p : tmp)
r.push_back(p.first);
for (auto& [v, c] : tmp)
r.push_back(v);
}
/**

4
src/sat/smt/arith_solver.cpp
View file

@ -1260,7 +1260,7 @@ namespace arith {
TRACE(arith_conflict,
tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
for (literal c : m_core) tout << c << ": " << literal2expr(c) << " := " << s().value(c) << "\n";
for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
for (auto [n1, n2] : m_eqs) tout << ctx.bpp(n1) << " == " << ctx.bpp(n2) << "\n";);
if (ctx.get_config().m_arith_validate)
VERIFY(validate_conflict());
@ -1268,7 +1268,7 @@ namespace arith {
if (is_conflict) {
DEBUG_CODE(
for (literal c : m_core) VERIFY(s().value(c) == l_true);
for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()));
for (auto [n1, n2] : m_eqs) VERIFY(n1->get_root() == n2->get_root()));
++m_num_conflicts;
++m_stats.m_conflicts;
auto* hint = explain_conflict(ty, m_core, m_eqs);

2
src/sat/smt/pb_pb.h
View file

@ -47,7 +47,7 @@ namespace pb {
void negate() override;
void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
void swap(unsigned i, unsigned j) noexcept override { std::swap(m_wlits[i], m_wlits[j]); }
literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
literal_vector literals() const override { literal_vector lits; for (auto [w, l] : *this) lits.push_back(l); return lits; }
bool is_watching(literal l) const override;
literal get_lit(unsigned i) const override { return m_wlits[i].second; }
void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; }

2
src/sat/smt/pb_solver.h
View file

@ -74,7 +74,7 @@ namespace pb {
unsigned bv_coeff(bool_var v) const;
void divide(unsigned c);
void weaken(unsigned i);
bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; }
bool contains(literal l) const { for (auto [w, lit] : m_wlits) if (lit == l) return true; return false; }
};
sat::sat_internalizer& si;