This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This is a second version of https://github.com/Z3Prover/z3/pull/9957. I
address @NikolajBjorner 's comments about not changing the semicolons
after macro invocations, because some editors work better with them
present. It now, to the best of my ability, only deletes semis:
* after the closing brace of namespace decl.
* after the closing brace of an extern "C" decl.
* after a function definition.
This PR is very large, but it consists entirely of deletions of
semicolons in these situations.
(If there was a way to update the previous PR, which had been closed,
and that is preferable, please let me know. I couldn't figure it out.)
`qe-lite` could produce malformed formulas when expanding bounded
quantifiers under nested binders, leaving outer de Bruijn indices
unshifted after eliminating an inner quantifier (e.g., `(:var 1)`
escaping capture). This change fixes index normalization in that rewrite
path and adds a regression for the reported forall/exists arithmetic
case.
- **Rewrite correctness in bounded quantifier expansion**
- In `src/qe/lite/qe_lite_tactic.cpp`, after substituting bounded
variables in payload conjuncts, apply `inv_var_shifter(num_decls)` so
outer bound variables are reindexed relative to the removed binder.
- This preserves quantifier structure correctness when
`try_expand_bounded_quantifier` eliminates an inner quantifier.
- **Regression coverage for the reported pattern**
- In `src/test/smt_context.cpp`, add a focused quantified arithmetic
formula matching the bug shape:
- outer `forall (x, x4)`
- inner `exists (y)`
- mixed inequalities that trigger qe-lite bounded expansion
- Assert the formula is unsatisfiable, preventing reintroduction of
invalid index handling in this path.
```c++
inst = vs(p, subst_map.size(), subst_map.data());
shift(inst, num_decls, inst); // reindex outer de Bruijn vars after eliminating inner quantifier
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the `iss-7027/small-30` snapshot regression (`Z3Prover/bench`
discussion #2705) **at its root**, instead of working around it by
retuning the LP heuristics.
- **Benchmark:** `inputs/issues/iss-7027/small-30.smt2` —
`(check-sat-using qe2)` over a single `(distinct ...)` of 33 mixed
Int/Real terms.
- The recorded oracle was `unknown`; current `master` produces
`timeout`.
## Root cause
`unknown`/`timeout` are both wrong here: the formula is a `distinct`
over 33 terms (free Int/Real constants plus the literals `0`/`1`), which
is **trivially `sat`** — there are infinitely many distinct reals.
The real bug is in the `qsat` tactic that backs `qe2`. Running
quantifier elimination on a **quantifier-free** formula has nothing to
eliminate, so `qsat` left an undecided residual goal and
`check-sat-using` reported `unknown`. This reproduces on any ground
formula with free variables, e.g.:
```
(declare-fun a () Int)(assert (> a 0))(check-sat-using qe2) ; -> unknown (should be sat)
```
For `small-30` the QE alternation additionally drove `theory_lra`
integer branch-and-bound down a non-terminating path, surfacing as a
`timeout` under the capture budget (the symptom the `random_hammers`
schedule change happened to expose).
## Fix
Under `check-sat` semantics, top-level free variables are implicitly
existentially quantified. So when the `qsat` input has no quantifiers,
decide satisfiability directly (route through the existing `qsat_sat`
path) instead of producing a residual goal. `qe2`/`qe` now return
`sat`/`unsat` for ground formulas.
QE of genuinely-quantified formulas is unchanged: `apply qe2` on a
quantified goal produces the same projected formula as before (verified
identical to `master`). Only the degenerate quantifier-free case is
affected.
This supersedes the previous approach in this PR (reverting the
`lp.random_hammers` default). That default is left **unchanged**
(`true`), preserving #9958's aggregate QF_LIA benefit. `small-30` now
returns `sat` in ~0.01s regardless of the heuristic schedule, because
the QE machinery no longer runs on this ground instance.
Two changes:
- `src/qe/qsat.cpp`: short-circuit quantifier-free input to the
satisfiability decision path.
- `Z3Prover/bench` `inputs/issues/iss-7027/small-30.expected.out`:
oracle updated `unknown` -> `sat` (to be committed alongside this fix).
## Validation
```
$ z3 small-30.smt2
sat # ~0.01s
$ echo '(declare-fun a () Int)(assert (> a 0))(check-sat-using qe2)' | z3 -in
sat
$ echo '(declare-fun a () Int)(assert (and (> a 0)(< a 0)))(check-sat-using qe2)' | z3 -in
unsat
```
Full unit-test suite (`test-z3 /a`) passes (92/92). Quantified `qe2`
round-trips (`apply qe2`) match `master` byte-for-byte.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Two fixes for mbp_dt_tg::apply() when encountering an accessor whose
argument has a different constructor in the model:
1. Don't call rm_accessor (which would assert a contradictory
recognizer, making the formula false). This prevents the original bug
where QEL returned 'false' for satisfiable formulas.
2. Branch on the model-assigned constructor for the accessor's argument.
The correct output should include the literal introduced in (2).
However, this fix does not produce it. Spacer is sound with this
over-approximation, as long as the counter example does not depend on
value of mismatched accessors (e.g. (tl nil)).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Initial plan
* simplify extract_var_bound in qe_lite_tactic.cpp via operator normalization
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add defensive check for integer type in lhs
Added a defensive check for integer type in lhs before proceeding with inequality checks.
* Update qe_lite_tactic.cpp
* Fix utility function call for integer check
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
After qe-light's equation solver (eq_der) eliminates variables from
linear equations, remaining bounded integer quantifiers may still have
non-unit coefficients that prevent Fourier-Motzkin elimination.
Add a bounded quantifier expansion step: when the remaining quantified
integer variables all have explicit finite bounds and the product of
domain sizes is <= 10000, expand the quantifier into a finite
disjunction. This turns e.g. exists y0 in [0,10), y1 in [0,15): P(x,y0,y1)
into P(x,0,0) | P(x,0,1) | ... | P(x,9,14), which is 150 disjuncts.
The SMT solver handles the resulting quantifier-free formula instantly,
whereas the previous QSAT/MBP approach timed out due to weak integer
projections from the (|a|-1)*(|b|-1) slack in Fourier-Motzkin resolution
with non-unit coefficients.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Initial plan
* Refactor mk_and and mk_or call sites to use overloaded methods
Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h)
* Fix compilation errors from mk_and/mk_or refactoring
Fixed type mismatches by:
- Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads)
- Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and)
- Verified build succeeds and Z3 works correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix test files to use correct mk_and/mk_or overloads
Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter
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>
* 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).
mbp_qel uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
Heuristic for EMBPR is to unify terms that occur in uninterpreted contents. Walk partitions that are pure f(t) and an impure f(s)
and attempt to unify t with s ensuring that merges from s preserves satisfiability.
spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
