Cabal-version: 2.4
Name:          what4
Version:       1.5.1
Author:        Galois Inc.
Maintainer:    rscott@galois.com, kquick@galois.com
Copyright:     (c) Galois, Inc 2014-2023
License:       BSD-3-Clause
License-file:  LICENSE
Build-type:    Simple
Homepage:      https://github.com/GaloisInc/what4
Bug-reports:   https://github.com/GaloisInc/what4/issues
Tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2
Category:      Formal Methods, Theorem Provers, Symbolic Computation, SMT
Synopsis:      Solver-agnostic symbolic values support for issuing queries
Description:
  What4 is a generic library for representing values as symbolic formulae which may
  contain references to symbolic values, representing unknown variables.
  It provides support for communicating with a variety of SAT and SMT solvers,
  including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.

  The data representation types make heavy use of GADT-style type indices
  to ensure type-correct manipulation of symbolic values.

data-files: solverBounds.config

Extra-source-files:
  test/responses/*.exp
  test/responses/*.rsp

Extra-doc-files:
  README.md
  CHANGES.md
  doc/README.md
  doc/implementation.md
  doc/bvdomain.cry
  doc/arithdomain.cry
  doc/bitsdomain.cry
  doc/xordomain.cry

source-repository head
  type: git
  location: https://github.com/GaloisInc/what4

flag solverTests
  description: extra tests that require all the solvers to be installed
  manual: True
  default: False

flag dRealTestDisable
  description: when running solver tests, disable testing using dReal (ignored unless -fsolverTests)
  manual: True
  default: False

flag STPTestDisable
  description: when running solver tests, disable testing using STP (ignored unless -fsolverTests)
  manual: True
  default: False

common bldflags
  default-language: Haskell2010
  ghc-options: -Wall
               -Werror=incomplete-patterns
               -Werror=missing-methods
               -Werror=overlapping-patterns
               -Wcompat
               -Wpartial-fields

common testdefs
  hs-source-dirs: test
  build-depends: base
               , parameterized-utils
               , tasty >= 0.10
               , what4

common testdefs-quickcheck
  import: testdefs
  build-depends: tasty-quickcheck >= 0.10
               , QuickCheck >= 2.12

common testdefs-hedgehog
  import: testdefs
  hs-source-dirs: test/hedgehog
  build-depends: hedgehog >= 1.0.2
               , tasty-hedgehog >= 1.2
  other-modules: Test.Tasty.Hedgehog.Alt

common testdefs-hunit
  import: testdefs
  build-depends: tasty-hunit >= 0.9

library
  import: bldflags
  build-depends:
    base >= 4.10 && < 5,
    async,
    attoparsec >= 0.13,
    bimap >= 0.2,
    bifunctors >= 5,
    BoundedChan >= 1 && < 2,
    bv-sized >= 1.0.0,
    bytestring >= 0.10,
    deriving-compat >= 0.5,
    concurrent-extra >= 0.7 && < 0.8,
    config-value >= 0.8 && < 0.9,
    containers >= 0.5.0.0,
    deepseq >= 1.3,
    directory >= 1.2.2,
    exceptions >= 0.10,
    filepath >= 1.3,
    fingertree >= 0.1.4,
    hashable >= 1.3,
    hashtables >= 1.2.3,
    io-streams >= 1.5,
    lens >= 4.18,
    libBF >= 0.6 && < 0.7,
    megaparsec >= 8 && < 10,
    mtl >= 2.2.1,
    ordered-containers >= 0.2 && < 0.3,
    panic >= 0.3,
    parameterized-utils >= 2.1 && < 2.2,
    parsec >= 3 && < 4,
    prettyprinter >= 1.7.0,
    process >= 1.2,
    s-cargot >= 0.1 && < 0.2,
    scientific >= 0.3.6,
    stm,
    temporary >= 1.2,
    template-haskell,
    text >= 1.2.4.0 && < 2.1,
    th-lift >= 0.8.2 && < 0.9,
    th-lift-instances >= 0.1 && < 0.2,
    time >= 1.8 && < 1.13,
    transformers >= 0.4,
    unliftio >= 0.2 && < 0.3,
    unordered-containers >= 0.2.10,
    utf8-string >= 1.0.1,
    vector >= 0.12.1,
    versions >= 6.0.2 && < 6.1,
    zenc >= 0.1.0 && < 0.2.0,
    ghc-prim >= 0.5.2

  default-extensions:
     NondecreasingIndentation

  hs-source-dirs: src

  exposed-modules:
    What4.BaseTypes
    What4.Concrete
    What4.Config
    What4.FunctionName
    What4.IndexLit
    What4.Interface
    What4.InterpretedFloatingPoint
    What4.FloatMode
    What4.LabeledPred
    What4.Panic
    What4.Partial
    What4.ProblemFeatures
    What4.ProgramLoc
    What4.SatResult
    What4.SemiRing
    What4.SpecialFunctions
    What4.Symbol
    What4.SFloat
    What4.SWord
    What4.WordMap

    What4.Expr
    What4.Expr.Allocator
    What4.Expr.App
    What4.Expr.ArrayUpdateMap
    What4.Expr.AppTheory
    What4.Expr.BoolMap
    What4.Expr.Builder
    What4.Expr.GroundEval
    What4.Expr.MATLAB
    What4.Expr.Simplify
    What4.Expr.StringSeq
    What4.Expr.VarIdentification
    What4.Expr.WeightedSum
    What4.Expr.UnaryBV

    What4.Serialize.FastSExpr
    What4.Serialize.Log
    What4.Serialize.Normalize
    What4.Serialize.Parser
    What4.Serialize.Printer
    What4.Serialize.SETokens

    What4.Solver
    What4.Solver.Adapter
    What4.Solver.Boolector
    What4.Solver.CVC4
    What4.Solver.CVC5
    What4.Solver.DReal
    What4.Solver.ExternalABC
    What4.Solver.STP
    What4.Solver.Yices
    What4.Solver.Z3

    What4.Protocol.Online
    What4.Protocol.SMTLib2
    What4.Protocol.SMTLib2.Parse
    What4.Protocol.SMTLib2.Response
    What4.Protocol.SMTLib2.Syntax
    What4.Protocol.SMTWriter
    What4.Protocol.ReadDecimal
    What4.Protocol.SExp
    What4.Protocol.PolyRoot
    What4.Protocol.VerilogWriter
    What4.Protocol.VerilogWriter.AST
    What4.Protocol.VerilogWriter.ABCVerilog
    What4.Protocol.VerilogWriter.Backend

    What4.Utils.AbstractDomains
    What4.Utils.AnnotatedMap
    What4.Utils.Arithmetic
    What4.Utils.BVDomain
    What4.Utils.BVDomain.Arith
    What4.Utils.BVDomain.Bitwise
    What4.Utils.BVDomain.XOR
    What4.Utils.Complex
    What4.Utils.Endian
    What4.Utils.Environment
    What4.Utils.HandleReader
    What4.Utils.IncrHash
    What4.Utils.FloatHelpers
    What4.Utils.LeqMap
    What4.Utils.MonadST
    What4.Utils.OnlyIntRepr
    What4.Utils.Process
    What4.Utils.ResolveBounds.BV
    What4.Utils.Serialize
    What4.Utils.Streams
    What4.Utils.StringLiteral
    What4.Utils.Word16String
    What4.Utils.Versions

    Test.Verification

  if impl(ghc >= 8.6)
    default-extensions: NoStarIsType

executable quickstart
  main-is: doc/QuickStart.hs
  default-language: Haskell2010

  build-depends:
    base,
    parameterized-utils,
    what4

test-suite abduct
  import: testdefs-hunit
  type: exitcode-stdio-1.0
  main-is: Abduct.hs
  default-language: Haskell2010

  build-depends:
    base,
    parameterized-utils,
    what4,
    text,
    temporary

test-suite adapter-test
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: AdapterTest.hs

  other-modules: ProbeSolvers

  if flag(solverTests)
    buildable: True
    if ! flag(dRealTestDisable)
      cpp-options: -DTEST_DREAL
    if ! flag(STPTestDisable)
      cpp-options: -DTEST_STP
  else
    buildable: False

  build-depends:
    bv-sized,
    bytestring,
    containers,
    lens,
    mtl >= 2.2.1,
    process,
    tasty-expected-failure >= 0.12 && < 0.13,
    text,
    versions

test-suite config-test
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0
  main-is: ConfigTest.hs
  build-depends: containers
               , parameterized-utils
               , prettyprinter
               , tasty-checklist >= 1.0 && < 1.1
               , text

test-suite online-solver-test
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: OnlineSolverTest.hs

  other-modules: ProbeSolvers

  if flag(solverTests)
    buildable: True
    if ! flag(STPTestDisable)
      cpp-options: -DTEST_STP
  else
    buildable: False

  build-depends:
    async,
    bv-sized,
    bytestring,
    clock,
    containers,
    exceptions,
    lens,
    prettyprinter,
    process,
    tasty-expected-failure >= 0.12 && < 0.13,
    tasty-checklist >= 1.0 && < 1.1,
    text,
    units,
    units-defs,
    versions

test-suite expr-builder-smtlib2
  import: bldflags, testdefs-hedgehog, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: ExprBuilderSMTLib2.hs

  other-modules: ProbeSolvers

  build-depends:
    bv-sized,
    bytestring,
    containers,
    libBF,
    prettyprinter,
    process,
    tasty-expected-failure >= 0.12 && < 0.13,
    tasty-checklist >= 1.0.3 && < 1.1,
    text,
    versions


test-suite exprs_tests
  import: bldflags, testdefs-hedgehog, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: ExprsTest.hs

  other-modules:
    GenWhat4Expr

  build-depends: bv-sized


test-suite iteexprs_tests
  import: bldflags, testdefs-hedgehog, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: IteExprs.hs

  other-modules:
    GenWhat4Expr

  build-depends: bv-sized
               , containers >= 0.5.0.0


test-suite bvdomain_tests
  import: bldflags, testdefs-quickcheck
  type: exitcode-stdio-1.0

  hs-source-dirs: test/QC
  main-is: BVDomTests.hs

  other-modules:  VerifyBindings

  build-depends: transformers


test-suite bvdomain_tests_hh
  import: bldflags, testdefs-hedgehog
  type: exitcode-stdio-1.0

  hs-source-dirs: test/HH
  main-is: BVDomTests.hs

  other-modules:  VerifyBindings

  build-depends: transformers


test-suite template_tests
  import: bldflags, testdefs-hedgehog
  type: exitcode-stdio-1.0
  main-is : TestTemplate.hs
  build-depends: bv-sized
               , libBF
               , transformers


test-suite solver_parsing_tests
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0
  main-is : SolverParserTest.hs
  build-depends: contravariant
               , exceptions
               , io-streams
               , lumberjack
               , tasty-sugar >= 2.0 && < 2.3
               , text

test-suite what4-serialize-tests
  default-language: Haskell2010
  type: exitcode-stdio-1.0
  ghc-options: -Wall -Wcompat -rtsopts -threaded
  hs-source-dirs: test
  main-is: SerializeTests.hs
  other-modules: SymFnTests, SerializeTestUtils
  build-depends:   what4
                 , base
                 , containers
                 , directory
                 , exceptions
                 , hedgehog
                 , libBF
                 , tasty
                 , tasty-hunit
                 , tasty-hedgehog
                 , text
                 , parameterized-utils
                 , async
                 , directory
                 , ordered-containers

test-suite invariant-synthesis
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0

  main-is: InvariantSynthesis.hs

  other-modules: ProbeSolvers

  build-depends:
    bv-sized,
    process,
    tasty-expected-failure >= 0.12 && < 0.13