[Conventions] Refactor SAT components to use structured bindings for literal and expression pairs

[github-actions]

This PR refactors SAT solver components to use C++17 structured bindings for literal and expression pairs, improving code readability and eliminating .first/.second access patterns.

Changes

File 1: src/sat/sat_probing.cpp

probing::operator() (lines 279-290)

• Refactored literal equivalence processing
• Type: std::pair(literal, literal) (pair of SAT literals)
• Naming: [l1, l2] for literal pairs
• Context: Union-find merging of equivalent literals
• Impact: Eliminates intermediate variables and 2 .first/.second accesses

Before:

for (auto const& p : m_equivs) {
    literal l1 = p.first, l2 = p.second;
    uf.merge(l1.index(), l2.index());
    uf.merge((~l1).index(), (~l2).index());
}

After:

for (auto const& [l1, l2] : m_equivs) {
    uf.merge(l1.index(), l2.index());
    uf.merge((~l1).index(), (~l2).index());
}

File 2: src/sat/sat_bcd.cpp

bcd::operator() (lines 84-92)

• Refactored binary clause collection and registration
• Type: Binary clause pair (pair of literals)
• Naming: [l1, l2] for literal pair
• Context: Collecting and creating binary clauses from solver
• Impact: Eliminates intermediate variable and 2 .first/.second accesses

Before:

for (auto b : bc) {
    literal lits[2] = { b.first, b.second };
    clause* cls = s.cls_allocator().mk_clause(2, lits, false);
    // ... register clause
}

After:

for (auto [l1, l2] : bc) {
    literal lits[2] = { l1, l2 };
    clause* cls = s.cls_allocator().mk_clause(2, lits, false);
    // ... register clause
}

File 3: src/sat/smt/user_solver.cpp

solver::add_assumptions() (lines 280-284)

• Refactored equality antecedent addition
• Type: std::pair(expr*, expr*) (pair of expressions)
• Naming: [e1, e2] for expression pairs
• Context: Adding equality assumptions to SMT context
• Impact: Eliminates 1 intermediate variable and 2 .first/.second accesses

solver::validate_propagation() (lines 290-297)

• Refactored equality validation in debug mode
• Type: std::pair(expr*, expr*) (pair of expressions)
• Naming: [e1, e2] for expression pairs
• Context: Verifying propagated equalities have same root
• Impact: Eliminates 1 intermediate variable and 2 .first/.second accesses

solver::display_justification() (lines 305-313)

• Refactored justification display
• Type: std::pair(expr*, expr*) (pair of expressions)
• Naming: [e1, e2] for expression pairs
• Context: Pretty-printing equality justifications
• Impact: Eliminates 1 intermediate variable and 2 .first/.second accesses

Total Impact

• 5 locations refactored across 3 files
• 12+ member accesses eliminated (.first, .second)
• 4 intermediate variables eliminated (p, b in loops, local p extractions)
• 3 subsystems: SAT probing, SAT BCD, SAT-based SMT solver

Benefits

1. Readability: Clear variable names (l1/l2 for literals, e1/e2 for expressions)
2. Consistency: Uniform pattern across SAT and SMT bridge code
3. Less Verbose: Eliminates intermediate variable declarations
4. Modern C++: Leverages C++17 structured bindings
5. Self-Documenting: Variable names indicate literal or expression pairs

Examples by Context

Literal Pairs (SAT)

// Before: Generic pair access
for (auto const& p : m_equivs) {
    literal l1 = p.first, l2 = p.second;
    process(l1, l2);
}

// After: Direct structured binding
for (auto const& [l1, l2] : m_equivs) {
    process(l1, l2);
}

Expression Pairs (SMT)

// Before: Member access
for (auto const& p : prop.m_eqs) {
    ctx.add_eq_antecedent(probing, expr2enode(p.first), expr2enode(p.second));
}

// After: Clear component names
for (auto const& [e1, e2] : prop.m_eqs) {
    ctx.add_eq_antecedent(probing, expr2enode(e1), expr2enode(e2));
}

Testing

• No functional changes to SAT or SMT logic
• All pair accesses replaced with equivalent structured bindings
• Probing, BCD, and user solver behavior unchanged
• Debug validation paths maintained

Notes

• Part of ongoing C++17 modernization effort
• Naming convention: [l1, l2] for literals, [e1, e2] for expressions
• Applied to both production and debug code (VERIFY macros)

AI generated by Code Conventions Analyzer