language-smtlib-0.1.0.0: language-smtlib.cabal
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 <https://github.com/msakai/language-smtlib#readme> 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