Maximizing a real objective under a strict inequality (e.g. `maximize r`
subject to `r < 1`) must yield the strict supremum `1 - epsilon`, but z3
was reporting a plain feasible model value (`0`).
Regression from commit fdc32d0e6 ("Fix inconsistent optimization result
with unvalidated LP bound", #10028), which stopped committing the LP
optimization hint to m_objective_values up front and instead defers the
commit until check_bound() validates it. That fix targets plain-rational
over-estimates produced by shared uninterpreted symbols (e.g. large
`distinct` encodings), which have a zero infinitesimal.
For a strict real supremum/infimum the hint has a non-zero infinitesimal
(`1 - epsilon`). check_bound() can never validate it because
opt_solver::mk_ge drops the negative infinitesimal, turning the bound
`r >= 1 - epsilon` into the unsatisfiable `r >= 1`. Validation therefore
fails, maximize_objective() returns false, and m_objective_values is left
holding the strictly smaller current model value, which callers such as
optsmt::geometric_lex report as the optimum.
Restore the pre-#10028 eager commit, scoped to finite values with a
non-zero infinitesimal. Such values are strict optima that no concrete
model can attain and that check_bound() cannot validate, so the arithmetic
hint is authoritative. Plain-rational (zero-infinitesimal) values,
including all integer objectives and the #10028 shared-symbol case, are
untouched and continue through the deferred-commit validation path.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Small readability refactor in `opt_solver`, no behavioral change.
## Rename
- `m_models` → `m_objective_models`
- `m_last_model` → `m_model`
## Rationale
`m_models` is the per-objective vector of witnessing models, indexed by
the objective index `i` exactly like `m_objective_vars`,
`m_objective_values`, and `m_objective_terms`. It was the only member of
that parallel family not following the `m_objective_*` naming, so
`m_objective_models` makes the intent self-documenting.
`m_last_model` is the single, transient model most recently obtained
from the context and handed back to callers via `get_model_core`.
Renaming it to `m_model` reads more naturally, and the two now-distinct
names (`m_model` vs `m_objective_models`) avoid the previous one-letter
`m_model`/`m_models` clash hazard.
Both are private members of `opt_solver`, so the change is fully
self-contained within `opt_solver.{h,cpp}`. A stale TRACE label ("last
model") was updated to "current model" to match.
## Testing
- Builds clean (CMake/Ninja, Release).
- `test-z3 /a`: 92 passed, 0 failed.
- Spot-checked optimization behavior (single-objective minimize with
large `distinct`, box mode) — unchanged.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fixes#10028.
## Problem
Minimizing an integer variable over a problem containing a large
`distinct` constraint returned an **inconsistent** result: the reported
optimum did not match the returned model, and it was not the true
optimum.
Reproducer from the issue (a Golomb-ruler problem, true optimum = 55):
```python
import z3
n, U = 10, 500
x = [z3.Int(f"x{i}") for i in range(n)]
o = z3.Optimize()
for xi in x: o.add(xi >= 0, xi <= U)
o.add(x[0] == 0)
for i in range(n - 1): o.add(x[i] < x[i + 1])
o.add(z3.Distinct([x[j] - x[i] for i in range(n) for j in range(i + 1, n)]))
h = o.minimize(x[n - 1])
print(o.check(), o.lower(h), o.upper(h), o.model()[x[n - 1]])
# sat 20 20 500 <-- objective 20, but model has x9 = 500 (and 20 is unsat)
```
## Root cause
A `distinct` with more than 32 arguments is encoded with a fresh
uninterpreted sort and function (`smt_internalizer.cpp`), so the
objective variable becomes a *shared symbol* whose feasible values
depend on EUF as well as arithmetic. The arithmetic relaxation therefore
only produces a **hint** for the optimum, which may over-estimate it and
be unachievable.
Two combined defects:
- `opt_solver::maximize_objective` committed the hint into
`m_objective_values` **before** validating it with `check_bound`, and
never rolled it back when validation failed. `update_objective` only
ever *raises* the stored value, so the real (achievable) model value was
discarded.
- `optsmt::geometric_lex` **ignored** the boolean return value and
asserted the blocker derived from the unachievable hint, so the very
next `check_sat` was UNSAT and the search terminated prematurely,
reporting the bogus bound together with a non-matching model.
## Fix
- `opt_solver.cpp`: do not commit the hint before it is validated. On
validation failure, `update_objective` now records the actual achievable
model value. The no-model early-return keeps its previous behavior.
- `optsmt.cpp`: `geometric_lex` now honors the validation result. When
the hint could not be validated, it discards the poisoned blocker and
tightens from the real model value, so the search keeps converging
toward the true optimum. When the hint is valid, the condition reduces
to the original expression and behavior is unchanged.
After the fix the same reproducer produces consistent,
monotonically-improving bounds (325 → 85 → … → 58 → … → 55), and the
reported objective always matches the returned model.
## Testing
Exact-optimum, fast-terminating checks (all correct): EUF-forced minimum
(= 5), `distinct(x, 0..32)` minimize (= 33), Golomb n=8 (= 34), plus
basic min/max, real objective, box, lex, pareto, and weighted
soft/maxsat.
Regression suites, rebuilt in **both Release and Debug**:
| Suite | Release | Debug |
|-------|---------|-------|
| `test-z3 /a` | 92 passed, 0 failed | 92 passed, 0 failed |
| z3test `regressions/smt2` (908 files, `model_validate=true`) | 0
failures | 0 failures |
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Push/pop isolation in maximize_objectives1 (added for #7677) can corrupt
LP column values between objectives. For non-linear objectives like mod,
the LP maximize call may return stale values after a preceding
objective's push/pop cycle.
Fix: save the baseline model before the push/pop loop and use it as a
floor for each objective's value. Extract two helpers:
- maximize_objective_isolated: push/pop + save/restore per objective
- update_from_baseline_model: adopt baseline model value when it is better
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* preserve the initial state of the solver with push/pop for multiple objectives
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Fix memory corruption in Z3_polynomial_subresultants
The API function had a memory corruption bug where allocating the result
vector while the default_expr2polynomial converter was still in scope
could corrupt the converter's internal expr2var mapping.
Fixed by restructuring the code to:
1. Complete all polynomial computation in a scoped block
2. Store results in a temporary expr_ref_vector
3. Let the converter go out of scope
4. Then allocate and populate the result vector
Also improved the test to:
- Use randomized testing with 20 iterations
- Test both cases: variable in polynomials and variable not in polynomials
- Use proper reference counting (inc_ref before dec_ref)
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663).
underlying issue is that model updates for multi-objective and single objective solving are too brittle to serve its use cases among different plugins.
For maxlex, the last model is always the best and it doesn't use multiple objectives.
