Data.SBV.Dynamic

Dynamically typed low-level API to the SBV library, for users who want to generate symbolic values at run-time. Note that with this API it is possible to create terms that are not type correct; use at your own risk!

Programming with symbolic values

Symbolic types

Abstract symbolic value type

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.

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

Show instance for SVal. Not particularly "desirable", but will do if needed NB. We do not show the type info on constant KBool values, since there's no implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)

Methods

showsPrec :: Int -> SVal -> ShowS

show :: SVal -> String

showList :: [SVal] -> ShowS

NFData SVal

Methods

rnf :: SVal -> ()

HasKind SVal

Methods

kindOf :: SVal -> Kind

hasSign :: SVal -> Bool

intSizeOf :: SVal -> Int

isBoolean :: SVal -> Bool

isBounded :: SVal -> Bool

isReal :: SVal -> Bool

isFloat :: SVal -> Bool

isDouble :: SVal -> Bool

isInteger :: SVal -> Bool

isUninterpreted :: SVal -> Bool

showType :: SVal -> String

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

Methods

kindOf :: Bool -> Kind

hasSign :: Bool -> Bool

intSizeOf :: Bool -> Int

isBoolean :: Bool -> Bool

isBounded :: Bool -> Bool

isReal :: Bool -> Bool

isFloat :: Bool -> Bool

isDouble :: Bool -> Bool

isInteger :: Bool -> Bool

isUninterpreted :: Bool -> Bool

showType :: Bool -> String

HasKind Double

Methods

kindOf :: Double -> Kind

hasSign :: Double -> Bool

intSizeOf :: Double -> Int

isBoolean :: Double -> Bool

isBounded :: Double -> Bool

isReal :: Double -> Bool

isFloat :: Double -> Bool

isDouble :: Double -> Bool

isInteger :: Double -> Bool

isUninterpreted :: Double -> Bool

showType :: Double -> String

HasKind Float

Methods

kindOf :: Float -> Kind

hasSign :: Float -> Bool

intSizeOf :: Float -> Int

isBoolean :: Float -> Bool

isBounded :: Float -> Bool

isReal :: Float -> Bool

isFloat :: Float -> Bool

isDouble :: Float -> Bool

isInteger :: Float -> Bool

isUninterpreted :: Float -> Bool

showType :: Float -> String

HasKind Int8

Methods

kindOf :: Int8 -> Kind

hasSign :: Int8 -> Bool

intSizeOf :: Int8 -> Int

isBoolean :: Int8 -> Bool

isBounded :: Int8 -> Bool

isReal :: Int8 -> Bool

isFloat :: Int8 -> Bool

isDouble :: Int8 -> Bool

isInteger :: Int8 -> Bool

isUninterpreted :: Int8 -> Bool

showType :: Int8 -> String

HasKind Int16

Methods

kindOf :: Int16 -> Kind

hasSign :: Int16 -> Bool

intSizeOf :: Int16 -> Int

isBoolean :: Int16 -> Bool

isBounded :: Int16 -> Bool

isReal :: Int16 -> Bool

isFloat :: Int16 -> Bool

isDouble :: Int16 -> Bool

isInteger :: Int16 -> Bool

isUninterpreted :: Int16 -> Bool

showType :: Int16 -> String

HasKind Int32

Methods

kindOf :: Int32 -> Kind

hasSign :: Int32 -> Bool

intSizeOf :: Int32 -> Int

isBoolean :: Int32 -> Bool

isBounded :: Int32 -> Bool

isReal :: Int32 -> Bool

isFloat :: Int32 -> Bool

isDouble :: Int32 -> Bool

isInteger :: Int32 -> Bool

isUninterpreted :: Int32 -> Bool

showType :: Int32 -> String

HasKind Int64

Methods

kindOf :: Int64 -> Kind

hasSign :: Int64 -> Bool

intSizeOf :: Int64 -> Int

isBoolean :: Int64 -> Bool

isBounded :: Int64 -> Bool

isReal :: Int64 -> Bool

isFloat :: Int64 -> Bool

isDouble :: Int64 -> Bool

isInteger :: Int64 -> Bool

isUninterpreted :: Int64 -> Bool

showType :: Int64 -> String

HasKind Integer

Methods

kindOf :: Integer -> Kind

hasSign :: Integer -> Bool

intSizeOf :: Integer -> Int

isBoolean :: Integer -> Bool

isBounded :: Integer -> Bool

isReal :: Integer -> Bool

isFloat :: Integer -> Bool

isDouble :: Integer -> Bool

isInteger :: Integer -> Bool

isUninterpreted :: Integer -> Bool

showType :: Integer -> String

HasKind Word8

Methods

kindOf :: Word8 -> Kind

hasSign :: Word8 -> Bool

intSizeOf :: Word8 -> Int

isBoolean :: Word8 -> Bool

isBounded :: Word8 -> Bool

isReal :: Word8 -> Bool

isFloat :: Word8 -> Bool

isDouble :: Word8 -> Bool

isInteger :: Word8 -> Bool

isUninterpreted :: Word8 -> Bool

showType :: Word8 -> String

HasKind Word16

Methods

kindOf :: Word16 -> Kind

hasSign :: Word16 -> Bool

intSizeOf :: Word16 -> Int

isBoolean :: Word16 -> Bool

isBounded :: Word16 -> Bool

isReal :: Word16 -> Bool

isFloat :: Word16 -> Bool

isDouble :: Word16 -> Bool

isInteger :: Word16 -> Bool

isUninterpreted :: Word16 -> Bool

showType :: Word16 -> String

HasKind Word32

Methods

kindOf :: Word32 -> Kind

hasSign :: Word32 -> Bool

intSizeOf :: Word32 -> Int

isBoolean :: Word32 -> Bool

isBounded :: Word32 -> Bool

isReal :: Word32 -> Bool

isFloat :: Word32 -> Bool

isDouble :: Word32 -> Bool

isInteger :: Word32 -> Bool

isUninterpreted :: Word32 -> Bool

showType :: Word32 -> String

HasKind Word64

Methods

kindOf :: Word64 -> Kind

hasSign :: Word64 -> Bool

intSizeOf :: Word64 -> Int

isBoolean :: Word64 -> Bool

isBounded :: Word64 -> Bool

isReal :: Word64 -> Bool

isFloat :: Word64 -> Bool

isDouble :: Word64 -> Bool

isInteger :: Word64 -> Bool

isUninterpreted :: Word64 -> Bool

showType :: Word64 -> String

HasKind AlgReal

Methods

kindOf :: AlgReal -> Kind

hasSign :: AlgReal -> Bool

intSizeOf :: AlgReal -> Int

isBoolean :: AlgReal -> Bool

isBounded :: AlgReal -> Bool

isReal :: AlgReal -> Bool

isFloat :: AlgReal -> Bool

isDouble :: AlgReal -> Bool

isInteger :: AlgReal -> Bool

isUninterpreted :: AlgReal -> Bool

showType :: AlgReal -> String

HasKind Kind

Methods

kindOf :: Kind -> Kind

hasSign :: Kind -> Bool

intSizeOf :: Kind -> Int

isBoolean :: Kind -> Bool

isBounded :: Kind -> Bool

isReal :: Kind -> Bool

isFloat :: Kind -> Bool

isDouble :: Kind -> Bool

isInteger :: Kind -> Bool

isUninterpreted :: Kind -> Bool

showType :: Kind -> String

HasKind ExtCW

Kind instance for Extended CW

Methods

kindOf :: ExtCW -> Kind

hasSign :: ExtCW -> Bool

intSizeOf :: ExtCW -> Int

isBoolean :: ExtCW -> Bool

isBounded :: ExtCW -> Bool

isReal :: ExtCW -> Bool

isFloat :: ExtCW -> Bool

isDouble :: ExtCW -> Bool

isInteger :: ExtCW -> Bool

isUninterpreted :: ExtCW -> Bool

showType :: ExtCW -> String

HasKind GeneralizedCW

Kind instance for generalized CW

Methods

kindOf :: GeneralizedCW -> Kind

hasSign :: GeneralizedCW -> Bool

intSizeOf :: GeneralizedCW -> Int

isBoolean :: GeneralizedCW -> Bool

isBounded :: GeneralizedCW -> Bool

isReal :: GeneralizedCW -> Bool

isFloat :: GeneralizedCW -> Bool

isDouble :: GeneralizedCW -> Bool

isInteger :: GeneralizedCW -> Bool

isUninterpreted :: GeneralizedCW -> Bool

showType :: GeneralizedCW -> String

HasKind CW

Kind instance for CW

Methods

kindOf :: CW -> Kind

hasSign :: CW -> Bool

intSizeOf :: CW -> Int

isBoolean :: CW -> Bool

isBounded :: CW -> Bool

isReal :: CW -> Bool

isFloat :: CW -> Bool

isDouble :: CW -> Bool

isInteger :: CW -> Bool

isUninterpreted :: CW -> Bool

showType :: CW -> String

HasKind RoundingMode

RoundingMode kind

Methods

kindOf :: RoundingMode -> Kind

hasSign :: RoundingMode -> Bool

intSizeOf :: RoundingMode -> Int

isBoolean :: RoundingMode -> Bool

isBounded :: RoundingMode -> Bool

isReal :: RoundingMode -> Bool

isFloat :: RoundingMode -> Bool

isDouble :: RoundingMode -> Bool

isInteger :: RoundingMode -> Bool

isUninterpreted :: RoundingMode -> Bool

showType :: RoundingMode -> String

HasKind SVal

Methods

kindOf :: SVal -> Kind

hasSign :: SVal -> Bool

intSizeOf :: SVal -> Int

isBoolean :: SVal -> Bool

isBounded :: SVal -> Bool

isReal :: SVal -> Bool

isFloat :: SVal -> Bool

isDouble :: SVal -> Bool

isInteger :: SVal -> Bool

isUninterpreted :: SVal -> Bool

showType :: SVal -> String

HasKind SW

Methods

kindOf :: SW -> Kind

hasSign :: SW -> Bool

intSizeOf :: SW -> Int

isBoolean :: SW -> Bool

isBounded :: SW -> Bool

isReal :: SW -> Bool

isFloat :: SW -> Bool

isDouble :: SW -> Bool

isInteger :: SW -> Bool

isUninterpreted :: SW -> Bool

showType :: SW -> String

HasKind E

Methods

kindOf :: E -> Kind

hasSign :: E -> Bool

intSizeOf :: E -> Int

isBoolean :: E -> Bool

isBounded :: E -> Bool

isReal :: E -> Bool

isFloat :: E -> Bool

isDouble :: E -> Bool

isInteger :: E -> Bool

isUninterpreted :: E -> Bool

showType :: E -> String

HasKind Word4

HasKind instance; simply returning the underlying kind for the type

Methods

kindOf :: Word4 -> Kind

hasSign :: Word4 -> Bool

intSizeOf :: Word4 -> Int

isBoolean :: Word4 -> Bool

isBounded :: Word4 -> Bool

isReal :: Word4 -> Bool

isFloat :: Word4 -> Bool

isDouble :: Word4 -> Bool

isInteger :: Word4 -> Bool

isUninterpreted :: Word4 -> Bool

showType :: Word4 -> String

HasKind Sport

Methods

kindOf :: Sport -> Kind

hasSign :: Sport -> Bool

intSizeOf :: Sport -> Int

isBoolean :: Sport -> Bool

isBounded :: Sport -> Bool

isReal :: Sport -> Bool

isFloat :: Sport -> Bool

isDouble :: Sport -> Bool

isInteger :: Sport -> Bool

isUninterpreted :: Sport -> Bool

showType :: Sport -> String

HasKind Pet

Methods

kindOf :: Pet -> Kind

hasSign :: Pet -> Bool

intSizeOf :: Pet -> Int

isBoolean :: Pet -> Bool

isBounded :: Pet -> Bool

isReal :: Pet -> Bool

isFloat :: Pet -> Bool

isDouble :: Pet -> Bool

isInteger :: Pet -> Bool

isUninterpreted :: Pet -> Bool

showType :: Pet -> String

HasKind Beverage

Methods

kindOf :: Beverage -> Kind

hasSign :: Beverage -> Bool

intSizeOf :: Beverage -> Int

isBoolean :: Beverage -> Bool

isBounded :: Beverage -> Bool

isReal :: Beverage -> Bool

isFloat :: Beverage -> Bool

isDouble :: Beverage -> Bool

isInteger :: Beverage -> Bool

isUninterpreted :: Beverage -> Bool

showType :: Beverage -> String

HasKind Nationality

Methods

kindOf :: Nationality -> Kind

hasSign :: Nationality -> Bool

intSizeOf :: Nationality -> Int

isBoolean :: Nationality -> Bool

isBounded :: Nationality -> Bool

isReal :: Nationality -> Bool

isFloat :: Nationality -> Bool

isDouble :: Nationality -> Bool

isInteger :: Nationality -> Bool

isUninterpreted :: Nationality -> Bool

showType :: Nationality -> String

HasKind Color

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isInteger :: Color -> Bool

isUninterpreted :: Color -> Bool

showType :: Color -> String

HasKind Location

Methods

kindOf :: Location -> Kind

hasSign :: Location -> Bool

intSizeOf :: Location -> Int

isBoolean :: Location -> Bool

isBounded :: Location -> Bool

isReal :: Location -> Bool

isFloat :: Location -> Bool

isDouble :: Location -> Bool

isInteger :: Location -> Bool

isUninterpreted :: Location -> Bool

showType :: Location -> String

HasKind U2Member

Methods

kindOf :: U2Member -> Kind

hasSign :: U2Member -> Bool

intSizeOf :: U2Member -> Int

isBoolean :: U2Member -> Bool

isBounded :: U2Member -> Bool

isReal :: U2Member -> Bool

isFloat :: U2Member -> Bool

isDouble :: U2Member -> Bool

isInteger :: U2Member -> Bool

isUninterpreted :: U2Member -> Bool

showType :: U2Member -> String

HasKind B

Methods

kindOf :: B -> Kind

hasSign :: B -> Bool

intSizeOf :: B -> Int

isBoolean :: B -> Bool

isBounded :: B -> Bool

isReal :: B -> Bool

isFloat :: B -> Bool

isDouble :: B -> Bool

isInteger :: B -> Bool

isUninterpreted :: B -> Bool

showType :: B -> String

HasKind Q

Methods

kindOf :: Q -> Kind

hasSign :: Q -> Bool

intSizeOf :: Q -> Int

isBoolean :: Q -> Bool

isBounded :: Q -> Bool

isReal :: Q -> Bool

isFloat :: Q -> Bool

isDouble :: Q -> Bool

isInteger :: Q -> Bool

isUninterpreted :: Q -> Bool

showType :: Q -> String

HasKind L

Similarly, HasKinds default implementation is sufficient.

Methods

kindOf :: L -> Kind

hasSign :: L -> Bool

intSizeOf :: L -> Int

isBoolean :: L -> Bool

isBounded :: L -> Bool

isReal :: L -> Bool

isFloat :: L -> Bool

isDouble :: L -> Bool

isInteger :: L -> Bool

isUninterpreted :: L -> Bool

showType :: L -> String

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 Kind

Kind of symbolic value

Constructors

KBool

KBounded !Bool !Int

KUnbounded

KReal

KUserSort String (Either String [String])

KFloat

KDouble

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

Methods

kindOf :: Kind -> Kind

hasSign :: Kind -> Bool

intSizeOf :: Kind -> Int

isBoolean :: Kind -> Bool

isBounded :: Kind -> Bool

isReal :: Kind -> Bool

isFloat :: Kind -> Bool

isDouble :: Kind -> Bool

isInteger :: Kind -> Bool

isUninterpreted :: Kind -> Bool

showType :: Kind -> String

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

• _cwKind :: !Kind
• cwVal :: !CWVal

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

Methods

kindOf :: CW -> Kind

hasSign :: CW -> Bool

intSizeOf :: CW -> Int

isBoolean :: CW -> Bool

isBounded :: CW -> Bool

isReal :: CW -> Bool

isFloat :: CW -> Bool

isDouble :: CW -> Bool

isInteger :: CW -> Bool

isUninterpreted :: CW -> Bool

showType :: CW -> String

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

cwToBool :: CW -> Bool

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

Arrays of symbolic values

data SArr

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 SArr values
• Typically slower as it heavily relies on SMT-solving for the array theory

readSArr :: SArr -> SVal -> SVal

Read the array element at a

resetSArr :: SArr -> SVal -> SArr

Reset all the elements of the array to the value b

writeSArr :: SArr -> SVal -> SVal -> SArr

Update the element at a to be b

mergeSArr :: SVal -> SArr -> SArr -> SArr

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

newSArr :: (Kind, Kind) -> (Int -> String) -> Maybe SVal -> Symbolic SArr

Create a named new array, with an optional initial value

eqSArr :: SArr -> SArr -> SVal

Compare two arrays for equality

Creating a symbolic variable

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

Methods

forAll_ :: Predicate -> Predicate

forAll :: [String] -> Predicate -> Predicate

forSome_ :: Predicate -> Predicate

forSome :: [String] -> Predicate -> 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)

Methods

sName_ :: Symbolic a -> Symbolic ()

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

data Quantifier

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

Constructors

ALL

EX

Instances

Eq Quantifier

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

NFData Quantifier

Methods

rnf :: Quantifier -> ()

svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic SVal

Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. If not, then we pick existential for SAT calls and universal for everything else. randomCW is used for generating random values for this variable when used for quickCheck purposes.

Operations on symbolic values

Boolean literals

svTrue :: SVal

Boolean True.

svFalse :: SVal

Boolean False.

svBool :: Bool -> SVal

Convert from a Boolean.

svAsBool :: SVal -> Maybe Bool

Extract a bool, by properly interpreting the integer stored.

Integer literals

svInteger :: Kind -> Integer -> SVal

Convert from an Integer.

svAsInteger :: SVal -> Maybe Integer

Extract an integer from a concrete value.

Float literals

svFloat :: Float -> SVal

Convert from a Float

svDouble :: Double -> SVal

Convert from a Float

Algebraic reals (only from rationals)

svReal :: Rational -> SVal

Convert from a Rational

svNumerator :: SVal -> Maybe Integer

Grab the numerator of an SReal, if available

svDenominator :: SVal -> Maybe Integer

Grab the denominator of an SReal, if available

Symbolic equality

svEqual :: SVal -> SVal -> SVal

Equality.

svNotEqual :: SVal -> SVal -> SVal

Inequality.

Constructing concrete lists

svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]

Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like [1, 5 .. 200] :: [SInt8] work just fine (end evaluate to empty list), since we see [1, 5 .. -56] in the Integer domain. Also note the explicit check for s /= f below to make sure we don't stutter and produce an infinite list.

Symbolic ordering

svLessThan :: SVal -> SVal -> SVal

Less than.

svGreaterThan :: SVal -> SVal -> SVal

Greater than.

svLessEq :: SVal -> SVal -> SVal

Less than or equal to.

svGreaterEq :: SVal -> SVal -> SVal

Greater than or equal to.

Arithmetic operations

svPlus :: SVal -> SVal -> SVal

Addition.

svTimes :: SVal -> SVal -> SVal

Multiplication.

svMinus :: SVal -> SVal -> SVal

Subtraction.

svUNeg :: SVal -> SVal

Unary minus.

svAbs :: SVal -> SVal

Absolute value.

svDivide :: SVal -> SVal -> SVal

Division.

svQuot :: SVal -> SVal -> SVal

Quotient: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "div" operator (Euclidean division, which always has a non-negative remainder). For unsigned bitvectors, it is "bvudiv"; and for signed bitvectors it is "bvsdiv", which rounds toward zero. All operations have unspecified semantics in case y = 0.

svRem :: SVal -> SVal -> SVal

Remainder: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "mod" operator (always non-negative). For unsigned bitvectors, it is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds toward zero (sign of remainder matches that of x). All operations have unspecified semantics in case y = 0.

svExp :: SVal -> SVal -> SVal

Exponentiation.

svAddConstant :: Integral a => SVal -> a -> SVal

Add a constant value:

svIncrement :: SVal -> SVal

Increment:

svDecrement :: SVal -> SVal

Decrement:

Logical operations

svAnd :: SVal -> SVal -> SVal

Bitwise and.

svOr :: SVal -> SVal -> SVal

Bitwise or.

svXOr :: SVal -> SVal -> SVal

Bitwise xor.

svNot :: SVal -> SVal

Bitwise complement.

svShl :: SVal -> Int -> SVal

Shift left by a constant amount. Translates to the "bvshl" operation in SMT-Lib.

svShr :: SVal -> Int -> SVal

Shift right by a constant amount. Translates to either "bvlshr" (logical shift right) or "bvashr" (arithmetic shift right) in SMT-Lib, depending on whether x is a signed bitvector.

svRol :: SVal -> Int -> SVal

Rotate-left, by a constant

svRor :: SVal -> Int -> SVal

Rotate-right, by a constant

Splitting, joining, and extending

svExtract :: Int -> Int -> SVal -> SVal

Extract bit-sequences.

svJoin :: SVal -> SVal -> SVal

Join two words, by concataneting

Sign-casting

svSign :: SVal -> SVal

Convert a symbolic bitvector from unsigned to signed.

svUnsign :: SVal -> SVal

Convert a symbolic bitvector from signed to unsigned.

Numeric conversions

svFromIntegral :: Kind -> SVal -> SVal

Convert a symbolic bitvector from one integral kind to another.

Indexed lookups

svSelect :: [SVal] -> SVal -> SVal -> SVal

Total indexing operation. svSelect xs default index is intuitively the same as xs !! index, except it evaluates to default if index overflows. Translates to SMT-Lib tables.

Word-level operations

svToWord1 :: SVal -> SVal

Convert an SVal from kind Bool to an unsigned bitvector of size 1.

svFromWord1 :: SVal -> SVal

Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.

svTestBit :: SVal -> Int -> SVal

Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.

svSetBit :: SVal -> Int -> SVal

Set a given bit at index

svShiftLeft :: SVal -> SVal -> SVal

Generalization of svShl, where the shift-amount is symbolic. The first argument should be a bounded quantity.

svShiftRight :: SVal -> SVal -> SVal

Generalization of svShr, where the shift-amount is symbolic. The first argument should be a bounded quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical.

svRotateLeft :: SVal -> SVal -> SVal

Generalization of svRol, where the rotation amount is symbolic. The first argument should be a bounded quantity.

svRotateRight :: SVal -> SVal -> SVal

Generalization of svRor, where the rotation amount is symbolic. The first argument should be a bounded quantity.

svWordFromBE :: [SVal] -> SVal

Un-bit-blast from little-endian representation to a word of the right size. The input is assumed to be unsigned.

svWordFromLE :: [SVal] -> SVal

Un-bit-blast from big-endian representation to a word of the right size. The input is assumed to be unsigned.

svBlastLE :: SVal -> [SVal]

Bit-blast: Little-endian. Assumes the input is a bit-vector.

svBlastBE :: SVal -> [SVal]

Bit-blast: Big-endian. Assumes the input is a bit-vector.

Conditionals: Mergeable values

svIte :: SVal -> SVal -> SVal -> SVal

If-then-else. This one will force branches.

svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal

Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.

svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal

Merge two symbolic values, at kind k, possibly force'ing the branches to make sure they do not evaluate to the same result.

svIsSatisfiableInCurrentPath :: SVal -> Symbolic (Maybe SatResult)

Reduce a condition (i.e., try to concretize it) under the given path

Uninterpreted sorts, constants, and functions

svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.

Properties, proofs, and satisfiability

Proving properties

proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult

Proves the predicate using the given SMT-solver

Checking satisfiability

satWith :: SMTConfig -> Symbolic SVal -> IO SatResult

Find a satisfying assignment using the given SMT-solver

allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult

Find all satisfying assignments using the given SMT-solver

Checking safety

safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]

Check safety using the given SMT-solver

Proving properties using multiple solvers

proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, ThmResult)]

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, ThmResult)

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, SatResult)]

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, SatResult)

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Quick-check

svQuickCheck :: Symbolic SVal -> IO Bool

Dynamic variant of quick-check

Model extraction

Inspecting proof results

newtype ThmResult

A prove call results in a ThmResult

Constructors

ThmResult SMTResult

Instances

Show ThmResult

User friendly way of printing theorem results

Methods

showsPrec :: Int -> ThmResult -> ShowS

show :: ThmResult -> String

showList :: [ThmResult] -> ShowS

Modelable ThmResult

ThmResult as a generic model provider

Methods

modelExists :: ThmResult -> Bool

getModel :: SatModel b => ThmResult -> Either String (Bool, b)

getModelDictionary :: ThmResult -> Map String CW

getModelValue :: SymWord b => String -> ThmResult -> Maybe b

getModelUninterpretedValue :: String -> ThmResult -> Maybe String

extractModel :: SatModel b => ThmResult -> Maybe b

getModelObjectives :: ThmResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCW

extractUnsatCore :: ThmResult -> Maybe [String]

newtype SatResult

A sat call results in a SatResult The reason for having a separate SatResult is to have a more meaningful Show instance.

Constructors

SatResult SMTResult

Instances

Show SatResult

User friendly way of printing satisfiablity results

Methods

showsPrec :: Int -> SatResult -> ShowS

show :: SatResult -> String

showList :: [SatResult] -> ShowS

Modelable SatResult

SatResult as a generic model provider

Methods

modelExists :: SatResult -> Bool

getModel :: SatModel b => SatResult -> Either String (Bool, b)

getModelDictionary :: SatResult -> Map String CW

getModelValue :: SymWord b => String -> SatResult -> Maybe b

getModelUninterpretedValue :: String -> SatResult -> Maybe String

extractModel :: SatModel b => SatResult -> Maybe b

getModelObjectives :: SatResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCW

extractUnsatCore :: SatResult -> Maybe [String]

newtype AllSatResult

An allSat call results in a AllSatResult. The boolean says whether we should warn the user about prefix-existentials.

Constructors

AllSatResult (Bool, [SMTResult])

Instances

Show AllSatResult

The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available.

Methods

showsPrec :: Int -> AllSatResult -> ShowS

show :: AllSatResult -> String

showList :: [AllSatResult] -> ShowS

newtype SafeResult

A safe call results in a SafeResult

Constructors

SafeResult (Maybe String, String, SMTResult)

Instances

Show SafeResult

User friendly way of printing safety results

Methods

showsPrec :: Int -> SafeResult -> ShowS

show :: SafeResult -> String

showList :: [SafeResult] -> ShowS

data OptimizeResult

An optimize call results in a OptimizeResult

Constructors

LexicographicResult SMTResult

ParetoResult [SMTResult]

IndependentResult [(String, SMTResult)]

Instances

Show OptimizeResult

Show instance for optimization results

Methods

showsPrec :: Int -> OptimizeResult -> ShowS

show :: OptimizeResult -> String

showList :: [OptimizeResult] -> ShowS

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 (Maybe [String])

Unsatisfiable, with unsat-core if requested

Satisfiable SMTConfig SMTModel

Satisfiable with model

SatExtField SMTConfig SMTModel

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

Unknown SMTConfig SMTModel

Prover returned unknown, with a potential (possibly bogus) model

ProofError SMTConfig [String]

Prover errored out

TimeOut SMTConfig

Computation timed out (see the timeout combinator)

Instances

NFData SMTResult

Methods

rnf :: SMTResult -> ()

Modelable SMTResult

SMTResult as a generic model provider

Methods

modelExists :: SMTResult -> Bool

getModel :: SatModel b => SMTResult -> Either String (Bool, b)

getModelDictionary :: SMTResult -> Map String CW

getModelValue :: SymWord b => String -> SMTResult -> Maybe b

getModelUninterpretedValue :: String -> SMTResult -> Maybe String

extractModel :: SatModel b => SMTResult -> Maybe b

getModelObjectives :: SMTResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SMTResult -> Maybe GeneralizedCW

extractUnsatCore :: SMTResult -> Maybe [String]

Programmable model extraction

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

Parse a signed/sized value from a sequence of CWs

getModel :: SMTResult -> Either String (Bool, [CW])

Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)

getModelDictionary :: SMTResult -> Map String CW

Extract a model dictionary. Extract a dictionary mapping the variables to their respective values as returned by the SMT solver. Also see getModelDictionaries.

SMT Interface: Configurations and solvers

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

• verbose :: Bool

  Debug mode

• timing :: Timing

  Print timing information on how long different phases took (construction, solving, etc.)

• sBranchTimeOut :: Maybe Int

  How much time to give to the solver for each call of sBranch check. (In seconds. Default: No limit.)

• timeOut :: Maybe Int

  How much time to give to the solver. (In seconds. Default: No limit.)

• printBase :: Int

  Print integral literals in this base (2, 10, and 16 are supported.)

• printRealPrec :: Int

  Print algebraic real values with this precision. (SReal, default: 16)

• solverTweaks :: [String]

  Additional lines of script to give to the solver (user specified)

• optimizeArgs :: [String]

  Additional commands to pass before check-sat is issued

• satCmd :: String

  Usually "(check-sat)". However, users might tweak it based on solver characteristics.

• isNonModelVar :: String -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

• smtFile :: Maybe FilePath

  If Just, the generated SMT script will be put in this file (for debugging purposes mostly)

• smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

• solver :: SMTSolver

  The actual SMT solver.

• roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

• useLogic :: Maybe Logic

  If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.

• getUnsatCore :: Bool

  Should we query unsat-core?

Instances

Show SMTConfig

Methods

showsPrec :: Int -> SMTConfig -> ShowS

show :: SMTConfig -> String

showList :: [SMTConfig] -> ShowS

NFData SMTConfig

Methods

rnf :: SMTConfig -> ()

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

Instances

Bounded SMTLibVersion

Methods

minBound :: SMTLibVersion

maxBound :: SMTLibVersion

Enum SMTLibVersion

Methods

succ :: SMTLibVersion -> SMTLibVersion

pred :: SMTLibVersion -> SMTLibVersion

toEnum :: Int -> SMTLibVersion

fromEnum :: SMTLibVersion -> Int

enumFrom :: SMTLibVersion -> [SMTLibVersion]

enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

Eq SMTLibVersion

Methods

(==) :: SMTLibVersion -> SMTLibVersion -> Bool

(/=) :: SMTLibVersion -> SMTLibVersion -> Bool

Show SMTLibVersion

Methods

showsPrec :: Int -> SMTLibVersion -> ShowS

show :: SMTLibVersion -> String

showList :: [SMTLibVersion] -> ShowS

NFData SMTLibVersion

Methods

rnf :: SMTLibVersion -> ()

data SMTLibLogic

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the user can override this choice using the useLogic parameter to the configuration. This is especially handy if one is experimenting with custom logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for the official list.

Constructors

AUFLIA

Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.

AUFLIRA

Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.

AUFNIRA

Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.

LRA

Linear formulas in linear real arithmetic.

QF_ABV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays.

QF_AUFBV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.

QF_AUFLIA

Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.

QF_AX

Quantifier-free formulas over the theory of arrays with extensionality.

QF_BV

Quantifier-free formulas over the theory of fixed-size bitvectors.

QF_IDL

Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.

QF_LIA

Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.

QF_LRA

Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.

QF_NIA

Quantifier-free integer arithmetic.

QF_NRA

Quantifier-free real arithmetic.

QF_RDL

Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.

QF_UF

Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.

QF_UFBV

Unquantified formulas over bitvectors with uninterpreted sort function and symbols.

QF_UFIDL

Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.

QF_UFLIA

Unquantified linear integer arithmetic with uninterpreted sort and function symbols.

QF_UFLRA

Unquantified linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNRA

Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNIRA

Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols.

UFLRA

Linear real arithmetic with uninterpreted sort and function symbols.

UFNIA

Non-linear integer arithmetic with uninterpreted sort and function symbols.

QF_FPBV

Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors.

QF_FP

Quantifier-free formulas over the theory of floating point numbers.

QF_FD

Quantifier-free finite domains

Instances

Show SMTLibLogic

Methods

showsPrec :: Int -> SMTLibLogic -> ShowS

show :: SMTLibLogic -> String

showList :: [SMTLibLogic] -> ShowS

NFData SMTLibLogic

NFData instance for SMTLibLogic

Methods

rnf :: SMTLibLogic -> ()

data Logic

Chosen logic for the solver

Constructors

PredefinedLogic SMTLibLogic

Use one of the logics as defined by the standard

CustomLogic String

Use this name for the logic

Instances

Show Logic

Methods

showsPrec :: Int -> Logic -> ShowS

show :: Logic -> String

showList :: [Logic] -> ShowS

NFData Logic

NFData instance for Logic

Methods

rnf :: Logic -> ()

data Solver

Solvers that SBV is aware of

Constructors

Z3

Yices

Boolector

CVC4

MathSAT

ABC

Instances

Bounded Solver

Methods

minBound :: Solver

maxBound :: Solver

Enum Solver

Methods

succ :: Solver -> Solver

pred :: Solver -> Solver

toEnum :: Int -> Solver

fromEnum :: Solver -> Int

enumFrom :: Solver -> [Solver]

enumFromThen :: Solver -> Solver -> [Solver]

enumFromTo :: Solver -> Solver -> [Solver]

enumFromThenTo :: Solver -> Solver -> Solver -> [Solver]

Show Solver

Methods

showsPrec :: Int -> Solver -> ShowS

show :: Solver -> String

showList :: [Solver] -> ShowS

data SMTSolver

An SMT solver

Constructors

SMTSolver

Fields

• name :: Solver

  The solver in use

• executable :: String

  The path to its executable

• options :: [String]

  Options to provide to the solver

• engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

• capabilities :: SolverCapabilities

  Various capabilities of the solver

Instances

Show SMTSolver

Methods

showsPrec :: Int -> SMTSolver -> ShowS

show :: SMTSolver -> String

showList :: [SMTSolver] -> ShowS

boolector :: SMTConfig

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig

Default configuration for the MathSAT SMT solver

abc :: SMTConfig

Default configuration for the ABC synthesis and verification tool.

defaultSolverConfig :: Solver -> SMTConfig

The default configs corresponding to supported SMT solvers

sbvCurrentSolver :: SMTConfig

The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.

defaultSMTCfg :: SMTConfig

The default solver used by SBV. This is currently set to z3.

sbvCheckSolverInstallation :: SMTConfig -> IO Bool

Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.

sbvAvailableSolvers :: IO [SMTConfig]

Return the known available solver configs, installed on your machine.

Symbolic computations

outputSVal :: SVal -> Symbolic ()

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

Code generation from symbolic programs

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

Instances

Monad SBVCodeGen

Methods

(>>=) :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b

(>>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b

return :: a -> SBVCodeGen a

fail :: String -> SBVCodeGen a

Functor SBVCodeGen

Methods

fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b

(<$) :: a -> SBVCodeGen b -> SBVCodeGen a

Applicative SBVCodeGen

Methods

pure :: a -> SBVCodeGen a

(<*>) :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b

(*>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b

(<*) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a

MonadIO SBVCodeGen

Methods

liftIO :: IO a -> SBVCodeGen a

MonadState CgState SBVCodeGen

Methods

get :: SBVCodeGen CgState

put :: CgState -> SBVCodeGen ()

state :: (CgState -> (a, CgState)) -> SBVCodeGen a

Setting code-generation options

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.

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.

Designating inputs

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.

Designating outputs

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

Creates an atomic output in the generated code.

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

Creates an array output in the generated code.

Designating return values

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.

Code generation with uninterpreted functions

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

Code generation with SInteger and SReal types

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

Instances

Eq CgSRealType

Methods

(==) :: CgSRealType -> CgSRealType -> Bool

(/=) :: CgSRealType -> CgSRealType -> Bool

Show CgSRealType

Show instance for cgSRealType displays values as they would be used in a C program

Methods

showsPrec :: Int -> CgSRealType -> ShowS

show :: CgSRealType -> String

showList :: [CgSRealType] -> ShowS

Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
• The second argument is the name of the C function to generate.
• The final argument is the function to be compiled.

Compilation will also generate a Makefile, a header file, and a driver (test) program, etc.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
• The second argument is the name of the archive to generate.
• The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of compileToC, except in a list.

Compilation to SMTLib

compileToSMTLib

Arguments

:: SMTLibVersion

If True, output SMT-Lib2, otherwise SMT-Lib1

-> Bool

If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.)

-> Symbolic SVal

-> IO String

Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library. It takes two arguments:

• version: The SMTLib-version to produce. Note that we currently only support SMTLib2.
• isSat : If True, will translate it as a SAT query, i.e., in the positive. If False, will translate as a PROVE query, i.e., it will negate the result. (In this case, the check-sat call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)

generateSMTBenchmarks :: Bool -> FilePath -> Symbolic SVal -> IO ()

Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with suffix ".smt2". The Bool argument controls whether this is a SAT instance, i.e., translate the query directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to compileToSMTLib for details.)