This simplifies the recent `choice` axiom path in the SMT array solver
for consistency with the SAT-side implementation. The change is purely
structural: align local naming with the quantifier body it represents,
inline a single-use literal, and remove stray whitespace in the array
decl header.
- **Choice axiom cleanup**
- Rename the local implication term in
`theory_array_full::instantiate_choice_axiom` from `ax` to `body`
- Match the naming already used in
`sat/smt/array_axioms.cpp::assert_choice_axiom`
- **Single-use literal inlining**
- Replace the temporary `literal l = mk_literal(q); assert_axiom(l);`
with a direct call
- Reduce noise without changing behavior
- **Header whitespace cleanup**
- Remove trailing whitespace in `src/ast/array_decl_plugin.h`
```c++
expr_ref body(m.mk_implies(px, pc), m);
expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q);
assert_axiom(mk_literal(q));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
- only the internalizer performs closure conversion
- theory_array treats propagation of lambdas similar to stores
- ho_matcher treats top-level flex patterns as first-order
- pattern-inference fix to handle quantifiers (lambdas) in patterns that are computed
A `root-obj`-driven unsat case was exiting with a leaked `mpz_manager`
allocation even though solver output was correct. The leak came from
temporary rational bounds created during algebraic-number comparison and
not released before shutdown.
- **Root cause**
- `algebraic_numbers::compare_core()` materialized interval bounds as
raw `mpq` temporaries.
- Those temporaries could allocate backing `mpz` storage, but their
lifetime was not tied to the manager, so the allocator retained leaked
cells at process exit.
- **Change**
- Replace the raw `mpq` temporaries with `scoped_mpq` in
`/src/math/polynomial/algebraic_numbers.cpp`.
- This keeps the comparison logic unchanged while making temporary bound
conversion use RAII-managed cleanup.
- **Effect**
- `root-obj` comparisons no longer leave `mpz_manager` allocations
behind.
- Solver behavior is unchanged; the fix is limited to temporary numeral
lifetime management.
```c++
- mpq l_a, u_a, l_b, u_b;
+ scoped_mpq l_a(qm()), u_a(qm()), l_b(qm()), u_b(qm());
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change wires SMT-LIB Hilbert choice parsing to a concrete
array-theory operator and ensures both array backends enforce the
expected semantic axiom. Previously, `(choice ((x T)) phi)` parsed as
NYI and had no solver-side instantiation path.
- **Parser: lower `choice_k` into array `OP_CHOICE`**
- `pop_quant_frame(choice_k)` now builds `(choice p)` instead of
throwing.
- Added parser include/use of array utilities to construct the term
directly from the generated lambda predicate.
- **Array decl plugin: add `OP_CHOICE` typing + surface syntax**
- Added declaration support for `choice` with signature:
- `(Array T Bool) -> T` (encoded as `('a -> Bool) -> 'a` in HO view).
- Added recognizer/util helpers (`is_choice`, `mk_choice`) and exposed
`"choice"` in op names.
- **SMT array theory (`theory_array_full`): instantiate choice axiom**
- Added instantiation for each encountered `choice(p)`:
- `forall x . p(x) => p(choice(p))`
- Integrated into internalization/relevancy paths and statistics.
- **SAT/SMT array backend (`sat/smt/array_*`): instantiate choice
axiom**
- Added new axiom record kind for choice, internalization hook,
assertion routine, and diagnostics/stat tracking.
- Uses the same quantified implication schema as above.
- **Regression coverage**
- Extended SMT2 parser regression with an HO `choice` example to ensure
parser/eval pipeline accepts and processes choice terms.
Example of the now-supported input:
```smt2
(set-logic HO_ALL)
(declare-sort U 0)
(declare-fun P () (-> U Bool))
(assert (exists ((x U)) (P x)))
(assert (= witness (choice ((x U)) (P x))))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates a formatting regression introduced in the `pop_app_frame`
non-`expr_head` path, where block indentation made control flow harder
to read. The patch is whitespace-only and keeps parser behavior
unchanged.
- **What changed**
- Reindented the `else` body in
`src/parsers/smt2/smt2parser.cpp::pop_app_frame` so nested `if/else`
structure is visually unambiguous.
- Removed trailing spaces on the `m_ctx.mk_app(symbol("select"), ...)`
lines in the same block.
- **Scope**
- No control-flow, data-flow, or API changes.
- No changes outside `pop_app_frame`.
```cpp
// Before
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
// After
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
So far, `algebraic_numbers compare_core ` handles an edge case
incorrectly:
- If the two compared numbers (`a`, `b`) are different,
- the intervals still overlap after refinements, and
- both a and b are a root of the second polynomial (`cell_b->m_p`), e.g.
they are the first and second root
then the method would return `sign_zero` (i.e. "equal"). This behavior
can be replicated with the provided test case (before the fix). This
requires `algebraic.factor=false`, though i first encountered it during
solver runs on QF_NRA instances with the default
`algebraic.factor=true`, which apparently means that the polynomials for
anums are still not always factored.
The fix is to compare the interval bounds of b to a and vice versa. Then
the Sturm-Tarski check is only run if `a` and `b` both lie in the
intersection of the intervals, because only then is it guaranteed to be
correct.
The SMT2 front-end rejected valid higher-order inputs using `HO_ALL` and
failed on curried applications where the function position is itself an
expression (e.g., `((transfer top) 0)`).
This update adds `HO_ALL` support and makes curried parsing consistently
lower to implicit `select` chains.
- **Logic recognition**
- Treat `HO_ALL` as an `ALL`-class logic in SMT logic classification.
- This unblocks `(set-logic HO_ALL)` in the standard SMT2 command path.
- **Curried application parsing**
- Extend application-frame handling to support parenthesized expression
heads, not only symbol heads.
- When the head is an expression, parse application arguments normally
and construct nested implicit selects:
- `(f a b)` → `(select (select f a) b)`
- Preserve existing behavior for symbol-based applications, qualified
identifiers, and lambda-led forms.
- **Regression coverage**
- Add a focused parser/eval regression using the reported higher-order
case to lock in behavior.
```smt2
(set-logic HO_ALL)
(declare-fun transfer () (-> (-> Int Bool) (-> Int Bool)))
(assert (forall ((P (-> Int Bool))) (=> (P 0) ((transfer P) 0))))
(declare-fun top () (-> Int Bool))
(assert (forall ((x Int)) (top x)))
(assert (not ((transfer top) 0)))
(check-sat)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Adds a new lemma pattern to nla_grobner::propagate_quotients that
derives a modular-residue constraint from polynomial divisibility,
filling a gap between quotient1-5 (model-value-driven case splits) and
the polynomials Grobner actually produces on Skolem-encoded mod
arithmetic.
Pattern
-------
For a polynomial p with all-integer free variables and a linear monomial
c_v * v (single integer var), the pattern computes M = gcd(|c_i/c_v|)
over the other monomials and K = c0/c_v for the constant term. When both
are integers, dividing p by c_v gives
v + M*Q + K = 0 with Q an integer
so v ≡ -K (mod M). The pattern emits the sound disjunctive lemma
(v < 0) ∨ (v ≥ M) ∨ (v = target)
where target = (-K) mod M ∈ [0, M-1]. This encodes "v ∈ target + M·Z" in
a form the LP / SAT layer can refute against current bounds.
Motivation
----------
QF_UFNIA verification benchmarks over fixed-prime modular arithmetic
(e.g. zk applications using the BabyBear prime 2013265921) regularly
produce basis polynomials of the form
-p*v_div + p*(v_a * v_b) - v_mod = 0
where v_mod is the result of (mod (* v_a v_b) p). The polynomial sits in
the Grobner basis but none of quotient1-5 fires: they all require
specific model-value alignments (r_value == 0, |v_value| > |r_value|,
etc.) that don't hold when all variables in scope are similarly sized
integers in [0, p). The proof spins on interval-tightening lemmas
without ever extracting the modular conclusion.
The author of propagate_quotients flagged this gap with the comment
\"other division lemmas are possible\" preceding the fall-through \"no
lemmas found\" CTRACE. This patch supplies one.
Soundness
---------
The lemma is sound regardless of v's LP bounds — the bound-negation
disjuncts (v < 0) and (v ≥ M) make the disjunction unconditionally true
under the polynomial identity, with v = target as the canonical residue
in [0, M-1]. M is derived from the polynomial's coefficient gcd, not
from any LP-side bound.
Validated under smt.arith.validate=true on the mod-factor-propagation
reproducers (PR #9235 follow-up), zk verifier benchmarks, and a broader
QF_UFNIA sample — 50+ files total, zero validate_conflict() assertion
violations.
Performance
-----------
A model-value gate (skip emission when v's current value already
satisfies one of the disjuncts) prevents the pattern from
short-circuiting the propagate_quotients || propagate_gcd_test ||
propagate_eqs || propagate_factorization || propagate_linear_equations
chain with redundant emissions. Without the gate, a single (v, M,
target) triple can re-emit each Grobner round and starve the downstream
propagators — observed in regression testing as thousands of identical
emissions on a small benchmark, turning a sub-second closure into a
timeout.
On six small mod-factor-propagation reproducers, the patch closes four
cases that previously timed out at 30 s (~1 s typical under the
Grobner-ramped config: smt.arith.nl.gr_q=50,
smt.arith.nl.grobner_eqs_growth=50,
smt.arith.nl.grobner_exp_delay=false, smt.arith.nl.grobner_frequency=1).
The two remaining timeouts in that set are attributable to different
gaps (Boolean-disjunction propagation, and the multi-bounded-mod-result
polynomial shape that needs Grobner over Z/pZ), not to mod_residue
itself.
Diagnostics
-----------
TRACE under the existing 'grobner' tag emits one line per lemma
emission, recording v, M, c_v, c0, and target.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
The JS bindings currently assume the wasm can be located via the default
Emscripten path resolution, which can force Deno users into
`--allow-read`. This change lets callers provide a custom wasm load path
through `init(...)`, so Deno can resolve the packaged wasm asset without
filesystem reads.
- **Public init API**
- Extend the JS entrypoints (`node` and `browser`) so `init(...)`
accepts optional Emscripten module overrides.
- Surface a typed `Z3ModuleOverrides` shape with explicit support for
`locateFile(path, prefix)`.
- **Low-level initialization**
- Thread module overrides through the generated low-level wrapper
instead of always calling the Emscripten module factory with no
arguments.
- Keep the default behavior unchanged when no overrides are provided.
- **Docs**
- Document the Deno usage pattern in the published JS README.
- Clarify the `locateFile` signature and show the intended Deno 2.1+
`import.meta.resolve(...)` flow.
- **Focused coverage**
- Add unit tests for `node` and `browser` init to verify module
overrides are forwarded correctly.
Example:
```ts
import { init } from 'npm:z3-solver';
const api = await init({
locateFile: (file, _prefix): string =>
import.meta.resolve(`npm:z3-solver/build/${file}`),
});
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The Windows ARM64 nightly build (`mk_win_dist_cmake.py --arm64-only`)
was failing because the cmake-built `Microsoft.Z3` NuGet package was
produced without any native Windows DLL, causing the downstream dotnet
example build to fail.
## Root causes
- **Wrong DLL path in `Microsoft.Z3.csproj.in`**: Path included
`/$(_DN_CMAKE_CONFIG)/` (e.g., `.../RelWithDebInfo/libz3.dll`), but
`CMakeLists.txt` sets `CMAKE_RUNTIME_OUTPUT_DIRECTORY =
PROJECT_BINARY_DIR` with no config subdir. With Ninja single-config, the
DLL lands at `build-dir/libz3.dll`. The `Exists()` guard silently
excluded the DLL from the package.
- **Wrong runtime identifier**: ARM64 DLL was being packed under
`runtimes\win-x64\native` instead of `runtimes\win-arm64\native`.
- **Legacy copy fires for `net8.0`**: `Microsoft.Z3.targets` excluded
`netstandard`/`netcoreapp` but not modern TFMs like `net8.0`, so
`CopyToOutputDirectory` fired and failed trying to copy the absent
`win-x64` DLL.
## Changes
- **`src/api/dotnet/CMakeLists.txt`**: Introduce `Z3_DOTNET_WIN_RID`
cmake variable (`win-x64` / `win-x86` / `win-arm64`) derived from
`TARGET_ARCHITECTURE`; used at `configure_file` time.
- **`src/api/dotnet/Microsoft.Z3.csproj.in`**: Remove
`/$(_DN_CMAKE_CONFIG)` from the Windows DLL path; replace hardcoded
`runtimes\win-x64\native` with `runtimes\${Z3_DOTNET_WIN_RID}\native`.
- **`src/api/dotnet/Microsoft.Z3.targets`**: Add
`!$(TargetFramework.Contains('.'))` to the legacy-copy condition, which
correctly excludes `net5.0`/`net6.0`/`net7.0`/`net8.0` (all use dotted
TFMs) while keeping `net45`/`net472` etc.
- **`src/api/dotnet/Microsoft.Z3.props`**: Add explicit `arm64`
condition mapping `$(Platform) == 'arm64'` to
`runtimes\win-arm64\native\libz3.dll` for legacy .NET Framework ARM64
consumers.
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.
- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.
- **Rewriter fix**
- Added a sound rewrite branch for:
- `store* ((as const ...) v)` vs `store* ((as const ...) w)`
- When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
- select equalities for touched indices (existing behavior)
- **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.
- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.
```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
