mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-27 12:28:43 +00:00
Code Activity

Refactor arith_rewriter::find_nl_factor() to use std::optional (#8313)

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-23 19:16:27 -08:00 • committed by GitHub
parent 1d022fa591
commit c2d996574f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/arith_rewriter.cpp
View file

@ -591,7 +591,7 @@ void arith_rewriter::get_nl_muls(expr* t, ptr_buffer<expr>& muls) {
muls.push_back(t);
}
expr* arith_rewriter::find_nl_factor(expr* t) {
std::optional<expr*> arith_rewriter::find_nl_factor(expr* t) {
ptr_buffer<expr> 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));

3
src/ast/rewriter/arith_rewriter.h
View file

@ -18,6 +18,7 @@ Notes:
--*/
#pragma once
#include <optional>
#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<arith_rewriter_core> {
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<expr*> find_nl_factor(expr* t);
void get_nl_muls(expr* t, ptr_buffer<expr>& 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);