mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

simplify solve_eqs: move early return, replace ternary with if, fix indentation

Browse source 
- 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>
This commit is contained in:
github-actions[bot] 2026-04-12 21:01:41 +00:00 • committed by GitHub
parent 68e528eaf7
commit 717888572a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/solve_eqs.cpp
View file

@ -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;
}

2
src/params/smt_params_helper.pyg
View file

@ -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'),