1-----------------------------------------------------------------------------
2-- |
3-- Module    : Data.SBV.Trans
4-- Copyright : (c) Brian Schroeder
5--                 Levent Erkok
6-- License   : BSD3
7-- Maintainer: erkokl@gmail.com
8-- Stability : experimental
9--
10-- More generalized alternative to @Data.SBV@ for advanced client use
11-----------------------------------------------------------------------------
12
13{-# OPTIONS_GHC -Wall -Werror #-}
14
15module Data.SBV.Trans (
16  -- * Symbolic types
17
18  -- ** Booleans
19    SBool
20  -- *** Boolean values and functions
21  , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), fromBool, oneIf
22  -- *** Logical functions
23  , sAnd, sOr, sAny, sAll
24  -- ** Bit-vectors
25  -- *** Unsigned bit-vectors
26  , SWord8, SWord16, SWord32, SWord64, SWord, WordN
27  -- *** Signed bit-vectors
28  , SInt8, SInt16, SInt32, SInt64, SInt, IntN
29  -- *** Converting between fixed-size and arbitrary bitvectors
30  , BVIsNonZero, FromSized, ToSized, fromSized, toSized
31  -- ** Unbounded integers
32  , SInteger
33  -- ** Floating point numbers
34  , SFloat, SDouble, SFloatingPoint
35  -- ** Algebraic reals
36  , SReal, AlgReal, sRealToSInteger
37  -- ** Characters, Strings and Regular Expressions
38  , SChar, SString
39  -- ** Symbolic lists
40  , SList
41  -- * Arrays of symbolic values
42  , SymArray(newArray_, newArray, readArray, writeArray, mergeArrays), SArray, SFunArray
43
44  -- * Creating symbolic values
45  -- ** Single value
46  , sBool, sWord8, sWord16, sWord32, sWord64, sWord, sInt8, sInt16, sInt32, sInt64, sInt, sInteger, sReal, sFloat, sDouble, sChar, sString, sList
47
48  -- ** List of values
49  , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sWords, sInt8s, sInt16s, sInt32s, sInt64s, sInts, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings, sLists
50
51  -- * Symbolic Equality and Comparisons
52  , EqSymbolic(..), OrdSymbolic(..), Equality(..)
53  -- * Conditionals: Mergeable values
54  , Mergeable(..), ite, iteLazy
55
56  -- * Symbolic integral numbers
57  , SIntegral
58  -- * Division and Modulus
59  , SDivisible(..)
60  -- * Bit-vector operations
61  -- ** Conversions
62  , sFromIntegral
63  -- ** Shifts and rotates
64  , sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight
65  -- ** Finite bit-vector operations
66  , SFiniteBits(..)
67  -- ** Splitting, joining, and extending bit-vectors
68  , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
69  -- ** Exponentiation
70  , (.^)
71  -- * IEEE-floating point numbers
72  , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity
73  -- ** Rounding modes
74  , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ
75  -- ** Conversion to/from floats
76  , IEEEFloatConvertible(..)
77
78  -- ** Bit-pattern conversions
79  , sFloatAsSWord32,       sWord32AsSFloat
80  , sDoubleAsSWord64,      sWord64AsSDouble
81  , sFloatingPointAsSWord, sWordAsSFloatingPoint
82
83  -- ** Extracting bit patterns from floats
84  , blastSFloat
85  , blastSDouble
86  , blastSFloatingPoint
87
88  -- * Enumerations
89  , mkSymbolicEnumeration
90
91  -- * Uninterpreted sorts, axioms, constants, and functions
92  , mkUninterpretedSort, Uninterpreted(..), addAxiom
93
94  -- * Properties, proofs, and satisfiability
95  , Predicate, Goal, MProvable(..), Provable, proveWithAll, proveWithAny , satWithAll
96  , proveConcurrentWithAny, proveConcurrentWithAll, satConcurrentWithAny, satConcurrentWithAll
97  , satWithAny, generateSMTBenchmark
98  , solve
99  -- * Constraints
100  -- ** General constraints
101  , constrain, softConstrain
102
103  -- ** Constraint Vacuity
104
105  -- ** Named constraints and attributes
106  , namedConstraint, constrainWithAttribute
107
108  -- ** Unsat cores
109
110  -- ** Cardinality constraints
111  , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed
112
113  -- * Checking safety
114  , sAssert, isSafe, SExecutable(..)
115
116  -- * Quick-checking
117  , sbvQuickCheck
118
119  -- * Optimization
120
121  -- ** Multiple optimization goals
122  , OptimizeStyle(..)
123  -- ** Objectives
124  , Objective(..), Metric(..)
125  -- ** Soft assumptions
126  , assertWithPenalty , Penalty(..)
127  -- ** Field extensions
128  -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.
129  , ExtCV(..), GeneralizedCV(..)
130
131  -- * Model extraction
132
133  -- ** Inspecting proof results
134  , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..)
135
136  -- ** Observing expressions
137  , observe
138
139  -- ** Programmable model extraction
140  , SatModel(..), Modelable(..), displayModels, extractModels
141  , getModelDictionaries, getModelValues, getModelUninterpretedValues
142
143  -- * SMT Interface
144  , SMTConfig(..), Timing(..), SMTLibVersion(..), Solver(..), SMTSolver(..)
145  -- ** Controlling verbosity
146
147  -- ** Solvers
148  , boolector, cvc4, yices, z3, mathSAT, abc
149  -- ** Configurations
150  , defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers
151  , setLogic, Logic(..), setOption, setInfo, setTimeOut
152  -- ** SBV exceptions
153  , SBVException(..)
154
155  -- * Abstract SBV type
156  , SBV, HasKind(..), Kind(..), SymVal(..)
157  , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith
158
159  -- * Module exports
160
161  , module Data.Bits
162  , module Data.Word
163  , module Data.Int
164  , module Data.Ratio
165  ) where
166
167import Data.SBV.Core.AlgReals
168import Data.SBV.Core.Data
169import Data.SBV.Core.Kind
170import Data.SBV.Core.Model
171import Data.SBV.Core.Floating
172import Data.SBV.Core.Sized
173import Data.SBV.Core.Symbolic
174
175import Data.SBV.Provers.Prover
176
177import Data.SBV.Client
178import Data.SBV.Client.BaseIO  (FromSized, ToSized, fromSized, toSized)
179
180
181import Data.SBV.Utils.TDiff   (Timing(..))
182
183import Data.Bits
184import Data.Int
185import Data.Ratio
186import Data.Word
187
188import Data.SBV.SMT.Utils (SBVException(..))
189import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
190