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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV

Contents

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 = 32 :: 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
  • 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, SFunArray: Flat 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

sTrue :: SBool Source #

Symbolic True

sNot :: SBool -> SBool Source #

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

fromBool :: Bool -> SBool Source #

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

type SWord8 = SBV Word8 Source #

8-bit unsigned symbolic value

type SWord16 = SBV Word16 Source #

16-bit unsigned symbolic value

type SWord32 = SBV Word32 Source #

32-bit unsigned symbolic value

type SWord64 = SBV Word64 Source #

64-bit unsigned symbolic value

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

A symbolic unsigned bit-vector carrying its size info

data WordN (n :: Nat) Source #

An unsigned bit-vector carrying its size info

Instances
(KnownNat n, IsNonZero n) => Bounded (WordN n) Source #

Bounded instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

minBound :: WordN n #

maxBound :: WordN n #

(KnownNat n, IsNonZero n) => Enum (WordN n) Source #

Enum instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

succ :: 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 details

Defined in Data.SBV.Core.Sized

Methods

(==) :: WordN n -> WordN n -> Bool #

(/=) :: WordN n -> WordN n -> Bool #

(KnownNat n, IsNonZero n) => Integral (WordN n) Source #

Integral instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

quot :: WordN n -> WordN n -> WordN n #

rem :: WordN n -> WordN n -> WordN n #

div :: WordN n -> WordN n -> WordN n #

mod :: WordN n -> WordN n -> WordN n #

quotRem :: WordN n -> WordN n -> (WordN n, WordN n) #

divMod :: WordN n -> WordN n -> (WordN n, WordN n) #

toInteger :: WordN n -> Integer #

(KnownNat n, IsNonZero n) => Num (WordN n) Source #

Num instance for WordN

Instance details

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

fromInteger :: Integer -> WordN n #

Ord (WordN n) Source # 
Instance details

Defined in Data.SBV.Core.Sized

Methods

compare :: WordN n -> WordN n -> Ordering #

(<) :: WordN n -> WordN n -> Bool #

(<=) :: WordN n -> WordN n -> Bool #

(>) :: WordN n -> WordN n -> Bool #

(>=) :: WordN n -> WordN n -> Bool #

max :: WordN n -> WordN n -> WordN n #

min :: WordN n -> WordN n -> WordN n #

(KnownNat n, IsNonZero n) => Real (WordN n) Source #

Real instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

toRational :: WordN n -> Rational #

Show (WordN n) Source #

Show instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

showsPrec :: Int -> WordN n -> ShowS #

show :: WordN n -> String #

showList :: [WordN n] -> ShowS #

(KnownNat n, IsNonZero n) => Bits (WordN n) Source # 
Instance details

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

zeroBits :: 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 #

bitSizeMaybe :: WordN n -> Maybe Int #

bitSize :: WordN n -> Int #

isSigned :: WordN n -> Bool #

shiftL :: WordN n -> Int -> WordN n #

unsafeShiftL :: WordN n -> Int -> WordN n #

shiftR :: WordN n -> Int -> WordN n #

unsafeShiftR :: WordN n -> Int -> WordN n #

rotateL :: WordN n -> Int -> WordN n #

rotateR :: WordN n -> Int -> WordN n #

popCount :: WordN n -> Int #

(KnownNat n, IsNonZero n) => HasKind (WordN n) Source #

WordN has a kind

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SymVal (WordN n) Source #

SymVal instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SatModel (WordN n) Source #

Constructing models for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

parseCVs :: [CV] -> Maybe (WordN n, [CV]) Source #

cvtModel :: (WordN n -> Maybe b) -> Maybe (WordN n, [CV]) -> Maybe (b, [CV]) Source #

(KnownNat n, IsNonZero n) => Metric (WordN n) Source #

Optimizing WordN

Instance details

Defined in Data.SBV.Core.Sized

Associated Types

type MetricSpace (WordN n) :: Type Source #

(KnownNat n, IsNonZero n) => SDivisible (SWord n) Source #

SDivisible instance for SWord

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n) Source #

sDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source #

sQuot :: SWord n -> SWord n -> SWord n Source #

sRem :: SWord n -> SWord n -> SWord n Source #

sDiv :: SWord n -> SWord n -> SWord n Source #

sMod :: SWord n -> SWord n -> SWord n Source #

(KnownNat n, IsNonZero n) => SDivisible (WordN n) Source #

SDivisible instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: WordN n -> WordN n -> (WordN n, WordN n) Source #

sDivMod :: WordN n -> WordN n -> (WordN n, WordN n) Source #

sQuot :: WordN n -> WordN n -> WordN n Source #

sRem :: WordN n -> WordN n -> WordN n Source #

sDiv :: WordN n -> WordN n -> WordN n Source #

sMod :: WordN n -> WordN n -> WordN n Source #

(KnownNat n, IsNonZero n) => SFiniteBits (WordN n) Source #

SFiniteBits instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SIntegral (WordN n) Source #

SIntegral instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

ByteConverter (SWord 8) Source #

SWord 8 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 8 -> [SWord 8] Source #

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

ByteConverter (SWord 16) Source #

SWord 16 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 16 -> [SWord 8] Source #

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

ByteConverter (SWord 32) Source #

SWord 32 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 32 -> [SWord 8] Source #

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

ByteConverter (SWord 64) Source #

SWord 64 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 64 -> [SWord 8] Source #

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

ByteConverter (SWord 128) Source #

SWord 128 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 128 -> [SWord 8] Source #

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

ByteConverter (SWord 256) Source #

SWord 256 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 256 -> [SWord 8] Source #

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

ByteConverter (SWord 512) Source #

SWord 512 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 512 -> [SWord 8] Source #

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

ByteConverter (SWord 1024) Source #

SWord 1024 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 1024 -> [SWord 8] Source #

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

(KnownNat n, IsNonZero n) => Polynomial (SWord n) Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [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 #

showPoly :: SWord n -> String Source #

showPolynomial :: Bool -> SWord n -> String Source #

type MetricSpace (WordN n) Source # 
Instance details

Defined 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

type SInt16 = SBV Int16 Source #

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

type SInt32 = SBV Int32 Source #

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

type SInt64 = SBV Int64 Source #

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

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

A symbolic signed bit-vector carrying its size info

data IntN (n :: Nat) Source #

A signed bit-vector carrying its size info

Instances
(KnownNat n, IsNonZero n) => Bounded (IntN n) Source #

Bounded instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

minBound :: IntN n #

maxBound :: IntN n #

(KnownNat n, IsNonZero n) => Enum (IntN n) Source #

Enum instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

succ :: 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 details

Defined in Data.SBV.Core.Sized

Methods

(==) :: IntN n -> IntN n -> Bool #

(/=) :: IntN n -> IntN n -> Bool #

(KnownNat n, IsNonZero n) => Integral (IntN n) Source #

Integral instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

quot :: IntN n -> IntN n -> IntN n #

rem :: IntN n -> IntN n -> IntN n #

div :: IntN n -> IntN n -> IntN n #

mod :: IntN n -> IntN n -> IntN n #

quotRem :: IntN n -> IntN n -> (IntN n, IntN n) #

divMod :: IntN n -> IntN n -> (IntN n, IntN n) #

toInteger :: IntN n -> Integer #

(KnownNat n, IsNonZero n) => Num (IntN n) Source #

Num instance for IntN

Instance details

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

fromInteger :: Integer -> IntN n #

Ord (IntN n) Source # 
Instance details

Defined in Data.SBV.Core.Sized

Methods

compare :: IntN n -> IntN n -> Ordering #

(<) :: IntN n -> IntN n -> Bool #

(<=) :: IntN n -> IntN n -> Bool #

(>) :: IntN n -> IntN n -> Bool #

(>=) :: IntN n -> IntN n -> Bool #

max :: IntN n -> IntN n -> IntN n #

min :: IntN n -> IntN n -> IntN n #

(KnownNat n, IsNonZero n) => Real (IntN n) Source #

Real instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

toRational :: IntN n -> Rational #

Show (IntN n) Source #

Show instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

showsPrec :: Int -> IntN n -> ShowS #

show :: IntN n -> String #

showList :: [IntN n] -> ShowS #

(KnownNat n, IsNonZero n) => Bits (IntN n) Source # 
Instance details

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

zeroBits :: 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 #

bitSizeMaybe :: IntN n -> Maybe Int #

bitSize :: IntN n -> Int #

isSigned :: IntN n -> Bool #

shiftL :: IntN n -> Int -> IntN n #

unsafeShiftL :: IntN n -> Int -> IntN n #

shiftR :: IntN n -> Int -> IntN n #

unsafeShiftR :: IntN n -> Int -> IntN n #

rotateL :: IntN n -> Int -> IntN n #

rotateR :: IntN n -> Int -> IntN n #

popCount :: IntN n -> Int #

(KnownNat n, IsNonZero n) => HasKind (IntN n) Source #

IntN has a kind

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SymVal (IntN n) Source #

SymVal instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SatModel (IntN n) Source #

Constructing models for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

parseCVs :: [CV] -> Maybe (IntN n, [CV]) Source #

cvtModel :: (IntN n -> Maybe b) -> Maybe (IntN n, [CV]) -> Maybe (b, [CV]) Source #

(KnownNat n, IsNonZero n) => Metric (IntN n) Source #

Optimizing IntN

Instance details

Defined in Data.SBV.Core.Sized

Associated Types

type MetricSpace (IntN n) :: Type Source #

(KnownNat n, IsNonZero n) => SDivisible (SInt n) Source #

SDivisible instance for SInt

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n) Source #

sDivMod :: SInt n -> SInt n -> (SInt n, SInt n) Source #

sQuot :: SInt n -> SInt n -> SInt n Source #

sRem :: SInt n -> SInt n -> SInt n Source #

sDiv :: SInt n -> SInt n -> SInt n Source #

sMod :: SInt n -> SInt n -> SInt n Source #

(KnownNat n, IsNonZero n) => SDivisible (IntN n) Source #

SDivisible instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n) Source #

sDivMod :: IntN n -> IntN n -> (IntN n, IntN n) Source #

sQuot :: IntN n -> IntN n -> IntN n Source #

sRem :: IntN n -> IntN n -> IntN n Source #

sDiv :: IntN n -> IntN n -> IntN n Source #

sMod :: IntN n -> IntN n -> IntN n Source #

(KnownNat n, IsNonZero n) => SFiniteBits (IntN n) Source #

SFiniteBits instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SIntegral (IntN n) Source #

SIntegral instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

type MetricSpace (IntN n) Source # 
Instance details

Defined in Data.SBV.Core.Sized

type MetricSpace (IntN n) = WordN n

Converting between fixed-size and arbitrary bitvectors

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

Type family to create the appropriate non-zero constraint

Equations

IsNonZero 0 = TypeError ZeroWidth 
IsNonZero n = () 

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

Capture the correspondence between sized and fixed-sized BVs

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

Capture the correspondence between fixed-sized and sized BVs

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:

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

type SInteger = SBV Integer Source #

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 SFloat = SBV Float Source #

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double Source #

IEEE-754 double-precision floating point numbers

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

type SReal = SBV AlgReal Source #

Infinite precision symbolic algebraic real value

data AlgReal Source #

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

Instances
Eq AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Methods

(==) :: AlgReal -> AlgReal -> Bool #

(/=) :: AlgReal -> AlgReal -> Bool #

Fractional AlgReal Source #

NB: Following the other types we have, we require `a/0` to be `0` for all a.

Instance details

Defined in Data.SBV.Core.AlgReals

Num AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Ord AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Real AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Show AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Arbitrary AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Random AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Methods

randomR :: 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] #

HasKind AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Kind

SymVal AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

SatModel AlgReal Source #

AlgReal as extracted from a model

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCVs :: [CV] -> Maybe (AlgReal, [CV]) Source #

cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CV]) -> Maybe (b, [CV]) Source #

Metric AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

Associated Types

type MetricSpace AlgReal :: Type Source #

IEEEFloatConvertible AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Floating

type MetricSpace AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

sRealToSInteger :: SReal -> SInteger Source #

Convert an SReal to an SInteger. That is, it computes the largest integer n that satisfies sIntegerToSReal n <= r essentially giving us the floor.

For instance, 1.3 will be 1, but -1.3 will be -2.

algRealToRational :: AlgReal -> Either Rational Rational Source #

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.

Characters, Strings and Regular Expressions

Support for characters, strings, and regular expressions (intial 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, as far as SBV's symbolic strings are concerned, a character is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV character for the time being. This limitation is due to the SMT-solvers only supporting this particular subset. However, there is a pending proposal to add support for unicode, and SBV will track these changes to have full unicode support as solvers become available. For details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

type SString = SBV String Source #

A symbolic string. Note that a symbolic string is not a list of symbolic characters, that is, it is not the case that SString = [SChar], unlike what one might expect following Haskell strings. An SString is a symbolic value of its own, of possibly arbitrary but finite length, and internally processed as one unit as opposed to a fixed-length list of characters.

Symbolic lists

Support for symbolic lists (intial 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
SymTuple () Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c, d) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c, d, e) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymTuple (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined 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
Show a => Show (RCSet a) Source #

Show instance. Regular sets are shown as usual. Complements are shown "U -" notation.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> RCSet a -> ShowS #

show :: RCSet a -> String #

showList :: [RCSet a] -> ShowS #

HasKind a => HasKind (RCSet a) Source # 
Instance details

Defined in Data.SBV.Core.Concrete

(Ord a, SymVal a) => SymVal (RCSet a) Source # 
Instance details

Defined in Data.SBV.Core.Model

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 #

Flat arrays of symbolic values An array a b is an array indexed by the type SBV a, with elements of type SBV b.

If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.

While it's certainly possible for user to create instances of SymArray, the SArray and SFunArray instances already provided should cover most use cases in practice. Note that there are a few differences between these two models in terms of use models:

  • SArray produces SMTLib arrays, and requires a solver that understands the array theory. SFunArray is internally handled, and thus can be used with any solver. (Note that all solvers except abc support arrays, so this isn't a big decision factor.)
  • For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
  • Only SArray supports checking equality of arrays. (That is, checking if an entire array is equivalent to another.) SFunArrays cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible.
  • Only SFunArray supports compilation to C. Programs using SArray will not be accepted by the C-code generator.
  • You cannot use quickcheck on programs that contain these arrays. (Neither SArray nor SFunArray.)
  • With SArray, SBV transfers all array-processing to the SMT-solver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. With SFunArray, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.

As a rule of thumb, try SArray first. These should generate compact code. However, if the backend solver has hard time solving the generated problems, switch to SFunArray. If you still have issues, please report so we can see what the problem might be!

Methods

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
SymArray SFunArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SFunArray a b) Source #

newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SFunArray a b) Source #

readArray :: SFunArray a b -> SBV a -> SBV b Source #

writeArray :: SymVal b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #

mergeArrays :: SymVal b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source #

SymArray SArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source #

newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source #

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 unintialized value is OK. If the default value is given in newArray, it will be the result. Otherwise, the read yields an uninterpreted constant.
  • Can check for equality of these arrays
  • Cannot be used in code-generation (i.e., compilation to C)
  • Cannot quick-check theorems using SArray values
  • Typically slower as it heavily relies on SMT-solving for the array theory
Instances
SymArray SArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source #

newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source #

(HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: (SArray a b -> p) -> SymbolicT m SBool Source #

forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool Source #

forSome_ :: (SArray a b -> p) -> SymbolicT m SBool Source #

forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool Source #

prove :: (SArray a b -> p) -> m ThmResult Source #

proveWith :: SMTConfig -> (SArray a b -> p) -> m ThmResult Source #

sat :: (SArray a b -> p) -> m SatResult Source #

satWith :: SMTConfig -> (SArray a b -> p) -> m SatResult Source #

allSat :: (SArray a b -> p) -> m AllSatResult Source #

allSatWith :: SMTConfig -> (SArray a b -> p) -> m AllSatResult Source #

optimize :: OptimizeStyle -> (SArray a b -> p) -> m OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> m OptimizeResult Source #

isVacuous :: (SArray a b -> p) -> m Bool Source #

isVacuousWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #

isTheorem :: (SArray a b -> p) -> m Bool Source #

isTheoremWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #

isSatisfiable :: (SArray a b -> p) -> m Bool Source #

isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> m Bool Source #

validate :: Bool -> SMTConfig -> (SArray a b -> p) -> SMTResult -> m SMTResult Source #

(HasKind a, HasKind b) => Show (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

showsPrec :: Int -> SArray a b -> ShowS #

show :: SArray a b -> String #

showList :: [SArray a b] -> ShowS #

SymVal b => Mergeable (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #

select :: (Ord b0, SymVal b0, Num b0) => [SArray a b] -> SArray a b -> SBV b0 -> SArray a b Source #

EqSymbolic (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(.==) :: SArray a b -> SArray a b -> SBool Source #

(./=) :: SArray a b -> SArray a b -> SBool Source #

(.===) :: SArray a b -> SArray a b -> SBool Source #

(./==) :: SArray a b -> SArray a b -> SBool Source #

distinct :: [SArray a b] -> SBool Source #

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

allEqual :: [SArray a b] -> SBool Source #

sElem :: SArray a b -> [SArray a b] -> SBool Source #

sNotElem :: SArray a b -> [SArray a b] -> SBool Source #

data SFunArray a b Source #

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

  • Internally handled by the library and not mapped to SMT-Lib, hence can be used with solvers that don't support arrays. (Such as abc.)
  • Reading from an unintialized value is OK. If the default value is given in newArray, it will be the result. Otherwise, the read yields an uninterpreted constant.
  • Cannot check for equality of arrays.
  • Can be used in code-generation (i.e., compilation to C).
  • Can not quick-check theorems using SFunArray values
  • Typically faster as it gets compiled away during translation.
Instances
SymArray SFunArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SFunArray a b) Source #

newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SFunArray a b) Source #

readArray :: SFunArray a b -> SBV a -> SBV b Source #

writeArray :: SymVal b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #

mergeArrays :: SymVal b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source #

(HasKind a, HasKind b, MProvable m p) => MProvable m (SFunArray a b -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

(HasKind a, HasKind b) => Show (SFunArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

showsPrec :: Int -> SFunArray a b -> ShowS #

show :: SFunArray a b -> String #

showList :: [SFunArray a b] -> ShowS #

SymVal b => Mergeable (SFunArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

select :: (Ord b0, SymVal b0, Num b0) => [SFunArray a b] -> SFunArray a b -> SBV b0 -> SFunArray a b Source #

Creating symbolic values

Single value

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.

sBool :: String -> Symbolic SBool Source #

Declare a named SBool

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

sBool_ :: Symbolic SBool Source #

Declare an unnamed SBool

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

sWord8 :: String -> Symbolic SWord8 Source #

Declare a named SWord8

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

sWord8_ :: Symbolic SWord8 Source #

Declare an unnamed SWord8

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

sWord16 :: String -> Symbolic SWord16 Source #

Declare a named SWord16

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

sWord16_ :: Symbolic SWord16 Source #

Declare an unnamed SWord16

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

sWord32 :: String -> Symbolic SWord32 Source #

Declare a named SWord32

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

sWord32_ :: Symbolic SWord32 Source #

Declare an unamed SWord32

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

sWord64 :: String -> Symbolic SWord64 Source #

Declare a named SWord64

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

sWord64_ :: Symbolic SWord64 Source #

Declare an unnamed SWord64

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

sWord :: (KnownNat n, IsNonZero 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, IsNonZero n) => Symbolic (SWord n) Source #

Declare an unnamed SWord

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

sInt8 :: String -> Symbolic SInt8 Source #

Declare a named SInt8

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

sInt8_ :: Symbolic SInt8 Source #

Declare an unnamed SInt8

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

sInt16 :: String -> Symbolic SInt16 Source #

Declare a named SInt16

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

sInt16_ :: Symbolic SInt16 Source #

Declare an unnamed SInt16

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

sInt32 :: String -> Symbolic SInt32 Source #

Declare a named SInt32

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

sInt32_ :: Symbolic SInt32 Source #

Declare an unnamed SInt32

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

sInt64 :: String -> Symbolic SInt64 Source #

Declare a named SInt64

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

sInt64_ :: Symbolic SInt64 Source #

Declare an unnamed SInt64

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

sInt :: (KnownNat n, IsNonZero 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, IsNonZero n) => Symbolic (SInt n) Source #

Declare an unnamed SInt

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

sInteger :: String -> Symbolic SInteger Source #

Declare a named SInteger

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

sInteger_ :: Symbolic SInteger Source #

Declare an unnamed SInteger

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

sReal :: String -> Symbolic SReal Source #

Declare a named SReal

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

sReal_ :: Symbolic SReal Source #

Declare an unnamed SReal

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

sFloat :: String -> Symbolic SFloat Source #

Declare a named SFloat

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

sFloat_ :: Symbolic SFloat Source #

Declare an unnamed SFloat

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

sDouble :: String -> Symbolic SDouble Source #

Declare a named SDouble

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

sDouble_ :: Symbolic SDouble Source #

Declare an unnamed SDouble

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

sChar :: String -> Symbolic SChar Source #

Declare a named SChar

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

sChar_ :: Symbolic SChar Source #

Declare an unnamed SChar

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

sString :: String -> Symbolic SString Source #

Declare a named SString

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

sString_ :: Symbolic SString Source #

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, IsNonZero 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, IsNonZero 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

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

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
EqSymbolic Bool Source # 
Instance details

Defined in Data.SBV.Core.Model

EqSymbolic a => EqSymbolic [a] Source # 
Instance details

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

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

EqSymbolic (SBV a) Source # 
Instance details

Defined 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

Defined in Documentation.SBV.Examples.ProofTools.BMC

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 details

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

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

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

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

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

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

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

Defined in Data.SBV.Core.Model

Methods

(.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.===) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(./==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

distinct :: [(a, b, c, d, e, f, g)] -> SBool Source #

distinctExcept :: [(a, b, c, d, e, f, g)] -> [(a, b, c, d, e, f, g)] -> SBool Source #

allEqual :: [(a, b, c, d, e, f, g)] -> SBool Source #

sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source #

sNotElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source #

class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #

Symbolic Comparisons. Similar to Eq, we cannot implement Haskell's Ord class since there is no way to return an Ordering value from a symbolic comparison. Furthermore, OrdSymbolic requires Mergeable to implement if-then-else, for the benefit of implementing symbolic versions of max and min functions.

Minimal complete definition

(.<)

Methods

(.<) :: a -> a -> SBool infix 4 Source #

Symbolic less than.

(.<=) :: a -> a -> SBool infix 4 Source #

Symbolic less than or equal to.

(.>) :: a -> a -> SBool infix 4 Source #

Symbolic greater than.

(.>=) :: a -> a -> SBool infix 4 Source #

Symbolic greater than or equal to.

smin :: a -> a -> a Source #

Symbolic minimum.

smax :: a -> a -> a Source #

Symbolic maximum.

inRange :: a -> (a, a) -> SBool Source #

Is the value withing the allowed inclusive range?

Instances
OrdSymbolic a => OrdSymbolic [a] Source # 
Instance details

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

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

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

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

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

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

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

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

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

Defined in Data.SBV.Core.Model

Methods

(.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #

smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #

inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool Source #

class Equality a where Source #

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

Methods

(===) :: a -> a -> IO ThmResult infix 4 Source #

Instances
(SymVal a, SymVal b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # 
Instance details

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

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

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

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

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

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

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

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

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

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

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

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

Defined in Data.SBV.Core.Model

Methods

(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source #

Conditionals: Mergeable values

class Mergeable a where Source #

Symbolic conditionals are modeled by the Mergeable class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed.

A Mergeable instance may be automatically derived for a custom data-type with a single constructor where the type of each field is an instance of Mergeable, such as a record of symbolic values. Users only need to add Generic and Mergeable to the deriving clause for the data-type. See Status for an example and an illustration of what the instance would look like if written by hand.

The function select is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way generalization of the ite function.

Minimal complete definition: None, if the type is instance of Generic. Otherwise symbolicMerge. Note that most types subject to merging are likely to be trivial instances of Generic.

Minimal complete definition

Nothing

Methods

symbolicMerge :: Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

select :: (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a Source #

Total indexing operation. select xs default index is intuitively the same as xs !! index, except it evaluates to default if index underflows/overflows.

symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

Instances
Mergeable () Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> () -> () -> () Source #

select :: (Ord b, SymVal b, Num b) => [()] -> () -> SBV b -> () Source #

Mergeable Mostek Source # 
Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

Methods

symbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek Source #

select :: (Ord b, SymVal b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source #

Mergeable Status Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

symbolicMerge :: Bool -> SBool -> Status -> Status -> Status Source #

select :: (Ord b, SymVal b, Num b) => [Status] -> Status -> SBV b -> Status Source #

Mergeable a => Mergeable [a] Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.ProofTools.Sum

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

Methods

symbolicMerge :: 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

Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> Array a b -> Array a b -> Array a b Source #

select :: (Ord b0, SymVal b0, Num b0) => [Array a b] -> Array a b -> SBV b0 -> Array a b Source #

SymVal b => Mergeable (SFunArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

select :: (Ord b0, SymVal b0, Num b0) => [SFunArray a b] -> SFunArray a b -> SBV b0 -> SFunArray a b Source #

SymVal b => Mergeable (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Tools.STree

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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 details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: 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
SIntegral Int8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Int16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Int32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Int64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Integer Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Word8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Word16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Word32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SIntegral Word64 Source # 
Instance details

Defined in Data.SBV.Core.Model

(KnownNat n, IsNonZero n) => SIntegral (IntN n) Source #

SIntegral instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SIntegral (WordN n) Source #

SIntegral instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Division and Modulus

class SDivisible a where Source #

The SDivisible class captures the essence of division. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic 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

sQuotRem, sDivMod

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
SDivisible Int8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Int16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Int32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Int64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Integer Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Word8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Word16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Word32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible Word64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible CV Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

sQuotRem :: 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 #

SDivisible SInteger Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord8 Source # 
Instance details

Defined in Data.SBV.Core.Model

(KnownNat n, IsNonZero n) => SDivisible (SInt n) Source #

SDivisible instance for SInt

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n) Source #

sDivMod :: SInt n -> SInt n -> (SInt n, SInt n) Source #

sQuot :: SInt n -> SInt n -> SInt n Source #

sRem :: SInt n -> SInt n -> SInt n Source #

sDiv :: SInt n -> SInt n -> SInt n Source #

sMod :: SInt n -> SInt n -> SInt n Source #

(KnownNat n, IsNonZero n) => SDivisible (IntN n) Source #

SDivisible instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n) Source #

sDivMod :: IntN n -> IntN n -> (IntN n, IntN n) Source #

sQuot :: IntN n -> IntN n -> IntN n Source #

sRem :: IntN n -> IntN n -> IntN n Source #

sDiv :: IntN n -> IntN n -> IntN n Source #

sMod :: IntN n -> IntN n -> IntN n Source #

(KnownNat n, IsNonZero n) => SDivisible (SWord n) Source #

SDivisible instance for SWord

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n) Source #

sDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source #

sQuot :: SWord n -> SWord n -> SWord n Source #

sRem :: SWord n -> SWord n -> SWord n Source #

sDiv :: SWord n -> SWord n -> SWord n Source #

sMod :: SWord n -> SWord n -> SWord n Source #

(KnownNat n, IsNonZero n) => SDivisible (WordN n) Source #

SDivisible instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Methods

sQuotRem :: 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

sFiniteBitSize :: SBV a -> Int Source #

Bit size.

lsb :: SBV a -> SBool Source #

Least significant bit of a word, always stored at index 0.

msb :: SBV a -> SBool Source #

Most significant bit of a word, always stored at the last position.

blastBE :: SBV a -> [SBool] Source #

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.

sPopCount :: SBV a -> SWord8 Source #

Variant of popCount, returning a symbolic value.

setBitTo :: SBV a -> Int -> SBool -> SBV a Source #

A combo of setBit and clearBit, when the bit to be set is symbolic.

fullAdder :: SBV a -> SBV a -> (SBool, SBV a) Source #

Full adder, returns carry-out from the addition. Only for unsigned quantities.

fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) Source #

Full multipler, returns both high and low-order bits. Only for unsigned quantities.

sCountLeadingZeros :: SBV a -> SWord8 Source #

Count leading zeros in a word, big-endian interpretation.

sCountTrailingZeros :: SBV a -> SWord8 Source #

Count trailing zeros in a word, big-endian interpretation.

Instances
SFiniteBits Int8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Int16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Int32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Int64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Word8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Word16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Word32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SFiniteBits Word64 Source # 
Instance details

Defined in Data.SBV.Core.Model

(KnownNat n, IsNonZero n) => SFiniteBits (IntN n) Source #

SFiniteBits instance for IntN

Instance details

Defined in Data.SBV.Core.Sized

(KnownNat n, IsNonZero n) => SFiniteBits (WordN n) Source #

SFiniteBits instance for WordN

Instance details

Defined in Data.SBV.Core.Sized

Splitting, joining, and extending bit-vectors

bvExtract Source #

Arguments

:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) 
=> proxy i

i: Start position, numbered from n-1 to 0

-> proxy j

j: End position, numbered from n-1 to 0, j <= i must hold

-> SBV (bv n)

Input bit vector of size n

-> SBV (bv ((i - j) + 1))

Output is of size i - j + 1

Extract a portion of bits to form a smaller bit-vector.

>>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
Q.E.D.

(#) infixr 5 Source #

Arguments

:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m)) 
=> SBV (bv n)

First input, of size n, becomes the left side

-> SBV (bv m)

Second input, of size m, becomes the right side

-> SBV (bv (n + m))

Concatenation, of size n+m

Join two bitvectors.

>>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
Q.E.D.

zeroExtend Source #

Arguments

:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), IsNonZero (m - n)) 
=> SBV (bv n)

Input, of size n

-> SBV (bv m)

Output, of size m. n < m must hold

Zero extend a bit-vector.

>>> prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.

signExtend Source #

Arguments

:: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), IsNonZero (m - n)) 
=> SBV (bv n)

Input, of size n

-> SBV (bv m)

Output, of size m. n < m must hold

Sign extend a bit-vector.

>>> prove $ \x -> sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.
>>> prove $ \x ->       msb x  .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
Q.E.D.

bvDrop Source #

Arguments

:: (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, IsNonZero (n - i)) 
=> proxy i

i: Number of bits to drop. i < n must hold.

-> SBV (bv n)

Input, of size n

-> SBV (bv m)

Output, of size m. m = n - i holds.

Drop bits from the top of a bit-vector.

>>> prove $ \x -> bvDrop (Proxy @0) (x :: SWord 43) .== x
Q.E.D.
>>> prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0
Q.E.D.

bvTake Source #

Arguments

:: (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n) 
=> proxy i

i: Number of bits to take. 0 < i <= n must hold.

-> SBV (bv n)

Input, of size n

-> SBV (bv i)

Output, of size i

Take bits from the top of a bit-vector.

>>> prove $ \x -> bvTake (Proxy @13) (x :: SWord 13) .== x
Q.E.D.
>>> prove $ \x -> bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
Q.E.D.
>>> prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
Q.E.D.

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
ByteConverter (SWord 8) Source #

SWord 8 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 8 -> [SWord 8] Source #

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

ByteConverter (SWord 16) Source #

SWord 16 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 16 -> [SWord 8] Source #

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

ByteConverter (SWord 32) Source #

SWord 32 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 32 -> [SWord 8] Source #

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

ByteConverter (SWord 64) Source #

SWord 64 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 64 -> [SWord 8] Source #

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

ByteConverter (SWord 128) Source #

SWord 128 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 128 -> [SWord 8] Source #

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

ByteConverter (SWord 256) Source #

SWord 256 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 256 -> [SWord 8] Source #

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

ByteConverter (SWord 512) Source #

SWord 512 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 512 -> [SWord 8] Source #

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

ByteConverter (SWord 1024) Source #

SWord 1024 instance for ByteConverter

Instance details

Defined in Data.SBV.Core.Sized

Methods

toBytes :: SWord 1024 -> [SWord 8] Source #

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

Exponentiation

(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b Source #

Symbolic exponentiation using bit blasting and repeated squaring.

N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.

IEEE-floating point numbers

class (SymVal a, RealFloat a) => IEEEFloating a where Source #

A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.

Minimal complete definition

Nothing

Methods

fpAbs :: SBV a -> SBV a Source #

Compute the floating point absolute value.

fpNeg :: SBV a -> SBV a Source #

Compute the unary negation. Note that 0 - x is not equivalent to -x for floating-point, since -0 and 0 are different.

fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Add two floating point values, using the given rounding mode

fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Subtract two floating point values, using the given rounding mode

fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Multiply two floating point values, using the given rounding mode

fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Divide two floating point values, using the given rounding mode

fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a Source #

Fused-multiply-add three floating point values, using the given rounding mode. fpFMA x y z = x*y+z but with only one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since Haskell lacks an FMA implementation.

fpSqrt :: SRoundingMode -> SBV a -> SBV a Source #

Compute the square-root of a float, using the given rounding mode

fpRem :: SBV a -> SBV a -> SBV a Source #

Compute the remainder: x - y * n, where n is the truncated integer nearest to x/y. The rounding mode is implicitly assumed to be RoundNearestTiesToEven.

fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a Source #

Round to the nearest integral value, using the given rounding mode.

fpMin :: SBV a -> SBV a -> SBV a Source #

Compute the minimum of two floats, respects infinity and NaN values

fpMax :: SBV a -> SBV a -> SBV a Source #

Compute the maximum of two floats, respects infinity and NaN values

fpIsEqualObject :: SBV a -> SBV a -> SBool Source #

Are the two given floats exactly the same. That is, NaN will compare equal to itself, +0 will not compare equal to -0 etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==.)

fpIsNormal :: SBV a -> SBool Source #

Is the floating-point number a normal value. (i.e., not denormalized.)

fpIsSubnormal :: SBV a -> SBool Source #

Is the floating-point number a subnormal value. (Also known as denormal.)

fpIsZero :: SBV a -> SBool Source #

Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)

fpIsInfinite :: SBV a -> SBool Source #

Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)

fpIsNaN :: SBV a -> SBool Source #

Is the floating-point number a NaN value?

fpIsNegative :: SBV a -> SBool Source #

Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.

fpIsPositive :: SBV a -> SBool Source #

Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.

fpIsNegativeZero :: SBV a -> SBool Source #

Is the floating point number -0?

fpIsPositiveZero :: SBV a -> SBool Source #

Is the floating point number +0?

fpIsPoint :: SBV a -> SBool Source #

Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.

Instances
IEEEFloating Double Source #

SDouble instance

Instance details

Defined in Data.SBV.Core.Floating

IEEEFloating Float Source #

SFloat instance

Instance details

Defined in Data.SBV.Core.Floating

data RoundingMode Source #

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Constructors

RoundNearestTiesToEven

Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.)

RoundNearestTiesToAway

Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.)

RoundTowardPositive

Round towards positive infinity. (Also known as rounding-up or ceiling.)

RoundTowardNegative

Round towards negative infinity. (Also known as rounding-down or floor.)

RoundTowardZero

Round towards zero. (Also known as truncation.)

Instances
Bounded RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Enum RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Eq RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Data RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RoundingMode #

toConstr :: RoundingMode -> Constr #

dataTypeOf :: RoundingMode -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RoundingMode) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RoundingMode) #

gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

Ord RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Read RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

HasKind RoundingMode Source #

RoundingMode kind

Instance details

Defined in Data.SBV.Core.Symbolic

SymVal RoundingMode Source #

RoundingMode can be used symbolically

Instance details

Defined in Data.SBV.Core.Data

SatModel RoundingMode Source #

A rounding mode, extracted from a model. (Default definition suffices)

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCVs :: [CV] -> Maybe (RoundingMode, [CV]) Source #

cvtModel :: (RoundingMode -> Maybe b) -> Maybe (RoundingMode, [CV]) -> Maybe (b, [CV]) Source #

type SRoundingMode = SBV RoundingMode Source #

The symbolic variant of RoundingMode

nan :: Floating a => a Source #

Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

infinity :: Floating a => a Source #

Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

sNaN :: (Floating a, SymVal a) => SBV a Source #

Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat.

sInfinity :: (Floating a, SymVal a) => SBV a Source #

Symbolic variant of infinity. This value will inhabit both SDouble and SFloat.

Rounding modes

Conversion to/from floats

class SymVal a => IEEEFloatConvertible a where Source #

Capture convertability from/to FloatingPoint representations.

Conversions to float: toSFloat and toSDouble simply return the nearest representable float from the given type based on the rounding mode provided.

Conversions from float: fromSFloat and fromSDouble functions do the reverse conversion. However some care is needed when given values that are not representable in the integral target domain. For instance, converting an SFloat to an SInt8 is problematic. The rules are as follows:

If the input value is a finite point and when rounded in the given rounding mode to an integral value lies within the target bounds, then that result is returned. (This is the regular interpretation of rounding in IEEE754.)

Otherwise (i.e., if the integral value in the float or double domain) doesn't fit into the target type, then the result is unspecified. Note that if the input is +oo, -oo, or NaN, then the result is unspecified.

Due to the unspecified nature of conversions, SBV will never constant fold conversions from floats to integral values. That is, you will always get a symbolic value as output. (Conversions from floats to other floats will be constant folded. Conversions from integral values to floats will also be constant folded.)

Note that unspecified really means unspecified: In particular, SBV makes no guarantees about matching the behavior between what you might get in Haskell, via SMT-Lib, or the C-translation. If the input value is out-of-bounds as defined above, or is NaN or oo or -oo, then all bets are off. In particular C and SMTLib are decidedly undefine this case, though that doesn't mean they do the same thing! Same goes for Haskell, which seems to convert via Int64, but we do not model that behavior in SBV as it doesn't seem to be intentional nor well documented.

You can check for NaN, oo and -oo, using the predicates fpIsNaN, fpIsInfinite, and fpIsPositive, fpIsNegative predicates, respectively; and do the proper conversion based on your needs. (0 is a good choice, as are min/max bounds of the target type.)

Currently, SBV provides no predicates to check if a value would lie within range for a particular conversion task, as this depends on the rounding mode and the types involved and can be rather tricky to determine. (See http://github.com/LeventErkok/sbv/issues/456 for a discussion of the issues involved.) In a future release, we hope to be able to provide underflow and overflow predicates for these conversions as well.

Minimal complete definition

Nothing

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV a Source #

Convert from an IEEE74 single precision float.

toSFloat :: SRoundingMode -> SBV a -> SFloat Source #

Convert to an IEEE-754 Single-precision float.

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSFloat m (toSFloat m x) .== x
:}
>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Falsifiable. Counter-example:
  s0 = RoundNearestTiesToEven :: RoundingMode
  s1 =             -264306721 :: Int32

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

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

Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.

toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat Source #

Convert to an IEEE-754 Single-precision float.

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSFloat m (toSFloat m x) .== x
:}
>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Falsifiable. Counter-example:
  s0 = RoundNearestTiesToEven :: RoundingMode
  s1 =             -264306721 :: Int32

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

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

Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.

fromSDouble :: SRoundingMode -> SDouble -> SBV a Source #

Convert from an IEEE74 double precision float.

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

Convert to an IEEE-754 Double-precision float.

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSDouble m (toSDouble m x) .== x
:}
>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Q.E.D.
>>> prove $ roundTrip @Word32
Q.E.D.
>>> prove $ roundTrip @Int64
Falsifiable. Counter-example:
  s0 =  RoundTowardNegative :: RoundingMode
  s1 = -8069753317450726624 :: Int64

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

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

In this case the numerator is off by 224!

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

Convert to an IEEE-754 Double-precision float.

>>> :{
roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool
roundTrip m x = fromSDouble m (toSDouble m x) .== x
:}
>>> prove $ roundTrip @Int8
Q.E.D.
>>> prove $ roundTrip @Word8
Q.E.D.
>>> prove $ roundTrip @Int16
Q.E.D.
>>> prove $ roundTrip @Word16
Q.E.D.
>>> prove $ roundTrip @Int32
Q.E.D.
>>> prove $ roundTrip @Word32
Q.E.D.
>>> prove $ roundTrip @Int64
Falsifiable. Counter-example:
  s0 =  RoundTowardNegative :: RoundingMode
  s1 = -8069753317450726624 :: Int64

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

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

In this case the numerator is off by 224!

Instances
IEEEFloatConvertible Double Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Float Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Int8 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Int16 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Int32 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Int64 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Integer Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Word8 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Word16 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Word32 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible Word64 Source # 
Instance details

Defined in Data.SBV.Core.Floating

IEEEFloatConvertible AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Floating

Bit-pattern conversions

sFloatAsSWord32 :: SFloat -> SWord32 Source #

Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the representation for NaNs are not unique, this function will return a symbolic value when given a concrete NaN.

Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.

sWord32AsSFloat :: SWord32 -> SFloat Source #

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