sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright (c) Brian SchroederLevent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Trans

Description

More generalized alternative to Data.SBV for advanced client use

Synopsis

# Symbolic types

## Booleans

type SBool = SBV Bool Source #

A symbolic boolean/bit

### Boolean values and functions

Symbolic True

Symbolic False

Symbolic boolean negation

(.&&) :: SBool -> SBool -> SBool infixr 3 Source #

Symbolic conjunction

(.||) :: SBool -> SBool -> SBool infixr 2 Source #

Symbolic disjunction

(.<+>) :: SBool -> SBool -> SBool infixl 6 Source #

Symbolic logical xor

(.~&) :: SBool -> SBool -> SBool infixr 3 Source #

Symbolic nand

(.~|) :: SBool -> SBool -> SBool infixr 2 Source #

Symbolic nor

(.=>) :: SBool -> SBool -> SBool infixr 1 Source #

Symbolic implication

(.<=>) :: SBool -> SBool -> SBool infixr 1 Source #

Symbolic boolean equivalence

Conversion from Bool to SBool

oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a Source #

Returns 1 if the boolean is sTrue, otherwise 0.

### Logical functions

sAnd :: [SBool] -> SBool Source #

Generalization of and

sOr :: [SBool] -> SBool Source #

Generalization of or

sAny :: (a -> SBool) -> [a] -> SBool Source #

Generalization of any

sAll :: (a -> SBool) -> [a] -> SBool Source #

Generalization of all

## Bit-vectors

### Unsigned bit-vectors

8-bit unsigned symbolic value

16-bit unsigned symbolic value

32-bit unsigned symbolic value

64-bit unsigned symbolic value

type SWord (n :: Nat) = SBV (WordN n) Source #

A symbolic unsigned bit-vector carrying its size info

data WordN (n :: Nat) Source #

An unsigned bit-vector carrying its size info

Instances
 (KnownNat n, IsNonZero n) => Bounded (WordN n) Source # Bounded instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Methods (KnownNat n, IsNonZero n) => Enum (WordN n) Source # Enum instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Methodssucc :: WordN n -> WordN n #pred :: WordN n -> WordN n #toEnum :: Int -> WordN n #fromEnum :: WordN n -> Int #enumFrom :: WordN n -> [WordN n] #enumFromThen :: WordN n -> WordN n -> [WordN n] #enumFromTo :: WordN n -> WordN n -> [WordN n] #enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] # Eq (WordN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methods(==) :: WordN n -> WordN n -> Bool #(/=) :: WordN n -> WordN n -> Bool # (KnownNat n, IsNonZero n) => Integral (WordN n) Source # Integral instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Methodsquot :: WordN n -> WordN n -> WordN n #rem :: WordN n -> WordN n -> WordN n #div :: WordN n -> WordN n -> WordN n #mod :: WordN n -> WordN n -> WordN n #quotRem :: WordN n -> WordN n -> (WordN n, WordN n) #divMod :: WordN n -> WordN n -> (WordN n, WordN n) #toInteger :: WordN n -> Integer # (KnownNat n, IsNonZero n) => Num (WordN n) Source # Num instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Methods(+) :: WordN n -> WordN n -> WordN n #(-) :: WordN n -> WordN n -> WordN n #(*) :: WordN n -> WordN n -> WordN n #negate :: WordN n -> WordN n #abs :: WordN n -> WordN n #signum :: WordN n -> WordN n # Ord (WordN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methodscompare :: WordN n -> WordN n -> Ordering #(<) :: WordN n -> WordN n -> Bool #(<=) :: WordN n -> WordN n -> Bool #(>) :: WordN n -> WordN n -> Bool #(>=) :: WordN n -> WordN n -> Bool #max :: WordN n -> WordN n -> WordN n #min :: WordN n -> WordN n -> WordN n # (KnownNat n, IsNonZero n) => Real (WordN n) Source # Real instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodstoRational :: WordN n -> Rational # Show (WordN n) Source # Show instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodsshowsPrec :: Int -> WordN n -> ShowS #show :: WordN n -> String #showList :: [WordN n] -> ShowS # (KnownNat n, IsNonZero n) => Bits (WordN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methods(.&.) :: WordN n -> WordN n -> WordN n #(.|.) :: WordN n -> WordN n -> WordN n #xor :: WordN n -> WordN n -> WordN n #complement :: WordN n -> WordN n #shift :: WordN n -> Int -> WordN n #rotate :: WordN n -> Int -> WordN n #bit :: Int -> WordN n #setBit :: WordN n -> Int -> WordN n #clearBit :: WordN n -> Int -> WordN n #complementBit :: WordN n -> Int -> WordN n #testBit :: WordN n -> Int -> Bool #bitSize :: WordN n -> Int #isSigned :: WordN n -> Bool #shiftL :: WordN n -> Int -> WordN n #unsafeShiftL :: WordN n -> Int -> WordN n #shiftR :: WordN n -> Int -> WordN n #unsafeShiftR :: WordN n -> Int -> WordN n #rotateL :: WordN n -> Int -> WordN n #rotateR :: WordN n -> Int -> WordN n #popCount :: WordN n -> Int # (KnownNat n, IsNonZero n) => HasKind (WordN n) Source # WordN has a kind Instance detailsDefined in Data.SBV.Core.Sized MethodskindOf :: WordN n -> Kind Source #hasSign :: WordN n -> Bool Source #intSizeOf :: WordN n -> Int Source #isReal :: WordN n -> Bool Source #isFloat :: WordN n -> Bool Source #isDouble :: WordN n -> Bool Source #isChar :: WordN n -> Bool Source #isString :: WordN n -> Bool Source #isList :: WordN n -> Bool Source #isSet :: WordN n -> Bool Source #isTuple :: WordN n -> Bool Source #isMaybe :: WordN n -> Bool Source #isEither :: WordN n -> Bool Source # (KnownNat n, IsNonZero n) => SymVal (WordN n) Source # SymVal instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (WordN n)) Source #literal :: WordN n -> SBV (WordN n) Source #fromCV :: CV -> WordN n Source #isConcretely :: SBV (WordN n) -> (WordN n -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV (WordN n)) Source #forall_ :: MonadSymbolic m => m (SBV (WordN n)) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV (WordN n)] Source #exists :: MonadSymbolic m => String -> m (SBV (WordN n)) Source #exists_ :: MonadSymbolic m => m (SBV (WordN n)) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV (WordN n)] Source #free :: MonadSymbolic m => String -> m (SBV (WordN n)) Source #free_ :: MonadSymbolic m => m (SBV (WordN n)) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV (WordN n)] Source #symbolic :: MonadSymbolic m => String -> m (SBV (WordN n)) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV (WordN n)] Source #unliteral :: SBV (WordN n) -> Maybe (WordN n) Source #isConcrete :: SBV (WordN n) -> Bool Source #isSymbolic :: SBV (WordN n) -> Bool Source # (KnownNat n, IsNonZero n) => SatModel (WordN n) Source # Constructing models for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodsparseCVs :: [CV] -> Maybe (WordN n, [CV]) Source #cvtModel :: (WordN n -> Maybe b) -> Maybe (WordN n, [CV]) -> Maybe (b, [CV]) Source # (KnownNat n, IsNonZero n) => Metric (WordN n) Source # Optimizing WordN Instance detailsDefined in Data.SBV.Core.Sized Associated Typestype MetricSpace (WordN n) :: Type Source # MethodstoMetricSpace :: SBV (WordN n) -> SBV (MetricSpace (WordN n)) Source #fromMetricSpace :: SBV (MetricSpace (WordN n)) -> SBV (WordN n) Source #msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (WordN n) -> m () Source #msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (WordN n) -> m () Source # (KnownNat n, IsNonZero n) => SDivisible (SWord n) Source # SDivisible instance for SWord Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: SWord n -> SWord n -> (SWord n, SWord n) Source #sDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source #sQuot :: SWord n -> SWord n -> SWord n Source #sRem :: SWord n -> SWord n -> SWord n Source #sDiv :: SWord n -> SWord n -> SWord n Source #sMod :: SWord n -> SWord n -> SWord n Source # (KnownNat n, IsNonZero n) => SDivisible (WordN n) Source # SDivisible instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: WordN n -> WordN n -> (WordN n, WordN n) Source #sDivMod :: WordN n -> WordN n -> (WordN n, WordN n) Source #sQuot :: WordN n -> WordN n -> WordN n Source #sRem :: WordN n -> WordN n -> WordN n Source #sDiv :: WordN n -> WordN n -> WordN n Source #sMod :: WordN n -> WordN n -> WordN n Source # (KnownNat n, IsNonZero n) => SFiniteBits (WordN n) Source # SFiniteBits instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodssFiniteBitSize :: SBV (WordN n) -> Int Source #lsb :: SBV (WordN n) -> SBool Source #msb :: SBV (WordN n) -> SBool Source #blastBE :: SBV (WordN n) -> [SBool] Source #blastLE :: SBV (WordN n) -> [SBool] Source #fromBitsBE :: [SBool] -> SBV (WordN n) Source #fromBitsLE :: [SBool] -> SBV (WordN n) Source #sTestBit :: SBV (WordN n) -> Int -> SBool Source #sExtractBits :: SBV (WordN n) -> [Int] -> [SBool] Source #sPopCount :: SBV (WordN n) -> SWord8 Source #setBitTo :: SBV (WordN n) -> Int -> SBool -> SBV (WordN n) Source #fullAdder :: SBV (WordN n) -> SBV (WordN n) -> (SBool, SBV (WordN n)) Source #fullMultiplier :: SBV (WordN n) -> SBV (WordN n) -> (SBV (WordN n), SBV (WordN n)) Source # (KnownNat n, IsNonZero n) => SIntegral (WordN n) Source # SIntegral instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Source # SWord 8 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 8 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 8 Source # Source # SWord 16 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 16 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 16 Source # Source # SWord 32 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 32 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 32 Source # Source # SWord 64 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 64 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 64 Source # ByteConverter (SWord 128) Source # SWord 128 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 128 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 128 Source # ByteConverter (SWord 256) Source # SWord 256 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 256 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 256 Source # ByteConverter (SWord 512) Source # SWord 512 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 512 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 512 Source # ByteConverter (SWord 1024) Source # SWord 1024 instance for ByteConverter Instance detailsDefined in Data.SBV.Core.Sized MethodstoBytes :: SWord 1024 -> [SWord 8] Source #fromBytes :: [SWord 8] -> SWord 1024 Source # (KnownNat n, IsNonZero n) => Polynomial (SWord n) Source # Instance detailsDefined in Data.SBV.Tools.Polynomial Methodspolynomial :: [Int] -> SWord n Source #pAdd :: SWord n -> SWord n -> SWord n Source #pMult :: (SWord n, SWord n, [Int]) -> SWord n Source #pDiv :: SWord n -> SWord n -> SWord n Source #pMod :: SWord n -> SWord n -> SWord n Source #pDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source # type MetricSpace (WordN n) Source # Instance detailsDefined in Data.SBV.Core.Sized type MetricSpace (WordN n) = WordN n

### Signed bit-vectors

type SInt8 = SBV Int8 Source #

8-bit signed symbolic value, 2's complement representation

16-bit signed symbolic value, 2's complement representation

32-bit signed symbolic value, 2's complement representation

64-bit signed symbolic value, 2's complement representation

type SInt (n :: Nat) = SBV (IntN n) Source #

A symbolic signed bit-vector carrying its size info

data IntN (n :: Nat) Source #

A signed bit-vector carrying its size info

Instances
 (KnownNat n, IsNonZero n) => Bounded (IntN n) Source # Bounded instance for IntN Instance detailsDefined in Data.SBV.Core.Sized Methods (KnownNat n, IsNonZero n) => Enum (IntN n) Source # Enum instance for IntN Instance detailsDefined in Data.SBV.Core.Sized Methodssucc :: IntN n -> IntN n #pred :: IntN n -> IntN n #toEnum :: Int -> IntN n #fromEnum :: IntN n -> Int #enumFrom :: IntN n -> [IntN n] #enumFromThen :: IntN n -> IntN n -> [IntN n] #enumFromTo :: IntN n -> IntN n -> [IntN n] #enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] # Eq (IntN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methods(==) :: IntN n -> IntN n -> Bool #(/=) :: IntN n -> IntN n -> Bool # (KnownNat n, IsNonZero n) => Integral (IntN n) Source # Integral instance for IntN Instance detailsDefined in Data.SBV.Core.Sized Methodsquot :: IntN n -> IntN n -> IntN n #rem :: IntN n -> IntN n -> IntN n #div :: IntN n -> IntN n -> IntN n #mod :: IntN n -> IntN n -> IntN n #quotRem :: IntN n -> IntN n -> (IntN n, IntN n) #divMod :: IntN n -> IntN n -> (IntN n, IntN n) #toInteger :: IntN n -> Integer # (KnownNat n, IsNonZero n) => Num (IntN n) Source # Num instance for IntN Instance detailsDefined in Data.SBV.Core.Sized Methods(+) :: IntN n -> IntN n -> IntN n #(-) :: IntN n -> IntN n -> IntN n #(*) :: IntN n -> IntN n -> IntN n #negate :: IntN n -> IntN n #abs :: IntN n -> IntN n #signum :: IntN n -> IntN n # Ord (IntN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methodscompare :: IntN n -> IntN n -> Ordering #(<) :: IntN n -> IntN n -> Bool #(<=) :: IntN n -> IntN n -> Bool #(>) :: IntN n -> IntN n -> Bool #(>=) :: IntN n -> IntN n -> Bool #max :: IntN n -> IntN n -> IntN n #min :: IntN n -> IntN n -> IntN n # (KnownNat n, IsNonZero n) => Real (IntN n) Source # Real instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodstoRational :: IntN n -> Rational # Show (IntN n) Source # Show instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodsshowsPrec :: Int -> IntN n -> ShowS #show :: IntN n -> String #showList :: [IntN n] -> ShowS # (KnownNat n, IsNonZero n) => Bits (IntN n) Source # Instance detailsDefined in Data.SBV.Core.Sized Methods(.&.) :: IntN n -> IntN n -> IntN n #(.|.) :: IntN n -> IntN n -> IntN n #xor :: IntN n -> IntN n -> IntN n #complement :: IntN n -> IntN n #shift :: IntN n -> Int -> IntN n #rotate :: IntN n -> Int -> IntN n #bit :: Int -> IntN n #setBit :: IntN n -> Int -> IntN n #clearBit :: IntN n -> Int -> IntN n #complementBit :: IntN n -> Int -> IntN n #testBit :: IntN n -> Int -> Bool #bitSize :: IntN n -> Int #isSigned :: IntN n -> Bool #shiftL :: IntN n -> Int -> IntN n #unsafeShiftL :: IntN n -> Int -> IntN n #shiftR :: IntN n -> Int -> IntN n #unsafeShiftR :: IntN n -> Int -> IntN n #rotateL :: IntN n -> Int -> IntN n #rotateR :: IntN n -> Int -> IntN n #popCount :: IntN n -> Int # (KnownNat n, IsNonZero n) => HasKind (IntN n) Source # IntN has a kind Instance detailsDefined in Data.SBV.Core.Sized MethodskindOf :: IntN n -> Kind Source #hasSign :: IntN n -> Bool Source #intSizeOf :: IntN n -> Int Source #isBoolean :: IntN n -> Bool Source #isBounded :: IntN n -> Bool Source #isReal :: IntN n -> Bool Source #isFloat :: IntN n -> Bool Source #isDouble :: IntN n -> Bool Source #isChar :: IntN n -> Bool Source #isString :: IntN n -> Bool Source #isList :: IntN n -> Bool Source #isSet :: IntN n -> Bool Source #isTuple :: IntN n -> Bool Source #isMaybe :: IntN n -> Bool Source #isEither :: IntN n -> Bool Source # (KnownNat n, IsNonZero n) => SymVal (IntN n) Source # SymVal instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (IntN n)) Source #literal :: IntN n -> SBV (IntN n) Source #fromCV :: CV -> IntN n Source #isConcretely :: SBV (IntN n) -> (IntN n -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV (IntN n)) Source #forall_ :: MonadSymbolic m => m (SBV (IntN n)) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV (IntN n)] Source #exists :: MonadSymbolic m => String -> m (SBV (IntN n)) Source #exists_ :: MonadSymbolic m => m (SBV (IntN n)) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV (IntN n)] Source #free :: MonadSymbolic m => String -> m (SBV (IntN n)) Source #free_ :: MonadSymbolic m => m (SBV (IntN n)) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV (IntN n)] Source #symbolic :: MonadSymbolic m => String -> m (SBV (IntN n)) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV (IntN n)] Source #unliteral :: SBV (IntN n) -> Maybe (IntN n) Source #isConcrete :: SBV (IntN n) -> Bool Source #isSymbolic :: SBV (IntN n) -> Bool Source # (KnownNat n, IsNonZero n) => SatModel (IntN n) Source # Constructing models for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodsparseCVs :: [CV] -> Maybe (IntN n, [CV]) Source #cvtModel :: (IntN n -> Maybe b) -> Maybe (IntN n, [CV]) -> Maybe (b, [CV]) Source # (KnownNat n, IsNonZero n) => Metric (IntN n) Source # Optimizing IntN Instance detailsDefined in Data.SBV.Core.Sized Associated Typestype MetricSpace (IntN n) :: Type Source # MethodstoMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n)) Source #fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n) Source #msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (IntN n) -> m () Source #msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (IntN n) -> m () Source # (KnownNat n, IsNonZero n) => SDivisible (SInt n) Source # SDivisible instance for SInt Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: SInt n -> SInt n -> (SInt n, SInt n) Source #sDivMod :: SInt n -> SInt n -> (SInt n, SInt n) Source #sQuot :: SInt n -> SInt n -> SInt n Source #sRem :: SInt n -> SInt n -> SInt n Source #sDiv :: SInt n -> SInt n -> SInt n Source #sMod :: SInt n -> SInt n -> SInt n Source # (KnownNat n, IsNonZero n) => SDivisible (IntN n) Source # SDivisible instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: IntN n -> IntN n -> (IntN n, IntN n) Source #sDivMod :: IntN n -> IntN n -> (IntN n, IntN n) Source #sQuot :: IntN n -> IntN n -> IntN n Source #sRem :: IntN n -> IntN n -> IntN n Source #sDiv :: IntN n -> IntN n -> IntN n Source #sMod :: IntN n -> IntN n -> IntN n Source # (KnownNat n, IsNonZero n) => SFiniteBits (IntN n) Source # SFiniteBits instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodssFiniteBitSize :: SBV (IntN n) -> Int Source #lsb :: SBV (IntN n) -> SBool Source #msb :: SBV (IntN n) -> SBool Source #blastBE :: SBV (IntN n) -> [SBool] Source #blastLE :: SBV (IntN n) -> [SBool] Source #fromBitsBE :: [SBool] -> SBV (IntN n) Source #fromBitsLE :: [SBool] -> SBV (IntN n) Source #sTestBit :: SBV (IntN n) -> Int -> SBool Source #sExtractBits :: SBV (IntN n) -> [Int] -> [SBool] Source #sPopCount :: SBV (IntN n) -> SWord8 Source #setBitTo :: SBV (IntN n) -> Int -> SBool -> SBV (IntN n) Source #fullAdder :: SBV (IntN n) -> SBV (IntN n) -> (SBool, SBV (IntN n)) Source #fullMultiplier :: SBV (IntN n) -> SBV (IntN n) -> (SBV (IntN n), SBV (IntN n)) Source # (KnownNat n, IsNonZero n) => SIntegral (IntN n) Source # SIntegral instance for IntN Instance detailsDefined in Data.SBV.Core.Sized type MetricSpace (IntN n) Source # Instance detailsDefined in Data.SBV.Core.Sized type MetricSpace (IntN n) = WordN n

### Converting between fixed-size and arbitrary bitvectors

type family IsNonZero (arg :: Nat) :: Constraint where ... Source #

Type family to create the appropriate non-zero constraint

Equations

 IsNonZero 0 = TypeError ZeroWidth IsNonZero n = ()

type family FromSized (t :: Type) :: Type where ... Source #

Capture the correspondence between sized and fixed-sized BVs

Equations

 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 fixed-sized and sized BVs

Equations

 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

fromSized :: FromSizedBV a => a -> FromSized a Source #

Convert a sized bit-vector to the corresponding fixed-sized bit-vector, for instance 'SWord 16' to SWord16. See also toSized.

toSized :: ToSizedBV a => a -> ToSized a Source #

Convert a fixed-sized bit-vector to the corresponding sized bit-vector, for instance SWord16 to 'SWord 16'. See also fromSized.

## Unbounded integers

Infinite precision signed symbolic value

## Floating point numbers

IEEE-754 single-precision floating point numbers

IEEE-754 double-precision floating point numbers

## Algebraic reals

Infinite precision symbolic algebraic real value

data AlgReal Source #

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

Instances
 Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods(==) :: AlgReal -> AlgReal -> Bool #(/=) :: AlgReal -> AlgReal -> Bool # Source # NB: Following the other types we have, we require a/0 to be 0 for all a. Instance detailsDefined in Data.SBV.Core.AlgReals Methods Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods(<) :: AlgReal -> AlgReal -> Bool #(<=) :: AlgReal -> AlgReal -> Bool #(>) :: AlgReal -> AlgReal -> Bool #(>=) :: AlgReal -> AlgReal -> Bool # Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods Source # Instance detailsDefined in Data.SBV.Core.AlgReals MethodsshowList :: [AlgReal] -> ShowS # Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methodsshrink :: AlgReal -> [AlgReal] # Source # Instance detailsDefined in Data.SBV.Core.AlgReals MethodsrandomR :: RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g) #random :: RandomGen g => g -> (AlgReal, g) #randomRs :: RandomGen g => (AlgReal, AlgReal) -> g -> [AlgReal] #randoms :: RandomGen g => g -> [AlgReal] # Source # Instance detailsDefined in Data.SBV.Core.Kind Methods Source # Instance detailsDefined in Data.SBV.Core.Model MethodsisConcretely :: SBV AlgReal -> (AlgReal -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV AlgReal) Source #forall_ :: MonadSymbolic m => m (SBV AlgReal) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV AlgReal] Source #exists :: MonadSymbolic m => String -> m (SBV AlgReal) Source #exists_ :: MonadSymbolic m => m (SBV AlgReal) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV AlgReal] Source #free :: MonadSymbolic m => String -> m (SBV AlgReal) Source #free_ :: MonadSymbolic m => m (SBV AlgReal) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV AlgReal] Source #symbolic :: MonadSymbolic m => String -> m (SBV AlgReal) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV AlgReal] Source # Source # AlgReal as extracted from a model Instance detailsDefined in Data.SBV.SMT.SMT MethodsparseCVs :: [CV] -> Maybe (AlgReal, [CV]) Source #cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Data.SBV.Core.Model Associated Types MethodsmsMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV AlgReal -> m () Source #msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV AlgReal -> m () Source # Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Model

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 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV character for the time being. This limitation is due to the SMT-solvers 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/theories-UnicodeStrings.shtml

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 fixed-length 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 fixed-length 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 SBV a, with elements of type 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 except abc 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.) SFunArrays 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 using SArray will not be accepted by the C-code generator.
• You cannot use quickcheck on programs that contain these arrays. (Neither SArray nor SFunArray.)
• With SArray, SBV transfers all array-processing to the SMT-solver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. With SFunArray, 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!

Minimal complete definition

Methods

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 if-then-else choice down on to elements

Instances
 Source # Instance detailsDefined in Data.SBV.Core.Data MethodsnewArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SFunArray a b) Source #newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SFunArray a b) Source #readArray :: SFunArray a b -> SBV a -> SBV b Source #writeArray :: SymVal b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #mergeArrays :: SymVal b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source # Source # Instance detailsDefined in Data.SBV.Core.Data MethodsnewArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source #newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source #readArray :: SArray a b -> SBV a -> SBV b Source #writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source #mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source #

data SArray a b Source #

Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

• Maps directly to SMT-lib 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 code-generation (i.e., compilation to C)
• Cannot quick-check theorems using SArray values
• Typically slower as it heavily relies on SMT-solving for the array theory
Instances
 Source # Instance detailsDefined in Data.SBV.Core.Data MethodsnewArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source #newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source #readArray :: SArray a b -> SBV a -> SBV b Source #writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source #mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source # (HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) Source # Instance detailsDefined in Data.SBV.Provers.Prover MethodsforAll_ :: (SArray a b -> p) -> SymbolicT m SBool Source #forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool Source #forSome_ :: (SArray a b -> p) -> SymbolicT m SBool Source #forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool Source #prove :: (SArray a b -> p) -> m ThmResult Source #proveWith :: SMTConfig -> (SArray a b -> p) -> m ThmResult Source #sat :: (SArray a b -> p) -> m SatResult Source #satWith :: SMTConfig -> (SArray a b -> p) -> m SatResult Source #allSat :: (SArray a b -> p) -> m AllSatResult Source #allSatWith :: SMTConfig -> (SArray a b -> p) -> m AllSatResult Source #optimize :: OptimizeStyle -> (SArray a b -> p) -> m OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> m OptimizeResult Source #isVacuous :: (SArray a b -> p) -> m Bool Source #isVacuousWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #isTheorem :: (SArray a b -> p) -> m Bool Source #isTheoremWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #isSatisfiable :: (SArray a b -> p) -> m Bool Source #isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #validate :: Bool -> SMTConfig -> (SArray a b -> p) -> SMTResult -> m SMTResult Source # (HasKind a, HasKind b) => Show (SArray a b) Source # Instance detailsDefined in Data.SBV.Core.Data MethodsshowsPrec :: Int -> SArray a b -> ShowS #show :: SArray a b -> String #showList :: [SArray a b] -> ShowS # SymVal b => Mergeable (SArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #select :: (Ord b0, SymVal b0, Num b0) => [SArray a b] -> SArray a b -> SBV b0 -> SArray a b Source # EqSymbolic (SArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: SArray a b -> SArray a b -> SBool Source #(./=) :: SArray a b -> SArray a b -> SBool Source #(.===) :: SArray a b -> SArray a b -> SBool Source #(./==) :: SArray a b -> SArray a b -> SBool Source #distinct :: [SArray a b] -> SBool Source #distinctExcept :: [SArray a b] -> [SArray a b] -> SBool Source #allEqual :: [SArray a b] -> SBool Source #sElem :: SArray a b -> [SArray a b] -> SBool Source #sNotElem :: SArray a b -> [SArray a b] -> SBool Source #

data SFunArray a b Source #

Arrays implemented internally, without translating to SMT-Lib functions:

• Internally handled by the library and not mapped to SMT-Lib, 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 code-generation (i.e., compilation to C).
• Can not quick-check theorems using SFunArray values
• Typically faster as it gets compiled away during translation.
Instances
 Source # Instance detailsDefined in Data.SBV.Core.Data MethodsnewArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SFunArray a b) Source #newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SFunArray a b) Source #readArray :: SFunArray a b -> SBV a -> SBV b Source #writeArray :: SymVal b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #mergeArrays :: SymVal b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source # (HasKind a, HasKind b, MProvable m p) => MProvable m (SFunArray a b -> p) Source # Instance detailsDefined in Data.SBV.Provers.Prover MethodsforAll_ :: (SFunArray a b -> p) -> SymbolicT m SBool Source #forAll :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool Source #forSome_ :: (SFunArray a b -> p) -> SymbolicT m SBool Source #forSome :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool Source #prove :: (SFunArray a b -> p) -> m ThmResult Source #proveWith :: SMTConfig -> (SFunArray a b -> p) -> m ThmResult Source #sat :: (SFunArray a b -> p) -> m SatResult Source #satWith :: SMTConfig -> (SFunArray a b -> p) -> m SatResult Source #allSat :: (SFunArray a b -> p) -> m AllSatResult Source #allSatWith :: SMTConfig -> (SFunArray a b -> p) -> m AllSatResult Source #optimize :: OptimizeStyle -> (SFunArray a b -> p) -> m OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> (SFunArray a b -> p) -> m OptimizeResult Source #isVacuous :: (SFunArray a b -> p) -> m Bool Source #isVacuousWith :: SMTConfig -> (SFunArray a b -> p) -> m Bool Source #isTheorem :: (SFunArray a b -> p) -> m Bool Source #isTheoremWith :: SMTConfig -> (SFunArray a b -> p) -> m Bool Source #isSatisfiable :: (SFunArray a b -> p) -> m Bool Source #isSatisfiableWith :: SMTConfig -> (SFunArray a b -> p) -> m Bool Source #validate :: Bool -> SMTConfig -> (SFunArray a b -> p) -> SMTResult -> m SMTResult Source # (HasKind a, HasKind b) => Show (SFunArray a b) Source # Instance detailsDefined in Data.SBV.Core.Data MethodsshowsPrec :: Int -> SFunArray a b -> ShowS #show :: SFunArray a b -> String #showList :: [SFunArray a b] -> ShowS # SymVal b => Mergeable (SFunArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #select :: (Ord b0, SymVal b0, Num b0) => [SFunArray a b] -> SFunArray a b -> SBV b0 -> SFunArray a b Source #

# Creating symbolic values

## Single value

sBool :: MonadSymbolic m => String -> m SBool Source #

Generalization of sBool

sWord8 :: MonadSymbolic m => String -> m SWord8 Source #

Generalization of sWord8

sWord16 :: MonadSymbolic m => String -> m SWord16 Source #

Generalization of sWord16

sWord32 :: MonadSymbolic m => String -> m SWord32 Source #

Generalization of sWord32

sWord64 :: MonadSymbolic m => String -> m SWord64 Source #

Generalization of sWord64

sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SWord n) Source #

Generalization of sWord

sInt8 :: MonadSymbolic m => String -> m SInt8 Source #

Generalization of sInt8

sInt16 :: MonadSymbolic m => String -> m SInt16 Source #

Generalization of sInt16

sInt32 :: MonadSymbolic m => String -> m SInt32 Source #

Generalization of sInt32

sInt64 :: MonadSymbolic m => String -> m SInt64 Source #

Generalization of sInt64

sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SInt n) Source #

Generalization of sInt

Generalization of sInteger

sReal :: MonadSymbolic m => String -> m SReal Source #

Generalization of sReal

sFloat :: MonadSymbolic m => String -> m SFloat Source #

Generalization of sFloat

sDouble :: MonadSymbolic m => String -> m SDouble Source #

Generalization of sDouble

sChar :: MonadSymbolic m => String -> m SChar Source #

Generalization of sChar

sString :: MonadSymbolic m => String -> m SString Source #

Generalization of sString

sList :: (SymVal a, MonadSymbolic m) => String -> m (SList a) Source #

Generalization of sList

## List of values

sBools :: MonadSymbolic m => [String] -> m [SBool] Source #

Generalization of sBools

sWord8s :: MonadSymbolic m => [String] -> m [SWord8] Source #

Generalization of sWord8s

sWord16s :: MonadSymbolic m => [String] -> m [SWord16] Source #

Generalization of sWord16s

sWord32s :: MonadSymbolic m => [String] -> m [SWord32] Source #

Generalization of sWord32s

sWord64s :: MonadSymbolic m => [String] -> m [SWord64] Source #

Generalization of sWord64s

sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SWord n] Source #

Generalization of sWord64s

sInt8s :: MonadSymbolic m => [String] -> m [SInt8] Source #

Generalization of sInt8s

sInt16s :: MonadSymbolic m => [String] -> m [SInt16] Source #

Generalization of sInt16s

sInt32s :: MonadSymbolic m => [String] -> m [SInt32] Source #

Generalization of sInt32s

sInt64s :: MonadSymbolic m => [String] -> m [SInt64] Source #

Generalization of sInt64s

sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SInt n] Source #

Generalization of sInts

sIntegers :: MonadSymbolic m => [String] -> m [SInteger] Source #

Generalization of sIntegers

sReals :: MonadSymbolic m => [String] -> m [SReal] Source #

Generalization of sReals

sFloats :: MonadSymbolic m => [String] -> m [SFloat] Source #

Generalization of sFloats

sDoubles :: MonadSymbolic m => [String] -> m [SDouble] Source #

Generalization of sDoubles

sChars :: MonadSymbolic m => [String] -> m [SChar] Source #

Generalization of sChars

sStrings :: MonadSymbolic m => [String] -> m [SString] Source #

Generalization of sStrings

sLists :: (SymVal a, MonadSymbolic m) => [String] -> m [SList a] Source #

Generalization of sLists

# 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.

Minimal complete definition

(.==)

Methods

(.==) :: 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.

distinctExcept :: [a] -> [a] -> SBool Source #

Returns (symbolic) sTrue if all the elements of the given list are different. The second list contains exceptions, i.e., if an element belongs to that set, it will be considered distinct regardless of repetition.

>>> prove $\a -> distinctExcept [a, a] [0::SInteger] .<=> a .== 0 Q.E.D. >>> prove$ \a b -> distinctExcept [a, b] [0::SWord8] .<=> (a .== b .=> a .== 0)
Q.E.D.
>>> prove $\a b c d -> distinctExcept [a, b, c, d] [] .== distinct [a, b, c, (d::SInteger)] Q.E.D.  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. sNotElem :: a -> [a] -> SBool Source # Symbolic negated membership test. Instances  Source # Instance detailsDefined in Data.SBV.Core.Model Methodsdistinct :: [Bool] -> SBool Source #distinctExcept :: [Bool] -> [Bool] -> SBool Source #allEqual :: [Bool] -> SBool Source #sElem :: Bool -> [Bool] -> SBool Source #sNotElem :: Bool -> [Bool] -> SBool Source # EqSymbolic a => EqSymbolic [a] Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: [a] -> [a] -> SBool Source #(./=) :: [a] -> [a] -> SBool Source #(.===) :: [a] -> [a] -> SBool Source #(./==) :: [a] -> [a] -> SBool Source #distinct :: [[a]] -> SBool Source #distinctExcept :: [[a]] -> [[a]] -> SBool Source #allEqual :: [[a]] -> SBool Source #sElem :: [a] -> [[a]] -> SBool Source #sNotElem :: [a] -> [[a]] -> SBool Source # EqSymbolic a => EqSymbolic (Maybe a) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: Maybe a -> Maybe a -> SBool Source #(./=) :: Maybe a -> Maybe a -> SBool Source #(.===) :: Maybe a -> Maybe a -> SBool Source #(./==) :: Maybe a -> Maybe a -> SBool Source #distinct :: [Maybe a] -> SBool Source #distinctExcept :: [Maybe a] -> [Maybe a] -> SBool Source #allEqual :: [Maybe a] -> SBool Source #sElem :: Maybe a -> [Maybe a] -> SBool Source #sNotElem :: Maybe a -> [Maybe a] -> SBool Source # Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: SBV a -> SBV a -> SBool Source #(./=) :: SBV a -> SBV a -> SBool Source #(.===) :: SBV a -> SBV a -> SBool Source #(./==) :: SBV a -> SBV a -> SBool Source #distinct :: [SBV a] -> SBool Source #distinctExcept :: [SBV a] -> [SBV a] -> SBool Source #allEqual :: [SBV a] -> SBool Source #sElem :: SBV a -> [SBV a] -> SBool Source #sNotElem :: SBV a -> [SBV a] -> SBool Source # EqSymbolic a => EqSymbolic (S a) Source # Symbolic equality for S. Instance details Methods(.==) :: S a -> S a -> SBool Source #(./=) :: S a -> S a -> SBool Source #(.===) :: S a -> S a -> SBool Source #(./==) :: S a -> S a -> SBool Source #distinct :: [S a] -> SBool Source #distinctExcept :: [S a] -> [S a] -> SBool Source #allEqual :: [S a] -> SBool Source #sElem :: S a -> [S a] -> SBool Source #sNotElem :: S a -> [S a] -> SBool Source # (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: 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 #distinct :: [Either a b] -> SBool Source #distinctExcept :: [Either a b] -> [Either a b] -> SBool Source #allEqual :: [Either a b] -> SBool Source #sElem :: Either a b -> [Either a b] -> SBool Source #sNotElem :: Either a b -> [Either a b] -> SBool Source # (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (a, b) -> (a, b) -> SBool Source #(./=) :: (a, b) -> (a, b) -> SBool Source #(.===) :: (a, b) -> (a, b) -> SBool Source #(./==) :: (a, b) -> (a, b) -> SBool Source #distinct :: [(a, b)] -> SBool Source #distinctExcept :: [(a, b)] -> [(a, b)] -> SBool Source #allEqual :: [(a, b)] -> SBool Source #sElem :: (a, b) -> [(a, b)] -> SBool Source #sNotElem :: (a, b) -> [(a, b)] -> SBool Source # EqSymbolic (SArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: SArray a b -> SArray a b -> SBool Source #(./=) :: SArray a b -> SArray a b -> SBool Source #(.===) :: SArray a b -> SArray a b -> SBool Source #(./==) :: SArray a b -> SArray a b -> SBool Source #distinct :: [SArray a b] -> SBool Source #distinctExcept :: [SArray a b] -> [SArray a b] -> SBool Source #allEqual :: [SArray a b] -> SBool Source #sElem :: SArray a b -> [SArray a b] -> SBool Source #sNotElem :: SArray a b -> [SArray a b] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (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 #distinct :: [(a, b, c)] -> SBool Source #distinctExcept :: [(a, b, c)] -> [(a, b, c)] -> SBool Source #allEqual :: [(a, b, c)] -> SBool Source #sElem :: (a, b, c) -> [(a, b, c)] -> SBool Source #sNotElem :: (a, b, c) -> [(a, b, c)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (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 #distinctExcept :: [(a, b, c, d)] -> [(a, b, c, d)] -> SBool Source #allEqual :: [(a, b, c, d)] -> SBool Source #sElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source #sNotElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (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 #distinctExcept :: [(a, b, c, d, e)] -> [(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 #sNotElem :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (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 #distinctExcept :: [(a, b, c, d, e, f)] -> [(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 #sNotElem :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.==) :: (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 #distinctExcept :: [(a, b, c, d, e, f, g)] -> [(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 #sNotElem :: (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 if-then-else, for the benefit of implementing symbolic versions of max and min functions. Minimal complete definition (.<) Methods (.<) :: 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. smin :: a -> a -> a Source # Symbolic minimum. smax :: a -> a -> a Source # Symbolic maximum. inRange :: a -> (a, a) -> SBool Source # Is the value withing the allowed inclusive range? Instances  OrdSymbolic a => OrdSymbolic [a] Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: [a] -> [a] -> SBool Source #(.<=) :: [a] -> [a] -> SBool Source #(.>) :: [a] -> [a] -> SBool Source #(.>=) :: [a] -> [a] -> SBool Source #smin :: [a] -> [a] -> [a] Source #smax :: [a] -> [a] -> [a] Source #inRange :: [a] -> ([a], [a]) -> SBool Source # OrdSymbolic a => OrdSymbolic (Maybe a) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: Maybe a -> Maybe a -> SBool Source #(.<=) :: Maybe a -> Maybe a -> SBool Source #(.>) :: Maybe a -> Maybe a -> SBool Source #(.>=) :: Maybe a -> Maybe a -> SBool Source #smin :: Maybe a -> Maybe a -> Maybe a Source #smax :: Maybe a -> Maybe a -> Maybe a Source #inRange :: Maybe a -> (Maybe a, Maybe a) -> SBool Source # (Ord a, SymVal a) => OrdSymbolic (SBV a) Source # If comparison is over something SMTLib can handle, just translate it. Otherwise desugar. Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: SBV a -> SBV a -> SBool Source #(.<=) :: SBV a -> SBV a -> SBool Source #(.>) :: SBV a -> SBV a -> SBool Source #(.>=) :: SBV a -> SBV a -> SBool Source #smin :: SBV a -> SBV a -> SBV a Source #smax :: SBV a -> SBV a -> SBV a Source #inRange :: SBV a -> (SBV a, SBV a) -> SBool Source # (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: 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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (a, b) -> (a, b) -> SBool Source #(.<=) :: (a, b) -> (a, b) -> SBool Source #(.>) :: (a, b) -> (a, b) -> SBool Source #(.>=) :: (a, b) -> (a, b) -> SBool Source #smin :: (a, b) -> (a, b) -> (a, b) Source #smax :: (a, b) -> (a, b) -> (a, b) Source #inRange :: (a, b) -> ((a, b), (a, b)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (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 # Instance detailsDefined in Data.SBV.Core.Model Methods(.<) :: (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 bit-precise proofs. Methods (===) :: a -> a -> IO ThmResult infix 4 Source # Instances  (SymVal a, SymVal b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult Source # (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult Source # (SymVal a, SymVal b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult Source # (SymVal a, EqSymbolic z) => Equality (SBV a -> z) Source # Instance detailsDefined in Data.SBV.Core.Model Methods(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source # # Conditionals: Mergeable values class Mergeable a where Source # Symbolic conditionals are modeled by the Mergeable class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed. A Mergeable instance may be automatically derived for a custom data-type 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 data-type. See Status for an example and an illustration of what the instance would look like if written by hand. The function select is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way 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. Minimal complete definition Nothing Methods symbolicMerge :: Bool -> SBool -> a -> a -> a Source # Merge two values based on the condition. The first argument states whether we force the then-and-else 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 then-and-else 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  Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> () -> () -> () Source #select :: (Ord b, SymVal b, Num b) => [()] -> () -> SBV b -> () Source # Source # Instance details Methodsselect :: (Ord b, SymVal b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source # Source # Instance details Methodsselect :: (Ord b, SymVal b, Num b) => [Status] -> Status -> SBV b -> Status Source # Mergeable a => Mergeable [a] Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> [a] -> [a] -> [a] Source #select :: (Ord b, SymVal b, Num b) => [[a]] -> [a] -> SBV b -> [a] Source # Mergeable a => Mergeable (Maybe a) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> Maybe a -> Maybe a -> Maybe a Source #select :: (Ord b, SymVal b, Num b) => [Maybe a] -> Maybe a -> SBV b -> Maybe a Source # Mergeable a => Mergeable (ZipList a) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> ZipList a -> ZipList a -> ZipList a Source #select :: (Ord b, SymVal b, Num b) => [ZipList a] -> ZipList a -> SBV b -> ZipList a Source # SymVal a => Mergeable (SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a Source #select :: (Ord b, SymVal b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a Source # Mergeable a => Mergeable (S a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> S a -> S a -> S a Source #select :: (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a Source # Mergeable a => Mergeable (S a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> S a -> S a -> S a Source #select :: (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a Source # Mergeable a => Mergeable (Move a) Source # Mergeable instance for Move simply pushes the merging the data after run of each branch starting from the same state. Instance details MethodssymbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a Source #select :: (Ord b, SymVal b, Num b) => [Move a] -> Move a -> SBV b -> Move a Source # SymVal a => Mergeable (AppS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a Source #select :: (Ord b, SymVal b, Num b) => [AppS a] -> AppS a -> SBV b -> AppS a Source # Mergeable a => Mergeable (IncS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> IncS a -> IncS a -> IncS a Source #select :: (Ord b, SymVal b, Num b) => [IncS a] -> IncS a -> SBV b -> IncS a Source # Mergeable a => Mergeable (FibS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> FibS a -> FibS a -> FibS a Source #select :: (Ord b, SymVal b, Num b) => [FibS a] -> FibS a -> SBV b -> FibS a Source # Mergeable a => Mergeable (GCDS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> GCDS a -> GCDS a -> GCDS a Source #select :: (Ord b, SymVal b, Num b) => [GCDS a] -> GCDS a -> SBV b -> GCDS a Source # Mergeable a => Mergeable (DivS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> DivS a -> DivS a -> DivS a Source #select :: (Ord b, SymVal b, Num b) => [DivS a] -> DivS a -> SBV b -> DivS a Source # Mergeable a => Mergeable (SqrtS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> SqrtS a -> SqrtS a -> SqrtS a Source #select :: (Ord b, SymVal b, Num b) => [SqrtS a] -> SqrtS a -> SBV b -> SqrtS a Source # SymVal a => Mergeable (LenS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> LenS a -> LenS a -> LenS a Source #select :: (Ord b, SymVal b, Num b) => [LenS a] -> LenS a -> SBV b -> LenS a Source # Mergeable a => Mergeable (SumS a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> SumS a -> SumS a -> SumS a Source #select :: (Ord b, SymVal b, Num b) => [SumS a] -> SumS a -> SBV b -> SumS a Source # Mergeable b => Mergeable (a -> b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a -> b) -> (a -> b) -> a -> b Source #select :: (Ord b0, SymVal b0, Num b0) => [a -> b] -> (a -> b) -> SBV b0 -> a -> b Source # (Mergeable a, Mergeable b) => Mergeable (Either a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> Either a b -> Either a b -> Either a b Source #select :: (Ord b0, SymVal b0, Num b0) => [Either a b] -> Either a b -> SBV b0 -> Either a b Source # (Mergeable a, Mergeable b) => Mergeable (a, b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b) -> (a, b) -> (a, b) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b)] -> (a, b) -> SBV b0 -> (a, b) Source # (Ix a, Mergeable b) => Mergeable (Array a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> Array a b -> Array a b -> Array a b Source #select :: (Ord b0, SymVal b0, Num b0) => [Array a b] -> Array a b -> SBV b0 -> Array a b Source # SymVal b => Mergeable (SFunArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #select :: (Ord b0, SymVal b0, Num b0) => [SFunArray a b] -> SFunArray a b -> SBV b0 -> SFunArray a b Source # SymVal b => Mergeable (SArray a b) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #select :: (Ord b0, SymVal b0, Num b0) => [SArray a b] -> SArray a b -> SBV b0 -> SArray a b Source # SymVal e => Mergeable (STree i e) Source # Instance detailsDefined in Data.SBV.Tools.STree MethodssymbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e Source #select :: (Ord b, SymVal b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e Source # (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b, c) -> (a, b, c) -> (a, b, c) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b, c)] -> (a, b, c) -> SBV b0 -> (a, b, c) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b, c, d)] -> (a, b, c, d) -> SBV b0 -> (a, b, c, d) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b, c, d, e)] -> (a, b, c, d, e) -> SBV b0 -> (a, b, c, d, e) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b, c, d, e, f)] -> (a, b, c, d, e, f) -> SBV b0 -> (a, b, c, d, e, f) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) Source # Instance detailsDefined in Data.SBV.Core.Model MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #select :: (Ord b0, SymVal b0, Num b0) => [(a, b, c, d, e, f, g)] -> (a, b, c, d, e, f, g) -> SBV b0 -> (a, b, c, d, e, f, g) Source # ite :: Mergeable a => SBool -> a -> a -> a Source # If-then-else. 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 type-signatures that work for all symbolic numbers, such as SWord8, SInt8 etc. For instance, we can write a generic list-minimum 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  Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model Source # Instance detailsDefined in Data.SBV.Core.Model (KnownNat n, IsNonZero n) => SIntegral (IntN n) Source # SIntegral instance for IntN Instance detailsDefined in Data.SBV.Core.Sized (KnownNat n, IsNonZero n) => SIntegral (WordN n) Source # SIntegral instance for WordN Instance detailsDefined 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 bit-vectors. 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:  x sQuotRem 0 = (0, x) x sDivMod 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. Minimal complete definition Methods sQuotRem :: a -> a -> (a, a) Source # sDivMod :: a -> a -> (a, a) Source # sQuot :: a -> a -> a Source # sRem :: a -> a -> a Source # sDiv :: a -> a -> a Source # sMod :: a -> a -> a Source # Instances  Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Int8 -> Int8 -> (Int8, Int8) Source #sDivMod :: Int8 -> Int8 -> (Int8, Int8) Source #sQuot :: Int8 -> Int8 -> Int8 Source #sRem :: Int8 -> Int8 -> Int8 Source #sDiv :: Int8 -> Int8 -> Int8 Source #sMod :: Int8 -> Int8 -> Int8 Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Int16 -> Int16 -> (Int16, Int16) Source #sDivMod :: Int16 -> Int16 -> (Int16, Int16) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Int32 -> Int32 -> (Int32, Int32) Source #sDivMod :: Int32 -> Int32 -> (Int32, Int32) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Int64 -> Int64 -> (Int64, Int64) Source #sDivMod :: Int64 -> Int64 -> (Int64, Int64) Source # Source # Instance detailsDefined in Data.SBV.Core.Model Methods Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Word8 -> Word8 -> (Word8, Word8) Source #sDivMod :: Word8 -> Word8 -> (Word8, Word8) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Word16 -> Word16 -> (Word16, Word16) Source #sDivMod :: Word16 -> Word16 -> (Word16, Word16) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Word32 -> Word32 -> (Word32, Word32) Source #sDivMod :: Word32 -> Word32 -> (Word32, Word32) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: Word64 -> Word64 -> (Word64, Word64) Source #sDivMod :: Word64 -> Word64 -> (Word64, Word64) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: CV -> CV -> (CV, CV) Source #sDivMod :: CV -> CV -> (CV, CV) Source #sQuot :: CV -> CV -> CV Source #sRem :: CV -> CV -> CV Source #sDiv :: CV -> CV -> CV Source #sMod :: CV -> CV -> CV Source # Source # Instance detailsDefined in Data.SBV.Core.Model Methods Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64) Source #sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32) Source #sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16) Source #sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8) Source #sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # Source # Instance detailsDefined in Data.SBV.Core.Model Methods Source # Instance detailsDefined in Data.SBV.Core.Model Methods Source # Instance detailsDefined in Data.SBV.Core.Model Methods Source # Instance detailsDefined in Data.SBV.Core.Model MethodssQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8) Source #sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # (KnownNat n, IsNonZero n) => SDivisible (SInt n) Source # SDivisible instance for SInt Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: SInt n -> SInt n -> (SInt n, SInt n) Source #sDivMod :: SInt n -> SInt n -> (SInt n, SInt n) Source #sQuot :: SInt n -> SInt n -> SInt n Source #sRem :: SInt n -> SInt n -> SInt n Source #sDiv :: SInt n -> SInt n -> SInt n Source #sMod :: SInt n -> SInt n -> SInt n Source # (KnownNat n, IsNonZero n) => SDivisible (IntN n) Source # SDivisible instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: IntN n -> IntN n -> (IntN n, IntN n) Source #sDivMod :: IntN n -> IntN n -> (IntN n, IntN n) Source #sQuot :: IntN n -> IntN n -> IntN n Source #sRem :: IntN n -> IntN n -> IntN n Source #sDiv :: IntN n -> IntN n -> IntN n Source #sMod :: IntN n -> IntN n -> IntN n Source # (KnownNat n, IsNonZero n) => SDivisible (SWord n) Source # SDivisible instance for SWord Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: SWord n -> SWord n -> (SWord n, SWord n) Source #sDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source #sQuot :: SWord n -> SWord n -> SWord n Source #sRem :: SWord n -> SWord n -> SWord n Source #sDiv :: SWord n -> SWord n -> SWord n Source #sMod :: SWord n -> SWord n -> SWord n Source # (KnownNat n, IsNonZero n) => SDivisible (WordN n) Source # SDivisible instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodssQuotRem :: WordN n -> WordN n -> (WordN n, WordN n) Source #sDivMod :: WordN n -> WordN n -> (WordN n, WordN n) Source #sQuot :: WordN n -> WordN n -> WordN n Source #sRem :: WordN n -> WordN n -> WordN n Source #sDiv :: WordN n -> WordN n -> WordN n Source #sMod :: WordN n -> WordN n -> WordN n Source # # Bit-vector 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 integral-symbolic values, akin to Haskell's fromIntegral ## Shifts and rotates sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source # Generalization of shiftL, when the shift-amount is symbolic. Since Haskell's shiftL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source # Generalization of shiftR, when the shift-amount 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. sRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source # Generalization of rotateL, when the shift-amount is symbolic. Since Haskell's rotateL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity. sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source # An implementation of rotate-left, 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.


sRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Generalization of rotateR, when the shift-amount is symbolic. Since Haskell's rotateR only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #

An implementation of rotate-right, 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 shift-right 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 sign-bit, 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 bit-vector operations class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where Source # Finite bit-length 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. Minimal complete definition sFiniteBitSize Methods 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 # Big-endian blasting of a word into its bits. blastLE :: SBV a -> [SBool] Source # Little-endian blasting of a word into its bits. fromBitsBE :: [SBool] -> SBV a Source # Reconstruct from given bits, given in little-endian. fromBitsLE :: [SBool] -> SBV a Source # Reconstruct from given bits, given in little-endian. sTestBit :: SBV a -> Int -> SBool Source # Replacement for testBit, returning SBool instead of Bool. sExtractBits :: SBV a -> [Int] -> [SBool] Source # Variant of sTestBit, where we want to extract multiple bit positions. Variant of popCount, returning a symbolic value. setBitTo :: SBV a -> Int -> SBool -> SBV a Source # A combo of setBit and clearBit, when the bit to be set is symbolic. fullAdder :: SBV a -> SBV a -> (SBool, SBV a) Source # Full adder, returns carry-out from the addition. Only for unsigned quantities. fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) Source # Full multipler, returns both high and low-order bits. Only for unsigned quantities. Count leading zeros in a word, big-endian interpretation. Count trailing zeros in a word, big-endian interpretation. Instances  Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Int8 -> [SBool] Source #blastLE :: SBV Int8 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Int8 Source #fromBitsLE :: [SBool] -> SBV Int8 Source #sExtractBits :: SBV Int8 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Int16 -> [SBool] Source #blastLE :: SBV Int16 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Int16 Source #fromBitsLE :: [SBool] -> SBV Int16 Source #sExtractBits :: SBV Int16 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Int32 -> [SBool] Source #blastLE :: SBV Int32 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Int32 Source #fromBitsLE :: [SBool] -> SBV Int32 Source #sExtractBits :: SBV Int32 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Int64 -> [SBool] Source #blastLE :: SBV Int64 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Int64 Source #fromBitsLE :: [SBool] -> SBV Int64 Source #sExtractBits :: SBV Int64 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Word8 -> [SBool] Source #blastLE :: SBV Word8 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Word8 Source #fromBitsLE :: [SBool] -> SBV Word8 Source #sExtractBits :: SBV Word8 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Word16 -> [SBool] Source #blastLE :: SBV Word16 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Word16 Source #fromBitsLE :: [SBool] -> SBV Word16 Source #sExtractBits :: SBV Word16 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Word32 -> [SBool] Source #blastLE :: SBV Word32 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Word32 Source #fromBitsLE :: [SBool] -> SBV Word32 Source #sExtractBits :: SBV Word32 -> [Int] -> [SBool] Source # Source # Instance detailsDefined in Data.SBV.Core.Model MethodsblastBE :: SBV Word64 -> [SBool] Source #blastLE :: SBV Word64 -> [SBool] Source #fromBitsBE :: [SBool] -> SBV Word64 Source #fromBitsLE :: [SBool] -> SBV Word64 Source #sExtractBits :: SBV Word64 -> [Int] -> [SBool] Source # (KnownNat n, IsNonZero n) => SFiniteBits (IntN n) Source # SFiniteBits instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodssFiniteBitSize :: SBV (IntN n) -> Int Source #lsb :: SBV (IntN n) -> SBool Source #msb :: SBV (IntN n) -> SBool Source #blastBE :: SBV (IntN n) -> [SBool] Source #blastLE :: SBV (IntN n) -> [SBool] Source #fromBitsBE :: [SBool] -> SBV (IntN n) Source #fromBitsLE :: [SBool] -> SBV (IntN n) Source #sTestBit :: SBV (IntN n) -> Int -> SBool Source #sExtractBits :: SBV (IntN n) -> [Int] -> [SBool] Source #sPopCount :: SBV (IntN n) -> SWord8 Source #setBitTo :: SBV (IntN n) -> Int -> SBool -> SBV (IntN n) Source #fullAdder :: SBV (IntN n) -> SBV (IntN n) -> (SBool, SBV (IntN n)) Source #fullMultiplier :: SBV (IntN n) -> SBV (IntN n) -> (SBV (IntN n), SBV (IntN n)) Source # (KnownNat n, IsNonZero n) => SFiniteBits (WordN n) Source # SFiniteBits instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodssFiniteBitSize :: SBV (WordN n) -> Int Source #lsb :: SBV (WordN n) -> SBool Source #msb :: SBV (WordN n) -> SBool Source #blastBE :: SBV (WordN n) -> [SBool] Source #blastLE :: SBV (WordN n) -> [SBool] Source #fromBitsBE :: [SBool] -> SBV (WordN n) Source #fromBitsLE :: [SBool] -> SBV (WordN n) Source #sTestBit :: SBV (WordN n) -> Int -> SBool Source #sExtractBits :: SBV (WordN n) -> [Int] -> [SBool] Source #sPopCount :: SBV (WordN n) -> SWord8 Source #setBitTo :: SBV (WordN n) -> Int -> SBool -> SBV (WordN n) Source #fullAdder :: SBV (WordN n) -> SBV (WordN n) -> (SBool, SBV (WordN n)) Source #fullMultiplier :: SBV (WordN n) -> SBV (WordN n) -> (SBV (WordN n), SBV (WordN n)) Source # ## Splitting, joining, and extending bit-vectors Arguments  :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) => proxy i i: Start position, numbered from n-1 to 0 -> proxy j j: End position, numbered from n-1 to 0, j <= i must hold -> SBV (bv n) Input bit vector of size n -> SBV (bv ((i - j) + 1)) Output is of size i - j + 1 Extract a portion of bits to form a smaller bit-vector. >>> prove$ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
Q.E.D.


(#) infixr 5 Source #

Arguments

 :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m)) => SBV (bv n) First input, of size n, becomes the left side -> SBV (bv m) Second input, of size m, becomes the right side -> SBV (bv (n + m)) Concatenation, of size n+m

Join two bitvectors.

>>> prove $\x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71)) Q.E.D.  Arguments  :: (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 n -> SBV (bv m) Output, of size m. n < m must hold Zero extend a bit-vector. >>> prove$ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.


Arguments

 :: (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 n -> SBV (bv m) Output, of size m. n < m must hold

Sign extend a bit-vector.

>>> 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.


Arguments

 :: (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, IsNonZero (n - i)) => proxy i i: Number of bits to drop. i < n must hold. -> SBV (bv n) Input, of size n -> SBV (bv m) Output, of size m. m = n - i holds.

Drop bits from the top of a bit-vector.

>>> 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.


Arguments

 :: (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n) => proxy i i: Number of bits to take. 0 < i <= n must hold. -> SBV (bv n) Input, of size n -> SBV (bv i) Output, of size i

Take bits from the top of a bit-vector.

>>> 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. # IEEE-floating point numbers class (SymVal a, RealFloat a) => IEEEFloating a where Source # A class of floating-point (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. Minimal complete definition Nothing Methods 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 floating-point, 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 # Fused-multiply-add 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 square-root 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. 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 .==.) Is the floating-point number a normal value. (i.e., not denormalized.) Is the floating-point number a subnormal value. (Also known as denormal.) fpIsZero :: SBV a -> SBool Source # Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.) Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.) fpIsNaN :: SBV a -> SBool Source # Is the floating-point number a NaN value? Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not. Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not. Is the floating point number -0? Is the floating point number +0? fpIsPoint :: SBV a -> SBool Source # Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed. Instances  Source # SDouble instance Instance detailsDefined in Data.SBV.Core.Floating Methods Source # SFloat instance Instance detailsDefined in Data.SBV.Core.Floating Methods Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell. Constructors  RoundNearestTiesToEven Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.) RoundNearestTiesToAway Round to nearest representable floating point value. If precisely at half-way, 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 rounding-up or ceiling.) RoundTowardNegative Round towards negative infinity. (Also known as rounding-down or floor.) RoundTowardZero Round towards zero. (Also known as truncation.) Instances  Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RoundingMode #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RoundingMode) #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RoundingMode) #gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode # Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # Instance detailsDefined in Data.SBV.Core.Symbolic MethodsshowList :: [RoundingMode] -> ShowS # Source # RoundingMode kind Instance detailsDefined in Data.SBV.Core.Symbolic Methods Source # RoundingMode can be used symbolically Instance detailsDefined in Data.SBV.Core.Data Methodsforall :: MonadSymbolic m => String -> m (SBV RoundingMode) Source #forall_ :: MonadSymbolic m => m (SBV RoundingMode) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV RoundingMode] Source #exists :: MonadSymbolic m => String -> m (SBV RoundingMode) Source #exists_ :: MonadSymbolic m => m (SBV RoundingMode) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV RoundingMode] Source #free :: MonadSymbolic m => String -> m (SBV RoundingMode) Source #free_ :: MonadSymbolic m => m (SBV RoundingMode) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV RoundingMode] Source #symbolic :: MonadSymbolic m => String -> m (SBV RoundingMode) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV RoundingMode] Source # Source # A rounding mode, extracted from a model. (Default definition suffices) Instance detailsDefined in Data.SBV.SMT.SMT MethodsparseCVs :: [CV] -> Maybe (RoundingMode, [CV]) Source #cvtModel :: (RoundingMode -> Maybe b) -> Maybe (RoundingMode, [CV]) -> Maybe (b, [CV]) Source # The symbolic variant of RoundingMode nan :: Floating a => a Source # Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here. infinity :: Floating a => a Source # Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here. sNaN :: (Floating a, SymVal a) => SBV a Source # Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat. sInfinity :: (Floating a, SymVal a) => SBV a Source # Symbolic variant of infinity. This value will inhabit both SDouble and SFloat. ## Rounding modes Symbolic variant of RoundNearestTiesToEven Symbolic variant of RoundNearestTiesToAway Symbolic variant of RoundTowardPositive Symbolic variant of RoundTowardNegative Symbolic variant of RoundTowardZero Alias for sRoundNearestTiesToEven Alias for sRoundNearestTiesToAway Alias for sRoundTowardPositive Alias for sRoundTowardNegative 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 SMT-Lib, or the C-translation. If the input value is out-of-bounds 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. Minimal complete definition Nothing Methods Convert from an IEEE74 single precision float. Convert to an IEEE-754 Single-precision 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. Counter-example:
s0 = RoundNearestTiesToEven :: RoundingMode
s1 =             -264306721 :: Int32


Note how we get a failure on Int32. The counter-example value is not representable exactly as a single precision float:

>>> toRational (-264306721 :: Float)
(-264306720) % 1


Note how the numerator is different, it is off by 1. 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 IEEE-754 Single-precision 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. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = -264306721 :: Int32  Note how we get a failure on Int32. The counter-example value is not representable exactly as a single precision float: >>> toRational (-264306721 :: Float) (-264306720) % 1  Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable. Convert from an IEEE74 double precision float. Convert to an IEEE-754 Double-precision 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. Counter-example:
s0 =  RoundTowardNegative :: RoundingMode
s1 = -8069753317450726624 :: Int64


Just like in the SFloat case, once we reach 64-bits, we no longer can exactly represent the integer value for all possible values:

>>> toRational ( -8069753317450726624 :: Double)
(-8069753317450726400) % 1


In this case the numerator is off by 224!

toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble Source #

Convert to an IEEE-754 Double-precision 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. Counter-example:
s0 =  RoundTowardNegative :: RoundingMode
s1 = -8069753317450726624 :: Int64


Just like in the SFloat case, once we reach 64-bits, we no longer can exactly represent the integer value for all possible values:

>>> toRational ( -8069753317450726624 :: Double)
(-8069753317450726400) % 1


In this case the numerator is off by 224!

Instances
 Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods Source # Instance detailsDefined in Data.SBV.Core.Floating Methods

## Bit-pattern conversions

Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the representation for NaNs 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 bit-representation 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 code-generation mode, we simply map it to a simple conversion.

Reinterpret the bits in a 32-bit word as a single-precision floating point number

Convert an SDouble to an SWord64, preserving the bit-correspondence. Note that since the representation for NaNs 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.

Reinterpret the bits in a 32-bit word as a single-precision floating point number

blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) Source #

Extract the sign/exponent/mantissa of a single-precision 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 single-precision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.

# Enumerations

Make an enumeration a symbolic type.

# Uninterpreted sorts, axioms, 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 uninterpreted-functions as a general means of black-box'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 end-users should not need to define their own instances.

Minimal complete definition

sbvUninterpret

Methods

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 code-generation. For execution and verification the value is used as is. For code-generation, 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 end-user-code, but is rather useful for the library development.

Instances
 HasKind a => Uninterpreted (SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model MethodscgUninterpret :: String -> [String] -> SBV a -> SBV a Source #sbvUninterpret :: Maybe ([String], SBV a) -> String -> SBV a Source # (SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a Source # (SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a Source # (SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # (SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # (SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # (SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # (SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # (SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # (SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # Instance detailsDefined in Data.SBV.Core.Model Methodsuninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #