language-smtlib 0.1.0.0 → 0.2.0.0

raw patch · 22 files changed

+552/−94 lines, 22 filesdep +hashabledep +unordered-containersdep ~containersnew-component:exe:language-smtlib-fmtPVP ok

version bump matches the API change (PVP)

Dependencies added: hashable, unordered-containers

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +37/−1
• README.md +26/−23
• app/Main.hs +27/−7
• conformance/Main.hs +2/−2
• conformance/README.md +7/−6
• docs/conformance.md +165/−0
• language-smtlib.cabal +19/−8
• src/Language/SMTLIB.hs +0/−2
• src/Language/SMTLIB/Internal/Lexical.hs +0/−6
• src/Language/SMTLIB/Parser.hs +22/−1
• src/Language/SMTLIB/Parser/Command.hs +31/−2
• src/Language/SMTLIB/Parser/Response.hs +7/−1
• src/Language/SMTLIB/Printer/Class.hs +2/−0
• src/Language/SMTLIB/Syntax/Annotation.hs +5/−1
• src/Language/SMTLIB/Syntax/Attribute.hs +10/−3
• src/Language/SMTLIB/Syntax/Command.hs +19/−4
• src/Language/SMTLIB/Syntax/Constant.hs +7/−2
• src/Language/SMTLIB/Syntax/Datatype.hs +16/−6
• src/Language/SMTLIB/Syntax/Identifier.hs +10/−3
• src/Language/SMTLIB/Syntax/Response.hs +22/−7
• src/Language/SMTLIB/Syntax/Term.hs +14/−5
• test/Spec.hs +104/−4

@@ -6,7 +6,43 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). -## Unreleased+## 0.2.0.0 - 2026-07-06++- Add `UnknownCommand` (to `Command`) and `ROther` (to `CommandResponse`) so a+  syntactically well-formed but unrecognized command or solver response can be+  kept verbatim for the application to handle, instead of failing the parse.+  Command parsing stays strict by default (`parseScript`/`pCommand` reject an+  unknown head keyword); the new lenient parsers `pCommandLenient` /+  `pScriptLenient` (in `Language.SMTLIB.Parser.Command`, run via `parseWith`)+  produce `UnknownCommand` instead.  The fallback fires only on an unknown head+  keyword — a recognized command with malformed arguments still fails.+  Solver-response parsing (`pCommandResponse`) is always lenient, keeping an+  unrecognized response as `ROther`.+- `language-smtlib-fmt` gains a `--lenient` flag that formats scripts+  containing unrecognized commands (via `pScriptLenient`) instead of failing;+  without it the formatter stays strict as before.+- Derive `Ord`, `Generic` and `Hashable` for every AST type (and `SrcSpan`),+  so syntax trees can be used as `Data.Map`/`Data.HashMap` keys.  These+  comparisons and hashes are structural and follow the existing `Eq`+  (numeric literals compare by raw lexeme; annotations participate, so erase+  them with `noAnn` for annotation-insensitive keys).  This adds a dependency+  on the `hashable` package (`>= 1.3 && < 1.6`).+- Read the `test/samples/smt/` sample files as UTF-8 explicitly, so the test+  suite no longer fails on the non-ASCII samples under a non-UTF-8 locale+  (e.g. `C`/`POSIX`).+- `Language.SMTLIB.Parser` now re-exports the `Language.SMTLIB.Parser.Command`+  and `Language.SMTLIB.Parser.Response` combinators, making it the single,+  complete public parsing API.  The command combinators (including the lenient+  `pCommandLenient` / `pScriptLenient` variants) are therefore now reachable+  from the umbrella `Language.SMTLIB` module too, matching the response+  combinators and removing the need to import `Language.SMTLIB.Parser.Command`+  separately.  The umbrella drops its own direct `Language.SMTLIB.Parser.Response`+  re-export, as it now arrives transitively through `Language.SMTLIB.Parser`.+- Rename the developer executable `language-smtlib-exe` to `language-smtlib-fmt`,+  and replace the `conformance` build flag with a broader manual `tools` flag+  that now gates **both** `language-smtlib-fmt` and `language-smtlib-conformance`.+  Neither executable is built by a plain `stack build` anymore; pass+  `--flag language-smtlib:tools` to build them.  ## 0.1.0.0 - 2026-06-08 

@@ -1,6 +1,7 @@ # language-smtlib  [![build](https://github.com/msakai/language-smtlib/actions/workflows/build.yaml/badge.svg)](https://github.com/msakai/language-smtlib/actions/workflows/build.yaml)+[![Hackage](https://img.shields.io/hackage/v/language-smtlib.svg)](https://hackage.haskell.org/package/language-smtlib)  A robust, `Text`-based Haskell library for reading, writing and incrementally streaming the [SMT-LIB 2](https://smt-lib.org/) format.@@ -10,7 +11,9 @@ - **Full SMT-LIB 2.7 grammar** — commands, terms, sorts, datatypes   (`declare-datatype(s)`, `match`, `par`), the 2.7 additions (`lambda`,   `declare-sort-parameter`, `define-const`, the `_` wildcard pattern), and-  solver command responses.+  solver command responses. See [docs/conformance.md](docs/conformance.md) for+  the exact conformance boundaries, benign supersets, and how solver-specific+  extensions are handled. - **`Text`-based** throughout, with rich parse errors from   [megaparsec](https://hackage.haskell.org/package/megaparsec). - **Optional source spans.** Every AST node carries a final annotation type@@ -77,22 +80,6 @@ | `Language.SMTLIB.Printer` | rendering to `Text` | | `Language.SMTLIB.Reader` / `.Reader.Handle` | pure / `Handle`-based incremental readers | -## Conformance notes--- 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.-- As a benign superset, Unicode letters are accepted in simple symbols (so-  identifiers like `あいうえお` need no quoting), and `(push)` / `(pop)` without-  a numeral are read as `(push 1)` / `(pop 1)`.-- 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.- ## Building  ```@@ -100,13 +87,28 @@ stack test     # round-trip properties, framer units, and sample files ``` +## Testing tools++Two developer tools exercise the parser and printer against real-world corpora.+Both are gated behind the manual `tools` flag, so they stay off by default — out+of a plain `stack build`/`stack test`, and never a burden on downstream+consumers. CI builds them behind the flag so they cannot bit-rot, but does not+run them:++```+stack build --flag language-smtlib:tools+```++- `language-smtlib-fmt` parses a file/stdin and re-emits it canonically (the+  corpus script below drives it);+- `language-smtlib-conformance` round-trips large external benchmark suites.+ ### Testing against large external benchmarks  To stress-test the parser and printer against the full SMT-LIB / SMT-COMP-benchmark suites on [Zenodo](https://zenodo.org/), there is an optional-`language-smtlib-conformance` driver, built only behind the `conformance` flag-(so it is never part of the normal build, test suite, or CI) and run on-benchmark data that is downloaded separately and never committed. See+benchmark suites on [Zenodo](https://zenodo.org/), use the+`language-smtlib-conformance` driver. Running it requires benchmark data that is+downloaded separately and never committed. See [`conformance/README.md`](conformance/README.md).  ### Round-trip checking a corpus of `.smt2` files@@ -114,8 +116,9 @@ For a quick, dependency-free check against an arbitrary collection of `.smt2` files (for example the example/regression suites shipped with cvc5, OpenSMT, Yices2, or Z3), use [`scripts/roundtrip-check.sh`](scripts/roundtrip-check.sh).-It drives the `language-smtlib-exe` front end (parse → render) over every file-and verifies that the canonical rendering is idempotent:+It drives the `language-smtlib-fmt` front end (parse → render) over every file+and verifies that the canonical rendering is idempotent (the script builds it+with the `tools` flag when run with `--build`):  ``` scripts/roundtrip-check.sh [--build] [--out DIR] [PATH...]

@@ -14,10 +14,30 @@ main :: IO () main = do   args <- getArgs-  (name, src) <- case args of-    []     -> (,) "<stdin>" <$> T.getContents-    [f]    -> (,) f <$> T.readFile f-    _      -> hPutStrLn stderr "usage: language-smtlib-exe [FILE]" >> exitFailure >> pure ("", "")-  case parseScript name src of-    Left err     -> hPutStrLn stderr (errorBundlePretty err) >> exitFailure-    Right script -> T.putStr (renderScript script)+  case parseArgs args of+    Left msg -> hPutStrLn stderr msg >> exitFailure+    Right (lenient, mpath) -> do+      (name, src) <- case mpath of+        Nothing -> (,) "<stdin>" <$> T.getContents+        Just f  -> (,) f <$> T.readFile f+      let parse = if lenient then parseWith pScriptLenient else parseScript+      case parse name src of+        Left err     -> hPutStrLn stderr (errorBundlePretty err) >> exitFailure+        Right script -> T.putStr (renderScript script)++-- | Parse the command line into @(lenient, optional path)@.  @--lenient@ keeps+-- unrecognized commands as @UnknownCommand@ instead of failing the parse.+parseArgs :: [String] -> Either String (Bool, Maybe FilePath)+parseArgs = go False Nothing+  where+    go lenient mpath args = case args of+      []                  -> Right (lenient, mpath)+      ("--lenient" : rest) -> go True mpath rest+      (a : rest)+        | take 1 a == "-"  -> Left ("unknown option: " ++ a ++ "\n" ++ usage)+        | otherwise        -> case mpath of+            Nothing -> go lenient (Just a) rest+            Just _  -> Left ("too many file arguments\n" ++ usage)++usage :: String+usage = "usage: language-smtlib-fmt [--lenient] [FILE]"

@@ -18,10 +18,10 @@ -- -- This tool is intentionally /not/ part of the normal build or test suite: the -- benchmark data is huge and lives outside the repository.  It is only built--- when the @conformance@ cabal flag is set, e.g.+-- when the @tools@ cabal flag is set, e.g. -- -- @--- stack build --flag language-smtlib:conformance+-- stack build --flag language-smtlib:tools -- stack exec language-smtlib-conformance -- benchmarks\/ -- @ module Main (main) where

@@ -5,11 +5,12 @@ collections — in particular the SMT-LIB / SMT-COMP suites published on [Zenodo](https://zenodo.org/). -It is **deliberately excluded from the normal build, test suite and CI**: the+It is **never run as part of the normal build, test suite or CI**: the benchmark data is huge (tens to hundreds of GB once extracted) and lives outside-the repository. The tool is only built when the `conformance` cabal flag is set,-and the benchmark data is never committed (the default download directory-`benchmarks/` is gitignored).+the repository. The tool is built only when the `tools` cabal flag is set — CI+compiles it behind that flag so it cannot bit-rot, but never runs it — and the+benchmark data is never committed (the default download directory `benchmarks/`+is gitignored).  ## What it checks @@ -38,8 +39,8 @@ scripts/fetch-smtlib-benchmarks.sh --record 11061097 QF_BV QF_LIA  # 2. Build the checker with the flag enabled:-stack build --flag language-smtlib:conformance-#    (with cabal:  cabal build -f conformance language-smtlib-conformance)+stack build --flag language-smtlib:tools+#    (with cabal:  cabal build -f tools language-smtlib-conformance)  # 3. Run it over the downloaded files: stack exec language-smtlib-conformance -- benchmarks/

@@ -0,0 +1,165 @@+# 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.

@@ -1,11 +1,11 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.38.1.+-- This file has been generated from package.yaml by hpack version 0.39.6. -- -- see: https://github.com/sol/hpack  name:           language-smtlib-version:        0.1.0.0+version:        0.2.0.0 synopsis:       Parsing, printing and incremental I/O for the SMT-LIB 2 format description:    A @Text@-based library for parsing, printing, and incrementally streaming the SMT-LIB 2.7 format.                 .@@ -67,18 +67,19 @@     README.md     CHANGELOG.md     conformance/README.md+    docs/conformance.md  source-repository head   type: git   location: https://github.com/msakai/language-smtlib -flag conformance-  description: Build language-smtlib-conformance, a driver that round-trips large external SMT-LIB benchmark suites (e.g. the SMT-LIB / SMT-COMP collections on Zenodo).  Off by default: it is not part of the normal build, test suite or CI.+flag profiling+  description: Add -fprof-auto (automatic cost centres) to this package's own components when building with profiling.  Off by default so that downstream packages profiling their own code are not cluttered with cost centres from language-smtlib.   manual: True   default: False -flag profiling-  description: Add -fprof-auto (automatic cost centres) to this package's own components when building with profiling.  Off by default so that downstream packages profiling their own code are not cluttered with cost centres from language-smtlib.+flag tools+  description: Build the developer-facing command-line tools shipped with this package: language-smtlib-fmt, a round-trip front end that parses an SMT-LIB script and re-emits it in canonical form; and language-smtlib-conformance, a driver that round-trips large external SMT-LIB benchmark suites (e.g. the SMT-LIB / SMT-COMP collections on Zenodo).  Off by default: these are development utilities, not needed by downstream packages that only depend on the library.   manual: True   default: False @@ -114,6 +115,7 @@   default-extensions:       DeriveFoldable       DeriveFunctor+      DeriveGeneric       DeriveTraversable       LambdaCase       OverloadedStrings@@ -123,6 +125,7 @@   build-depends:       base >=4.7 && <5     , containers >=0.6 && <0.8+    , hashable >=1.3 && <1.6     , megaparsec >=9.0 && <10     , parser-combinators >=1.0 && <1.4     , prettyprinter ==1.7.*@@ -143,6 +146,7 @@   default-extensions:       DeriveFoldable       DeriveFunctor+      DeriveGeneric       DeriveTraversable       LambdaCase       OverloadedStrings@@ -156,12 +160,12 @@     , language-smtlib     , text >=1.2 && <2.2   default-language: Haskell2010-  if !flag(conformance)+  if !flag(tools)     buildable: False   if flag(profiling)     ghc-prof-options: -fprof-auto -executable language-smtlib-exe+executable language-smtlib-fmt   main-is: Main.hs   other-modules:       Paths_language_smtlib@@ -172,6 +176,7 @@   default-extensions:       DeriveFoldable       DeriveFunctor+      DeriveGeneric       DeriveTraversable       LambdaCase       OverloadedStrings@@ -183,6 +188,8 @@     , language-smtlib     , text >=1.2 && <2.2   default-language: Haskell2010+  if !flag(tools)+    buildable: False   if flag(profiling)     ghc-prof-options: -fprof-auto @@ -199,6 +206,7 @@   default-extensions:       DeriveFoldable       DeriveFunctor+      DeriveGeneric       DeriveTraversable       LambdaCase       OverloadedStrings@@ -208,8 +216,10 @@   build-depends:       QuickCheck     , base >=4.7 && <5+    , containers     , directory     , filepath+    , hashable     , language-smtlib     , megaparsec     , quickcheck-instances@@ -217,4 +227,5 @@     , tasty-hunit     , tasty-quickcheck     , text+    , unordered-containers   default-language: Haskell2010

@@ -14,7 +14,6 @@ module Language.SMTLIB   ( module Language.SMTLIB.Syntax   , module Language.SMTLIB.Parser-  , module Language.SMTLIB.Parser.Response   , module Language.SMTLIB.Printer     -- * Error rendering (re-exported from megaparsec) @@ -26,6 +25,5 @@ import Text.Megaparsec (errorBundlePretty)  import Language.SMTLIB.Parser-import Language.SMTLIB.Parser.Response import Language.SMTLIB.Printer import Language.SMTLIB.Syntax

@@ -20,12 +20,6 @@ -- | The SMT-LIB 2.7 reserved words: the auxiliary tokens plus every command -- name.  A simple symbol may not coincide with one of these, so a @Symbol@ -- whose value is a reserved word must be printed quoted.------ Note: @lambda@ is treated as a reserved word here, consistently with the--- other binders (@forall@\/@exists@\/@let@\/@match@), so that a @(lambda ...)@--- term round-trips unambiguously.  The Version 2.7 concrete-syntax appendix--- omits @lambda@ from its reserved-word list, but the term grammar gives it a--- dedicated binder production, so we follow the grammar. reservedWords :: Set Text reservedWords = Set.fromList $   -- auxiliary / general reserved words

@@ -10,6 +10,16 @@ --     so it can distinguish \"needs more input\" ('Partial') from a real --     framing error, and only invokes megaparsec on a complete frame.  This is --     the entry point for REPL\/pipe drivers.+--+-- The whole-text entry points are /strict/: an unrecognized command is a parse+-- error.  For lenient parsing — keeping an unknown command as+-- 'Language.SMTLIB.Syntax.Command.UnknownCommand' for the application to handle+-- — run the lenient parsers ('pScriptLenient' \/ 'pCommandLenient'), re-exported+-- here from "Language.SMTLIB.Parser.Command", through 'parseWith', e.g.+-- @'parseWith' 'pScriptLenient'@.  The solver-response parsers (re-exported from+-- "Language.SMTLIB.Parser.Response") are likewise run through 'parseWith', and+-- are always lenient: an unrecognized response is kept as+-- 'Language.SMTLIB.Syntax.Response.ROther'. module Language.SMTLIB.Parser   ( -- * Parser monad     P@@ -34,14 +44,25 @@   , feed   , isCleanEnd   , frameSExpr+    -- * Command combinators+    -- | The lower-level command parsers, including the lenient variants+    -- ('pScriptLenient' \/ 'pCommandLenient') that keep an unrecognized command+    -- as 'Language.SMTLIB.Syntax.Command.UnknownCommand'.  Run them through+    -- 'parseWith'.+  , module Language.SMTLIB.Parser.Command+    -- * Response combinators+    -- | The solver-response parsers.  These have no whole-text wrapper of their+    -- own; run them through 'parseWith'.+  , module Language.SMTLIB.Parser.Response   ) where  import Data.Text (Text) import Data.Void (Void) import Text.Megaparsec hiding (ParseError) -import Language.SMTLIB.Parser.Command (pCommand, pScript)+import Language.SMTLIB.Parser.Command import Language.SMTLIB.Parser.Internal (P, sc)+import Language.SMTLIB.Parser.Response import Language.SMTLIB.Parser.SExpr import Language.SMTLIB.Parser.Term (pTerm) import Language.SMTLIB.Syntax.Annotation (SrcSpan, noAnn)

@@ -1,7 +1,9 @@ -- | Parsers for commands, options and info flags. module Language.SMTLIB.Parser.Command   ( pCommand+  , pCommandLenient   , pScript+  , pScriptLenient   , pOption   , pInfoFlag   ) where@@ -20,14 +22,41 @@ pScript :: P (Script SrcSpan) pScript = many pCommand +-- | Like 'pScript', but unrecognized commands are kept as+-- 'Language.SMTLIB.Syntax.Command.UnknownCommand' rather than rejected.+pScriptLenient :: P (Script SrcSpan)+pScriptLenient = many pCommandLenient+ -- | A top-level @command@. -- -- The command keyword is read once as a single word and then dispatched on, -- rather than attempting each alternative in turn.  This avoids re-scanning the -- keyword (and the backtracking that goes with it) for every command — a large -- saving on scripts dominated by a few command shapes (e.g. @assert@).+--+-- An unrecognized head keyword is a parse error.  Use 'pCommandLenient' to keep+-- such commands as 'Language.SMTLIB.Syntax.Command.UnknownCommand' instead. pCommand :: P (Command SrcSpan)-pCommand = withSpan $ do+pCommand = pCommandWith $ \kw -> fail ("unknown command: " ++ T.unpack kw)++-- | Like 'pCommand', but an unrecognized head keyword is accepted: the command+-- is kept as 'Language.SMTLIB.Syntax.Command.UnknownCommand' carrying the+-- keyword and its raw argument s-expressions, leaving the application to decide+-- what to do with it.+--+-- The fallback fires /only/ on an unknown head keyword.  A recognized command+-- with malformed arguments (e.g. @(assert)@) still fails, so genuine syntax+-- errors in known commands are not silently swallowed.+pCommandLenient :: P (Command SrcSpan)+pCommandLenient = pCommandWith $ \kw -> UnknownCommand kw <$> many pSExpr++-- | The shared command body, parameterized over how to handle an unrecognized+-- head keyword.  The handler is given the keyword and yields a constructor+-- still awaiting its final 'SrcSpan' field (as 'withSpan' expects).+pCommandWith+  :: (T.Text -> P (SrcSpan -> Command SrcSpan))+  -> P (Command SrcSpan)+pCommandWith onUnknown = withSpan $ do   _ <- openP   kw <- pAnyWord   c <- case kw of@@ -65,7 +94,7 @@     "get-value"               -> GetValue <$> parens (some pTerm)     "echo"                    -> Echo <$> pStringLit     "exit"                    -> pure Exit-    _                         -> fail ("unknown command: " ++ T.unpack kw)+    _                         -> onUnknown kw   _ <- closeP   pure c 

@@ -38,6 +38,11 @@ -- | The context-free responses (@success@, @unsupported@, the @check-sat@ -- answers, and @(error ...)@).  Use the specific parsers below for -- list-shaped responses.+--+-- Any other syntactically well-formed s-expression — a solver's non-standard or+-- extension output — is kept as+-- 'Language.SMTLIB.Syntax.Response.ROther' rather than rejected, leaving the+-- application to decide what to do with it. pCommandResponse :: P (CommandResponse SrcSpan) pCommandResponse = choice   [ tok "success"     $> RSuccess@@ -45,7 +50,8 @@   , tok "sat"         $> RCheckSat Sat   , tok "unsat"       $> RCheckSat Unsat   , tok "unknown"     $> RCheckSat Unknown-  , parens (tok "error" *> (RError <$> pStringLit))+  , try (parens (tok "error" *> (RError <$> pStringLit)))+  , ROther <$> pSExpr   ]  -- | @success | unsupported | (error string)@.

@@ -251,6 +251,7 @@     GetInfo flag _          -> parens (text "get-info" <+> pretty flag)     Echo s _                -> parens (text "echo" <+> prettyStringLit s)     Exit _                  -> parens (text "exit")+    UnknownCommand kw args _ -> parens (hsep (text kw : map pretty args))  instance Pretty CheckSatResponse where   pretty Sat     = text "sat"@@ -305,4 +306,5 @@     RGetUnsatAssumptions ts -> parens (hsep (map pretty ts))     RGetUnsatCore ss       -> parens (hsep (map prettySymbol ss))     RGetValue vps          -> parens (hsep (map pretty vps))+    ROther e               -> pretty e     where assignPair (s, b) = parens (prettySymbol s <+> prettyBool b)

@@ -12,6 +12,8 @@   ) where  import Data.Functor (void)+import Data.Hashable (Hashable)+import GHC.Generics (Generic)  -- | A half-open span @[spanStart, spanEnd)@ in the source text, measured in -- 0-based character offsets.  Offsets (rather than line\/column pairs) keep span@@ -20,7 +22,9 @@ data SrcSpan = SrcSpan   { spanStart :: !Int   , spanEnd   :: !Int-  } deriving (Eq, Ord, Show)+  } deriving (Eq, Ord, Show, Generic)++instance Hashable SrcSpan  -- | Access or replace the top-level annotation of a node. --

@@ -6,6 +6,9 @@   , Attribute(..)   ) where +import Data.Hashable (Hashable)+import GHC.Generics (Generic)+ import Language.SMTLIB.Syntax.Annotation (Annotated(..)) import Language.SMTLIB.Syntax.Constant (Keyword, SpecConstant, Symbol) @@ -16,20 +19,24 @@   | SEKeyword  !Keyword         a   | SEReserved !Symbol          a  -- ^ a reserved word appearing in an s-expr (e.g. @_@, @as@)   | SEList     [SExpr a]        a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | An @attribute_value@. data AttributeValue a   = AVConstant (SpecConstant a) a   | AVSymbol   !Symbol          a   | AVSExpr    [SExpr a]        a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | An @attribute@: a keyword, optionally carrying a value. data Attribute a   = Attribute     !Keyword                    a   | AttributeWith !Keyword (AttributeValue a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable a => Hashable (SExpr a)+instance Hashable a => Hashable (AttributeValue a)+instance Hashable a => Hashable (Attribute a)  instance Annotated SExpr where   ann = \case

@@ -6,10 +6,12 @@   , Script   ) where +import Data.Hashable (Hashable) import Data.Text (Text)+import GHC.Generics (Generic)  import Language.SMTLIB.Syntax.Annotation (Annotated(..))-import Language.SMTLIB.Syntax.Attribute (Attribute)+import Language.SMTLIB.Syntax.Attribute (Attribute, SExpr) import Language.SMTLIB.Syntax.Constant (Keyword, Symbol) import Language.SMTLIB.Syntax.Datatype   (DatatypeDec, FunctionDec, FunctionDef, SortDec)@@ -33,7 +35,7 @@   | ReproducibleResourceLimit  !Integer       a   | Verbosity                  !Integer       a   | OptionAttribute            (Attribute a)  a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | An @info_flag@ for @get-info@. data InfoFlag a@@ -45,7 +47,7 @@   | ReasonUnknownFlag   a   | InfoVersion         a   | InfoFlagKeyword !Keyword a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A top-level @command@. data Command a@@ -81,11 +83,22 @@   | GetInfo          (InfoFlag a)                       a   | Echo             !Text                              a   | Exit             a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  | UnknownCommand   !Symbol [SExpr a]                  a+    -- ^ A syntactically well-formed command whose head keyword is not one of+    -- the recognized commands above.  Carries the head keyword and the raw+    -- argument s-expressions so the application can decide how to handle it.+    -- Only produced by the lenient parsers+    -- (@Language.SMTLIB.Parser.Command.pCommandLenient@ \/ @pScriptLenient@);+    -- the strict parsers reject an unknown head keyword instead.+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A script is a sequence of commands. type Script a = [Command a] +instance Hashable a => Hashable (Option a)+instance Hashable a => Hashable (InfoFlag a)+instance Hashable a => Hashable (Command a)+ instance Annotated Option where   ann = \case     DiagnosticOutputChannel _ a   -> a@@ -174,6 +187,7 @@     GetInfo _ a             -> a     Echo _ a                -> a     Exit a                  -> a+    UnknownCommand _ _ a    -> a   setAnn a = \case     SetLogic x _            -> SetLogic x a     SetOption x _           -> SetOption x a@@ -207,3 +221,4 @@     GetInfo x _             -> GetInfo x a     Echo x _                -> Echo x a     Exit _                  -> Exit a+    UnknownCommand kw xs _  -> UnknownCommand kw xs a

@@ -19,9 +19,11 @@   ) where  import Data.Char (digitToInt)+import Data.Hashable (Hashable) import Data.Scientific (Scientific) import Data.Text (Text) import qualified Data.Text as T+import GHC.Generics (Generic)  import Language.SMTLIB.Syntax.Annotation (Annotated(..)) @@ -38,13 +40,16 @@   | SCHexadecimal !Text    a  -- ^ digits only (no @#x@), e.g. @"00aF"@   | SCBinary      !Text    a  -- ^ digits only (no @#b@), e.g. @"0110"@   | SCString      !Text    a  -- ^ decoded string value (no quotes, @""@ unescaped)-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | An @index@ of an indexed identifier @(_ sym i ...)@. data Index a   = IxNumeral !Integer a   | IxSymbol  !Symbol  a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable a => Hashable (SpecConstant a)+instance Hashable a => Hashable (Index a)  instance Annotated SpecConstant where   ann = \case

@@ -8,6 +8,9 @@   , FunctionDef(..)   ) where +import Data.Hashable (Hashable)+import GHC.Generics (Generic)+ import Language.SMTLIB.Syntax.Annotation (Annotated(..)) import Language.SMTLIB.Syntax.Constant (Symbol) import Language.SMTLIB.Syntax.Identifier (Sort)@@ -15,30 +18,37 @@  -- | A @sort_dec@ @(symbol numeral)@ heading a @declare-datatypes@. data SortDec a = SortDec !Symbol !Integer a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @selector_dec@ @(symbol sort)@. data SelectorDec a = SelectorDec !Symbol (Sort a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @constructor_dec@ @(symbol selector_dec*)@. data ConstructorDec a = ConstructorDec !Symbol [SelectorDec a] a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @datatype_dec@.  The first field holds the @par@ type variables; it is -- empty for a non-parametric @(constructor_dec+)@ declaration and non-empty for -- a @(par (u+) (constructor_dec+))@ declaration. data DatatypeDec a = DatatypeDec [Symbol] [ConstructorDec a] a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @function_dec@ @(symbol (sorted_var*) sort)@, used by @define-funs-rec@. data FunctionDec a = FunctionDec !Symbol [SortedVar a] (Sort a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @function_def@ @symbol (sorted_var*) sort term@, used by @define-fun@ and -- @define-fun-rec@. data FunctionDef a = FunctionDef !Symbol [SortedVar a] (Sort a) (Term a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable a => Hashable (SortDec a)+instance Hashable a => Hashable (SelectorDec a)+instance Hashable a => Hashable (ConstructorDec a)+instance Hashable a => Hashable (DatatypeDec a)+instance Hashable a => Hashable (FunctionDec a)+instance Hashable a => Hashable (FunctionDef a)  instance Annotated SortDec where   ann (SortDec _ _ a) = a

@@ -6,13 +6,16 @@   , pattern Symbol   ) where +import Data.Hashable (Hashable)+import GHC.Generics (Generic)+ import Language.SMTLIB.Syntax.Annotation (Annotated(..)) import Language.SMTLIB.Syntax.Constant (Index, Symbol)  -- | An @identifier@: a symbol optionally followed by a non-empty list of -- indices, in which case it prints as @(_ sym i ...)@. data Identifier a = Identifier !Symbol [Index a] a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A simple (non-indexed) identifier. pattern Symbol :: Symbol -> Identifier ()@@ -20,14 +23,18 @@  -- | A @sort@: an identifier applied to zero or more argument sorts. data Sort a = Sort (Identifier a) [Sort a] a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @qual_identifier@: an identifier, optionally annotated with a result sort -- via @(as id sort)@. data QualIdentifier a   = QIdentifier   (Identifier a)          a   | QIdentifierAs (Identifier a) (Sort a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable a => Hashable (Identifier a)+instance Hashable a => Hashable (Sort a)+instance Hashable a => Hashable (QualIdentifier a)  instance Annotated Identifier where   ann (Identifier _ _ a) = a

@@ -9,7 +9,9 @@   , CommandResponse(..)   ) where +import Data.Hashable (Hashable) import Data.Text (Text)+import GHC.Generics (Generic)  import Language.SMTLIB.Syntax.Attribute (Attribute, AttributeValue, SExpr) import Language.SMTLIB.Syntax.Constant (Symbol)@@ -18,18 +20,18 @@  -- | The response to @check-sat@. data CheckSatResponse = Sat | Unsat | Unknown-  deriving (Show, Eq)+  deriving (Show, Eq, Ord, Generic)  -- | The @:error-behavior@ of a solver. data ErrorBehavior = ImmediateExit | ContinuedExecution-  deriving (Show, Eq)+  deriving (Show, Eq, Ord, Generic)  -- | The @:reason-unknown@ explanation. data ReasonUnknown a   = RUMemout   | RUIncomplete   | RUOther (SExpr a)-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A single entry of a @get-info@ response. data InfoResponse a@@ -40,18 +42,18 @@   | IRReasonUnknown (ReasonUnknown a)   | IRVersion !Text   | IRAttribute (Attribute a)-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @(term value)@ pair of a @get-value@ response. data ValuationPair a = ValuationPair (Term a) (Term a)-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A single definition of a @get-model@ response. data ModelResponse a   = MRDefineFun (FunctionDef a)   | MRDefineFunRec (FunctionDef a)   | MRDefineFunsRec [FunctionDec a] [Term a]-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A solver's response to a command.  Which constructor a given solver emits -- depends on the command it answers; the parsers in@@ -72,4 +74,17 @@   | RGetUnsatAssumptions [Term a]   | RGetUnsatCore [Symbol]   | RGetValue [ValuationPair a]-  deriving (Show, Eq, Functor, Foldable, Traversable)+  | ROther (SExpr a)+    -- ^ A syntactically well-formed response that matches none of the+    -- recognized forms above.  The raw s-expression is kept verbatim so the+    -- application can decide how to handle a solver's non-standard or+    -- extension output.  Produced by 'Language.SMTLIB.Parser.Response.pCommandResponse'.+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable CheckSatResponse+instance Hashable ErrorBehavior+instance Hashable a => Hashable (ReasonUnknown a)+instance Hashable a => Hashable (InfoResponse a)+instance Hashable a => Hashable (ValuationPair a)+instance Hashable a => Hashable (ModelResponse a)+instance Hashable a => Hashable (CommandResponse a)

@@ -8,6 +8,9 @@   , MatchCase(..)   ) where +import Data.Hashable (Hashable)+import GHC.Generics (Generic)+ import Language.SMTLIB.Syntax.Annotation (Annotated(..)) import Language.SMTLIB.Syntax.Attribute (Attribute) import Language.SMTLIB.Syntax.Constant (SpecConstant, Symbol)@@ -24,15 +27,15 @@   | TExists    [SortedVar a]  (Term a)       a   | TMatch     (Term a) [MatchCase a]        a   | TAnnot     (Term a) [Attribute a]        a  -- ^ @(! term attr ...)@; attrs non-empty-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @var_binding@ @(symbol term)@ of a @let@. data VarBinding a = VarBinding !Symbol (Term a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @sorted_var@ @(symbol sort)@. data SortedVar a = SortedVar !Symbol (Sort a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @pattern@ of a @match@ case: either a single variable\/nullary -- constructor symbol, or @(constructor x1 ... xn)@.  As of SMT-LIB 2.7 the@@ -41,11 +44,17 @@ data Pattern a   = PVar  !Symbol           a   | PCtor !Symbol [Symbol]  a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)  -- | A @match_case@ @(pattern term)@. data MatchCase a = MatchCase (Pattern a) (Term a) a-  deriving (Show, Eq, Functor, Foldable, Traversable)+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)++instance Hashable a => Hashable (Term a)+instance Hashable a => Hashable (VarBinding a)+instance Hashable a => Hashable (SortedVar a)+instance Hashable a => Hashable (Pattern a)+instance Hashable a => Hashable (MatchCase a)  instance Annotated Term where   ann = \case

@@ -3,21 +3,25 @@ module Main (main) where  import Control.Monad (filterM, forM)+import Data.Either (isLeft)+import Data.Hashable (Hashable, hash)+import qualified Data.HashMap.Strict as HM+import Data.List (nub)+import qualified Data.Map.Strict as M import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T import System.Directory (doesDirectoryExist, doesFileExist, listDirectory) import System.FilePath ((</>), takeExtension)+import System.IO (IOMode (ReadMode), hSetEncoding, utf8, withFile) import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck-import Text.Megaparsec (eof, errorBundlePretty, parse)+import Text.Megaparsec (eof, parse)  import Arbitrary () import Language.SMTLIB-import Language.SMTLIB.Parser.Command import Language.SMTLIB.Parser.Internal-import Language.SMTLIB.Parser.SExpr import Language.SMTLIB.Parser.Term import Language.SMTLIB.Reader (frameAll) @@ -26,8 +30,10 @@   sampleTests <- loadSampleTests   defaultMain $ testGroup "language-smtlib"     [ roundTripTests+    , leniencyTests     , framerTests     , streamingTests+    , instancesTests     , sampleTests     ] @@ -68,6 +74,62 @@   , testProperty "Command"        (roundTrip pCommand        :: Command () -> Property)   ] +-- Leniency: unknown commands / responses -------------------------------------++-- | A 'Command' built from an unrecognized head keyword, for exercising the+-- lenient parser's round-trip.  The head is a simple word guaranteed not to be+-- one of the recognized commands.+newtype UnknownCmd = UnknownCmd (Command ()) deriving Show++instance Arbitrary UnknownCmd where+  arbitrary = do+    kw   <- genUnknownHead+    args <- resize 3 (listOf (resize 3 arbitrary))+    pure (UnknownCmd (UnknownCommand kw args ()))++genUnknownHead :: Gen Text+genUnknownHead = (T.pack <$> word) `suchThat` (`notElem` knownCommandWords)+  where+    word = (:) <$> elements ['a'..'z']+               <*> resize 6 (listOf (elements (['a'..'z'] ++ "-")))++knownCommandWords :: [Text]+knownCommandWords =+  [ "set-logic", "set-option", "set-info", "declare-sort-parameter"+  , "declare-sort", "declare-const", "define-const", "declare-datatypes"+  , "declare-datatype", "declare-fun", "define-sort", "define-fun-rec"+  , "define-funs-rec", "define-fun", "push", "pop", "reset-assertions"+  , "reset", "assert", "check-sat-assuming", "check-sat", "get-assertions"+  , "get-assignment", "get-info", "get-model", "get-option", "get-proof"+  , "get-unsat-assumptions", "get-unsat-core", "get-value", "echo", "exit"+  ]++leniencyTests :: TestTree+leniencyTests = testGroup "leniency (unknown commands / responses)"+  [ testProperty "UnknownCommand round-trips via pCommandLenient" $+      \(UnknownCmd c) -> roundTrip pCommandLenient c+  , testCase "strict pCommand rejects an unknown head keyword" $+      assertBool "expected a parse failure" $+        isLeft (parse (sc *> pCommand <* eof) "<l>" "(frobnicate 1 2)")+  , testCase "lenient pCommand keeps an unknown head keyword" $+      case parse (sc *> pCommandLenient <* eof) "<l>" "(frobnicate 1 2)" of+        Right (UnknownCommand kw args _) -> do+          kw @?= "frobnicate"+          length args @?= 2+        _ -> assertFailure "expected UnknownCommand"+  , testCase "lenient pCommand still rejects a malformed known command" $+      assertBool "expected a parse failure" $+        isLeft (parse (sc *> pCommandLenient <* eof) "<l>" "(assert)")+  , testCase "unknown response falls back to ROther" $+      case parse (sc *> pCommandResponse <* eof) "<l>" "(custom-response 1 2)" of+        Right (ROther _) -> pure ()+        _ -> assertFailure "expected ROther"+  , testCase "known responses are still recognized" $+      case parse (sc *> pCommandResponse <* eof) "<l>" "success" of+        Right RSuccess -> pure ()+        _ -> assertFailure "expected RSuccess"+  ]+ -- Framer ---------------------------------------------------------------------  data Outcome = ODone Text Text | OPartial | OFailed FrameError Text@@ -141,6 +203,36 @@   in counterexample (T.unpack txt) $        (direct == Right cmds) .&&. either (const False) (== cmds) perFrame +-- Ord / Hashable instances ---------------------------------------------------++instancesTests :: TestTree+instancesTests = testGroup "Ord / Hashable instances"+  [ testProperty "Eq agrees with Ord (Term)"       (propEqOrd :: Term () -> Term () -> Property)+  , testProperty "Eq agrees with Ord (Command)"    (propEqOrd :: Command () -> Command () -> Property)+  , testProperty "Eq implies equal hash (Term)"    (propEqHash :: Term () -> Property)+  , testProperty "Eq implies equal hash (Command)" (propEqHash :: Command () -> Property)+  , testProperty "usable as Map key (Term)"        (propMapKey :: [Term ()] -> Property)+  , testProperty "usable as HashMap key (Command)" (propHashMapKey :: [Command ()] -> Property)+  ]++-- | The derived 'Ord' must be consistent with the derived 'Eq'.+propEqOrd :: Ord a => a -> a -> Property+propEqOrd x y = (x == y) === (compare x y == EQ)++-- | Structurally-equal values (here, a value against itself) hash equally;+-- this is the law every 'Hashable' instance must satisfy.+propEqHash :: Hashable a => a -> Property+propEqHash x = hash x === hash x++-- | A consistent 'Ord' lets values act as 'Data.Map' keys: a map keyed by a+-- list has exactly as many entries as the list has distinct elements.+propMapKey :: Ord a => [a] -> Property+propMapKey xs = M.size (M.fromList [(x, ()) | x <- xs]) === length (nub xs)++-- | Likewise for 'Data.HashMap' via the 'Hashable'\/'Eq' instances.+propHashMapKey :: Hashable a => [a] -> Property+propHashMapKey xs = HM.size (HM.fromList [(x, ()) | x <- xs]) === length (nub xs)+ -- Sample files ---------------------------------------------------------------  loadSampleTests :: IO TestTree@@ -154,9 +246,17 @@       let smt2 = [ dir </> e | e <- entries, takeExtension e == ".smt2" ]       files <- filterM doesFileExist smt2       cases <- forM files $ \f -> do-        src <- T.readFile f+        src <- readFileUtf8 f         pure (testCase f (assertParsesAndRoundTrips src))       pure (testGroup "samples (parse + render idempotence)" cases)++-- | Read a file as UTF-8, independent of the process's locale encoding.+-- (Sample files contain non-ASCII symbols, so the default locale-based+-- 'T.readFile' would fail under a non-UTF-8 locale such as @C@/@POSIX@.)+readFileUtf8 :: FilePath -> IO Text+readFileUtf8 f = withFile f ReadMode $ \h -> do+  hSetEncoding h utf8+  T.hGetContents h  assertParsesAndRoundTrips :: Text -> Assertion assertParsesAndRoundTrips src =