[Conventions] Refactor sat_solver to use structured bindings for priority and literal pairs

[github-actions]

This refactoring modernizes the SAT solver core to use C++17 structured bindings instead of accessing .first and .second members of pairs.

Changes

File: src/sat/sat_solver.cpp

Scope: Refactoring of priority, binary clause, and literal pair patterns

Sites refactored: 6 member accesses across 3 functions

Types:

• std::pair(double, bool_var) (priority + variable)
• Literal pairs (binary clause literals)

Naming:

• [priority, var] for priority/variable pairs
• [l1, l2] for literal pairs - standard naming for binary clauses

Functions Modified

1. Local search priority processing (1 site - commented out code)

• Line 1398: Changed priorities[i].second → auto [priority, var] = priorities[i];
• Makes priority-based variable ordering more readable
• Note: This is within #if 0 block but still valuable for future use

2. solver::check_model() - Binary clause validation (1 site - debug code)

• Lines 2154-2156: Changed p.first/p.second → auto [l1, l2] = ...
• Eliminates intermediate p variable
• Makes binary clause checking more direct
• Note: Within #if 0 block for debugging

3. solver::user_scope::extract_big() - Big clause extraction (1 site)

• Lines 4182-4184: Changed b.first/b.second → auto [l1, l2] = ...
• Eliminates intermediate variable declarations (l1, l2)
• Makes binary clause processing cleaner

Benefits

1. Improved Readability: Meaningful names (priority/var, l1/l2) instead of .first/.second
2. Code Simplification: Eliminates intermediate variable declarations in loops
3. Clearer Intent: Binary clause structure is explicit through named literals
4. Type Safety: Structured bindings provide compile-time type checking
5. Consistency: Aligns with modern C++17 idioms used throughout Z3

Semantic Context

The pairs represent different SAT solver concepts:

• Priority pairs (priority, var): Variable priority scores paired with variable IDs for ordering
• Binary clauses (l1, l2): Two literals forming a binary clause constraint

The refactoring makes these relationships clearer, especially for binary clause processing where l1/l2 naming is standard SAT solver convention.

Code Change Summary

• Lines changed: 11 lines across 3 functions
• Net impact: -2 lines (code simplification in extract_big)
• Intermediate variables eliminated: 2 (l1, l2 declarations in extract_big)
• Member accesses eliminated: 6 (.first/.second replaced with structured bindings)

Testing

• No functional changes to the SAT solver logic
• Existing unit tests for SAT solving should pass unchanged
• The refactoring is semantically equivalent to the original code
• Two refactorings are in debug/commented code (#if 0) so no runtime impact

Related Work

This continues the structured bindings modernization effort in Z3:

• Consistent with previous refactorings in SAT, SMT, and AST subsystems
• Part of ongoing C++17/C++20 adoption across the codebase
• Follows the naming convention of using semantically meaningful names for structured bindings
• Particularly relevant for binary clause patterns used throughout the SAT solver
• Complements previous SAT refactorings (bin_clause, wliteral, var_pos patterns)

AI generated by Code Conventions Analyzer