# Conformance notes and solver extensions
`language-smtlib` targets **SMT-LIB 2.7**. This document records what the
library conforms to, where it deviates as *benign supersets*, the scope
boundaries of the AST, and how it handles the solver-specific extensions found
in real benchmark corpora (cvc5, Z3, Yices2, OpenSMT).
## Baseline
- Targets SMT-LIB **2.7** as the baseline. The string-escape rules and
reserved-word set are isolated in `Language.SMTLIB.Syntax.Constant` and
`Language.SMTLIB.Internal.Lexical` for easy verification against the 2.7
reference. The `->` map sort parses as an ordinary sort application; the
higher-order apply operator `_` is parsed where it coincides with the
indexed-identifier syntax (`(_ f x)`), matching the 2.7 concrete grammar
(Appendix B), which adds no dedicated application production.
- Numeric literals (decimal/hex/binary) keep their raw lexeme, so printing
round-trips byte-for-byte; use the interpreters in
`Language.SMTLIB.Syntax.Constant` for their values.
## Scope
The library covers SMT-LIB *scripts* (commands, terms, sorts, datatypes) and
the *solver-response* protocol. The theory/logic **catalog** format — the
`(theory …)` and `(logic …)` declarations with their attribute grammars
(`sort_symbol_decl`, `par_fun_symbol_decl`, `theory_attribute`, …) — is
intentionally **out of scope**: it describes the theory/logic definitions
published on smt-lib.org, not input a solver reads from a script.
## Benign supersets accepted beyond 2.7
A few inputs the strict 2.7 grammar forbids are accepted anyway because they
round-trip losslessly. These are **not** extensions any single solver needs:
- Unicode letters in simple symbols (so identifiers like `あいうえお` need no
quoting);
- `(push)` / `(pop)` without a numeral, read as `(push 1)` / `(pop 1)`;
- leading-zero numerals (`007`), leading-zero or trailing-dot decimals (`01.5`,
`1.`), kept verbatim via the raw `SCDecimal` lexeme;
- non-printable control characters inside string and quoted-symbol literals.
## Well-formedness constraints not enforced
Some *well-formedness* constraints that the grammar states separately from the
production rules are not enforced (the parser is syntactic only): in particular
the equal-length linkage between the two lists of `declare-datatypes`
(`sort_dec`ⁿ⁺¹ / `datatype_dec`ⁿ⁺¹) and of `define-funs-rec`
(`function_dec`ⁿ⁺¹ / `term`ⁿ⁺¹) is accepted even when the counts differ.
## Unknown commands and responses
By default command parsing is strict: an unrecognized command (an unknown head
keyword) is a parse error. The lenient parsers `pCommandLenient` /
`pScriptLenient` (in `Language.SMTLIB.Parser.Command`, run through `parseWith`)
instead keep such a command as `UnknownCommand keyword args`, capturing its raw
argument s-expressions so the application can decide what to do — the fallback
fires only on an unknown head keyword, so a recognized command with malformed
arguments still fails. Solver-response parsing (`pCommandResponse`) is always
lenient, keeping an unrecognized response as `ROther`; both forms round-trip.
The rest of this document catalogs the solver extensions found in the
cvc5/Z3/Yices2/OpenSMT suites and their support status (extension
commands/responses are lenient; term/sort/lexical extensions are not).
## Solver extensions and support status
Real solvers extend the format with their own commands, responses and surface
syntax, and those extensions show up throughout the example/regression suites
shipped with cvc5, Z3, Yices2 and OpenSMT. The tables below catalog the
extensions that appear in those corpora and record whether — and how — the
library handles each one.
Status legend:
| Status | Meaning |
| --- | --- |
| ✅ **Modeled** | Parsed into a dedicated typed AST node (standard 2.7, plus the benign supersets listed above). |
| 🟡 **Lenient** | Parsed but kept **verbatim** — an extension *command* as `UnknownCommand`, an extension *response* as `ROther`. No typed model; the raw s-expressions are preserved so the application can interpret them. Requires the lenient parser (see below). Round-trips through the printer. |
| ❌ **Unsupported** | A parse error. These are non-command extensions to the term/sort/lexical grammar; there is currently no way to accept them. |
The validation behind these tables (running the strict parser over the four
solver corpora, then re-running the failures through the lenient parser) is
summarised in [PR #18](https://github.com/msakai/language-smtlib/pull/18).
### Extension commands — 🟡 lenient (`UnknownCommand`)
By default command parsing is **strict**: an unrecognized head keyword is a
parse error. The lenient parsers keep such a command instead:
```haskell
import Language.SMTLIB -- re-exports pScriptLenient via Language.SMTLIB.Parser
parseWith pScriptLenient "<input>" src
```
`pCommandLenient` / `pScriptLenient` (defined in `Language.SMTLIB.Parser.Command`
and re-exported from `Language.SMTLIB.Parser`, run through `parseWith`) produce
```haskell
UnknownCommand !Symbol [SExpr a] -- head keyword + raw argument s-expressions
```
for any command whose head keyword is not one of the 32 recognized commands. The
fallback fires **only** on an unknown head keyword: a *recognized* command with
malformed arguments (e.g. `(assert)`) still fails, so genuine syntax errors are
not swallowed. Both `language-smtlib-fmt --lenient` and the whole-text
`parseWith pScriptLenient` entry points expose this behavior.
The extension commands observed in the solver corpora, grouped by feature:
| Feature | Commands | Solver(s) |
| --- | --- | --- |
| Interpolation | `get-interpolant`, `get-interpolants`, `get-interpolant-next`, `get-unsat-model-interpolant`, `get-unsat-core-lemmas` | cvc5, OpenSMT, Yices2 |
| Abduction | `get-abduct`, `get-abduct-next` | cvc5 |
| Synthesis / SyGuS | `declare-var`, `find-synth`, `find-synth-next` | cvc5 |
| Separation logic | `declare-heap` | cvc5 |
| Model exploration | `block-model`, `block-model-values`, `get-model-domain-elements`, `check-sat-assuming-model` | cvc5, Yices2 |
| Quantifier elimination | `get-qe`, `get-qe-disjunct` | cvc5 |
| Datalog / Horn (Z3 μZ / Spacer) | `declare-rel`, `declare-var`, `rule`, `query` | Z3 |
| Codatatypes | `declare-codatatype`, `declare-codatatypes` | cvc5 |
| Quantifier-instantiation pools | `declare-pool` | cvc5 |
| Diagnostics / control | `simplify`, `get-difficulty`, `get-learned-literals`, `get-timeout-core`, `get-timeout-core-assuming` | cvc5 |
The list is illustrative, not exhaustive — the lenient parser accepts **any**
unknown head keyword, so solver commands not seen in these corpora are handled
the same way.
### Extension responses — 🟡 lenient (`ROther`)
Solver-response parsing (`Language.SMTLIB.Parser.Response`, `pCommandResponse`)
is **always** lenient: an unrecognized response is kept as
```haskell
ROther (SExpr a)
```
so a driver reading a solver's stdout never fails on a response shape it does
not model (extension `get-info` fields, solver-specific `(error …)` payloads,
custom `get-value`/model formats, etc.). It also round-trips through the printer.
### Non-command syntactic extensions — ❌ unsupported
These extend the **term / sort / lexical** grammar rather than the command set,
so command-level leniency does not help — they are still parse errors. They are
listed here so the gaps are documented, not hidden. (Note that some
solver-specific *operators* are **not** in this list because they already parse
as ordinary function applications and so need no special handling — e.g. the
separation-logic operators `sep`, `pto`, `emp`, `nil`; only the `declare-heap`
command needs leniency.)
| Extension | Example | Solver | Notes |
| --- | --- | --- | --- |
| Finite-field literals | `#f0m3` (`#f`⟨value⟩`m`⟨modulus⟩) | cvc5 (theory `FF`) | A new numeric literal shape the framer cannot lex. |
| `set.comprehension` binder | `(set.comprehension ((x U)) φ t)` | cvc5 (sets) | A binder form; its `((x U))` binder list is not a term. |
| Character code-point index | `(_ char #x93A83)` | cvc5 (strings) | An indexed identifier whose index is a hex literal, not a numeral/symbol. |
| Nullary application | `(nullable.some)`, `(fp)` | cvc5 | A 0-ary function applied with parentheses; 2.7 requires the bare symbol. |
| Old-style datatype declarations | `(((zero) n) …)` | cvc4-era / TIP benchmarks | Pre-2.6 `declare-datatypes` constructor syntax. |
| C-style string escapes | `"foo \" bar"` | OpenSMT | 2.6+ strings only escape `"` by doubling it (`""`); backslash escapes are not recognized. |
| Reserved word as identifier | `(declare-fun lambda () …)` | cvc5 | `lambda` (and other 2.7 reserved words) cannot name a function. |
Also correctly rejected — and *not* extensions but malformed input — are the
solvers' intentional **negative/error test files** (a recognized command with
bad arguments such as `(get-proof :sat)` or `(get-value ())`, truncated input,
extra parentheses) and files that are not SMT-LIB at all (e.g. `diff` output
mis-named `.smt2`). Leniency deliberately leaves these failing.