From 717888572af49028a4f828f24276a4e46985b45b Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sun, 12 Apr 2026 21:01:41 +0000 Subject: [PATCH] simplify solve_eqs: move early return, replace ternary with if, fix indentation - Move early return before variable declaration in is_linear() for cleaner control flow - Replace 'num_values += expr ? 1 : 0' with idiomatic 'if (expr) ++num_values' - Fix tab/space inconsistency in smt_params_helper.pyg for the newly-added solve_eqs.linear parameter Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/simplifiers/solve_eqs.cpp | 4 ++-- src/params/smt_params_helper.pyg | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 36b61e9a2..eb57070e8 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -317,11 +317,11 @@ namespace euf { } bool solve_eqs::is_linear(expr* t) const { - unsigned num_values = 0; if (!is_app(t)) return false; + unsigned num_values = 0; for (auto arg : *to_app(t)) - num_values += m.is_value(arg) ? 1 : 0; + if (m.is_value(arg)) ++num_values; return num_values <= 1; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index cfa146477..49042e3be 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -21,7 +21,7 @@ def_module_params(module_name='smt', ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'), ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'), ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'), - ('solve_eqs.linear', BOOL, False, 'allow only linear substitutions where a variable is replaced by a term having at most one non-constant argument'), + ('solve_eqs.linear', BOOL, False, 'allow only linear substitutions where a variable is replaced by a term having at most one non-constant argument'), ('propagate_values', BOOL, True, 'pre-processing: propagate values'), ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'), ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),