Copyright  (c) Brian Schroeder Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
 Symbolic types
 Arrays of symbolic values
 Creating symbolic values
 Symbolic Equality and Comparisons
 Conditionals: Mergeable values
 Symbolic integral numbers
 Division and Modulus
 Bitvector operations
 IEEEfloating point numbers
 Enumerations
 Uninterpreted sorts, constants, and functions
 Properties, proofs, and satisfiability
 Constraints
 Checking safety
 Quickchecking
 Optimization
 Model extraction
 SMT Interface
 Abstract SBV type
 Module exports
More generalized alternative to Data.SBV
for advanced client use
Synopsis
 type SBool = SBV Bool
 sTrue :: SBool
 sFalse :: SBool
 sNot :: SBool > SBool
 (.&&) :: SBool > SBool > SBool
 (.) :: SBool > SBool > SBool
 (.<+>) :: SBool > SBool > SBool
 (.~&) :: SBool > SBool > SBool
 (.~) :: SBool > SBool > SBool
 (.=>) :: SBool > SBool > SBool
 (.<=>) :: SBool > SBool > SBool
 fromBool :: Bool > SBool
 oneIf :: (Ord a, Num a, SymVal a) => SBool > SBV a
 sAnd :: [SBool] > SBool
 sOr :: [SBool] > SBool
 sAny :: (a > SBool) > [a] > SBool
 sAll :: (a > SBool) > [a] > SBool
 type SWord8 = SBV Word8
 type SWord16 = SBV Word16
 type SWord32 = SBV Word32
 type SWord64 = SBV Word64
 type SWord (n :: Nat) = SBV (WordN n)
 data WordN (n :: Nat)
 type SInt8 = SBV Int8
 type SInt16 = SBV Int16
 type SInt32 = SBV Int32
 type SInt64 = SBV Int64
 type SInt (n :: Nat) = SBV (IntN n)
 data IntN (n :: Nat)
 type family IsNonZero (arg :: Nat) :: Constraint where ...
 type family FromSized (t :: Type) :: Type where ...
 type family ToSized (t :: Type) :: Type where ...
 fromSized :: FromSizedBV a => a > FromSized a
 toSized :: ToSizedBV a => a > ToSized a
 type SInteger = SBV Integer
 type SFloat = SBV Float
 type SDouble = SBV Double
 type SReal = SBV AlgReal
 data AlgReal
 sRealToSInteger :: SReal > SInteger
 type SChar = SBV Char
 type SString = SBV String
 type SList a = SBV [a]
 class SymArray array where
 newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) > m (array a b)
 newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String > Maybe (SBV b) > m (array a b)
 readArray :: array a b > SBV a > SBV b
 writeArray :: SymVal b => array a b > SBV a > SBV b > array a b
 mergeArrays :: SymVal b => SBV Bool > array a b > array a b > array a b
 data SArray a b
 data SFunArray a b
 sBool :: MonadSymbolic m => String > m SBool
 sWord8 :: MonadSymbolic m => String > m SWord8
 sWord16 :: MonadSymbolic m => String > m SWord16
 sWord32 :: MonadSymbolic m => String > m SWord32
 sWord64 :: MonadSymbolic m => String > m SWord64
 sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String > m (SWord n)
 sInt8 :: MonadSymbolic m => String > m SInt8
 sInt16 :: MonadSymbolic m => String > m SInt16
 sInt32 :: MonadSymbolic m => String > m SInt32
 sInt64 :: MonadSymbolic m => String > m SInt64
 sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String > m (SInt n)
 sInteger :: MonadSymbolic m => String > m SInteger
 sReal :: MonadSymbolic m => String > m SReal
 sFloat :: MonadSymbolic m => String > m SFloat
 sDouble :: MonadSymbolic m => String > m SDouble
 sChar :: MonadSymbolic m => String > m SChar
 sString :: MonadSymbolic m => String > m SString
 sList :: (SymVal a, MonadSymbolic m) => String > m (SList a)
 sBools :: MonadSymbolic m => [String] > m [SBool]
 sWord8s :: MonadSymbolic m => [String] > m [SWord8]
 sWord16s :: MonadSymbolic m => [String] > m [SWord16]
 sWord32s :: MonadSymbolic m => [String] > m [SWord32]
 sWord64s :: MonadSymbolic m => [String] > m [SWord64]
 sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] > m [SWord n]
 sInt8s :: MonadSymbolic m => [String] > m [SInt8]
 sInt16s :: MonadSymbolic m => [String] > m [SInt16]
 sInt32s :: MonadSymbolic m => [String] > m [SInt32]
 sInt64s :: MonadSymbolic m => [String] > m [SInt64]
 sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] > m [SInt n]
 sIntegers :: MonadSymbolic m => [String] > m [SInteger]
 sReals :: MonadSymbolic m => [String] > m [SReal]
 sFloats :: MonadSymbolic m => [String] > m [SFloat]
 sDoubles :: MonadSymbolic m => [String] > m [SDouble]
 sChars :: MonadSymbolic m => [String] > m [SChar]
 sStrings :: MonadSymbolic m => [String] > m [SString]
 sLists :: (SymVal a, MonadSymbolic m) => [String] > m [SList a]
 class EqSymbolic a where
 class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
 class Equality a where
 class Mergeable a where
 ite :: Mergeable a => SBool > a > a > a
 iteLazy :: Mergeable a => SBool > a > a > a
 class (SymVal a, Num a, Bits a, Integral a) => SIntegral a
 class SDivisible a where
 sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a > SBV b
 sShiftLeft :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sShiftRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sRotateLeft :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a > SBV b > SBV a
 sRotateRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a > SBV b > SBV a
 sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a > SBV b > SBV a
 class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where
 sFiniteBitSize :: SBV a > Int
 lsb :: SBV a > SBool
 msb :: SBV a > SBool
 blastBE :: SBV a > [SBool]
 blastLE :: SBV a > [SBool]
 fromBitsBE :: [SBool] > SBV a
 fromBitsLE :: [SBool] > SBV a
 sTestBit :: SBV a > Int > SBool
 sExtractBits :: SBV a > [Int] > [SBool]
 sPopCount :: SBV a > SWord8
 setBitTo :: SBV a > Int > SBool > SBV a
 fullAdder :: SBV a > SBV a > (SBool, SBV a)
 fullMultiplier :: SBV a > SBV a > (SBV a, SBV a)
 sCountLeadingZeros :: SBV a > SWord8
 sCountTrailingZeros :: SBV a > SWord8
 bvExtract :: forall i j n bv proxy. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i  j) + 1)) => proxy i > proxy j > SBV (bv n) > SBV (bv ((i  j) + 1))
 (#) :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m)) => SBV (bv n) > SBV (bv m) > SBV (bv (n + m))
 zeroExtend :: forall n m bv. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m  n)), IsNonZero (m  n)) => SBV (bv n) > SBV (bv m)
 signExtend :: forall n m bv. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m  n)), IsNonZero (m  n)) => SBV (bv n) > SBV (bv m)
 bvDrop :: forall i n m bv proxy. (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m)  n) <= 0, IsNonZero (n  i)) => proxy i > SBV (bv n) > SBV (bv m)
 bvTake :: forall i n bv proxy. (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n) => proxy i > SBV (bv n) > SBV (bv i)
 (.^) :: (Mergeable b, Num b, SIntegral e) => b > SBV e > b
 class (SymVal a, RealFloat a) => IEEEFloating a where
 fpAbs :: SBV a > SBV a
 fpNeg :: SBV a > SBV a
 fpAdd :: SRoundingMode > SBV a > SBV a > SBV a
 fpSub :: SRoundingMode > SBV a > SBV a > SBV a
 fpMul :: SRoundingMode > SBV a > SBV a > SBV a
 fpDiv :: SRoundingMode > SBV a > SBV a > SBV a
 fpFMA :: SRoundingMode > SBV a > SBV a > SBV a > SBV a
 fpSqrt :: SRoundingMode > SBV a > SBV a
 fpRem :: SBV a > SBV a > SBV a
 fpRoundToIntegral :: SRoundingMode > SBV a > SBV a
 fpMin :: SBV a > SBV a > SBV a
 fpMax :: SBV a > SBV a > SBV a
 fpIsEqualObject :: SBV a > SBV a > SBool
 fpIsNormal :: SBV a > SBool
 fpIsSubnormal :: SBV a > SBool
 fpIsZero :: SBV a > SBool
 fpIsInfinite :: SBV a > SBool
 fpIsNaN :: SBV a > SBool
 fpIsNegative :: SBV a > SBool
 fpIsPositive :: SBV a > SBool
 fpIsNegativeZero :: SBV a > SBool
 fpIsPositiveZero :: SBV a > SBool
 fpIsPoint :: SBV a > SBool
 data RoundingMode
 type SRoundingMode = SBV RoundingMode
 nan :: Floating a => a
 infinity :: Floating a => a
 sNaN :: (Floating a, SymVal a) => SBV a
 sInfinity :: (Floating a, SymVal a) => SBV a
 sRoundNearestTiesToEven :: SRoundingMode
 sRoundNearestTiesToAway :: SRoundingMode
 sRoundTowardPositive :: SRoundingMode
 sRoundTowardNegative :: SRoundingMode
 sRoundTowardZero :: SRoundingMode
 sRNE :: SRoundingMode
 sRNA :: SRoundingMode
 sRTP :: SRoundingMode
 sRTN :: SRoundingMode
 sRTZ :: SRoundingMode
 class SymVal a => IEEEFloatConvertible a where
 fromSFloat :: SRoundingMode > SFloat > SBV a
 toSFloat :: SRoundingMode > SBV a > SFloat
 fromSDouble :: SRoundingMode > SDouble > SBV a
 toSDouble :: SRoundingMode > SBV a > SDouble
 sFloatAsSWord32 :: SFloat > SWord32
 sWord32AsSFloat :: SWord32 > SFloat
 sDoubleAsSWord64 :: SDouble > SWord64
 sWord64AsSDouble :: SWord64 > SDouble
 blastSFloat :: SFloat > (SBool, [SBool], [SBool])
 blastSDouble :: SDouble > (SBool, [SBool], [SBool])
 mkSymbolicEnumeration :: Name > Q [Dec]
 class Uninterpreted a where
 uninterpret :: String > a
 cgUninterpret :: String > [String] > a > a
 sbvUninterpret :: Maybe ([String], a) > String > a
 addAxiom :: MonadSymbolic m => String > [String] > m ()
 type Predicate = Symbolic SBool
 type Goal = Symbolic ()
 class ExtractIO m => MProvable m a where
 forAll_ :: a > SymbolicT m SBool
 forAll :: [String] > a > SymbolicT m SBool
 forSome_ :: a > SymbolicT m SBool
 forSome :: [String] > a > SymbolicT m SBool
 prove :: a > m ThmResult
 proveWith :: SMTConfig > a > m ThmResult
 sat :: a > m SatResult
 satWith :: SMTConfig > a > m SatResult
 allSat :: a > m AllSatResult
 allSatWith :: SMTConfig > a > m AllSatResult
 optimize :: OptimizeStyle > a > m OptimizeResult
 optimizeWith :: SMTConfig > OptimizeStyle > a > m OptimizeResult
 isVacuous :: a > m Bool
 isVacuousWith :: SMTConfig > a > m Bool
 isTheorem :: a > m Bool
 isTheoremWith :: SMTConfig > a > m Bool
 isSatisfiable :: a > m Bool
 isSatisfiableWith :: SMTConfig > a > m Bool
 validate :: Bool > SMTConfig > a > SMTResult > m SMTResult
 type Provable = MProvable IO
 proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, ThmResult)]
 proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, ThmResult)
 satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, SatResult)]
 satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, SatResult)
 generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool > a > m String
 solve :: MonadSymbolic m => [SBool] > m SBool
 constrain :: SolverContext m => SBool > m ()
 softConstrain :: SolverContext m => SBool > m ()
 namedConstraint :: SolverContext m => String > SBool > m ()
 constrainWithAttribute :: SolverContext m => [(String, String)] > SBool > m ()
 pbAtMost :: [SBool] > Int > SBool
 pbAtLeast :: [SBool] > Int > SBool
 pbExactly :: [SBool] > Int > SBool
 pbLe :: [(Int, SBool)] > Int > SBool
 pbGe :: [(Int, SBool)] > Int > SBool
 pbEq :: [(Int, SBool)] > Int > SBool
 pbMutexed :: [SBool] > SBool
 pbStronglyMutexed :: [SBool] > SBool
 sAssert :: HasKind a => Maybe CallStack > String > SBool > SBV a > SBV a
 isSafe :: SafeResult > Bool
 class ExtractIO m => SExecutable m a where
 sName_ :: a > SymbolicT m ()
 sName :: [String] > a > SymbolicT m ()
 safe :: a > m [SafeResult]
 safeWith :: SMTConfig > a > m [SafeResult]
 sbvQuickCheck :: Symbolic SBool > IO Bool
 data OptimizeStyle
 = Lexicographic
  Independent
  Pareto (Maybe Int)
 data Objective a
 class Metric a where
 type MetricSpace a :: *
 toMetricSpace :: SBV a > SBV (MetricSpace a)
 fromMetricSpace :: SBV (MetricSpace a) > SBV a
 msMinimize :: (MonadSymbolic m, SolverContext m) => String > SBV a > m ()
 msMaximize :: (MonadSymbolic m, SolverContext m) => String > SBV a > m ()
 assertWithPenalty :: MonadSymbolic m => String > SBool > Penalty > m ()
 data Penalty
 data ExtCV
 data GeneralizedCV
 newtype ThmResult = ThmResult SMTResult
 newtype SatResult = SatResult SMTResult
 newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])
 newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
 data OptimizeResult
 data SMTResult
 data SMTReasonUnknown
 observe :: SymVal a => String > SBV a > SBV a
 class SatModel a where
 class Modelable a where
 modelExists :: a > Bool
 getModelAssignment :: SatModel b => a > Either String (Bool, b)
 getModelDictionary :: a > Map String CV
 getModelValue :: SymVal b => String > a > Maybe b
 getModelUninterpretedValue :: String > a > Maybe String
 extractModel :: SatModel b => a > Maybe b
 getModelObjectives :: a > Map String GeneralizedCV
 getModelObjectiveValue :: String > a > Maybe GeneralizedCV
 getModelUIFuns :: a > Map String (SBVType, ([([CV], CV)], CV))
 getModelUIFunValue :: String > a > Maybe (SBVType, ([([CV], CV)], CV))
 displayModels :: SatModel a => ([(Bool, a)] > [(Bool, a)]) > (Int > (Bool, a) > IO ()) > AllSatResult > IO Int
 extractModels :: SatModel a => AllSatResult > [a]
 getModelDictionaries :: AllSatResult > [Map String CV]
 getModelValues :: SymVal b => String > AllSatResult > [Maybe b]
 getModelUninterpretedValues :: String > AllSatResult > [Maybe String]
 data SMTConfig = SMTConfig {
 verbose :: Bool
 timing :: Timing
 printBase :: Int
 printRealPrec :: Int
 satCmd :: String
 allSatMaxModelCount :: Maybe Int
 allSatPrintAlong :: Bool
 satTrackUFs :: Bool
 isNonModelVar :: String > Bool
 validateModel :: Bool
 optimizeValidateConstraints :: Bool
 transcript :: Maybe FilePath
 smtLibVersion :: SMTLibVersion
 solver :: SMTSolver
 allowQuantifiedQueries :: Bool
 roundingMode :: RoundingMode
 solverSetOptions :: [SMTOption]
 ignoreExitCode :: Bool
 redirectVerbose :: Maybe FilePath
 data Timing
 data SMTLibVersion = SMTLib2
 data Solver
 data SMTSolver = SMTSolver {
 name :: Solver
 executable :: String
 preprocess :: String > String
 options :: SMTConfig > [String]
 engine :: SMTEngine
 capabilities :: SolverCapabilities
 boolector :: SMTConfig
 cvc4 :: SMTConfig
 yices :: SMTConfig
 z3 :: SMTConfig
 mathSAT :: SMTConfig
 abc :: SMTConfig
 defaultSolverConfig :: Solver > SMTConfig
 defaultSMTCfg :: SMTConfig
 sbvCheckSolverInstallation :: SMTConfig > IO Bool
 sbvAvailableSolvers :: IO [SMTConfig]
 setLogic :: SolverContext m => Logic > m ()
 data Logic
 setOption :: SolverContext m => SMTOption > m ()
 setInfo :: SolverContext m => String > [String] > m ()
 setTimeOut :: SolverContext m => Integer > m ()
 data SBVException = SBVException {
 sbvExceptionDescription :: String
 sbvExceptionSent :: Maybe String
 sbvExceptionExpected :: Maybe String
 sbvExceptionReceived :: Maybe String
 sbvExceptionStdOut :: Maybe String
 sbvExceptionStdErr :: Maybe String
 sbvExceptionExitCode :: Maybe ExitCode
 sbvExceptionConfig :: SMTConfig
 sbvExceptionReason :: Maybe [String]
 sbvExceptionHint :: Maybe [String]
 data SBV a
 class HasKind a where
 kindOf :: a > Kind
 hasSign :: a > Bool
 intSizeOf :: a > Int
 isBoolean :: a > Bool
 isBounded :: a > Bool
 isReal :: a > Bool
 isFloat :: a > Bool
 isDouble :: a > Bool
 isUnbounded :: a > Bool
 isUninterpreted :: a > Bool
 isChar :: a > Bool
 isString :: a > Bool
 isList :: a > Bool
 isSet :: a > Bool
 isTuple :: a > Bool
 isMaybe :: a > Bool
 isEither :: a > Bool
 showType :: a > String
 data Kind
 class (HasKind a, Typeable a) => SymVal a where
 mkSymVal :: MonadSymbolic m => Maybe Quantifier > Maybe String > m (SBV a)
 literal :: a > SBV a
 fromCV :: CV > a
 isConcretely :: SBV a > (a > Bool) > Bool
 forall :: MonadSymbolic m => String > m (SBV a)
 forall_ :: MonadSymbolic m => m (SBV a)
 mkForallVars :: MonadSymbolic m => Int > m [SBV a]
 exists :: MonadSymbolic m => String > m (SBV a)
 exists_ :: MonadSymbolic m => m (SBV a)
 mkExistVars :: MonadSymbolic m => Int > m [SBV a]
 free :: MonadSymbolic m => String > m (SBV a)
 free_ :: MonadSymbolic m => m (SBV a)
 mkFreeVars :: MonadSymbolic m => Int > m [SBV a]
 symbolic :: MonadSymbolic m => String > m (SBV a)
 symbolics :: MonadSymbolic m => [String] > m [SBV a]
 unliteral :: SBV a > Maybe a
 isConcrete :: SBV a > Bool
 isSymbolic :: SBV a > Bool
 class MonadIO m => MonadSymbolic m where
 symbolicEnv :: m State
 type Symbolic = SymbolicT IO
 data SymbolicT m a
 label :: SymVal a => String > SBV a > SBV a
 output :: (Outputtable a, MonadSymbolic m) => a > m a
 runSMT :: MonadIO m => SymbolicT m a > m a
 runSMTWith :: MonadIO m => SMTConfig > SymbolicT m a > m a
 module Data.Bits
 module Data.Word
 module Data.Int
 module Data.Ratio
Symbolic types
Booleans
Boolean values and functions
oneIf :: (Ord a, Num a, SymVal a) => SBool > SBV a Source #
Returns 1 if the boolean is sTrue
, otherwise 0.
Logical functions
Bitvectors
Unsigned bitvectors
data WordN (n :: Nat) Source #
An unsigned bitvector carrying its size info
Instances
Signed bitvectors
A signed bitvector carrying its size info
Instances
Converting between fixedsize and arbitrary bitvectors
type family IsNonZero (arg :: Nat) :: Constraint where ... Source #
Type family to create the appropriate nonzero constraint
type family FromSized (t :: Type) :: Type where ... Source #
Capture the correspondence between sized and fixedsized BVs
FromSized (WordN 8) = Word8  
FromSized (WordN 16) = Word16  
FromSized (WordN 32) = Word32  
FromSized (WordN 64) = Word64  
FromSized (IntN 8) = Int8  
FromSized (IntN 16) = Int16  
FromSized (IntN 32) = Int32  
FromSized (IntN 64) = Int64  
FromSized (SWord 8) = SWord8  
FromSized (SWord 16) = SWord16  
FromSized (SWord 32) = SWord32  
FromSized (SWord 64) = SWord64  
FromSized (SInt 8) = SInt8  
FromSized (SInt 16) = SInt16  
FromSized (SInt 32) = SInt32  
FromSized (SInt 64) = SInt64 
type family ToSized (t :: Type) :: Type where ... Source #
Capture the correspondence between fixedsized and sized BVs
ToSized Word8 = WordN 8  
ToSized Word16 = WordN 16  
ToSized Word32 = WordN 32  
ToSized Word64 = WordN 64  
ToSized Int8 = IntN 8  
ToSized Int16 = IntN 16  
ToSized Int32 = IntN 32  
ToSized Int64 = IntN 64  
ToSized SWord8 = SWord 8  
ToSized SWord16 = SWord 16  
ToSized SWord32 = SWord 32  
ToSized SWord64 = SWord 64  
ToSized SInt8 = SInt 8  
ToSized SInt16 = SInt 16  
ToSized SInt32 = SInt 32  
ToSized SInt64 = SInt 64 
Unbounded integers
Floating point numbers
Algebraic reals
Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the rootsofpolynomials are represented implicitly by their defining equation
Instances
sRealToSInteger :: SReal > SInteger Source #
Convert an SReal to an SInteger. That is, it computes the
largest integer n
that satisfies sIntegerToSReal n <= r
essentially giving us the floor
.
For instance, 1.3
will be 1
, but 1.3
will be 2
.
Characters, Strings and Regular Expressions
type SChar = SBV Char Source #
A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
is currently an 8bit unsigned value, corresponding to the ISO88591 (Latin1) character
set: http://en.wikipedia.org/wiki/ISO/IEC_88591. A Haskell Char
, on the other hand, is based
on unicode. Therefore, there isn't a 11 correspondence between a Haskell character and an SBV
character for the time being. This limitation is due to the SMTsolvers only supporting this
particular subset. However, there is a pending proposal to add support for unicode, and SBV
will track these changes to have full unicode support as solvers become available. For
details, see: http://smtlib.cs.uiowa.edu/theoriesUnicodeStrings.shtml
type SString = SBV String Source #
A symbolic string. Note that a symbolic string is not a list of symbolic characters,
that is, it is not the case that SString = [SChar]
, unlike what one might expect following
Haskell strings. An SString
is a symbolic value of its own, of possibly arbitrary but finite length,
and internally processed as one unit as opposed to a fixedlength list of characters.
Symbolic lists
type SList a = SBV [a] Source #
A symbolic list of items. Note that a symbolic list is not a list of symbolic items,
that is, it is not the case that SList a = [a]
, unlike what one might expect following
haskell lists/sequences. An SList
is a symbolic value of its own, of possibly arbitrary but finite
length, and internally processed as one unit as opposed to a fixedlength list of items.
Note that lists can be nested, i.e., we do allow lists of lists of ... items.
Arrays of symbolic values
class SymArray array where Source #
Flat arrays of symbolic values
An array a b
is an array indexed by the type
, with elements of type SBV
a
.SBV
b
If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.
While it's certainly possible for user to create instances of SymArray
, the
SArray
and SFunArray
instances already provided should cover most use cases
in practice. Note that there are a few differences between these two models in
terms of use models:
SArray
produces SMTLib arrays, and requires a solver that understands the array theory.SFunArray
is internally handled, and thus can be used with any solver. (Note that all solvers exceptabc
support arrays, so this isn't a big decision factor.) For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
 Only
SArray
supports checking equality of arrays. (That is, checking if an entire array is equivalent to another.)SFunArray
s cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible.  Only
SFunArray
supports compilation to C. Programs usingSArray
will not be accepted by the Ccode generator.  You cannot use quickcheck on programs that contain these arrays. (Neither
SArray
norSFunArray
.)  With
SArray
, SBV transfers all arrayprocessing to the SMTsolver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. WithSFunArray
, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.
As a rule of thumb, try SArray
first. These should generate compact code. However, if
the backend solver has hard time solving the generated problems, switch to
SFunArray
. If you still have issues, please report so we can see what the problem might be!
newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) > m (array a b) Source #
Generalization of newArray_
newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String > Maybe (SBV b) > m (array a b) Source #
Generalization of newArray
readArray :: array a b > SBV a > SBV b Source #
Read the array element at a
writeArray :: SymVal b => array a b > SBV a > SBV b > array a b Source #
Update the element at a
to be b
mergeArrays :: SymVal b => SBV Bool > array a b > array a b > array a b Source #
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b
.
Merging pushes the ifthenelse choice down on to elements
Instances
Arrays implemented in terms of SMTarrays: http://smtlib.cs.uiowa.edu/theoriesArraysEx.shtml
 Maps directly to SMTlib arrays
 Reading from an unintialized value is OK. If the default value is given in
newArray
, it will be the result. Otherwise, the read yields an uninterpreted constant.  Can check for equality of these arrays
 Cannot be used in codegeneration (i.e., compilation to C)
 Cannot quickcheck theorems using
SArray
values  Typically slower as it heavily relies on SMTsolving for the array theory
Instances
Arrays implemented internally, without translating to SMTLib functions:
 Internally handled by the library and not mapped to SMTLib, hence can be used with solvers that don't support arrays. (Such as abc.)
 Reading from an unintialized value is OK. If the default value is given in
newArray
, it will be the result. Otherwise, the read yields an uninterpreted constant.  Cannot check for equality of arrays.
 Can be used in codegeneration (i.e., compilation to C).
 Can not quickcheck theorems using
SFunArray
values  Typically faster as it gets compiled away during translation.
Instances
Creating symbolic values
Single value
sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String > m (SWord n) Source #
Generalization of sWord
sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String > m (SInt n) Source #
Generalization of sInt
List of values
sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] > m [SWord n] Source #
Generalization of sWord64s
sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] > m [SInt n] Source #
Generalization of sInts
Symbolic Equality and Comparisons
class EqSymbolic a where Source #
Symbolic Equality. Note that we can't use Haskell's Eq
class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.
(.==) :: a > a > SBool infix 4 Source #
Symbolic equality.
(./=) :: a > a > SBool infix 4 Source #
Symbolic inequality.
(.===) :: a > a > SBool infix 4 Source #
Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that
is NaN == NaN
holds, but +0 == 0
doesn't. On other types, (.===) is simply (.==).
Note that (.==) is the right notion of equality for floats per IEEE754 specs, since by
definition +0 == 0
and NaN
equals no other value including itself. But occasionally
we want to be stronger and state NaN
equals NaN
and +0
and 0
are different from
each other. In a context where your type is concrete, simply use fpIsEqualObject
. But in
a polymorphic context, use the strong equality instead.
NB. If you do not care about or work with floats, simply use (.==) and (./=).
(./==) :: a > a > SBool infix 4 Source #
Negation of strong equality. Equaivalent to negation of (.===) on all types.
distinct :: [a] > SBool Source #
Returns (symbolic) sTrue
if all the elements of the given list are different.
allEqual :: [a] > SBool Source #
Returns (symbolic) sTrue
if all the elements of the given list are the same.
sElem :: a > [a] > SBool Source #
Symbolic membership test.
Instances
EqSymbolic Bool Source #  
Defined in Data.SBV.Core.Model  
EqSymbolic a => EqSymbolic [a] Source #  
EqSymbolic a => EqSymbolic (Maybe a) Source #  
EqSymbolic (SBV a) Source #  
Defined in Data.SBV.Core.Model  
EqSymbolic a => EqSymbolic (S a) Source #  Symbolic equality for 
Defined in Documentation.SBV.Examples.ProofTools.BMC  
(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source #  
Defined in Data.SBV.Core.Model  
(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source #  
Defined in Data.SBV.Core.Model  
EqSymbolic (SArray a b) Source #  
Defined in Data.SBV.Core.Model  
(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source #  
Defined in Data.SBV.Core.Model  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (./=) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.===) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (./==) :: (a, b, c, d) > (a, b, c, d) > SBool Source # distinct :: [(a, b, c, d)] > SBool Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (./=) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.===) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (./==) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # distinct :: [(a, b, c, d, e)] > SBool Source # allEqual :: [(a, b, c, d, e)] > SBool Source # sElem :: (a, b, c, d, e) > [(a, b, c, d, e)] > SBool Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (./=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.===) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (./==) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # distinct :: [(a, b, c, d, e, f)] > SBool Source # allEqual :: [(a, b, c, d, e, f)] > SBool Source # sElem :: (a, b, c, d, e, f) > [(a, b, c, d, e, f)] > SBool Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (./=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.===) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (./==) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # distinct :: [(a, b, c, d, e, f, g)] > SBool Source # allEqual :: [(a, b, c, d, e, f, g)] > SBool Source # sElem :: (a, b, c, d, e, f, g) > [(a, b, c, d, e, f, g)] > SBool Source # 
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #
Symbolic Comparisons. Similar to Eq
, we cannot implement Haskell's Ord
class
since there is no way to return an Ordering
value from a symbolic comparison.
Furthermore, OrdSymbolic
requires Mergeable
to implement ifthenelse, for the
benefit of implementing symbolic versions of max
and min
functions.
(.<) :: a > a > SBool infix 4 Source #
Symbolic less than.
(.<=) :: a > a > SBool infix 4 Source #
Symbolic less than or equal to.
(.>) :: a > a > SBool infix 4 Source #
Symbolic greater than.
(.>=) :: a > a > SBool infix 4 Source #
Symbolic greater than or equal to.
Symbolic minimum.
Symbolic maximum.
inRange :: a > (a, a) > SBool Source #
Is the value withing the allowed inclusive range?
Instances
OrdSymbolic a => OrdSymbolic [a] Source #  
OrdSymbolic a => OrdSymbolic (Maybe a) Source #  
Defined in Data.SBV.Core.Model  
(Ord a, SymVal a) => OrdSymbolic (SBV a) Source #  If comparison is over something SMTLib can handle, just translate it. Otherwise desugar. 
Defined in Data.SBV.Core.Model  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source #  
Defined in Data.SBV.Core.Model (.<) :: Either a b > Either a b > SBool Source # (.<=) :: Either a b > Either a b > SBool Source # (.>) :: Either a b > Either a b > SBool Source # (.>=) :: Either a b > Either a b > SBool Source # smin :: Either a b > Either a b > Either a b Source # smax :: Either a b > Either a b > Either a b Source # inRange :: Either a b > (Either a b, Either a b) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c) > (a, b, c) > SBool Source # (.<=) :: (a, b, c) > (a, b, c) > SBool Source # (.>) :: (a, b, c) > (a, b, c) > SBool Source # (.>=) :: (a, b, c) > (a, b, c) > SBool Source # smin :: (a, b, c) > (a, b, c) > (a, b, c) Source # smax :: (a, b, c) > (a, b, c) > (a, b, c) Source # inRange :: (a, b, c) > ((a, b, c), (a, b, c)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.<=) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.>) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.>=) :: (a, b, c, d) > (a, b, c, d) > SBool Source # smin :: (a, b, c, d) > (a, b, c, d) > (a, b, c, d) Source # smax :: (a, b, c, d) > (a, b, c, d) > (a, b, c, d) Source # inRange :: (a, b, c, d) > ((a, b, c, d), (a, b, c, d)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.<=) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.>) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.>=) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # smin :: (a, b, c, d, e) > (a, b, c, d, e) > (a, b, c, d, e) Source # smax :: (a, b, c, d, e) > (a, b, c, d, e) > (a, b, c, d, e) Source # inRange :: (a, b, c, d, e) > ((a, b, c, d, e), (a, b, c, d, e)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.<=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.>) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.>=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # smin :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > (a, b, c, d, e, f) Source # smax :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > (a, b, c, d, e, f) Source # inRange :: (a, b, c, d, e, f) > ((a, b, c, d, e, f), (a, b, c, d, e, f)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.<=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.>) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.>=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # smin :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) Source # smax :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) Source # inRange :: (a, b, c, d, e, f, g) > ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) > SBool Source # 
class Equality a where Source #
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bitprecise proofs.
Instances
Conditionals: Mergeable values
class Mergeable a where Source #
Symbolic conditionals are modeled by the Mergeable
class, describing
how to merge the results of an ifthenelse call with a symbolic test. SBV
provides all basic types as instances of this class, so users only need
to declare instances for custom datatypes of their programs as needed.
A Mergeable
instance may be automatically derived for a custom datatype
with a single constructor where the type of each field is an instance of
Mergeable
, such as a record of symbolic values. Users only need to add
Generic
and Mergeable
to the deriving
clause for the datatype. See
Status
for an example and an
illustration of what the instance would look like if written by hand.
The function select
is a totalindexing function out of a list of choices
with a default value, simulating array/list indexing. It's an nway generalization
of the ite
function.
Minimal complete definition: None, if the type is instance of Generic
. Otherwise
symbolicMerge
. Note that most types subject to merging are likely to be
trivial instances of Generic
.
Nothing
symbolicMerge :: Bool > SBool > a > a > a Source #
Merge two values based on the condition. The first argument states whether we force the thenandelse branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
select :: (Ord b, SymVal b, Num b) => [a] > a > SBV b > a Source #
Total indexing operation. select xs default index
is intuitively
the same as xs !! index
, except it evaluates to default
if index
underflows/overflows.
symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool > SBool > a > a > a Source #
Merge two values based on the condition. The first argument states whether we force the thenandelse branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
Instances
ite :: Mergeable a => SBool > a > a > a Source #
Ifthenelse. This is by definition symbolicMerge
with both
branches forced. This is typically the desired behavior, but also
see iteLazy
should you need more laziness.
iteLazy :: Mergeable a => SBool > a > a > a Source #
A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.
Symbolic integral numbers
class (SymVal a, Num a, Bits a, Integral a) => SIntegral a Source #
Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic typesignatures that work for all
symbolic numbers, such as SWord8
, SInt8
etc. For instance, we can write a generic
listminimum function as follows:
mm :: SIntegral a => [SBV a] > SBV a mm = foldr1 (a b > ite (a .<= b) a b)
It is similar to the standard Integral
class, except ranging over symbolic instances.
Instances
SIntegral Int8 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int16 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int32 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int64 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Integer Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word8 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word16 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word32 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word64 Source #  
Defined in Data.SBV.Core.Model  
(KnownNat n, IsNonZero n) => SIntegral (IntN n) Source #  
Defined in Data.SBV.Core.Sized  
(KnownNat n, IsNonZero n) => SIntegral (WordN n) Source #  
Defined in Data.SBV.Core.Sized 
Division and Modulus
class SDivisible a where Source #
The SDivisible
class captures the essence of division.
Unfortunately we cannot use Haskell's Integral
class since the Real
and Enum
superclasses are not implementable for symbolic bitvectors.
However, quotRem
and divMod
both make perfect sense, and the SDivisible
class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following pair of laws:
xsQuotRem
0 = (0, x) xsDivMod
0 = (0, x)
Note that our instances implement this law even when x
is 0
itself.
NB. quot
truncates toward zero, while div
truncates toward negative infinity.
C code generation of division operations
In the case of division or modulo of a minimal signed value (e.g. 128
for
SInt8
) by 1
, SMTLIB and Haskell agree on what the result should be.
Unfortunately the result in C code depends on CPU architecture and compiler
settings, as this is undefined behaviour in C. **SBV does not guarantee**
what will happen in generated C code in this corner case.
Instances
Bitvector operations
Conversions
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a > SBV b Source #
Conversion between integralsymbolic values, akin to Haskell's fromIntegral
Shifts and rotates
sShiftRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a Source #
Generalization of shiftR
, when the shiftamount is symbolic. Since Haskell's
shiftR
only takes an Int
as the shift amount, it cannot be used when we have
a symbolic amount to shift with.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
following the usual Haskell convention. See sSignedShiftArithRight
for a variant
that explicitly uses the msb as the sign bit, even for unsigned underlying types.
sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a > SBV b > SBV a Source #
An implementation of rotateleft, using a barrel shifter like design. Only works when both
arguments are finite bitvectors, and furthermore when the second argument is unsigned.
The first condition is enforced by the type, but the second is dynamically checked.
We provide this implementation as an alternative to sRotateLeft
since SMTLib logic
does not support variable argument rotates (as opposed to shifts), and thus this
implementation can produce better code for verification compared to sRotateLeft
.
>>>
prove $ \x y > (x `sBarrelRotateLeft` y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)
Q.E.D.
sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a > SBV b > SBV a Source #
An implementation of rotateright, using a barrel shifter like design. See comments
for sBarrelRotateLeft
for details.
>>>
prove $ \x y > (x `sBarrelRotateRight` y) `sBarrelRotateLeft` (y :: SWord32) .== (x :: SWord64)
Q.E.D.
sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a > SBV b > SBV a Source #
Arithmetic shiftright with a symbolic unsigned shift amount. This is equivalent
to sShiftRight
when the argument is signed. However, if the argument is unsigned,
then it explicitly treats its msb as a signbit, and uses it as the bit that
gets shifted in. Useful when using the underlying unsigned bit representation to implement
custom signed operations. Note that there is no direct Haskell analogue of this function.
Finite bitvector operations
class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where Source #
Finite bitlength symbolic values. Essentially the same as SIntegral
, but further leaves out Integer
. Loosely
based on Haskell's FiniteBits
class, but with more methods defined and structured differently to fit into the
symbolic world view. Minimal complete definition: sFiniteBitSize
.
sFiniteBitSize :: SBV a > Int Source #
Bit size.
lsb :: SBV a > SBool Source #
Least significant bit of a word, always stored at index 0.
msb :: SBV a > SBool Source #
Most significant bit of a word, always stored at the last position.
blastBE :: SBV a > [SBool] Source #
Bigendian blasting of a word into its bits.
blastLE :: SBV a > [SBool] Source #
Littleendian blasting of a word into its bits.
fromBitsBE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
fromBitsLE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
sTestBit :: SBV a > Int > SBool Source #
sExtractBits :: SBV a > [Int] > [SBool] Source #
Variant of sTestBit
, where we want to extract multiple bit positions.
sPopCount :: SBV a > SWord8 Source #
Variant of popCount
, returning a symbolic value.
setBitTo :: SBV a > Int > SBool > SBV a Source #
fullAdder :: SBV a > SBV a > (SBool, SBV a) Source #
Full adder, returns carryout from the addition. Only for unsigned quantities.
fullMultiplier :: SBV a > SBV a > (SBV a, SBV a) Source #
Full multipler, returns both high and loworder bits. Only for unsigned quantities.
sCountLeadingZeros :: SBV a > SWord8 Source #
Count leading zeros in a word, bigendian interpretation.
sCountTrailingZeros :: SBV a > SWord8 Source #
Count trailing zeros in a word, bigendian interpretation.
Instances
Splitting, joining, and extending bitvectors
:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i  j) + 1))  
=> proxy i 

> proxy j 

> SBV (bv n)  Input bit vector of size 
> SBV (bv ((i  j) + 1))  Output is of size 
Extract a portion of bits to form a smaller bitvector.
>>>
prove $ \x > bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
Q.E.D.
:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m))  
=> SBV (bv n)  First input, of size 
> SBV (bv m)  Second input, of size 
> SBV (bv (n + m))  Concatenation, of size 
Join two bitvectors.
>>>
prove $ \x y > x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
Q.E.D.
:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m  n)), IsNonZero (m  n))  
=> SBV (bv n)  Input, of size 
> SBV (bv m)  Output, of size 
Zero extend a bitvector.
>>>
prove $ \x > bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.
:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m  n)), IsNonZero (m  n))  
=> SBV (bv n)  Input, of size 
> SBV (bv m)  Output, of size 
Sign extend a bitvector.
>>>
prove $ \x > sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.>>>
prove $ \x > msb x .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
Q.E.D.
:: (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m)  n) <= 0, IsNonZero (n  i))  
=> proxy i 

> SBV (bv n)  Input, of size 
> SBV (bv m)  Output, of size 
Drop bits from the top of a bitvector.
>>>
prove $ \x > bvDrop (Proxy @0) (x :: SWord 43) .== x
Q.E.D.>>>
prove $ \x > bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0
Q.E.D.
:: (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n)  
=> proxy i 

> SBV (bv n)  Input, of size 
> SBV (bv i)  Output, of size 
Take bits from the top of a bitvector.
>>>
prove $ \x > bvTake (Proxy @13) (x :: SWord 13) .== x
Q.E.D.>>>
prove $ \x > bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
Q.E.D.>>>
prove $ \x > bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
Q.E.D.
Exponentiation
(.^) :: (Mergeable b, Num b, SIntegral e) => b > SBV e > b Source #
Symbolic exponentiation using bit blasting and repeated squaring.
N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.
IEEEfloating point numbers
class (SymVal a, RealFloat a) => IEEEFloating a where Source #
A class of floatingpoint (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.
Nothing
fpAbs :: SBV a > SBV a Source #
Compute the floating point absolute value.
fpNeg :: SBV a > SBV a Source #
Compute the unary negation. Note that 0  x
is not equivalent to x
for floatingpoint, since 0
and 0
are different.
fpAdd :: SRoundingMode > SBV a > SBV a > SBV a Source #
Add two floating point values, using the given rounding mode
fpSub :: SRoundingMode > SBV a > SBV a > SBV a Source #
Subtract two floating point values, using the given rounding mode
fpMul :: SRoundingMode > SBV a > SBV a > SBV a Source #
Multiply two floating point values, using the given rounding mode
fpDiv :: SRoundingMode > SBV a > SBV a > SBV a Source #
Divide two floating point values, using the given rounding mode
fpFMA :: SRoundingMode > SBV a > SBV a > SBV a > SBV a Source #
Fusedmultiplyadd three floating point values, using the given rounding mode. fpFMA x y z = x*y+z
but with only
one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
Haskell lacks an FMA implementation.
fpSqrt :: SRoundingMode > SBV a > SBV a Source #
Compute the squareroot of a float, using the given rounding mode
fpRem :: SBV a > SBV a > SBV a Source #
Compute the remainder: x  y * n
, where n
is the truncated integer nearest to x/y. The rounding mode
is implicitly assumed to be RoundNearestTiesToEven
.
fpRoundToIntegral :: SRoundingMode > SBV a > SBV a Source #
Round to the nearest integral value, using the given rounding mode.
fpMin :: SBV a > SBV a > SBV a Source #
Compute the minimum of two floats, respects infinity
and NaN
values
fpMax :: SBV a > SBV a > SBV a Source #
Compute the maximum of two floats, respects infinity
and NaN
values
fpIsEqualObject :: SBV a > SBV a > SBool Source #
Are the two given floats exactly the same. That is, NaN
will compare equal to itself, +0
will not compare
equal to 0
etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==
.)
fpIsNormal :: SBV a > SBool Source #
Is the floatingpoint number a normal value. (i.e., not denormalized.)
fpIsSubnormal :: SBV a > SBool Source #
Is the floatingpoint number a subnormal value. (Also known as denormal.)
fpIsZero :: SBV a > SBool Source #
Is the floatingpoint number 0? (Note that both +0 and 0 will satisfy this predicate.)
fpIsInfinite :: SBV a > SBool Source #
Is the floatingpoint number infinity? (Note that both +oo and oo will satisfy this predicate.)
fpIsNaN :: SBV a > SBool Source #
Is the floatingpoint number a NaN value?
fpIsNegative :: SBV a > SBool Source #
Is the floatingpoint number negative? Note that 0 satisfies this predicate but +0 does not.
fpIsPositive :: SBV a > SBool Source #
Is the floatingpoint number positive? Note that +0 satisfies this predicate but 0 does not.
fpIsNegativeZero :: SBV a > SBool Source #
Is the floating point number 0?
fpIsPositiveZero :: SBV a > SBool Source #
Is the floating point number +0?
fpIsPoint :: SBV a > SBool Source #
Is the floatingpoint number a regular floating point, i.e., not NaN, nor +oo, nor oo. Normals or denormals are allowed.
Instances
data RoundingMode Source #
Rounding mode to be used for the IEEE floatingpoint operations.
Note that Haskell's default is RoundNearestTiesToEven
. If you use
a different rounding mode, then the counterexamples you get may not
match what you observe in Haskell.
RoundNearestTiesToEven  Round to nearest representable floating point value. If precisely at halfway, pick the even number. (In this context, even means the lowestorder bit is zero.) 
RoundNearestTiesToAway  Round to nearest representable floating point value. If precisely at halfway, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.) 
RoundTowardPositive  Round towards positive infinity. (Also known as roundingup or ceiling.) 
RoundTowardNegative  Round towards negative infinity. (Also known as roundingdown or floor.) 
RoundTowardZero  Round towards zero. (Also known as truncation.) 
Instances
type SRoundingMode = SBV RoundingMode Source #
The symbolic variant of RoundingMode
Rounding modes
sRoundNearestTiesToEven :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToAway :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToAway
sRoundTowardPositive :: SRoundingMode Source #
Symbolic variant of RoundTowardPositive
sRoundTowardNegative :: SRoundingMode Source #
Symbolic variant of RoundTowardNegative
sRoundTowardZero :: SRoundingMode Source #
Symbolic variant of RoundTowardZero
sRNE :: SRoundingMode Source #
Alias for sRoundNearestTiesToEven
sRNA :: SRoundingMode Source #
Alias for sRoundNearestTiesToAway
sRTP :: SRoundingMode Source #
Alias for sRoundTowardPositive
sRTN :: SRoundingMode Source #
Alias for sRoundTowardNegative
sRTZ :: SRoundingMode Source #
Alias for sRoundTowardZero
Conversion to/from floats
class SymVal a => IEEEFloatConvertible a where Source #
Capture convertability from/to FloatingPoint representations.
Conversions to float: toSFloat
and toSDouble
simply return the
nearest representable float from the given type based on the rounding
mode provided.
Conversions from float: fromSFloat
and fromSDouble
functions do
the reverse conversion. However some care is needed when given values
that are not representable in the integral target domain. For instance,
converting an SFloat
to an SInt8
is problematic. The rules are as follows:
If the input value is a finite point and when rounded in the given rounding mode to an integral value lies within the target bounds, then that result is returned. (This is the regular interpretation of rounding in IEEE754.)
Otherwise (i.e., if the integral value in the float or double domain) doesn't
fit into the target type, then the result is unspecified. Note that if the input
is +oo
, oo
, or NaN
, then the result is unspecified.
Due to the unspecified nature of conversions, SBV will never constant fold conversions from floats to integral values. That is, you will always get a symbolic value as output. (Conversions from floats to other floats will be constant folded. Conversions from integral values to floats will also be constant folded.)
Note that unspecified really means unspecified: In particular, SBV makes
no guarantees about matching the behavior between what you might get in
Haskell, via SMTLib, or the Ctranslation. If the input value is outofbounds
as defined above, or is NaN
or oo
or oo
, then all bets are off. In particular
C and SMTLib are decidedly undefine this case, though that doesn't mean they do the
same thing! Same goes for Haskell, which seems to convert via Int64, but we do
not model that behavior in SBV as it doesn't seem to be intentional nor well documented.
You can check for NaN
, oo
and oo
, using the predicates fpIsNaN
, fpIsInfinite
,
and fpIsPositive
, fpIsNegative
predicates, respectively; and do the proper conversion
based on your needs. (0 is a good choice, as are min/max bounds of the target type.)
Currently, SBV provides no predicates to check if a value would lie within range for a particular conversion task, as this depends on the rounding mode and the types involved and can be rather tricky to determine. (See http://github.com/LeventErkok/sbv/issues/456 for a discussion of the issues involved.) In a future release, we hope to be able to provide underflow and overflow predicates for these conversions as well.
Nothing
fromSFloat :: SRoundingMode > SFloat > SBV a Source #
Convert from an IEEE74 single precision float.
toSFloat :: SRoundingMode > SBV a > SFloat Source #
Convert to an IEEE754 Singleprecision float.
>>>
:{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode > SBV a > SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}
>>>
prove $ roundTrip @Int8
Q.E.D.>>>
prove $ roundTrip @Word8
Q.E.D.>>>
prove $ roundTrip @Int16
Q.E.D.>>>
prove $ roundTrip @Word16
Q.E.D.>>>
prove $ roundTrip @Int32
Falsifiable. Counterexample: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 134280664 :: Int32
Note how we get a failure on Int32
. The counterexample value is not representable exactly as a single precision float:
>>>
toRational (134280664 :: Float)
134280672 % 1
Note how the numerator is different, it is off by 8. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.
toSFloat :: Integral a => SRoundingMode > SBV a > SFloat Source #
Convert to an IEEE754 Singleprecision float.
>>>
:{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode > SBV a > SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}
>>>
prove $ roundTrip @Int8
Q.E.D.>>>
prove $ roundTrip @Word8
Q.E.D.>>>
prove $ roundTrip @Int16
Q.E.D.>>>
prove $ roundTrip @Word16
Q.E.D.>>>
prove $ roundTrip @Int32
Falsifiable. Counterexample: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 134280664 :: Int32
Note how we get a failure on Int32
. The counterexample value is not representable exactly as a single precision float:
>>>
toRational (134280664 :: Float)
134280672 % 1
Note how the numerator is different, it is off by 8. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.
fromSDouble :: SRoundingMode > SDouble > SBV a Source #
Convert from an IEEE74 double precision float.
toSDouble :: SRoundingMode > SBV a > SDouble Source #
Convert to an IEEE754 Doubleprecision float.
>>>
:{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode > SBV a > SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}
>>>
prove $ roundTrip @Int8
Q.E.D.>>>
prove $ roundTrip @Word8
Q.E.D.>>>
prove $ roundTrip @Int16
Q.E.D.>>>
prove $ roundTrip @Word16
Q.E.D.>>>
prove $ roundTrip @Int32
Q.E.D.>>>
prove $ roundTrip @Word32
Q.E.D.>>>
prove $ roundTrip @Int64
Falsifiable. Counterexample: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 8005056270191255168 :: Int64
Just like in the SFloat
case, once we reach 64bits, we no longer can exactly represent the
integer value for all possible values:
>>>
toRational (8005056270191255168 :: Double)
8005056270191255552 % 1
In this case the numerator is off by 384!
toSDouble :: Integral a => SRoundingMode > SBV a > SDouble Source #
Convert to an IEEE754 Doubleprecision float.
>>>
:{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode > SBV a > SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}
>>>
prove $ roundTrip @Int8
Q.E.D.>>>
prove $ roundTrip @Word8
Q.E.D.>>>
prove $ roundTrip @Int16
Q.E.D.>>>
prove $ roundTrip @Word16
Q.E.D.>>>
prove $ roundTrip @Int32
Q.E.D.>>>
prove $ roundTrip @Word32
Q.E.D.>>>
prove $ roundTrip @Int64
Falsifiable. Counterexample: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 8005056270191255168 :: Int64
Just like in the SFloat
case, once we reach 64bits, we no longer can exactly represent the
integer value for all possible values:
>>>
toRational (8005056270191255168 :: Double)
8005056270191255552 % 1
In this case the numerator is off by 384!
Instances
Bitpattern conversions
sFloatAsSWord32 :: SFloat > SWord32 Source #
Convert an SFloat
to an SWord32
, preserving the bitcorrespondence. Note that since the
representation for NaN
s are not unique, this function will return a symbolic value when given a
concrete NaN
.
Implementation note: Since there's no corresponding function in SMTLib for conversion to bitrepresentation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In codegeneration mode, we simply map it to a simple conversion.
sWord32AsSFloat :: SWord32 > SFloat Source #
Reinterpret the bits in a 32bit word as a singleprecision floating point number
sDoubleAsSWord64 :: SDouble > SWord64 Source #
Convert an SDouble
to an SWord64
, preserving the bitcorrespondence. Note that since the
representation for NaN
s are not unique, this function will return a symbolic value when given a
concrete NaN
.
See the implementation note for sFloatAsSWord32
, as it applies here as well.
sWord64AsSDouble :: SWord64 > SDouble Source #
Reinterpret the bits in a 32bit word as a singleprecision floating point number
blastSFloat :: SFloat > (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a singleprecision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
blastSDouble :: SDouble > (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a singleprecision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
Enumerations
Uninterpreted sorts, constants, and functions
class Uninterpreted a where Source #
Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpretedfunctions as a general means of blackbox'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Minimal complete definition: sbvUninterpret
. However, most instances in
practice are already provided by SBV, so endusers should not need to define their
own instances.
uninterpret :: String > a Source #
Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.
cgUninterpret :: String > [String] > a > a Source #
Uninterpret a value, only for the purposes of codegeneration. For execution and verification the value is used as is. For codegeneration, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.
sbvUninterpret :: Maybe ([String], a) > String > a Source #
Most generalized form of uninterpretation, this function should not be needed by endusercode, but is rather useful for the library development.