| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
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.
- 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
- data Symbolic a
- runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result
- runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
- newtype SBV a = SBV {}
- slet :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
- data CW = CW {}
- data Kind
- class HasKind a where
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data Quantifier
- mkConstCW :: Integral a => Kind -> a -> CW
- genVar :: Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)
- genVar_ :: Maybe Quantifier -> Kind -> Symbolic (SBV a)
- liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (SymWord a, Num 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 :: 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
- fpRound0 :: (RealFloat a, Integral b) => a -> b
- fpRatio0 :: RealFloat 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
Result of running a symbolic computation
Constructors
| Result | |
Fields
| |
data SBVRunMode Source #
Different means of running a symbolic piece of code
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.
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
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
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.
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.
Kind of symbolic value
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.
Methods
intSizeOf :: a -> Int Source #
isBoolean :: a -> Bool Source #
isBounded :: a -> Bool Source #
isDouble :: a -> Bool Source #
isInteger :: a -> Bool Source #
isUninterpreted :: a -> Bool 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 # |
|
| HasKind RoundingMode Source # |
|
| 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 (SBV a) 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 |
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 # | |
| Random AlgReal Source # | |
| Arbitrary AlgReal Source # | |
| HasKind AlgReal Source # | |
| SatModel AlgReal Source # |
|
| IEEEFloatConvertable AlgReal Source # | |
data Quantifier Source #
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
Instances
genVar :: Maybe Quantifier -> Kind -> String -> Symbolic (SBV a) Source #
Generate a finite symbolic bitvector, named
genVar_ :: Maybe Quantifier -> Kind -> Symbolic (SBV a) Source #
Generate a finite symbolic bitvector, unnamed
liftQRem :: SymWord 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 (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.)
newExpr :: State -> Kind -> SBVExpr -> IO SW Source #
Create a new expression; hash-cons as necessary
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.)
A symbolic expression
Symbolic operations
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.
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
genMkSymVar :: 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
A model, as returned by a solver
Constructors
| SMTModel | |
Fields
| |
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.
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. |
Different kinds of "files" we can produce. Currently this is quite C specific.
Various math utilities around floats
fpRound0 :: (RealFloat a, Integral b) => a -> b Source #
A variant of round; except defaulting to 0 when fed NaN or Infinity
fpRatio0 :: RealFloat 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!