mirror of
https://github.com/Z3Prover/z3
synced 2026-07-16 12:05:43 +00:00
316d249b3f
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>
|
||
|---|---|---|
| .. | ||
| assertions | ||
| check_logic.cpp | ||
| check_logic.h | ||
| check_sat_result.cpp | ||
| check_sat_result.h | ||
| CMakeLists.txt | ||
| combined_solver.cpp | ||
| combined_solver.h | ||
| combined_solver_params.pyg | ||
| mus.cpp | ||
| mus.h | ||
| parallel_params.pyg | ||
| parallel_tactical.cpp | ||
| parallel_tactical.h | ||
| parallel_tactical2.cpp | ||
| parallel_tactical2.h | ||
| preferred_value_propagator.h | ||
| progress_callback.h | ||
| simplifier_solver.cpp | ||
| simplifier_solver.h | ||
| slice_solver.cpp | ||
| slice_solver.h | ||
| smt_logics.cpp | ||
| smt_logics.h | ||
| solver.cpp | ||
| solver.h | ||
| solver2tactic.cpp | ||
| solver2tactic.h | ||
| solver_na2as.cpp | ||
| solver_na2as.h | ||
| solver_pool.cpp | ||
| solver_pool.h | ||
| solver_preprocess.cpp | ||
| solver_preprocess.h | ||
| tactic2solver.cpp | ||
| tactic2solver.h | ||