mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-15 17:49:59 +00:00
Code Activity

Enable som (sum of monomials) in optimizer simplification

Browse source 
The optimizer's simplification pass did not expand products of sums
into sum-of-monomials form. This caused mathematically equivalent
expressions like (5-x)^2 vs (x-5)^2 to simplify into different
internal forms, where the former produced nested multiplies
(+ 5.0 (* -1.0 x)) that led to harder purification constraints
and solver timeouts.

Enabling som=true in the first simplification tactic normalizes
polynomial objectives into canonical monomial form, making the
optimizer robust to operand ordering.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-11 18:28:40 -10:00
parent ce7c7f458e
commit b8d6952e9e
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/opt_context.cpp
View file

@ -948,8 +948,10 @@ namespace opt {
g->assert_expr(fml);
for (expr * a : asms)
g->assert_expr(a, a);
params_ref som_params(m_params);
som_params.set_bool("som", true);
tactic_ref tac0 =
and_then(mk_simplify_tactic(m, m_params),
and_then(mk_simplify_tactic(m, som_params),
mk_propagate_values_tactic(m),
m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
mk_simplify_tactic(m));