| 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
- 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
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data Quantifier
- 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])
- 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, 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
Result of running a symbolic computation
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
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 | |
| Arbitrary AlgReal Source | |
| Random 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 :: (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.)
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
genLiteral :: Integral a => Kind -> a -> SBV b Source
Generate a finite constant bitvector
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
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, 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!