-
Notifications
You must be signed in to change notification settings - Fork 45
/
z3.cabal
147 lines (119 loc) · 4.43 KB
/
z3.cabal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
Name: z3
Version: 411.0.1
Synopsis: Bindings for the Z3 Theorem Prover
Description:
Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).
.
* "Z3.Base.C" provides the raw foreign imports from Z3's C API.
.
* "Z3.Base" does the marshaling of values between Haskell and C,
and transparently handles reference counting of Z3 objects for you.
.
* "Z3.Monad" provides a convenient monadic wrapper for the common usage scenario.
.
Examples: <https://github.com/IagoAbal/haskell-z3/tree/master/examples>
.
Changelog: <https://github.com/IagoAbal/haskell-z3/blob/master/CHANGES.md>
.
Installation:
.
* /Unix-like/: Just be sure to use the standard locations for
dynamic libraries (\/usr\/lib) and header files (\/usr\/include),
or else use the --extra-lib-dirs and --extra-include-dirs Cabal flags.
.
(Hackage reports a build failure because Z3's library is missing.)
Homepage: https://github.com/IagoAbal/haskell-z3
Bug-reports: https://github.com/IagoAbal/haskell-z3/issues
License: BSD3
License-file: LICENSE
Author: Iago Abal <[email protected]>,
David Castro <[email protected]>
Maintainer: Iago Abal <[email protected]>
Copyright: 2012-2022, Iago Abal, David Castro
Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors
Build-type: Simple
Cabal-version: >= 1.10
Extra-source-files: README.md CHANGES.md HACKING.md
source-repository head
type: git
location: [email protected]:IagoAbal/haskell-z3.git
Library
hs-source-dirs: src
Exposed-modules:
Z3.Base
Z3.Base.C
Z3.Opts
Z3.Monad
Other-Modules:
Z3.Common
Z3.RLock
Z3.Lock
-- TODO: Add flag to compile with -Werror, Hackage doesn't like it.
ghc-options: -Wall
-- Ban to mtl-2.1: modify in MonadState causes <<loop>> in mtl-2.1
Build-depends: base >= 4.5 && <5,
containers,
transformers >= 0.2
if impl(ghc < 8)
Build-depends: semigroups >= 0.5
Build-tools: hsc2hs
Default-language: Haskell2010
Default-extensions: FlexibleInstances
FlexibleContexts
ForeignFunctionInterface
MultiParamTypeClasses
Other-extensions: CPP
DeriveDataTypeable
EmptyDataDecls
GeneralizedNewtypeDeriving
PatternGuards
includes: z3.h
-- In OS X libz3 is linked statically against libgomp.
-- In Windows Z3 is compiled using MS C++.
if os(darwin) || os(windows)
extra-libraries: z3
else
extra-libraries: gomp z3 gomp
Flag examples
Description: Build examples.
Default: False
Manual: True
Executable examples
if flag(examples)
Buildable: True
Build-depends: base >=4.5,
z3,
containers,
transformers >= 0.2
else
Buildable: False
Default-language: Haskell2010
Hs-source-dirs: examples
Main-Is: Examples.hs
Other-Modules: Example.Monad.Queens4
Example.Monad.Queens4All
Example.Monad.DataTypes
Example.Monad.FuncModel
Example.Monad.MutuallyRecursive
Example.Monad.ParserInterface
Example.Monad.ParserEvalInterface
Example.Monad.Quantifiers
Example.Monad.QuantifierElimination
Example.Monad.ToSMTLib
Example.Monad.Tuple
Test-suite spec
Type: exitcode-stdio-1.0
Ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N
Default-language: Haskell2010
Default-extensions: ScopedTypeVariables
Hs-source-dirs: test
examples
Main-is: Spec.hs
Other-modules: Z3.Base.Spec
Z3.Monad.Spec
Z3.Regression
Example.Monad.IntList
Build-depends: base >= 4.5,
z3,
hspec >= 2.1,
QuickCheck >= 2.5.1