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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Trans
-- Copyright : (c) Brian Schroeder
-- Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- More generalized alternative to @Data.SBV@ for advanced client use
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Trans (
-- * Symbolic types
-- ** Booleans
SBool
-- *** Boolean values and functions
, sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), fromBool, oneIf
-- *** Logical functions
, sAnd, sOr, sAny, sAll
-- ** Bit-vectors
-- *** Unsigned bit-vectors
, SWord8, SWord16, SWord32, SWord64, SWord, WordN
-- *** Signed bit-vectors
, SInt8, SInt16, SInt32, SInt64, SInt, IntN
-- *** Converting between fixed-size and arbitrary bitvectors
, BVIsNonZero, FromSized, ToSized, fromSized, toSized
-- ** Unbounded integers
, SInteger
-- ** Floating point numbers
, SFloat, SDouble, SFloatingPoint
-- ** Algebraic reals
, SReal, AlgReal, sRealToSInteger
-- ** Characters, Strings and Regular Expressions
, SChar, SString
-- ** Symbolic lists
, SList
-- * Arrays of symbolic values
, SymArray(newArray_, newArray, readArray, writeArray, mergeArrays), SArray
-- * Creating symbolic values
-- ** Single value
, sBool, sWord8, sWord16, sWord32, sWord64, sWord, sInt8, sInt16, sInt32, sInt64, sInt, sInteger, sReal, sFloat, sDouble, sChar, sString, sList
-- ** List of values
, sBools, sWord8s, sWord16s, sWord32s, sWord64s, sWords, sInt8s, sInt16s, sInt32s, sInt64s, sInts, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings, sLists
-- * Symbolic Equality and Comparisons
, EqSymbolic(..), OrdSymbolic(..), Equality(..)
-- * Conditionals: Mergeable values
, Mergeable(..), ite, iteLazy
-- * Symbolic integral numbers
, SIntegral
-- * Division and Modulus
, SDivisible(..)
-- * Bit-vector operations
-- ** Conversions
, sFromIntegral
-- ** Shifts and rotates
, sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight
-- ** Finite bit-vector operations
, SFiniteBits(..)
-- ** Splitting, joining, and extending bit-vectors
, bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
-- ** Exponentiation
, (.^)
-- * IEEE-floating point numbers
, IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity
-- ** Rounding modes
, sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ
-- ** Conversion to/from floats
, IEEEFloatConvertible(..)
-- ** Bit-pattern conversions
, sFloatAsSWord32, sWord32AsSFloat
, sDoubleAsSWord64, sWord64AsSDouble
, sFloatingPointAsSWord, sWordAsSFloatingPoint
-- ** Extracting bit patterns from floats
, blastSFloat
, blastSDouble
, blastSFloatingPoint
-- * Enumerations
, mkSymbolicEnumeration
-- * Uninterpreted sorts, axioms, constants, and functions
, mkUninterpretedSort, SMTDefinable(..)
-- * Properties, proofs, and satisfiability
, Predicate, ConstraintSet, ProvableM(..), Provable, SatisfiableM(..), Satisfiable
, generateSMTBenchmarkSat, generateSMTBenchmarkProof
, solve
-- * Constraints
-- ** General constraints
, constrain, softConstrain
-- ** Constraint Vacuity
-- ** Named constraints and attributes
, namedConstraint, constrainWithAttribute
-- ** Unsat cores
-- ** Cardinality constraints
, pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed
-- * Checking safety
, sAssert, isSafe, SExecutable(..)
-- * Quick-checking
, sbvQuickCheck
-- * Optimization
-- ** Multiple optimization goals
, OptimizeStyle(..)
-- ** Objectives
, Objective(..)
-- ** Soft assumptions
, assertWithPenalty , Penalty(..)
-- ** Field extensions
-- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.
, ExtCV(..), GeneralizedCV(..)
-- * Model extraction
-- ** Inspecting proof results
, ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..)
-- ** Observing expressions
, observe
-- ** Programmable model extraction
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues, getModelUninterpretedValues
-- * SMT Interface
, SMTConfig(..), Timing(..), SMTLibVersion(..), Solver(..), SMTSolver(..)
-- ** Controlling verbosity
-- ** Solvers
, boolector, bitwuzla, cvc4, cvc5, dReal, yices, z3, mathSAT, abc
-- ** Configurations
, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers
, setLogic, Logic(..), setOption, setInfo, setTimeOut
-- ** SBV exceptions
, SBVException(..)
-- * Abstract SBV type
, SBV, HasKind(..), Kind(..), SymVal(..)
, MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith
-- * Module exports
, module Data.Bits
, module Data.Word
, module Data.Int
, module Data.Ratio
) where
import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Model
import Data.SBV.Core.Floating
import Data.SBV.Core.Sized
import Data.SBV.Core.Symbolic
import Data.SBV.Provers.Prover
import Data.SBV.Client
import Data.SBV.Client.BaseIO (FromSized, ToSized, fromSized, toSized)
import Data.SBV.Utils.TDiff (Timing(..))
import Data.Bits
import Data.Int
import Data.Ratio
import Data.Word
import Data.SBV.SMT.Utils (SBVException(..))
import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
|
