mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-29 13:28:44 +00:00
Code Activity

Refactor bound_manager to use C++17 structured bindings (#8404)

Browse source 
* Initial plan

* Refactor bound_manager to use C++17 structured bindings

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-27 20:04:01 -08:00 • committed by GitHub
parent 7747a17bb7
commit 560985893e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/simplifiers/bound_manager.cpp
View file

@ -155,7 +155,8 @@ void bound_manager::operator()(expr * f, expr_dependency * d, proof* p) {
void bound_manager::insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d) {
limit old;
if (m_uppers.find(v, old)) {
if (n < old.first || (n == old.first && strict && !old.second)) {
auto [old_bound, old_strict] = old;
if (n < old_bound || (n == old_bound && strict && !old_strict)) {
// improved bound
m_uppers.insert(v, limit(n, strict));
if (d)
@ -175,7 +176,8 @@ void bound_manager::insert_upper(expr * v, bool strict, numeral const & n, expr_
void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d) {
limit old;
if (m_lowers.find(v, old)) {
if (n > old.first || (n == old.first && strict && !old.second)) {
auto [old_bound, old_strict] = old;
if (n > old_bound || (n == old_bound && strict && !old_strict)) {
// improved bound
m_lowers.insert(v, limit(n, strict));
if (d)