mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-29 13:28:44 +00:00
Code Activity

Refactor sat_solver to use C++17 structured bindings for pair destructuring (#8403)

Browse source 
* Initial plan

* Refactor sat_solver.cpp to use structured bindings for pairs

- Line 1398: Changed priorities[i].second to use [priority, var]
- Lines 2154-2156: Changed p.first/p.second to use [l1, l2] for binary clauses
- Lines 4182-4184: Eliminated intermediate l1, l2 variables using [l1, l2] binding

This modernizes the code to use C++17 structured bindings instead of .first/.second member accesses.

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-27 20:06:07 -08:00 • committed by GitHub
parent 560985893e
commit 1d49af5ee6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/sat_solver.cpp
View file

@ -1394,8 +1394,10 @@ namespace sat {
for (unsigned i = 0; i < mdl.size(); ++i)
priorities[i] = { m_local_search->get_priority(i), i };
std::sort(priorities.begin(), priorities.end(), [](auto& x, auto& y) { return x.first > y.first; });
for (unsigned i = priorities.size() / 10; i-- > 0; )
move_to_front(priorities[i].second);
for (unsigned i = priorities.size() / 10; i-- > 0; ) {
auto [priority, var] = priorities[i];
move_to_front(var);
}
#endif
@ -2151,9 +2153,9 @@ namespace sat {
#if 0
IF_VERBOSE(2, for (bool_var v = 0; v < num; ++v) verbose_stream() << v << ": " << m_model[v] << "\n";);
for (auto p : big::s_del_bin) {
if (value(p.first) != l_true && value(p.second) != l_true) {
IF_VERBOSE(2, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n");
for (auto [l1, l2] : big::s_del_bin) {
if (value(l1) != l_true && value(l2) != l_true) {
IF_VERBOSE(2, verbose_stream() << "binary violation: " << l1 << " " << l2 << "\n");
}
}
#endif
@ -4179,9 +4181,7 @@ namespace sat {
// m_binary_clause_graph.reset();
collect_bin_clauses(m_user_bin_clauses, true, false);
hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
for (auto const& b : m_user_bin_clauses) {
literal l1 = b.first;
literal l2 = b.second;
for (auto const& [l1, l2] : m_user_bin_clauses) {
literal_pair p(l1, l2);
if (!seen_bc.contains(p)) {
seen_bc.insert(p);