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>
Same as test_bnh_optimize but constructs f1 and f2 with reversed
parameter order in mk_add, mk_mul, mk_sub calls. Exposes optimizer
sensitivity to expression structure.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
**Root cause**: `vector::resize(SZ s, Args args...)` in `src/util/vector.h` took `args` by value and used `std::forward<Args>(args)` in a loop. The first iteration moved from `args`, leaving all subsequent elements with a moved-from state (`rational{0/0}` instead of
`rational{0/1}`). This corrupted the coefficient vector in the pretty printer, causing a division-by-zero assertion when multiplying.
**Fix**: Changed `resize` to take `Args const& args` and copy-construct each element instead of forwarding/moving.
Each step in every SKILL.md now carries labeled Action, Expectation,
and Result blocks so the agent can mechanically execute, verify, and
branch at each stage. Format chosen after comparing three variants
(indented blocks, inline keywords, tables) on a prove-validity
simulation; indented blocks scored highest on routing completeness
and checkability.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Introduce .github/skills/ with solve, prove, optimize, simplify,
encode, explain, benchmark, memory-safety, static-analysis, and
deeptest skills. Each skill follows a SKILL.md + scripts/ pattern
with Python scripts backed by a shared SQLite logging library
(z3db.py). Two orchestrator agents (z3-solver, z3-verifier) route
requests to the appropriate skills.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add ENSURE(result == Z3_L_TRUE) for each BNH optimization call and
ENSURE(num_sat == 7) at the end so CI catches regressions.
- Remove test_bnh_optimize() from tst_api() to avoid duplicate
execution under /a; keep standalone tst_bnh_opt() entry point.
- Fix Test 2 comment: it tests same-size backup, not backup-longer.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Relax restore_x() to handle backup/current size mismatches: when
backup is shorter (new columns added), call
move_non_basic_columns_to_bounds() to find a feasible solution.
- Fix 100x performance regression in nonlinear optimization: save LP
optimum before check_nla and return it as bound regardless of NLA
result, so opt_solver::check_bound() can validate via full re-solve
with accumulated NLA lemmas.
- Refactor theory_lra::maximize() into three helpers: max_with_lp(),
max_with_nl(), and max_result().
- Add mk_gt(theory_var, impq const&) overload for building blockers
from saved LP optimum values.
- Add BNH multi-objective optimization test (7/7 sat in <1s vs 1/7
in 30s before fix).
- Add restore_x test for backup size mismatch handling.
Fixes#8890
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
