Refactor bound_manager to use C++17 structured bindings

[Copilot]

Replaces .first/.second member access with structured bindings in bound comparison logic.

Changes

src/ast/simplifiers/bound_manager.cpp

Refactored insert_upper() and insert_lower() to use structured bindings for limit pairs:

// Before
if (n < old.first || (n == old.first && strict && !old.second)) {
    // ...
}

// After
auto [old_bound, old_strict] = old;
if (n < old_bound || (n == old_bound && strict && !old_strict)) {
    // ...
}

The limit type is std::pair<numeral, bool> representing bound value and strictness flag. Variable names now self-document the comparison semantics:

• Upper bound: accept if new bound is smaller or equal-but-stricter
• Lower bound: accept if new bound is larger or equal-but-stricter

Scope limited to these two functions where complex boolean logic benefits most from descriptive names. Simple assignments elsewhere remain unchanged.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Refactor bound_manager to use structured bindings for limit pairs</issue_title>
<issue_description>This refactoring modernizes the bound manager to use C++17 structured bindings instead of accessing .first and .second members of limit pairs.

Changes

File: src/ast/simplifiers/bound_manager.cpp

Scope: Refactoring of bound comparison logic for upper and lower bounds

Sites refactored: 4 member accesses across 2 functions

Type: limit (alias for std::pair(numeral, bool) - bound value + strictness flag)

Naming: [old_bound, old_strict] - clear semantics for bound value and strictness

Functions Modified

1. bound_manager::insert_upper() - Upper bound insertion

• Line 158: Changed comparison from old.first and old.second to structured bindings
• Added: auto [old_bound, old_strict] = old;
• Replaced: old.first → old_bound, old.second → old_strict

2. bound_manager::insert_lower() - Lower bound insertion

• Line 178: Changed comparison from old.first and old.second to structured bindings
• Added: auto [old_bound, old_strict] = old;
• Replaced: old.first → old_bound, old.second → old_strict

Benefits

1. Improved Readability: Variable names old_bound and old_strict are much more descriptive than old.first and old.second
2. Self-Documenting: The meaning of the pair components is immediately clear
3. Clearer Logic: The bound comparison expressions are easier to understand with meaningful names
4. Type Safety: Structured bindings provide compile-time type checking
5. Consistency: Aligns with modern C++17 idioms used throughout Z3

Semantic Context

The limit type represents a bound constraint:

• Bound value (old_bound): The numeric limit (rational number)
• Strictness flag (old_strict): Whether the bound is strict (< or >) vs non-strict (≤ or ≥)

The comparison logic checks if a new bound improves the existing bound:

• For upper bounds: New bound is better if it's smaller, or equal but stricter
• For lower bounds: New bound is better if it's larger, or equal but stricter

The refactoring makes this logic much clearer through descriptive variable names.

Code Change Summary

• Lines changed: 8 lines (4 in each function)
• Net impact: +2 lines (added structured binding declarations)
• Member accesses eliminated: 4 (.first/.second replaced with named variables)
• Readability improvement: Significant - complex boolean expressions now self-explanatory

Testing

• No functional changes to the bound management logic
• Existing unit tests for bound manager should pass unchanged
• The refactoring is semantically equivalent to the original code

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 valuable for improving readability of complex comparison logic

AI generated by Code Conventions Analyzer

Comments on the Issue (you are @copilot in this section)

Custom agent used: agentic-workflows
GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing

• Fixes [Conventions] Refactor bound_manager to use structured bindings for limit pairs #8394

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.