From c2d996574f93d78daaa7b90435a17a67444a019c Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 23 Jan 2026 19:16:27 -0800 Subject: [PATCH] Refactor arith_rewriter::find_nl_factor() to use std::optional (#8313) * Initial plan * Refactor arith_rewriter::find_nl_factor() to use std::optional 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> --- src/ast/rewriter/arith_rewriter.cpp | 11 ++++++----- src/ast/rewriter/arith_rewriter.h | 3 ++- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index f5d25b8c3..228a38f86 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -591,7 +591,7 @@ void arith_rewriter::get_nl_muls(expr* t, ptr_buffer& muls) { muls.push_back(t); } -expr* arith_rewriter::find_nl_factor(expr* t) { +std::optional arith_rewriter::find_nl_factor(expr* t) { ptr_buffer sum, muls; sum.push_back(t); @@ -608,18 +608,19 @@ expr* arith_rewriter::find_nl_factor(expr* t) { if (is_add_factor(m, t)) return m; } - return nullptr; + return std::nullopt; } } - return nullptr; + return std::nullopt; } br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) { if (is_zero(arg2)) { - expr* f = find_nl_factor(arg1); - if (!f) + auto opt_f = find_nl_factor(arg1); + if (!opt_f) return BR_FAILED; + expr* f = *opt_f; expr_ref f2 = remove_factor(f, arg1); expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1)); result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z)); diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index a1aadfa7f..9c1a0aba9 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -18,6 +18,7 @@ Notes: --*/ #pragma once +#include #include "ast/rewriter/poly_rewriter.h" #include "ast/arith_decl_plugin.h" #include "ast/seq_decl_plugin.h" @@ -75,7 +76,7 @@ class arith_rewriter : public poly_rewriter { br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); bool is_add_factor(expr* s, expr* t); bool is_mul_factor(expr* s, expr* t); - expr* find_nl_factor(expr* t); + std::optional find_nl_factor(expr* t); void get_nl_muls(expr* t, ptr_buffer& muls); expr_ref remove_factor(expr* s, expr* t); br_status factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);