| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| 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 :: (CnstMap, [(SV, CV)])
- resTables :: [((Int, Kind, Kind), [SV])]
- resArrays :: [(Int, ArrayInfo)]
- resUIConsts :: [(String, SBVType)]
- resAxioms :: [(Bool, 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 VarContext
- data SolverCapabilities = SolverCapabilities {
- supportsQuantifiers :: Bool
- supportsDefineFun :: Bool
- supportsDistinct :: Bool
- supportsBitVectors :: Bool
- supportsUninterpretedSorts :: Bool
- supportsUnboundedInts :: Bool
- supportsInt2bv :: Bool
- supportsReals :: Bool
- supportsApproxReals :: Bool
- supportsDeltaSat :: Maybe String
- supportsIEEE754 :: Bool
- supportsSets :: Bool
- supportsOptimization :: Bool
- supportsPseudoBooleans :: Bool
- supportsCustomQueries :: Bool
- supportsGlobalDecls :: Bool
- supportsDataTypes :: Bool
- supportsDirectAccessors :: 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 SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)
- type SFPHalf = SBV FPHalf
- type SFPBFloat = SBV FPBFloat
- type SFPSingle = SBV FPSingle
- type SFPDouble = SBV FPDouble
- type SFPQuad = SBV FPQuad
- type SRational = SBV Rational
- 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 => VarContext -> Maybe String -> m (SBV a)
- literal :: a -> SBV a
- fromCV :: CV -> a
- isConcretely :: SBV a -> (a -> Bool) -> Bool
- sbvForall :: MonadSymbolic m => String -> m (SBV a)
- sbvForall_ :: MonadSymbolic m => m (SBV a)
- mkForallVars :: MonadSymbolic m => Int -> m [SBV a]
- sbvExists :: MonadSymbolic m => String -> m (SBV a)
- sbvExists_ :: 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) -> (FP -> FP -> b) -> (Rational -> Rational -> 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) -> (FP -> FP) -> (Rational -> Rational) -> (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) -> (FP -> FP -> FP) -> (Rational -> Rational -> Rational) -> (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 {}
- mkSymSBV :: forall a m. MonadSymbolic m => VarContext -> 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)
- sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> 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 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
- isRational :: a -> Bool
- isFP :: a -> Bool
- isUnbounded :: a -> Bool
- isUserSort :: 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
- | ZeroExtend Int
- | SignExtend Int
- | LkUp (Int, Kind, Kind, Int) !SV !SV
- | ArrEq ArrayIndex ArrayIndex
- | ArrRead ArrayIndex
- | KindCast Kind Kind
- | Uninterpreted String
- | Label String
- | IEEEFP FPOp
- | NonLinear NROp
- | OverflowOp OvOp
- | PseudoBoolean PBOp
- | StrOp StrOp
- | RegExOp RegExOp
- | SeqOp SeqOp
- | SetOp SetOp
- | TupleConstructor Int
- | TupleAccess Int Int
- | EitherConstructor Kind Kind Bool
- | EitherIs Kind Kind Bool
- | EitherAccess Bool
- | RationalConstructor
- | MaybeConstructor Kind Bool
- | MaybeIs Kind Bool
- | MaybeAccess
- data PBOp
- data FPOp
- data StrOp
- data RegExOp
- data SeqOp
- data RegExp
- data NamedSymVar = NamedSymVar !SV !Name
- 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 :: (CnstMap, [(SV, CV)])
- resTables :: [((Int, Kind, Kind), [SV])]
- resArrays :: [(Int, ArrayInfo)]
- resUIConsts :: [(String, SBVType)]
- resAxioms :: [(Bool, 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 ()
- addAxiom :: String -> [String] -> m ()
- addSMTDefinition :: String -> [String] -> 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 ()
- data Quantifier
- needsExistentials :: [Quantifier] -> Bool
- data SMTLibPgm = SMTLibPgm SMTLibVersion [String]
- data SMTLibVersion = SMTLib2
- smtLibVersionExtension :: SMTLibVersion -> String
- smtLibReservedNames :: [String]
- data SolverCapabilities = SolverCapabilities {
- supportsQuantifiers :: Bool
- supportsDefineFun :: Bool
- supportsDistinct :: Bool
- supportsBitVectors :: Bool
- supportsUninterpretedSorts :: Bool
- supportsUnboundedInts :: Bool
- supportsInt2bv :: Bool
- supportsReals :: Bool
- supportsApproxReals :: Bool
- supportsDeltaSat :: Maybe String
- supportsIEEE754 :: Bool
- supportsSets :: Bool
- supportsOptimization :: Bool
- supportsPseudoBooleans :: Bool
- supportsCustomQueries :: Bool
- supportsGlobalDecls :: Bool
- supportsDataTypes :: Bool
- supportsDirectAccessors :: 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
- crackNum :: Bool
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- satTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- dsatPrecision :: Maybe Double
- solver :: SMTSolver
- extraArgs :: [String]
- 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
- 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 -> VarContext -> 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 ()
- svToSV :: State -> SVal -> IO SV
- compileToC' :: String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
- compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], 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 ()
- cgShowU8UsingHex :: 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
- cgShowU8InHex :: 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 a -> IO (a, 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
- floatToWord :: Float -> Word32
- wordToFloat :: Word32 -> Float
- doubleToWord :: Double -> Word64
- wordToDouble :: Word64 -> Double
- 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
- showBFloat :: (Show a, RealFloat a) => a -> ShowS
- showFloatAtBase :: (Show a, RealFloat a) => Int -> a -> ShowS
- showSMTFloat :: RoundingMode -> Float -> String
- showSMTDouble :: RoundingMode -> Double -> String
- smtRoundingMode :: RoundingMode -> String
- cvToSMTLib :: RoundingMode -> CV -> String
- mkSkolemZero :: RoundingMode -> Kind -> String
- showNegativeNumber :: (Show a, Num a, Ord a) => a -> 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
- sFloatingPointAsComparableSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
- sComparableSWord32AsSFloat :: SWord32 -> SFloat
- sComparableSWord64AsSDouble :: SWord64 -> SDouble
- sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
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 # | |
data VarContext Source #
Which context is this variable being created?
Constructors
| NonQueryVar (Maybe Quantifier) | |
| QueryVar |
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 SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) Source #
A symbolic arbitrary precision floating point value
type SChar = SBV Char Source #
A symbolic character. Note that this is the full unicode character set. see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml for details.
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
sNaN :: (Floating a, SymVal a) => SBV a Source #
Symbolic variant of Not-A-Number. This value will inhabit
SFloat, SDouble and SFloatingPoint. types.
sInfinity :: (Floating a, SymVal a) => SBV a Source #
Symbolic variant of infinity. This value will inhabit both
SFloat, SDouble and SFloatingPoint. types.
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 => VarContext -> Maybe String -> m (SBV a) Source #
Generalization of mkSymVal
default mkSymVal :: (MonadSymbolic m, Read a, Data a) => VarContext -> Maybe String -> m (SBV a) Source #
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?
sbvForall :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of sbvForall
sbvForall_ :: MonadSymbolic m => m (SBV a) Source #
Generalization of sbvForall_
mkForallVars :: MonadSymbolic m => Int -> m [SBV a] Source #
Generalization of mkForallVars
sbvExists :: MonadSymbolic m => String -> m (SBV a) Source #
Generalization of sbvExists
sbvExists_ :: MonadSymbolic m => m (SBV a) Source #
Generalization of sbvExists_
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
| Show CV Source # | Show instance for |
| NFData CV Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Eq CV Source # | |
| Ord CV Source # | |
| 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 # isRational :: CV -> Bool Source # isUnbounded :: CV -> Bool Source # isUserSort :: CV -> Bool Source # isString :: CV -> Bool Source # isTuple :: CV -> Bool Source # isMaybe :: CV -> Bool Source # | |
| SDivisible CV Source # | |
| SatModel CV Source # |
|
| PrettyNum CV Source # | |
A constant value
Constructors
| CAlgReal !AlgReal | Algebraic real |
| CInteger !Integer | Bit-vector/unbounded integer |
| CFloat !Float | Float |
| CDouble !Double | Double |
| CFP !FP | Arbitrary float |
| CRational Rational | Rational |
| 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 |
| AlgInterval (RealPoint Rational) (RealPoint Rational) | interval, with low and high bounds |
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
| Show AlgRealPoly Source # | |
Defined in Data.SBV.Core.AlgReals Methods showsPrec :: Int -> AlgRealPoly -> ShowS # show :: AlgRealPoly -> String # showList :: [AlgRealPoly] -> ShowS # | |
| 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 # | |
A simple expression type over extended 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 # isRational :: ExtCV -> Bool Source # isFP :: ExtCV -> Bool Source # isUnbounded :: ExtCV -> Bool Source # isUserSort :: 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) -> (FP -> FP -> b) -> (Rational -> Rational -> 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) -> (FP -> FP) -> (Rational -> Rational) -> (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) -> (FP -> FP -> FP) -> (Rational -> Rational -> Rational) -> (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
| Data SV Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SV -> c SV # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SV # dataTypeOf :: SV -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SV) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SV) # gmapT :: (forall b. Data b => b -> b) -> SV -> SV # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SV -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SV -> r # gmapQ :: (forall d. Data d => d -> u) -> SV -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SV -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SV -> m SV # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SV -> m SV # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SV -> m SV # | |
| Show SV Source # | |
| NFData SV Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Eq SV Source # | For equality, we merely use the node-id |
| Ord SV Source # | Again, simply use the node-id for ordering |
| 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 # isRational :: SV -> Bool Source # isUnbounded :: SV -> Bool Source # isUserSort :: 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
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
A symbolic node id
Instances
| Data NodeId Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NodeId -> c NodeId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NodeId # toConstr :: NodeId -> Constr # dataTypeOf :: NodeId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NodeId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeId) # gmapT :: (forall b. Data b => b -> b) -> NodeId -> NodeId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NodeId -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NodeId -> r # gmapQ :: (forall d. Data d => d -> u) -> NodeId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NodeId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NodeId -> m NodeId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeId -> m NodeId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NodeId -> m NodeId # | |
| Eq NodeId Source # | |
| Ord NodeId Source # | |
mkSymSBV :: forall a m. MonadSymbolic m => VarContext -> Kind -> Maybe String -> m (SBV a) Source #
Generalization of mkSymSBV
data ArrayContext Source #
The context of a symbolic array as created
Constructors
| ArrayFree (Maybe SV) | A new array, the contents are initialized with the given value, if any |
| ArrayMutate ArrayIndex SV SV | An array created by mutating another array at a given cell |
| ArrayMerge SV ArrayIndex ArrayIndex | An array created by symbolically merging two other arrays |
Instances
| Show ArrayContext Source # | |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> ArrayContext -> ShowS # show :: ArrayContext -> String # showList :: [ArrayContext] -> ShowS # | |
| NFData ArrayContext Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: ArrayContext -> () # | |
class SymArray array where Source #
Arrays of symbolic values
An array a b is an array indexed by the type SBV aSBV b
If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.
The reason for this class is rather historic. In the past, SBV provided two different kinds of
arrays: an SArray abstraction that mapped directly to SMTLib arrays (which is still available
today), and a functional notion of arrays that used internal caching, called SFunArray. The latter
has been removed as the code turned out to be rather tricky and hard to maintain; so we only
have one instance of this class. But end users can add their own instances, if needed.
NB. sListArray insists on a concrete initializer, because not having one would break
referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details.
Minimal complete definition
readArray, writeArray, mergeArrays, (newArray_, newArray | newArrayInState), sListArray
Methods
newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b) Source #
Generalization of newArray_
newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b) Source #
Generalization of newArray
sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b Source #
Create a literal array
readArray :: array a b -> SBV a -> SBV b Source #
Read the array element at a
writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b Source #
Update the element at a to be b
mergeArrays :: SymVal 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
newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b) Source #
Internal function, not exported to the user
Instances
| SymArray SArray Source # | |
Defined in Data.SBV.Core.Data Methods newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source # newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source # sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SArray a b Source # readArray :: SArray a b -> SBV a -> SBV b Source # writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source # mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source # newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source # | |
Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
- Maps directly to SMT-lib arrays
- Reading from an uninitialized value is OK. If the default value is given in
newArray, it will be the result. Otherwise, the read yields an uninterpreted constant. - Can check for equality of these arrays
- Cannot be used in code-generation (i.e., compilation to C)
- Cannot quick-check theorems using
SArrayvalues
Instances
sbvToSymSV :: MonadSymbolic m => SBV a -> m SV Source #
Generalization of sbvToSymSW
forceSVArg :: SV -> IO () Source #
Forcing an argument; this is a necessary evil to make sure all the arguments to an uninterpreted function are evaluated before called; the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's
A symbolic expression
Instances
| Data SBVExpr Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SBVExpr -> c SBVExpr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SBVExpr # toConstr :: SBVExpr -> Constr # dataTypeOf :: SBVExpr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SBVExpr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVExpr) # gmapT :: (forall b. Data b => b -> b) -> SBVExpr -> SBVExpr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SBVExpr -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SBVExpr -> r # gmapQ :: (forall d. Data d => d -> u) -> SBVExpr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SBVExpr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SBVExpr -> m SBVExpr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVExpr -> m SBVExpr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVExpr -> m SBVExpr # | |
| Show SBVExpr Source # | |
| NFData SBVExpr Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Eq SBVExpr Source # | |
| Ord SBVExpr Source # | |
Defined in Data.SBV.Core.Symbolic | |
newExpr :: State -> Kind -> SBVExpr -> IO SV 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 observable sharing trick for the inspiration behind this technique: http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf
Note that this is *not* a general memo utility!
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex Source #
Uncache, retrieving SMT array indexes
class HasKind a where Source #
A class for capturing values that have a sign and a size (finite or infinite)
minimal complete definition: kindOf, unless you can take advantage of the default
signature: This class can be automatically derived for data-types that have
a Data instance; this is useful for creating uninterpreted sorts. So, in
reality, end users should almost never need to define any methods.
Minimal complete definition
Nothing
Methods
intSizeOf :: a -> Int Source #
isBoolean :: a -> Bool Source #
isBounded :: a -> Bool Source #
isDouble :: a -> Bool Source #
isRational :: a -> Bool Source #
isUnbounded :: a -> Bool Source #
isUserSort :: a -> Bool Source #
isString :: a -> Bool Source #
Instances
Symbolic operations
Constructors
| 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 | |
| ZeroExtend Int | |
| SignExtend Int | |
| LkUp (Int, Kind, Kind, Int) !SV !SV | |
| ArrEq ArrayIndex ArrayIndex | |
| ArrRead ArrayIndex | |
| KindCast Kind Kind | |
| Uninterpreted String | |
| Label String | |
| IEEEFP FPOp | |
| NonLinear NROp | |
| OverflowOp OvOp | |
| PseudoBoolean PBOp | |
| StrOp StrOp | |
| RegExOp RegExOp | |
| SeqOp SeqOp | |
| SetOp SetOp | |
| TupleConstructor Int | |
| TupleAccess Int Int | |
| EitherConstructor Kind Kind Bool | |
| EitherIs Kind Kind Bool | |
| EitherAccess Bool | |
| RationalConstructor | |
| MaybeConstructor Kind Bool | |
| MaybeIs Kind Bool | |
| MaybeAccess |
Instances
| Data Op Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Op -> c Op # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Op # dataTypeOf :: Op -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Op) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op) # gmapT :: (forall b. Data b => b -> b) -> Op -> Op # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r # gmapQ :: (forall d. Data d => d -> u) -> Op -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Op -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Op -> m Op # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Op -> m Op # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Op -> m Op # | |
| Show Op Source # | |
| Eq Op Source # | |
| Ord Op Source # | |
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 |
Instances
| Data PBOp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PBOp -> c PBOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PBOp # dataTypeOf :: PBOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PBOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PBOp) # gmapT :: (forall b. Data b => b -> b) -> PBOp -> PBOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PBOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PBOp -> r # gmapQ :: (forall d. Data d => d -> u) -> PBOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PBOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PBOp -> m PBOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PBOp -> m PBOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PBOp -> m PBOp # | |
| Show PBOp Source # | |
| Eq PBOp Source # | |
| Ord PBOp Source # | |
Floating point operations
Constructors
Instances
| Data FPOp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FPOp -> c FPOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FPOp # dataTypeOf :: FPOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FPOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FPOp) # gmapT :: (forall b. Data b => b -> b) -> FPOp -> FPOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FPOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FPOp -> r # gmapQ :: (forall d. Data d => d -> u) -> FPOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FPOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FPOp -> m FPOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FPOp -> m FPOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FPOp -> m FPOp # | |
| Show FPOp Source # | |
| Eq FPOp Source # | |
| Ord FPOp Source # | |
String operations. Note that we do not define StrAt as it translates to StrSubstr trivially.
Constructors
| StrConcat | Concatenation of one or more strings |
| StrLen | String length |
| StrUnit | Unit string |
| StrNth | Nth element |
| StrSubstr | Retrieves substring of |
| StrIndexOf | Retrieves first position of |
| StrContains | Does |
| StrPrefixOf | Is |
| StrSuffixOf | Is |
| StrReplace | Replace the first occurrence of |
| StrStrToNat | Retrieve integer encoded by string |
| StrNatToStr | Retrieve string encoded by integer |
| StrToCode | Equivalent to Haskell's ord |
| StrFromCode | Equivalent to Haskell's chr |
| StrInRe RegExp | Check if string is in the regular expression |
Instances
| Data StrOp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> StrOp -> c StrOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c StrOp # dataTypeOf :: StrOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c StrOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c StrOp) # gmapT :: (forall b. Data b => b -> b) -> StrOp -> StrOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> StrOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> StrOp -> r # gmapQ :: (forall d. Data d => d -> u) -> StrOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> StrOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> StrOp -> m StrOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> StrOp -> m StrOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> StrOp -> m StrOp # | |
| Show StrOp Source # | Show instance for |
| Eq StrOp Source # | |
| Ord StrOp Source # | |
Regular-expression operators. The only thing we can do is to compare for equality/disequality.
Instances
| Data RegExOp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RegExOp -> c RegExOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RegExOp # toConstr :: RegExOp -> Constr # dataTypeOf :: RegExOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RegExOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RegExOp) # gmapT :: (forall b. Data b => b -> b) -> RegExOp -> RegExOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RegExOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RegExOp -> r # gmapQ :: (forall d. Data d => d -> u) -> RegExOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RegExOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RegExOp -> m RegExOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RegExOp -> m RegExOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RegExOp -> m RegExOp # | |
| Show RegExOp Source # | Show instance for |
| Eq RegExOp Source # | |
| Ord RegExOp Source # | |
Defined in Data.SBV.Core.Symbolic | |
Sequence operations.
Constructors
| SeqConcat | See StrConcat |
| SeqLen | See StrLen |
| SeqUnit | See StrUnit |
| SeqNth | See StrNth |
| SeqSubseq | See StrSubseq |
| SeqIndexOf | See StrIndexOf |
| SeqContains | See StrContains |
| SeqPrefixOf | See StrPrefixOf |
| SeqSuffixOf | See StrSuffixOf |
| SeqReplace | See StrReplace |
| SBVReverse Kind | Reversal of sequences. NB. Also works for strings; hence the name. |
Instances
| Data SeqOp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SeqOp -> c SeqOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SeqOp # dataTypeOf :: SeqOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SeqOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SeqOp) # gmapT :: (forall b. Data b => b -> b) -> SeqOp -> SeqOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SeqOp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SeqOp -> r # gmapQ :: (forall d. Data d => d -> u) -> SeqOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SeqOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SeqOp -> m SeqOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SeqOp -> m SeqOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SeqOp -> m SeqOp # | |
| Show SeqOp Source # | Show instance for SeqOp. Again, mapping is important. |
| Eq SeqOp Source # | |
| Ord SeqOp Source # | |
Regular expressions. Note that regular expressions themselves are
concrete, but the match function from the RegExpMatchable class
can check membership against a symbolic string/character. Also, we
are preferring a datatype approach here, as opposed to coming up with
some string-representation; there are way too many alternatives
already so inventing one isn't a priority. Please get in touch if you
would like a parser for this type as it might be easier to use.
Constructors
| Literal String | Precisely match the given string |
| All | Accept every string |
| AllChar | Accept every single character |
| None | Accept no strings |
| Range Char Char | Accept range of characters |
| Conc [RegExp] | Concatenation |
| KStar RegExp | Kleene Star: Zero or more |
| KPlus RegExp | Kleene Plus: One or more |
| Opt RegExp | Zero or one |
| Comp RegExp | Complement of regular expression |
| Diff RegExp RegExp | Difference of regular expressions |
| Loop Int Int RegExp | From |
| Power Int RegExp | Exactly |
| Union [RegExp] | Union of regular expressions |
| Inter RegExp RegExp | Intersection of regular expressions |
Instances
| Data RegExp Source # | |
Defined in Data.SBV.Core.Symbolic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RegExp -> c RegExp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RegExp # toConstr :: RegExp -> Constr # dataTypeOf :: RegExp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RegExp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RegExp) # gmapT :: (forall b. Data b => b -> b) -> RegExp -> RegExp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RegExp -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RegExp -> r # gmapQ :: (forall d. Data d => d -> u) -> RegExp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RegExp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RegExp -> m RegExp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RegExp -> m RegExp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RegExp -> m RegExp # | |
| IsString RegExp Source # | With overloaded strings, we can have direct literal regular expressions. |
Defined in Data.SBV.Core.Symbolic Methods fromString :: String -> RegExp # | |
| Num RegExp Source # | Regular expressions as a |
| Show RegExp Source # | Convert a reg-exp to a Haskell-like string |
| Eq RegExp Source # | |
| Ord RegExp Source # | |
| EqSymbolic RegExp Source # | Regular expressions can be compared for equality. Note that we diverge here from the equality in the concrete sense; i.e., the Eq instance does not match the symbolic case. This is a bit unfortunate, but unavoidable with the current design of how we "distinguish" operators. Hopefully shouldn't be a big deal, though one should be careful. |
Defined in Data.SBV.Core.Model Methods (.==) :: RegExp -> RegExp -> SBool Source # (./=) :: RegExp -> RegExp -> SBool Source # (.===) :: RegExp -> RegExp -> SBool Source # (./==) :: RegExp -> RegExp -> SBool Source # distinct :: [RegExp] -> SBool Source # distinctExcept :: [RegExp] -> [RegExp] -> SBool Source # allEqual :: [RegExp] -> SBool Source # | |
data NamedSymVar Source #
NamedSymVar pairs symbolic values and user given/automatically generated names
Constructors
| NamedSymVar !SV !Name |
Instances
| Generic NamedSymVar Source # | |
Defined in Data.SBV.Core.Symbolic Associated Types type Rep NamedSymVar :: Type -> Type # | |
| Show NamedSymVar Source # | |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> NamedSymVar -> ShowS # show :: NamedSymVar -> String # showList :: [NamedSymVar] -> ShowS # | |
| NFData NamedSymVar Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: NamedSymVar -> () # | |
| Eq NamedSymVar Source # | For comparison purposes, we simply use the SV and ignore the name |
Defined in Data.SBV.Core.Symbolic | |
| Ord NamedSymVar Source # | |
Defined in Data.SBV.Core.Symbolic Methods compare :: NamedSymVar -> NamedSymVar -> Ordering # (<) :: NamedSymVar -> NamedSymVar -> Bool # (<=) :: NamedSymVar -> NamedSymVar -> Bool # (>) :: NamedSymVar -> NamedSymVar -> Bool # (>=) :: NamedSymVar -> NamedSymVar -> Bool # max :: NamedSymVar -> NamedSymVar -> NamedSymVar # min :: NamedSymVar -> NamedSymVar -> NamedSymVar # | |
| type Rep NamedSymVar Source # | |
Defined in Data.SBV.Core.Symbolic | |
getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int Source #
Create a new table; hash-cons as necessary
A program is a sequence of assignments
Constructors
| SBVPgm | |
Fields
| |
runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result) Source #
Generalization of runSymbolic
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.
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 # | |
Kind of symbolic value
Constructors
| KBool | |
| KBounded !Bool !Int | |
| KUnbounded | |
| KReal | |
| KUserSort String (Maybe [String]) | |
| KFloat | |
| KDouble | |
| KFP !Int !Int | |
| KChar | |
| KString | |
| KList Kind | |
| KSet Kind | |
| KTuple [Kind] | |
| KMaybe Kind | |
| KRational | |
| KEither Kind Kind |
Instances
| Data Kind Source # | |
Defined in Data.SBV.Core.Kind Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Kind -> c Kind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Kind # dataTypeOf :: Kind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Kind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind) # gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r # gmapQ :: (forall d. Data d => d -> u) -> Kind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Kind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Kind -> m Kind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind # | |
| Show Kind Source # | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently
ignores the enumeration constructors. Also, when we construct a |
| NFData Kind Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Eq Kind Source # | |
| Ord Kind Source # | |
| HasKind Kind Source # | |
Defined in Data.SBV.Core.Kind Methods kindOf :: Kind -> Kind Source # hasSign :: Kind -> Bool Source # intSizeOf :: Kind -> Int Source # isBoolean :: Kind -> Bool Source # isBounded :: Kind -> Bool Source # isReal :: Kind -> Bool Source # isFloat :: Kind -> Bool Source # isDouble :: Kind -> Bool Source # isRational :: Kind -> Bool Source # isUnbounded :: Kind -> Bool Source # isUserSort :: Kind -> Bool Source # isChar :: Kind -> Bool Source # isString :: Kind -> Bool Source # isList :: Kind -> Bool Source # isSet :: Kind -> Bool Source # isTuple :: Kind -> Bool Source # isMaybe :: Kind -> Bool Source # | |
class Outputtable a where Source #
A class representing what can be returned from a symbolic computation.
Instances
Result of running a symbolic computation
Constructors
| Result | |
Fields
| |
class SolverContext m where Source #
Actions we can do in a context: Either at problem description
time or while we are dynamically querying. Symbolic and Query are
two instances of this class. Note that we use this mechanism
internally and do not export it from SBV.
Minimal complete definition
constrain, softConstrain, namedConstraint, constrainWithAttribute, setOption, addAxiom, addSMTDefinition, contextState
Methods
constrain :: SBool -> m () Source #
Add a constraint, any satisfying instance must satisfy this condition.
softConstrain :: SBool -> m () Source #
Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
namedConstraint :: String -> SBool -> m () Source #
Add a named constraint. The name is used in unsat-core extraction.
constrainWithAttribute :: [(String, String)] -> SBool -> m () Source #
Add a constraint, with arbitrary attributes.
setInfo :: String -> [String] -> m () Source #
Set info. Example: setInfo ":status" ["unsat"].
setOption :: SMTOption -> m () Source #
Set an option.
setLogic :: Logic -> m () Source #
Set the logic.
addAxiom :: String -> [String] -> m () 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 sensible by any means. A separate formalization of SMT-Lib would be very useful here.
addSMTDefinition :: String -> [String] -> m () Source #
Add a user-defined SMTLib function. You should define the name given here as an uninterpreted value as well. SBV performs no checks on the SMTLib definition you give, so if it doesn't match the required type, or is malformed in any way, the call will fail at run-time.
setTimeOut :: Integer -> m () Source #
Set a solver time-out value, in milli-seconds. This function
essentially translates to the SMTLib call (set-info :timeout val),
and your backend solver may or may not support it! The amount given
is in milliseconds. Also see the function timeOut for finer level
control of time-outs, directly from SBV.
contextState :: m State Source #
Get the state associated with this context
Instances
internalVariable :: State -> Kind -> IO SV 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 -> Bool -> [(String, String)] -> SVal -> IO () Source #
Require a boolean condition to be true in the state. Only used for internal purposes.
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
data Quantifier Source #
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
Instances
| Show Quantifier Source # | Show instance for |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> Quantifier -> ShowS # show :: Quantifier -> String # showList :: [Quantifier] -> ShowS # | |
| NFData Quantifier Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: Quantifier -> () # | |
| Eq Quantifier Source # | |
Defined in Data.SBV.Core.Symbolic | |
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 |
Instances
| Bounded SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Enum SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic Methods succ :: SMTLibVersion -> SMTLibVersion # pred :: SMTLibVersion -> SMTLibVersion # toEnum :: Int -> SMTLibVersion # fromEnum :: SMTLibVersion -> Int # enumFrom :: SMTLibVersion -> [SMTLibVersion] # enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion] # enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion] # enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion] # | |
| Show SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> SMTLibVersion -> ShowS # show :: SMTLibVersion -> String # showList :: [SMTLibVersion] -> ShowS # | |
| NFData SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: SMTLibVersion -> () # | |
| Eq SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic Methods (==) :: SMTLibVersion -> SMTLibVersion -> Bool # (/=) :: SMTLibVersion -> SMTLibVersion -> Bool # | |
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.
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. If unsat-cores are enabled, they will be returned in the second parameter. |
| Satisfiable SMTConfig SMTModel | Satisfiable with model |
| DeltaSat SMTConfig (Maybe String) SMTModel | Delta satisfiable with queried string if available and model |
| SatExtField SMTConfig SMTModel | Prover returned a model, but in an extension field containing Infinite/epsilon |
| Unknown SMTConfig SMTReasonUnknown | Prover returned unknown, with the given reason |
| ProofError SMTConfig [String] (Maybe SMTResult) | Prover errored out, with possibly a bogus result |
Instances
| NFData SMTResult Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Modelable SMTResult Source # |
|
Defined in Data.SBV.SMT.SMT Methods modelExists :: SMTResult -> Bool Source # getModelAssignment :: SatModel b => SMTResult -> Either String (Bool, b) Source # getModelDictionary :: SMTResult -> Map String CV Source # getModelValue :: SymVal b => String -> SMTResult -> Maybe b Source # getModelUninterpretedValue :: String -> SMTResult -> Maybe String Source # extractModel :: SatModel b => SMTResult -> Maybe b Source # getModelObjectives :: SMTResult -> Map String GeneralizedCV Source # getModelObjectiveValue :: String -> SMTResult -> Maybe GeneralizedCV Source # getModelUIFuns :: SMTResult -> Map String (SBVType, ([([CV], CV)], CV)) Source # getModelUIFunValue :: String -> SMTResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source # | |
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.
The crackNum field can be used to display numbers in detail, all its bits and how they are laid out in memory. Works with all bounded number types
(i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in
memory following the IEEE754 rules.
Constructors
| SMTConfig | |
Fields
| |
data OptimizeStyle Source #
Style of optimization. Note that in the pareto case the user is allowed
to specify a max number of fronts to query the solver for, since there might
potentially be an infinite number of them and there is no way to know exactly
how many ahead of time. If Nothing is given, SBV will possibly loop forever
if the number is really infinite.
Constructors
| Lexicographic | Objectives are optimized in the order given, earlier objectives have higher priority. |
| Independent | Each objective is optimized independently. |
| Pareto (Maybe Int) | Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. |
Instances
| Show OptimizeStyle Source # | |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> OptimizeStyle -> ShowS # show :: OptimizeStyle -> String # showList :: [OptimizeStyle] -> ShowS # | |
| NFData OptimizeStyle Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: OptimizeStyle -> () # | |
| Eq OptimizeStyle Source # | |
Defined in Data.SBV.Core.Symbolic Methods (==) :: OptimizeStyle -> OptimizeStyle -> Bool # (/=) :: OptimizeStyle -> OptimizeStyle -> Bool # | |
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.
Constructors
| Minimize String a | Minimize this metric |
| Maximize String a | Maximize this metric |
| AssertWithPenalty String a Penalty | A soft assertion, with an associated penalty |
data QueryState Source #
The state we keep track of as we interact with the solver
Constructors
| QueryState | |
Fields
| |
A query is a user-guided mechanism to directly communicate and extract
results from the solver. A generalization of Query.
Instances
newtype SMTProblem Source #
Internal representation of a symbolic simulation result
Constructors
| SMTProblem | SMTLib representation, given the config |
Operations useful for instantiating SBV type classes
CV represents a concrete word of a fixed size:
For signed words, the most significant digit is considered to be the sign.
Instances
| Show CV Source # | Show instance for |
| NFData CV Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Eq CV Source # | |
| Ord CV Source # | |
| 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 # isRational :: CV -> Bool Source # isUnbounded :: CV -> Bool Source # isUserSort :: CV -> Bool Source # isString :: CV -> Bool Source # isTuple :: CV -> Bool Source # isMaybe :: CV -> Bool Source # | |
| SDivisible CV Source # | |
| SatModel CV Source # |
|
| PrettyNum CV Source # | |
genMkSymVar :: MonadSymbolic m => Kind -> VarContext -> Maybe String -> m (SBV a) Source #
Generalization of genMkSymVar
genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV]) Source #
Parse a signed/sized value from a sequence of CVs
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 :: (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a) Source #
Lift quotRem to symbolic words. Division by 0 is defined s.t. x/0 = 0; which
holds even when x is 0 itself.
liftDMod :: (Ord a, SymVal a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) Source #
Lift divMod 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)
registerKind :: State -> Kind -> IO () Source #
Register a new kind with the system, used for uninterpreted sorts.
NB: Is it safe to have new kinds in query mode? It could be that
the new kind might introduce a constraint that effects the logic. For
instance, if we're seeing Double for the first time and using a BV
logic, then things would fall apart. But this should be rare, and hopefully
the success-response checking mechanism will catch the rare cases where this
is an issue. In either case, the user can always arrange for the right
logic by calling setLogic appropriately, so it seems safe to just
allow for this.
Compilation to C, extras
compileToC' :: String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle) Source #
Lower level version of compileToC, producing a CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, 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
cgSym :: Symbolic a -> SBVCodeGen a Source #
Reach into symbolic monad from code-generation
Specifying inputs, SBV variants
cgInput :: SymVal a => String -> SBVCodeGen (SBV a) Source #
Creates an atomic input in the generated code.
cgInputArr :: SymVal 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 :: SymVal 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 :: SymVal 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
cgOverwriteFiles :: Bool -> SBVCodeGen () Source #
If passed True, then we will not ask the user if we're overwriting files as we generate
the C code. Otherwise, we'll prompt.
cgShowU8UsingHex :: Bool -> SBVCodeGen () Source #
If passed True, then we will show 'SWord 8' type in hex. Otherwise we'll show it in decimal. All signed
types are shown decimal, and all unsigned larger types are shown hexadecimal otherwise.
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
| Show CgSRealType Source # | |
Defined in Data.SBV.Compilers.CodeGen Methods showsPrec :: Int -> CgSRealType -> ShowS # show :: CgSRealType -> String # showList :: [CgSRealType] -> ShowS # | |
| Eq CgSRealType Source # | |
Defined in Data.SBV.Compilers.CodeGen | |
Infrastructure
Options for code-generation.
Constructors
| CgConfig | |
Fields
| |
Code-generation state
Constructors
| CgState | |
Instances
| MonadState CgState SBVCodeGen Source # | |
Defined in Data.SBV.Compilers.CodeGen Methods get :: SBVCodeGen CgState # put :: CgState -> SBVCodeGen () # state :: (CgState -> (a, CgState)) -> SBVCodeGen a # | |
data CgPgmBundle Source #
Representation of a collection of generated programs.
Constructors
| CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |
Instances
| Show CgPgmBundle Source # | |
Defined in Data.SBV.Compilers.CodeGen Methods showsPrec :: Int -> CgPgmBundle -> ShowS # show :: CgPgmBundle -> String # showList :: [CgPgmBundle] -> ShowS # | |
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 constituent functions has a driver. (See compileToCLib.)
cgGenerateMakefile :: Bool -> SBVCodeGen () Source #
Should we generate a Makefile? Default: True.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, 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 -> (CgConfig, CgPgmBundle) -> IO () Source #
Render a code-gen bundle to a directory or to stdout
Various math utilities around floats
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: http://ghc.haskell.org/trac/ghc/ticket/10378 http://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
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.
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.
fpCompareObjectH :: RealFloat a => a -> a -> Ordering Source #
Ordering for floats, avoiding the +0-0NaN issues. Note that this is essentially used for indexing into a map, so we need to be total. Thus, the order we pick is: NaN -oo -0 +0 +oo The placement of NaN here is questionable, but immaterial.
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!
Pretty number printing
class PrettyNum a where Source #
PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
Methods
Show a number in hexadecimal, starting with 0x and type.
Show a number in binary, starting with 0b and type.
Show a number in hexadecimal, starting with 0x but no type.
Show a number in binary, starting with 0b but no type.
Show a number in hex, without prefix, or types.
Show a number in bin, without prefix, or types.
Instances
readBin :: Num a => String -> a Source #
A more convenient interface for reading binary numbers, also supports negative numbers
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #
Show as a hexadecimal value. First bool controls whether type info is printed while the second boolean controls whether 0x prefix is printed. The tuple is the signedness and the bit-length of the input. The length of the string will not depend on the value, but rather the bit-length.
chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #
Show as hexadecimal, but for C programs. We have to be careful about printing min-bounds, since C does some funky casting, possibly losing the sign bit. In those cases, we use the defined constants in stdint.h. We also properly append the necessary suffixes as needed.
shexI :: Bool -> Bool -> Integer -> String Source #
Show as a hexadecimal value, integer version. Almost the same as shex above except we don't have a bit-length so the length of the string will depend on the actual value.
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #
Similar to shex; except in binary.
showCFloat :: Float -> String Source #
A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showCDouble :: Double -> String Source #
A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showHFloat :: Float -> String Source #
A version of show for floats that generates correct Haskell literals for nan/infinite
showHDouble :: Double -> String Source #
A version of show for doubles that generates correct Haskell literals for nan/infinite
showFloatAtBase :: (Show a, RealFloat a) => Int -> a -> ShowS Source #
Like Haskell's showHFloat, but uses arbitrary base instead.
Note that the exponent is always written in decimal. Let the exponent value be d:
If base=10, then we use e to denote the exponent; meaning 10^d
If base is a power of 2, then we use p to denote the exponent; meaning 2^d
Otherwise, we use @ to denote the exponent, and it means base^d
showSMTFloat :: RoundingMode -> Float -> String Source #
A version of show for floats that generates correct SMTLib literals using the rounding mode
showSMTDouble :: RoundingMode -> Double -> String Source #
A version of show for doubles that generates correct SMTLib literals using the rounding mode
smtRoundingMode :: RoundingMode -> String Source #
Convert a rounding mode to the format SMT-Lib2 understands.
cvToSMTLib :: RoundingMode -> CV -> String Source #
Convert a CV to an SMTLib2 compliant value
mkSkolemZero :: RoundingMode -> Kind -> String Source #
Create a skolem 0 for the kind
showNegativeNumber :: (Show a, Num a, Ord a) => a -> String Source #
When we show a negative number in SMTLib, we must properly parenthesize.
Timing computations
Specify how to save timing information, if at all.
Constructors
| NoTiming | |
| PrintTiming | |
| SaveTiming (IORef NominalDiffTime) |
showTDiff :: NominalDiffTime -> String Source #
Show NominalDiffTime in human readable form. NominalDiffTime is
essentially picoseconds (10^-12 seconds). We show it so that
it's represented at the day:hour:minute:second.XXX granularity.
Coordinating with the solver
In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this
should be avoided if at all possible. Users should prefer the provided API. If you do find yourself
needing send and ask directly, please get in touch to see if SBV can support a typed API for your use case.
Similarly, the function retrieveResponseFromSolver might occasionally be necessary to clean-up the communication
buffer. We would like to hear if you do need these functions regularly so we can provide better support.
sendStringToSolver :: (MonadIO m, MonadQuery m) => String -> m () Source #
Send an arbitrary string to the solver in a query. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!
sendRequestToSolver :: (MonadIO m, MonadQuery m) => String -> m String Source #
Send an arbitrary string to the solver in a query, and return a response. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV.
retrieveResponseFromSolver :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String] Source #
Retrieve multiple responses from the solver, until it responds with a user given tag that we shall arrange for internally. The optional timeout is in milliseconds. If the time-out is exceeded, then we will raise an error. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!
Defining new metrics
addSValOptGoal :: MonadSymbolic m => Objective SVal -> m () Source #
Generalization of addSValOptGoal
sFloatAsComparableSWord32 :: SFloat -> SWord32 Source #
Convert a float to a comparable SWord32. The trick is to ignore the
sign of -0, and if it's a negative value flip all the bits, and otherwise
only flip the sign bit. This is known as the lexicographic ordering on floats
and it works as long as you do not have a NaN.
sDoubleAsComparableSWord64 :: SDouble -> SWord64 Source #
Convert a double to a comparable SWord64. The trick is to ignore the
sign of -0, and if it's a negative value flip all the bits, and otherwise
only flip the sign bit. This is known as the lexicographic ordering on doubles
and it works as long as you do not have a NaN.
sFloatingPointAsComparableSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb) Source #
Convert a float to the correct size word, that can be used in lexicographic ordering. Used in optimization.
sComparableSWord32AsSFloat :: SWord32 -> SFloat Source #
Inverse transformation to sFloatAsComparableSWord32. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0.
Otherwise, it's faithful:
>>>prove $ \x -> let f = sComparableSWord32AsSFloat x in fpIsNaN f .|| fpIsNegativeZero f .|| sFloatAsComparableSWord32 f .== xQ.E.D.>>>prove $ \x -> fpIsNegativeZero x .|| sComparableSWord32AsSFloat (sFloatAsComparableSWord32 x) `fpIsEqualObject` xQ.E.D.
sComparableSWord64AsSDouble :: SWord64 -> SDouble Source #
Inverse transformation to sDoubleAsComparableSWord64. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0.
Otherwise, it's faithful:
>>>prove $ \x -> let d = sComparableSWord64AsSDouble x in fpIsNaN d .|| fpIsNegativeZero d .|| sDoubleAsComparableSWord64 d .== xQ.E.D.>>>prove $ \x -> fpIsNegativeZero x .|| sComparableSWord64AsSDouble (sDoubleAsComparableSWord64 x) `fpIsEqualObject` xQ.E.D.
sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb Source #
Inverse transformation to sFloatingPointAsComparableSWord. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0.
Otherwise, it's faithful:
>>>prove $ \x -> let d = sComparableSWordAsSFloatingPoint x in fpIsNaN d .|| fpIsNegativeZero d .|| sFloatingPointAsComparableSWord (d :: SFPHalf) .== xQ.E.D.>>>prove $ \x -> fpIsNegativeZero x .|| sComparableSWordAsSFloatingPoint (sFloatingPointAsComparableSWord x) `fpIsEqualObject` (x :: SFPHalf)Q.E.D.