| 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
- supportsDTConstructorSigs :: Bool
- supportsDTAccessorSigs :: 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
- 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 Quantifier -> Kind -> Maybe String -> m (SBV a)
- data ArrayContext
- = ArrayFree (Maybe SV)
- | ArrayMutate ArrayIndex SV SV
- | ArrayMerge SV ArrayIndex ArrayIndex
- type ArrayInfo = (String, (Kind, Kind), ArrayContext)
- class SymArray array where
- newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
- newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
- readArray :: array a b -> SBV a -> SBV b
- writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b
- mergeArrays :: SymVal b => SBV Bool -> array a b -> array a b -> array a b
- newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
- newtype SFunArray a b = SFunArray {}
- newtype SArray a b = SArray {}
- sbvToSV :: State -> SBV a -> IO SV
- sbvToSymSV :: MonadSymbolic m => SBV a -> m SV
- forceSVArg :: SV -> IO ()
- data SBVExpr = SBVApp !Op ![SV]
- newExpr :: State -> Kind -> SBVExpr -> IO SV
- cache :: (State -> IO a) -> Cached a
- data Cached a
- uncache :: Cached SV -> State -> IO SV
- uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
- 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
- isUnbounded :: a -> Bool
- isUninterpreted :: a -> Bool
- isChar :: a -> Bool
- isString :: a -> Bool
- isList :: a -> Bool
- isSet :: a -> Bool
- isTuple :: a -> Bool
- isMaybe :: a -> Bool
- isEither :: a -> Bool
- showType :: a -> String
- data Op
- = Plus
- | Times
- | Minus
- | UNeg
- | Abs
- | Quot
- | Rem
- | Equal
- | NotEqual
- | LessThan
- | GreaterThan
- | LessEq
- | GreaterEq
- | Ite
- | And
- | Or
- | XOr
- | Not
- | Shl
- | Shr
- | Rol Int
- | Ror Int
- | Extract Int Int
- | Join
- | LkUp (Int, Kind, Kind, Int) !SV !SV
- | ArrEq ArrayIndex ArrayIndex
- | ArrRead ArrayIndex
- | KindCast Kind Kind
- | Uninterpreted String
- | Label String
- | IEEEFP FPOp
- | PseudoBoolean PBOp
- | OverflowOp OvOp
- | StrOp StrOp
- | SeqOp SeqOp
- | SetOp SetOp
- | TupleConstructor Int
- | TupleAccess Int Int
- | EitherConstructor Kind Kind Bool
- | EitherIs Kind Kind Bool
- | EitherAccess Bool
- | MaybeConstructor Kind Bool
- | MaybeIs Kind Bool
- | MaybeAccess
- data PBOp
- data FPOp
- data StrOp
- data SeqOp
- data RegExp
- type NamedSymVar = (SV, String)
- getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int
- newtype SBVPgm = SBVPgm {
- pgmAssignments :: Seq (SV, SBVExpr)
- type Symbolic = SymbolicT IO
- runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result)
- data State
- getPathCondition :: State -> SBool
- extendPathCondition :: State -> (SBool -> SBool) -> State
- inSMTMode :: State -> IO Bool
- data SBVRunMode
- = SMTMode QueryContext IStage Bool SMTConfig
- | CodeGen
- | Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]))
- data Kind
- class Outputtable a where
- output :: MonadSymbolic m => a -> m a
- 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]
- class SolverContext m where
- constrain :: SBool -> m ()
- softConstrain :: SBool -> m ()
- namedConstraint :: String -> SBool -> m ()
- constrainWithAttribute :: [(String, String)] -> SBool -> m ()
- setInfo :: String -> [String] -> m ()
- setOption :: SMTOption -> m ()
- setLogic :: Logic -> m ()
- setTimeOut :: Integer -> m ()
- contextState :: m State
- internalVariable :: State -> Kind -> IO SV
- internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
- isCodeGenMode :: State -> IO Bool
- newtype SBVType = SBVType [Kind]
- newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
- addAxiom :: MonadSymbolic m => String -> [String] -> m ()
- data Quantifier
- needsExistentials :: [Quantifier] -> Bool
- data SMTLibPgm = SMTLibPgm SMTLibVersion [String]
- data SMTLibVersion = SMTLib2
- smtLibVersionExtension :: SMTLibVersion -> String
- smtLibReservedNames :: [String]
- 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
- supportsDTConstructorSigs :: Bool
- supportsDTAccessorSigs :: Bool
- supportsFlattenedModels :: Maybe [String]
- extractSymbolicSimulationState :: State -> IO Result
- data SMTScript = SMTScript {
- scriptBody :: String
- scriptModel :: [String]
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: String -> String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- data SMTResult
- data SMTModel = SMTModel {
- modelObjectives :: [(String, GeneralizedCV)]
- modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
- modelAssocs :: [(String, CV)]
- modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- satTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- allowQuantifiedQueries :: Bool
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)
- data Penalty
- data Objective a
- data QueryState = QueryState {
- queryAsk :: Maybe Int -> String -> IO String
- querySend :: Maybe Int -> String -> IO ()
- queryRetrieveResponse :: Maybe Int -> IO String
- queryConfig :: SMTConfig
- queryTerminate :: IO ()
- queryTimeOutValue :: Maybe Int
- queryAssertionStackDepth :: Int
- queryTblArrPreserveIndex :: Maybe (Int, Int)
- newtype QueryT m a = QueryT {}
- newtype SMTProblem = SMTProblem {}
- genLiteral :: Integral a => Kind -> a -> SBV b
- genFromCV :: Integral a => CV -> a
- data CV = CV {}
- genMkSymVar :: MonadSymbolic m => Kind -> Maybe Quantifier -> Maybe String -> m (SBV a)
- genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV])
- showModel :: SMTConfig -> SMTModel -> String
- data SMTModel = SMTModel {
- modelObjectives :: [(String, GeneralizedCV)]
- modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
- modelAssocs :: [(String, CV)]
- modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
- liftQRem :: (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (Ord a, SymVal a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
- registerKind :: State -> Kind -> IO ()
- compileToC' :: String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle)
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO (CgConfig, CgPgmBundle)
- newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
- cgSym :: Symbolic a -> SBVCodeGen a
- cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
- cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
- cgOutput :: String -> SBV a -> SBVCodeGen ()
- cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
- cgReturn :: SBV a -> SBVCodeGen ()
- cgReturnArr :: SymVal 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 ()
- cgOverwriteFiles :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
- class CgTarget a where
- targetName :: a -> String
- translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
- data CgConfig = CgConfig {
- cgRTC :: Bool
- cgInteger :: Maybe Int
- cgReal :: Maybe CgSRealType
- cgDriverVals :: [Integer]
- cgGenDriver :: Bool
- cgGenMakefile :: Bool
- cgIgnoreAsserts :: Bool
- cgOverwriteGenerated :: 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 (CgConfig, CgPgmBundle)
- renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
- 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
- fpCompareObjectH :: RealFloat a => a -> a -> Ordering
- fpIsNormalizedH :: RealFloat a => a -> Bool
- class PrettyNum a where
- readBin :: Num a => String -> a
- shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
- chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
- shexI :: Bool -> Bool -> Integer -> String
- sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
- sbinI :: Bool -> Bool -> Integer -> String
- showCFloat :: Float -> String
- showCDouble :: Double -> String
- showHFloat :: Float -> String
- showHDouble :: Double -> String
- showSMTFloat :: RoundingMode -> Float -> String
- showSMTDouble :: RoundingMode -> Double -> String
- smtRoundingMode :: RoundingMode -> String
- cvToSMTLib :: RoundingMode -> CV -> String
- mkSkolemZero :: RoundingMode -> Kind -> String
- data Timing
- showTDiff :: NominalDiffTime -> String
- sendStringToSolver :: (MonadIO m, MonadQuery m) => String -> m ()
- sendRequestToSolver :: (MonadIO m, MonadQuery m) => String -> m String
- retrieveResponseFromSolver :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
- addSValOptGoal :: MonadSymbolic m => Objective SVal -> m ()
- sFloatAsComparableSWord32 :: SFloat -> SWord32
- sDoubleAsComparableSWord64 :: SDouble -> SWord64
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
Constructors
| SMTMode QueryContext IStage Bool SMTConfig | In regular mode, with a stage. Bool is True if this is SAT. |
| CodeGen | Code generation mode. |
| Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)])) | Concrete simulation mode, with given environment if any. If Nothing: Random. |
Instances
| Show SBVRunMode Source # | |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> SBVRunMode -> ShowS # show :: SBVRunMode -> String # showList :: [SBVRunMode] -> ShowS # | |
data QueryContext Source #
Query execution context
Constructors
| QueryInternal | Triggered from inside SBV |
| QueryExternal | Triggered from user code |
Instances
| Show QueryContext Source # | Show instance for |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> QueryContext -> ShowS # show :: QueryContext -> String # showList :: [QueryContext] -> ShowS # | |
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
type SChar = SBV Char Source #
A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character
set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based
on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV
character for the time being. This limitation is due to the SMT-solvers only supporting this
particular subset. However, there is a pending proposal to add support for unicode, and SBV
will track these changes to have full unicode support as solvers become available. For
details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml
type SString = SBV String Source #
A symbolic string. Note that a symbolic string is not a list of symbolic characters,
that is, it is not the case that SString = [SChar], unlike what one might expect following
Haskell strings. An SString is a symbolic value of its own, of possibly arbitrary but finite length,
and internally processed as one unit as opposed to a fixed-length list of characters.
type SList a = SBV [a] Source #
A symbolic list of items. Note that a symbolic list is not a list of symbolic items,
that is, it is not the case that SList a = [a], unlike what one might expect following
haskell lists/sequences. An SList is a symbolic value of its own, of possibly arbitrary but finite
length, and internally processed as one unit as opposed to a fixed-length list of items.
Note that lists can be nested, i.e., we do allow lists of lists of ... items.
A RCSet is either a regular set or a set given by its complement from the corresponding universal set.
Constructors
| RegularSet (Set a) | |
| ComplementSet (Set a) |
Instances
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
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 RoundTowardPositive
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, Typeable a) => SymVal a where Source #
A SymVal is a potential symbolic value that can be created instances of to be fed to a symbolic program.
Minimal complete definition
Nothing
Methods
mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV a) Source #
Generalization of mkSymVal
literal :: a -> SBV a Source #
Turn a literal constant to symbolic
Extract a literal, from a CV representation
isConcretely :: SBV a -> (a -> Bool) -> Bool Source #
Does it concretely satisfy the given predicate?
mkSymVal :: (MonadSymbolic m, Read a, Data a) => Maybe Quantifier -> Maybe String -> m (SBV a) Source #
Generalization of mkSymVal
literal :: Show a => a -> SBV a Source #
Turn a literal constant to symbolic
fromCV :: Read a => CV -> a Source #
Extract a literal, from a CV representation
forall :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of forall
forall_ :: MonadSymbolic m => m (SBV a) Source #
Generalization of forall_
mkForallVars :: MonadSymbolic m => Int -> m [SBV a] Source #
Generalization of mkForallVars
exists :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of exists
exists_ :: MonadSymbolic m => m (SBV a) Source #
Generalization of exists_
mkExistVars :: MonadSymbolic m => Int -> m [SBV a] Source #
Generalization of mkExistVars
free :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of free
free_ :: MonadSymbolic m => m (SBV a) Source #
Generalization of free_
mkFreeVars :: MonadSymbolic m => Int -> m [SBV a] Source #
Generalization of mkFreeVars
symbolic :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of symbolic
symbolics :: MonadSymbolic m => [String] -> m [SBV a] Source #
Generalization of symbolics
unliteral :: SBV a -> Maybe a Source #
Extract a literal, if the value is concrete
isConcrete :: SBV a -> Bool Source #
Is the symbolic word concrete?
isSymbolic :: SBV a -> Bool Source #
Is the symbolic word really symbolic?
Instances
CV represents a concrete word of a fixed size:
For signed words, the most significant digit is considered to be the sign.
Instances
| Eq CV Source # | |
| Ord CV Source # | |
| Show CV Source # | Show instance for |
| NFData CV Source # | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind CV Source # |
|
Defined in Data.SBV.Core.Concrete Methods hasSign :: CV -> Bool Source # intSizeOf :: CV -> Int Source # isBoolean :: CV -> Bool Source # isBounded :: CV -> Bool Source # isFloat :: CV -> Bool Source # isDouble :: CV -> Bool Source # isUnbounded :: CV -> Bool Source # isUninterpreted :: CV -> Bool Source # isString :: CV -> Bool Source # isTuple :: CV -> Bool Source # isMaybe :: CV -> Bool Source # | |
| PrettyNum CV Source # | |
| SatModel CV Source # |
|
| SDivisible CV Source # | |
A constant value
Constructors
| CAlgReal !AlgReal | Algebraic real |
| CInteger !Integer | Bit-vector/unbounded integer |
| CFloat !Float | Float |
| CDouble !Double | Double |
| CChar !Char | Character |
| CString !String | String |
| CList ![CVal] | List |
| CSet !(RCSet CVal) | Set. Can be regular or complemented. |
| CUserSort !(Maybe Int, String) | Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations |
| CTuple ![CVal] | Tuple |
| CMaybe !(Maybe CVal) | Maybe |
| CEither !(Either CVal CVal) | Disjoint union |
Instances
| Eq CVal Source # | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal 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 CVal Source # | Ord instance for VWVal. 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 | bool says it's exact (i.e., SMT-solver did not return it with ? at the end.) |
| AlgPolyRoot (Integer, AlgRealPoly) (Maybe String) | which root of this polynomial and an approximate decimal representation with given precision, if available |
Instances
newtype AlgRealPoly Source #
A univariate polynomial, represented simply as a coefficient list. For instance, "5x^3 + 2x - 5" is represented as [(5, 3), (2, 1), (-5, 0)]
Constructors
| AlgRealPoly [(Integer, Integer)] |
Instances
| Eq AlgRealPoly Source # | |
Defined in Data.SBV.Core.AlgReals | |
| Ord AlgRealPoly Source # | |
Defined in Data.SBV.Core.AlgReals Methods compare :: AlgRealPoly -> AlgRealPoly -> Ordering # (<) :: AlgRealPoly -> AlgRealPoly -> Bool # (<=) :: AlgRealPoly -> AlgRealPoly -> Bool # (>) :: AlgRealPoly -> AlgRealPoly -> Bool # (>=) :: AlgRealPoly -> AlgRealPoly -> Bool # max :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly # min :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly # | |
| Show AlgRealPoly Source # | |
Defined in Data.SBV.Core.AlgReals Methods showsPrec :: Int -> AlgRealPoly -> ShowS # show :: AlgRealPoly -> String # showList :: [AlgRealPoly] -> ShowS # | |
A simple expression type over extendent values, covering infinity, epsilon and intervals.
Constructors
| Infinite Kind | |
| Epsilon Kind | |
| Interval ExtCV ExtCV | |
| BoundedCV CV | |
| AddExtCV ExtCV ExtCV | |
| MulExtCV ExtCV ExtCV |
Instances
| Show ExtCV Source # | Show instance, shows with the kind |
| HasKind ExtCV Source # | Kind instance for Extended CV |
Defined in Data.SBV.Core.Concrete Methods kindOf :: ExtCV -> Kind Source # hasSign :: ExtCV -> Bool Source # intSizeOf :: ExtCV -> Int Source # isBoolean :: ExtCV -> Bool Source # isBounded :: ExtCV -> Bool Source # isReal :: ExtCV -> Bool Source # isFloat :: ExtCV -> Bool Source # isDouble :: ExtCV -> Bool Source # isUnbounded :: ExtCV -> Bool Source # isUninterpreted :: ExtCV -> Bool Source # isChar :: ExtCV -> Bool Source # isString :: ExtCV -> Bool Source # isList :: ExtCV -> Bool Source # isSet :: ExtCV -> Bool Source # isTuple :: ExtCV -> Bool Source # isMaybe :: ExtCV -> Bool Source # | |
data GeneralizedCV Source #
A generalized CV allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
Constructors
| ExtendedCV ExtCV | |
| RegularCV CV |
Instances
isRegularCV :: GeneralizedCV -> Bool Source #
Is this a regular 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 Source #
Lift a binary function through a CV.
mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (Char -> Char) -> (String -> String) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV Source #
Map a unary function through a 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 Source #
Map a binary function through a CV.
A symbolic word, tracking it's signedness and size.
Instances
| Eq SV Source # | |
| Ord SV Source # | |
| Show SV Source # | |
| NFData SV Source # | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind SV Source # | |
Defined in Data.SBV.Core.Symbolic Methods hasSign :: SV -> Bool Source # intSizeOf :: SV -> Int Source # isBoolean :: SV -> Bool Source # isBounded :: SV -> Bool Source # isFloat :: SV -> Bool Source # isDouble :: SV -> Bool Source # isUnbounded :: SV -> Bool Source # isUninterpreted :: SV -> Bool Source # isString :: SV -> Bool Source # isTuple :: SV -> Bool Source # isMaybe :: SV -> Bool Source # | |
Normalize a CV. 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 # | This instance is only defined so that we can define an instance for
|
| Show SVal Source # | |
| NFData SVal Source # | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind SVal Source # | |
Defined in Data.SBV.Core.Symbolic Methods kindOf :: SVal -> Kind Source # hasSign :: SVal -> Bool Source # intSizeOf :: SVal -> Int Source # isBoolean :: SVal -> Bool Source # isBounded :: SVal -> Bool Source # isReal :: SVal -> Bool Source # isFloat :: SVal -> Bool Source # isDouble :: SVal -> Bool Source # isUnbounded :: SVal -> Bool Source # isUninterpreted :: SVal -> Bool Source # isChar :: SVal -> Bool Source # isString :: SVal -> Bool Source # isList :: SVal -> Bool Source # isSet :: SVal -> Bool Source # isTuple :: SVal -> Bool Source # isMaybe :: SVal -> Bool Source # | |
| ArithOverflow SVal Source # | |
Defined in Data.SBV.Tools.Overflow | |
| Testable (Symbolic SVal) Source # | |
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.