| 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
- 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
- Pretty number printing
- Timing computations
- Coordinating with the solver
- Defining new metrics
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.
NB. There are various coding invariants in SBV that are maintained throughout the code. Indiscriminate use of functions in this module can break those invariants. So, you are on your own if you do utilize the functions here. (Unfortunately, what exactly those invariants are is a very good but also a very difficult question to answer!)
Synopsis
- data Result = Result {
- reskinds :: Set Kind
- resTraces :: [(String, CV)]
- resObservables :: [(String, CV -> Bool, SV)]
- resUISegs :: [(String, [String])]
- resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
- resConsts :: [(SV, CV)]
- resTables :: [((Int, Kind, Kind), [SV])]
- resArrays :: [(Int, ArrayInfo)]
- resUIConsts :: [(String, SBVType)]
- resAxioms :: [(String, [String])]
- resAsgns :: SBVPgm
- resConstraints :: Seq (Bool, [(String, String)], SV)
- resAssertions :: [(String, Maybe CallStack, SV)]
- resOutputs :: [SV]
- data SBVRunMode
- = SMTMode QueryContext IStage Bool SMTConfig
- | CodeGen
- | Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]))
- data IStage
- data QueryContext
- data SolverCapabilities = SolverCapabilities {
- supportsQuantifiers :: Bool
- supportsUninterpretedSorts :: Bool
- supportsUnboundedInts :: Bool
- supportsReals :: Bool
- supportsApproxReals :: Bool
- supportsIEEE754 :: Bool
- supportsSets :: Bool
- supportsOptimization :: Bool
- supportsPseudoBooleans :: Bool
- supportsCustomQueries :: Bool
- supportsGlobalDecls :: Bool
- supportsDataTypes :: Bool
- supportsFlattenedModels :: Maybe [String]
- 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
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- type SEither a b = SBV (Either a b)
- type SMaybe a = SBV (Maybe a)
- type STuple a b = SBV (a, b)
- type STuple2 a b = SBV (a, b)
- type STuple3 a b c = SBV (a, b, c)
- type STuple4 a b c d = SBV (a, b, c, d)
- type STuple5 a b c d e = SBV (a, b, c, d, e)
- type STuple6 a b c d e f = SBV (a, b, c, d, e, f)
- type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)
- type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)
- data RCSet a
- = RegularSet (Set a)
- | ComplementSet (Set a)
- type SSet a = SBV (RCSet a)
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymVal a) => SBV a
- sInfinity :: (Floating a, SymVal 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, Typeable a) => SymVal a where
- mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV a)
- literal :: a -> SBV a
- fromCV :: CV -> a
- isConcretely :: SBV a -> (a -> Bool) -> Bool
- forall :: MonadSymbolic m => String -> m (SBV a)
- forall_ :: MonadSymbolic m => m (SBV a)
- mkForallVars :: MonadSymbolic m => Int -> m [SBV a]
- exists :: MonadSymbolic m => String -> m (SBV a)
- exists_ :: MonadSymbolic m => m (SBV a)
- mkExistVars :: MonadSymbolic m => Int -> m [SBV a]
- free :: MonadSymbolic m => String -> m (SBV a)
- free_ :: MonadSymbolic m => m (SBV a)
- mkFreeVars :: MonadSymbolic m => Int -> m [SBV a]
- symbolic :: MonadSymbolic m => String -> m (SBV a)
- symbolics :: MonadSymbolic m => [String] -> m [SBV a]
- unliteral :: SBV a -> Maybe a
- isConcrete :: SBV a -> Bool
- isSymbolic :: SBV a -> Bool
- data CV = CV {}
- data CVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, AlgRealPoly) (Maybe String)
- newtype AlgRealPoly = AlgRealPoly [(Integer, Integer)]
- data ExtCV
- data GeneralizedCV
- isRegularCV :: GeneralizedCV -> Bool
- cvSameType :: CV -> CV -> Bool
- cvToBool :: CV -> Bool
- mkConstCV :: Integral a => Kind -> a -> CV
- liftCV2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ([CVal] -> [CVal] -> b) -> ([CVal] -> [CVal] -> b) -> (Maybe CVal -> Maybe CVal -> b) -> (Either CVal CVal -> Either CVal CVal -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CV -> CV -> b
- mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (Char -> Char) -> (String -> String) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV
- mapCV2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (Char -> Char -> Char) -> (String -> String -> String) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV -> CV
- data SV = SV !Kind !NodeId
- trueSV :: SV
- falseSV :: SV
- trueCV :: CV
- falseCV :: CV
- normCV :: CV -> CV
- data SVal = SVal !Kind !(Either CV (Cached SV))
- sTrue :: SBool
- sFalse :: SBool
- sNot :: SBool -> SBool
- (.&&) :: SBool -> SBool -> SBool
- (.||) :: SBool -> SBool -> SBool
- (.<+>) :: SBool -> SBool -> SBool
- (.~&) :: SBool -> SBool -> SBool
- (.~|) :: SBool -> SBool -> SBool
- (.=>) :: SBool -> SBool -> SBool
- (.<=>) :: SBool -> SBool -> SBool
- sAnd :: [SBool] -> SBool
- sOr :: [SBool] -> SBool
- sAny :: (a -> SBool) -> [a] -> SBool
- sAll :: (a -> SBool) -> [a] -> SBool
- fromBool :: Bool -> SBool
- newtype SBV a = SBV {}
- newtype NodeId = NodeId Int
- mkSymSBV :: forall a m. MonadSymbolic m => Maybe