From b8d6952e9ee5a4bb401b4c4552763828c1e195e6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 11 Mar 2026 18:28:40 -1000 Subject: [PATCH] Enable som (sum of monomials) in optimizer simplification 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> --- src/opt/opt_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8bfef7f24..0b79f6a31 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -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));