diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,33 @@ +# Changelog for `language-smtlib` + +All notable changes to this project will be documented in this file. + +The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), +and this project adheres to the +[Haskell Package Versioning Policy](https://pvp.haskell.org/). + +## Unreleased + +## 0.1.0.0 - 2026-06-08 + +- Initial release of the `Text`-based SMT-LIB 2 library. +- Full SMT-LIB 2.7 AST (`Language.SMTLIB.Syntax`) with an optional source-span + annotation parameter on every node, including datatypes, `match` and `par`. +- SMT-LIB 2.7 syntax additions over 2.6: the `lambda` binder, the + `declare-sort-parameter` and `define-const` commands, and the `_` wildcard in + `match` patterns. (The `->` map sort and term-level apply operator `_` already + fit the existing sort/identifier grammar.) +- SMT-LIB 2.7 reference sample scripts under `test/samples/smt/` (Figures 3.11 + and 3.12, plus the `lambda`/`define-const`, `declare-sort-parameter`, and + polymorphic list `match` examples). +- megaparsec-based parser (`Language.SMTLIB.Parser`) with whole-text and + location-free (`parseScript'`/`parseCommand'`/`parseTerm'`) entry points. +- Incremental S-expression framer (`Language.SMTLIB.Parser.SExpr`) with + `Done`/`Partial`/`Failed` results and minimal reads, plus pure + (`Language.SMTLIB.Reader`) and `Handle`-based + (`Language.SMTLIB.Reader.Handle`) incremental readers. +- `prettyprinter`-based printer (`Language.SMTLIB.Printer`) with centralised + symbol/string quoting and a `parse . render == id` guarantee. +- Solver command-response types and parsers (`Language.SMTLIB.*.Response`). +- Test suite: round-trip properties for every AST type, framer unit tests, + framer-vs-parser equivalence, and parse/render idempotence over sample files. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,28 @@ +BSD 3-Clause License + +Copyright (c) 2026, Masahiro Sakai + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,148 @@ +# 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) + +A robust, `Text`-based Haskell library for reading, writing and incrementally +streaming the [SMT-LIB 2](https://smt-lib.org/) format. + +## Features + +- **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. +- **`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 + parameter `a`. Use `()` for a plain tree or `SrcSpan` for one decorated with + source offsets; `noAnn` (= `void`) erases annotations uniformly. +- **Incremental S-expression framer** with attoparsec-`Partial`-style + semantics: it distinguishes *complete* / *needs-more-input* / *error* and + reads only as much as needed to frame one S-expression — so a REPL can prompt + for continuation lines and a pipe driver never blocks reading past one + command. +- **Round-trip guarantee.** `parse . render == id` for well-formed trees; the + printer is the single source of truth for symbol/string quoting. + +## Quick start + +```haskell +{-# LANGUAGE OverloadedStrings #-} +import qualified Data.Text.IO as T +import Language.SMTLIB + +main :: IO () +main = do + src <- T.readFile "problem.smt2" + case parseScript "problem.smt2" src of + Left err -> putStr (errorBundlePretty err) + Right script -> T.putStr (renderScript script) -- canonical re-print +``` + +Parse into location-free trees with `parseScript'` / `parseCommand'` / +`parseTerm'`, or keep spans with `parseScript` / `parseCommand` / `parseTerm`. + +### Incremental input (REPL) + +```haskell +import Language.SMTLIB + +-- frameCommand decides the boundary before parsing: +-- Done (Right cmd) rest -- a command, plus the unconsumed remainder +-- Done (Left err) rest -- a complete frame that failed to parse +-- Partial k -- input ends mid-command: prompt for more, then `feed` +-- Failed fe rest -- a framing error (EndOfInput = clean end of stream) +step = frameCommand "(assert (> x" -- => Partial ... +``` + +### Streaming from a handle or solver pipe + +```haskell +import Language.SMTLIB.Reader.Handle + +driver h = do + r <- newHandleReader h + readCommand r -- reads only until one command is complete; never over-reads +``` + +## Modules + +| Module | Purpose | +| --- | --- | +| `Language.SMTLIB` | umbrella: AST + parser + printer | +| `Language.SMTLIB.Syntax` | the AST (`Term`, `Command`, `Sort`, …) and annotation machinery | +| `Language.SMTLIB.Parser` | whole-text + incremental parsing | +| `Language.SMTLIB.Parser.SExpr` | the low-level incremental framer | +| `Language.SMTLIB.Parser.Response` | solver-response parsers | +| `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 + +``` +stack build +stack test # round-trip properties, framer units, and sample files +``` + +### 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 +[`conformance/README.md`](conformance/README.md). + +### Round-trip checking a corpus of `.smt2` files + +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: + +``` +scripts/roundtrip-check.sh [--build] [--out DIR] [PATH...] +``` + +For each file it runs the parser/printer twice and compares the results: + +- **stage 1** — `parse(src) → out1`; counted as `parse_fail` if the source does + not parse (this just means the input is not standard SMT-LIB 2.7, e.g. a + solver-specific extension, a negative-test file, or non-`smt2` data); +- **stage 2** — `parse(out1) → out2`; counted as `reprint_fail` if our own + output fails to re-parse; +- **compare** — `out1 == out2`; counted as `diff` if the rendering is not + idempotent. + +Because the library contract is `parse . render == id`, a stable canonical +rendering (`out1 == out2`) is a necessary consequence, so any `reprint_fail` or +`diff` flags a genuine parser/printer bug — and the script exits non-zero only +in that case, making it usable as a CI gate. Options: + +- `--build` runs `stack build` first; +- `--out DIR` writes the failing-file lists to `DIR` (`parse-fail.tsv` includes + the first parse-error message for each file); +- `PATH...` are the files and/or directories to scan (directories are searched + recursively for `*.smt2`; default: the current directory). + +``` +# example: build, then check the bundled solver corpora, saving failure lists +scripts/roundtrip-check.sh --build --out /tmp/rt misc +``` diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- | A small command-line front end: parse an SMT-LIB 2 script from a file (or +-- stdin) and re-emit it in canonical form, or report the parse error. +module Main (main) where + +import qualified Data.Text.IO as T +import System.Environment (getArgs) +import System.Exit (exitFailure) +import System.IO (hPutStrLn, stderr) + +import Language.SMTLIB + +main :: IO () +main = do + args <- getArgs + (name, src) <- case args of + [] -> (,) "" <$> 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) diff --git a/conformance/Main.hs b/conformance/Main.hs new file mode 100644 --- /dev/null +++ b/conformance/Main.hs @@ -0,0 +1,265 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE BangPatterns #-} + +-- | A conformance / stress-test driver for large external SMT-LIB 2 benchmark +-- suites (such as the SMT-LIB / SMT-COMP collections published on Zenodo). +-- +-- It walks one or more files or directories, finds every @.smt2@ file, and for +-- each one verifies the library's full round-trip guarantee: +-- +-- * read every command (streaming, one command at a time, so arbitrarily +-- large files use bounded memory); +-- * re-render each command with 'renderText'; +-- * re-parse the rendered text with 'parseCommand''; +-- * check that the re-parsed AST equals the original (modulo source spans). +-- +-- Failures are classified (parse / re-parse / AST mismatch / I\/O) and a summary +-- is printed at the end. The process exits non-zero if any file failed. +-- +-- 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. +-- +-- @ +-- stack build --flag language-smtlib:conformance +-- stack exec language-smtlib-conformance -- benchmarks\/ +-- @ +module Main (main) where + +import Control.Exception (SomeException, try) +import Control.Monad (foldM, forM, when) +import Data.IORef +import Data.List (sort) +import qualified Data.Text as T +import System.Directory (doesDirectoryExist, doesFileExist, listDirectory) +import System.Environment (getArgs, getProgName) +import System.Exit (exitFailure, exitSuccess) +import System.FilePath (takeExtension, ()) +import System.IO + +import Language.SMTLIB +import Language.SMTLIB.Reader.Handle (newHandleReader, readCommand) + +-- --------------------------------------------------------------------------- +-- Options +-- --------------------------------------------------------------------------- + +data Options = Options + { optLimit :: !(Maybe Int) -- ^ process at most this many files + , optQuiet :: !Bool -- ^ suppress per-failure lines (summary only) + , optShowFailures :: !Int -- ^ cap on per-failure lines printed + , optPaths :: ![FilePath] -- ^ files or directories to scan + } + +defaultOptions :: Options +defaultOptions = Options + { optLimit = Nothing + , optQuiet = False + , optShowFailures = 20 + , optPaths = [] + } + +parseArgs :: [String] -> Either String Options +parseArgs = go defaultOptions + where + go opts [] = Right opts { optPaths = reverse (optPaths opts) } + go opts (a : rest) = case a of + "--limit" -> case rest of + (n : rest') -> withInt n (\k -> go opts { optLimit = Just k } rest') + [] -> Left "--limit requires an argument" + "--show-failures" -> case rest of + (n : rest') -> withInt n (\k -> go opts { optShowFailures = k } rest') + [] -> Left "--show-failures requires an argument" + "--quiet" -> go opts { optQuiet = True } rest + _ | take 2 a == "--" -> Left ("unknown option: " ++ a) + | otherwise -> go opts { optPaths = a : optPaths opts } rest + + withInt s k = case reads s of + [(n, "")] -> k n + _ -> Left ("expected an integer, got: " ++ s) + +usage :: String -> String +usage prog = unlines + [ "usage: " ++ prog ++ " [OPTIONS] PATH..." + , "" + , "Round-trip (parse -> render -> re-parse) every .smt2 file under each PATH." + , "A PATH may be a single file or a directory (scanned recursively)." + , "" + , "Options:" + , " --limit N process at most N files" + , " --show-failures N print at most N failure detail lines (default 20)" + , " --quiet only print the final summary" + , " -h, --help show this help" + ] + +-- --------------------------------------------------------------------------- +-- Per-file checking +-- --------------------------------------------------------------------------- + +data FailKind = ParseFail | ReparseFail | MismatchFail | IOFail + deriving (Eq, Ord, Show) + +kindLabel :: FailKind -> String +kindLabel ParseFail = "parse" +kindLabel ReparseFail = "reparse" +kindLabel MismatchFail = "mismatch" +kindLabel IOFail = "io" + +data Failure = Failure + { fKind :: !FailKind + , fMsg :: !String + } + +data Outcome = Outcome + { oCommands :: !Int -- ^ commands successfully read + , oFailure :: !(Maybe Failure) + } + +-- | Stream a single file command-by-command, round-tripping each command. +-- Stops at the first failure (a framing error makes the rest unreliable, and +-- one report per file keeps the output manageable). +checkFile :: FilePath -> IO Outcome +checkFile path = do + res <- try (withFile path ReadMode run) :: IO (Either SomeException Outcome) + pure $ case res of + Left e -> Outcome 0 (Just (Failure IOFail (show e))) + Right o -> o + where + run h = do + hSetEncoding h utf8 + hr <- newHandleReader h + let loop !n = do + r <- readCommand hr + case r of + Left err -> pure (Outcome n (Just (Failure ParseFail err))) + Right Nothing -> pure (Outcome n Nothing) + Right (Just c) -> + let rendered = renderText c + in case parseCommand' "" rendered of + Left e -> pure (Outcome (n + 1) + (Just (Failure ReparseFail (errorBundlePretty e)))) + Right c' + | noAnn c == c' -> loop (n + 1) + | otherwise -> pure (Outcome (n + 1) + (Just (Failure MismatchFail + ("AST changed after render/re-parse; rendered: " + ++ truncateStr 200 (T.unpack rendered))))) + loop 0 + +-- --------------------------------------------------------------------------- +-- File discovery +-- --------------------------------------------------------------------------- + +-- | Collect @.smt2@ files. An explicitly named file is taken as-is regardless +-- of extension; directories are recursed and filtered to @.smt2@. +gather :: FilePath -> IO [FilePath] +gather p = do + isDir <- doesDirectoryExist p + if isDir + then collectDir p + else do + isFile <- doesFileExist p + if isFile + then pure [p] + else do + hPutStrLn stderr ("warning: path not found, skipping: " ++ p) + pure [] + +collectDir :: FilePath -> IO [FilePath] +collectDir d = do + entries <- listDirectory d + fmap concat $ forM (sort entries) $ \e -> do + let p = d e + isDir <- doesDirectoryExist p + if isDir + then collectDir p + else pure [p | takeExtension p == ".smt2"] + +-- --------------------------------------------------------------------------- +-- Driver +-- --------------------------------------------------------------------------- + +main :: IO () +main = do + hSetBuffering stdout LineBuffering + args <- getArgs + prog <- getProgName + if any (`elem` ["-h", "--help"]) args + then putStr (usage prog) >> exitSuccess + else pure () + opts <- case parseArgs args of + Left err -> hPutStrLn stderr (err ++ "\n") >> hPutStr stderr (usage prog) >> exitFailure + Right o -> pure o + when (null (optPaths opts)) $ do + hPutStrLn stderr "error: no paths given\n" + hPutStr stderr (usage prog) + exitFailure + + files0 <- concat <$> mapM gather (optPaths opts) + let files = maybe id take (optLimit opts) files0 + putStrLn ("Found " ++ show (length files) ++ " .smt2 file(s) to check.") + + -- Counters. + cmdTotal <- newIORef (0 :: Integer) + failParse <- newIORef (0 :: Int) + failRepars <- newIORef (0 :: Int) + failMismat <- newIORef (0 :: Int) + failIO <- newIORef (0 :: Int) + printed <- newIORef (0 :: Int) + + let bump ref = modifyIORef' ref (+ 1) + bumpKind ParseFail = bump failParse + bumpKind ReparseFail = bump failRepars + bumpKind MismatchFail = bump failMismat + bumpKind IOFail = bump failIO + + okCount <- foldM + (\ !ok path -> do + o <- checkFile path + modifyIORef' cmdTotal (+ fromIntegral (oCommands o)) + case oFailure o of + Nothing -> pure (ok + 1 :: Int) + Just f -> do + bumpKind (fKind f) + n <- readIORef printed + when (not (optQuiet opts) && n < optShowFailures opts) $ do + writeIORef printed (n + 1) + putStrLn ("FAIL [" ++ kindLabel (fKind f) ++ "] " ++ path + ++ ": " ++ firstLine (fMsg f)) + pure ok) + 0 + files + + -- Summary. + cmds <- readIORef cmdTotal + fp <- readIORef failParse + fr <- readIORef failRepars + fm <- readIORef failMismat + fi <- readIORef failIO + let total = length files + failed = fp + fr + fm + fi + putStrLn "" + putStrLn "==== Summary ====" + putStrLn ("files checked : " ++ show total) + putStrLn (" passed : " ++ show okCount) + putStrLn (" failed : " ++ show failed) + putStrLn ("commands read : " ++ show cmds) + when (failed > 0) $ do + putStrLn "failures by kind:" + putStrLn (" parse : " ++ show fp) + putStrLn (" reparse : " ++ show fr) + putStrLn (" mismatch : " ++ show fm) + putStrLn (" io : " ++ show fi) + if failed > 0 then exitFailure else exitSuccess + +-- --------------------------------------------------------------------------- +-- Helpers +-- --------------------------------------------------------------------------- + +firstLine :: String -> String +firstLine = truncateStr 300 . takeWhile (/= '\n') + +truncateStr :: Int -> String -> String +truncateStr n s = + let (h, t) = splitAt n s + in if null t then h else h ++ "..." diff --git a/conformance/README.md b/conformance/README.md new file mode 100644 --- /dev/null +++ b/conformance/README.md @@ -0,0 +1,90 @@ +# Conformance checker for external SMT-LIB benchmark suites + +This directory contains `language-smtlib-conformance`, a stand-alone driver that +stress-tests the parser and printer against large, real-world SMT-LIB 2 benchmark +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 +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). + +## What it checks + +For every `.smt2` file it finds, the tool verifies the library's full +round-trip guarantee, one command at a time (streaming, so arbitrarily large +files use bounded memory): + +1. read each command with the incremental handle reader + (`Language.SMTLIB.Reader.Handle.readCommand`); +2. re-render it with `renderText`; +3. re-parse the rendered text with `parseCommand'`; +4. assert the re-parsed AST equals the original (modulo source spans, via + `noAnn`). + +Failures are classified as `parse`, `reparse`, `mismatch`, or `io`, and a +summary is printed. The process exits non-zero if any file failed. + +## Workflow + +```sh +# 1. Download benchmarks on your own machine (Zenodo is not reachable from CI). +# List what a record contains: +scripts/fetch-smtlib-benchmarks.sh --record 11061097 --list + +# Fetch a subset (a few logics) or omit the logic names for the whole record: +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) + +# 3. Run it over the downloaded files: +stack exec language-smtlib-conformance -- benchmarks/ +``` + +Or use the convenience wrapper, which builds and runs in one step: + +```sh +scripts/run-conformance.sh benchmarks/ +``` + +### Known Zenodo records + +| Collection | Record id | URL | +| ---------------------------------- | ---------- | ------------------------------------- | +| non-incremental 2023 | `10607722` | | +| non-incremental 2024 | `11061097` | | +| non-incremental 2025 (2025.05.22) | `15493090` | | +| non-incremental 2025 (2025.08.04) | `16740866` | | +| incremental 2023 | `10607775` | | +| incremental 2024 (2024.04.23) | `11061220` | | +| incremental 2024 (2024.05.13) | `11186591` | | +| incremental 2025 | `15493096` | | + +Pass any record id to `--record`; the script reads the actual file list from the +Zenodo REST API, so newer releases work without code changes. + +## Tool options + +``` +language-smtlib-conformance [OPTIONS] PATH... + + --limit N process at most N files + --show-failures N print at most N failure detail lines (default 20) + --quiet only print the final summary + -h, --help show this help +``` + +A `PATH` may be a single `.smt2` file or a directory (scanned recursively). + +## Notes & caveats + +- The download script needs `curl` and either `jq` or `python3` (to read the + Zenodo API), plus `tar --zstd` or the `zstd` tool to extract archives. +- Disk space and time: SMT-LIB archives have a very high compression ratio. + Check the sizes with `--list` before downloading, and prefer a few logics. +- A benchmark the tool cannot parse or round-trip is itself the finding — that + is exactly the kind of coverage gap this checker exists to surface. diff --git a/language-smtlib.cabal b/language-smtlib.cabal new file mode 100644 --- /dev/null +++ b/language-smtlib.cabal @@ -0,0 +1,220 @@ +cabal-version: 2.2 + +-- This file has been generated from package.yaml by hpack version 0.38.1. +-- +-- see: https://github.com/sol/hpack + +name: language-smtlib +version: 0.1.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. + . + It provides a parametric, fully-annotated AST in which every node carries an optional source-span annotation; a megaparsec-based parser with both whole-text and incremental (S-expression framing) entry points, suitable for solver pipes and REPLs; and a prettyprinter-based printer that guarantees @parse . render == id@ for well-formed trees. + . + See the README at for details and examples. +category: Language, SMT +homepage: https://github.com/msakai/language-smtlib#readme +bug-reports: https://github.com/msakai/language-smtlib/issues +author: Masahiro Sakai +maintainer: masahiro.sakai@gmail.com +copyright: 2026 Masahiro Sakai +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple +tested-with: + GHC == 9.6.7 + , GHC == 9.8.4 + , GHC == 9.10.3 + , GHC == 9.12.4 +extra-source-files: + test/samples/smt/assertion-stack-levels-2.smt2 + test/samples/smt/assertion-stack-levels.smt2 + test/samples/smt/assumptions.smt2 + test/samples/smt/chain.smt2 + test/samples/smt/declare-const.smt2 + test/samples/smt/define-fun-rec.smt2 + test/samples/smt/define-funs-rec.smt2 + test/samples/smt/division-by-zero.smt2 + test/samples/smt/echo.smt2 + test/samples/smt/figure-3.11-example-script.smt2 + test/samples/smt/figure-3.12-example-script.smt2 + test/samples/smt/get-assertions.smt2 + test/samples/smt/get-assignment.smt2 + test/samples/smt/get-model.smt2 + test/samples/smt/get-value.smt2 + test/samples/smt/global-declarations.smt2 + test/samples/smt/list-append-match.smt2 + test/samples/smt/print-success.smt2 + test/samples/smt/QF_ABV.smt2 + test/samples/smt/QF_AUFLIA.smt2 + test/samples/smt/QF_BV.smt2 + test/samples/smt/QF_LIA.smt2 + test/samples/smt/QF_LRA.smt2 + test/samples/smt/QF_LRA_2.smt2 + test/samples/smt/QF_UF.smt2 + test/samples/smt/QF_UFLRA.smt2 + test/samples/smt/quoted-symbol.smt2 + test/samples/smt/reset-assertions.smt2 + test/samples/smt/reset.smt2 + test/samples/smt/set-info-status.smt2 + test/samples/smt/smtlib-2.7-check-sat-assuming-terms.smt2 + test/samples/smt/smtlib-2.7-declare-sort-parameter.smt2 + test/samples/smt/smtlib-2.7-lambda-define-const.smt2 + test/samples/smt/swap.smt2 + test/samples/smt/unicode-symbol.smt2 + test/samples/smt/unsat-core.smt2 +extra-doc-files: + README.md + CHANGELOG.md + conformance/README.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. + 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. + manual: True + default: False + +library + exposed-modules: + Language.SMTLIB + Language.SMTLIB.Internal.Lexical + Language.SMTLIB.Parser + Language.SMTLIB.Parser.Command + Language.SMTLIB.Parser.Internal + Language.SMTLIB.Parser.Response + Language.SMTLIB.Parser.SExpr + Language.SMTLIB.Parser.Term + Language.SMTLIB.Printer + Language.SMTLIB.Printer.Class + Language.SMTLIB.Reader + Language.SMTLIB.Reader.Handle + Language.SMTLIB.Syntax + Language.SMTLIB.Syntax.Annotation + Language.SMTLIB.Syntax.Attribute + Language.SMTLIB.Syntax.Command + Language.SMTLIB.Syntax.Constant + Language.SMTLIB.Syntax.Datatype + Language.SMTLIB.Syntax.Identifier + Language.SMTLIB.Syntax.Response + Language.SMTLIB.Syntax.Term + other-modules: + Paths_language_smtlib + autogen-modules: + Paths_language_smtlib + hs-source-dirs: + src + default-extensions: + DeriveFoldable + DeriveFunctor + DeriveTraversable + LambdaCase + OverloadedStrings + PatternSynonyms + TupleSections + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + build-depends: + base >=4.7 && <5 + , containers >=0.6 && <0.8 + , megaparsec >=9.0 && <10 + , parser-combinators >=1.0 && <1.4 + , prettyprinter ==1.7.* + , scientific ==0.3.* + , text >=1.2 && <2.2 + default-language: Haskell2010 + if flag(profiling) + ghc-prof-options: -fprof-auto + +executable language-smtlib-conformance + main-is: Main.hs + other-modules: + Paths_language_smtlib + autogen-modules: + Paths_language_smtlib + hs-source-dirs: + conformance + default-extensions: + DeriveFoldable + DeriveFunctor + DeriveTraversable + LambdaCase + OverloadedStrings + PatternSynonyms + TupleSections + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , directory ==1.3.* + , filepath >=1.4 && <1.6 + , language-smtlib + , text >=1.2 && <2.2 + default-language: Haskell2010 + if !flag(conformance) + buildable: False + if flag(profiling) + ghc-prof-options: -fprof-auto + +executable language-smtlib-exe + main-is: Main.hs + other-modules: + Paths_language_smtlib + autogen-modules: + Paths_language_smtlib + hs-source-dirs: + app + default-extensions: + DeriveFoldable + DeriveFunctor + DeriveTraversable + LambdaCase + OverloadedStrings + PatternSynonyms + TupleSections + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , language-smtlib + , text >=1.2 && <2.2 + default-language: Haskell2010 + if flag(profiling) + ghc-prof-options: -fprof-auto + +test-suite language-smtlib-test + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Arbitrary + Paths_language_smtlib + autogen-modules: + Paths_language_smtlib + hs-source-dirs: + test + default-extensions: + DeriveFoldable + DeriveFunctor + DeriveTraversable + LambdaCase + OverloadedStrings + PatternSynonyms + TupleSections + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + QuickCheck + , base >=4.7 && <5 + , directory + , filepath + , language-smtlib + , megaparsec + , quickcheck-instances + , tasty + , tasty-hunit + , tasty-quickcheck + , text + default-language: Haskell2010 diff --git a/src/Language/SMTLIB.hs b/src/Language/SMTLIB.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB.hs @@ -0,0 +1,31 @@ +-- | Top-level entry point for the SMT-LIB 2 library: the AST, the parser +-- (whole-text and incremental) and the printer. +-- +-- @ +-- import qualified Data.Text.IO as T +-- import Language.SMTLIB +-- +-- main = do +-- src <- T.readFile \"problem.smt2\" +-- case parseScript \"problem.smt2\" src of +-- Left err -> putStr (errorBundlePretty err) +-- Right script -> T.putStr (renderScript script) +-- @ +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) + + -- | Render a megaparsec error bundle (as returned by 'parseScript' and + -- friends) into a human-readable, multi-line string. + , errorBundlePretty + ) where + +import Text.Megaparsec (errorBundlePretty) + +import Language.SMTLIB.Parser +import Language.SMTLIB.Parser.Response +import Language.SMTLIB.Printer +import Language.SMTLIB.Syntax diff --git a/src/Language/SMTLIB/Internal/Lexical.hs b/src/Language/SMTLIB/Internal/Lexical.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Internal/Lexical.hs @@ -0,0 +1,102 @@ +-- | Lexical conventions shared by the parser and the printer: the reserved-word +-- set, the simple-symbol character classes, and string-literal escaping. This +-- is the single source of truth so the two sides cannot drift apart. +module Language.SMTLIB.Internal.Lexical + ( reservedWords + , isSimpleSymbolChar + , isSimpleSymbolStartChar + , isSimpleSymbol + , symbolNeedsQuoting + , escapeStringLit + , unescapeStringLit + ) where + +import Data.Char (isAlpha, isDigit) +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Text (Text) +import qualified Data.Text as T + +-- | 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 + [ "!", "_", "as", "BINARY", "DECIMAL", "exists", "forall" + , "HEXADECIMAL", "lambda", "let", "match", "NUMERAL", "par", "STRING" + ] ++ + -- command names + [ "assert", "check-sat", "check-sat-assuming" + , "declare-const", "declare-datatype", "declare-datatypes" + , "declare-fun", "declare-sort", "declare-sort-parameter" + , "define-const", "define-fun", "define-fun-rec", "define-funs-rec" + , "define-sort" + , "echo", "exit" + , "get-assertions", "get-assignment", "get-info", "get-model" + , "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core" + , "get-value", "pop", "push", "reset", "reset-assertions" + , "set-info", "set-logic", "set-option" + ] + +-- | Whether @c@ is one of the non-alphanumeric characters permitted in a simple +-- symbol (the set @~ ! \@ $ % ^ & * _ - + = < > . ? \/@). +isSpecialChar :: Char -> Bool +isSpecialChar = \case + '~' -> True; '!' -> True; '@' -> True; '$' -> True + '%' -> True; '^' -> True; '&' -> True; '*' -> True + '_' -> True; '-' -> True; '+' -> True; '=' -> True + '<' -> True; '>' -> True; '.' -> True; '?' -> True + '/' -> True; _ -> False + +-- | Whether @c@ may appear anywhere in a simple symbol. +-- +-- The SMT-LIB 2 standard restricts simple-symbol letters to ASCII; as a +-- documented, benign superset (matching what solvers such as z3 accept) we also +-- admit any Unicode letter, so identifiers like @あいうえお@ need no quoting. +-- +-- The ASCII cases are tested first by direct comparison (the overwhelmingly +-- common path); 'isAlpha' is consulted only for non-ASCII code points. +isSimpleSymbolChar :: Char -> Bool +isSimpleSymbolChar c = + (c >= 'a' && c <= 'z') + || (c >= 'A' && c <= 'Z') + || (c >= '0' && c <= '9') + || isSpecialChar c + || (c > '\127' && isAlpha c) + +-- | Whether @c@ may appear as the /first/ character of a simple symbol (i.e. a +-- simple-symbol character that is not a digit). +isSimpleSymbolStartChar :: Char -> Bool +isSimpleSymbolStartChar c = isSimpleSymbolChar c && not (isDigit c) + +-- | Whether a symbol can be rendered without @|...|@ quoting: non-empty, made +-- only of simple-symbol characters, not starting with a digit, and not a +-- reserved word. +isSimpleSymbol :: Text -> Bool +isSimpleSymbol t = case T.uncons t of + Nothing -> False + Just (c, cs) -> + isSimpleSymbolStartChar c + && T.all isSimpleSymbolChar cs + && t `Set.notMember` reservedWords + +-- | Whether a symbol must be quoted on output (the negation of 'isSimpleSymbol'). +symbolNeedsQuoting :: Text -> Bool +symbolNeedsQuoting = not . isSimpleSymbol + +-- | Encode the logical value of a string literal into its quoted body by +-- doubling every double-quote. (Does not add the surrounding quotes.) +escapeStringLit :: Text -> Text +escapeStringLit = T.replace "\"" "\"\"" + +-- | Decode the body of a string literal (the text between the surrounding +-- quotes) by collapsing every doubled double-quote back into one. +unescapeStringLit :: Text -> Text +unescapeStringLit = T.replace "\"\"" "\"" diff --git a/src/Language/SMTLIB/Parser.hs b/src/Language/SMTLIB/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser.hs @@ -0,0 +1,109 @@ +-- | The public parsing API. +-- +-- Two entry styles are offered: +-- +-- * Whole-text parsing ('parseScript', 'parseCommand', 'parseTerm') runs +-- megaparsec over the entire input and yields its rich +-- @ParseErrorBundle@ on failure. +-- +-- * Incremental parsing ('frameCommand') runs the S-expression framer first, +-- 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. +module Language.SMTLIB.Parser + ( -- * Parser monad + P + -- * Errors + , MPError + , ParseError(..) + , prettyParseError + -- * Whole-text parsing + , parseScript + , parseCommand + , parseTerm + , parseWith + -- * Whole-text parsing (plain, location-free trees) + , parseScript' + , parseCommand' + , parseTerm' + -- * Incremental parsing + , frameCommand + -- * Re-exports from the framer + , Result(..) + , FrameError(..) + , feed + , isCleanEnd + , frameSExpr + ) 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.Internal (P, sc) +import Language.SMTLIB.Parser.SExpr +import Language.SMTLIB.Parser.Term (pTerm) +import Language.SMTLIB.Syntax.Annotation (SrcSpan, noAnn) +import Language.SMTLIB.Syntax.Command (Command, Script) +import Language.SMTLIB.Syntax.Term (Term) + +-- | The megaparsec error bundle produced for syntactic errors. +type MPError = ParseErrorBundle Text Void + +-- | A unified parse error: either the framer rejected the input, or megaparsec +-- found a syntax error within a complete frame. +data ParseError + = FramingError FrameError + | SyntaxError MPError + deriving (Show) + +-- | Render a 'ParseError' for human consumption. +prettyParseError :: ParseError -> String +prettyParseError (FramingError e) = "framing error: " ++ show e +prettyParseError (SyntaxError e) = errorBundlePretty e + +runWhole :: P a -> FilePath -> Text -> Either MPError a +runWhole p = runParser (sc *> p <* eof) + +-- | Parse a whole script (zero or more commands). +parseScript :: FilePath -> Text -> Either MPError (Script SrcSpan) +parseScript = runWhole pScript + +-- | Parse a single command. +parseCommand :: FilePath -> Text -> Either MPError (Command SrcSpan) +parseCommand = runWhole pCommand + +-- | Parse a single term. +parseTerm :: FilePath -> Text -> Either MPError (Term SrcSpan) +parseTerm = runWhole pTerm + +-- | Run any parser (e.g. a response parser from +-- "Language.SMTLIB.Parser.Response") over a whole input, requiring it to +-- consume everything. Leading whitespace is skipped automatically. +parseWith :: P a -> FilePath -> Text -> Either MPError a +parseWith p = runWhole p + +-- | Like 'parseScript' but discarding source spans. +parseScript' :: FilePath -> Text -> Either MPError (Script ()) +parseScript' fp = fmap (map noAnn) . parseScript fp + +-- | Like 'parseCommand' but discarding source spans. +parseCommand' :: FilePath -> Text -> Either MPError (Command ()) +parseCommand' fp = fmap noAnn . parseCommand fp + +-- | Like 'parseTerm' but discarding source spans. +parseTerm' :: FilePath -> Text -> Either MPError (Term ()) +parseTerm' fp = fmap noAnn . parseTerm fp + +-- | Incrementally frame and parse one command. +-- +-- The framer decides the boundary, so the result is: +-- +-- * @'Done' ('Right' cmd) rest@ — a command parsed, with the remaining input; +-- * @'Done' ('Left' err) rest@ — a complete frame that failed to parse; +-- * @'Partial' k@ — the input ends mid-command; feed more (a REPL would +-- prompt for a continuation line); +-- * @'Failed' fe rest@ — a framing error (or @EndOfInput@ at a clean end). +frameCommand :: Text -> Result (Either MPError (Command SrcSpan)) +frameCommand = fmap (runParser (sc *> pCommand <* eof) "") . frameSExpr diff --git a/src/Language/SMTLIB/Parser/Command.hs b/src/Language/SMTLIB/Parser/Command.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser/Command.hs @@ -0,0 +1,103 @@ +-- | Parsers for commands, options and info flags. +module Language.SMTLIB.Parser.Command + ( pCommand + , pScript + , pOption + , pInfoFlag + ) where + +import Data.Functor (($>)) +import qualified Data.Text as T +import Text.Megaparsec + +import Language.SMTLIB.Parser.Internal +import Language.SMTLIB.Parser.Term +import Language.SMTLIB.Syntax.Annotation (SrcSpan) +import Language.SMTLIB.Syntax.Command + +-- | A whole script: zero or more commands. (Leading whitespace is the caller's +-- responsibility; see "Language.SMTLIB.Parser".) +pScript :: P (Script SrcSpan) +pScript = many pCommand + +-- | 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@). +pCommand :: P (Command SrcSpan) +pCommand = withSpan $ do + _ <- openP + kw <- pAnyWord + c <- case kw of + "set-logic" -> SetLogic <$> pSymbolRaw + "set-option" -> SetOption <$> pOption + "set-info" -> SetInfo <$> pAttribute + "declare-sort-parameter" -> DeclareSortParameter <$> pSymbolRaw + "declare-sort" -> DeclareSort <$> pSymbolRaw <*> numeral + "declare-const" -> DeclareConst <$> pSymbolRaw <*> pSort + "define-const" -> DefineConst <$> pSymbolRaw <*> pSort <*> pTerm + "declare-datatypes" -> DeclareDatatypes <$> parens (some pSortDec) + <*> parens (some pDatatypeDec) + "declare-datatype" -> DeclareDatatype <$> pSymbolRaw <*> pDatatypeDec + "declare-fun" -> DeclareFun <$> pSymbolRaw <*> parens (many pSort) <*> pSort + "define-sort" -> DefineSort <$> pSymbolRaw <*> parens (many pSymbolRaw) <*> pSort + "define-fun-rec" -> DefineFunRec <$> pFunctionDef + "define-funs-rec" -> DefineFunsRec <$> parens (some pFunctionDec) + <*> parens (some pTerm) + "define-fun" -> DefineFun <$> pFunctionDef + "push" -> Push <$> (numeral <|> pure 1) + "pop" -> Pop <$> (numeral <|> pure 1) + "reset-assertions" -> pure ResetAssertions + "reset" -> pure Reset + "assert" -> Assert <$> pTerm + "check-sat-assuming" -> CheckSatAssuming <$> parens (many pTerm) + "check-sat" -> pure CheckSat + "get-assertions" -> pure GetAssertions + "get-assignment" -> pure GetAssignment + "get-info" -> GetInfo <$> pInfoFlag + "get-model" -> pure GetModel + "get-option" -> GetOption <$> pKeyword + "get-proof" -> pure GetProof + "get-unsat-assumptions" -> pure GetUnsatAssumptions + "get-unsat-core" -> pure GetUnsatCore + "get-value" -> GetValue <$> parens (some pTerm) + "echo" -> Echo <$> pStringLit + "exit" -> pure Exit + _ -> fail ("unknown command: " ++ T.unpack kw) + _ <- closeP + pure c + +-- | An @option@ for @set-option@. +pOption :: P (Option SrcSpan) +pOption = withSpan $ choice + [ tok ":diagnostic-output-channel" *> (DiagnosticOutputChannel <$> pStringLit) + , tok ":global-declarations" *> (GlobalDeclarations <$> pBool) + , tok ":interactive-mode" *> (InteractiveMode <$> pBool) + , tok ":print-success" *> (PrintSuccess <$> pBool) + , tok ":produce-assertions" *> (ProduceAssertions <$> pBool) + , tok ":produce-assignments" *> (ProduceAssignments <$> pBool) + , tok ":produce-models" *> (ProduceModels <$> pBool) + , tok ":produce-proofs" *> (ProduceProofs <$> pBool) + , tok ":produce-unsat-assumptions" *> (ProduceUnsatAssumptions <$> pBool) + , tok ":produce-unsat-cores" *> (ProduceUnsatCores <$> pBool) + , tok ":random-seed" *> (RandomSeed <$> numeral) + , tok ":regular-output-channel" *> (RegularOutputChannel <$> pStringLit) + , tok ":reproducible-resource-limit" *> (ReproducibleResourceLimit <$> numeral) + , tok ":verbosity" *> (Verbosity <$> numeral) + , OptionAttribute <$> pAttribute + ] + +-- | An @info_flag@ for @get-info@. +pInfoFlag :: P (InfoFlag SrcSpan) +pInfoFlag = withSpan $ choice + [ tok ":all-statistics" $> AllStatistics + , tok ":assertion-stack-levels" $> AssertionStackLevels + , tok ":authors" $> Authors + , tok ":error-behavior" $> ErrorBehaviorFlag + , tok ":name" $> InfoName + , tok ":reason-unknown" $> ReasonUnknownFlag + , tok ":version" $> InfoVersion + , InfoFlagKeyword <$> pKeyword + ] diff --git a/src/Language/SMTLIB/Parser/Internal.hs b/src/Language/SMTLIB/Parser/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser/Internal.hs @@ -0,0 +1,238 @@ +-- | The megaparsec lexer and the grammar shared by terms and commands: +-- spec-constants, symbols, keywords, indices, identifiers, sorts, qualified +-- identifiers, s-expressions and attributes. +-- +-- Every node parser is wrapped with 'withSpan', so each AST node is annotated +-- with the t'SrcSpan' it was parsed from. The annotation always occupies the +-- last field of a constructor, which means a fully-applied-but-for-the-span +-- constructor has type @t'SrcSpan' -> node t'SrcSpan'@ — exactly what 'withSpan' +-- consumes. +module Language.SMTLIB.Parser.Internal + ( P + -- * Lexing + , sc + , lexeme + , withSpan + , tok + , openP + , closeP + , parens + , numeral + , pBool + , pStringLit + -- * Lexical tokens + , pSpecConstant + , pSymbolRaw + , pAnyWord + , pKeyword + -- * Shared grammar + , pIndex + , pIdentifier + , pSort + , pQualIdentifier + , pSExpr + , pAttribute + , pAttributeValue + ) where + +import Data.Char (isDigit, isHexDigit) +import Data.Functor (($>)) +import qualified Data.Set as Set +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.Read as TR +import Data.Void (Void) +import Text.Megaparsec +import Text.Megaparsec.Char (char, string) +import qualified Text.Megaparsec.Char.Lexer as L + +import Language.SMTLIB.Internal.Lexical + (isSimpleSymbolChar, isSimpleSymbolStartChar, reservedWords) +import Language.SMTLIB.Syntax.Annotation (SrcSpan(..)) +import Language.SMTLIB.Syntax.Attribute +import Language.SMTLIB.Syntax.Constant +import Language.SMTLIB.Syntax.Identifier + +-- | The concrete parser monad: megaparsec over strict 'Text' with no custom +-- error component. +type P = Parsec Void Text + +-- | The whitespace consumer: spaces and @;@ line comments (SMT-LIB has no block +-- comments). +sc :: P () +sc = L.space spaceChars (L.skipLineComment ";") empty + where spaceChars = () <$ takeWhile1P (Just "white space") isWs + isWs c = c == ' ' || c == '\t' || c == '\n' || c == '\r' + +-- | Run a parser then consume trailing whitespace\/comments. +lexeme :: P a -> P a +lexeme = L.lexeme sc + +-- | Annotate a node with the source span it covers. The supplied parser yields +-- a constructor still awaiting its final t'SrcSpan' field. +withSpan :: P (SrcSpan -> a) -> P a +withSpan p = do + s <- getOffset + f <- p + e <- getOffset + pure (f (SrcSpan s e)) + +-- | Match a fixed token (keyword or reserved word), ensuring it is not merely a +-- prefix of a longer symbol. +tok :: Text -> P () +tok w = (lexeme . try) (string w *> notFollowedBy (satisfy isSimpleSymbolChar)) $> () + +-- | An opening parenthesis (and trailing whitespace). +openP :: P () +openP = lexeme (char '(') $> () + +-- | A closing parenthesis (and trailing whitespace). +closeP :: P () +closeP = lexeme (char ')') $> () + +-- | @parens p@ parses @p@ between a balanced pair of parentheses. +parens :: P a -> P a +parens p = openP *> p <* closeP + +-- | A numeral (sequence of digits). +numeral :: P Integer +numeral = lexeme (readInteger <$> takeWhile1P (Just "digit") isDigit) + +-- | Parse a non-empty run of decimal digits to an 'Integer', reading directly +-- from the 'Text' (no intermediate 'String'). Only ever called on input that +-- the caller has already constrained to one or more digits, so the error case +-- is unreachable. +readInteger :: Text -> Integer +readInteger t = case TR.decimal t of + Right (n, _) -> n + Left e -> error ("readInteger: " ++ e ++ ": " ++ T.unpack t) + +-- | @true@ \/ @false@. +pBool :: P Bool +pBool = (tok "true" $> True) <|> (tok "false" $> False) + +isBinDigit :: Char -> Bool +isBinDigit c = c == '0' || c == '1' + +-- | A @spec_constant@. Numeric literals keep their raw lexeme so that printing +-- round-trips exactly. +pSpecConstant :: P (SpecConstant SrcSpan) +pSpecConstant = withSpan (lexeme (pHash <|> pStr <|> pNumDec)) + where + pHash = char '#' *> (pHex <|> pBin) + pHex = char 'x' *> (SCHexadecimal <$> takeWhile1P (Just "hex digit") isHexDigit) + pBin = char 'b' *> (SCBinary <$> takeWhile1P (Just "binary digit") isBinDigit) + pStr = SCString <$> pStringBody + pNumDec = do + intp <- takeWhile1P (Just "digit") isDigit + mfrac <- optional (char '.' *> takeWhileP (Just "digit") isDigit) + pure $ case mfrac of + Nothing -> SCNumeral (readInteger intp) + Just fr -> SCDecimal (T.concat [intp, ".", fr]) + +-- | The body of a string literal (no trailing whitespace), decoding @""@ into a +-- single quote. +pStringBody :: P Text +pStringBody = char '"' *> go + where + go = do + seg <- takeWhileP (Just "string char") (/= '"') + _ <- char '"' + mq <- optional (char '"') + case mq of + Just _ -> (\rest -> T.concat [seg, "\"", rest]) <$> go + Nothing -> pure seg + +-- | A string literal as a lexeme. +pStringLit :: P Text +pStringLit = lexeme pStringBody + +-- | A symbol (simple or @|...|@ quoted), returning its logical value. Simple +-- symbols that are reserved words are rejected so the grammar's keywords are +-- not swallowed. +pSymbolRaw :: P Symbol +pSymbolRaw = lexeme (pSimple <|> pQuoted) + where + pSimple = try $ do + h <- satisfy isSimpleSymbolStartChar + t <- takeWhileP (Just "symbol char") isSimpleSymbolChar + let s = T.cons h t + if s `Set.member` reservedWords + then fail ("reserved word " ++ T.unpack s) + else pure s + pQuoted = quotedBody + +-- | A @|...|@ quoted symbol body, returning its logical value. +quotedBody :: P Text +quotedBody = char '|' *> takeWhileP (Just "quoted-symbol char") (\c -> c /= '|' && c /= '\\') <* char '|' + +-- | A simple word /including/ reserved words (used inside s-expressions). +pAnyWord :: P Text +pAnyWord = lexeme $ do + h <- satisfy isSimpleSymbolStartChar + t <- takeWhileP (Just "symbol char") isSimpleSymbolChar + pure (T.cons h t) + +-- | A keyword, returned without its leading colon. +pKeyword :: P Keyword +pKeyword = lexeme (char ':' *> takeWhile1P (Just "keyword char") isSimpleSymbolChar) + +-- | An @index@: a numeral or a symbol. +pIndex :: P (Index SrcSpan) +pIndex = withSpan ((IxNumeral <$> numeral) <|> (IxSymbol <$> pSymbolRaw)) + +-- | An @identifier@: a symbol, or @(_ symbol index+)@. +pIdentifier :: P (Identifier SrcSpan) +pIdentifier = withSpan (plain <|> indexed) + where + plain = (\s -> Identifier s []) <$> pSymbolRaw + indexed = do + _ <- openP + _ <- tok "_" + s <- pSymbolRaw + ixs <- some pIndex + _ <- closeP + pure (Identifier s ixs) + +-- | A @sort@: an identifier, or @(identifier sort+)@. +pSort :: P (Sort SrcSpan) +pSort = withSpan (try simple <|> param) + where + simple = (\i -> Sort i []) <$> pIdentifier + param = parens (Sort <$> pIdentifier <*> some pSort) + +-- | A @qual_identifier@: an identifier or @(as identifier sort)@. +pQualIdentifier :: P (QualIdentifier SrcSpan) +pQualIdentifier = withSpan (try asForm <|> plain) + where + asForm = parens (tok "as" *> (QIdentifierAs <$> pIdentifier <*> pSort)) + plain = QIdentifier <$> pIdentifier + +-- | An @s_expr@. +pSExpr :: P (SExpr SrcSpan) +pSExpr = withSpan $ choice + [ SEConstant <$> pSpecConstant + , SEKeyword <$> pKeyword + , SEList <$> parens (many pSExpr) + , wordOrReserved + , SESymbol <$> lexeme quotedBody + ] + where + wordOrReserved = do + w <- pAnyWord + pure (if w `Set.member` reservedWords then SEReserved w else SESymbol w) + +-- | An @attribute_value@. +pAttributeValue :: P (AttributeValue SrcSpan) +pAttributeValue = withSpan $ choice + [ AVConstant <$> pSpecConstant + , AVSExpr <$> parens (many pSExpr) + , AVSymbol <$> pSymbolRaw + ] + +-- | An @attribute@: a keyword, optionally followed by a value. +pAttribute :: P (Attribute SrcSpan) +pAttribute = withSpan $ do + k <- pKeyword + mv <- optional pAttributeValue + pure (maybe (Attribute k) (AttributeWith k) mv) diff --git a/src/Language/SMTLIB/Parser/Response.hs b/src/Language/SMTLIB/Parser/Response.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser/Response.hs @@ -0,0 +1,139 @@ +-- | Parsers for solver command responses. +-- +-- Many responses share the @( ... )@ shape, so they cannot be told apart +-- without knowing which command they answer. This module therefore exposes a +-- per-response parser for each command, plus 'pCommandResponse' for the +-- context-free responses (@success@, @unsupported@, @sat@\/@unsat@\/@unknown@ +-- and @(error ...)@). +module Language.SMTLIB.Parser.Response + ( -- * Combinators + pCommandResponse + , pGeneralResponse + , pCheckSatResponse + , pGetValueResponse + , pGetModelResponse + , pGetAssignmentResponse + , pGetUnsatCoreResponse + , pGetUnsatAssumptionsResponse + , pGetAssertionsResponse + , pGetInfoResponse + , pGetProofResponse + , pGetOptionResponse + , pInfoResponse + , pValuationPair + , pModelResponse + ) where + +import Data.Functor (($>)) +import Text.Megaparsec + +import Language.SMTLIB.Parser.Internal +import Language.SMTLIB.Parser.Term (pFunctionDec, pFunctionDef, pTerm) +import Language.SMTLIB.Syntax.Annotation (SrcSpan) +import Language.SMTLIB.Syntax.Attribute (AttributeValue, SExpr) +import Language.SMTLIB.Syntax.Constant (Symbol) +import Language.SMTLIB.Syntax.Response +import Language.SMTLIB.Syntax.Term (Term) + +-- | The context-free responses (@success@, @unsupported@, the @check-sat@ +-- answers, and @(error ...)@). Use the specific parsers below for +-- list-shaped responses. +pCommandResponse :: P (CommandResponse SrcSpan) +pCommandResponse = choice + [ tok "success" $> RSuccess + , tok "unsupported" $> RUnsupported + , tok "sat" $> RCheckSat Sat + , tok "unsat" $> RCheckSat Unsat + , tok "unknown" $> RCheckSat Unknown + , parens (tok "error" *> (RError <$> pStringLit)) + ] + +-- | @success | unsupported | (error string)@. +pGeneralResponse :: P (CommandResponse SrcSpan) +pGeneralResponse = choice + [ tok "success" $> RSuccess + , tok "unsupported" $> RUnsupported + , parens (tok "error" *> (RError <$> pStringLit)) + ] + +-- | @sat | unsat | unknown@. +pCheckSatResponse :: P CheckSatResponse +pCheckSatResponse = choice + [ tok "sat" $> Sat + , tok "unsat" $> Unsat + , tok "unknown" $> Unknown + ] + +-- | @( (term value)+ )@. +pGetValueResponse :: P [ValuationPair SrcSpan] +pGetValueResponse = parens (some pValuationPair) + +-- | A @(term value)@ pair. +pValuationPair :: P (ValuationPair SrcSpan) +pValuationPair = parens (ValuationPair <$> pTerm <*> pTerm) + +-- | @( model_response* )@, tolerating a legacy leading @model@ keyword. +pGetModelResponse :: P [ModelResponse SrcSpan] +pGetModelResponse = parens (optional (tok "model") *> many pModelResponse) + +-- | A single @model_response@ definition (@define-fun@\/@-rec@\/@-funs-rec@). +pModelResponse :: P (ModelResponse SrcSpan) +pModelResponse = parens $ choice + [ tok "define-fun-rec" *> (MRDefineFunRec <$> pFunctionDef) + , tok "define-funs-rec" *> (MRDefineFunsRec <$> parens (some pFunctionDec) + <*> parens (some pTerm)) + , tok "define-fun" *> (MRDefineFun <$> pFunctionDef) + ] + +-- | @( (symbol b_value)* )@. +pGetAssignmentResponse :: P [(Symbol, Bool)] +pGetAssignmentResponse = parens (many (parens ((,) <$> pSymbolRaw <*> pBool))) + +-- | @( symbol* )@. +pGetUnsatCoreResponse :: P [Symbol] +pGetUnsatCoreResponse = parens (many pSymbolRaw) + +-- | @( term* )@ (SMT-LIB 2.7 generalised assumptions: arbitrary Bool terms). +pGetUnsatAssumptionsResponse :: P [Term SrcSpan] +pGetUnsatAssumptionsResponse = parens (many pTerm) + +-- | @( term* )@. +pGetAssertionsResponse :: P [Term SrcSpan] +pGetAssertionsResponse = parens (many pTerm) + +-- | @( info_response+ )@. +pGetInfoResponse :: P [InfoResponse SrcSpan] +pGetInfoResponse = parens (some pInfoResponse) + +-- | A single @info_response@ entry. +pInfoResponse :: P (InfoResponse SrcSpan) +pInfoResponse = choice + [ tok ":assertion-stack-levels" *> (IRAssertionStackLevels <$> numeral) + , tok ":authors" *> (IRAuthors <$> pStringLit) + , tok ":error-behavior" *> (IRErrorBehavior <$> pErrorBehavior) + , tok ":name" *> (IRName <$> pStringLit) + , tok ":reason-unknown" *> (IRReasonUnknown <$> pReasonUnknown) + , tok ":version" *> (IRVersion <$> pStringLit) + , IRAttribute <$> pAttribute + ] + +pErrorBehavior :: P ErrorBehavior +pErrorBehavior = choice + [ tok "immediate-exit" $> ImmediateExit + , tok "continued-execution" $> ContinuedExecution + ] + +pReasonUnknown :: P (ReasonUnknown SrcSpan) +pReasonUnknown = choice + [ tok "memout" $> RUMemout + , tok "incomplete" $> RUIncomplete + , RUOther <$> pSExpr + ] + +-- | A single @s_expr@. +pGetProofResponse :: P (SExpr SrcSpan) +pGetProofResponse = pSExpr + +-- | An @attribute_value@. +pGetOptionResponse :: P (AttributeValue SrcSpan) +pGetOptionResponse = pAttributeValue diff --git a/src/Language/SMTLIB/Parser/SExpr.hs b/src/Language/SMTLIB/Parser/SExpr.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser/SExpr.hs @@ -0,0 +1,183 @@ +-- | The incremental S-expression framer: the low-level primitive that decides +-- where one complete top-level S-expression ends. +-- +-- It scans 'Text' left-to-right tracking parenthesis depth, string literals, +-- @|...|@ quoted symbols and @;@ line comments, and classifies the input as one +-- of three outcomes ('Result'): +-- +-- * 'Done' — a complete frame, with the unconsumed remainder of the chunk. +-- * 'Partial' — the input ends in the middle of a frame; feed more to +-- continue (this is the \"needs more input\" signal a REPL uses to prompt +-- for a continuation line). +-- * 'Failed' — a lexical framing error. +-- +-- It performs /minimal reads/: it returns 'Done' the instant a frame closes and +-- hands back the remainder, so a pipe driver never consumes past one command. +-- It only asks for more input at genuine ambiguities (an open list, an open +-- string\/quoted symbol, or a trailing @\"@ that might begin a @\"\"@ escape). +-- +-- The framer is deliberately permissive about /syntax/: it accepts any +-- balanced byte sequence and leaves rich syntactic error reporting to the +-- megaparsec layer that re-parses the framed text. +module Language.SMTLIB.Parser.SExpr + ( Result(..) + , FrameError(..) + , feed + , isCleanEnd + , frameSExpr + ) where + +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.Lazy as TL +import Data.Text.Lazy.Builder (Builder) +import qualified Data.Text.Lazy.Builder as B + +-- | The outcome of framing. @a@ is the framed payload (raw 'Text' for +-- 'frameSExpr'). +data Result a + = Done a !Text -- ^ framed value and the unconsumed remainder + | Partial (Text -> Result a) -- ^ feed the next chunk; feed @""@ to signal EOF + | Failed FrameError !Text -- ^ framing error and the remaining input + +-- | Map over the framed payload, threading through 'Partial' continuations. +-- This is how the framed 'Text' of a 'Done' is handed to the megaparsec layer. +instance Functor Result where + fmap f (Done a t) = Done (f a) t + fmap f (Partial k) = Partial (fmap f . k) + fmap _ (Failed e t) = Failed e t + +-- | A framing-level error. 'EndOfInput' is benign: it reports that the stream +-- ended cleanly at a frame boundary with no partial frame in progress. +data FrameError + = UnterminatedString -- ^ EOF inside a @"..."@ literal + | UnterminatedQuotedSymbol -- ^ EOF inside a @|...|@ symbol + | UnterminatedList -- ^ EOF inside a @(...)@ with unmatched @(@ + | UnexpectedCloseParen -- ^ a @)@ with no matching @(@ + | EndOfInput -- ^ stream ended cleanly between frames (not an error) + deriving (Eq, Show) + +-- | Apply the next input chunk to a pending 'Partial'. A non-'Partial' result +-- is returned unchanged. Feed @""@ to signal end of input. +feed :: Result a -> Text -> Result a +feed (Partial k) t = k t +feed r _ = r + +-- | Whether a result is the benign end-of-stream marker (@'Failed' 'EndOfInput'@). +isCleanEnd :: Result a -> Bool +isCleanEnd (Failed EndOfInput _) = True +isCleanEnd _ = False + +-- | Frame exactly one top-level S-expression from the given input, returning +-- the raw 'Text' of the frame (verbatim, including any interior comments and +-- whitespace) on success. +frameSExpr :: Text -> Result Text +frameSExpr = skip False + +-- The accumulator holds the frame characters consumed so far; leading layout +-- (whitespace and comments before the frame) is never accumulated. + +-- | Whitespace recognised between tokens. +isWs :: Char -> Bool +isWs c = c == ' ' || c == '\t' || c == '\n' || c == '\r' + +-- | Characters that terminate a bare top-level atom. +isDelim :: Char -> Bool +isDelim c = isWs c || c == '(' || c == ')' || c == '"' || c == '|' || c == ';' + +toText :: Builder -> Text +toText = TL.toStrict . B.toLazyText + +done :: Builder -> Text -> Result Text +done acc rest = Done (toText acc) rest + +-- | Inner lexical mode while scanning the body of a list. +data Inner = INormal | IComment | IQuo | IStr | IStrQuote + +-- | Skip leading whitespace and comments, then dispatch on the first +-- significant character. The 'Bool' records whether we are currently inside a +-- leading line comment. +skip :: Bool -> Text -> Result Text +skip inComment t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then Failed EndOfInput T.empty else skip inComment more + Just (c, rest) + | inComment -> skip (not (c == '\n' || c == '\r')) rest + | c == ';' -> skip True rest + | isWs c -> skip False rest + | c == '(' -> inList INormal 1 (B.singleton '(') rest + | c == ')' -> Failed UnexpectedCloseParen t + | c == '"' -> inStr (B.singleton '"') rest + | c == '|' -> inQuo (B.singleton '|') rest + | otherwise -> inSimple (B.singleton c) rest + +-- | A bare top-level atom, ending at the first delimiter or at EOF. +inSimple :: Builder -> Text -> Result Text +inSimple acc t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then done acc T.empty else inSimple acc more + Just (c, _) + | isDelim c -> done acc t -- delimiter not consumed + Just (c, rest) -> inSimple (acc <> B.singleton c) rest + +-- | A top-level @"..."@ string literal. +inStr :: Builder -> Text -> Result Text +inStr acc t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then Failed UnterminatedString T.empty else inStr acc more + Just (c, rest) + | c == '"' -> inStrQuote (acc <> B.singleton '"') rest + | otherwise -> inStr (acc <> B.singleton c) rest + +-- | Just consumed a @"@ inside a top-level string; decide whether it closed the +-- string or begins a @""@ escape. +inStrQuote :: Builder -> Text -> Result Text +inStrQuote acc t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then done acc T.empty else inStrQuote acc more -- EOF: string closed + Just (c, rest) + | c == '"' -> inStr (acc <> B.singleton '"') rest -- "" escape + | otherwise -> done acc t -- closed; c is remainder + +-- | A top-level @|...|@ quoted symbol. +inQuo :: Builder -> Text -> Result Text +inQuo acc t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then Failed UnterminatedQuotedSymbol T.empty else inQuo acc more + Just (c, rest) + | c == '|' -> done (acc <> B.singleton '|') rest + | otherwise -> inQuo (acc <> B.singleton c) rest + +-- | Inside a list at the given depth (>= 1). +inList :: Inner -> Int -> Builder -> Text -> Result Text +inList inner depth acc t = case T.uncons t of + Nothing -> Partial $ \more -> + if T.null more then Failed UnterminatedList T.empty + else inList inner depth acc more + Just (c, rest) -> case inner of + INormal -> normalChar depth acc c rest + IComment + | c == '\n' || c == '\r' -> inList INormal depth (acc <> B.singleton c) rest + | otherwise -> inList IComment depth (acc <> B.singleton c) rest + IQuo + | c == '|' -> inList INormal depth (acc <> B.singleton c) rest + | otherwise -> inList IQuo depth (acc <> B.singleton c) rest + IStr + | c == '"' -> inList IStrQuote depth (acc <> B.singleton c) rest + | otherwise -> inList IStr depth (acc <> B.singleton c) rest + IStrQuote + | c == '"' -> inList IStr depth (acc <> B.singleton c) rest -- "" escape + | otherwise -> normalChar depth acc c rest -- string closed + +-- | Process one character in normal (non-string\/comment) list context. +normalChar :: Int -> Builder -> Char -> Text -> Result Text +normalChar depth acc c rest = + let acc' = acc <> B.singleton c in + case c of + '(' -> inList INormal (depth + 1) acc' rest + ')' | depth == 1 -> done acc' rest + | otherwise -> inList INormal (depth - 1) acc' rest + '"' -> inList IStr depth acc' rest + '|' -> inList IQuo depth acc' rest + ';' -> inList IComment depth acc' rest + _ -> inList INormal depth acc' rest diff --git a/src/Language/SMTLIB/Parser/Term.hs b/src/Language/SMTLIB/Parser/Term.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Parser/Term.hs @@ -0,0 +1,131 @@ +-- | Parsers for terms (with their binders and the @match@ form) and for the +-- declaration shapes built on top of them: sorted vars, datatype declarations +-- and function definitions. +module Language.SMTLIB.Parser.Term + ( pTerm + , pVarBinding + , pSortedVar + , pPattern + , pMatchCase + , pSortDec + , pSelectorDec + , pConstructorDec + , pDatatypeDec + , pFunctionDec + , pFunctionDef + ) where + +import Data.Char (isDigit) +import Data.Functor (($>)) +import Text.Megaparsec + +import Language.SMTLIB.Parser.Internal +import Language.SMTLIB.Syntax.Annotation (SrcSpan) +import Language.SMTLIB.Syntax.Constant (Symbol) +import Language.SMTLIB.Syntax.Datatype +import Language.SMTLIB.Syntax.Term + +-- | A @term@. +-- +-- The first character selects the form directly instead of attempting and +-- rolling back alternatives: a non-paren term is a spec-constant (digit, @#@ or +-- @\"@) or a bare symbol; a paren term is dispatched by 'parenCompound'. +pTerm :: P (Term SrcSpan) +pTerm = withSpan $ do + c <- lookAhead anySingle + case c of + '(' -> parenCompound + _ | isConstStart c -> TConstant <$> pSpecConstant + | otherwise -> TQualIdent <$> pQualIdentifier + where + isConstStart x = isDigit x || x == '#' || x == '"' + +-- | A parenthesised compound term: a binder +-- (@let@\/@lambda@\/@forall@\/@exists@), @match@, @!@, a qualified identifier +-- used directly (@(as ...)@ or @(_ ...)@), or an application. +-- +-- The head word immediately after the @(@ is peeked (without committing) to +-- choose the form, so no alternative has to be parsed and rolled back. The +-- @(as ...)@ \/ @(_ ...)@ cases delegate to 'pQualIdentifier', which consumes +-- the paren itself; the other cases consume it here. +parenCompound :: P (SrcSpan -> Term SrcSpan) +parenCompound = do + mw <- lookAhead (openP *> optional pAnyWord) + case mw of + Just "let" -> binder (TLet <$> parens (some pVarBinding) <*> pTerm) + Just "lambda" -> binder (TLambda <$> parens (some pSortedVar) <*> pTerm) + Just "forall" -> binder (TForall <$> parens (some pSortedVar) <*> pTerm) + Just "exists" -> binder (TExists <$> parens (some pSortedVar) <*> pTerm) + Just "match" -> binder (TMatch <$> pTerm <*> parens (some pMatchCase)) + Just "!" -> binder (TAnnot <$> pTerm <*> some pAttribute) + Just "as" -> TQualIdent <$> pQualIdentifier + Just "_" -> TQualIdent <$> pQualIdentifier + _ -> openP *> (TApp <$> pQualIdentifier <*> some pTerm) <* closeP + where + -- consume @(@ and the (already-peeked) head keyword, then the body + binder body = openP *> pAnyWord *> body <* closeP + +-- | A @var_binding@ @(symbol term)@. +pVarBinding :: P (VarBinding SrcSpan) +pVarBinding = withSpan (parens (VarBinding <$> pSymbolRaw <*> pTerm)) + +-- | A @sorted_var@ @(symbol sort)@. +pSortedVar :: P (SortedVar SrcSpan) +pSortedVar = withSpan (parens (SortedVar <$> pSymbolRaw <*> pSort)) + +-- | A @pattern@: a single symbol, or @(constructor x1 ... xn)@. The bound +-- variables (and a whole single-symbol pattern) may be the @_@ wildcard +-- (SMT-LIB 2.7); the constructor symbol itself may not. +pPattern :: P (Pattern SrcSpan) +pPattern = withSpan (pvar <|> ctor) + where + pvar = PVar <$> pPatternSymbol + ctor = parens (PCtor <$> pSymbolRaw <*> some pPatternSymbol) + +-- | A symbol in a @match@ pattern binding position: an ordinary symbol or the +-- @_@ wildcard. @_@ is otherwise a reserved word, so 'pSymbolRaw' rejects it. +pPatternSymbol :: P Symbol +pPatternSymbol = pSymbolRaw <|> (tok "_" $> "_") + +-- | A @match_case@ @(pattern term)@. +pMatchCase :: P (MatchCase SrcSpan) +pMatchCase = withSpan (parens (MatchCase <$> pPattern <*> pTerm)) + +-- | A @sort_dec@ @(symbol numeral)@. +pSortDec :: P (SortDec SrcSpan) +pSortDec = withSpan (parens (SortDec <$> pSymbolRaw <*> numeral)) + +-- | A @selector_dec@ @(symbol sort)@. +pSelectorDec :: P (SelectorDec SrcSpan) +pSelectorDec = withSpan (parens (SelectorDec <$> pSymbolRaw <*> pSort)) + +-- | A @constructor_dec@ @(symbol selector_dec*)@. +pConstructorDec :: P (ConstructorDec SrcSpan) +pConstructorDec = withSpan (parens (ConstructorDec <$> pSymbolRaw <*> many pSelectorDec)) + +-- | A @datatype_dec@: @(constructor_dec+)@ or @(par (u+) (constructor_dec+))@. +pDatatypeDec :: P (DatatypeDec SrcSpan) +pDatatypeDec = withSpan $ do + _ <- openP + r <- par <|> nonPar + _ <- closeP + pure r + where + par = tok "par" *> (DatatypeDec <$> parens (some pSymbolRaw) + <*> parens (some pConstructorDec)) + nonPar = DatatypeDec [] <$> some pConstructorDec + +-- | A @function_dec@ @(symbol (sorted_var*) sort)@. +pFunctionDec :: P (FunctionDec SrcSpan) +pFunctionDec = + withSpan (parens (FunctionDec <$> pSymbolRaw + <*> parens (many pSortedVar) + <*> pSort)) + +-- | A @function_def@ @symbol (sorted_var*) sort term@ (no surrounding parens). +pFunctionDef :: P (FunctionDef SrcSpan) +pFunctionDef = + withSpan (FunctionDef <$> pSymbolRaw + <*> parens (many pSortedVar) + <*> pSort + <*> pTerm) diff --git a/src/Language/SMTLIB/Printer.hs b/src/Language/SMTLIB/Printer.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Printer.hs @@ -0,0 +1,50 @@ +-- | Rendering the SMT-LIB AST to 'Text'. +-- +-- The default layout puts each top-level form on a single line (no automatic +-- line breaks), which keeps the output deterministic and trivially +-- round-trippable. t'RenderOptions' lets callers opt into a wrapped layout. +module Language.SMTLIB.Printer + ( Pretty(..) + , RenderOptions(..) + , defaultRenderOptions + , render + , renderText + , renderTextWith + , renderScript + ) where + +import Data.Text (Text) +import qualified Data.Text as T +import Prettyprinter (Doc, LayoutOptions(..), PageWidth(..), layoutPretty) +import Prettyprinter.Render.Text (renderStrict) + +import Language.SMTLIB.Printer.Class (Pretty(..)) +import Language.SMTLIB.Syntax.Command (Script) + +-- | Layout configuration. +newtype RenderOptions = RenderOptions + { roPageWidth :: PageWidth + -- ^ 'Unbounded' (the default) keeps every form on one line. + } + +-- | Single-line layout: each form rendered without automatic wrapping. +defaultRenderOptions :: RenderOptions +defaultRenderOptions = RenderOptions { roPageWidth = Unbounded } + +-- | Render any 'Doc' to 'Text' with the given options. +render :: RenderOptions -> Doc ann -> Text +render opts = renderStrict . layoutPretty layoutOpts + where layoutOpts = LayoutOptions { layoutPageWidth = roPageWidth opts } + +-- | Render a single AST node to 'Text' using 'defaultRenderOptions'. +renderText :: Pretty a => a -> Text +renderText = renderTextWith defaultRenderOptions + +-- | Render a single AST node to 'Text' with explicit options. +renderTextWith :: Pretty a => RenderOptions -> a -> Text +renderTextWith opts = render opts . pretty + +-- | Render a whole script, one command per line, terminated by a newline. +renderScript :: Script a -> Text +renderScript [] = T.empty +renderScript cmds = T.unlines (map renderText cmds) diff --git a/src/Language/SMTLIB/Printer/Class.hs b/src/Language/SMTLIB/Printer/Class.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Printer/Class.hs @@ -0,0 +1,308 @@ +{-# LANGUAGE FlexibleInstances #-} + +-- | The 'Pretty' class that renders the SMT-LIB AST back to concrete syntax, +-- together with the symbol\/keyword\/string quoting rules. Annotations are +-- ignored, so @pretty x == pretty (noAnn x)@ for every node. +-- +-- Quoting is centralised here ('prettySymbol', 'prettyKeyword', +-- 'prettyStringLit') and always derives the surface form from the /logical/ +-- value, which guarantees @parse . render == id@ for well-formed trees. +module Language.SMTLIB.Printer.Class + ( Pretty(..) + , prettySymbol + , prettyKeyword + , prettyStringLit + , prettyBool + ) where + +import Data.Text (Text) +import qualified Data.Text as T +import Prettyprinter (Doc, (<+>), hsep, parens) +import qualified Prettyprinter as PP + +import Language.SMTLIB.Internal.Lexical + (escapeStringLit, symbolNeedsQuoting) +import Language.SMTLIB.Syntax.Attribute +import Language.SMTLIB.Syntax.Command +import Language.SMTLIB.Syntax.Constant +import Language.SMTLIB.Syntax.Datatype +import Language.SMTLIB.Syntax.Identifier +import Language.SMTLIB.Syntax.Response +import Language.SMTLIB.Syntax.Term + +-- | Render an AST node to a 'Doc'. The renderers in +-- "Language.SMTLIB.Printer" turn the result into 'Text'. +class Pretty a where + pretty :: a -> Doc ann + +text :: Text -> Doc ann +text = PP.pretty + +int :: Integer -> Doc ann +int = PP.pretty + +-- | Render a symbol, quoting with @|...|@ when it is not a simple symbol. +prettySymbol :: Symbol -> Doc ann +prettySymbol s + | symbolNeedsQuoting s = text (T.concat ["|", s, "|"]) + | otherwise = text s + +-- | Render a symbol that appears in a @match@ pattern binding position. The +-- @_@ wildcard (SMT-LIB 2.7) is printed bare; every other symbol follows the +-- usual quoting rules (note @_@ is otherwise a reserved word). +prettyPatternSymbol :: Symbol -> Doc ann +prettyPatternSymbol s + | s == "_" = text "_" + | otherwise = prettySymbol s + +-- | Render a keyword (stored without its colon) as @:keyword@. +prettyKeyword :: Keyword -> Doc ann +prettyKeyword k = text (T.cons ':' k) + +-- | Render the logical value of a string as a quoted, escaped string literal. +prettyStringLit :: Text -> Doc ann +prettyStringLit s = text (T.concat ["\"", escapeStringLit s, "\""]) + +-- | Render a boolean as @true@ \/ @false@. +prettyBool :: Bool -> Doc ann +prettyBool True = text "true" +prettyBool False = text "false" + +-- | @(head args...)@, dropping to just @head@ when there are no args. +app :: Doc ann -> [Doc ann] -> Doc ann +app hd [] = hd +app hd xs = parens (hsep (hd : xs)) + +instance Pretty (SpecConstant a) where + pretty = \case + SCNumeral n _ -> int n + SCDecimal t _ -> text t + SCHexadecimal t _ -> text (T.append "#x" t) + SCBinary t _ -> text (T.append "#b" t) + SCString t _ -> prettyStringLit t + +instance Pretty (Index a) where + pretty = \case + IxNumeral n _ -> int n + IxSymbol s _ -> prettySymbol s + +instance Pretty (Identifier a) where + pretty (Identifier s [] _) = prettySymbol s + pretty (Identifier s ixs _) = + parens (hsep (text "_" : prettySymbol s : map pretty ixs)) + +instance Pretty (Sort a) where + pretty (Sort i args _) = app (pretty i) (map pretty args) + +instance Pretty (QualIdentifier a) where + pretty = \case + QIdentifier i _ -> pretty i + QIdentifierAs i s _ -> parens (text "as" <+> pretty i <+> pretty s) + +instance Pretty (SExpr a) where + pretty = \case + SEConstant c _ -> pretty c + SESymbol s _ -> prettySymbol s + SEKeyword k _ -> prettyKeyword k + SEReserved s _ -> text s + SEList xs _ -> parens (hsep (map pretty xs)) + +instance Pretty (AttributeValue a) where + pretty = \case + AVConstant c _ -> pretty c + AVSymbol s _ -> prettySymbol s + AVSExpr xs _ -> parens (hsep (map pretty xs)) + +instance Pretty (Attribute a) where + pretty = \case + Attribute k _ -> prettyKeyword k + AttributeWith k v _ -> prettyKeyword k <+> pretty v + +instance Pretty (VarBinding a) where + pretty (VarBinding s t _) = parens (prettySymbol s <+> pretty t) + +instance Pretty (SortedVar a) where + pretty (SortedVar s srt _) = parens (prettySymbol s <+> pretty srt) + +instance Pretty (Pattern a) where + pretty = \case + PVar s _ -> prettyPatternSymbol s + PCtor c xs _ -> parens (hsep (prettySymbol c : map prettyPatternSymbol xs)) + +instance Pretty (MatchCase a) where + pretty (MatchCase p t _) = parens (pretty p <+> pretty t) + +instance Pretty (Term a) where + pretty = \case + TConstant c _ -> pretty c + TQualIdent q _ -> pretty q + TApp q args _ -> parens (hsep (pretty q : map pretty args)) + TLet bs t _ -> + parens (text "let" <+> parens (hsep (map pretty bs)) <+> pretty t) + TLambda vs t _ -> + parens (text "lambda" <+> parens (hsep (map pretty vs)) <+> pretty t) + TForall vs t _ -> + parens (text "forall" <+> parens (hsep (map pretty vs)) <+> pretty t) + TExists vs t _ -> + parens (text "exists" <+> parens (hsep (map pretty vs)) <+> pretty t) + TMatch t cs _ -> + parens (text "match" <+> pretty t <+> parens (hsep (map pretty cs))) + TAnnot t as _ -> + parens (hsep (text "!" : pretty t : map pretty as)) + +instance Pretty (SortDec a) where + pretty (SortDec s n _) = parens (prettySymbol s <+> int n) + +instance Pretty (SelectorDec a) where + pretty (SelectorDec s srt _) = parens (prettySymbol s <+> pretty srt) + +instance Pretty (ConstructorDec a) where + pretty (ConstructorDec s sels _) = + parens (hsep (prettySymbol s : map pretty sels)) + +instance Pretty (DatatypeDec a) where + pretty (DatatypeDec [] ctors _) = parens (hsep (map pretty ctors)) + pretty (DatatypeDec ps ctors _) = + parens (text "par" + <+> parens (hsep (map prettySymbol ps)) + <+> parens (hsep (map pretty ctors))) + +instance Pretty (FunctionDec a) where + pretty (FunctionDec s vs srt _) = + parens (prettySymbol s <+> parens (hsep (map pretty vs)) <+> pretty srt) + +-- | A t'FunctionDef' renders /without/ surrounding parens, since the enclosing +-- command supplies them. +instance Pretty (FunctionDef a) where + pretty (FunctionDef s vs srt t _) = + prettySymbol s <+> parens (hsep (map pretty vs)) <+> pretty srt <+> pretty t + +instance Pretty (Option a) where + pretty = \case + DiagnosticOutputChannel s _ -> text ":diagnostic-output-channel" <+> prettyStringLit s + GlobalDeclarations b _ -> text ":global-declarations" <+> prettyBool b + InteractiveMode b _ -> text ":interactive-mode" <+> prettyBool b + PrintSuccess b _ -> text ":print-success" <+> prettyBool b + ProduceAssertions b _ -> text ":produce-assertions" <+> prettyBool b + ProduceAssignments b _ -> text ":produce-assignments" <+> prettyBool b + ProduceModels b _ -> text ":produce-models" <+> prettyBool b + ProduceProofs b _ -> text ":produce-proofs" <+> prettyBool b + ProduceUnsatAssumptions b _ -> text ":produce-unsat-assumptions" <+> prettyBool b + ProduceUnsatCores b _ -> text ":produce-unsat-cores" <+> prettyBool b + RandomSeed n _ -> text ":random-seed" <+> int n + RegularOutputChannel s _ -> text ":regular-output-channel" <+> prettyStringLit s + ReproducibleResourceLimit n _ -> text ":reproducible-resource-limit" <+> int n + Verbosity n _ -> text ":verbosity" <+> int n + OptionAttribute attr _ -> pretty attr + +instance Pretty (InfoFlag a) where + pretty = \case + AllStatistics _ -> text ":all-statistics" + AssertionStackLevels _ -> text ":assertion-stack-levels" + Authors _ -> text ":authors" + ErrorBehaviorFlag _ -> text ":error-behavior" + InfoName _ -> text ":name" + ReasonUnknownFlag _ -> text ":reason-unknown" + InfoVersion _ -> text ":version" + InfoFlagKeyword k _ -> prettyKeyword k + +instance Pretty (Command a) where + pretty = \case + SetLogic s _ -> parens (text "set-logic" <+> prettySymbol s) + SetOption o _ -> parens (text "set-option" <+> pretty o) + SetInfo attr _ -> parens (text "set-info" <+> pretty attr) + DeclareSort s n _ -> parens (text "declare-sort" <+> prettySymbol s <+> int n) + DeclareSortParameter s _ -> parens (text "declare-sort-parameter" <+> prettySymbol s) + DefineSort s args srt _ -> + parens (text "define-sort" <+> prettySymbol s + <+> parens (hsep (map prettySymbol args)) <+> pretty srt) + DeclareConst s srt _ -> parens (text "declare-const" <+> prettySymbol s <+> pretty srt) + DefineConst s srt t _ -> + parens (text "define-const" <+> prettySymbol s <+> pretty srt <+> pretty t) + DeclareFun s args ret _ -> + parens (text "declare-fun" <+> prettySymbol s + <+> parens (hsep (map pretty args)) <+> pretty ret) + DefineFun fd _ -> parens (text "define-fun" <+> pretty fd) + DefineFunRec fd _ -> parens (text "define-fun-rec" <+> pretty fd) + DefineFunsRec decs ts _ -> + parens (text "define-funs-rec" + <+> parens (hsep (map pretty decs)) + <+> parens (hsep (map pretty ts))) + DeclareDatatype s dd _ -> parens (text "declare-datatype" <+> prettySymbol s <+> pretty dd) + DeclareDatatypes sds dds _ -> + parens (text "declare-datatypes" + <+> parens (hsep (map pretty sds)) + <+> parens (hsep (map pretty dds))) + Push n _ -> parens (text "push" <+> int n) + Pop n _ -> parens (text "pop" <+> int n) + Reset _ -> parens (text "reset") + ResetAssertions _ -> parens (text "reset-assertions") + Assert t _ -> parens (text "assert" <+> pretty t) + CheckSat _ -> parens (text "check-sat") + CheckSatAssuming ts _ -> parens (text "check-sat-assuming" <+> parens (hsep (map pretty ts))) + GetAssertions _ -> parens (text "get-assertions") + GetModel _ -> parens (text "get-model") + GetProof _ -> parens (text "get-proof") + GetUnsatCore _ -> parens (text "get-unsat-core") + GetUnsatAssumptions _ -> parens (text "get-unsat-assumptions") + GetValue ts _ -> parens (text "get-value" <+> parens (hsep (map pretty ts))) + GetAssignment _ -> parens (text "get-assignment") + GetOption k _ -> parens (text "get-option" <+> prettyKeyword k) + GetInfo flag _ -> parens (text "get-info" <+> pretty flag) + Echo s _ -> parens (text "echo" <+> prettyStringLit s) + Exit _ -> parens (text "exit") + +instance Pretty CheckSatResponse where + pretty Sat = text "sat" + pretty Unsat = text "unsat" + pretty Unknown = text "unknown" + +instance Pretty ErrorBehavior where + pretty ImmediateExit = text "immediate-exit" + pretty ContinuedExecution = text "continued-execution" + +instance Pretty (ReasonUnknown a) where + pretty = \case + RUMemout -> text "memout" + RUIncomplete -> text "incomplete" + RUOther e -> pretty e + +instance Pretty (InfoResponse a) where + pretty = \case + IRAssertionStackLevels n -> text ":assertion-stack-levels" <+> int n + IRAuthors s -> text ":authors" <+> prettyStringLit s + IRErrorBehavior b -> text ":error-behavior" <+> pretty b + IRName s -> text ":name" <+> prettyStringLit s + IRReasonUnknown r -> text ":reason-unknown" <+> pretty r + IRVersion s -> text ":version" <+> prettyStringLit s + IRAttribute attr -> pretty attr + +instance Pretty (ValuationPair a) where + pretty (ValuationPair t v) = parens (pretty t <+> pretty v) + +instance Pretty (ModelResponse a) where + pretty = \case + MRDefineFun fd -> parens (text "define-fun" <+> pretty fd) + MRDefineFunRec fd -> parens (text "define-fun-rec" <+> pretty fd) + MRDefineFunsRec ds ts -> + parens (text "define-funs-rec" + <+> parens (hsep (map pretty ds)) + <+> parens (hsep (map pretty ts))) + +instance Pretty (CommandResponse a) where + pretty = \case + RSuccess -> text "success" + RUnsupported -> text "unsupported" + RError s -> parens (text "error" <+> prettyStringLit s) + RCheckSat r -> pretty r + REcho s -> prettyStringLit s + RGetAssertions ts -> parens (hsep (map pretty ts)) + RGetAssignment ps -> parens (hsep (map assignPair ps)) + RGetInfo irs -> parens (hsep (map pretty irs)) + RGetModel ms -> parens (hsep (map pretty ms)) + RGetOption v -> pretty v + RGetProof e -> pretty e + RGetUnsatAssumptions ts -> parens (hsep (map pretty ts)) + RGetUnsatCore ss -> parens (hsep (map prettySymbol ss)) + RGetValue vps -> parens (hsep (map pretty vps)) + where assignPair (s, b) = parens (prettySymbol s <+> prettyBool b) diff --git a/src/Language/SMTLIB/Reader.hs b/src/Language/SMTLIB/Reader.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Reader.hs @@ -0,0 +1,42 @@ +-- | Pure helpers for the incremental S-expression reader. Re-exports the +-- framer primitives and adds bulk\/whole-text conveniences built on top of them. +module Language.SMTLIB.Reader + ( -- * Framer primitives (re-exported) + Result(..) + , FrameError(..) + , feed + , isCleanEnd + , frameSExpr + -- * Whole-text helpers + , frameAll + , frameOne + ) where + +import Data.Text (Text) + +import Language.SMTLIB.Parser.SExpr + +-- | Frame a single complete S-expression from @t@, signalling end-of-input so +-- that an incomplete frame becomes a 'FrameError' rather than a 'Partial'. +-- +-- Returns @Right (Just (frame, remainder))@ on success, @Right Nothing@ if @t@ +-- holds only whitespace\/comments, or @Left err@ on an incomplete or invalid +-- frame. +frameOne :: Text -> Either FrameError (Maybe (Text, Text)) +frameOne t = case feed (frameSExpr t) "" of + Done f rest -> Right (Just (f, rest)) + Failed EndOfInput _ -> Right Nothing + Failed e _ -> Left e + Partial _ -> Right Nothing -- unreachable: EOF resolves every Partial + +-- | Split a complete input into its top-level S-expression frames. The second +-- component is 'Just' an error when the trailing input is an incomplete or +-- malformed frame (the successfully framed prefix is still returned). +frameAll :: Text -> ([Text], Maybe FrameError) +frameAll = go [] + where + go acc t = case feed (frameSExpr t) "" of + Done f rest -> go (f : acc) rest + Failed EndOfInput _ -> (reverse acc, Nothing) + Failed e _ -> (reverse acc, Just e) + Partial _ -> (reverse acc, Nothing) -- unreachable after EOF diff --git a/src/Language/SMTLIB/Reader/Handle.hs b/src/Language/SMTLIB/Reader/Handle.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Reader/Handle.hs @@ -0,0 +1,73 @@ +-- | Reading S-expressions and commands incrementally from a 'Handle' (a file, a +-- socket, or a pipe to a running solver). +-- +-- A t'HandleReader' buffers any input read past the end of one frame, so the +-- next read resumes from it. Crucially, it reads from the handle /only/ while a +-- frame is still incomplete: once a frame closes it returns immediately without +-- touching the handle, so it never blocks waiting for input beyond the command +-- it has already received. Reads use 'T.hGetChunk', which returns whatever is +-- currently available rather than waiting to fill a buffer. +-- +-- This module deliberately does not manage solver subprocesses; it provides the +-- reading primitive that such a driver builds on. +module Language.SMTLIB.Reader.Handle + ( HandleReader + , newHandleReader + , readSExpr + , readCommand + ) where + +import Data.IORef +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import System.IO (Handle) +import Text.Megaparsec (eof, errorBundlePretty, parse) + +import Language.SMTLIB.Parser.Command (pCommand) +import Language.SMTLIB.Parser.Internal (sc) +import Language.SMTLIB.Parser.SExpr +import Language.SMTLIB.Syntax.Annotation (SrcSpan) +import Language.SMTLIB.Syntax.Command (Command) + +-- | A handle paired with a buffer of input read past the previous frame. +data HandleReader = HandleReader + { hrHandle :: !Handle + , hrLeftover :: !(IORef Text) + } + +-- | Create a reader over a handle. +newHandleReader :: Handle -> IO HandleReader +newHandleReader h = HandleReader h <$> newIORef T.empty + +-- | Read the next complete top-level S-expression as raw 'Text'. +-- +-- * @'Right' ('Just' frame)@ — a complete frame; +-- * @'Right' 'Nothing'@ — the stream ended cleanly with no further frame; +-- * @'Left' err@ — a framing error (e.g. unbalanced parentheses, EOF inside a +-- string). +readSExpr :: HandleReader -> IO (Either FrameError (Maybe Text)) +readSExpr hr = do + leftover <- readIORef (hrLeftover hr) + drive (frameSExpr leftover) + where + drive (Done frame rest) = do + writeIORef (hrLeftover hr) rest + pure (Right (Just frame)) + drive (Failed EndOfInput _) = pure (Right Nothing) + drive (Failed e _) = pure (Left e) + drive (Partial k) = do + chunk <- T.hGetChunk (hrHandle hr) -- "" at EOF; never reads more than available + drive (k chunk) + +-- | Read and parse the next complete command. Returns @Right Nothing@ at a +-- clean end of stream, @Left msg@ on a framing or syntax error. +readCommand :: HandleReader -> IO (Either String (Maybe (Command SrcSpan))) +readCommand hr = do + r <- readSExpr hr + pure $ case r of + Left fe -> Left ("framing error: " ++ show fe) + Right Nothing -> Right Nothing + Right (Just txt) -> case parse (sc *> pCommand <* eof) "" txt of + Left e -> Left (errorBundlePretty e) + Right c -> Right (Just c) diff --git a/src/Language/SMTLIB/Syntax.hs b/src/Language/SMTLIB/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax.hs @@ -0,0 +1,24 @@ +-- | The full SMT-LIB 2 abstract syntax tree. +-- +-- Every node type takes a final annotation type parameter @a@; use @()@ for a +-- plain tree or t'SrcSpan' for one decorated with source positions. This module +-- re-exports all of the individual @Language.SMTLIB.Syntax.*@ modules. +module Language.SMTLIB.Syntax + ( module Language.SMTLIB.Syntax.Annotation + , module Language.SMTLIB.Syntax.Constant + , module Language.SMTLIB.Syntax.Identifier + , module Language.SMTLIB.Syntax.Attribute + , module Language.SMTLIB.Syntax.Term + , module Language.SMTLIB.Syntax.Datatype + , module Language.SMTLIB.Syntax.Command + , module Language.SMTLIB.Syntax.Response + ) where + +import Language.SMTLIB.Syntax.Annotation +import Language.SMTLIB.Syntax.Attribute +import Language.SMTLIB.Syntax.Command +import Language.SMTLIB.Syntax.Constant +import Language.SMTLIB.Syntax.Datatype +import Language.SMTLIB.Syntax.Identifier +import Language.SMTLIB.Syntax.Response +import Language.SMTLIB.Syntax.Term diff --git a/src/Language/SMTLIB/Syntax/Annotation.hs b/src/Language/SMTLIB/Syntax/Annotation.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Annotation.hs @@ -0,0 +1,35 @@ +-- | Source-location machinery for the (optionally) annotated SMT-LIB AST. +-- +-- Every AST node carries a final type parameter @a@ that holds an annotation. +-- Use @()@ for a plain, location-free tree and t'SrcSpan' for a tree decorated +-- with source positions. Because the annotation always sits in the last field +-- of every constructor, the AST types derive 'Functor'/'Foldable'/'Traversable' +-- over @a@, so 'noAnn' (= 'void') erases all annotations uniformly. +module Language.SMTLIB.Syntax.Annotation + ( SrcSpan(..) + , Annotated(..) + , noAnn + ) where + +import Data.Functor (void) + +-- | A half-open span @[spanStart, spanEnd)@ in the source text, measured in +-- 0-based character offsets. Offsets (rather than line\/column pairs) keep span +-- capture O(1) per node; line and column can be recovered on demand from the +-- original source. +data SrcSpan = SrcSpan + { spanStart :: !Int + , spanEnd :: !Int + } deriving (Eq, Ord, Show) + +-- | Access or replace the top-level annotation of a node. +-- +-- Unlike 'Foldable', which would collect the annotations of /every/ sub-node, +-- 'ann' returns only the annotation attached to the outermost constructor. +class Annotated f where + ann :: f a -> a + setAnn :: a -> f a -> f a + +-- | Erase all annotations, turning any annotated tree into a plain @()@ tree. +noAnn :: Functor f => f a -> f () +noAnn = void diff --git a/src/Language/SMTLIB/Syntax/Attribute.hs b/src/Language/SMTLIB/Syntax/Attribute.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Attribute.hs @@ -0,0 +1,64 @@ +-- | S-expressions and attributes, as used by @set-info@, @set-option@, the +-- @(! term ...)@ annotation form and solver responses. +module Language.SMTLIB.Syntax.Attribute + ( SExpr(..) + , AttributeValue(..) + , Attribute(..) + ) where + +import Language.SMTLIB.Syntax.Annotation (Annotated(..)) +import Language.SMTLIB.Syntax.Constant (Keyword, SpecConstant, Symbol) + +-- | An @s_expr@. +data SExpr a + = SEConstant (SpecConstant a) a + | SESymbol !Symbol a + | 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) + +-- | An @attribute_value@. +data AttributeValue a + = AVConstant (SpecConstant a) a + | AVSymbol !Symbol a + | AVSExpr [SExpr a] a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | 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) + +instance Annotated SExpr where + ann = \case + SEConstant _ a -> a + SESymbol _ a -> a + SEKeyword _ a -> a + SEReserved _ a -> a + SEList _ a -> a + setAnn a = \case + SEConstant x _ -> SEConstant x a + SESymbol x _ -> SESymbol x a + SEKeyword x _ -> SEKeyword x a + SEReserved x _ -> SEReserved x a + SEList x _ -> SEList x a + +instance Annotated AttributeValue where + ann = \case + AVConstant _ a -> a + AVSymbol _ a -> a + AVSExpr _ a -> a + setAnn a = \case + AVConstant x _ -> AVConstant x a + AVSymbol x _ -> AVSymbol x a + AVSExpr x _ -> AVSExpr x a + +instance Annotated Attribute where + ann = \case + Attribute _ a -> a + AttributeWith _ _ a -> a + setAnn a = \case + Attribute k _ -> Attribute k a + AttributeWith k v _ -> AttributeWith k v a diff --git a/src/Language/SMTLIB/Syntax/Command.hs b/src/Language/SMTLIB/Syntax/Command.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Command.hs @@ -0,0 +1,209 @@ +-- | Top-level commands of an SMT-LIB 2 script. +module Language.SMTLIB.Syntax.Command + ( Command(..) + , Option(..) + , InfoFlag(..) + , Script + ) where + +import Data.Text (Text) + +import Language.SMTLIB.Syntax.Annotation (Annotated(..)) +import Language.SMTLIB.Syntax.Attribute (Attribute) +import Language.SMTLIB.Syntax.Constant (Keyword, Symbol) +import Language.SMTLIB.Syntax.Datatype + (DatatypeDec, FunctionDec, FunctionDef, SortDec) +import Language.SMTLIB.Syntax.Identifier (Sort) +import Language.SMTLIB.Syntax.Term (Term) + +-- | An @option@ for @set-option@. +data Option a + = DiagnosticOutputChannel !Text a + | GlobalDeclarations !Bool a + | InteractiveMode !Bool a + | PrintSuccess !Bool a + | ProduceAssertions !Bool a + | ProduceAssignments !Bool a + | ProduceModels !Bool a + | ProduceProofs !Bool a + | ProduceUnsatAssumptions !Bool a + | ProduceUnsatCores !Bool a + | RandomSeed !Integer a + | RegularOutputChannel !Text a + | ReproducibleResourceLimit !Integer a + | Verbosity !Integer a + | OptionAttribute (Attribute a) a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | An @info_flag@ for @get-info@. +data InfoFlag a + = AllStatistics a + | AssertionStackLevels a + | Authors a + | ErrorBehaviorFlag a + | InfoName a + | ReasonUnknownFlag a + | InfoVersion a + | InfoFlagKeyword !Keyword a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A top-level @command@. +data Command a + = SetLogic !Symbol a + | SetOption (Option a) a + | SetInfo (Attribute a) a + | DeclareSort !Symbol !Integer a + | DeclareSortParameter !Symbol a -- ^ SMT-LIB 2.7 + | DefineSort !Symbol [Symbol] (Sort a) a + | DeclareConst !Symbol (Sort a) a + | DefineConst !Symbol (Sort a) (Term a) a -- ^ SMT-LIB 2.7 + | DeclareFun !Symbol [Sort a] (Sort a) a + | DefineFun (FunctionDef a) a + | DefineFunRec (FunctionDef a) a + | DefineFunsRec [FunctionDec a] [Term a] a + | DeclareDatatype !Symbol (DatatypeDec a) a + | DeclareDatatypes [SortDec a] [DatatypeDec a] a + | Push !Integer a + | Pop !Integer a + | Reset a + | ResetAssertions a + | Assert (Term a) a + | CheckSat a + | CheckSatAssuming [Term a] a -- ^ assumptions: arbitrary Bool terms (SMT-LIB 2.7; was @prop_literal@) + | GetAssertions a + | GetModel a + | GetProof a + | GetUnsatCore a + | GetUnsatAssumptions a + | GetValue [Term a] a + | GetAssignment a + | GetOption !Keyword a + | GetInfo (InfoFlag a) a + | Echo !Text a + | Exit a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A script is a sequence of commands. +type Script a = [Command a] + +instance Annotated Option where + ann = \case + DiagnosticOutputChannel _ a -> a + GlobalDeclarations _ a -> a + InteractiveMode _ a -> a + PrintSuccess _ a -> a + ProduceAssertions _ a -> a + ProduceAssignments _ a -> a + ProduceModels _ a -> a + ProduceProofs _ a -> a + ProduceUnsatAssumptions _ a -> a + ProduceUnsatCores _ a -> a + RandomSeed _ a -> a + RegularOutputChannel _ a -> a + ReproducibleResourceLimit _ a -> a + Verbosity _ a -> a + OptionAttribute _ a -> a + setAnn a = \case + DiagnosticOutputChannel x _ -> DiagnosticOutputChannel x a + GlobalDeclarations x _ -> GlobalDeclarations x a + InteractiveMode x _ -> InteractiveMode x a + PrintSuccess x _ -> PrintSuccess x a + ProduceAssertions x _ -> ProduceAssertions x a + ProduceAssignments x _ -> ProduceAssignments x a + ProduceModels x _ -> ProduceModels x a + ProduceProofs x _ -> ProduceProofs x a + ProduceUnsatAssumptions x _ -> ProduceUnsatAssumptions x a + ProduceUnsatCores x _ -> ProduceUnsatCores x a + RandomSeed x _ -> RandomSeed x a + RegularOutputChannel x _ -> RegularOutputChannel x a + ReproducibleResourceLimit x _ -> ReproducibleResourceLimit x a + Verbosity x _ -> Verbosity x a + OptionAttribute x _ -> OptionAttribute x a + +instance Annotated InfoFlag where + ann = \case + AllStatistics a -> a + AssertionStackLevels a -> a + Authors a -> a + ErrorBehaviorFlag a -> a + InfoName a -> a + ReasonUnknownFlag a -> a + InfoVersion a -> a + InfoFlagKeyword _ a -> a + setAnn a = \case + AllStatistics _ -> AllStatistics a + AssertionStackLevels _ -> AssertionStackLevels a + Authors _ -> Authors a + ErrorBehaviorFlag _ -> ErrorBehaviorFlag a + InfoName _ -> InfoName a + ReasonUnknownFlag _ -> ReasonUnknownFlag a + InfoVersion _ -> InfoVersion a + InfoFlagKeyword k _ -> InfoFlagKeyword k a + +instance Annotated Command where + ann = \case + SetLogic _ a -> a + SetOption _ a -> a + SetInfo _ a -> a + DeclareSort _ _ a -> a + DeclareSortParameter _ a -> a + DefineSort _ _ _ a -> a + DeclareConst _ _ a -> a + DefineConst _ _ _ a -> a + DeclareFun _ _ _ a -> a + DefineFun _ a -> a + DefineFunRec _ a -> a + DefineFunsRec _ _ a -> a + DeclareDatatype _ _ a -> a + DeclareDatatypes _ _ a -> a + Push _ a -> a + Pop _ a -> a + Reset a -> a + ResetAssertions a -> a + Assert _ a -> a + CheckSat a -> a + CheckSatAssuming _ a -> a + GetAssertions a -> a + GetModel a -> a + GetProof a -> a + GetUnsatCore a -> a + GetUnsatAssumptions a -> a + GetValue _ a -> a + GetAssignment a -> a + GetOption _ a -> a + GetInfo _ a -> a + Echo _ a -> a + Exit a -> a + setAnn a = \case + SetLogic x _ -> SetLogic x a + SetOption x _ -> SetOption x a + SetInfo x _ -> SetInfo x a + DeclareSort x y _ -> DeclareSort x y a + DeclareSortParameter x _ -> DeclareSortParameter x a + DefineSort x y z _ -> DefineSort x y z a + DeclareConst x y _ -> DeclareConst x y a + DefineConst x y z _ -> DefineConst x y z a + DeclareFun x y z _ -> DeclareFun x y z a + DefineFun x _ -> DefineFun x a + DefineFunRec x _ -> DefineFunRec x a + DefineFunsRec x y _ -> DefineFunsRec x y a + DeclareDatatype x y _ -> DeclareDatatype x y a + DeclareDatatypes x y _ -> DeclareDatatypes x y a + Push x _ -> Push x a + Pop x _ -> Pop x a + Reset _ -> Reset a + ResetAssertions _ -> ResetAssertions a + Assert x _ -> Assert x a + CheckSat _ -> CheckSat a + CheckSatAssuming x _ -> CheckSatAssuming x a + GetAssertions _ -> GetAssertions a + GetModel _ -> GetModel a + GetProof _ -> GetProof a + GetUnsatCore _ -> GetUnsatCore a + GetUnsatAssumptions _ -> GetUnsatAssumptions a + GetValue x _ -> GetValue x a + GetAssignment _ -> GetAssignment a + GetOption x _ -> GetOption x a + GetInfo x _ -> GetInfo x a + Echo x _ -> Echo x a + Exit _ -> Exit a diff --git a/src/Language/SMTLIB/Syntax/Constant.hs b/src/Language/SMTLIB/Syntax/Constant.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Constant.hs @@ -0,0 +1,81 @@ +-- | Lexical constants of the SMT-LIB 2 language: symbols, keywords, indices and +-- spec-constants, plus helpers to interpret the numeric literals. +-- +-- 'Symbol', 'Keyword' and the string payload of 'SCString' always hold the +-- /logical/ value (unquoted, unescaped). Quoting and escaping is entirely the +-- printer's responsibility. The numeric literals 'SCDecimal', 'SCHexadecimal' +-- and 'SCBinary' keep the raw lexeme 'Text' so that printing round-trips +-- byte-for-byte (leading zeros, letter case); use the interpreters below to +-- recover their values. +module Language.SMTLIB.Syntax.Constant + ( Symbol + , Keyword + , SpecConstant(..) + , Index(..) + -- * Numeric interpreters + , hexToInteger + , binToInteger + , decimalToScientific + ) where + +import Data.Char (digitToInt) +import Data.Scientific (Scientific) +import Data.Text (Text) +import qualified Data.Text as T + +import Language.SMTLIB.Syntax.Annotation (Annotated(..)) + +-- | An SMT-LIB symbol, stored as its logical (unquoted) value. +type Symbol = Text + +-- | An SMT-LIB keyword, stored /without/ its leading colon. +type Keyword = Text + +-- | A @spec_constant@. +data SpecConstant a + = SCNumeral !Integer a -- ^ @42@ + | SCDecimal !Text a -- ^ raw lexeme, e.g. @"1.500"@ + | 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) + +-- | An @index@ of an indexed identifier @(_ sym i ...)@. +data Index a + = IxNumeral !Integer a + | IxSymbol !Symbol a + deriving (Show, Eq, Functor, Foldable, Traversable) + +instance Annotated SpecConstant where + ann = \case + SCNumeral _ a -> a + SCDecimal _ a -> a + SCHexadecimal _ a -> a + SCBinary _ a -> a + SCString _ a -> a + setAnn a = \case + SCNumeral x _ -> SCNumeral x a + SCDecimal x _ -> SCDecimal x a + SCHexadecimal x _ -> SCHexadecimal x a + SCBinary x _ -> SCBinary x a + SCString x _ -> SCString x a + +instance Annotated Index where + ann = \case + IxNumeral _ a -> a + IxSymbol _ a -> a + setAnn a = \case + IxNumeral x _ -> IxNumeral x a + IxSymbol x _ -> IxSymbol x a + +-- | Interpret the digits of an 'SCHexadecimal' lexeme as an 'Integer'. +hexToInteger :: Text -> Integer +hexToInteger = T.foldl' (\acc c -> acc * 16 + toInteger (digitToInt c)) 0 + +-- | Interpret the digits of an 'SCBinary' lexeme as an 'Integer'. +binToInteger :: Text -> Integer +binToInteger = T.foldl' (\acc c -> acc * 2 + toInteger (digitToInt c)) 0 + +-- | Interpret an 'SCDecimal' lexeme as a 'Scientific' value. +decimalToScientific :: Text -> Scientific +decimalToScientific = read . T.unpack diff --git a/src/Language/SMTLIB/Syntax/Datatype.hs b/src/Language/SMTLIB/Syntax/Datatype.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Datatype.hs @@ -0,0 +1,65 @@ +-- | Declarations for sorts, datatypes and (recursive) function definitions. +module Language.SMTLIB.Syntax.Datatype + ( SortDec(..) + , SelectorDec(..) + , ConstructorDec(..) + , DatatypeDec(..) + , FunctionDec(..) + , FunctionDef(..) + ) where + +import Language.SMTLIB.Syntax.Annotation (Annotated(..)) +import Language.SMTLIB.Syntax.Constant (Symbol) +import Language.SMTLIB.Syntax.Identifier (Sort) +import Language.SMTLIB.Syntax.Term (SortedVar, Term) + +-- | A @sort_dec@ @(symbol numeral)@ heading a @declare-datatypes@. +data SortDec a = SortDec !Symbol !Integer a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @selector_dec@ @(symbol sort)@. +data SelectorDec a = SelectorDec !Symbol (Sort a) a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @constructor_dec@ @(symbol selector_dec*)@. +data ConstructorDec a = ConstructorDec !Symbol [SelectorDec a] a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | 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) + +-- | 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) + +-- | 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) + +instance Annotated SortDec where + ann (SortDec _ _ a) = a + setAnn a (SortDec s n _) = SortDec s n a + +instance Annotated SelectorDec where + ann (SelectorDec _ _ a) = a + setAnn a (SelectorDec s t _) = SelectorDec s t a + +instance Annotated ConstructorDec where + ann (ConstructorDec _ _ a) = a + setAnn a (ConstructorDec s ss _) = ConstructorDec s ss a + +instance Annotated DatatypeDec where + ann (DatatypeDec _ _ a) = a + setAnn a (DatatypeDec ps cs _) = DatatypeDec ps cs a + +instance Annotated FunctionDec where + ann (FunctionDec _ _ _ a) = a + setAnn a (FunctionDec s vs r _) = FunctionDec s vs r a + +instance Annotated FunctionDef where + ann (FunctionDef _ _ _ _ a) = a + setAnn a (FunctionDef s vs r t _) = FunctionDef s vs r t a diff --git a/src/Language/SMTLIB/Syntax/Identifier.hs b/src/Language/SMTLIB/Syntax/Identifier.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Identifier.hs @@ -0,0 +1,46 @@ +-- | Identifiers, qualified identifiers and sorts. +module Language.SMTLIB.Syntax.Identifier + ( Identifier(..) + , QualIdentifier(..) + , Sort(..) + , pattern Symbol + ) where + +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) + +-- | A simple (non-indexed) identifier. +pattern Symbol :: Symbol -> Identifier () +pattern Symbol s = Identifier s [] () + +-- | 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) + +-- | 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) + +instance Annotated Identifier where + ann (Identifier _ _ a) = a + setAnn a (Identifier s ix _) = Identifier s ix a + +instance Annotated Sort where + ann (Sort _ _ a) = a + setAnn a (Sort i ss _) = Sort i ss a + +instance Annotated QualIdentifier where + ann = \case + QIdentifier _ a -> a + QIdentifierAs _ _ a -> a + setAnn a = \case + QIdentifier i _ -> QIdentifier i a + QIdentifierAs i s _ -> QIdentifierAs i s a diff --git a/src/Language/SMTLIB/Syntax/Response.hs b/src/Language/SMTLIB/Syntax/Response.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Response.hs @@ -0,0 +1,75 @@ +-- | Solver command responses (the output side of the protocol). +module Language.SMTLIB.Syntax.Response + ( CheckSatResponse(..) + , ErrorBehavior(..) + , ReasonUnknown(..) + , InfoResponse(..) + , ValuationPair(..) + , ModelResponse(..) + , CommandResponse(..) + ) where + +import Data.Text (Text) + +import Language.SMTLIB.Syntax.Attribute (Attribute, AttributeValue, SExpr) +import Language.SMTLIB.Syntax.Constant (Symbol) +import Language.SMTLIB.Syntax.Datatype (FunctionDec, FunctionDef) +import Language.SMTLIB.Syntax.Term (Term) + +-- | The response to @check-sat@. +data CheckSatResponse = Sat | Unsat | Unknown + deriving (Show, Eq) + +-- | The @:error-behavior@ of a solver. +data ErrorBehavior = ImmediateExit | ContinuedExecution + deriving (Show, Eq) + +-- | The @:reason-unknown@ explanation. +data ReasonUnknown a + = RUMemout + | RUIncomplete + | RUOther (SExpr a) + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A single entry of a @get-info@ response. +data InfoResponse a + = IRAssertionStackLevels !Integer + | IRAuthors !Text + | IRErrorBehavior ErrorBehavior + | IRName !Text + | IRReasonUnknown (ReasonUnknown a) + | IRVersion !Text + | IRAttribute (Attribute a) + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @(term value)@ pair of a @get-value@ response. +data ValuationPair a = ValuationPair (Term a) (Term a) + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | 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) + +-- | A solver's response to a command. Which constructor a given solver emits +-- depends on the command it answers; the parsers in +-- "Language.SMTLIB.Parser.Response" therefore offer both a general parser and +-- per-command parsers. +data CommandResponse a + = RSuccess + | RUnsupported + | RError !Text + | RCheckSat CheckSatResponse + | REcho !Text + | RGetAssertions [Term a] + | RGetAssignment [(Symbol, Bool)] + | RGetInfo [InfoResponse a] + | RGetModel [ModelResponse a] + | RGetOption (AttributeValue a) + | RGetProof (SExpr a) + | RGetUnsatAssumptions [Term a] + | RGetUnsatCore [Symbol] + | RGetValue [ValuationPair a] + deriving (Show, Eq, Functor, Foldable, Traversable) diff --git a/src/Language/SMTLIB/Syntax/Term.hs b/src/Language/SMTLIB/Syntax/Term.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMTLIB/Syntax/Term.hs @@ -0,0 +1,90 @@ +-- | Terms and their binders, including the SMT-LIB 2.6 @match@ form and the +-- SMT-LIB 2.7 @lambda@ binder. +module Language.SMTLIB.Syntax.Term + ( Term(..) + , VarBinding(..) + , SortedVar(..) + , Pattern(..) + , MatchCase(..) + ) where + +import Language.SMTLIB.Syntax.Annotation (Annotated(..)) +import Language.SMTLIB.Syntax.Attribute (Attribute) +import Language.SMTLIB.Syntax.Constant (SpecConstant, Symbol) +import Language.SMTLIB.Syntax.Identifier (QualIdentifier, Sort) + +-- | A @term@. +data Term a + = TConstant (SpecConstant a) a + | TQualIdent (QualIdentifier a) a + | TApp (QualIdentifier a) [Term a] a -- ^ function application; args non-empty + | TLet [VarBinding a] (Term a) a + | TLambda [SortedVar a] (Term a) a -- ^ @(lambda ((x S) ...) t)@; SMT-LIB 2.7 + | TForall [SortedVar a] (Term a) a + | 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) + +-- | A @var_binding@ @(symbol term)@ of a @let@. +data VarBinding a = VarBinding !Symbol (Term a) a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @sorted_var@ @(symbol sort)@. +data SortedVar a = SortedVar !Symbol (Sort a) a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @pattern@ of a @match@ case: either a single variable\/nullary +-- constructor symbol, or @(constructor x1 ... xn)@. As of SMT-LIB 2.7 the +-- special symbol @_@ may also be used as a wildcard, both as a whole pattern +-- (@PVar \"_\"@) and as a bound variable inside a constructor pattern. +data Pattern a + = PVar !Symbol a + | PCtor !Symbol [Symbol] a + deriving (Show, Eq, Functor, Foldable, Traversable) + +-- | A @match_case@ @(pattern term)@. +data MatchCase a = MatchCase (Pattern a) (Term a) a + deriving (Show, Eq, Functor, Foldable, Traversable) + +instance Annotated Term where + ann = \case + TConstant _ a -> a + TQualIdent _ a -> a + TApp _ _ a -> a + TLet _ _ a -> a + TLambda _ _ a -> a + TForall _ _ a -> a + TExists _ _ a -> a + TMatch _ _ a -> a + TAnnot _ _ a -> a + setAnn a = \case + TConstant x _ -> TConstant x a + TQualIdent x _ -> TQualIdent x a + TApp f x _ -> TApp f x a + TLet b t _ -> TLet b t a + TLambda v t _ -> TLambda v t a + TForall v t _ -> TForall v t a + TExists v t _ -> TExists v t a + TMatch t c _ -> TMatch t c a + TAnnot t x _ -> TAnnot t x a + +instance Annotated VarBinding where + ann (VarBinding _ _ a) = a + setAnn a (VarBinding s t _) = VarBinding s t a + +instance Annotated SortedVar where + ann (SortedVar _ _ a) = a + setAnn a (SortedVar s t _) = SortedVar s t a + +instance Annotated Pattern where + ann = \case + PVar _ a -> a + PCtor _ _ a -> a + setAnn a = \case + PVar s _ -> PVar s a + PCtor s x _ -> PCtor s x a + +instance Annotated MatchCase where + ann (MatchCase _ _ a) = a + setAnn a (MatchCase p t _) = MatchCase p t a diff --git a/test/Arbitrary.hs b/test/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/test/Arbitrary.hs @@ -0,0 +1,256 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | Size-bounded 'Arbitrary' generators for the @()@-annotated AST, used by the +-- round-trip property tests. Symbols and string values are generated as their +-- /logical/ values (including ones that force the printer to quote\/escape), so +-- the round-trip property exercises the quoting rules. +module Arbitrary () where + +import qualified Data.Text as T +import Test.QuickCheck + +import Language.SMTLIB.Syntax + +-- Characters ----------------------------------------------------------------- + +startChars :: [Char] +startChars = ['a'..'z'] ++ ['A'..'Z'] ++ "~!@$%^&*_-+=<>.?/" + +contChars :: [Char] +contChars = startChars ++ ['0'..'9'] + +-- Includes characters that force |...| quoting (space, ':', '#', '"', digit +-- leads) but never '|' or '\\', which are not representable inside a quoted +-- symbol. +weirdChars :: [Char] +weirdChars = contChars ++ " :#\"0123456789" + +genSymbol :: Gen Symbol +genSymbol = oneof [simple, weird] + where + simple = do + h <- elements startChars + t <- resize 3 (listOf (elements contChars)) + pure (T.pack (h : t)) + weird = T.pack <$> resize 4 (listOf1 (elements weirdChars)) + +-- | A symbol usable in a @match@ pattern binding position: an ordinary symbol +-- or the @_@ wildcard (SMT-LIB 2.7). +genPatternSymbol :: Gen Symbol +genPatternSymbol = frequency [(1, pure "_"), (4, genSymbol)] + +genKeyword :: Gen Keyword +genKeyword = T.pack <$> resize 4 (listOf1 (elements contChars)) + +genStringValue :: Gen T.Text +genStringValue = T.pack <$> resize 6 (listOf (elements stringChars)) + where stringChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ " \t\"()|;" + +genDigits :: Gen T.Text +genDigits = T.pack <$> resize 4 (listOf1 (elements ['0'..'9'])) + +-- Bounded list helpers ------------------------------------------------------- + +listOf1' :: Int -> Gen a -> Gen [a] +listOf1' n g = choose (1, max 1 n) >>= \k -> vectorOf k g + +listOf' :: Int -> Gen a -> Gen [a] +listOf' n g = choose (0, n) >>= \k -> vectorOf k g + +-- Constants ------------------------------------------------------------------ + +instance Arbitrary (SpecConstant ()) where + arbitrary = oneof + [ (\n -> SCNumeral n ()) . getNonNegative <$> arbitrary + , (\i f -> SCDecimal (T.concat [i, ".", f]) ()) <$> genDigits <*> genDigits + , (\t -> SCHexadecimal t ()) . T.pack <$> resize 4 (listOf1 (elements "0123456789abcdefABCDEF")) + , (\t -> SCBinary t ()) . T.pack <$> resize 4 (listOf1 (elements "01")) + , (\s -> SCString s ()) <$> genStringValue + ] + +instance Arbitrary (Index ()) where + arbitrary = oneof + [ (\n -> IxNumeral n ()) . getNonNegative <$> arbitrary + , (\s -> IxSymbol s ()) <$> genSymbol + ] + +-- Identifiers and sorts ------------------------------------------------------ + +instance Arbitrary (Identifier ()) where + arbitrary = Identifier <$> genSymbol <*> listOf' 2 arbitrary <*> pure () + +instance Arbitrary (Sort ()) where + arbitrary = sized go + where + go n + | n <= 0 = (\i -> Sort i [] ()) <$> arbitrary + | otherwise = do + i <- arbitrary + args <- listOf' 2 (resize (n `div` 2) (sized go)) + pure (Sort i args ()) + +instance Arbitrary (QualIdentifier ()) where + arbitrary = oneof + [ (\i -> QIdentifier i ()) <$> arbitrary + , (\i s -> QIdentifierAs i s ()) <$> arbitrary <*> arbitrary + ] + +-- S-expressions and attributes ----------------------------------------------- + +instance Arbitrary (SExpr ()) where + arbitrary = sized go + where + go n + | n <= 0 = oneof + [ (\c -> SEConstant c ()) <$> arbitrary + , (\k -> SEKeyword k ()) <$> genKeyword + , (\s -> SESymbol s ()) <$> genSymbol + , (\w -> SEReserved w ()) <$> elements reservedList + ] + | otherwise = oneof + [ (\c -> SEConstant c ()) <$> arbitrary + , (\k -> SEKeyword k ()) <$> genKeyword + , (\s -> SESymbol s ()) <$> genSymbol + , (\w -> SEReserved w ()) <$> elements reservedList + , (\xs -> SEList xs ()) <$> listOf' 3 (resize (n `div` 2) (sized go)) + ] + reservedList = ["_", "as", "let", "lambda", "forall", "exists", "match", "par", "!"] + +instance Arbitrary (AttributeValue ()) where + arbitrary = oneof + [ (\c -> AVConstant c ()) <$> arbitrary + , (\s -> AVSymbol s ()) <$> genSymbol + , (\xs -> AVSExpr xs ()) <$> resize 3 (listOf' 3 arbitrary) + ] + +instance Arbitrary (Attribute ()) where + arbitrary = oneof + [ (\k -> Attribute k ()) <$> genKeyword + , (\k v -> AttributeWith k v ()) <$> genKeyword <*> arbitrary + ] + +-- Terms ---------------------------------------------------------------------- + +instance Arbitrary (VarBinding ()) where + arbitrary = VarBinding <$> genSymbol <*> resize 2 arbitrary <*> pure () + +instance Arbitrary (SortedVar ()) where + arbitrary = SortedVar <$> genSymbol <*> resize 2 arbitrary <*> pure () + +instance Arbitrary (Pattern ()) where + arbitrary = oneof + [ (\s -> PVar s ()) <$> genPatternSymbol + , (\c xs -> PCtor c xs ()) <$> genSymbol <*> listOf1' 2 genPatternSymbol + ] + +instance Arbitrary (MatchCase ()) where + arbitrary = MatchCase <$> arbitrary <*> resize 2 arbitrary <*> pure () + +instance Arbitrary (Term ()) where + arbitrary = sized go + where + leaf = oneof + [ (\c -> TConstant c ()) <$> arbitrary + , (\q -> TQualIdent q ()) <$> arbitrary + ] + go n + | n <= 0 = leaf + | otherwise = oneof + [ leaf + , (\q ts -> TApp q ts ()) <$> arbitrary <*> listOf1' 3 (sub n) + , (\bs t -> TLet bs t ()) <$> listOf1' 2 (resize (n `div` 2) arbitrary) <*> sub n + , (\vs t -> TLambda vs t ()) <$> listOf1' 2 (resize (n `div` 2) arbitrary) <*> sub n + , (\vs t -> TForall vs t ()) <$> listOf1' 2 (resize (n `div` 2) arbitrary) <*> sub n + , (\vs t -> TExists vs t ()) <$> listOf1' 2 (resize (n `div` 2) arbitrary) <*> sub n + , (\t cs -> TMatch t cs ()) <$> sub n <*> listOf1' 2 (resize (n `div` 2) arbitrary) + , (\t as -> TAnnot t as ()) <$> sub n <*> listOf1' 2 (resize (n `div` 2) arbitrary) + ] + sub n = resize (n `div` 2) (sized go) + +-- Datatype / function declarations ------------------------------------------- + +instance Arbitrary (SortDec ()) where + arbitrary = SortDec <$> genSymbol <*> (getNonNegative <$> arbitrary) <*> pure () + +instance Arbitrary (SelectorDec ()) where + arbitrary = SelectorDec <$> genSymbol <*> resize 2 arbitrary <*> pure () + +instance Arbitrary (ConstructorDec ()) where + arbitrary = ConstructorDec <$> genSymbol <*> listOf' 2 arbitrary <*> pure () + +instance Arbitrary (DatatypeDec ()) where + arbitrary = oneof + [ (\cs -> DatatypeDec [] cs ()) <$> listOf1' 2 arbitrary + , (\ps cs -> DatatypeDec ps cs ()) <$> listOf1' 2 genSymbol <*> listOf1' 2 arbitrary + ] + +instance Arbitrary (FunctionDec ()) where + arbitrary = FunctionDec <$> genSymbol <*> listOf' 2 arbitrary <*> resize 2 arbitrary <*> pure () + +instance Arbitrary (FunctionDef ()) where + arbitrary = FunctionDef <$> genSymbol <*> listOf' 2 arbitrary + <*> resize 2 arbitrary <*> resize 2 arbitrary <*> pure () + +-- Commands ------------------------------------------------------------------- + +instance Arbitrary (Option ()) where + arbitrary = oneof + [ b PrintSuccess, b GlobalDeclarations, b InteractiveMode + , b ProduceAssertions, b ProduceAssignments, b ProduceModels, b ProduceProofs + , b ProduceUnsatAssumptions, b ProduceUnsatCores + , (\s -> DiagnosticOutputChannel s ()) <$> genStringValue + , (\s -> RegularOutputChannel s ()) <$> genStringValue + , n RandomSeed, n Verbosity, n ReproducibleResourceLimit + , (\a -> OptionAttribute a ()) <$> arbitrary + ] + where + b con = (\x -> con x ()) <$> arbitrary + n con = (\x -> con x ()) . getNonNegative <$> arbitrary + +instance Arbitrary (InfoFlag ()) where + arbitrary = oneof + [ pure (AllStatistics ()), pure (AssertionStackLevels ()), pure (Authors ()) + , pure (ErrorBehaviorFlag ()), pure (InfoName ()), pure (ReasonUnknownFlag ()) + , pure (InfoVersion ()), (\k -> InfoFlagKeyword k ()) <$> genKeyword + ] + +instance Arbitrary (Command ()) where + arbitrary = oneof + [ (\s -> SetLogic s ()) <$> genSymbol + , (\o -> SetOption o ()) <$> arbitrary + , (\a -> SetInfo a ()) <$> arbitrary + , (\s k -> DeclareSort s k ()) <$> genSymbol <*> (getNonNegative <$> arbitrary) + , (\s -> DeclareSortParameter s ()) <$> genSymbol + , (\s ps r -> DefineSort s ps r ()) <$> genSymbol <*> listOf' 2 genSymbol <*> arbitrary + , (\s r -> DeclareConst s r ()) <$> genSymbol <*> arbitrary + , (\s r t -> DefineConst s r t ()) <$> genSymbol <*> arbitrary <*> resize 2 arbitrary + , (\s as r -> DeclareFun s as r ()) <$> genSymbol <*> listOf' 2 arbitrary <*> arbitrary + , (\d -> DefineFun d ()) <$> arbitrary + , (\d -> DefineFunRec d ()) <$> arbitrary + , funsRec + , (\s d -> DeclareDatatype s d ()) <$> genSymbol <*> arbitrary + , datatypes + , (\k -> Push k ()) . getNonNegative <$> arbitrary + , (\k -> Pop k ()) . getNonNegative <$> arbitrary + , pure (Reset ()), pure (ResetAssertions ()) + , (\t -> Assert t ()) <$> arbitrary + , pure (CheckSat ()) + , (\ps -> CheckSatAssuming ps ()) <$> listOf' 3 arbitrary + , pure (GetAssertions ()), pure (GetModel ()), pure (GetProof ()) + , pure (GetUnsatCore ()), pure (GetUnsatAssumptions ()) + , (\ts -> GetValue ts ()) <$> listOf1' 3 arbitrary + , pure (GetAssignment ()) + , (\k -> GetOption k ()) <$> genKeyword + , (\f -> GetInfo f ()) <$> arbitrary + , (\s -> Echo s ()) <$> genStringValue + , pure (Exit ()) + ] + where + funsRec = do + k <- choose (1, 2) + DefineFunsRec <$> vectorOf k arbitrary <*> vectorOf k arbitrary <*> pure () + datatypes = do + k <- choose (1, 2) + DeclareDatatypes <$> vectorOf k arbitrary <*> vectorOf k arbitrary <*> pure () diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,168 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Control.Monad (filterM, forM) +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 Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck +import Text.Megaparsec (eof, errorBundlePretty, 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) + +main :: IO () +main = do + sampleTests <- loadSampleTests + defaultMain $ testGroup "language-smtlib" + [ roundTripTests + , framerTests + , streamingTests + , sampleTests + ] + +-- Round-trip: parse . render == id (modulo annotations) ---------------------- + +roundTrip + :: (Eq (f ()), Show (f ()), Functor f, Pretty (f ())) + => P (f SrcSpan) -> f () -> Property +roundTrip p x = + let txt = renderText x + in case parse (sc *> p <* eof) "" txt of + Left e -> counterexample (T.unpack txt ++ "\n" ++ errorBundlePretty e) (property False) + Right y -> counterexample (T.unpack txt) (noAnn y === x) + +roundTripTests :: TestTree +roundTripTests = testGroup "round-trip (parse . render == id)" + [ testProperty "SpecConstant" (roundTrip pSpecConstant :: SpecConstant () -> Property) + , testProperty "Index" (roundTrip pIndex :: Index () -> Property) + , testProperty "Identifier" (roundTrip pIdentifier :: Identifier () -> Property) + , testProperty "Sort" (roundTrip pSort :: Sort () -> Property) + , testProperty "QualIdentifier" (roundTrip pQualIdentifier :: QualIdentifier () -> Property) + , testProperty "SExpr" (roundTrip pSExpr :: SExpr () -> Property) + , testProperty "AttributeValue" (roundTrip pAttributeValue :: AttributeValue () -> Property) + , testProperty "Attribute" (roundTrip pAttribute :: Attribute () -> Property) + , testProperty "VarBinding" (roundTrip pVarBinding :: VarBinding () -> Property) + , testProperty "SortedVar" (roundTrip pSortedVar :: SortedVar () -> Property) + , testProperty "Pattern" (roundTrip pPattern :: Pattern () -> Property) + , testProperty "MatchCase" (roundTrip pMatchCase :: MatchCase () -> Property) + , testProperty "Term" (roundTrip pTerm :: Term () -> Property) + , testProperty "SortDec" (roundTrip pSortDec :: SortDec () -> Property) + , testProperty "SelectorDec" (roundTrip pSelectorDec :: SelectorDec () -> Property) + , testProperty "ConstructorDec" (roundTrip pConstructorDec :: ConstructorDec () -> Property) + , testProperty "DatatypeDec" (roundTrip pDatatypeDec :: DatatypeDec () -> Property) + , testProperty "FunctionDec" (roundTrip pFunctionDec :: FunctionDec () -> Property) + , testProperty "FunctionDef" (roundTrip pFunctionDef :: FunctionDef () -> Property) + , testProperty "Option" (roundTrip pOption :: Option () -> Property) + , testProperty "InfoFlag" (roundTrip pInfoFlag :: InfoFlag () -> Property) + , testProperty "Command" (roundTrip pCommand :: Command () -> Property) + ] + +-- Framer --------------------------------------------------------------------- + +data Outcome = ODone Text Text | OPartial | OFailed FrameError Text + deriving (Eq, Show) + +toOutcome :: Result Text -> Outcome +toOutcome (Done a r) = ODone a r +toOutcome (Partial _) = OPartial +toOutcome (Failed e r) = OFailed e r + +-- | Feed all of @t@ then signal EOF. +runEOF :: Text -> Outcome +runEOF t = toOutcome (feed (frameSExpr t) "") + +-- | Frame @t@ without signalling EOF (REPL view). +runNoEOF :: Text -> Outcome +runNoEOF = toOutcome . frameSExpr + +-- | Feed the input one character at a time (no EOF). +feedByChar :: Text -> Outcome +feedByChar = toOutcome . T.foldl' (\r c -> feed r (T.singleton c)) (frameSExpr "") + +framerTests :: TestTree +framerTests = testGroup "S-expression framer" + [ testCase "complete list" $ runEOF "(check-sat)" @?= ODone "(check-sat)" "" + , testCase "incomplete list is Partial" $ runNoEOF "(assert (= a" @?= OPartial + , testCase "unexpected close paren" $ runNoEOF ")" @?= OFailed UnexpectedCloseParen ")" + , testCase "unterminated string" $ runEOF "\"ab" @?= OFailed UnterminatedString "" + , testCase "unterminated quoted symbol" $ runEOF "|abc" @?= OFailed UnterminatedQuotedSymbol "" + , testCase "top-level atom at EOF" $ runEOF "sat" @?= ODone "sat" "" + , testCase "top-level atom at delimiter" $ runNoEOF "sat " @?= ODone "sat" " " + , testCase "atom alone is Partial without EOF" $ runNoEOF "sat" @?= OPartial + , testCase "clean EOF on empty input" $ runEOF "" @?= OFailed EndOfInput "" + , testCase "clean EOF on whitespace" $ runEOF " \n " @?= OFailed EndOfInput "" + , testCase "minimal read keeps remainder" $ runNoEOF "(a)(b)" @?= ODone "(a)" "(b)" + , testCase "paren inside comment ignored" $ + runEOF "(a ; ) cmt\n b)" @?= ODone "(a ; ) cmt\n b)" "" + , testCase "paren inside string ignored" $ + runEOF "(echo \")\")" @?= ODone "(echo \")\")" "" + , testCase "escaped quote inside string" $ + runEOF "(echo \"a\"\"b\")" @?= ODone "(echo \"a\"\"b\")" "" + , testCase "char-by-char: Done only at boundary" $ + feedByChar "(a b)" @?= ODone "(a b)" "" + , testCase "char-by-char: Partial before boundary" $ + feedByChar "(a b" @?= OPartial + , testCase "leading comment skipped" $ + runEOF "; hello\n(exit)" @?= ODone "(exit)" "" + ] + +-- Streaming / framer-vs-parser equivalence ----------------------------------- + +streamingTests :: TestTree +streamingTests = testGroup "streaming" + [ testProperty "frameAll count matches command count" propFrameCount + , testProperty "frame-then-parse == direct parse" propFrameEqualsDirect + ] + +propFrameCount :: [Command ()] -> Property +propFrameCount cmds = + let txt = renderScript cmds + (frames, merr) = frameAll txt + in counterexample (T.unpack txt) $ + (merr === Nothing) .&&. (length frames === length cmds) + +propFrameEqualsDirect :: [Command ()] -> Property +propFrameEqualsDirect cmds = + let txt = renderScript cmds + direct = fmap (map noAnn) (parseScript "" txt) + (frames, _) = frameAll txt + perFrame = traverse (\f -> noAnn <$> parse (sc *> pCommand <* eof) "" f) frames + in counterexample (T.unpack txt) $ + (direct == Right cmds) .&&. either (const False) (== cmds) perFrame + +-- Sample files --------------------------------------------------------------- + +loadSampleTests :: IO TestTree +loadSampleTests = do + let dir = "test" "samples" "smt" + exists <- doesDirectoryExist dir + if not exists + then pure (testGroup "samples (skipped: directory not found)" []) + else do + entries <- listDirectory dir + let smt2 = [ dir e | e <- entries, takeExtension e == ".smt2" ] + files <- filterM doesFileExist smt2 + cases <- forM files $ \f -> do + src <- T.readFile f + pure (testCase f (assertParsesAndRoundTrips src)) + pure (testGroup "samples (parse + render idempotence)" cases) + +assertParsesAndRoundTrips :: Text -> Assertion +assertParsesAndRoundTrips src = + case parseScript "sample" src of + Left e -> assertFailure ("parse failed:\n" ++ errorBundlePretty e) + Right s1 -> + case parseScript "sample (rerender)" (renderScript s1) of + Left e -> assertFailure ("re-parse failed:\n" ++ errorBundlePretty e) + Right s2 -> map noAnn s1 @?= map noAnn s2 diff --git a/test/samples/smt/QF_ABV.smt2 b/test/samples/smt/QF_ABV.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_ABV.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_ABV) +(declare-fun x () (_ BitVec 32)) +(declare-fun y () (_ BitVec 16)) +(declare-fun z () (_ BitVec 20)) +(declare-fun A () (Array (_ BitVec 16) (_ BitVec 32))) +(assert + (let ((c1 (= ((_ sign_extend 12) z) (select A y))) + (A2 (store A ((_ extract 15 0) x) x))) + (let ((c2 (= A A2))) + (let ((c3 + (bvslt (concat z (_ bv5 12)) + (bvand (bvor (bvxor (bvnot x) + (select A2 ((_ zero_extend 12) #b1111))) + (concat #xAF02 y)) + (concat ((_ extract 15 0) + (bvmul x (select (store A y x) #x35FB))) + (bvashr (_ bv42 16) #x0001)))))) + (and c1 (xor c2 c3)))))) +(check-sat) +(exit) diff --git a/test/samples/smt/QF_AUFLIA.smt2 b/test/samples/smt/QF_AUFLIA.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_AUFLIA.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_AUFLIA) +(declare-fun A () (Array Int Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun P () Bool) +(declare-sort U 0) +(declare-fun f (U) (Array Int Int)) +(declare-fun c () U) +(assert + (let ((fc (f c))) + (and + (=> (= A (store fc x 5)) (> (+ (select fc y) (* 4 x)) 0)) + (= P (< (select A (+ 3 y)) (* (- 2) x)))))) +(check-sat) +(exit) diff --git a/test/samples/smt/QF_BV.smt2 b/test/samples/smt/QF_BV.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_BV.smt2 @@ -0,0 +1,18 @@ +(set-option :produce-models true) +(set-logic QF_BV) +(declare-fun x () (_ BitVec 32)) +(declare-fun y () (_ BitVec 16)) +(declare-fun z () (_ BitVec 20)) +(assert + (let ((c1 (= x ((_ sign_extend 12) z)))) + (let ((c2 (= y ((_ extract 18 3) x)))) + (let ((c3 + (bvslt (concat z (_ bv5 12)) + (bvand (bvor (bvxor (bvnot x) ((_ zero_extend 28) #b1111)) + (concat #xAF02 y)) + (concat (bvmul ((_ extract 31 16) x) y) + (bvashr (_ bv42 16) #x0001)))))) + (and c1 (xor c2 c3)))))) +(check-sat) +(get-model) +(exit) diff --git a/test/samples/smt/QF_LIA.smt2 b/test/samples/smt/QF_LIA.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_LIA.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun A () Bool) +(assert + (let ((i1 (ite A (<= (+ (* 2 x) (* (- 1) y)) (- 4)) + (= (* y 5) (- 2 x))))) + (and + i1 + (or (> x y) (= A (< (* 3 x) (+ (- 1) (* 1 (+ x y))))))))) +(check-sat) +(exit) diff --git a/test/samples/smt/QF_LRA.smt2 b/test/samples/smt/QF_LRA.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_LRA.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_LRA) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun A () Bool) +(assert + (let ((i1 (ite A (<= (+ (* 2.0 x) (* (/ 1 3) y)) (- 4)) + (= (* y 1.5) (- 2 x))))) + (and + i1 + (or (> x y) (= A (< (* 3 x) (+ (- 1) (* (/ 1 5) (+ x y))))))))) +(check-sat) +(exit) diff --git a/test/samples/smt/QF_LRA_2.smt2 b/test/samples/smt/QF_LRA_2.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_LRA_2.smt2 @@ -0,0 +1,39 @@ +(set-option :print-success true) +(set-logic QF_LRA) +(declare-fun c0 () Bool) +(declare-fun E0 () Bool) +(declare-fun f0 () Bool) +(declare-fun f1 () Bool) +(push 1) +(assert + (let ((.def_10 (not f0))) + (let ((.def_9 (not c0))) + (let ((.def_11 (or .def_9 .def_10))) + (let ((.def_7 (not f1))) + (let ((.def_8 (or c0 .def_7))) + (let ((.def_12 (and .def_8 .def_11))) + .def_12 +))))))) +(check-sat) +(pop 1) +(declare-fun f2 () Bool) +(declare-fun f3 () Bool) +(declare-fun f4 () Bool) +(declare-fun c1 () Bool) +(declare-fun E1 () Bool) +(assert + (let ((.def_23 (not f2))) + (let ((.def_20 (= c0 c1))) + (let ((.def_22 (or E0 .def_20))) + (let ((.def_24 (or .def_22 .def_23))) + (let ((.def_18 (not f4))) + (let ((.def_19 (or c1 .def_18))) + (let ((.def_25 (and .def_19 .def_24))) + .def_25 +)))))))) +(push 1) +(check-sat) +(assert (and f1 (not f1))) +(check-sat) +(pop 1) +(exit) diff --git a/test/samples/smt/QF_UF.smt2 b/test/samples/smt/QF_UF.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_UF.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_UF) +(set-info :status sat) +(declare-sort U 0) +(declare-fun f (U) U) +(declare-fun g (U) U) +(declare-fun A () Bool) +(declare-fun x () U) +(declare-fun y () U) +(assert +(let ((fx (f x)) + (cls1 (or A (= x y)))) + (and cls1 (distinct fx (g y))))) +(check-sat) +(exit) diff --git a/test/samples/smt/QF_UFLRA.smt2 b/test/samples/smt/QF_UFLRA.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/QF_UFLRA.smt2 @@ -0,0 +1,14 @@ +(set-option :produce-models true) +(set-logic QF_UFLRA) +(declare-sort U 0) +(declare-fun x () Real) +(declare-fun f (U) Real) +(declare-fun P (U) Bool) +(declare-fun g (U) U) +(declare-fun c () U) +(declare-fun d () U) +(assert (= (P c) (= (g c) c))) +(assert (ite (P c) (> x (f d)) (< x (f d)))) +(check-sat) +(get-model) +(exit) diff --git a/test/samples/smt/assertion-stack-levels-2.smt2 b/test/samples/smt/assertion-stack-levels-2.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/assertion-stack-levels-2.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or a b)) + +(get-info :assertion-stack-levels) + +; NOTE: omitting arguments of push/pop is not allowed in SMT-LIB2 +; but many solver implement the omission. +(push) +(get-info :assertion-stack-levels) +(pop) + +(get-info :assertion-stack-levels) diff --git a/test/samples/smt/assertion-stack-levels.smt2 b/test/samples/smt/assertion-stack-levels.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/assertion-stack-levels.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or a b)) + +(get-info :assertion-stack-levels) + +(push 1) +(get-info :assertion-stack-levels) +(pop 1) + +(get-info :assertion-stack-levels) diff --git a/test/samples/smt/assumptions.smt2 b/test/samples/smt/assumptions.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/assumptions.smt2 @@ -0,0 +1,8 @@ +(set-option :produce-unsat-assumptions true) +(get-option :produce-unsat-assumptions) +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or a b)) +(check-sat-assuming ((not a) (not b))) +(get-unsat-assumptions) diff --git a/test/samples/smt/chain.smt2 b/test/samples/smt/chain.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/chain.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (< 0 x y 2)) +;(assert (and (< 0 x) (< x y) (< y 2))) +(check-sat) diff --git a/test/samples/smt/declare-const.smt2 b/test/samples/smt/declare-const.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/declare-const.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LRA) +(declare-const b Bool) +(declare-const x Real) +(declare-const y Real) +(check-sat) diff --git a/test/samples/smt/define-fun-rec.smt2 b/test/samples/smt/define-fun-rec.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/define-fun-rec.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_UFLIA) +(define-fun-rec fact ((n Int)) Int + (ite (<= n 0) + 1 + (* n (fact (- n 1))))) +(check-sat) diff --git a/test/samples/smt/define-funs-rec.smt2 b/test/samples/smt/define-funs-rec.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/define-funs-rec.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_UFLIA) +(define-funs-rec + ((even ((x Int)) Bool) + (odd ((x Int)) Bool)) + ((ite (= x 0) true (odd (- x 1))) + (ite (= x 0) true (odd (- x 1))))) +(check-sat) diff --git a/test/samples/smt/division-by-zero.smt2 b/test/samples/smt/division-by-zero.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/division-by-zero.smt2 @@ -0,0 +1,18 @@ +(set-option :produce-models true) +(set-logic QF_LRA) +(declare-const x1 Real) +(declare-const x2 Real) + +(define-fun y1 () Real (/ x1 0)) +(define-fun y2 () Real (/ x2 0)) +(check-sat) ; sat +(get-value (x1 x2 y1 y2)) +(get-model) + +(assert (not (= y1 y2))) +(check-sat) ; sat +(get-value (x1 x2 y1 y2)) +(get-model) + +(assert (= x1 x2)) +(check-sat) ; unsat diff --git a/test/samples/smt/echo.smt2 b/test/samples/smt/echo.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/echo.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LRA) +(declare-const b Bool) +(echo "foo") +(declare-const x Real) +(echo "bar") +(declare-const y Real) +(echo "baz") +(check-sat) diff --git a/test/samples/smt/figure-3.11-example-script.smt2 b/test/samples/smt/figure-3.11-example-script.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/figure-3.11-example-script.smt2 @@ -0,0 +1,34 @@ +; Example script from the SMT-LIB 2.7 Reference, Figure 3.11 +; ("Example script (over two columns), with expected solver responses in +; comments"). The two columns are linearised here in reading order; the +; ';'-prefixed lines are the expected solver responses, kept as comments. + +(set-option :print-success true) +; success +(set-info :smt-lib-version 2.7) +; success +(set-logic QF_LIA) +; success +(declare-const w Int) +; success +(declare-const x Int) +; success +(declare-const y Int) +; success +(declare-const z Int) +; success +(assert (> x y)) +; success +(assert (> y z)) +; success +(push 1) +(assert (> z x)) +(check-sat) +; unsat +(get-info :all-statistics) +; (:time 0.01 :memory 0.2) +(pop 1) +(push 1) +(check-sat) +; sat +(exit) diff --git a/test/samples/smt/figure-3.12-example-script.smt2 b/test/samples/smt/figure-3.12-example-script.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/figure-3.12-example-script.smt2 @@ -0,0 +1,34 @@ +; Example script from the SMT-LIB 2.7 Reference, Figure 3.12 +; ("Another example script (excerpt), with expected solver responses in +; comments"). The two columns are linearised in reading order and the figure's +; "..." placeholders are dropped so the script is syntactically complete. +; The '@'-prefixed symbols are solver-generated abstract values, as in the PDF. + +(set-info :smt-lib-version 2.7) +(set-option :produce-models true) +(declare-const x Int) +(declare-const y Int) +(declare-fun f (Int) Int) +(assert (= (f x) (f y))) +(assert (not (= x y))) +(check-sat) +; sat +(get-value (x y)) +; ((x 0) +; (y 1) +; ) +(declare-const a (Array Int (List Int))) +(check-sat) +; sat +(get-value (a)) +; ( (a (as @array1 (Array Int (List Int)))) +; ) +(get-value ((select @array1 2))) +; (((select (as @array1 (Array Int (List Int))) 2) +; (as @list0 (List Int)) +; ) +; ) +(get-value ((first @list0) (rest @list0))) +; (((first (as @list0 (List Int))) 1) +; ((rest (as @list0 (List Int))) (as nil (List Int))) +; ) diff --git a/test/samples/smt/get-assertions.smt2 b/test/samples/smt/get-assertions.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/get-assertions.smt2 @@ -0,0 +1,13 @@ +(set-option :produce-assertions true) +; (set-option :interactive-mode true) +(get-option :produce-assertions) +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or (! a :named aa) (! b :named bb))) +(get-assertions) +(push) + (assert (not (and a bb))) + (get-assertions) +(pop) +(get-assertions) diff --git a/test/samples/smt/get-assignment.smt2 b/test/samples/smt/get-assignment.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/get-assignment.smt2 @@ -0,0 +1,9 @@ +(set-option :produce-assignments true) +(get-option :produce-assignments) +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or (! a :named aa) (! b :named bb))) +(assert (not (and a bb))) +(check-sat) +(get-assignment) diff --git a/test/samples/smt/get-model.smt2 b/test/samples/smt/get-model.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/get-model.smt2 @@ -0,0 +1,9 @@ +(set-option :produce-models true) +(get-option :produce-models) +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(assert (or a b)) +(assert (not (and a b))) +(check-sat) +(get-model) diff --git a/test/samples/smt/get-value.smt2 b/test/samples/smt/get-value.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/get-value.smt2 @@ -0,0 +1,12 @@ +(set-option :produce-models true) +(get-option :produce-models) +(set-logic QF_UF) +(set-info :status sat) +(declare-sort U 0) +(declare-fun f (U) U) +(declare-fun g (U) U) +(declare-fun A () Bool) +(declare-fun x () U) +(declare-fun y () U) +(check-sat) +(get-value (x A (f x) (g y))) diff --git a/test/samples/smt/global-declarations.smt2 b/test/samples/smt/global-declarations.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/global-declarations.smt2 @@ -0,0 +1,22 @@ +(get-option :global-declarations) + +(set-option :global-declarations false) +(get-option :global-declarations) +(set-logic QF_UFLRA) + +(push) +(declare-const x1 Bool) +(pop) +(declare-const x1 Real) + +(reset) + +(set-option :global-declarations true) +(get-option :global-declarations) +(set-logic QF_UFLRA) + +(push) +(define-fun x2 () Real 1.0) +(pop) +(assert (= x2 1.0)) +(check-sat) diff --git a/test/samples/smt/list-append-match.smt2 b/test/samples/smt/list-append-match.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/list-append-match.smt2 @@ -0,0 +1,40 @@ +; List append / length axioms from the SMT-LIB 2.7 Reference (the match section), +; demonstrating a polymorphic (par) datatype, the match binder, and the _ +; wildcard pattern (new in 2.7). Wrapped in a self-contained script: the List +; datatype and the append/length symbols are declared so the asserts parse. + +(set-info :smt-lib-version 2.7) + +; List is a polymorphic datatype with constructors "nil" and "cons". +(declare-datatype List + (par (T) ((nil) (cons (head T) (tail (List T)))))) + +(declare-fun append ((List Int) (List Int)) (List Int)) +(declare-fun length ((List Int)) Int) + +; Axiom for list append : version 1 +(assert + (forall ((l1 (List Int)) (l2 (List Int))) + (= (append l1 l2) + (match l1 ( + (nil l2) + ((cons h t) (cons h (append t l2)))))))) + +; Axiom for list append : version 2 (uses the _ wildcard pattern) +(assert + (forall ((l1 (List Int)) (l2 (List Int))) + (= (append l1 l2) + (match l1 ( + ((cons h t) (cons h (append t l2))) + (_ l2)))))) + +; Axiom for list length (uses _ as a bound variable inside a constructor pattern) +(assert + (forall ((l (List Int))) + (= (length l) + (match l ( + (nil 0) + ((cons _ t) (length t))))))) + +(check-sat) +(exit) diff --git a/test/samples/smt/print-success.smt2 b/test/samples/smt/print-success.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/print-success.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_UF) +(get-option :print-success) +(declare-fun a () Bool) +(set-option :print-success false) +(get-option :print-success) +(declare-fun b () Bool) +(assert (or a b)) +(check-sat) diff --git a/test/samples/smt/quoted-symbol.smt2 b/test/samples/smt/quoted-symbol.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/quoted-symbol.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LRA) +(set-info :status unsat) +(declare-fun abc () Real) +(assert (= abc 0)) +(assert (= |abc| 1)) +(check-sat) diff --git a/test/samples/smt/reset-assertions.smt2 b/test/samples/smt/reset-assertions.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/reset-assertions.smt2 @@ -0,0 +1,14 @@ +(set-option :produce-unsat-assumptions true) +(set-logic QF_UF) +(declare-fun x1 () Bool) +(declare-fun x2 () Bool) +(declare-fun x3 () Bool) +(assert (! x1 :named C1)) +(assert (! (not x1) :named C2)) +(assert (! (or (not x1) x2) :named C3)) +(assert (! (not x2) :named C4)) +(assert (! (or (not x1) x3) :named C5)) +(assert (! (not x3) :named C6)) +(check-sat) +(reset-assertions) +(check-sat) diff --git a/test/samples/smt/reset.smt2 b/test/samples/smt/reset.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/reset.smt2 @@ -0,0 +1,14 @@ +(set-option :produce-unsat-assumptions true) +(set-logic QF_UF) +(declare-fun x1 () Bool) +(declare-fun x2 () Bool) +(declare-fun x3 () Bool) +(assert (! x1 :named C1)) +(assert (! (not x1) :named C2)) +(assert (! (or (not x1) x2) :named C3)) +(assert (! (not x2) :named C4)) +(assert (! (or (not x1) x3) :named C5)) +(assert (! (not x3) :named C6)) +(check-sat) +(reset) +(check-sat) diff --git a/test/samples/smt/set-info-status.smt2 b/test/samples/smt/set-info-status.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/set-info-status.smt2 @@ -0,0 +1,15 @@ +(set-option :produce-models true) +(set-logic QF_UFLRA) +(declare-sort U 0) +(declare-fun x () Real) +(declare-fun f (U) Real) +(declare-fun P (U) Bool) +(declare-fun g (U) U) +(declare-fun c () U) +(declare-fun d () U) +(assert (= (P c) (= (g c) c))) +(assert (ite (P c) (> x (f d)) (< x (f d)))) +(set-info :status sat) +(check-sat) +(get-model) +(exit) diff --git a/test/samples/smt/smtlib-2.7-check-sat-assuming-terms.smt2 b/test/samples/smt/smtlib-2.7-check-sat-assuming-terms.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/smtlib-2.7-check-sat-assuming-terms.smt2 @@ -0,0 +1,11 @@ +; SMT-LIB 2.7 generalised check-sat-assuming: assumptions may be arbitrary +; Bool terms, not only prop_literals (a symbol or (not symbol)). +(set-logic QF_UF) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (or a b c)) +; arbitrary Bool terms as assumptions, plus an empty assumption list +(check-sat-assuming ((= a b) (not (and b c)) (or a (not c)))) +(check-sat-assuming ()) +(get-unsat-assumptions) diff --git a/test/samples/smt/smtlib-2.7-declare-sort-parameter.smt2 b/test/samples/smt/smtlib-2.7-declare-sort-parameter.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/smtlib-2.7-declare-sort-parameter.smt2 @@ -0,0 +1,18 @@ +; SMT-LIB 2.7 Reference, Section 4.2.3: the declare-sort-parameter command. +; +; "(declare-sort-parameter s) adds global sort parameter s to the current +; signature." Sort parameters are treated as implicitly universally quantified +; sort variables in each asserted formula (prenex / rank-1 polymorphism). + +(set-info :smt-lib-version 2.7) + +; Declare a global sort parameter X, then a polymorphic function over it. +(declare-sort-parameter X) +(declare-fun f (X) X) +(declare-const a X) + +; X behaves as an implicitly universally quantified sort variable here. +(assert (= (f a) a)) + +(check-sat) +(exit) diff --git a/test/samples/smt/smtlib-2.7-lambda-define-const.smt2 b/test/samples/smt/smtlib-2.7-lambda-define-const.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/smtlib-2.7-lambda-define-const.smt2 @@ -0,0 +1,28 @@ +; Examples from the SMT-LIB 2.7 Reference, Section 3.10 (Logic Declarations), +; illustrating the new 2.7 syntax: the -> map sort, the lambda binder, the +; define-const command, and the apply operator _. +; +; The PDF writes the conversions between a function symbol f of rank t1 t2 and a +; map of sort (-> t1 t2) as: +; (define-const c_f (lambda ((x t1)) (f x))) +; (define-fun f_c ((x t1)) t2 (_ e x)) +; Here t1 = t2 = Int. (define-const takes , so the map +; sort is given explicitly.) + +(set-info :smt-lib-version 2.7) + +; A function symbol of rank Int Int. +(declare-fun f (Int) Int) + +; The corresponding map, of sort (-> Int Int), built with lambda and named with +; define-const. +(define-const c_f (-> Int Int) (lambda ((x Int)) (f x))) + +; A map e, and the function obtained from it via the apply operator _. +(declare-const e (-> Int Int)) +(define-fun f_c ((x Int)) Int (_ e x)) + +; -> is right-associative: (-> Int Int Int) abbreviates (-> Int (-> Int Int)). +(declare-const g (-> Int Int Int)) + +(exit) diff --git a/test/samples/smt/swap.smt2 b/test/samples/smt/swap.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/swap.smt2 @@ -0,0 +1,28 @@ +; Modeling sequential code with bitvectors +;; Correct swap with no temp var +; int x, y; +; x = x + y; +; y = x - y; +; x = x - y; + +(set-option :produce-models true) +(set-logic QF_BV) + +(declare-const x_0 (_ BitVec 32)) +(declare-const x_1 (_ BitVec 32)) +(declare-const x_2 (_ BitVec 32)) +(declare-const y_0 (_ BitVec 32)) +(declare-const y_1 (_ BitVec 32)) +(assert (= x_1 (bvadd x_0 y_0))) +(assert (= y_1 (bvsub x_1 y_0))) +(assert (= x_2 (bvsub x_1 y_1))) +(assert (= x_1 (bvadd x_0 y_0))) +(assert (= y_1 (bvadd x_1 (bvneg y_0)))) +(assert (= x_2 (bvadd x_1 (bvneg y_1)))) + +(assert (not + (and (= x_2 y_0) + (= y_1 x_0)))) +(check-sat) +; unsat +(exit) diff --git a/test/samples/smt/unicode-symbol.smt2 b/test/samples/smt/unicode-symbol.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/unicode-symbol.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_LRA) +(declare-fun あいうえお () Real) +(declare-fun café () Real) +(check-sat) diff --git a/test/samples/smt/unsat-core.smt2 b/test/samples/smt/unsat-core.smt2 new file mode 100644 --- /dev/null +++ b/test/samples/smt/unsat-core.smt2 @@ -0,0 +1,18 @@ +; http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf +; φ= (x1) ∧ (¬x1) ∧ (¬x1∨x2) ∧ (¬x2) ∧ (¬x1∨x3) ∧ (¬x3) +; MUSes(φ) = {{C1, C2}, {C1, C3, C4}, {C1, C5, C6}} +; MCSes(φ) = {{C1}, {C2, C3, C5}, {C2, C3, C6}, {C2, C4, C5}, {C2, C4, C6}} +(set-option :produce-unsat-cores true) +(get-option :produce-unsat-cores) +(set-logic QF_UF) +(declare-fun x1 () Bool) +(declare-fun x2 () Bool) +(declare-fun x3 () Bool) +(assert (! x1 :named C1)) +(assert (! (not x1) :named C2)) +(assert (! (or (not x1) x2) :named C3)) +(assert (! (not x2) :named C4)) +(assert (! (or (not x1) x3) :named C5)) +(assert (! (not x3) :named C6)) +(check-sat) +(get-unsat-core)