sbv-8.17: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: SMT Based Verification

Express properties about Haskell programs and automatically prove them using SMT solvers.

>>> prove $\x -> x shiftL 2 .== 4 * (x :: SWord8) Q.E.D.  >>> prove$ \x -> x shiftL 2 .== 2 * (x :: SWord8)
Falsifiable. Counter-example:
s0 = 64 :: Word8


The function prove has the following type:

    prove :: Provable a => a -> IO ThmResult


The class Provable comes with instances for n-ary predicates, for arbitrary n. The predicates are just regular Haskell functions over symbolic types listed below. Functions for checking satisfiability (sat and allSat) are also provided.

The sbv library introduces the following symbolic types:

• SBool: Symbolic Booleans (bits).
• SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned).
• SInt8, SInt16, SInt32, SInt64: Symbolic Ints (signed).
• SWord n: Generalized symbolic words of arbitrary bit-size.
• SInt n: Generalized symbolic ints of arbitrary bit-size.
• SInteger: Unbounded signed integers.
• SReal: Algebraic-real numbers.
• SFloat: IEEE-754 single-precision floating point values.
• SDouble: IEEE-754 double-precision floating point values.
• SRational: Rationals. (Ratio of two symbolic integers.)
• SFloatingPoint: Generalized IEEE-754 floating point values, with user specified exponent and mantissa widths.
• SChar, SString, RegExp: Characters, strings and regular expressions.
• SList: Symbolic lists (which can be nested)
• STuple, STuple2, STuple3, .., STuple8 : Symbolic tuples (upto 8-tuples, can be nested)
• SEither: Symbolic sums
• SMaybe: Symbolic optional values.
• SSet: Symbolic sets.
• SArray: Arrays of symbolic values.
• Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
• Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
• Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
• Model validation: SBV can validate models returned by solvers, which allows for protection against bugs in SMT solvers and SBV itself. (See the validateModel parameter.)

The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the standard classes Num, Bits, custom versions of Eq (EqSymbolic) and Ord (OrdSymbolic), along with several other custom classes for simplifying programming with symbolic values. The framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return SBool) built out of these types can also be:

• proven correct via an external SMT solver (the prove function)
• checked for satisfiability (the sat, allSat functions)
• used in synthesis (the sat function with existentials)
• quick-checked

If a predicate is not valid, prove will return a counterexample: An assignment to inputs such that the predicate fails. The sat function will return a satisfying assignment, if there is one. The allSat function returns all satisfying assignments.

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://smtlib.cs.uiowa.edu/

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the following SMT-Solvers out-of-the box:

SBV requires recent versions of these solvers; please see the file SMTSolverVersions.md in the source distribution for specifics.

SBV also allows calling these solvers in parallel, either getting results from multiple solvers or returning the fastest one. (See proveWithAll, proveWithAny, etc.)

Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.

Synopsis

# Documentation

The SBV library is really two things:

• A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
• A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a seamless experience, i.e., let people program in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the Num and Bits classes simplify coding), it makes life harder in others. For instance, if-then-else only takes Bool as a test in Haskell, and comparisons (> etc.) only return Bools. Clearly we would like these values to be symbolic (i.e., SBool), thus stopping us from using some native Haskell constructs. When symbolic versions of operators are needed, they are typically obtained by prepending a dot, for instance == becomes .==. Care has been taken to make the transition painless. In particular, any Haskell program you build out of symbolic components is fully concretely executable within Haskell, without the need for any custom interpreters. (They are truly Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated feel of the system, one of the original design goals for SBV.

Incremental query mode: SBV provides a wide variety of ways to utilize SMT-solvers, without requiring the user to deal with the solvers themselves. While this mode is convenient, advanced users might need access to the underlying solver at a lower level. For such use cases, SBV allows users to have an interactive session: The user can issue commands to the solver, inspect the values/results, and formulate new constraints. This advanced feature is available through the Data.SBV.Control module, where most SMTLib features are made available via a typed-API.

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

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

Instances details
 (KnownNat n, BVIsNonZero n) => Bounded (WordN n) Source # Bounded instance for WordN Instance detailsDefined in Data.SBV.Core.Sized Methods (KnownNat n, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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 #isFP :: 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, BVIsNonZero n) => SymVal (WordN n) Source # SymVal instance for WordN Instance detailsDefined in Data.SBV.Core.Sized MethodsmkSymVal :: MonadSymbolic m => VarContext -> 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, BVIsNonZero 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, BVIsNonZero n) => Metric (WordN n) Source # Optimizing WordN Instance detailsDefined in Data.SBV.Core.Sized Associated Typestype MetricSpace (WordN n) 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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 # (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods(+!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n) Source #(-!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n) Source #(*!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n) Source #(/!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n) Source #negateChecked :: SBV (WordN n) -> SBV (WordN n) Source # (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: SWord n -> SWord n -> (SBool, SBool) Source #bvSubO :: SWord n -> SWord n -> (SBool, SBool) Source #bvMulO :: SWord n -> SWord n -> (SBool, SBool) Source #bvMulOFast :: SWord n -> SWord n -> (SBool, SBool) Source #bvDivO :: SWord n -> SWord n -> (SBool, SBool) Source #bvNegO :: SWord n -> (SBool, SBool) 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

Instances details
 (KnownNat n, BVIsNonZero n) => Bounded (IntN n) Source # Bounded instance for IntN Instance detailsDefined in Data.SBV.Core.Sized Methods (KnownNat n, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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 #isFP :: 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, BVIsNonZero n) => SymVal (IntN n) Source # SymVal instance for IntN Instance detailsDefined in Data.SBV.Core.Sized MethodsmkSymVal :: MonadSymbolic m => VarContext -> 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, BVIsNonZero 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, BVIsNonZero n) => Metric (IntN n) Source # Optimizing IntN Instance detailsDefined in Data.SBV.Core.Sized Associated Typestype MetricSpace (IntN n) 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero n) => SIntegral (IntN n) Source # SIntegral instance for IntN Instance detailsDefined in Data.SBV.Core.Sized (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods(+!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n) Source #(-!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n) Source #(*!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n) Source #(/!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n) Source #negateChecked :: SBV (IntN n) -> SBV (IntN n) Source # (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: SInt n -> SInt n -> (SBool, SBool) Source #bvSubO :: SInt n -> SInt n -> (SBool, SBool) Source #bvMulO :: SInt n -> SInt n -> (SBool, SBool) Source #bvMulOFast :: SInt n -> SInt n -> (SBool, SBool) Source #bvDivO :: SInt n -> SInt n -> (SBool, SBool) Source #bvNegO :: SInt n -> (SBool, SBool) Source # 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 BVIsNonZero (arg :: Nat) :: Constraint where ... Source #

Type family to create the appropriate non-zero constraint

Equations

 BVIsNonZero 0 = TypeError BVZeroWidth BVIsNonZero _ = ()

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

The SBV library supports unbounded signed integers with the type SInteger, which are not subject to overflow/underflow as it is the case with the bounded types, such as SWord8, SInt16, etc. However, some bit-vector based operations are not supported for the SInteger type while in the verification mode. That is, you can use these operations on SInteger values during normal programming/simulation. but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are:

• Rotations and shifts: rotateL, rotateR, shiftL, shiftR
• Bitwise logical ops: .&., .|., xor, complement
• Extraction and concatenation: bvExtract, #, zeroExtend, signExtend, bvDrop, and bvTake

Usual arithmetic (+, -, *, sQuotRem, sQuot, sRem, sDivMod, sDiv, sMod) and logical operations (.<, .<=, .>, .>=, .==, ./=) operations are supported for SInteger fully, both in programming and verification modes.

Infinite precision signed symbolic value

## Floating point numbers

Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's Float and Double types. For SMT support with floating-point numbers, see the paper by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.

type family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where ... Source #

A valid float has restrictions on eb/sb values. NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing. Filed this as a bug report for CPPHS at https://github.com/malcolmwallace/cpphs/issues/25.

Equations

 ValidFloat (eb :: Nat) (sb :: Nat) = (KnownNat eb, KnownNat sb, If ((((eb CmpNat 2) == 'EQ) || ((eb CmpNat 2) == 'GT)) && ((((eb CmpNat 61) == 'EQ) || ((eb CmpNat 61) == 'LT)) && ((((sb CmpNat 2) == 'EQ) || ((sb CmpNat 2) == 'GT)) && (((sb CmpNat 4611686018427387902) == 'EQ) || ((sb CmpNat 4611686018427387902) == 'LT))))) (() :: Constraint) (TypeError (InvalidFloat eb sb)))

IEEE-754 single-precision floating point numbers

IEEE-754 double-precision floating point numbers

type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) Source #

A symbolic arbitrary precision floating point value

data FloatingPoint (eb :: Nat) (sb :: Nat) Source #

A floating point value, indexed by its exponent and significand sizes.

An IEEE SP is FloatingPoint 8 24 DP is FloatingPoint 11 53 etc.

#### Instances

Instances details
 Eq (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.SizedFloats Methods(==) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool #(/=) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool # ValidFloat eb sb => Floating (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.SizedFloats Methodspi :: FloatingPoint eb sb #exp :: FloatingPoint eb sb -> FloatingPoint eb sb #log :: FloatingPoint eb sb -> FloatingPoint eb sb #sqrt :: FloatingPoint eb sb -> FloatingPoint eb sb #(**) :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #logBase :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #sin :: FloatingPoint eb sb -> FloatingPoint eb sb #cos :: FloatingPoint eb sb -> FloatingPoint eb sb #tan :: FloatingPoint eb sb -> FloatingPoint eb sb #asin :: FloatingPoint eb sb -> FloatingPoint eb sb #acos :: FloatingPoint eb sb -> FloatingPoint eb sb #atan :: FloatingPoint eb sb -> FloatingPoint eb sb #sinh :: FloatingPoint eb sb -> FloatingPoint eb sb #cosh :: FloatingPoint eb sb -> FloatingPoint eb sb #tanh :: FloatingPoint eb sb -> FloatingPoint eb sb #asinh :: FloatingPoint eb sb -> FloatingPoint eb sb #acosh :: FloatingPoint eb sb -> FloatingPoint eb sb #atanh :: FloatingPoint eb sb -> FloatingPoint eb sb #log1p :: FloatingPoint eb sb -> FloatingPoint eb sb #expm1 :: FloatingPoint eb sb -> FloatingPoint eb sb #log1pexp :: FloatingPoint eb sb -> FloatingPoint eb sb #log1mexp :: FloatingPoint eb sb -> FloatingPoint eb sb # ValidFloat eb sb => Floating (SFloatingPoint eb sb) Source # We give a specific instance for SFloatingPoint, because the underlying floating-point type doesn't support fromRational directly. The overlap with the above instance is unfortunate. Instance detailsDefined in Data.SBV.Core.Model Methodspi :: SFloatingPoint eb sb #exp :: SFloatingPoint eb sb -> SFloatingPoint eb sb #log :: SFloatingPoint eb sb -> SFloatingPoint eb sb #sqrt :: SFloatingPoint eb sb -> SFloatingPoint eb sb #(**) :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb #logBase :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb #sin :: SFloatingPoint eb sb -> SFloatingPoint eb sb #cos :: SFloatingPoint eb sb -> SFloatingPoint eb sb #tan :: SFloatingPoint eb sb -> SFloatingPoint eb sb #asin :: SFloatingPoint eb sb -> SFloatingPoint eb sb #acos :: SFloatingPoint eb sb -> SFloatingPoint eb sb #atan :: SFloatingPoint eb sb -> SFloatingPoint eb sb #sinh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #cosh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #tanh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #asinh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #acosh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #atanh :: SFloatingPoint eb sb -> SFloatingPoint eb sb #log1p :: SFloatingPoint eb sb -> SFloatingPoint eb sb #expm1 :: SFloatingPoint eb sb -> SFloatingPoint eb sb #log1pexp :: SFloatingPoint eb sb -> SFloatingPoint eb sb #log1mexp :: SFloatingPoint eb sb -> SFloatingPoint eb sb # ValidFloat eb sb => Fractional (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.SizedFloats Methods(/) :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #recip :: FloatingPoint eb sb -> FloatingPoint eb sb #fromRational :: Rational -> FloatingPoint eb sb # ValidFloat eb sb => Num (FloatingPoint eb sb) Source # Num instance for FloatingPoint Instance detailsDefined in Data.SBV.Core.SizedFloats Methods(+) :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #(-) :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #(*) :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #negate :: FloatingPoint eb sb -> FloatingPoint eb sb #abs :: FloatingPoint eb sb -> FloatingPoint eb sb #signum :: FloatingPoint eb sb -> FloatingPoint eb sb #fromInteger :: Integer -> FloatingPoint eb sb # Ord (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.SizedFloats Methodscompare :: FloatingPoint eb sb -> FloatingPoint eb sb -> Ordering #(<) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool #(<=) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool #(>) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool #(>=) :: FloatingPoint eb sb -> FloatingPoint eb sb -> Bool #max :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb #min :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb # ValidFloat eb sb => Real (FloatingPoint eb sb) Source # Real instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. Instance detailsDefined in Data.SBV.Core.Floating MethodstoRational :: FloatingPoint eb sb -> Rational # ValidFloat eb sb => RealFloat (FloatingPoint eb sb) Source # RealFloat instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. Instance detailsDefined in Data.SBV.Core.Floating MethodsfloatRadix :: FloatingPoint eb sb -> Integer #floatDigits :: FloatingPoint eb sb -> Int #floatRange :: FloatingPoint eb sb -> (Int, Int) #decodeFloat :: FloatingPoint eb sb -> (Integer, Int) #encodeFloat :: Integer -> Int -> FloatingPoint eb sb #exponent :: FloatingPoint eb sb -> Int #significand :: FloatingPoint eb sb -> FloatingPoint eb sb #scaleFloat :: Int -> FloatingPoint eb sb -> FloatingPoint eb sb #isNaN :: FloatingPoint eb sb -> Bool #isInfinite :: FloatingPoint eb sb -> Bool #isDenormalized :: FloatingPoint eb sb -> Bool #isNegativeZero :: FloatingPoint eb sb -> Bool #isIEEE :: FloatingPoint eb sb -> Bool #atan2 :: FloatingPoint eb sb -> FloatingPoint eb sb -> FloatingPoint eb sb # ValidFloat eb sb => RealFrac (FloatingPoint eb sb) Source # RealFrac instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. Instance detailsDefined in Data.SBV.Core.Floating MethodsproperFraction :: Integral b => FloatingPoint eb sb -> (b, FloatingPoint eb sb) #truncate :: Integral b => FloatingPoint eb sb -> b #round :: Integral b => FloatingPoint eb sb -> b #ceiling :: Integral b => FloatingPoint eb sb -> b #floor :: Integral b => FloatingPoint eb sb -> b # Show (FloatingPoint eb sb) Source # Show instance for Floats. By default we print in base 10, with standard scientific notation. Instance detailsDefined in Data.SBV.Core.SizedFloats MethodsshowsPrec :: Int -> FloatingPoint eb sb -> ShowS #show :: FloatingPoint eb sb -> String #showList :: [FloatingPoint eb sb] -> ShowS # ValidFloat eb sb => HasKind (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Model MethodskindOf :: FloatingPoint eb sb -> Kind Source #hasSign :: FloatingPoint eb sb -> Bool Source #intSizeOf :: FloatingPoint eb sb -> Int Source #isBoolean :: FloatingPoint eb sb -> Bool Source #isBounded :: FloatingPoint eb sb -> Bool Source #isReal :: FloatingPoint eb sb -> Bool Source #isFloat :: FloatingPoint eb sb -> Bool Source #isDouble :: FloatingPoint eb sb -> Bool Source #isRational :: FloatingPoint eb sb -> Bool Source #isFP :: FloatingPoint eb sb -> Bool Source #isUnbounded :: FloatingPoint eb sb -> Bool Source #isUserSort :: FloatingPoint eb sb -> Bool Source #isChar :: FloatingPoint eb sb -> Bool Source #isString :: FloatingPoint eb sb -> Bool Source #isList :: FloatingPoint eb sb -> Bool Source #isSet :: FloatingPoint eb sb -> Bool Source #isTuple :: FloatingPoint eb sb -> Bool Source #isMaybe :: FloatingPoint eb sb -> Bool Source #isEither :: FloatingPoint eb sb -> Bool Source #showType :: FloatingPoint eb sb -> String Source # ValidFloat eb sb => SymVal (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Model MethodsmkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (FloatingPoint eb sb)) Source #literal :: FloatingPoint eb sb -> SBV (FloatingPoint eb sb) Source #fromCV :: CV -> FloatingPoint eb sb Source #isConcretely :: SBV (FloatingPoint eb sb) -> (FloatingPoint eb sb -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV (FloatingPoint eb sb)) Source #forall_ :: MonadSymbolic m => m (SBV (FloatingPoint eb sb)) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV (FloatingPoint eb sb)] Source #exists :: MonadSymbolic m => String -> m (SBV (FloatingPoint eb sb)) Source #exists_ :: MonadSymbolic m => m (SBV (FloatingPoint eb sb)) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV (FloatingPoint eb sb)] Source #free :: MonadSymbolic m => String -> m (SBV (FloatingPoint eb sb)) Source #free_ :: MonadSymbolic m => m (SBV (FloatingPoint eb sb)) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV (FloatingPoint eb sb)] Source #symbolic :: MonadSymbolic m => String -> m (SBV (FloatingPoint eb sb)) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV (FloatingPoint eb sb)] Source #unliteral :: SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb) Source #isConcrete :: SBV (FloatingPoint eb sb) -> Bool Source #isSymbolic :: SBV (FloatingPoint eb sb) -> Bool Source # (KnownNat eb, KnownNat sb) => SatModel (FloatingPoint eb sb) Source # A general floating-point extracted from a model Instance detailsDefined in Data.SBV.SMT.SMT MethodsparseCVs :: [CV] -> Maybe (FloatingPoint eb sb, [CV]) Source #cvtModel :: (FloatingPoint eb sb -> Maybe b) -> Maybe (FloatingPoint eb sb, [CV]) -> Maybe (b, [CV]) Source # (BVIsNonZero (eb + sb), KnownNat (eb + sb), ValidFloat eb sb) => Metric (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Floating Associated Typestype MetricSpace (FloatingPoint eb sb) Source # MethodstoMetricSpace :: SBV (FloatingPoint eb sb) -> SBV (MetricSpace (FloatingPoint eb sb)) Source #fromMetricSpace :: SBV (MetricSpace (FloatingPoint eb sb)) -> SBV (FloatingPoint eb sb) Source #msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (FloatingPoint eb sb) -> m () Source #msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (FloatingPoint eb sb) -> m () Source # ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Floating MethodsfromSFloat :: SRoundingMode -> SFloat -> SBV (FloatingPoint eb sb) Source #toSFloat :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloat Source #toSDouble :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SDouble Source #fromSFloatingPoint :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFloat eb0 sb0 => SRoundingMode -> SFloatingPoint eb0 sb0 -> SBV (FloatingPoint eb sb) Source #toSFloatingPoint :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFloat eb0 sb0 => SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb0 sb0 Source # ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Floating MethodsfpAbs :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpNeg :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpAdd :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpSub :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpMul :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpDiv :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpFMA :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpSqrt :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpRem :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpRoundToIntegral :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpMin :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpMax :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source #fpIsEqualObject :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool Source #fpIsNormal :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsSubnormal :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsZero :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsInfinite :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsNaN :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsNegative :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsPositive :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsNegativeZero :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsPositiveZero :: SBV (FloatingPoint eb sb) -> SBool Source #fpIsPoint :: SBV (FloatingPoint eb sb) -> SBool Source # type MetricSpace (FloatingPoint eb sb) Source # Instance detailsDefined in Data.SBV.Core.Floating type MetricSpace (FloatingPoint eb sb) = WordN (eb + sb)

A symbolic half-precision float

type FPHalf = FloatingPoint 5 11 Source #

Abbreviation for IEEE half precision float, bit width 16 = 5 + 11.

A symbolic brain-float precision float

type FPBFloat = FloatingPoint 8 8 Source #

Abbreviation for brain-float precision float, bit width 16 = 8 + 8.

A symbolic single-precision float

type FPSingle = FloatingPoint 8 24 Source #

Abbreviation for IEEE single precision float, bit width 32 = 8 + 24.

A symbolic double-precision float

type FPDouble = FloatingPoint 11 53 Source #

Abbreviation for IEEE double precision float, bit width 64 = 11 + 53.

A symbolic quad-precision float

type FPQuad = FloatingPoint 15 113 Source #

Abbreviation for IEEE quadruble precision float, bit width 128 = 15 + 113.

## Rationals

A symbolic rational value.

## Algebraic reals

Algebraic reals are roots of single-variable polynomials with rational coefficients. (See http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite precision numbers, but they do not cover all real numbers. (In particular, they cannot represent transcendentals.) Some irrational numbers are algebraic (such as sqrt 2), while others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://smtlib.cs.uiowa.edu/theories-Reals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)

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

Constructors

 AlgRational Bool Rational bool says it's exact (i.e., SMT-solver did not return it with ? at the end.) AlgPolyRoot (Integer, AlgRealPoly) (Maybe String) which root of this polynomial and an approximate decimal representation with given precision, if available AlgInterval (RealPoint Rational) (RealPoint Rational) interval, with low and high bounds

#### Instances

Instances details
 Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods(==) :: AlgReal -> AlgReal -> Bool #(/=) :: AlgReal -> AlgReal -> Bool # Source # SReal Floating instance, used in conjunction with the dReal solver for delta-satisfiability. Note that we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing them for arbitrary rationals. Instance detailsDefined in Data.SBV.Core.Model Methodspi :: SReal #exp :: SReal -> SReal #log :: SReal -> SReal #sqrt :: SReal -> SReal #(**) :: SReal -> SReal -> SReal #logBase :: SReal -> SReal -> SReal #sin :: SReal -> SReal #cos :: SReal -> SReal #tan :: SReal -> SReal #asin :: SReal -> SReal #acos :: SReal -> SReal #atan :: SReal -> SReal #sinh :: SReal -> SReal #cosh :: SReal -> SReal #tanh :: SReal -> SReal #asinh :: SReal -> SReal #acosh :: SReal -> SReal #atanh :: SReal -> SReal #log1p :: SReal -> SReal #expm1 :: SReal -> SReal # 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 MethodsmkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV AlgReal) Source #isConcretely :: 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 MethodsfromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV AlgReal Source #toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb Source # 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.

Convert an AlgReal to a Rational. If the AlgReal is exact, then you get a Left value. Otherwise, you get a Right value which is simply an approximation.

data RealPoint a Source #

Is the endpoint included in the interval?

Constructors

 OpenPoint a open: i.e., doesn't include the point ClosedPoint a closed: i.e., includes the point

#### Instances

Instances details
 Eq a => Eq (RealPoint a) Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methods(==) :: RealPoint a -> RealPoint a -> Bool #(/=) :: RealPoint a -> RealPoint a -> Bool # Ord a => Ord (RealPoint a) Source # Instance detailsDefined in Data.SBV.Core.AlgReals Methodscompare :: RealPoint a -> RealPoint a -> Ordering #(<) :: RealPoint a -> RealPoint a -> Bool #(<=) :: RealPoint a -> RealPoint a -> Bool #(>) :: RealPoint a -> RealPoint a -> Bool #(>=) :: RealPoint a -> RealPoint a -> Bool #max :: RealPoint a -> RealPoint a -> RealPoint a #min :: RealPoint a -> RealPoint a -> RealPoint a # Show a => Show (RealPoint a) Source # Instance detailsDefined in Data.SBV.Core.AlgReals MethodsshowsPrec :: Int -> RealPoint a -> ShowS #show :: RealPoint a -> String #showList :: [RealPoint a] -> ShowS #

realPoint :: RealPoint a -> a Source #

Extract the point associated with the open-closed point

Conversion from internal rationals to Haskell values

Constructors

 RatIrreducible AlgReal Root of a polynomial, cannot be reduced RatExact Rational An exact rational RatApprox Rational An approximated value RatInterval (RealPoint Rational) (RealPoint Rational) Interval. Can be open/closed on both ends.

#### Instances

Instances details
 Source # Instance detailsDefined in Data.SBV.Core.AlgReals MethodsshowList :: [RationalCV] -> ShowS #

## Characters, Strings and Regular Expressions

Support for characters, strings, and regular expressions (initial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml and here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for related functions.

type SChar = SBV Char Source #

A symbolic character. Note that this is the full unicode character set. see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml for details.

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

Support for symbolic lists (initial version contributed by Joel Burget) adds support for sequence support, described here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.List for related functions.

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.

## Tuples

Tuples can be used as symbolic values. This is useful in combination with lists, for example SBV [(Integer, String)] is a valid type. These types can be arbitrarily nested, eg SBV [(Integer, [(Char, (Integer, String))])]. Instances of upto 8-tuples are provided.

class SymTuple a Source #

Identify tuple like things. Note that there are no methods, just instances to control type inference

#### Instances

Instances details
 SymTuple () Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c, d) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c, d, e) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c, d, e, f) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c, d, e, f, g) Source # Instance detailsDefined in Data.SBV.Core.Model SymTuple (a, b, c, d, e, f, g, h) Source # Instance detailsDefined in Data.SBV.Core.Model

type STuple a b = SBV (a, b) Source #

Symbolic 2-tuple. NB. STuple and STuple2 are equivalent.

type STuple2 a b = SBV (a, b) Source #

Symbolic 2-tuple. NB. STuple and STuple2 are equivalent.

type STuple3 a b c = SBV (a, b, c) Source #

Symbolic 3-tuple.

type STuple4 a b c d = SBV (a, b, c, d) Source #

Symbolic 4-tuple.

type STuple5 a b c d e = SBV (a, b, c, d, e) Source #

Symbolic 5-tuple.

type STuple6 a b c d e f = SBV (a, b, c, d, e, f) Source #

Symbolic 6-tuple.

type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g) Source #

Symbolic 7-tuple.

type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h) Source #

Symbolic 8-tuple.

## Sum types

type SMaybe a = SBV (Maybe a) Source #

Symbolic Maybe

type SEither a b = SBV (Either a b) Source #

Symbolic Either

## Sets

data RCSet a Source #

A RCSet is either a regular set or a set given by its complement from the corresponding universal set.

Constructors

 RegularSet (Set a) ComplementSet (Set a)

#### Instances

Instances details

type SSet a = SBV (RCSet a) Source #

Symbolic Set. Note that we use RCSet, which supports both regular sets and complements, i.e., those obtained from the universal set (of the right type) by removing elements.

# Arrays of symbolic values

class SymArray array where Source #

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.

The reason for this class is rather historic. In the past, SBV provided two different kinds of arrays: an SArray abstraction that mapped directly to SMTLib arrays (which is still available today), and a functional notion of arrays that used internal caching, called SFunArray. The latter has been removed as the code turned out to be rather tricky and hard to maintain; so we only have one instance of this class. But end users can add their own instances, if needed.

NB. sListArray insists on a concrete initializer, because not having one would break referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details.

Methods

sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b Source #

Create a literal array

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

Instances details
 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 #sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> 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 #

newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source #

Create a new anonymous array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see newArray_

newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) Source #

Create a named new array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see newArray

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

#### Instances

Instances details

# Creating symbolic values

## Single value

These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms for free (specialized at the given type), but they might be easier to use. We provide both the named and anonymous versions, latter with the underscore suffix.

Declare a named SBool

NB. For a version which generalizes over the underlying monad, see sBool

Declare an unnamed SBool

NB. For a version which generalizes over the underlying monad, see sBool_

Declare a named SWord8

NB. For a version which generalizes over the underlying monad, see sWord8

Declare an unnamed SWord8

NB. For a version which generalizes over the underlying monad, see sWord8_

Declare a named SWord16

NB. For a version which generalizes over the underlying monad, see sWord16

Declare an unnamed SWord16

NB. For a version which generalizes over the underlying monad, see sWord16_

Declare a named SWord32

NB. For a version which generalizes over the underlying monad, see sWord32

Declare an unamed SWord32

NB. For a version which generalizes over the underlying monad, see sWord32_

Declare a named SWord64

NB. For a version which generalizes over the underlying monad, see sWord64

Declare an unnamed SWord64

NB. For a version which generalizes over the underlying monad, see sWord64_

sWord :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SWord n) Source #

Declare a named SWord

NB. For a version which generalizes over the underlying monad, see sWord

sWord_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SWord n) Source #

Declare an unnamed SWord

NB. For a version which generalizes over the underlying monad, see sWord_

Declare a named SInt8

NB. For a version which generalizes over the underlying monad, see sInt8

Declare an unnamed SInt8

NB. For a version which generalizes over the underlying monad, see sInt8_

Declare a named SInt16

NB. For a version which generalizes over the underlying monad, see sInt16

Declare an unnamed SInt16

NB. For a version which generalizes over the underlying monad, see sInt16_

Declare a named SInt32

NB. For a version which generalizes over the underlying monad, see sInt32

Declare an unnamed SInt32

NB. For a version which generalizes over the underlying monad, see sInt32_

Declare a named SInt64

NB. For a version which generalizes over the underlying monad, see sInt64

Declare an unnamed SInt64

NB. For a version which generalizes over the underlying monad, see sInt64_

sInt :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SInt n) Source #

Declare a named SInt

NB. For a version which generalizes over the underlying monad, see sInt

sInt_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SInt n) Source #

Declare an unnamed SInt

NB. For a version which generalizes over the underlying monad, see sInt_

Declare a named SInteger

NB. For a version which generalizes over the underlying monad, see sInteger

Declare an unnamed SInteger

NB. For a version which generalizes over the underlying monad, see sInteger_

Declare a named SReal

NB. For a version which generalizes over the underlying monad, see sReal

Declare an unnamed SReal

NB. For a version which generalizes over the underlying monad, see sReal_

Declare a named SRational.

NB. For a version which generalizes over the underlying monad, see sRational

Declare an unnamed SRational.

NB. For a version which generalizes over the underlying monad, see sRational_

Declare a named SFloat

NB. For a version which generalizes over the underlying monad, see sFloat

Declare an unnamed SFloat

NB. For a version which generalizes over the underlying monad, see sFloat_

Declare a named SDouble

NB. For a version which generalizes over the underlying monad, see sDouble

Declare an unnamed SDouble

NB. For a version which generalizes over the underlying monad, see sDouble_

sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb) Source #

Declare a named 'SFloatingPoint eb sb'

NB. For a version which generalizes over the underlying monad, see sFloatingPoint

sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb) Source #

Declare an unnamed SFloatingPoint eb sb

NB. For a version which generalizes over the underlying monad, see sFloatingPoint_

Declare a named SFPHalf

NB. For a version which generalizes over the underlying monad, see sFPHalf

Declare an unnamed SFPHalf

NB. For a version which generalizes over the underlying monad, see sFPHalf_

Declare a named SFPBFloat

NB. For a version which generalizes over the underlying monad, see SFPBFloat

Declare an unnamed SFPBFloat

NB. For a version which generalizes over the underlying monad, see SFPBFloat

Declare a named SFPSingle

NB. For a version which generalizes over the underlying monad, see sFPSingle

Declare an unnamed SFPSingle

NB. For a version which generalizes over the underlying monad, see sFPSingle_

Declare a named SFPDouble

NB. For a version which generalizes over the underlying monad, see sFPDouble

Declare an unnamed SFPDouble

NB. For a version which generalizes over the underlying monad, see sFPDouble_

Declare a named SFPQuad

NB. For a version which generalizes over the underlying monad, see sFPQuad

Declare an unnamed SFPQuad

NB. For a version which generalizes over the underlying monad, see sFPQuad_

Declare a named SChar

NB. For a version which generalizes over the underlying monad, see sChar

Declare an unnamed SChar

NB. For a version which generalizes over the underlying monad, see sChar_

Declare a named SString

NB. For a version which generalizes over the underlying monad, see sString

Declare an unnamed SString

NB. For a version which generalizes over the underlying monad, see sString_

sList :: SymVal a => String -> Symbolic (SList a) Source #

Declare a named SList

NB. For a version which generalizes over the underlying monad, see sList

sList_ :: SymVal a => Symbolic (SList a) Source #

Declare an unnamed SList

NB. For a version which generalizes over the underlying monad, see sList_

sTuple :: (SymTuple tup, SymVal tup) => String -> Symbolic (SBV tup) Source #

Declare a named tuple.

NB. For a version which generalizes over the underlying monad, see sTuple

sTuple_ :: (SymTuple tup, SymVal tup) => Symbolic (SBV tup) Source #

Declare an unnamed tuple.

NB. For a version which generalizes over the underlying monad, see sTuple_

sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b) Source #

Declare a named SEither.

NB. For a version which generalizes over the underlying monad, see sEither

sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b) Source #

Declare an unnamed SEither.

NB. For a version which generalizes over the underlying monad, see sEither_

sMaybe :: SymVal a => String -> Symbolic (SMaybe a) Source #

Declare a named SMaybe.

NB. For a version which generalizes over the underlying monad, see sMaybe

sMaybe_ :: SymVal a => Symbolic (SMaybe a) Source #

Declare an unnamed SMaybe.

NB. For a version which generalizes over the underlying monad, see sMaybe_

sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a) Source #

Declare a named SSet.

NB. For a version which generalizes over the underlying monad, see sSet

sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a) Source #

Declare an unnamed SSet.

NB. For a version which generalizes over the underlying monad, see sSet_

## List of values

These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms for mapM free (specialized at the given type), but they might be easier to use.

sBools :: [String] -> Symbolic [SBool] Source #

Declare a list of SBools

NB. For a version which generalizes over the underlying monad, see sBools

sWord8s :: [String] -> Symbolic [SWord8] Source #

Declare a list of SWord8s

NB. For a version which generalizes over the underlying monad, see sWord8s

sWord16s :: [String] -> Symbolic [SWord16] Source #

Declare a list of SWord16s

NB. For a version which generalizes over the underlying monad, see sWord16s

sWord32s :: [String] -> Symbolic [SWord32] Source #

Declare a list of SWord32s

NB. For a version which generalizes over the underlying monad, see sWord32s

sWord64s :: [String] -> Symbolic [SWord64] Source #

Declare a list of SWord64s

NB. For a version which generalizes over the underlying monad, see sWord64s

sWords :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SWord n] Source #

Declare a list of SWord8s

NB. For a version which generalizes over the underlying monad, see sWords

sInt8s :: [String] -> Symbolic [SInt8] Source #

Declare a list of SInt8s

NB. For a version which generalizes over the underlying monad, see sInt8s

sInt16s :: [String] -> Symbolic [SInt16] Source #

Declare a list of SInt16s

NB. For a version which generalizes over the underlying monad, see sInt16s

sInt32s :: [String] -> Symbolic [SInt32] Source #

Declare a list of SInt32s

NB. For a version which generalizes over the underlying monad, see sInt32s

sInt64s :: [String] -> Symbolic [SInt64] Source #

Declare a list of SInt64s

NB. For a version which generalizes over the underlying monad, see sInt64s

sInts :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SInt n] Source #

Declare a list of SInts

NB. For a version which generalizes over the underlying monad, see sInts

sIntegers :: [String] -> Symbolic [SInteger] Source #

Declare a list of SIntegers

NB. For a version which generalizes over the underlying monad, see sIntegers

sReals :: [String] -> Symbolic [SReal] Source #

Declare a list of SReals

NB. For a version which generalizes over the underlying monad, see sReals

sRationals :: [String] -> Symbolic [SRational] Source #

Declare a list of SRational values.

NB. For a version which generalizes over the underlying monad, see sRationals

sFloats :: [String] -> Symbolic [SFloat] Source #

Declare a list of SFloats

NB. For a version which generalizes over the underlying monad, see sFloats

sDoubles :: [String] -> Symbolic [SDouble] Source #

Declare a list of SDoubles

NB. For a version which generalizes over the underlying monad, see sDoubles

sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb] Source #

Declare a list of SFloatingPoint eb sb's

NB. For a version which generalizes over the underlying monad, see sFloatingPoints

sFPHalfs :: [String] -> Symbolic [SFPHalf] Source #

Declare a list of SFPHalfs

NB. For a version which generalizes over the underlying monad, see sFPHalfs

sFPBFloats :: [String] -> Symbolic [SFPBFloat] Source #

Declare a list of SFPQuads

NB. For a version which generalizes over the underlying monad, see sFPBFloats

sFPSingles :: [String] -> Symbolic [SFPSingle] Source #

Declare a list of SFPSingles

NB. For a version which generalizes over the underlying monad, see sFPSingles

sFPDoubles :: [String] -> Symbolic [SFPDouble] Source #

Declare a list of SFPDoubles

NB. For a version which generalizes over the underlying monad, see sFPDoubles

sFPQuads :: [String] -> Symbolic [SFPQuad] Source #

Declare a list of SFPQuads

NB. For a version which generalizes over the underlying monad, see sFPQuads

sChars :: [String] -> Symbolic [SChar] Source #

Declare a list of SChars

NB. For a version which generalizes over the underlying monad, see sChars

sStrings :: [String] -> Symbolic [SString] Source #

Declare a list of SStrings

NB. For a version which generalizes over the underlying monad, see sStrings

sLists :: SymVal a => [String] -> Symbolic [SList a] Source #

Declare a list of SLists

NB. For a version which generalizes over the underlying monad, see sLists

sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup] Source #

Declare a list of tuples.

NB. For a version which generalizes over the underlying monad, see sTuples

sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b] Source #

Declare a list of SEither values.

NB. For a version which generalizes over the underlying monad, see sEithers

sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a] Source #

Declare a list of SMaybe values.

NB. For a version which generalizes over the underlying monad, see sMaybes

sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a] Source #

Declare a list of SSet values.

NB. For a version which generalizes over the underlying monad, see sSets

# 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 Instances details  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 within the allowed inclusive range? #### Instances Instances details  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 Instances details  (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. default symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a Source # 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. #### Instances Instances details  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 (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 Instances details  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, BVIsNonZero n) => SIntegral (IntN n) Source # SIntegral instance for IntN Instance detailsDefined in Data.SBV.Core.Sized (KnownNat n, BVIsNonZero 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 Instances details  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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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, BVIsNonZero 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 Symbolic words (both signed and unsigned) are an instance of Haskell's Bits class, so regular bitwise operations are automatically available for them. Shifts and rotates, however, require specialized type-signatures since Haskell insists on an Int second argument for them. 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 multiplier, 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 Instances details  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, BVIsNonZero 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, BVIsNonZero 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  :: forall i j n bv proxy. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, BVIsNonZero ((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, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero 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  :: forall n m bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), BVIsNonZero (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

 :: forall n m bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), BVIsNonZero (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

 :: forall i n m bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, BVIsNonZero (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

 :: forall i n bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero 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.  class ByteConverter a where Source # A helper class to convert sized bit-vectors to/from bytes. Methods toBytes :: a -> [SWord 8] Source # Convert to a sequence of bytes >>> prove$ \a b c d -> toBytes ((fromBytes [a, b, c, d]) :: SWord 32) .== [a, b, c, d]
Q.E.D.


fromBytes :: [SWord 8] -> a Source #

Convert from a sequence of bytes

>>> prove \$ \r -> fromBytes (toBytes r) .== (r :: SWord 64)
Q.E.D.


#### Instances

Instances details
 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