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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Internals

Contents

- Running symbolic programs manually
- Other internal structures useful for low-level programming
- Operations useful for instantiating SBV type classes
- Polynomial operations that operate on bit-vectors
- Compilation to C
- Various math utilities around floats

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

- data Result = Result {
  - reskinds :: Set Kind
  - resTraces :: [(String, CW)]
  - resUISegs :: [(String, [String])]
  - resInputs :: [(Quantifier, NamedSymVar)]
  - resConsts :: [(SW, CW)]
  - resTables :: [((Int, Kind, Kind), [SW])]
  - resArrays :: [(Int, ArrayInfo)]
  - resUIConsts :: [(String, SBVType)]
  - resAxioms :: [(String, [String])]
  - resAsgns :: SBVPgm
  - resConstraints :: [SW]
  - resAssertions :: [(String, Maybe CallStack, SW)]
  - resOutputs :: [SW]
  }
- data SBVRunMode
  - = Proof (Bool, SMTConfig)
  - | CodeGen
  - | Concrete StdGen
- data Symbolic a
- runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result
- runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
- newtype SBV a = SBV {
  - unSBV :: SVal
  }
- slet :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
- data CW = CW {
  - _cwKind :: !Kind
  - cwVal :: !CWVal
  }
- data Kind
  - = KBool
  - | KBounded Bool Int
  - | KUnbounded
  - | KReal
  - | KUserSort String (Either String [String])
  - | KFloat
  - | KDouble
- class HasKind a where
  - 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
- data CWVal
  - = CWAlgReal AlgReal
  - | CWInteger Integer
  - | CWFloat Float
  - | CWDouble Double
  - | CWUserSort (Maybe Int, String)
- data AlgReal
  - = AlgRational Bool Rational
  - | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data Quantifier
  - = ALL
  - | EX
- mkConstCW :: Integral a => Kind -> a -> CW
- genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)
- genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)
- liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
- symbolicMergeWithKind :: Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a
- cache :: (State -> IO a) -> Cached a
- sbvToSW :: State -> SBV a -> IO SW
- newExpr :: State -> Kind -> SBVExpr -> IO SW
- normCW :: CW -> CW
- data SBVExpr = SBVApp !Op ![SW]
- data Op
  - = Plus
  - | Times
  - | Minus
  - | UNeg
  - | Abs
  - | Quot
  - | Rem
  - | Equal
  - | NotEqual
  - | LessThan
  - | GreaterThan
  - | LessEq
  - | GreaterEq
  - | Ite
  - | And
  - | Or
  - | XOr
  - | Not
  - | Shl Int
  - | Shr Int
  - | Rol Int
  - | Ror Int
  - | Extract Int Int
  - | Join
  - | LkUp (Int, Kind, Kind, Int) !SW !SW
  - | ArrEq Int Int
  - | ArrRead Int
  - | IntCast Kind Kind
  - | Uninterpreted String
  - | Label String
  - | IEEEFP FPOp
- newtype SBVType = SBVType [Kind]
- newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
- forceSWArg :: SW -> IO ()
- genLiteral :: Integral a => Kind -> a -> SBV b
- genFromCW :: Integral a => CW -> a
- genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
- checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- showModel :: SMTConfig -> SMTModel -> String
- data SMTModel = SMTModel {
  - modelAssocs :: [(String, CW)]
  }
- smtLibReservedNames :: [String]
- ites :: SBool -> [SBool] -> [SBool] -> [SBool]
- mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
- addPoly :: [SBool] -> [SBool] -> [SBool]
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
  - = CgMakefile [String]
  - | CgHeader [Doc]
  - | CgSource
  - | CgDriver
- fpRound0 :: (RealFloat a, RealFrac a, Integral b) => a -> b
- fpRatio0 :: (RealFloat a, RealFrac a) => a -> Rational
- fpMaxH :: RealFloat a => a -> a -> a
- fpMinH :: RealFloat a => a -> a -> a
- fp2fp :: (RealFloat a, RealFloat b) => a -> b
- fpRemH :: RealFloat a => a -> a -> a
- fpRoundToIntegralH :: RealFloat a => a -> a
- fpIsEqualObjectH :: RealFloat a => a -> a -> Bool
- fpIsNormalizedH :: RealFloat a => a -> Bool

# Running symbolic programs manually

data Result Source

Result of running a symbolic computation

Constructors

Result |

Fields

reskinds :: Set Kind

  kinds used in the program

resTraces :: [(String, CW)]

  quick-check counter-example information (if any)

resUISegs :: [(String, [String])]

  uninterpeted code segments

resInputs :: [(Quantifier, NamedSymVar)]

  inputs (possibly existential)

resConsts :: [(SW, CW)]

  constants

resTables :: [((Int, Kind, Kind), [SW])]

  tables (automatically constructed) (tableno, index-type, result-type) elts

resArrays :: [(Int, ArrayInfo)]

  arrays (user specified)

resUIConsts :: [(String, SBVType)]

  uninterpreted constants

resAxioms :: [(String, [String])]

  axioms

resAsgns :: SBVPgm

  assignments

resConstraints :: [SW]

  additional constraints (boolean)

resAssertions :: [(String, Maybe CallStack, SW)]

  assertions

resOutputs :: [SW]

  outputs

Instances

Show Result Source | Show instance for `Result`. Only for debugging purposes.
NFData Result Source |

data SBVRunMode Source

Different means of running a symbolic piece of code

Constructors

Proof (Bool, SMTConfig) | Fully Symbolic, proof mode.
CodeGen | Code generation mode.
Concrete StdGen | Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs.

data Symbolic a Source

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 Source |
Functor Symbolic Source |
Applicative Symbolic Source |
MonadIO Symbolic Source |
Provable Predicate Source |
NFData a => SExecutable (Symbolic a) Source |

runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result Source

Run a symbolic computation in Proof mode and return a `Result`. The boolean argument indicates if this is a sat instance or not.

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

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

# Other internal structures useful for low-level programming

newtype SBV a Source

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

Constructors

SBV |

Fields

unSBV :: SVal

Instances

Provable SBool Source |
Provable Predicate Source |
SDivisible SInteger Source |
SDivisible SInt64 Source |
SDivisible SInt32 Source |
SDivisible SInt16 Source |
SDivisible SInt8 Source |
SDivisible SWord64 Source |
SDivisible SWord32 Source |
SDivisible SWord16 Source |
SDivisible SWord8 Source |
SDivisible SWord4 Source | SDvisible instance, using default methods
FromBits SInt64 Source |
FromBits SInt32 Source |
FromBits SInt16 Source |
FromBits SInt8 Source |
FromBits SWord64 Source |
FromBits SWord32 Source |
FromBits SWord16 Source |
FromBits SWord8 Source |
FromBits SBool Source |
FromBits SWord4 Source | Conversion from bits
Polynomial SWord64 Source |
Polynomial SWord32 Source |
Polynomial SWord16 Source |
Polynomial SWord8 Source |
Splittable SWord64 SWord32 Source |
Splittable SWord32 SWord16 Source |
Splittable SWord16 SWord8 Source |
Eq (SBV a) Source |
Show (SBV a) Source |
NFData a => NFData (SBV a) Source |
(Random a, SymWord a) => Random (SBV a) Source |
HasKind a => HasKind (SBV a) Source |
(NFData a, SymWord a) => SExecutable [SBV a] Source |
NFData a => SExecutable (SBV a) Source |
(SymWord a, PrettyNum a) => PrettyNum (SBV a) Source |
HasKind a => Uninterpreted (SBV a) Source |
SymWord a => Mergeable (SBV a) Source |
SymWord a => OrdSymbolic (SBV a) Source |
EqSymbolic (SBV a) Source |
(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) Source |
(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source |
(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) Source |
(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) Source |
(SymWord a, SExecutable p) => SExecutable (SBV a -> p) Source |
(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) Source |
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source |
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source |
(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) Source |
(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) Source |
(SymWord a, Provable p) => Provable (SBV a -> p) Source |
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source |
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) Source |
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source |
(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) Source |
(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) Source |
(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) Source |
(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) Source |
(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) Source |
(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) Source |
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source |
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) Source |
(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) Source |
(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) Source |
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) Source |
(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source |
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source |
(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) Source |
(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) Source |
(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) Source |
(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) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source |
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source |
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source |
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source |
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) Source |
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) Source |
(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) Source |
(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) Source |
(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) Source |
(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) Source |

slet :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b Source

Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms built in, based on Andy Gill's type-safe obervable sharing technique (see: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09). However, there might be times where being explicit on the sharing can help, especially in experimental code. The `slet` combinator ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most use cases of the SBV library should simply use Haskell's `let` construct for this purpose.

data CW Source

`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 Source |
Ord CW Source |
Show CW Source | Show instance for `CW`.
HasKind CW Source | `Kind` instance for CW
PrettyNum CW Source |
SatModel CW Source | `CW` as extracted from a model; trivial definition
SDivisible CW Source |

data Kind Source

Kind of symbolic value

Constructors

KBool |
KBounded Bool Int |
KUnbounded |
KReal |
KUserSort String (Either String [String]) |
KFloat |
KDouble |

Instances

Eq Kind Source | We want to equate user-sorts only by name
Ord Kind Source | We want to order user-sorts only by name
Show Kind Source |
HasKind Kind Source |

class HasKind a where Source

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.

Minimal complete definition

Nothing

Methods

kindOf :: a -> Kind Source

hasSign :: a -> Bool Source

intSizeOf :: a -> Int Source

isBoolean :: a -> Bool Source

isBounded :: a -> Bool Source

isReal :: a -> Bool Source

isFloat :: a -> Bool Source

isDouble :: a -> Bool Source

isInteger :: a -> Bool Source

isUninterpreted :: a -> Bool Source

showType :: a -> String Source

Instances

HasKind Bool Source |
HasKind Double Source |
HasKind Float Source |
HasKind Int8 Source |
HasKind Int16 Source |
HasKind Int32 Source |
HasKind Int64 Source |
HasKind Integer Source |
HasKind Word8 Source |
HasKind Word16 Source |
HasKind Word32 Source |
HasKind Word64 Source |
HasKind AlgReal Source |
HasKind Kind Source |
HasKind CW Source | `Kind` instance for CW
HasKind RoundingMode Source | `RoundingMode` kind
HasKind SVal Source |
HasKind E Source |
HasKind Word4 Source | HasKind instance; simply returning the underlying kind for the type
HasKind Sport Source |
HasKind Pet Source |
HasKind Beverage Source |
HasKind Nationality Source |
HasKind Color Source |
HasKind Location Source |
HasKind U2Member Source |
HasKind B Source |
HasKind Q Source |
HasKind L Source | Similarly, `HasKind`s default implementation is sufficient.
HasKind a => HasKind (SBV a) Source |

data CWVal Source

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 Source | 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:
Ord CWVal Source | Ord instance for CWVal. Same comments as the `Eq` instance why this cannot be derived.

data AlgReal Source

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

Constructors

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

Instances

Eq AlgReal Source |
Fractional AlgReal Source | NB: Following the other types we have, we require `a/0` to be `0` for all a.
Num AlgReal Source |
Ord AlgReal Source |
Real AlgReal Source |
Show AlgReal Source |
Arbitrary AlgReal Source |
Random AlgReal Source |
HasKind AlgReal Source |
SatModel AlgReal Source | `AlgReal` as extracted from a model
IEEEFloatConvertable AlgReal Source |

data Quantifier Source

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

Constructors

ALL |
EX |

Instances

Eq Quantifier Source |
NFData Quantifier Source |

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

Create a constant word from an integral.

genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a) Source

Generate a finite symbolic bitvector, named

genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a) Source

Generate a finite symbolic bitvector, unnamed

liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a) Source

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 a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) Source

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)

symbolicMergeWithKind :: Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a Source

Merge two symbolic values, at kind `k`, possibly `force`'ing the branches to make sure they do not evaluate to the same result. This should only be used for internal purposes; as default definitions provided should suffice in many cases. (i.e., End users should only need to define `symbolicMerge` when needed; which should be rare to start with.)

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

Cache a state-based computation

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

Convert a symbolic value to a symbolic-word

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

Create a new expression; hash-cons as necessary

normCW :: CW -> CW Source

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 SBVExpr Source

A symbolic expression

Constructors

SBVApp !Op ![SW] |

Instances

Eq SBVExpr Source |
Ord SBVExpr Source |
Show SBVExpr Source | Show instance for `SBVExpr`. Again, only for debugging purposes.
NFData SBVExpr Source |

data Op Source

Symbolic operations

Constructors

Plus |
Times |
Minus |
UNeg |
Abs |
Quot |
Rem |
Equal |
NotEqual |
LessThan |
GreaterThan |
LessEq |
GreaterEq |
Ite |
And |
Or |
XOr |
Not |
Shl Int |
Shr Int |
Rol Int |
Ror Int |
Extract Int Int |
Join |
LkUp (Int, Kind, Kind, Int) !SW !SW |
ArrEq Int Int |
ArrRead Int |
IntCast Kind Kind |
Uninterpreted String |
Label String |
IEEEFP FPOp |

Instances

Eq Op Source |
Ord Op Source |
Show Op Source | Show instance for `Op`. Note that this is largely for debugging purposes, not used for being read by any tool.

newtype SBVType Source

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

Instances

Eq SBVType Source |
Ord SBVType Source |
Show SBVType Source |
NFData SBVType Source |

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

Create a new uninterpreted symbol, possibly with user given code

forceSWArg :: SW -> IO () Source

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

# Operations useful for instantiating SBV type classes

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

Generate a finite constant bitvector

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

Convert a constant to an integral value

genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source

Generically make a symbolic var

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

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]) Source

Parse a signed/sized value from a sequence of CWs

showModel :: SMTConfig -> SMTModel -> String Source

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 Source

A model, as returned by a solver

Constructors

SMTModel |

Fields

modelAssocs :: [(String, CW)]

  Mapping of symbolic values to constants.

Instances

Show SMTModel Source |
NFData SMTModel Source |

smtLibReservedNames :: [String] Source

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.

# Polynomial operations that operate on bit-vectors

ites :: SBool -> [SBool] -> [SBool] -> [SBool] Source

Run down a boolean condition over two lists. Note that this is different than zipWith as shorter list is assumed to be filled with false at the end (i.e., zero-bits); which nicely pads it when considered as an unsigned number in little-endian form.

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) Source

Compute modulus/remainder of polynomials on bit-vectors.

addPoly :: [SBool] -> [SBool] -> [SBool] Source

Add two polynomials

# Compilation to C

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

Lower level version of `compileToC`, producing a `CgPgmBundle`

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

Lower level version of `compileToCLib`, producing a `CgPgmBundle`

data CgPgmBundle Source

Representation of a collection of generated programs.

Constructors

CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |

Instances

Show CgPgmBundle Source | A simple way to print bundles, mostly for debugging purposes.

data CgPgmKind Source

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

Constructors

CgMakefile [String] |
CgHeader [Doc] |
CgSource |
CgDriver |

# Various math utilities around floats

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

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

fpRatio0 :: (RealFloat a, RealFrac a) => a -> Rational Source

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

fpMaxH :: RealFloat a => a -> a -> a Source

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 Source

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

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

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

fpRemH :: RealFloat a => a -> a -> a Source

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 Source

Convert a float to the nearest integral representable in that type

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

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 Source

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!