mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-02 23:36:17 +00:00
Code Activity

Refactor sat_model_converter to use C++17 structured bindings (#8440)

Browse source 
* Initial plan

* Refactor sat_model_converter to use C++17 structured bindings

- Updated model_converter::process_stack() to use structured bindings
- Updated model_converter::display() to use structured bindings
- Updated model_converter::expand() to use structured bindings in range-based loop
- All changes compile successfully

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

* Fix build error in smt_justification.cpp structured binding

- Changed invalid syntax `enode_pair const & [n1, n2]` to `auto const& [n1, n2]`
- Wrapped for loop in extra parentheses to protect structured binding comma from macro expansion
- Build now completes successfully

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

* Fix DEBUG_CODE macro issue with structured bindings

- Reverted DEBUG_CODE block to use .first/.second instead of structured bindings
- Structured bindings with commas cause issues in macros (treated as argument separators)
- Build now works in both debug and release modes

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-31 17:13:07 -08:00 • committed by GitHub
parent db6e15361b
commit ff485eb545
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/sat_model_converter.cpp
View file

@ -46,8 +46,7 @@ namespace sat {
SASSERT(!stack.empty());
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
unsigned csz = stack[i].first;
literal lit = stack[i].second;
auto [csz, lit] = stack[i];
bool sat = false;
for (unsigned j = 0; !sat && j < csz; ++j) {
sat = value_at(c[j], m) == l_true;
@ -317,7 +316,8 @@ namespace sat {
elim_stackv const& stack = st->stack();
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
out << "\n " << stack[i].first << " " << stack[i].second;
auto [csz, lit] = stack[i];
out << "\n " << csz << " " << lit;
}
}
++index;
@ -385,9 +385,7 @@ namespace sat {
if (st) {
// clause sizes increase, so we can always swap
// the blocked literal to the front from the prefix.
for (auto const& p : st->stack()) {
unsigned csz = p.first;
literal lit = p.second;
for (auto const& [csz, lit] : st->stack()) {
swap(lit.var(), csz, clause);
update_stack.append(csz, clause.data());
update_stack.push_back(null_literal);