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

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

Data.SBV.Internals

Contents

Description

Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.

Synopsis

Running symbolic programs manually

data Result #

Result of running a symbolic computation

Constructors

Result 

Fields

Instances

Show Result # 
NFData Result # 

Methods

rnf :: Result -> () #

data SBVRunMode #

Different means of running a symbolic piece of code

Constructors

SMTMode IStage Bool SMTConfig

In regular mode, with a stage. Bool is True if this is SAT.

CodeGen

Code generation mode.

Concrete

Concrete simulation mode.

data IStage #

Stage of an interactive run

Constructors

ISetup 
IRun 

Solver capabilities

data SolverCapabilities #

Translation tricks needed for specific capabilities afforded by each solver

Constructors

SolverCapabilities 

Fields

Internal structures useful for low-level programming

type SBool = SBV Bool #

A symbolic boolean/bit

type SWord8 = SBV Word8 #

8-bit unsigned symbolic value

type SWord16 = SBV Word16 #

16-bit unsigned symbolic value

type SWord32 = SBV Word32 #

32-bit unsigned symbolic value

type SWord64 = SBV Word64 #

64-bit unsigned symbolic value

type SInt8 = SBV Int8 #

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

type SInt16 = SBV Int16 #

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

type SInt32 = SBV Int32 #

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

type SInt64 = SBV Int64 #

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

type SInteger = SBV Integer #

Infinite precision signed symbolic value

type SReal = SBV AlgReal #

Infinite precision symbolic algebraic real value

type SFloat = SBV Float #

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double #

IEEE-754 double-precision floating point numbers

nan :: Floating a => a #

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 #

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

sNaN :: (Floating a, SymWord a) => SBV a #

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

sInfinity :: (Floating a, SymWord a) => SBV a #

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

data RoundingMode #

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 # 
Enum RoundingMode # 
Eq RoundingMode # 
Data RoundingMode # 

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 # 
Read RoundingMode # 
Show RoundingMode # 
HasKind RoundingMode #

RoundingMode kind

SymWord RoundingMode #

RoundingMode can be used symbolically

SatModel RoundingMode #

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

Methods

parseCWs :: [CW] -> Maybe (RoundingMode, [CW]) #

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

type SRoundingMode = SBV RoundingMode #

The symbolic variant of RoundingMode

sRoundTowardPositive :: SRoundingMode #

Symbolic variant of RoundNearestPositive

class (HasKind a, Ord a) => SymWord a where #

A SymWord is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with prove, sat, allSat etc, as default instances automatically provide the necessary bits.

Methods

forall :: String -> Symbolic (SBV a) #

Create a user named input (universal)

forall_ :: Symbolic (SBV a) #

Create an automatically named input

mkForallVars :: Int -> Symbolic [SBV a] #

Get a bunch of new words

exists :: String -> Symbolic (SBV a) #

Create an existential variable

exists_ :: Symbolic (SBV a) #

Create an automatically named existential variable

mkExistVars :: Int -> Symbolic [SBV a] #

Create a bunch of existentials

free :: String -> Symbolic (SBV a) #

Create a free variable, universal in a proof, existential in sat

free_ :: Symbolic (SBV a) #

Create an unnamed free variable, universal in proof, existential in sat

mkFreeVars :: Int -> Symbolic [SBV a] #

Create a bunch of free vars

symbolic :: String -> Symbolic (SBV a) #

Similar to free; Just a more convenient name

symbolics :: [String] -> Symbolic [SBV a] #

Similar to mkFreeVars; but automatically gives names based on the strings

literal :: a -> SBV a #

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe a #

Extract a literal, if the value is concrete

fromCW :: CW -> a #

Extract a literal, from a CW representation

isConcrete :: SBV a -> Bool #

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool #

Is the symbolic word really symbolic?

isConcretely :: SBV a -> (a -> Bool) -> Bool #

Does it concretely satisfy the given predicate?

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #

One stop allocator

literal :: Show a => a -> SBV a #

Turn a literal constant to symbolic

fromCW :: Read a => CW -> a #

Extract a literal, from a CW representation

mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #

One stop allocator

Instances

SymWord RoundingMode #

RoundingMode can be used symbolically

SymWord E # 
SymWord Word4 #

SymWord instance, allowing this type to be used in proofs/sat etc.

SymWord Color # 
SymWord Nationality # 
SymWord Beverage # 
SymWord Pet # 
SymWord Sport # 
SymWord U2Member # 
SymWord Location # 
SymWord Day # 
SymWord BinOp # 
SymWord UnOp # 
SymWord B # 
SymWord Q # 
SymWord L #

Declare instances to make L a usable uninterpreted sort. First we need the SymWord instance, with the default definition sufficing.

data CW #

CW represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the FromBits class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW 

Fields

Instances

Eq CW # 

Methods

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

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

Ord CW # 

Methods

compare :: CW -> CW -> Ordering #

(<) :: CW -> CW -> Bool #

(<=) :: CW -> CW -> Bool #

(>) :: CW -> CW -> Bool #

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

max :: CW -> CW -> CW #

min :: CW -> CW -> CW #

Show CW #

Show instance for CW.

Methods

showsPrec :: Int -> CW -> ShowS #

show :: CW -> String #

showList :: [CW] -> ShowS #

HasKind CW #

Kind instance for CW

PrettyNum CW # 

Methods

hexS :: CW -> String #

binS :: CW -> String #

hex :: CW -> String #

bin :: CW -> String #

SatModel CW #

CW as extracted from a model; trivial definition

Methods

parseCWs :: [CW] -> Maybe (CW, [CW]) #

cvtModel :: (CW -> Maybe b) -> Maybe (CW, [CW]) -> Maybe (b, [CW]) #

SDivisible CW # 

Methods

sQuotRem :: CW -> CW -> (CW, CW) #

sDivMod :: CW -> CW -> (CW, CW) #

sQuot :: CW -> CW -> CW #

sRem :: CW -> CW -> CW #

sDiv :: CW -> CW -> CW #

sMod :: CW -> CW -> CW #

data CWVal #

A constant value

Constructors

CWAlgReal !AlgReal

algebraic real

CWInteger !Integer

bit-vector/unbounded integer

CWFloat !Float

float

CWDouble !Double

double

CWUserSort !(Maybe Int, String)

value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations

Instances

Eq CWVal #

Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal doesn't have proper instances for these when values are infinitely precise reals. However, we do need a structural eq/ord for Map indexes; so define custom ones here:

Methods

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

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

Ord CWVal #

Ord instance for CWVal. Same comments as the Eq instance why this cannot be derived.

Methods

compare :: CWVal -> CWVal -> Ordering #

(<) :: CWVal -> CWVal -> Bool #

(<=) :: CWVal -> CWVal -> Bool #

(>) :: CWVal -> CWVal -> Bool #

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

max :: CWVal -> CWVal -> CWVal #

min :: CWVal -> CWVal -> CWVal #

data AlgReal #

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

Constructors

AlgRational Bool Rational 
AlgPolyRoot (Integer, Polynomial) (Maybe String) 

Instances

Eq AlgReal # 

Methods

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

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

Fractional AlgReal #

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

Num AlgReal # 
Ord AlgReal # 
Real AlgReal # 
Show AlgReal # 
Arbitrary AlgReal # 
Random AlgReal # 

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

randomRIO :: (AlgReal, AlgReal) -> IO AlgReal #

randomIO :: IO AlgReal #

HasKind AlgReal # 
SatModel AlgReal #

AlgReal as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (AlgReal, [CW]) #

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

SMTValue AlgReal # 

Methods

sexprToVal :: SExpr -> Maybe AlgReal #

IEEEFloatConvertable AlgReal # 

data ExtCW #

A simple expression type over extendent values, covering infinity, epsilon and intervals.

Instances

Show ExtCW #

Show instance, shows with the kind

Methods

showsPrec :: Int -> ExtCW -> ShowS #

show :: ExtCW -> String #

showList :: [ExtCW] -> ShowS #

HasKind ExtCW #

Kind instance for Extended CW

data GeneralizedCW #

A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.

Constructors

ExtendedCW ExtCW 
RegularCW CW 

isRegularCW :: GeneralizedCW -> Bool #

Is this a regular CW?

cwSameType :: CW -> CW -> Bool #

Are two CW's of the same type?

cwToBool :: CW -> Bool #

Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)

mkConstCW :: Integral a => Kind -> a -> CW #

Create a constant word from an integral.

liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b #

Lift a binary function through a CW

mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW #

Map a unary function through a CW.

mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW #

Map a binary function through a CW.

data SW #

A symbolic word, tracking it's signedness and size.

Constructors

SW !Kind !NodeId 

Instances

Eq SW # 

Methods

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

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

Ord SW # 

Methods

compare :: SW -> SW -> Ordering #

(<) :: SW -> SW -> Bool #

(<=) :: SW -> SW -> Bool #

(>) :: SW -> SW -> Bool #

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

max :: SW -> SW -> SW #

min :: SW -> SW -> SW #

Show SW # 

Methods

showsPrec :: Int -> SW -> ShowS #

show :: SW -> String #

showList :: [SW] -> ShowS #

NFData SW # 

Methods

rnf :: SW -> () #

HasKind SW # 

trueSW :: SW #

Constant True as an SW. Note that this value always occupies slot -1.

falseSW :: SW #

Constant False as an SW. Note that this value always occupies slot -2.

trueCW :: CW #

Constant True as a CW. We represent it using the integer value 1.

falseCW :: CW #

Constant False as a CW. We represent it using the integer value 0.

normCW :: CW -> CW #

Normalize a CW. Essentially performs modular arithmetic to make sure the value can fit in the given bit-size. Note that this is rather tricky for negative values, due to asymmetry. (i.e., an 8-bit negative number represents values in the range -128 to 127; thus we have to be careful on the negative side.)

data SVal #

The Symbolic value. Either a constant (Left) or a symbolic value (Right Cached). Note that caching is essential for making sure sharing is preserved.

Constructors

SVal !Kind !(Either CW (Cached SW)) 

Instances

Eq SVal #

Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do.

Methods

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

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

Show SVal # 

Methods

showsPrec :: Int -> SVal -> ShowS #

show :: SVal -> String #

showList :: [SVal] -> ShowS #

NFData SVal # 

Methods

rnf :: SVal -> () #

HasKind SVal # 

newtype SBV a #

The Symbolic value. The parameter a is phantom, but is extremely important in keeping the user interface strongly typed.

Constructors

SBV 

Fields

Instances

Boolean SBool # 
Provable SBool # 
Provable Predicate # 
SDivisible SInteger # 
SDivisible SInt64 # 
SDivisible SInt32 # 
SDivisible SInt16 # 
SDivisible SInt8 # 

Methods

sQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8) #

sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8) #

sQuot :: SInt8 -> SInt8 -> SInt8 #

sRem :: SInt8 -> SInt8 -> SInt8 #

sDiv :: SInt8 -> SInt8 -> SInt8 #

sMod :: SInt8 -> SInt8 -> SInt8 #

SDivisible SWord64 # 
SDivisible SWord32 # 
SDivisible SWord16 # 
SDivisible SWord8 # 
SDivisible SWord4 #

SDvisible instance, using default methods

FromBits SInt64 # 
FromBits SInt32 # 
FromBits SInt16 # 
FromBits SInt8 # 

Methods

fromBitsLE :: [SBool] -> SInt8 #

fromBitsBE :: [SBool] -> SInt8 #

FromBits SWord64 # 
FromBits SWord32 # 
FromBits SWord16 # 
FromBits SWord8 # 
FromBits SBool # 

Methods

fromBitsLE :: [SBool] -> SBool #

fromBitsBE :: [SBool] -> SBool #

FromBits SWord4 #

Conversion from bits

Polynomial SWord64 # 
Polynomial SWord32 # 
Polynomial SWord16 # 
Polynomial SWord8 # 
Splittable SWord64 SWord32 # 
Splittable SWord32 SWord16 # 
Splittable SWord16 SWord8 # 
Eq (SBV a) # 

Methods

(==) :: SBV a -> SBV a -> Bool #

(/=) :: SBV a -> SBV a -> Bool #

Show (SBV a) # 

Methods

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

show :: SBV a -> String #

showList :: [SBV a] -> ShowS #

Generic (SBV a) # 

Associated Types

type Rep (SBV a) :: * -> * #

Methods

from :: SBV a -> Rep (SBV a) x #

to :: Rep (SBV a) x -> SBV a #

NFData (SBV a) # 

Methods

rnf :: SBV a -> () #

(Random a, SymWord a) => Random (SBV a) # 

Methods

randomR :: RandomGen g => (SBV a, SBV a) -> g -> (SBV a, g) #

random :: RandomGen g => g -> (SBV a, g) #

randomRs :: RandomGen g => (SBV a, SBV a) -> g -> [SBV a] #

randoms :: RandomGen g => g -> [SBV a] #

randomRIO :: (SBV a, SBV a) -> IO (SBV a) #

randomIO :: IO (SBV a) #

HasKind (SBV a) # 

Methods

kindOf :: SBV a -> Kind #

hasSign :: SBV a -> Bool #

intSizeOf :: SBV a -> Int #

isBoolean :: SBV a -> Bool #

isBounded :: SBV a -> Bool #

isReal :: SBV a -> Bool #

isFloat :: SBV a -> Bool #

isDouble :: SBV a -> Bool #

isInteger :: SBV a -> Bool #

isUninterpreted :: SBV a -> Bool #

showType :: SBV a -> String #

Outputtable (SBV a) # 

Methods

output :: SBV a -> Symbolic (SBV a) #

(SymWord a, PrettyNum a) => PrettyNum (SBV a) # 

Methods

hexS :: SBV a -> String #

binS :: SBV a -> String #

hex :: SBV a -> String #

bin :: SBV a -> String #

SExecutable [SBV a] # 

Methods

sName_ :: [SBV a] -> Symbolic () #

sName :: [String] -> [SBV a] -> Symbolic () #

safe :: [SBV a] -> IO [SafeResult] #

safeWith :: SMTConfig -> [SBV a] -> IO [SafeResult] #

SExecutable (SBV a) # 

Methods

sName_ :: SBV a -> Symbolic () #

sName :: [String] -> SBV a -> Symbolic () #

safe :: SBV a -> IO [SafeResult] #

safeWith :: SMTConfig -> SBV a -> IO [SafeResult] #

HasKind a => Uninterpreted (SBV a) # 

Methods

uninterpret :: String -> SBV a #

cgUninterpret :: String -> [String] -> SBV a -> SBV a #

sbvUninterpret :: Maybe ([String], SBV a) -> String -> SBV a #

SymWord a => Mergeable (SBV a) # 

Methods

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

select :: (SymWord b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a #

SymWord a => OrdSymbolic (SBV a) # 

Methods

(.<) :: SBV a -> SBV a -> SBool #

(.<=) :: SBV a -> SBV a -> SBool #

(.>) :: SBV a -> SBV a -> SBool #

(.>=) :: SBV a -> SBV a -> SBool #

smin :: SBV a -> SBV a -> SBV a #

smax :: SBV a -> SBV a -> SBV a #

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

EqSymbolic (SBV a) # 

Methods

(.==) :: SBV a -> SBV a -> SBool #

(./=) :: SBV a -> SBV a -> SBool #

distinct :: [SBV a] -> SBool #

allEqual :: [SBV a] -> SBool #

sElem :: SBV a -> [SBV a] -> SBool #

(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) # 

Methods

sName_ :: ((SBV a, SBV b) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO [SafeResult] #

(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) # 

Methods

sName_ :: ((SBV a, SBV b, SBV c) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult] #

(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) # 

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult] #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) # 

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult] #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) # 

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult] #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) # 

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult] #

(SymWord a, SExecutable p) => SExecutable (SBV a -> p) # 

Methods

sName_ :: (SBV a -> p) -> Symbolic () #

sName :: [String] -> (SBV a -> p) -> Symbolic () #

safe :: (SBV a -> p) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a -> p) -> IO [SafeResult] #

(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) # 

Methods

sName_ :: (SBV a, SBV b) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b) -> Symbolic () #

safe :: (SBV a, SBV b) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b) -> IO [SafeResult] #

(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate #

prove :: ((SBV a, SBV b) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b) -> p) -> IO String #

(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate #

prove :: ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b, SBV c) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c) -> p) -> IO String #

(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate #

prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO String #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate #

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO String #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate #

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO String #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) # 

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate #

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult #

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO String #

(SymWord a, Provable p) => Provable (SBV a -> p) # 

Methods

forAll_ :: (SBV a -> p) -> Predicate #

forAll :: [String] -> (SBV a -> p) -> Predicate #

forSome_ :: (SBV a -> p) -> Predicate #

forSome :: [String] -> (SBV a -> p) -> Predicate #

prove :: (SBV a -> p) -> IO ThmResult #

proveWith :: SMTConfig -> (SBV a -> p) -> IO ThmResult #

sat :: (SBV a -> p) -> IO SatResult #

satWith :: SMTConfig -> (SBV a -> p) -> IO SatResult #

allSat :: (SBV a -> p) -> IO AllSatResult #

allSatWith :: SMTConfig -> (SBV a -> p) -> IO AllSatResult #

optimize :: OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult #

optimizeWith :: SMTConfig -> OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult #

isVacuous :: (SBV a -> p) -> IO Bool #

isVacuousWith :: SMTConfig -> (SBV a -> p) -> IO Bool #

isTheorem :: (SBV a -> p) -> IO Bool #

isTheoremWith :: SMTConfig -> (SBV a -> p) -> IO Bool #

isSatisfiable :: (SBV a -> p) -> IO Bool #

isSatisfiableWith :: SMTConfig -> (SBV a -> p) -> IO Bool #

proveWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> (SBV a -> p) -> IO String #

(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a #

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) # 

Methods

uninterpret :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a #

(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a #

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a #

(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV c -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a #

(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) # 

Methods

uninterpret :: String -> SBV b -> SBV a #

cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a #

sbvUninterpret :: Maybe ([String], SBV b -> SBV a) -> String -> SBV b -> SBV a #

SymWord e => Mergeable (STree i e) # 

Methods

symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e #

select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e #

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) # 

Methods

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

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) # 

Methods

(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult #

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) # 

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) # 

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 #

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) # 

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult #

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) # 

Methods

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

(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) # 

Methods

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

(SymWord a, EqSymbolic z) => Equality (SBV a -> z) # 

Methods

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

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) # 

Methods

sName_ :: (SBV a, SBV b, SBV c) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b, SBV c) -> Symbolic () #

safe :: (SBV a, SBV b, SBV c) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c) -> IO [SafeResult] #

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) # 

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> Symbolic () #

safe :: (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult] #

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) # 

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () #

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult] #

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) # 

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () #

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult] #

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) # 

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () #

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () #

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult] #

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult] #

type Rep (SBV a) # 
type Rep (SBV a) = D1 (MetaData "SBV" "Data.SBV.Core.Data" "sbv-7.3-2BEKkYYE0P74Phph0RsW2y" True) (C1 (MetaCons "SBV" PrefixI True) (S1 (MetaSel (Just Symbol "unSBV") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SVal)))

newtype NodeId #

A symbolic node id

Constructors

NodeId Int 

Instances

mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) #

Create a symbolic variable.

data ArrayContext #

The context of a symbolic array as created

Constructors

ArrayFree

A new array, the contents are uninitialized

ArrayMutate Int SW SW

An array created by mutating another array at a given cell

ArrayMerge SW Int Int

An array created by symbolically merging two other arrays

type ArrayInfo = (String, (Kind, Kind), ArrayContext) #

Representation for symbolic arrays

class SymArray array where #

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

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. (There are some differences between these models, however, see the corresponding declaration.)

Minimal complete definition: All methods are required, no defaults.

Minimal complete definition

newArray_, newArray, readArray, writeArray, mergeArrays

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (array a b) #

Create a new anonymous array

newArray :: (HasKind a, HasKind b) => String -> Symbolic (array a b) #

Create a named new array

readArray :: array a b -> SBV a -> SBV b #

Read the array element at a

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b #

Update the element at a to be b

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b #

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

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b) #

newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b) #

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

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b #

newtype SFunArray a b #

Arrays implemented internally as functions

  • Internally handled by the library and not mapped to SMT-Lib
  • Reading an uninitialized value is considered an error (will throw exception)
  • Cannot check for equality (internally represented as functions)
  • Can quick-check
  • Typically faster as it gets compiled away during translation

Constructors

SFunArray (SBV a -> SBV b) 

Instances

(HasKind a, HasKind b) => Show (SFunArray a b) # 

Methods

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

show :: SFunArray a b -> String #

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

(HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) # 
SymWord b => Mergeable (SFunArray a b) # 

Methods

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

select :: (SymWord b, Num b) => [SFunArray a b] -> SFunArray a b -> SBV b -> SFunArray a b #

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b #

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)

newtype SArray a b #

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 and yields an unspecified result
  • Can check for equality of these arrays
  • Cannot quick-check theorems using SArray values
  • Typically slower as it heavily relies on SMT-solving for the array theory

Constructors

SArray 

Fields

Instances

SymArray SArray # 

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b) #

newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b) #

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

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b #

(HasKind a, HasKind b) => Show (SArray a b) # 

Methods

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

show :: SArray a b -> String #

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

(HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) # 

Methods

forAll_ :: (SArray a b -> p) -> Predicate #

forAll :: [String] -> (SArray a b -> p) -> Predicate #

forSome_ :: (SArray a b -> p) -> Predicate #

forSome :: [String] -> (SArray a b -> p) -> Predicate #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proveWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] #

proveWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult) #

satWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)] #

satWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult) #

generateSMTBenchmark :: Bool -> (SArray a b -> p) -> IO String #

SymWord b => Mergeable (SArray a b) # 

Methods

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

select :: (SymWord b, Num b) => [SArray a b] -> SArray a b -> SBV b -> SArray a b #

EqSymbolic (SArray a b) # 

Methods

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

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

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

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

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

sbvToSW :: State -> SBV a -> IO SW #

Convert a symbolic value to a symbolic-word

sbvToSymSW :: SBV a -> Symbolic SW #

Convert a symbolic value to an SW, inside the Symbolic monad

forceSWArg :: SW -> IO () #

Forcing an argument; this is a necessary evil to make sure all the arguments to an uninterpreted function are evaluated before called; the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's

data SBVExpr #

A symbolic expression

Constructors

SBVApp !Op ![SW] 

newExpr :: State -> Kind -> SBVExpr -> IO SW #

Create a new expression; hash-cons as necessary

cache :: (State -> IO a) -> Cached a #

Cache a state-based computation

data Cached a #

We implement a peculiar caching mechanism, applicable to the use case in implementation of SBV's. Whenever we do a state based computation, we do not want to keep on evaluating it in the then-current state. That will produce essentially a semantically equivalent value. Thus, we want to run it only once, and reuse that result, capturing the sharing at the Haskell level. This is similar to the "type-safe observable sharing" work, but also takes into the account of how symbolic simulation executes.

See Andy Gill's type-safe obervable sharing trick for the inspiration behind this technique: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09

Note that this is *not* a general memo utility!

Instances

NFData (Cached a) # 

Methods

rnf :: Cached a -> () #

uncache :: Cached SW -> State -> IO SW #

Uncache a previously cached computation

uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex #

Uncache, retrieving array indexes

class HasKind a where #

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf. This class can be automatically derived for data-types that have a Data instance; this is useful for creating uninterpreted sorts.

Methods

kindOf :: a -> Kind #

hasSign :: a -> Bool #

intSizeOf :: a -> Int #

isBoolean :: a -> Bool #

isBounded :: a -> Bool #

isReal :: a -> Bool #

isFloat :: a -> Bool #

isDouble :: a -> Bool #

isInteger :: a -> Bool #

isUninterpreted :: a -> Bool #

showType :: a -> String #

kindOf :: (Read a, Data a) => a -> Kind #

Instances

HasKind Bool # 
HasKind Double # 
HasKind Float # 
HasKind Int8 # 
HasKind Int16 # 
HasKind Int32 # 
HasKind Int64 # 
HasKind Integer # 
HasKind Word8 # 
HasKind Word16 # 
HasKind Word32 # 
HasKind Word64 # 
HasKind AlgReal # 
HasKind Kind # 
HasKind ExtCW #

Kind instance for Extended CW

HasKind GeneralizedCW #

Kind instance for generalized CW

HasKind CW #

Kind instance for CW

HasKind RoundingMode #

RoundingMode kind

HasKind SVal # 
HasKind SW # 
HasKind E # 
HasKind Word4 #

HasKind instance; simply returning the underlying kind for the type

HasKind Color # 
HasKind Nationality # 
HasKind Beverage # 
HasKind Pet # 
HasKind Sport # 
HasKind U2Member # 
HasKind Location # 
HasKind Day # 
HasKind BinOp # 
HasKind UnOp # 
HasKind B # 
HasKind Q # 
HasKind L #

Similarly, HasKinds default implementation is sufficient.

HasKind (SBV a) # 

Methods

kindOf :: SBV a -> Kind #

hasSign :: SBV a -> Bool #

intSizeOf :: SBV a -> Int #

isBoolean :: SBV a -> Bool #

isBounded :: SBV a -> Bool #

isReal :: SBV a -> Bool #

isFloat :: SBV a -> Bool #

isDouble :: SBV a -> Bool #

isInteger :: SBV a -> Bool #

isUninterpreted :: SBV a -> Bool #

showType :: SBV a -> String #

data Op #

Symbolic operations

Instances

Eq Op # 

Methods

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

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

Ord Op # 

Methods

compare :: Op -> Op -> Ordering #

(<) :: Op -> Op -> Bool #

(<=) :: Op -> Op -> Bool #

(>) :: Op -> Op -> Bool #

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

max :: Op -> Op -> Op #

min :: Op -> Op -> Op #

Show Op # 

Methods

showsPrec :: Int -> Op -> ShowS #

show :: Op -> String #

showList :: [Op] -> ShowS #

data PBOp #

Pseudo-boolean operations

Constructors

PB_AtMost Int

At most k

PB_AtLeast Int

At least k

PB_Exactly Int

Exactly k

PB_Le [Int] Int

At most k, with coefficients given. Generalizes PB_AtMost

PB_Ge [Int] Int

At least k, with coefficients given. Generalizes PB_AtLeast

PB_Eq [Int] Int

Exactly k, with coefficients given. Generalized PB_Exactly

Instances

Eq PBOp # 

Methods

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

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

Ord PBOp # 

Methods

compare :: PBOp -> PBOp -> Ordering #

(<) :: PBOp -> PBOp -> Bool #

(<=) :: PBOp -> PBOp -> Bool #

(>) :: PBOp -> PBOp -> Bool #

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

max :: PBOp -> PBOp -> PBOp #

min :: PBOp -> PBOp -> PBOp #

Show PBOp # 

Methods

showsPrec :: Int -> PBOp -> ShowS #

show :: PBOp -> String #

showList :: [PBOp] -> ShowS #

type NamedSymVar = (SW, String) #

NamedSymVar pairs symbolic words and user given/automatically generated names

getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int #

Create a new table; hash-cons as necessary

newtype SBVPgm #

A program is a sequence of assignments

Constructors

SBVPgm 

Instances

NFData SBVPgm # 

Methods

rnf :: SBVPgm -> () #

data Symbolic a #

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

Instances

Monad Symbolic # 

Methods

(>>=) :: Symbolic a -> (a -> Symbolic b) -> Symbolic b #

(>>) :: Symbolic a -> Symbolic b -> Symbolic b #

return :: a -> Symbolic a #

fail :: String -> Symbolic a #

Functor Symbolic # 

Methods

fmap :: (a -> b) -> Symbolic a -> Symbolic b #

(<$) :: a -> Symbolic b -> Symbolic a #

Applicative Symbolic # 

Methods

pure :: a -> Symbolic a #

(<*>) :: Symbolic (a -> b) -> Symbolic a -> Symbolic b #

(*>) :: Symbolic a -> Symbolic b -> Symbolic b #

(<*) :: Symbolic a -> Symbolic b -> Symbolic a #

MonadIO Symbolic # 

Methods

liftIO :: IO a -> Symbolic a #

Provable Predicate # 
MonadReader State Symbolic # 

Methods

ask :: Symbolic State #

local :: (State -> State) -> Symbolic a -> Symbolic a #

reader :: (State -> a) -> Symbolic a #

NFData a => SExecutable (Symbolic a) # 

runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result) #

Run a symbolic computation, and return a extra value paired up with the Result

data State #

Return and clean and incState

The state of the symbolic interpreter

Instances

NFData State # 

Methods

rnf :: State -> () #

MonadReader State Symbolic # 

Methods

ask :: Symbolic State #

local :: (State -> State) -> Symbolic a -> Symbolic a #

reader :: (State -> a) -> Symbolic a #

MonadState State Query # 

Methods

get :: Query State #

put :: State -> Query () #

state :: (State -> (a, State)) -> Query a #

getPathCondition :: State -> SBool #

Get the current path condition

extendPathCondition :: State -> (SBool -> SBool) -> State #

Extend the path condition with the given test value.

inSMTMode :: State -> IO Bool #

Are we running in proof mode?

data SBVRunMode #

Different means of running a symbolic piece of code

Constructors

SMTMode IStage Bool SMTConfig

In regular mode, with a stage. Bool is True if this is SAT.

CodeGen

Code generation mode.

Concrete

Concrete simulation mode.

data Kind #

Kind of symbolic value

Instances

Eq Kind #

We want to equate user-sorts only by name

Methods

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

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

Ord Kind #

We want to order user-sorts only by name

Methods

compare :: Kind -> Kind -> Ordering #

(<) :: Kind -> Kind -> Bool #

(<=) :: Kind -> Kind -> Bool #

(>) :: Kind -> Kind -> Bool #

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

max :: Kind -> Kind -> Kind #

min :: Kind -> Kind -> Kind #

Show Kind # 

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

HasKind Kind # 

class Outputtable a where #

A class representing what can be returned from a symbolic computation.

Minimal complete definition

output

Methods

output :: a -> Symbolic a #

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

Instances

Outputtable () # 

Methods

output :: () -> Symbolic () #

Outputtable a => Outputtable [a] # 

Methods

output :: [a] -> Symbolic [a] #

Outputtable (SBV a) # 

Methods

output :: SBV a -> Symbolic (SBV a) #

(Outputtable a, Outputtable b) => Outputtable (a, b) # 

Methods

output :: (a, b) -> Symbolic (a, b) #

(Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) # 

Methods

output :: (a, b, c) -> Symbolic (a, b, c) #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) # 

Methods

output :: (a, b, c, d) -> Symbolic (a, b, c, d) #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) # 

Methods

output :: (a, b, c, d, e) -> Symbolic (a, b, c, d, e) #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) # 

Methods

output :: (a, b, c, d, e, f) -> Symbolic (a, b, c, d, e, f) #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) # 

Methods

output :: (a, b, c, d, e, f, g) -> Symbolic (a, b, c, d, e, f, g) #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) # 

Methods

output :: (a, b, c, d, e, f, g, h) -> Symbolic (a, b, c, d, e, f, g, h) #

data Result #

Result of running a symbolic computation

Constructors

Result 

Fields

Instances

Show Result # 
NFData Result # 

Methods

rnf :: Result -> () #

class SolverContext m where #

Actions we can do in a context: Either at problem description time or while we are dynamically querying. Symbolic and Query are two instances of this class. Note that we use this mechanism internally and do not export it from SBV.

Minimal complete definition

constrain, namedConstraint, setOption

Methods

constrain :: SBool -> m () #

Add a constraint, any satisfying instance must satisfy this condition

namedConstraint :: String -> SBool -> m () #

Add a named constraint. The name is used in unsat-core extraction.

setInfo :: String -> [String] -> m () #

Set info. Example: setInfo ":status" ["unsat"].

setOption :: SMTOption -> m () #

Set an option.

setLogic :: Logic -> m () #

Set the logic.

setTimeOut :: Integer -> m () #

Set a solver time-out value, in milli-seconds. This function essentially translates to the SMTLib call (set-info :timeout val), and your backend solver may or may not support it! The amount given is in milliseconds. Also see the function timeOut for finer level control of time-outs, directly from SBV.

internalVariable :: State -> Kind -> IO SW #

Create an internal variable, which acts as an input but isn't visible to the user. Such variables are existentially quantified in a SAT context, and universally quantified in a proof context.

internalConstraint :: State -> Maybe String -> SVal -> IO () #

Require a boolean condition to be true in the state. Only used for internal purposes.

isCodeGenMode :: State -> IO Bool #

Is this a CodeGen run? (i.e., generating code)

newtype SBVType #

A simple type for SBV computations, used mainly for uninterpreted constants. We keep track of the signedness/size of the arguments. A non-function will have just one entry in the list.

Constructors

SBVType [Kind] 

newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () #

Create a new uninterpreted symbol, possibly with user given code

addAxiom :: String -> [String] -> Symbolic () #

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

data Quantifier #

Quantifiers: forall or exists. Note that we allow arbitrary nestings.

Constructors

ALL 
EX 

Instances

needsExistentials :: [Quantifier] -> Bool #

Are there any existential quantifiers?

data SMTLibPgm #

Representation of an SMT-Lib program. In between pre and post goes the refuted models

Instances

data SMTLibVersion #

Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.

Constructors

SMTLib2 

smtLibVersionExtension :: SMTLibVersion -> String #

The extension associated with the version

smtLibReservedNames :: [String] #

Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course there's no guarantee it'll stay that way.

data SolverCapabilities #

Translation tricks needed for specific capabilities afforded by each solver

Constructors

SolverCapabilities 

Fields

extractSymbolicSimulationState :: State -> IO Result #

Grab the program from a running symbolic simulation state.

data SMTScript #

A script, to be passed to the solver.

Constructors

SMTScript 

Fields

Instances

NFData SMTScript # 

Methods

rnf :: SMTScript -> () #

data Solver #

Solvers that SBV is aware of

Constructors

Z3 
Yices 
Boolector 
CVC4 
MathSAT 
ABC 

data SMTSolver #

An SMT solver

Constructors

SMTSolver 

Fields

data SMTResult #

The result of an SMT solver call. Each constructor is tagged with the SMTConfig that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

Unsatisfiable SMTConfig

Unsatisfiable

Satisfiable SMTConfig SMTModel

Satisfiable with model

SatExtField SMTConfig SMTModel

Prover returned a model, but in an extension field containing Infinite/epsilon

Unknown SMTConfig String

Prover returned unknown, with the given reason

ProofError SMTConfig [String]

Prover errored out

data SMTModel #

A model, as returned by a solver

Constructors

SMTModel 

Fields

Instances

data SMTConfig #

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.

Constructors

SMTConfig 

Fields

Instances

NFData SMTConfig # 

Methods

rnf :: SMTConfig -> () #

declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Symbolic (SArray a b) #

Declare a new symbolic array, with a potential initial value

declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b) #

Declare a new functional symbolic array. Note that a read from an uninitialized cell will result in an error.

data OptimizeStyle #

Style of optimization. Note that in the pareto case the user is allowed to specify a max number of fronts to query the solver for, since there might potentially be an infinite number of them and there is no way to know exactly how many ahead of time. If Nothing is given, SBV will possibly loop forever if the number is really infinite.

Constructors

Lexicographic

Objectives are optimized in the order given, earlier objectives have higher priority. This is the default.

Independent

Each objective is optimized independently.

Pareto (Maybe Int)

Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.

data Penalty #

Penalty for a soft-assertion. The default penalty is 1, with all soft-assertions belonging to the same objective goal. A positive weight and an optional group can be provided by using the Penalty constructor.

Constructors

DefaultPenalty

Default: Penalty of 1 and no group attached

Penalty Rational (Maybe String)

Penalty with a weight and an optional group

Instances

Show Penalty # 
NFData Penalty # 

Methods

rnf :: Penalty -> () #

data Objective a #

Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.

Constructors

Minimize String a

Minimize this metric

Maximize String a

Maximize this metric

AssertSoft String a Penalty

A soft assertion, with an associated penalty

Instances

Functor Objective # 

Methods

fmap :: (a -> b) -> Objective a -> Objective b #

(<$) :: a -> Objective b -> Objective a #

Show a => Show (Objective a) # 
NFData a => NFData (Objective a) # 

Methods

rnf :: Objective a -> () #

data QueryState #

The state we keep track of as we interact with the solver

newtype Query a #

A query is a user-guided mechanism to directly communicate and extract results from the solver.

Constructors

Query (StateT State IO a) 

Instances

Monad Query # 

Methods

(>>=) :: Query a -> (a -> Query b) -> Query b #

(>>) :: Query a -> Query b -> Query b #

return :: a -> Query a #

fail :: String -> Query a #

Functor Query # 

Methods

fmap :: (a -> b) -> Query a -> Query b #

(<$) :: a -> Query b -> Query a #

Applicative Query # 

Methods

pure :: a -> Query a #

(<*>) :: Query (a -> b) -> Query a -> Query b #

(*>) :: Query a -> Query b -> Query b #

(<*) :: Query a -> Query b -> Query a #

MonadIO Query # 

Methods

liftIO :: IO a -> Query a #

MonadState State Query # 

Methods

get :: Query State #

put :: State -> Query () #

state :: (State -> (a, State)) -> Query a #

newtype SMTProblem #

Internal representation of a symbolic simulation result

Constructors

SMTProblem

SMTLib representation, given the config

Operations useful for instantiating SBV type classes

genLiteral :: Integral a => Kind -> a -> SBV b #

Generate a finite constant bitvector

genFromCW :: Integral a => CW -> a #

Convert a constant to an integral value

data CW #

CW represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the FromBits class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW 

Fields

Instances

Eq CW # 

Methods

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

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

Ord CW # 

Methods

compare :: CW -> CW -> Ordering #

(<) :: CW -> CW -> Bool #

(<=) :: CW -> CW -> Bool #

(>) :: CW -> CW -> Bool #

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

max :: CW -> CW -> CW #

min :: CW -> CW -> CW #

Show CW #

Show instance for CW.

Methods

showsPrec :: Int -> CW -> ShowS #

show :: CW -> String #

showList :: [CW] -> ShowS #

HasKind CW #

Kind instance for CW

PrettyNum CW # 

Methods

hexS :: CW -> String #

binS :: CW -> String #

hex :: CW -> String #

bin :: CW -> String #

SatModel CW #

CW as extracted from a model; trivial definition

Methods

parseCWs :: [CW] -> Maybe (CW, [CW]) #

cvtModel :: (CW -> Maybe b) -> Maybe (CW, [CW]) -> Maybe (b, [CW]) #

SDivisible CW # 

Methods

sQuotRem :: CW -> CW -> (CW, CW) #

sDivMod :: CW -> CW -> (CW, CW) #

sQuot :: CW -> CW -> CW #

sRem :: CW -> CW -> CW #

sDiv :: CW -> CW -> CW #

sMod :: CW -> CW -> CW #

genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #

Generically make a symbolic var

checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a #

Perform a sanity check that we should receive precisely the same number of bits as required by the resulting type. The input is little-endian

genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) #

Parse a signed/sized value from a sequence of CWs

showModel :: SMTConfig -> SMTModel -> String #

Show a model in human readable form. Ignore bindings to those variables that start with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes

data SMTModel #

A model, as returned by a solver

Constructors

SMTModel 

Fields

Instances

liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) #

Lift QRem to symbolic words. Division by 0 is defined s.t. x/0 = 0; which holds even when x is 0 itself.

liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) #

Lift DMod to symbolic words. Division by 0 is defined s.t. x/0 = 0; which holds even when x is 0 itself. Essentially, this is conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)

Compilation to C, extras

compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle #

Lower level version of compileToC, producing a CgPgmBundle

compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle #

Lower level version of compileToCLib, producing a CgPgmBundle

Code generation primitives

The codegen monad

newtype SBVCodeGen a #

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

Constructors

SBVCodeGen (StateT CgState Symbolic a) 

Specifying inputs, SBV variants

cgInput :: SymWord a => String -> SBVCodeGen (SBV a) #

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] #

Creates an array input in the generated code.

cgOutput :: String -> SBV a -> SBVCodeGen () #

Creates an atomic output in the generated code.

cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen () #

Creates an array output in the generated code.

cgReturn :: SBV a -> SBVCodeGen () #

Creates a returned (unnamed) value in the generated code.

cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen () #

Creates a returned (unnamed) array value in the generated code.

Specifying inputs, SVal variants

svCgInput :: Kind -> String -> SBVCodeGen SVal #

Creates an atomic input in the generated code.

svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] #

Creates an array input in the generated code.

svCgOutput :: String -> SVal -> SBVCodeGen () #

Creates an atomic output in the generated code.

svCgOutputArr :: String -> [SVal] -> SBVCodeGen () #

Creates an array output in the generated code.

svCgReturn :: SVal -> SBVCodeGen () #

Creates a returned (unnamed) value in the generated code.

svCgReturnArr :: [SVal] -> SBVCodeGen () #

Creates a returned (unnamed) array value in the generated code.

Settings

cgPerformRTCs :: Bool -> SBVCodeGen () #

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: False.

cgSetDriverValues :: [Integer] -> SBVCodeGen () #

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgAddPrototype :: [String] -> SBVCodeGen () #

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () #

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () #

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

cgIgnoreSAssert :: Bool -> SBVCodeGen () #

Ignore assertions (those generated by sAssert calls) in the generated C code

cgIntegerSize :: Int -> SBVCodeGen () #

Sets number of bits to be used for representing the SInteger type in the generated C code. The argument must be one of 8, 16, 32, or 64. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () #

Sets the C type to be used for representing the SReal type in the generated C code. The setting can be one of C's "float", "double", or "long double", types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType #

Possible mappings for the SReal type when translated to C. Used in conjunction with the function cgSRealType. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat
float
CgDouble
double
CgLongDouble
long double

Infrastructure

class CgTarget a where #

Abstract over code generation for different languages

Minimal complete definition

targetName, translate

data CgConfig #

Options for code-generation.

Constructors

CgConfig 

Fields

data CgState #

Code-generation state

data CgPgmBundle #

Representation of a collection of generated programs.

data CgPgmKind #

Different kinds of "files" we can produce. Currently this is quite C specific.

data CgVal #

Abstraction of target language values

Constructors

CgAtomic SW 
CgArray [SW] 

defaultCgConfig :: CgConfig #

Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.

initCgState :: CgState #

Initial configuration for code-generation

isCgDriver :: CgPgmKind -> Bool #

Is this a driver program?

isCgMakefile :: CgPgmKind -> Bool #

Is this a make file?

Generating collateral

cgGenerateDriver :: Bool -> SBVCodeGen () #

Should we generate a driver program? Default: True. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See compileToCLib.)

cgGenerateMakefile :: Bool -> SBVCodeGen () #

Should we generate a Makefile? Default: True.

codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle #

Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection of makefiles, source code, headers, etc.

renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO () #

Render a code-gen bundle to a directory or to stdout

Various math utilities around floats

fpRound0 :: (RealFloat a, Integral b) => a -> b #

A variant of round; except defaulting to 0 when fed NaN or Infinity

fpRatio0 :: RealFloat a => a -> Rational #

A variant of toRational; except defaulting to 0 when fed NaN or Infinity

fpMaxH :: RealFloat a => a -> a -> a #

The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with Haskell's; and also it does not agree with what the hardware does. Sigh.. See: https://ghc.haskell.org/trac/ghc/ticket/10378 https://github.com/Z3Prover/z3/issues/68 So, we codify here what the Z3 (SMTLib) is implementing for fpMax. The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic

fpMinH :: RealFloat a => a -> a -> a #

SMTLib compliant definition for fpMin. See the comments for fpMax.

fp2fp :: (RealFloat a, RealFloat b) => a -> b #

Convert double to float and back. Essentially fromRational . toRational except careful on NaN, Infinities, and -0.

fpRemH :: RealFloat a => a -> a -> a #

Compute the "floating-point" remainder function, the float/double value that remains from the division of x and y. There are strict rules around 0's, Infinities, and NaN's as coded below, See http://smt-lib.org/papers/BTRW14.pdf, towards the end of section 4.c.

fpRoundToIntegralH :: RealFloat a => a -> a #

Convert a float to the nearest integral representable in that type

fpIsEqualObjectH :: RealFloat a => a -> a -> Bool #

Check that two floats are the exact same values, i.e., +0/-0 does not compare equal, and NaN's compare equal to themselves.

fpIsNormalizedH :: RealFloat a => a -> Bool #

Check if a number is "normal." Note that +0/-0 is not considered a normal-number and also this is not simply the negation of isDenormalized!

Pretty number printing

class PrettyNum a where #

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: hexS and binS

Minimal complete definition

hexS, binS, hex, bin

Methods

hexS :: a -> String #

Show a number in hexadecimal (starting with 0x and type.)

binS :: a -> String #

Show a number in binary (starting with 0b and type.)

hex :: a -> String #

Show a number in hex, without prefix, or types.

bin :: a -> String #

Show a number in bin, without prefix, or types.

Instances

PrettyNum Bool # 

Methods

hexS :: Bool -> String #

binS :: Bool -> String #

hex :: Bool -> String #

bin :: Bool -> String #

PrettyNum Int8 # 

Methods

hexS :: Int8 -> String #

binS :: Int8 -> String #

hex :: Int8 -> String #

bin :: Int8 -> String #

PrettyNum Int16 # 

Methods

hexS :: Int16 -> String #

binS :: Int16 -> String #

hex :: Int16 -> String #

bin :: Int16 -> String #

PrettyNum Int32 # 

Methods

hexS :: Int32 -> String #

binS :: Int32 -> String #

hex :: Int32 -> String #

bin :: Int32 -> String #

PrettyNum Int64 # 

Methods

hexS :: Int64 -> String #

binS :: Int64 -> String #

hex :: Int64 -> String #

bin :: Int64 -> String #

PrettyNum Integer # 
PrettyNum Word8 # 

Methods

hexS :: Word8 -> String #

binS :: Word8 -> String #

hex :: Word8 -> String #

bin :: Word8 -> String #

PrettyNum Word16 # 
PrettyNum Word32 # 
PrettyNum Word64 # 
PrettyNum CW # 

Methods

hexS :: CW -> String #

binS :: CW -> String #

hex :: CW -> String #

bin :: CW -> String #

(SymWord a, PrettyNum a) => PrettyNum (SBV a) # 

Methods

hexS :: SBV a -> String #

binS :: SBV a -> String #

hex :: SBV a -> String #

bin :: SBV a -> String #

readBin :: Num a => String -> a #

A more convenient interface for reading binary numbers, also supports negative numbers

shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String #

Show as a hexadecimal value. First bool controls whether type info is printed while the second boolean controls wether 0x prefix is printed. The tuple is the signedness and the bit-length of the input. The length of the string will not depend on the value, but rather the bit-length.

shexI :: Bool -> Bool -> Integer -> String #

Show as a hexadecimal value, integer version. Almost the same as shex above except we don't have a bit-length so the length of the string will depend on the actual value.

sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String #

Similar to shex; except in binary.

sbinI :: Bool -> Bool -> Integer -> String #

Similar to shexI; except in binary.

showCFloat :: Float -> String #

A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.

showCDouble :: Double -> String #

A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.

showHFloat :: Float -> String #

A version of show for floats that generates correct Haskell literals for nan/infinite

showHDouble :: Double -> String #

A version of show for doubles that generates correct Haskell literals for nan/infinite

showSMTFloat :: RoundingMode -> Float -> String #

A version of show for floats that generates correct SMTLib literals using the rounding mode

showSMTDouble :: RoundingMode -> Double -> String #

A version of show for doubles that generates correct SMTLib literals using the rounding mode

smtRoundingMode :: RoundingMode -> String #

Convert a rounding mode to the format SMT-Lib2 understands.

cwToSMTLib :: RoundingMode -> CW -> String #

Convert a CW to an SMTLib2 compliant value

mkSkolemZero :: RoundingMode -> Kind -> String #

Create a skolem 0 for the kind

Timing computations

data Timing #

Specify how to save timing information, if at all.

showTDiff :: NominalDiffTime -> String #

Show NominalDiffTime in human readable form. NominalDiffTime is essentially picoseconds (10^-12 seconds). We show it so that it's represented at the day:hour:minute:second.XXX granularity.

Coordinating with the solver

In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this should be avoided if at all possible. Users should prefer the provided API. If you do find yourself needing send and ask directly, please get in touch to see if SBV can support a typed API for your use case. Similarly, the function retrieveResponseFromSolver might occasionally be necessary to clean-up the communication buffer. We would like to hear if you do need these functions regularly so we can provide better support.

sendStringToSolver :: String -> Query () #

Send an arbitrary string to the solver in a query. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!

sendRequestToSolver :: String -> Query String #

Send an arbitrary string to the solver in a query, and return a response. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV.

retrieveResponseFromSolver :: String -> Maybe Int -> Query [String] #

Retrieve multiple responses from the solver, until it responds with a user given tag that we shall arrange for internally. The optional timeout is in milliseconds. If the time-out is exceeded, then we will raise an error. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!