language-smtlib-0.2.0.0: language-smtlib.cabal

cabal-version: 2.2

-- This file has been generated from package.yaml by hpack version 0.39.6.
--
-- see: https://github.com/sol/hpack

name:           language-smtlib
version:        0.2.0.0
synopsis:       Parsing, printing and incremental I/O for the SMT-LIB 2 format
description:    A @Text@-based library for parsing, printing, and incrementally streaming the SMT-LIB 2.7 format.
                .
                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
    docs/conformance.md

source-repository head
  type: git
  location: https://github.com/msakai/language-smtlib

flag profiling
  description: Add -fprof-auto (automatic cost centres) to this package's own components when building with profiling.  Off by default so that downstream packages profiling their own code are not cluttered with cost centres from language-smtlib.
  manual: True
  default: False

flag tools
  description: Build the developer-facing command-line tools shipped with this package: language-smtlib-fmt, a round-trip front end that parses an SMT-LIB script and re-emits it in canonical form; and language-smtlib-conformance, a driver that round-trips large external SMT-LIB benchmark suites (e.g. the SMT-LIB / SMT-COMP collections on Zenodo).  Off by default: these are development utilities, not needed by downstream packages that only depend on the library.
  manual: True
  default: False

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
      DeriveGeneric
      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
    , hashable >=1.3 && <1.6
    , 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
      DeriveGeneric
      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(tools)
    buildable: False
  if flag(profiling)
    ghc-prof-options: -fprof-auto

executable language-smtlib-fmt
  main-is: Main.hs
  other-modules:
      Paths_language_smtlib
  autogen-modules:
      Paths_language_smtlib
  hs-source-dirs:
      app
  default-extensions:
      DeriveFoldable
      DeriveFunctor
      DeriveGeneric
      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(tools)
    buildable: False
  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
      DeriveGeneric
      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
    , containers
    , directory
    , filepath
    , hashable
    , language-smtlib
    , megaparsec
    , quickcheck-instances
    , tasty
    , tasty-hunit
    , tasty-quickcheck
    , text
    , unordered-containers
  default-language: Haskell2010