PR #10180 moved nonlinear bound propagation to final_check only, removing
the eager propagate_nla() from the search-time propagation path. This left
E-matching without nla-implied bound facts during search, causing an
instantiation blowup on number-theory goals (e.g. FStar.Math.Euclid),
which exhausted rlimit and returned unknown on queries previously proved.
Re-run propagate_nla() before propagate_bounds_with_lp_solver() in the
l_true case of propagate_core so tightened nonlinear bounds are surfaced
to the SMT core during search. Recovers FStar.Math.Euclid-1/-2.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
With `(set-option :smtlib2_compliant true)`, Z3 disables implicit
Int→Real coercions. When the LP solver generates Gomory cuts/bounds over
expressions that mix Int and Real LP variables (as happens when
`to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int
are registered as LP vars), `coeffs2app` was constructing
`mk_mul(Real_numeral, Int_expr)`. Without implicit coercions,
`check_args` throws an `ast_exception` that bubbles up through
`cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown`
instead of `unsat`.
## Changes
- **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each
product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int &&
a.is_int(o)`. This makes the sort explicit rather than relying on
implicit coercions.
- **`src/test/smt2print_parse.cpp`**: Regression test for the exact
formula from the issue — verifies the result is `unsat` (not `unknown`)
when `smtlib2_compliant` is set.
```smt2
(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))
; ... mixed Int/Real via to_real ...
(check-sat)
; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int")
; now: unsat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10166
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
…icts
Add core::optimize_nl_bounds() (gated by arith.nl.optimize_bounds) which
runs LP max/min over monomial leaf variables inside core::propagate(),
analogous to solver=2's max_min_nl_vars, so nla (arith.solver=6) can
detect cross-nested conflicts previously missed. Collect improved bounds
first, then apply them and re-establish feasibility once; reconcile the
core solver via find_feasible_solution before the raw maximize solves to
preserve inf_heap_is_correct(). Skip null witnesses in
get_dependencies_of_maximum for implied/unconditional bounds.
On FStar-UInt128-divergence solver=6 this yields unsat in 2
final-checks, seed-insensitive (seeds 1-10).
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ac36bb84-de91-4e6c-86df-6008c7396ceb
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca),
theory_lra previously discovered the implied equality x = y only lazily via
assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065
this discovery is starved by E-matching, which unfolds the recursion and
bit-blasts an exploding FP subproblem before the branch closes.
Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite
unit-scaled coefficients and propagate the operand equality x = y directly to the
core, so congruence closure merges dependent terms immediately. This mirrors the
offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches
its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
Implement check_mod_congruence in nla_divisions: for two mod-atoms
sharing a (possibly symbolic) divisor y, emit the model-guided tautology
div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y.
This discharges linear congruences over a symbolic modulus that the
nonlinear core did not otherwise isolate. Thread the div(x,y) variable
through add_divisibility (nla_core/nla_solver/nla_divisions) and
register it in theory_lra for symbolic-divisor mod terms.
Solves FStar.BitVector-1 (0.7s) and FStar.Matrix-1 (1.6s), previously
300s timeouts; all 92 unit tests pass.
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the divergence in issue #7464: formulas involving `mod`/`div` by a
**variable** divisor could send `smt.arith.solver=6` into a
non-terminating nonlinear search.
Minimal reproducer (UNSAT, previously timed out; now solved in <0.5s):
```smt2
(declare-fun V () Int)
(declare-fun n () Int)
(declare-fun l () Int)
(assert (and (> V 0) (= 0 (mod n 2)) (= (div n 2) (div n l)) (= 0 (mod (div n l) V))))
(assert (distinct 0 (mod n V)))
(check-sat)
```
## Root cause
A variable-divisor `mod n V` is axiomatized by the Euclidean identity
`n = V*(n div V) + (n mod V)`. The `V*(n div V)` term is nonlinear, so
arith.solver=6
hands the problem to the nlsat/Gröbner branch, which branches on values
of `V` with no
termination bound and diverges.
## Fix
Add a **linear divisibility closure** lemma in `nla_divisions`:
> `mod(a, y) = 0 & x = c*a` (c an integer constant) ⟹ `mod(x, y) = 0`.
The emitted clause
```
(x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0)
```
is a **tautology for every integer `c`**, so mining a candidate `c =
val(x)/val(a)` from
the current model can never be unsound. It is only emitted when all
three literals are
false in the current model, so the clause is a genuine
conflict/propagation and always
makes progress. This lets the theory refute the instance directly
instead of entering the
divergent nonlinear branch.
Variable-divisor `mod` terms were previously **not registered** in nla
at all; they are now
registered into a new `m_divisibility` list in `theory_lra`, so the
reasoner can pair a
violated `mod(x, y)` with a satisfied `mod(a, y)` of the same divisor.
## Changes
- `src/math/lp/nla_divisions.{h,cpp}` — new `m_divisibility` list
`{r=mod, x=dividend, y=divisor}`, `add_divisibility(...)`, and
`check_linear_divisibility()`; invoked from `divisions::check()`.
- `src/math/lp/nla_core.h`, `src/math/lp/nla_solver.{h,cpp}` —
forwarding of `add_divisibility`.
- `src/smt/theory_lra.cpp` — register variable-divisor `mod` into the
divisibility list.
## Validation
- `min.smt2` → `unsat` in 0.46s, minimized core → 0.15s (were timeouts).
- Soundness: 350 differential fuzz formulas (arith.solver=6 vs
arith.solver=2), **0 mismatches**.
- Spot checks correct (divisor-3 variant → unsat; non-divisible variants
→ sat).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Problem
Maximizing/minimizing under a **strict** inequality has a delta-rational
optimum. For
```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```
the optimum is the supremum `1 - epsilon`, but z3 reported `r = 0`.
The same defect makes shared-symbol objectives report a value matching
**neither the model nor the true optimum** (issue #10028 follow-up).
Minimal reproducer — a 6-mark Golomb ruler (a `>32`-arg `distinct`, so
the objective is coupled to EUF) with a strict real objective `obj >
x5`, whose true optimum is `17 + epsilon`:
| case | before | after |
|---|---|---|
| `maximize r`, `r < 1` | `0` ❌ | `1 - epsilon` ✅ |
| `minimize r`, `r > 1` | `0` ❌ | `1 + epsilon` ✅ |
| Golomb `minimize obj`, `obj > x5` | `35/2` / `7+eps` ❌ | `17 +
epsilon` ✅ |
## Root cause
`check_bound` validates the LP hint by asserting `objective >= optimum`.
For a supremum `1 - epsilon` this is a **lower** bound whose value
carries a **negative** infinitesimal `(1, -1)`.
No `lconstraint_kind` can express that. The kind->infinitesimal map only
yields the *matching-sign* cases — `GT` -> lower `(r, +1)`, `LT` ->
upper `(r, -1)` — or zero (`GE`/`LE`). The opposite-sign lower bound
`(r, -1)` (i.e. `r >= r0 - delta`) is a *relaxation* that no strict
inequality produces. `opt_solver::mk_ge` therefore projected the
`-epsilon` away, turning `r >= 1 - epsilon` into the over-strong,
unsatisfiable `r >= 1`; validation failed and the strictly smaller
current model value was reported instead.
## Fix — carry the infinitesimal faithfully through the bound pipeline
- **`lp_api::bound`** gains an `eps` component so `get_value` returns
the true delta value (no spurious rational fixed-variable equality is
propagated to EUF).
- **`lar_base_constraint`** stores its right-hand side as a
delta-rational `impq` pair; `rhs()` returns the rational component,
`bound_eps()` the infinitesimal one.
- **`lar_solver`** bound activation/update threads the whole `impq`
bound, so a lower bound `(r, -1)` can be asserted. `constraint_holds`
accounts for it using the **same** strict-bounds delta that flattens the
model, computed **once per model**.
- **`theory_lra::mk_ge`** builds a *fresh* predicate for the `(r, -1)`
lower bound (to avoid colliding with an already-internalized `v >= r`
literal) and attaches `eps = -1`. **`opt_solver::mk_ge`** passes the
unprojected value to `theory_lra` / `theory_mi_arith` /
`theory_inf_arith` (whose bounds are already `inf_rational`).
The pair machinery is what makes the supremum both representable
(optimum `1 - epsilon`) and validatable; the reported witness model
remains the flattened rational (`find_delta_for_strict_bounds`),
consistent with the existing epsilon semantics.
## Validation
- Strict optima correct: `1-eps`, `1+eps`, bounded `2<r<5 -> 5-eps`, and
lex/box variants.
- Integer optima and the #10028 shared-symbol cases unchanged (Golomb
n=6/7/8 -> 17/25/34, consistent with the model).
- Unit tests **92/92** (release); no new debug-suite failures.
- Opt regression corpus (73 files, `model_validate=true`)
**byte-identical** to baseline.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Two TRACE blocks under the existing nla_solver tag:
1. theory_lra::false_case_of_check_nla emits a "varmap:" line for each
NLA lemma, listing j-var → SMT-name mappings for variables in the
lemma's collect_vars set. Lets lemur nla resolve the LP-internal
j-numbering back to the original SMT term names when displaying
lemmas. Without this, lemma-level analysis has to either guess at
variable identities (and j-numbers are reused across nlsat
invocations under backtracking — see j-vars-unstable note) or use a
different trace tag entirely (-tr:nra) for stable algebraic-number
IDs.
2. nla_grobner emits a "grobner-linear-eq:" line at each call to
add_term + update_column_type_and_bound that produces a Linear
Propagation row from completion. Lets us count Gröbner's effective
contribution to the LP tableau independently of the lemma stream.
Useful when investigating Gröbner-deficit hypotheses in NLA cascade
diagnosis.
Both are pure trace emission, behind TRACE(nla_solver, ...). Zero
runtime cost when tracing is off; no semantic change.
The is_mod handler in theory_lra called ensure_nla(), which
unnecessarily created the NLA solver for pure linear problems, causing
the optimizer to return a finite value instead of -infinity.
Fix: check `m_nla` instead of calling `ensure_nla()`, matching the
pattern used by the is_idiv handler. The mod division is only registered
when NLA is already active due to nonlinear terms.
Update mod_factor tests to use QF_NIA logic and assert the mul term
before the mod term so that internalize_mul triggers ensure_nla() before
mod internalization.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When a monic x*y has a factor x with mod(x, p) = 0 (fixed), propagate
mod(x*y, p) = 0. This enables Z3 to prove divisibility properties like
x mod p = 0 => (x*y) mod p = 0, which previously timed out even for
p = 2. The lemma fires in the NLA divisions check and allows Gröbner
basis and LIA to subsequently derive distributivity of div over addition.
Extends division tuples from (q, x, y) to (q, x, y, r) to track the
mod lpvar. Also registers bounded divisions from the mod internalization
path in theory_lra, not just the idiv path.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* outline of signature for assignment based conflict generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* outline of interface contract
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove confusing construction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add material in nra-solver to interface
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add marshaling from nlsat lemmas into core solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add call to check-assignment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Nl2lin (#7795)
* add linearized projection in nlsat
* implement nlsat check for given assignment
* add some comments
* fixup loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug nl2lin
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Nl2lin (#7827)
* fix linear projection
* fix linear projection
* use an explicit cell description in check_assignment
* clean up (#7844)
* Simplify no effect checks in nla_core.cpp
Move up linear nlsat call to replace bounded nlsat.
* t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* detangle mess
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove the too early return
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* do not set use_nra_model to true
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add a hook to add new multiplication definitions in nla_core
* add internalization routine that uses macro-expanded polynomial representation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add internalization routine that uses macro-expanded polynomial representation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup backtranslation to not use roots
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* call setup_assignment_solver instead of setup_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug the setup, still not working
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* updated clang format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* create polynomials with integer coefficients, use the hook to create new monomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* integrating changes from master related to work with polynomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add forgotten files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Update nlsat_explain.cpp
Remove a duplicate call
* fix
* move linear cell construction to levelwise
* fix
* fix
* Port throttle and soundness fixes from master
- Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure
- Gracefully handle root atoms in add_lemma
- Throttle check_assignment with failure counter (decrement on success)
- Add arith.nl.nra_check_assignment parameter
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Add arith.nl.nra_check_assignment_max_fail parameter
Replace hardcoded failure threshold with configurable parameter (default 10).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Add cha_abort_on_fail parameter to control failure counter decrement
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* abort nla check_assignment after a set number of allowed failures
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Add missing AST query methods to Java API (#8977)
* add Expr.isGround() to Java API
Expose Z3_is_ground as a public method on Expr. Returns true when the
expression contains no free variables.
* add Expr.isLambda() to Java API
Expose Z3_is_lambda as a public method on Expr. Returns true when the
expression is a lambda quantifier.
* add AST.getDepth() to Java API
Expose Z3_get_depth as a public method on AST. Returns the maximum
number of nodes on any path from root to leaf.
* add ArraySort.getArity() to Java API
Expose Z3_get_array_arity as a public method on ArraySort. Returns
the number of dimensions of a multi-dimensional array sort.
* add DatatypeSort.isRecursive() to Java API
Expose Z3_is_recursive_datatype_sort as a public method on
DatatypeSort. Returns true when the datatype refers to itself.
* add FPExpr.isNumeral() to Java API
Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true
when the expression is a concrete floating-point value.
* add isGroundExample test to JavaExample
Test Expr.isGround() on constants, variables, and compound
expressions.
* add astDepthExample test to JavaExample
Test AST.getDepth() on leaf nodes and nested expressions to verify
the depth computation.
* add arrayArityExample test to JavaExample
Test ArraySort.getArity() on single-domain and multi-domain array
sorts.
* add recursiveDatatypeExample test to JavaExample
Test DatatypeSort.isRecursive() on a recursive list datatype and a
non-recursive pair datatype.
* add fpNumeralExample test to JavaExample
Test FPExpr.isNumeral() on a floating point constant and a symbolic
variable.
* add isLambdaExample test to JavaExample
Test Expr.isLambda() on a lambda expression and a plain variable.
* change the default number of failures in check_assignment to 7
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983)
* Initial plan
* Add missing API functions to Go, Java, C++, and TypeScript bindings
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988)
* Initial plan
* Update qf-s-benchmark: debug build, seq tracing, trace analysis
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* disable linear approximation by default to check the merge
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* set check_assignment to true
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix restore_x by recalulating new column values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix restore_x by recalulating new column values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix a memory leak
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com>
Co-authored-by: Valentin Promies <valentin.promies@rwth-aachen.de>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com>
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@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>
When check_nla returns FC_CONTINUE it means NLA found constraint
violations and added lemmas. The current LP value is a valid lower
bound, so the status should be FEASIBLE, not UNBOUNDED.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
* 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).
