[Conventions] Refactor theory_bv to use structured bindings for disequality watch pairs

[github-actions]

This PR refactors bit-vector theory to use C++17 structured bindings for disequality watch pairs, improving code clarity in propagation logic.

Changes

File: src/smt/theory_bv.cpp

Location Refactored

theory_bv::propagate_bv2int() (lines 1258-1265)

• Refactored disequality watch propagation loop
• Type: Pair of expressions (disequality watch pair)
• Naming: [e1, e2] for expression pair
• Context: Processing watched disequalities after bit-vector to integer propagation
• Impact: Eliminates intermediate variable p and 2 .first/.second accesses

Details

The disequality watch mechanism tracks pairs of expressions that need to be expanded when certain variables are assigned. This refactoring makes the loop more readable by directly naming the two expressions being watched.

Before

if (params().m_bv_watch_diseq && !ctx.inconsistent() && 
    m_diseq_watch.size() > static_cast(unsigned)(v)) {
    unsigned sz = m_diseq_watch[v].size();
    for (unsigned i = 0; i < sz; ++i) {
        auto const & p = m_diseq_watch[v][i];
        expand_diseq(p.first, p.second);
    }
    m_diseq_watch[v].reset();
}

After

if (params().m_bv_watch_diseq && !ctx.inconsistent() && 
    m_diseq_watch.size() > static_cast(unsigned)(v)) {
    unsigned sz = m_diseq_watch[v].size();
    for (unsigned i = 0; i < sz; ++i) {
        auto const & [e1, e2] = m_diseq_watch[v][i];
        expand_diseq(e1, e2);
    }
    m_diseq_watch[v].reset();
}

Benefits

1. Clarity: [e1, e2] clearly shows we're dealing with two expressions
2. Less Verbose: Eliminates intermediate variable p
3. Self-Documenting: The structured binding makes the pair nature explicit
4. Modern C++: Uses C++17 structured bindings idiom
5. Consistency: Matches patterns in other SMT theories (array theory, etc.)

Context

The bit-vector theory maintains "disequality watches" - pairs of expressions that must be checked for disequality when certain variables are assigned. When a bit-vector variable v gets a value during propagation:

1. Look up all watched disequality pairs for v
2. For each pair (e1, e2), call expand_diseq(e1, e2)
3. Clear the watch list for v

This refactoring makes step 2 more readable by eliminating the generic p variable and directly naming the two expressions.

Impact

• 1 location refactored
• 2 member accesses eliminated (.first, .second)
• 1 intermediate variable eliminated (p)
• Module: SMT bit-vector theory

Testing

• No functional changes to bit-vector propagation
• Disequality watch behavior unchanged
• Parameter-gated code path (enabled by m_bv_watch_diseq)

Notes

• Part of ongoing C++17 modernization effort
• Follows SMT theory naming: [e1, e2] for expression pairs
• Applied to parameter-conditional code path (watch-based diseq handling)

AI generated by Code Conventions Analyzer