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