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>
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>
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.
The code is making some assumptions that arrays are 1-dimensional. This is not generally true.
Introducing pattern matching to ensure the assumption is met.
Avoid get_arg(..) especially when there is an approach based on pattern matching recognizers.
- remove reduce_invertible. It is subsumed by reduce_uncstr(2)
- introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter.
reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence.
The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner.
