| 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
- Solver capabilities
- Internal structures useful for low-level programming
- Operations useful for instantiating SBV type classes
- Getting SMT-Lib output (for offline analysis)
- Compilation to C, extras
- Code generation primitives
- The codegen monad
- Specifying inputs, SBV variants
- Specifying inputs, SVal variants
- Settings
- Infrastructure
- Generating collateral
- 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.
- 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 :: [(Maybe String, SW)]
- resTactics :: [Tactic SW]
- resGoals :: [Objective (SW, SW)]
- resAssertions :: [(String, Maybe CallStack, SW)]
- resOutputs :: [SW]
- data SBVRunMode
- data SolverCapabilities = SolverCapabilities {
- capSolverName :: String
- mbDefaultLogic :: Bool -> Maybe String
- supportsDefineFun :: Bool
- supportsProduceModels :: Bool
- supportsQuantifiers :: Bool
- supportsUninterpretedSorts :: Bool
- supportsUnboundedInts :: Bool
- supportsReals :: Bool
- supportsFloats :: Bool
- supportsDoubles :: Bool
- supportsOptimization :: Bool
- supportsPseudoBooleans :: Bool
- supportsUnsatCores :: Bool
- type SBool = SBV Bool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInteger = SBV Integer
- type SReal = SBV AlgReal
- type SFloat = SBV Float
- type SDouble = SBV Double
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymWord a) => SBV a
- sInfinity :: (Floating a, SymWord a) => SBV a
- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class (HasKind a, Ord a) => SymWord a where
- data CW = CW {}
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data ExtCW
- data GeneralizedCW
- isRegularCW :: GeneralizedCW -> Bool
- cwSameType :: CW -> CW -> Bool
- cwToBool :: CW -> Bool
- mkConstCW :: Integral a => Kind -> a -> CW
- liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b
- mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW
- mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW
- data SW = SW !Kind !NodeId
- trueSW :: SW
- falseSW :: SW
- trueCW :: CW
- falseCW :: CW
- normCW :: CW -> CW
- data SVal = SVal !Kind !(Either CW (Cached SW))
- newtype SBV a = SBV {}
- newtype NodeId = NodeId Int
- mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
- data ArrayContext
- = ArrayFree (Maybe SW)
- | ArrayReset Int SW
- | ArrayMutate Int SW SW
- | ArrayMerge SW Int Int
- type ArrayInfo = (String, (Kind, Kind), ArrayContext)
- class SymArray array where
- newtype SFunArray a b = SFunArray (SBV a -> SBV b)
- mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
- newtype SArray a b = SArray {}
- sbvToSW :: State -> SBV a -> IO SW
- sbvToSymSW :: SBV a -> Symbolic SW
- forceSWArg :: SW -> IO ()
- data SBVExpr = SBVApp !Op ![SW]
- newExpr :: State -> Kind -> SBVExpr -> IO SW
- cache :: (State -> IO a) -> Cached a
- data Cached a
- uncache :: Cached SW -> State -> IO SW
- uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
- class HasKind a where
- 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
- | KindCast Kind Kind
- | Uninterpreted String
- | Label String
- | IEEEFP FPOp
- | PseudoBoolean PBOp
- data PBOp
- data FPOp
- type NamedSymVar = (SW, String)
- getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
- newtype SBVPgm = SBVPgm {
- pgmAssignments :: Seq (SW, SBVExpr)
- data Symbolic a
- class SExecutable a where
- runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result
- runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
- data State
- getPathCondition :: State -> SBool
- extendPathCondition :: State -> (SBool -> SBool) -> State
- inProofMode :: State -> Bool
- data SBVRunMode
- data Kind
- class Outputtable a where
- 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 :: [(Maybe String, SW)]
- resTactics :: [Tactic SW]
- resGoals :: [Objective (SW, SW)]
- resAssertions :: [(String, Maybe CallStack, SW)]
- resOutputs :: [SW]
- data Logic
- data SMTLibLogic
- addConstraint :: Maybe String -> Maybe Double -> SBool -> SBool -> Symbolic ()
- internalVariable :: State -> Kind -> IO SW
- internalConstraint :: State -> Maybe String -> SVal -> IO ()
- isCodeGenMode :: State -> Bool
- newtype SBVType = SBVType [Kind]
- newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
- addAxiom :: String -> [String] -> Symbolic ()
- data Quantifier
- needsExistentials :: [Quantifier] -> Bool
- data SMTLibPgm = SMTLibPgm SMTLibVersion [String]
- data SMTLibVersion = SMTLib2
- smtLibVersionExtension :: SMTLibVersion -> String
- smtLibReservedNames :: [String]
- data SolverCapabilities = SolverCapabilities {
- capSolverName :: String
- mbDefaultLogic :: Bool -> Maybe String
- supportsDefineFun :: Bool
- supportsProduceModels :: Bool
- supportsQuantifiers :: Bool
- supportsUninterpretedSorts :: Bool
- supportsUnboundedInts :: Bool
- supportsReals :: Bool
- supportsFloats :: Bool
- supportsDoubles :: Bool
- supportsOptimization :: Bool
- supportsPseudoBooleans :: Bool
- supportsUnsatCores :: Bool
- extractSymbolicSimulationState :: State -> IO Result
- data SMTScript = SMTScript {}
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- options :: [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- data SMTResult
- data SMTModel = SMTModel {
- modelObjectives :: [(String, GeneralizedCW)]
- modelAssocs :: [(String, CW)]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- sBranchTimeOut :: Maybe Int
- timeOut :: Maybe Int
- printBase :: Int
- printRealPrec :: Int
- solverTweaks :: [String]
- optimizeArgs :: [String]
- satCmd :: String
- isNonModelVar :: String -> Bool
- smtFile :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- roundingMode :: RoundingMode
- useLogic :: Maybe Logic
- getUnsatCore :: Bool
- getSBranchRunConfig :: State -> Maybe SMTConfig
- declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b)
- declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b)
- data OptimizeStyle
- data Penalty
- data Objective a
- data Tactic a
- data CaseCond
- data SMTProblem = SMTProblem {}
- isParallelCaseAnywhere :: Tactic a -> Bool
- 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 {
- modelObjectives :: [(String, GeneralizedCW)]
- modelAssocs :: [(String, CW)]
- 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)
- compileToSMTLib :: Provable a => SMTLibVersion -> Bool -> a -> IO String
- generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
- cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
- cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]
- cgOutput :: String -> SBV a -> SBVCodeGen ()
- cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()
- cgReturn :: SBV a -> SBVCodeGen ()
- cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()
- svCgInput :: Kind -> String -> SBVCodeGen SVal
- svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
- svCgOutput :: String -> SVal -> SBVCodeGen ()
- svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
- svCgReturn :: SVal -> SBVCodeGen ()
- svCgReturnArr :: [SVal] -> SBVCodeGen ()
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
- class CgTarget a where
- data CgConfig = CgConfig {
- cgRTC :: Bool
- cgInteger :: Maybe Int
- cgReal :: Maybe CgSRealType
- cgDriverVals :: [Integer]
- cgGenDriver :: Bool
- cgGenMakefile :: Bool
- cgIgnoreAsserts :: Bool
- data CgState = CgState {}
- data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
- data CgVal
- defaultCgConfig :: CgConfig
- initCgState :: CgState
- isCgDriver :: CgPgmKind -> Bool
- isCgMakefile :: CgPgmKind -> Bool
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
- renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
- 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
Solver capabilities
data SolverCapabilities Source #
Translation tricks needed for specific capabilities afforded by each solver
Constructors
| SolverCapabilities | |
Fields
| |
Internal structures useful for low-level programming
data RoundingMode Source #
Rounding mode to be used for the IEEE floating-point operations.
Note that Haskell's default is RoundNearestTiesToEven. If you use
a different rounding mode, then the counter-examples you get may not
match what you observe in Haskell.
Constructors
| RoundNearestTiesToEven | Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.) |
| RoundNearestTiesToAway | Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.) |
| RoundTowardPositive | Round towards positive infinity. (Also known as rounding-up or ceiling.) |
| RoundTowardNegative | Round towards negative infinity. (Also known as rounding-down or floor.) |
| RoundTowardZero | Round towards zero. (Also known as truncation.) |
Instances
| Bounded RoundingMode Source # | |
| Enum RoundingMode Source # | |
| Eq RoundingMode Source # | |
| Data RoundingMode Source # | |
| Ord RoundingMode Source # | |
| Read RoundingMode Source # | |
| Show RoundingMode Source # | |
| HasKind RoundingMode Source # |
|
| SymWord RoundingMode Source # |
|
| SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices) |
type SRoundingMode = SBV RoundingMode Source #
The symbolic variant of RoundingMode
sRoundNearestTiesToEven :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToAway :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToAway
sRoundTowardPositive :: SRoundingMode Source #
Symbolic variant of RoundNearestPositive
sRoundTowardNegative :: SRoundingMode Source #
Symbolic variant of RoundTowardNegative
sRoundTowardZero :: SRoundingMode Source #
Symbolic variant of RoundTowardZero
sRNE :: SRoundingMode Source #
Alias for sRoundNearestTiesToEven
sRNA :: SRoundingMode Source #
Alias for sRoundNearestTiesToAway
sRTP :: SRoundingMode Source #
Alias for sRoundTowardPositive
sRTN :: SRoundingMode Source #
Alias for sRoundTowardNegative
sRTZ :: SRoundingMode Source #
Alias for sRoundTowardZero
class (HasKind a, Ord a) => SymWord a where Source #
A SymWord is a potential symbolic bitvector that can be created instances of
to be fed to a symbolic program. Note that these methods are typically not needed
in casual uses with prove, sat, allSat etc, as default instances automatically
provide the necessary bits.
Methods
forall :: String -> Symbolic (SBV a) Source #
Create a user named input (universal)
forall_ :: Symbolic (SBV a) Source #
Create an automatically named input
mkForallVars :: Int -> Symbolic [SBV a] Source #
Get a bunch of new words
exists :: String -> Symbolic (SBV a) Source #
Create an existential variable
exists_ :: Symbolic (SBV a) Source #
Create an automatically named existential variable
mkExistVars :: Int -> Symbolic [SBV a] Source #
Create a bunch of existentials
free :: String -> Symbolic (SBV a) Source #
Create a free variable, universal in a proof, existential in sat
free_ :: Symbolic (SBV a) Source #
Create an unnamed free variable, universal in proof, existential in sat
mkFreeVars :: Int -> Symbolic [SBV a] Source #
Create a bunch of free vars
symbolic :: String -> Symbolic (SBV a) Source #
Similar to free; Just a more convenient name
symbolics :: [String] -> Symbolic [SBV a] Source #
Similar to mkFreeVars; but automatically gives names based on the strings
literal :: a -> SBV a Source #
Turn a literal constant to symbolic
unliteral :: SBV a -> Maybe a Source #
Extract a literal, if the value is concrete
Extract a literal, from a CW representation
isConcrete :: SBV a -> Bool Source #
Is the symbolic word concrete?
isSymbolic :: SBV a -> Bool Source #
Is the symbolic word really symbolic?
isConcretely :: SBV a -> (a -> Bool) -> Bool Source #
Does it concretely satisfy the given predicate?
mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #
One stop allocator
literal :: Show a => a -> SBV a Source #
Turn a literal constant to symbolic
fromCW :: Read a => CW -> a Source #
Extract a literal, from a CW representation
mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #
One stop allocator
Instances
| SymWord RoundingMode Source # |
|
| SymWord E Source # | |
| SymWord Word4 Source # | SymWord instance, allowing this type to be used in proofs/sat etc. |
| SymWord Sport Source # | |
| SymWord Pet Source # | |
| SymWord Beverage Source # | |
| SymWord Nationality Source # | |
| SymWord Color Source # | |
| SymWord Location Source # | |
| SymWord U2Member Source # | |
| SymWord B Source # | |
| SymWord Q Source # | |
| SymWord L Source # | Declare instances to make |
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.
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 # | |
A simple expression type over extendent values, covering infinity, epsilon and intervals.
data GeneralizedCW Source #
A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
Constructors
| ExtendedCW ExtCW | |
| RegularCW CW |
Instances
| Show GeneralizedCW Source # | Show instance for Generalized |
| HasKind GeneralizedCW Source # |
|
isRegularCW :: GeneralizedCW -> Bool Source #
Is this a regular CW?
liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b Source #
Lift a binary function through a CW
mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW Source #
Map a unary function through a CW.
mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW Source #
Map a binary function through a CW.
A symbolic word, tracking it's signedness and size.
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.)
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 Source # | Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do. |
| Show SVal Source # | Show instance for |
| NFData SVal Source # | |
| HasKind SVal Source # | |
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
A symbolic node id
mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) Source #
Create a symbolic variable.
data ArrayContext Source #
The context of a symbolic array as created
Constructors
| ArrayFree (Maybe SW) | A new array, with potential initializer for each cell |
| ArrayReset Int SW | An array created from another array by fixing each element to another value |
| ArrayMutate Int SW SW | An array created by mutating another array at a given cell |
| ArrayMerge SW Int Int | An array created by symbolically merging two other arrays |
Instances
class SymArray array where Source #
Flat arrays of symbolic values
An array a b is an array indexed by the type SBV aSBV bnewArray_ and newArray methods, then the elements
are left unspecified, i.e., the solver is free to choose any value. This is the right thing
to do if arrays are used as inputs to functions to be verified, typically.
While it's certainly possible for user to create instances of SymArray, the
SArray and SFunArray instances already provided should cover most use cases
in practice. (There are some differences between these models, however, see the corresponding
declaration.)
Minimal complete definition: All methods are required, no defaults.
Minimal complete definition
newArray_, newArray, readArray, resetArray, writeArray, mergeArrays
Methods
newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source #
Create a new array, with an optional initial value
newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) Source #
Create a named new array, with an optional initial value
readArray :: array a b -> SBV a -> SBV b Source #
Read the array element at a
resetArray :: SymWord b => array a b -> SBV b -> array a b Source #
Reset all the elements of the array to the value b
writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b Source #
Update the element at a to be b
mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b Source #
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
newtype SFunArray a b Source #
Arrays implemented internally as functions
- Internally handled by the library and not mapped to SMT-Lib
- Reading an uninitialized value is considered an error (will throw exception)
- Cannot check for equality (internally represented as functions)
- Can quick-check
- Typically faster as it gets compiled away during translation
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source #
Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)
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
SArrayvalues - Typically slower as it heavily relies on SMT-solving for the array theory
sbvToSymSW :: SBV a -> Symbolic SW Source #
Convert a symbolic value to an SW, inside the Symbolic monad
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
A symbolic expression
newExpr :: State -> Kind -> SBVExpr -> IO SW Source #
Create a new expression; hash-cons as necessary
We implement a peculiar caching mechanism, applicable to the use case in implementation of SBV's. Whenever we do a state based computation, we do not want to keep on evaluating it in the then-current state. That will produce essentially a semantically equivalent value. Thus, we want to run it only once, and reuse that result, capturing the sharing at the Haskell level. This is similar to the "type-safe observable sharing" work, but also takes into the account of how symbolic simulation executes.
See Andy Gill's type-safe obervable sharing trick for the inspiration behind this technique: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09
Note that this is *not* a general memo utility!
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 ExtCW Source # | Kind instance for Extended CW |
| HasKind GeneralizedCW Source # |
|
| HasKind CW Source # |
|
| HasKind RoundingMode Source # |
|
| HasKind SVal Source # | |
| HasKind SW 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 # | |
Symbolic operations
Constructors
Pseudo-boolean operations
Constructors
| PB_AtMost Int | At most k |
| PB_AtLeast Int | At least k |
| PB_Exactly Int | Exactly k |
| PB_Le [Int] Int | At most k, with coefficients given. Generalizes PB_AtMost |
| PB_Ge [Int] Int | At least k, with coefficients given. Generalizes PB_AtLeast |
| PB_Eq [Int] Int | Exactly k, with coefficients given. Generalized PB_Exactly |
Floating point operations
type NamedSymVar = (SW, String) Source #
NamedSymVar pairs symbolic words and user given/automatically generated names
getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int Source #
Create a new table; hash-cons as necessary
A program is a sequence of assignments
Constructors
| SBVPgm | |
Fields
| |
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.
class SExecutable a where Source #
Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use
cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.
Instances
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
The state of the symbolic interpreter
getPathCondition :: State -> SBool Source #
Get the current path condition
extendPathCondition :: State -> (SBool -> SBool) -> State Source #
Extend the path condition with the given test value.
inProofMode :: State -> Bool Source #
Are we running in proof mode?
data SBVRunMode Source #
Different means of running a symbolic piece of code
Kind of symbolic value
class Outputtable a where Source #
A class representing what can be returned from a symbolic computation.
Minimal complete definition
Methods
output :: a -> Symbolic a Source #
Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.
Instances
| Outputtable () Source # | |
| Outputtable a => Outputtable [a] Source # | |
| Outputtable (SBV a) Source # | |
| (Outputtable a, Outputtable b) => Outputtable (a, b) Source # | |
| (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) Source # | |
| (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) Source # | |
| (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) Source # | |
| (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) Source # | |
| (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) Source # | |
| (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) Source # | |
Result of running a symbolic computation
Constructors
| Result | |
Fields
| |
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 |
data SMTLibLogic Source #
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 Source # | |
| NFData SMTLibLogic Source # | NFData instance for SMTLibLogic |
addConstraint :: Maybe String -> Maybe Double -> SBool -> SBool -> Symbolic () Source #
Add a constraint with a given probability.
internalVariable :: State -> Kind -> IO SW Source #
Create an internal variable, which acts as an input but isn't visible to the user. Such variables are existentially quantified in a SAT context, and universally quantified in a proof context.
internalConstraint :: State -> Maybe String -> SVal -> IO () Source #
Require a boolean condition to be true in the state. Only used for internal purposes.
isCodeGenMode :: State -> Bool Source #
Is this a CodeGen run? (i.e., generating code)
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
addAxiom :: String -> [String] -> Symbolic () Source #
Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.
data Quantifier Source #
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
Instances
needsExistentials :: [Quantifier] -> Bool Source #
Are there any existential quantifiers?
Representation of an SMT-Lib program. In between pre and post goes the refuted models
Constructors
| SMTLibPgm SMTLibVersion [String] |
data SMTLibVersion Source #
Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.
Constructors
| SMTLib2 |
smtLibVersionExtension :: SMTLibVersion -> String Source #
The extension associated with the version
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.
data SolverCapabilities Source #
Translation tricks needed for specific capabilities afforded by each solver
Constructors
| SolverCapabilities | |
Fields
| |
extractSymbolicSimulationState :: State -> IO Result Source #
Grab the program from a running symbolic simulation state. This is useful for internal purposes, for
instance when implementing sBranch.
A script, to be passed to the solver.
Constructors
| SMTScript | |
Fields
| |
Solvers that SBV is aware of
An SMT solver
Constructors
| SMTSolver | |
Fields
| |
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 |
A model, as returned by a solver
Constructors
| SMTModel | |
Fields
| |
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
| |
getSBranchRunConfig :: State -> Maybe SMTConfig Source #
If in proof mode, get the underlying configuration (used for sBranch)
declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b) Source #
Declare a new symbolic array, with a potential initial value
declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b) Source #
Declare a new functional symbolic array, with a potential initial value. Note that a read from an uninitialized cell will result in an error.
data OptimizeStyle Source #
Style of optimization
Constructors
| Lexicographic | Objectives are optimized in the order given, earlier objectives have higher priority. This is the default. |
| Independent | Each objective is optimized independently. |
| Pareto | Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. |
Instances
Penalty for a soft-assertion. The default penalty is 1, with all soft-assertions belonging
to the same objective goal. A positive weight and an optional group can be provided by using
the Penalty constructor.
Constructors
| DefaultPenalty | Default: Penalty of |
| Penalty Rational (Maybe String) | Penalty with a weight and an optional group |
Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.
Solver tactic
Constructors
| CaseSplit Bool [(String, a, [Tactic a])] | Case-split, with implicit coverage. Bool says whether we should be verbose. |
| CheckCaseVacuity Bool | Should the case-splits be checked for vacuity? (Default: True.) |
| ParallelCase | Run case-splits in parallel. (Default: Sequential.) |
| CheckConstrVacuity Bool | Should "constraints" be checked for vacuity? (Default: False.) |
| StopAfter Int | Time-out given to solver, in seconds. |
| CheckUsing String | Invoke with check-sat-using command, instead of check-sat |
| UseLogic Logic | Use this logic, a custom one can be specified too |
| UseSolver SMTConfig | Use this solver (z3, yices, etc.) |
| OptimizePriority OptimizeStyle | Use this style for optimize calls. (Default: Lexicographic) |
A case condition (internal)
Constructors
| NoCase | No case-split |
| CasePath [SW] | In a case-path |
| CaseVac [SW] SW | For checking the vacuity of a case |
| CaseCov [SW] [SW] | In a case-path end, coverage (first arg is path cond, second arg is coverage cond) |
| CstrVac | In a constraint vacuity check (top-level) |
| Opt [Objective (SW, SW)] | In an optimization call |
data SMTProblem Source #
Internal representation of a symbolic simulation result
Constructors
| SMTProblem | |
Fields
| |
Instances
isParallelCaseAnywhere :: Tactic a -> Bool Source #
Is there a parallel-case anywhere?
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
| |
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)
Getting SMT-Lib output (for offline analysis)
Arguments
| :: Provable a | |
| => SMTLibVersion | Version of SMTLib to compile to. (Only SMTLib2 supported currently.) |
| -> Bool | If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.) |
| -> a | |
| -> 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. IfFalse, 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 :: Provable a => Bool -> FilePath -> a -> IO () Source #
Create SMT-Lib benchmarks, for supported versions of SMTLib. The first argument is the basename of the file.
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.)
Compilation to C, extras
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
Code generation primitives
The codegen monad
newtype SBVCodeGen a Source #
The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.
Constructors
| SBVCodeGen (StateT CgState Symbolic a) |
Instances
Specifying inputs, SBV variants
cgInput :: SymWord a => String -> SBVCodeGen (SBV a) Source #
Creates an atomic input in the generated code.
cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] Source #
Creates an array input in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen () Source #
Creates an atomic output in the generated code.
cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen () Source #
Creates an array output in the generated code.
cgReturn :: SBV a -> SBVCodeGen () Source #
Creates a returned (unnamed) value in the generated code.
cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen () Source #
Creates a returned (unnamed) array value in the generated code.
Specifying inputs, SVal variants
svCgInput :: Kind -> String -> SBVCodeGen SVal Source #
Creates an atomic input in the generated code.
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] Source #
Creates an array input in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen () Source #
Creates an atomic output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen () Source #
Creates an array output in the generated code.
svCgReturn :: SVal -> SBVCodeGen () Source #
Creates a returned (unnamed) value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen () Source #
Creates a returned (unnamed) array value in the generated code.
Settings
cgPerformRTCs :: Bool -> SBVCodeGen () Source #
Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: False.
cgSetDriverValues :: [Integer] -> SBVCodeGen () Source #
Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
cgAddPrototype :: [String] -> SBVCodeGen () Source #
Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen () Source #
Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddLDFlags :: [String] -> SBVCodeGen () Source #
Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
cgIgnoreSAssert :: Bool -> SBVCodeGen () Source #
Ignore assertions (those generated by sAssert calls) in the generated C code
cgIntegerSize :: Int -> SBVCodeGen () Source #
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 () Source #
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 Source #
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 Source # | |
| Show CgSRealType Source # |
|
Infrastructure
class CgTarget a where Source #
Abstract over code generation for different languages
Minimal complete definition
Options for code-generation.
Constructors
| CgConfig | |
Fields
| |
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.
defaultCgConfig :: CgConfig Source #
Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
initCgState :: CgState Source #
Initial configuration for code-generation
isCgDriver :: CgPgmKind -> Bool Source #
Is this a driver program?
isCgMakefile :: CgPgmKind -> Bool Source #
Is this a make file?
Generating collateral
cgGenerateDriver :: Bool -> SBVCodeGen () Source #
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 () Source #
Should we generate a Makefile? Default: True.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle Source #
Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection of makefiles, source code, headers, etc.
renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO () Source #
Render a code-gen bundle to a directory or to stdout
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!