what4-1.1: what4.cabal
Name: what4
Version: 1.1
Author: Galois Inc.
Maintainer: jhendrix@galois.com, rdockins@galois.com
Copyright: (c) Galois, Inc 2014-2021
License: BSD3
License-file: LICENSE
Build-type: Simple
Cabal-version: 1.18
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.3
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, 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-doc-files:
README.md
CHANGES.md
doc/README.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
library
build-depends:
base >= 4.8 && < 5,
attoparsec >= 0.13,
bimap >= 0.2,
bifunctors >= 5,
bv-sized >= 1.0.0,
bytestring >= 0.10,
deriving-compat >= 0.5,
config-value >= 0.8 && < 0.9,
containers >= 0.5.0.0,
data-binary-ieee754,
deepseq >= 1.3,
directory >= 1.2.2,
exceptions >= 0.10,
extra >= 1.6,
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,
mtl >= 2.2.1,
panic >= 0.3,
parameterized-utils >= 2.1 && < 2.2,
prettyprinter >= 1.7.0,
process >= 1.2,
scientific >= 0.3.6,
temporary >= 1.2,
template-haskell,
text >= 1.2.4.0 && < 1.3,
th-abstraction >=0.1 && <0.5,
th-lift >= 0.8.2 && < 0.9,
th-lift-instances >= 0.1 && < 0.2,
transformers >= 0.4,
unordered-containers >= 0.2.10,
utf8-string >= 1.0.1,
vector >= 0.12.1,
versions >= 4.0 && < 5.0,
zenc >= 0.1.0 && < 0.2.0,
ghc-prim >= 0.5.2
default-language: Haskell2010
default-extensions:
NondecreasingIndentation
hs-source-dirs: src
exposed-modules:
What4.BaseTypes
What4.Concrete
What4.Config
What4.FunctionName
What4.IndexLit
What4.Interface
What4.InterpretedFloatingPoint
What4.LabeledPred
What4.Panic
What4.Partial
What4.ProblemFeatures
What4.ProgramLoc
What4.SatResult
What4.SemiRing
What4.Symbol
What4.SFloat
What4.SWord
What4.WordMap
What4.Expr
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.Solver
What4.Solver.Adapter
What4.Solver.Boolector
What4.Solver.CVC4
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.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.Streams
What4.Utils.StringLiteral
What4.Utils.Word16String
What4.Utils.Versions
Test.Verification
ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
-- ghc-prof-options: -fprof-auto-top
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 adapter-test
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is: AdapterTest.hs
if flag(solverTests)
buildable: True
if ! flag(dRealTestDisable)
cpp-options: -DTEST_DREAL
if ! flag(STPTestDisable)
cpp-options: -DTEST_STP
else
buildable: False
build-depends:
base,
bv-sized,
bytestring,
containers,
data-binary-ieee754,
lens,
mtl >= 2.2.1,
parameterized-utils,
process,
tasty >= 0.10,
tasty-hunit >= 0.9,
text,
versions,
what4
ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite online-solver-test
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is: OnlineSolverTest.hs
if flag(solverTests)
buildable: True
if ! flag(STPTestDisable)
cpp-options: -DTEST_STP
else
buildable: False
build-depends:
base,
bv-sized,
bytestring,
containers,
data-binary-ieee754,
lens,
parameterized-utils,
process,
tasty >= 0.10,
tasty-hunit >= 0.9,
text,
versions,
what4
ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite expr-builder-smtlib2
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is: ExprBuilderSMTLib2.hs
build-depends:
base,
bv-sized,
bytestring,
containers,
data-binary-ieee754,
libBF,
parameterized-utils,
tasty >= 0.10,
tasty-hunit >= 0.9,
text,
versions,
what4
ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite exprs_tests
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is: ExprsTest.hs
other-modules:
GenWhat4Expr
build-depends: base
, bv-sized
, hedgehog >= 1.0.2
, parameterized-utils
, tasty >= 0.10
, tasty-hunit >= 0.9
, tasty-hedgehog
, what4
ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite iteexprs_tests
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is: IteExprs.hs
other-modules:
GenWhat4Expr
build-depends: base
, bv-sized
, hedgehog >= 1.0.2
, parameterized-utils
, tasty >= 0.10
, tasty-hunit >= 0.9
, tasty-hedgehog
, containers >= 0.5.0.0
, what4
ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite bvdomain_tests
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test, test/QC
main-is: BVDomTests.hs
other-modules: VerifyBindings
build-depends: base
, parameterized-utils
, tasty >= 0.10
, tasty-quickcheck >= 0.10
, QuickCheck >= 2.12
, transformers
, what4
ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite bvdomain_tests_hh
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test, test/HH
main-is: BVDomTests.hs
other-modules: VerifyBindings
build-depends: base
, parameterized-utils
, tasty >= 0.10
, tasty-hedgehog
, hedgehog >= 1.0.2
, transformers
, what4
ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
test-suite template_tests
type: exitcode-stdio-1.0
default-language: Haskell2010
hs-source-dirs: test
main-is : TestTemplate.hs
build-depends: base
, bv-sized
, libBF
, parameterized-utils
, tasty >= 0.10
, tasty-hedgehog
, hedgehog >= 1.0.2
, transformers
, what4
ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns