| Copyright | (c) Brian Schroeder Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Trans
Contents
- Symbolic types
- Arrays of symbolic values
- Creating symbolic values
- Symbolic Equality and Comparisons
- Conditionals: Mergeable values
- Symbolic integral numbers
- Division and Modulus
- Bit-vector operations
- IEEE-floating point numbers
- Enumerations
- Uninterpreted sorts, axioms, constants, and functions
- Properties, proofs, and satisfiability
- Constraints
- Checking safety
- Quick-checking
- Optimization
- Model extraction
- SMT Interface
- Abstract SBV type
- Module exports
Description
More generalized alternative to Data.SBV for advanced client use
Synopsis
- type SBool = SBV Bool
- 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
- fromBool :: Bool -> SBool
- oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a
- sAnd :: [SBool] -> SBool
- sOr :: [SBool] -> SBool
- sAny :: (a -> SBool) -> [a] -> SBool
- sAll :: (a -> SBool) -> [a] -> SBool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SWord (n :: Nat) = SBV (WordN n)
- data WordN (n :: Nat)
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInt (n :: Nat) = SBV (IntN n)
- data IntN (n :: Nat)
- type family IsNonZero (arg :: Nat) :: Constraint where ...
- type family FromSized (t :: Type) :: Type where ...
- type family ToSized (t :: Type) :: Type where ...
- fromSized :: FromSizedBV a => a -> FromSized a
- toSized :: ToSizedBV a => a -> ToSized a
- type SInteger = SBV Integer
- type SFloat = SBV Float
- type SDouble = SBV Double
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSInteger :: SReal -> SInteger
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- 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
- data SArray a b
- data SFunArray a b
- sBool :: MonadSymbolic m => String -> m SBool
- sWord8 :: MonadSymbolic m => String -> m SWord8
- sWord16 :: MonadSymbolic m => String -> m SWord16
- sWord32 :: MonadSymbolic m => String -> m SWord32
- sWord64 :: MonadSymbolic m => String -> m SWord64
- sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SWord n)
- sInt8 :: MonadSymbolic m => String -> m SInt8
- sInt16 :: MonadSymbolic m => String -> m SInt16
- sInt32 :: MonadSymbolic m => String -> m SInt32
- sInt64 :: MonadSymbolic m => String -> m SInt64
- sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SInt n)
- sInteger :: MonadSymbolic m => String -> m SInteger
- sReal :: MonadSymbolic m => String -> m SReal
- sFloat :: MonadSymbolic m => String -> m SFloat
- sDouble :: MonadSymbolic m => String -> m SDouble
- sChar :: MonadSymbolic m => String -> m SChar
- sString :: MonadSymbolic m => String -> m SString
- sList :: (SymVal a, MonadSymbolic m) => String -> m (SList a)
- sBools :: MonadSymbolic m => [String] -> m [SBool]
- sWord8s :: MonadSymbolic m => [String] -> m [SWord8]
- sWord16s :: MonadSymbolic m => [String] -> m [SWord16]
- sWord32s :: MonadSymbolic m => [String] -> m [SWord32]
- sWord64s :: MonadSymbolic m => [String] -> m [SWord64]
- sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
- sInt8s :: MonadSymbolic m => [String] -> m [SInt8]
- sInt16s :: MonadSymbolic m => [String] -> m [SInt16]
- sInt32s :: MonadSymbolic m => [String] -> m [SInt32]
- sInt64s :: MonadSymbolic m => [String] -> m [SInt64]
- sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
- sIntegers :: MonadSymbolic m => [String] -> m [SInteger]
- sReals :: MonadSymbolic m => [String] -> m [SReal]
- sFloats :: MonadSymbolic m => [String] -> m [SFloat]
- sDoubles :: MonadSymbolic m => [String] -> m [SDouble]
- sChars :: MonadSymbolic m => [String] -> m [SChar]
- sStrings :: MonadSymbolic m => [String] -> m [SString]
- sLists :: (SymVal a, MonadSymbolic m) => [String] -> m [SList a]
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class Equality a where
- class Mergeable a where
- ite :: Mergeable a => SBool -> a -> a -> a
- iteLazy :: Mergeable a => SBool -> a -> a -> a
- class (SymVal a, Num a, Bits a, Integral a) => SIntegral a
- class SDivisible a where
- sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
- sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a
- class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where
- sFiniteBitSize :: SBV a -> Int
- lsb :: SBV a -> SBool
- msb :: SBV a -> SBool
- blastBE :: SBV a -> [SBool]
- blastLE :: SBV a -> [SBool]
- fromBitsBE :: [SBool] -> SBV a
- fromBitsLE :: [SBool] -> SBV a
- sTestBit :: SBV a -> Int -> SBool
- sExtractBits :: SBV a -> [Int] -> [SBool]
- sPopCount :: SBV a -> SWord8
- setBitTo :: SBV a -> Int -> SBool -> SBV a
- fullAdder :: SBV a -> SBV a -> (SBool, SBV a)
- fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)
- sCountLeadingZeros :: SBV a -> SWord8
- sCountTrailingZeros :: SBV a -> SWord8
- bvExtract :: forall i j n bv proxy. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) => proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
- (#) :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m)) => SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
- zeroExtend :: forall n m bv. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), IsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- signExtend :: forall n m bv. (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), IsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- bvDrop :: forall i n m bv proxy. (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, IsNonZero (n - i)) => proxy i -> SBV (bv n) -> SBV (bv m)
- bvTake :: forall i n bv proxy. (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n) => proxy i -> SBV (bv n) -> SBV (bv i)
- (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
- class (SymVal a, RealFloat a) => IEEEFloating a where
- fpAbs :: SBV a -> SBV a
- fpNeg :: SBV a -> SBV a
- fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
- fpSqrt :: SRoundingMode -> SBV a -> SBV a
- fpRem :: SBV a -> SBV a -> SBV a
- fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a
- fpMin :: SBV a -> SBV a -> SBV a
- fpMax :: SBV a -> SBV a -> SBV a
- fpIsEqualObject :: SBV a -> SBV a -> SBool
- fpIsNormal :: SBV a -> SBool
- fpIsSubnormal :: SBV a -> SBool
- fpIsZero :: SBV a -> SBool
- fpIsInfinite :: SBV a -> SBool
- fpIsNaN :: SBV a -> SBool
- fpIsNegative :: SBV a -> SBool
- fpIsPositive :: SBV a -> SBool
- fpIsNegativeZero :: SBV a -> SBool
- fpIsPositiveZero :: SBV a -> SBool
- fpIsPoint :: SBV a -> SBool
- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymVal a) => SBV a
- sInfinity :: (Floating a, SymVal a) => SBV a
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class SymVal a => IEEEFloatConvertible a where
- fromSFloat :: SRoundingMode -> SFloat -> SBV a
- toSFloat :: SRoundingMode -> SBV a -> SFloat
- fromSDouble :: SRoundingMode -> SDouble -> SBV a
- toSDouble :: SRoundingMode -> SBV a -> SDouble
- sFloatAsSWord32 :: SFloat -> SWord32
- sWord32AsSFloat :: SWord32 -> SFloat
- sDoubleAsSWord64 :: SDouble -> SWord64
- sWord64AsSDouble :: SWord64 -> SDouble
- blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
- blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
- mkSymbolicEnumeration :: Name -> Q [Dec]
- class Uninterpreted a where
- uninterpret :: String -> a
- cgUninterpret :: String -> [String] -> a -> a
- sbvUninterpret :: Maybe ([String], a) -> String -> a
- addAxiom :: SolverContext m => String -> [String] -> m ()
- type Predicate = Symbolic SBool
- type Goal = Symbolic ()
- class ExtractIO m => MProvable m a where
- forAll_ :: a -> SymbolicT m SBool
- forAll :: [String] -> a -> SymbolicT m SBool
- forSome_ :: a -> SymbolicT m SBool
- forSome :: [String] -> a -> SymbolicT m SBool
- prove :: a -> m ThmResult
- proveWith :: SMTConfig -> a -> m ThmResult
- sat :: a -> m SatResult
- satWith :: SMTConfig -> a -> m SatResult
- allSat :: a -> m AllSatResult
- allSatWith :: SMTConfig -> a -> m AllSatResult
- optimize :: OptimizeStyle -> a -> m OptimizeResult
- optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
- isVacuous :: a -> m Bool
- isVacuousWith :: SMTConfig -> a -> m Bool
- isTheorem :: a -> m Bool
- isTheoremWith :: SMTConfig -> a -> m Bool
- isSatisfiable :: a -> m Bool
- isSatisfiableWith :: SMTConfig -> a -> m Bool
- validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
- type Provable = MProvable IO
- proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
- satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
- proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
- proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
- satConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
- satConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
- satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
- generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String
- solve :: MonadSymbolic m => [SBool] -> m SBool
- constrain :: SolverContext m => SBool -> m ()
- softConstrain :: SolverContext m => SBool -> m ()
- namedConstraint :: SolverContext m => String -> SBool -> m ()
- constrainWithAttribute :: SolverContext m => [(String, String)] -> SBool -> m ()
- pbAtMost :: [SBool] -> Int -> SBool
- pbAtLeast :: [SBool] -> Int -> SBool
- pbExactly :: [SBool] -> Int -> SBool
- pbLe :: [(Int, SBool)] -> Int -> SBool
- pbGe :: [(Int, SBool)] -> Int -> SBool
- pbEq :: [(Int, SBool)] -> Int -> SBool
- pbMutexed :: [SBool] -> SBool
- pbStronglyMutexed :: [SBool] -> SBool
- sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a
- isSafe :: SafeResult -> Bool
- class ExtractIO m => SExecutable m a where
- sName_ :: a -> SymbolicT m ()
- sName :: [String] -> a -> SymbolicT m ()
- safe :: a -> m [SafeResult]
- safeWith :: SMTConfig -> a -> m [SafeResult]
- sbvQuickCheck :: Symbolic SBool -> IO Bool
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)
- data Objective a
- class Metric a where
- type MetricSpace a :: *
- toMetricSpace :: SBV a -> SBV (MetricSpace a)
- fromMetricSpace :: SBV (MetricSpace a) -> SBV a
- msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
- msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
- assertWithPenalty :: MonadSymbolic m => String -> SBool -> Penalty -> m ()
- data Penalty
- data ExtCV
- data GeneralizedCV
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- data SMTResult
- data SMTReasonUnknown
- observe :: SymVal a => String -> SBV a -> SBV a
- class SatModel a where
- class Modelable a where
- modelExists :: a -> Bool
- getModelAssignment :: SatModel b => a -> Either String (Bool, b)
- getModelDictionary :: a -> Map String CV
- getModelValue :: SymVal b => String -> a -> Maybe b
- getModelUninterpretedValue :: String -> a -> Maybe String
- extractModel :: SatModel b => a -> Maybe b
- getModelObjectives :: a -> Map String GeneralizedCV
- getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
- getModelUIFuns :: a -> Map String (SBVType, ([([CV], CV)], CV))
- getModelUIFunValue :: String -> a -> Maybe (SBVType, ([([CV], CV)], CV))
- displayModels :: SatModel a => ([(Bool, a)] -> [(Bool, a)]) -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
- extractModels :: SatModel a => AllSatResult -> [a]
- getModelDictionaries :: AllSatResult -> [Map String CV]
- getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b]
- getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
- 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
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- allowQuantifiedQueries :: Bool
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath
- data Timing
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: String -> String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- setLogic :: SolverContext m => Logic -> m ()
- data Logic
- setOption :: SolverContext m => SMTOption -> m ()
- setInfo :: SolverContext m => String -> [String] -> m ()
- setTimeOut :: SolverContext m => Integer -> m ()
- data SBVException = SBVException {
- sbvExceptionDescription :: String
- sbvExceptionSent :: Maybe String
- sbvExceptionExpected :: Maybe String
- sbvExceptionReceived :: Maybe String
- sbvExceptionStdOut :: Maybe String
- sbvExceptionStdErr :: Maybe String
- sbvExceptionExitCode :: Maybe ExitCode
- sbvExceptionConfig :: SMTConfig
- sbvExceptionReason :: Maybe [String]
- sbvExceptionHint :: Maybe [String]
- data SBV a
- 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 Kind
- 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
- class MonadIO m => MonadSymbolic m where
- symbolicEnv :: m State
- type Symbolic = SymbolicT IO
- data SymbolicT m a
- label :: SymVal a => String -> SBV a -> SBV a
- output :: (Outputtable a, MonadSymbolic m) => a -> m a
- runSMT :: MonadIO m => SymbolicT m a -> m a
- runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
- module Data.Bits
- module Data.Word
- module Data.Int
- module Data.Ratio
Symbolic types
Booleans
Boolean values and functions
oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a Source #
Returns 1 if the boolean is sTrue, otherwise 0.
Logical functions
Bit-vectors
Unsigned bit-vectors
data WordN (n :: Nat) Source #
An unsigned bit-vector carrying its size info
Instances
Signed bit-vectors
A signed bit-vector carrying its size info
Instances
Converting between fixed-size and arbitrary bitvectors
type family IsNonZero (arg :: Nat) :: Constraint where ... Source #
Type family to create the appropriate non-zero constraint
type family FromSized (t :: Type) :: Type where ... Source #
Capture the correspondence between sized and fixed-sized BVs
Equations
| FromSized (WordN 8) = Word8 | |
| FromSized (WordN 16) = Word16 | |
| FromSized (WordN 32) = Word32 | |
| FromSized (WordN 64) = Word64 | |
| FromSized (IntN 8) = Int8 | |
| FromSized (IntN 16) = Int16 | |
| FromSized (IntN 32) = Int32 | |
| FromSized (IntN 64) = Int64 | |
| FromSized (SWord 8) = SWord8 | |
| FromSized (SWord 16) = SWord16 | |
| FromSized (SWord 32) = SWord32 | |
| FromSized (SWord 64) = SWord64 | |
| FromSized (SInt 8) = SInt8 | |
| FromSized (SInt 16) = SInt16 | |
| FromSized (SInt 32) = SInt32 | |
| FromSized (SInt 64) = SInt64 |
type family ToSized (t :: Type) :: Type where ... Source #
Capture the correspondence between fixed-sized and sized BVs
Equations
| ToSized Word8 = WordN 8 | |
| ToSized Word16 = WordN 16 | |
| ToSized Word32 = WordN 32 | |
| ToSized Word64 = WordN 64 | |
| ToSized Int8 = IntN 8 | |
| ToSized Int16 = IntN 16 | |
| ToSized Int32 = IntN 32 | |
| ToSized Int64 = IntN 64 | |
| ToSized SWord8 = SWord 8 | |
| ToSized SWord16 = SWord 16 | |
| ToSized SWord32 = SWord 32 | |
| ToSized SWord64 = SWord 64 | |
| ToSized SInt8 = SInt 8 | |
| ToSized SInt16 = SInt 16 | |
| ToSized SInt32 = SInt 32 | |
| ToSized SInt64 = SInt 64 |
Unbounded integers
Floating point numbers
Algebraic reals
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
Instances
sRealToSInteger :: SReal -> SInteger Source #
Convert an SReal to an SInteger. That is, it computes the
largest integer n that satisfies sIntegerToSReal n <= r
essentially giving us the floor.
For instance, 1.3 will be 1, but -1.3 will be -2.
Characters, Strings and Regular Expressions
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.
Symbolic lists
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.
Arrays of symbolic values
class SymArray array where Source #
Flat 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.
While it's certainly possible for user to create instances of SymArray, the
SArray and SFunArray instances already provided should cover most use cases
in practice. Note that there are a few differences between these two models in
terms of use models:
SArrayproduces SMTLib arrays, and requires a solver that understands the array theory.SFunArrayis internally handled, and thus can be used with any solver. (Note that all solvers exceptabcsupport arrays, so this isn't a big decision factor.)- For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
- Only
SArraysupports checking equality of arrays. (That is, checking if an entire array is equivalent to another.)SFunArrays cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible. - Only
SFunArraysupports compilation to C. Programs usingSArraywill not be accepted by the C-code generator. - You cannot use quickcheck on programs that contain these arrays. (Neither
SArraynorSFunArray.) - With
SArray, SBV transfers all array-processing to the SMT-solver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. WithSFunArray, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.
As a rule of thumb, try SArray first. These should generate compact code. However, if
the backend solver has hard time solving the generated problems, switch to
SFunArray. If you still have issues, please report so we can see what the problem might be!
Minimal complete definition
readArray, writeArray, mergeArrays, (newArray_, newArray | newArrayInState)
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
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
Instances
Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
- Maps directly to SMT-lib arrays
- Reading from an unintialized value is OK. 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 - Typically slower as it heavily relies on SMT-solving for the array theory
Instances
Arrays implemented internally, without translating to SMT-Lib functions:
- Internally handled by the library and not mapped to SMT-Lib, hence can be used with solvers that don't support arrays. (Such as abc.)
- Reading from an unintialized value is OK. If the default value is given in
newArray, it will be the result. Otherwise, the read yields an uninterpreted constant. - Cannot check for equality of arrays.
- Can be used in code-generation (i.e., compilation to C).
- Can not quick-check theorems using
SFunArrayvalues - Typically faster as it gets compiled away during translation.
Instances
Creating symbolic values
Single value
sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SWord n) Source #
Generalization of sWord
sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SInt n) Source #
Generalization of sInt
List of values
sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SWord n] Source #
Generalization of sWord64s
sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SInt n] Source #
Generalization of sInts
Symbolic Equality and Comparisons
class EqSymbolic a where Source #
Symbolic Equality. Note that we can't use Haskell's Eq class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.
Minimal complete definition
Methods
(.==) :: a -> a -> SBool infix 4 Source #
Symbolic equality.
(./=) :: a -> a -> SBool infix 4 Source #
Symbolic inequality.
(.===) :: a -> a -> SBool infix 4 Source #
Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that
is NaN == NaN holds, but +0 == -0 doesn't. On other types, (.===) is simply (.==).
Note that (.==) is the right notion of equality for floats per IEEE754 specs, since by
definition +0 == -0 and NaN equals no other value including itself. But occasionally
we want to be stronger and state NaN equals NaN and +0 and -0 are different from
each other. In a context where your type is concrete, simply use fpIsEqualObject. But in
a polymorphic context, use the strong equality instead.
NB. If you do not care about or work with floats, simply use (.==) and (./=).
(./==) :: a -> a -> SBool infix 4 Source #
Negation of strong equality. Equaivalent to negation of (.===) on all types.
distinct :: [a] -> SBool Source #
Returns (symbolic) sTrue if all the elements of the given list are different.
distinctExcept :: [a] -> [a] -> SBool Source #
Returns (symbolic) sTrue if all the elements of the given list are different. The second
list contains exceptions, i.e., if an element belongs to that set, it will be considered
distinct regardless of repetition.
>>>prove $ \a -> distinctExcept [a, a] [0::SInteger] .<=> a .== 0Q.E.D.>>>prove $ \a b -> distinctExcept [a, b] [0::SWord8] .<=> (a .== b .=> a .== 0)Q.E.D.>>>prove $ \a b c d -> distinctExcept [a, b, c, d] [] .== distinct [a, b, c, (d::SInteger)]Q.E.D.
allEqual :: [a] -> SBool Source #
Returns (symbolic) sTrue if all the elements of the given list are the same.
sElem :: a -> [a] -> SBool Source #
Symbolic membership test.
sNotElem :: a -> [a] -> SBool Source #
Symbolic negated membership test.
Instances
| EqSymbolic Bool Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: Bool -> Bool -> SBool Source # (./=) :: Bool -> Bool -> SBool Source # (.===) :: Bool -> Bool -> SBool Source # (./==) :: Bool -> Bool -> SBool Source # distinct :: [Bool] -> SBool Source # distinctExcept :: [Bool] -> [Bool] -> SBool Source # allEqual :: [Bool] -> SBool Source # | |
| EqSymbolic a => EqSymbolic [a] Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: [a] -> [a] -> SBool Source # (./=) :: [a] -> [a] -> SBool Source # (.===) :: [a] -> [a] -> SBool Source # (./==) :: [a] -> [a] -> SBool Source # distinct :: [[a]] -> SBool Source # distinctExcept :: [[a]] -> [[a]] -> SBool Source # allEqual :: [[a]] -> SBool Source # | |
| EqSymbolic a => EqSymbolic (Maybe a) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: Maybe a -> Maybe a -> SBool Source # (./=) :: Maybe a -> Maybe a -> SBool Source # (.===) :: Maybe a -> Maybe a -> SBool Source # (./==) :: Maybe a -> Maybe a -> SBool Source # distinct :: [Maybe a] -> SBool Source # distinctExcept :: [Maybe a] -> [Maybe a] -> SBool Source # allEqual :: [Maybe a] -> SBool Source # | |
| EqSymbolic (SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: SBV a -> SBV a -> SBool Source # (./=) :: SBV a -> SBV a -> SBool Source # (.===) :: SBV a -> SBV a -> SBool Source # (./==) :: SBV a -> SBV a -> SBool Source # distinct :: [SBV a] -> SBool Source # distinctExcept :: [SBV a] -> [SBV a] -> SBool Source # allEqual :: [SBV a] -> SBool Source # | |
| EqSymbolic a => EqSymbolic (S a) Source # | Symbolic equality for |
Defined in Documentation.SBV.Examples.ProofTools.BMC Methods (.==) :: S a -> S a -> SBool Source # (./=) :: S a -> S a -> SBool Source # (.===) :: S a -> S a -> SBool Source # (./==) :: S a -> S a -> SBool Source # distinct :: [S a] -> SBool Source # distinctExcept :: [S a] -> [S a] -> SBool Source # allEqual :: [S a] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: Either a b -> Either a b -> SBool Source # (./=) :: Either a b -> Either a b -> SBool Source # (.===) :: Either a b -> Either a b -> SBool Source # (./==) :: Either a b -> Either a b -> SBool Source # distinct :: [Either a b] -> SBool Source # distinctExcept :: [Either a b] -> [Either a b] -> SBool Source # allEqual :: [Either a b] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b) -> (a, b) -> SBool Source # (./=) :: (a, b) -> (a, b) -> SBool Source # (.===) :: (a, b) -> (a, b) -> SBool Source # (./==) :: (a, b) -> (a, b) -> SBool Source # distinct :: [(a, b)] -> SBool Source # distinctExcept :: [(a, b)] -> [(a, b)] -> SBool Source # allEqual :: [(a, b)] -> SBool Source # | |
| EqSymbolic (SArray a b) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: SArray a b -> SArray a b -> SBool Source # (./=) :: SArray a b -> SArray a b -> SBool Source # (.===) :: SArray a b -> SArray a b -> SBool Source # (./==) :: SArray a b -> SArray a b -> SBool Source # distinct :: [SArray a b] -> SBool Source # distinctExcept :: [SArray a b] -> [SArray a b] -> SBool Source # allEqual :: [SArray a b] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b, c) -> (a, b, c) -> SBool Source # (./=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.===) :: (a, b, c) -> (a, b, c) -> SBool Source # (./==) :: (a, b, c) -> (a, b, c) -> SBool Source # distinct :: [(a, b, c)] -> SBool Source # distinctExcept :: [(a, b, c)] -> [(a, b, c)] -> SBool Source # allEqual :: [(a, b, c)] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.===) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # distinct :: [(a, b, c, d)] -> SBool Source # distinctExcept :: [(a, b, c, d)] -> [(a, b, c, d)] -> SBool Source # allEqual :: [(a, b, c, d)] -> SBool Source # sElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # sNotElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.===) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # distinct :: [(a, b, c, d, e)] -> SBool Source # distinctExcept :: [(a, b, c, d, e)] -> [(a, b, c, d, e)] -> SBool Source # allEqual :: [(a, b, c, d, e)] -> SBool Source # sElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # sNotElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.===) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # distinct :: [(a, b, c, d, e, f)] -> SBool Source # distinctExcept :: [(a, b, c, d, e, f)] -> [(a, b, c, d, e, f)] -> SBool Source # allEqual :: [(a, b, c, d, e, f)] -> SBool Source # sElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # sNotElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.===) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # distinct :: [(a, b, c, d, e, f, g)] -> SBool Source # distinctExcept :: [(a, b, c, d, e, f, g)] -> [(a, b, c, d, e, f, g)] -> SBool Source # allEqual :: [(a, b, c, d, e, f, g)] -> SBool Source # sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source # sNotElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source # | |
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #
Symbolic Comparisons. Similar to Eq, we cannot implement Haskell's Ord class
since there is no way to return an Ordering value from a symbolic comparison.
Furthermore, OrdSymbolic requires Mergeable to implement if-then-else, for the
benefit of implementing symbolic versions of max and min functions.
Minimal complete definition
Methods
(.<) :: a -> a -> SBool infix 4 Source #
Symbolic less than.
(.<=) :: a -> a -> SBool infix 4 Source #
Symbolic less than or equal to.
(.>) :: a -> a -> SBool infix 4 Source #
Symbolic greater than.
(.>=) :: a -> a -> SBool infix 4 Source #
Symbolic greater than or equal to.
Symbolic minimum.
Symbolic maximum.
inRange :: a -> (a, a) -> SBool Source #
Is the value withing the allowed inclusive range?
Instances
| OrdSymbolic a => OrdSymbolic [a] Source # | |
| OrdSymbolic a => OrdSymbolic (Maybe a) Source # | |
Defined in Data.SBV.Core.Model | |
| (Ord a, SymVal a) => OrdSymbolic (SBV a) Source # | If comparison is over something SMTLib can handle, just translate it. Otherwise desugar. |
| (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: Either a b -> Either a b -> SBool Source # (.<=) :: Either a b -> Either a b -> SBool Source # (.>) :: Either a b -> Either a b -> SBool Source # (.>=) :: Either a b -> Either a b -> SBool Source # smin :: Either a b -> Either a b -> Either a b Source # smax :: Either a b -> Either a b -> Either a b Source # inRange :: Either a b -> (Either a b, Either a b) -> SBool Source # | |
| (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: (a, b, c) -> (a, b, c) -> SBool Source # (.<=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>=) :: (a, b, c) -> (a, b, c) -> SBool Source # smin :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # smax :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # inRange :: (a, b, c) -> ((a, b, c), (a, b, c)) -> SBool Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # inRange :: (a, b, c, d) -> ((a, b, c, d), (a, b, c, d)) -> SBool Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # inRange :: (a, b, c, d, e) -> ((a, b, c, d, e), (a, b, c, d, e)) -> SBool Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # smin :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # smax :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # inRange :: (a, b, c, d, e, f) -> ((a, b, c, d, e, f), (a, b, c, d, e, f)) -> SBool Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool Source # | |
class Equality a where Source #
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.
Instances
Conditionals: Mergeable values
class Mergeable a where Source #
Symbolic conditionals are modeled by the Mergeable class, describing
how to merge the results of an if-then-else call with a symbolic test. SBV
provides all basic types as instances of this class, so users only need
to declare instances for custom data-types of their programs as needed.
A Mergeable instance may be automatically derived for a custom data-type
with a single constructor where the type of each field is an instance of
Mergeable, such as a record of symbolic values. Users only need to add
Generic and Mergeable to the deriving clause for the data-type. See
Status for an example and an
illustration of what the instance would look like if written by hand.
The function select is a total-indexing function out of a list of choices
with a default value, simulating array/list indexing. It's an n-way generalization
of the ite function.
Minimal complete definition: None, if the type is instance of Generic. Otherwise
symbolicMerge. Note that most types subject to merging are likely to be
trivial instances of Generic.
Minimal complete definition
Nothing
Methods
symbolicMerge :: Bool -> SBool -> a -> a -> a Source #
Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
select :: (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a Source #
Total indexing operation. select xs default index is intuitively
the same as xs !! index, except it evaluates to default if index
underflows/overflows.
symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a Source #
Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
Instances
ite :: Mergeable a => SBool -> a -> a -> a Source #
If-then-else. This is by definition symbolicMerge with both
branches forced. This is typically the desired behavior, but also
see iteLazy should you need more laziness.
iteLazy :: Mergeable a => SBool -> a -> a -> a Source #
A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.
Symbolic integral numbers
class (SymVal a, Num a, Bits a, Integral a) => SIntegral a Source #
Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic type-signatures that work for all
symbolic numbers, such as SWord8, SInt8 etc. For instance, we can write a generic
list-minimum function as follows:
mm :: SIntegral a => [SBV a] -> SBV a mm = foldr1 (a b -> ite (a .<= b) a b)
It is similar to the standard Integral class, except ranging over symbolic instances.
Instances
| SIntegral Int8 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Int16 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Int32 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Int64 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Integer Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Word8 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Word16 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Word32 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Word64 Source # | |
Defined in Data.SBV.Core.Model | |
| (KnownNat n, IsNonZero n) => SIntegral (IntN n) Source # | |
Defined in Data.SBV.Core.Sized | |
| (KnownNat n, IsNonZero n) => SIntegral (WordN n) Source # | |
Defined in Data.SBV.Core.Sized | |
Division and Modulus
class SDivisible a where Source #
The SDivisible class captures the essence of division.
Unfortunately we cannot use Haskell's Integral class since the Real
and Enum superclasses are not implementable for symbolic bit-vectors.
However, quotRem and divMod both make perfect sense, and the SDivisible class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following pair of laws:
xsQuotRem0 = (0, x) xsDivMod0 = (0, x)
Note that our instances implement this law even when x is 0 itself.
NB. quot truncates toward zero, while div truncates toward negative infinity.
C code generation of division operations
In the case of division or modulo of a minimal signed value (e.g. -128 for
SInt8) by -1, SMTLIB and Haskell agree on what the result should be.
Unfortunately the result in C code depends on CPU architecture and compiler
settings, as this is undefined behaviour in C. **SBV does not guarantee**
what will happen in generated C code in this corner case.
Instances
Bit-vector operations
Conversions
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b Source #
Conversion between integral-symbolic values, akin to Haskell's fromIntegral
Shifts and rotates
sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #
Generalization of shiftR, when the shift-amount is symbolic. Since Haskell's
shiftR only takes an Int as the shift amount, it cannot be used when we have
a symbolic amount to shift with.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
following the usual Haskell convention. See sSignedShiftArithRight for a variant
that explicitly uses the msb as the sign bit, even for unsigned underlying types.
sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #
An implementation of rotate-left, using a barrel shifter like design. Only works when both
arguments are finite bitvectors, and furthermore when the second argument is unsigned.
The first condition is enforced by the type, but the second is dynamically checked.
We provide this implementation as an alternative to sRotateLeft since SMTLib logic
does not support variable argument rotates (as opposed to shifts), and thus this
implementation can produce better code for verification compared to sRotateLeft.
>>>prove $ \x y -> (x `sBarrelRotateLeft` y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)Q.E.D.
sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #
An implementation of rotate-right, using a barrel shifter like design. See comments
for sBarrelRotateLeft for details.
>>>prove $ \x y -> (x `sBarrelRotateRight` y) `sBarrelRotateLeft` (y :: SWord32) .== (x :: SWord64)Q.E.D.
sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a Source #
Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent
to sShiftRight when the argument is signed. However, if the argument is unsigned,
then it explicitly treats its msb as a sign-bit, and uses it as the bit that
gets shifted in. Useful when using the underlying unsigned bit representation to implement
custom signed operations. Note that there is no direct Haskell analogue of this function.
Finite bit-vector operations
class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where Source #
Finite bit-length symbolic values. Essentially the same as SIntegral, but further leaves out Integer. Loosely
based on Haskell's FiniteBits class, but with more methods defined and structured differently to fit into the
symbolic world view. Minimal complete definition: sFiniteBitSize.
Minimal complete definition
Methods
sFiniteBitSize :: SBV a -> Int Source #
Bit size.
lsb :: SBV a -> SBool Source #
Least significant bit of a word, always stored at index 0.
msb :: SBV a -> SBool Source #
Most significant bit of a word, always stored at the last position.
blastBE :: SBV a -> [SBool] Source #
Big-endian blasting of a word into its bits.
blastLE :: SBV a -> [SBool] Source #
Little-endian blasting of a word into its bits.
fromBitsBE :: [SBool] -> SBV a Source #
Reconstruct from given bits, given in little-endian.
fromBitsLE :: [SBool] -> SBV a Source #
Reconstruct from given bits, given in little-endian.
sTestBit :: SBV a -> Int -> SBool Source #
sExtractBits :: SBV a -> [Int] -> [SBool] Source #
Variant of sTestBit, where we want to extract multiple bit positions.
sPopCount :: SBV a -> SWord8 Source #
Variant of popCount, returning a symbolic value.
setBitTo :: SBV a -> Int -> SBool -> SBV a Source #
fullAdder :: SBV a -> SBV a -> (SBool, SBV a) Source #
Full adder, returns carry-out from the addition. Only for unsigned quantities.
fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) Source #
Full multipler, returns both high and low-order bits. Only for unsigned quantities.
sCountLeadingZeros :: SBV a -> SWord8 Source #
Count leading zeros in a word, big-endian interpretation.
sCountTrailingZeros :: SBV a -> SWord8 Source #
Count trailing zeros in a word, big-endian interpretation.
Instances
Splitting, joining, and extending bit-vectors
Arguments
| :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) | |
| => proxy i |
|
| -> proxy j |
|
| -> SBV (bv n) | Input bit vector of size |
| -> SBV (bv ((i - j) + 1)) | Output is of size |
Extract a portion of bits to form a smaller bit-vector.
>>>prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)Q.E.D.
Arguments
| :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m)) | |
| => SBV (bv n) | First input, of size |
| -> SBV (bv m) | Second input, of size |
| -> SBV (bv (n + m)) | Concatenation, of size |
Join two bitvectors.
>>>prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))Q.E.D.
Arguments
| :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), IsNonZero (m - n)) | |
| => SBV (bv n) | Input, of size |
| -> SBV (bv m) | Output, of size |
Zero extend a bit-vector.
>>>prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0Q.E.D.
Arguments
| :: (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), IsNonZero (m - n)) | |
| => SBV (bv n) | Input, of size |
| -> SBV (bv m) | Output, of size |
Sign extend a bit-vector.
>>>prove $ \x -> sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0Q.E.D.>>>prove $ \x -> msb x .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0Q.E.D.
Arguments
| :: (KnownNat n, IsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, IsNonZero (n - i)) | |
| => proxy i |
|
| -> SBV (bv n) | Input, of size |
| -> SBV (bv m) | Output, of size |
Drop bits from the top of a bit-vector.
>>>prove $ \x -> bvDrop (Proxy @0) (x :: SWord 43) .== xQ.E.D.>>>prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0Q.E.D.
Arguments
| :: (KnownNat n, IsNonZero n, KnownNat i, IsNonZero i, i <= n) | |
| => proxy i |
|
| -> SBV (bv n) | Input, of size |
| -> SBV (bv i) | Output, of size |
Take bits from the top of a bit-vector.
>>>prove $ \x -> bvTake (Proxy @13) (x :: SWord 13) .== xQ.E.D.>>>prove $ \x -> bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0Q.E.D.>>>prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)Q.E.D.
Exponentiation
(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b Source #
Symbolic exponentiation using bit blasting and repeated squaring.
N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.
IEEE-floating point numbers
class (SymVal a, RealFloat a) => IEEEFloating a where Source #
A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.
Minimal complete definition
Nothing
Methods
fpAbs :: SBV a -> SBV a Source #
Compute the floating point absolute value.
fpNeg :: SBV a -> SBV a Source #
Compute the unary negation. Note that 0 - x is not equivalent to -x for floating-point, since -0 and 0 are different.
fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #
Add two floating point values, using the given rounding mode
fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #
Subtract two floating point values, using the given rounding mode
fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #
Multiply two floating point values, using the given rounding mode
fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #
Divide two floating point values, using the given rounding mode
fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a Source #
Fused-multiply-add three floating point values, using the given rounding mode. fpFMA x y z = x*y+z but with only
one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
Haskell lacks an FMA implementation.
fpSqrt :: SRoundingMode -> SBV a -> SBV a Source #
Compute the square-root of a float, using the given rounding mode
fpRem :: SBV a -> SBV a -> SBV a Source #
Compute the remainder: x - y * n, where n is the truncated integer nearest to x/y. The rounding mode
is implicitly assumed to be RoundNearestTiesToEven.
fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a Source #
Round to the nearest integral value, using the given rounding mode.
fpMin :: SBV a -> SBV a -> SBV a Source #
Compute the minimum of two floats, respects infinity and NaN values
fpMax :: SBV a -> SBV a -> SBV a Source #
Compute the maximum of two floats, respects infinity and NaN values
fpIsEqualObject :: SBV a -> SBV a -> SBool Source #
Are the two given floats exactly the same. That is, NaN will compare equal to itself, +0 will not compare
equal to -0 etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==.)
fpIsNormal :: SBV a -> SBool Source #
Is the floating-point number a normal value. (i.e., not denormalized.)
fpIsSubnormal :: SBV a -> SBool Source #
Is the floating-point number a subnormal value. (Also known as denormal.)
fpIsZero :: SBV a -> SBool Source #
Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)
fpIsInfinite :: SBV a -> SBool Source #
Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)
fpIsNaN :: SBV a -> SBool Source #
Is the floating-point number a NaN value?
fpIsNegative :: SBV a -> SBool Source #
Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.
fpIsPositive :: SBV a -> SBool Source #
Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.
fpIsNegativeZero :: SBV a -> SBool Source #
Is the floating point number -0?
fpIsPositiveZero :: SBV a -> SBool Source #
Is the floating point number +0?
fpIsPoint :: SBV a -> SBool Source #
Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.
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
Rounding modes
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
Conversion to/from floats
class SymVal a => IEEEFloatConvertible a where Source #
Capture convertability from/to FloatingPoint representations.
Conversions to float: toSFloat and toSDouble simply return the
nearest representable float from the given type based on the rounding
mode provided.
Conversions from float: fromSFloat and fromSDouble functions do
the reverse conversion. However some care is needed when given values
that are not representable in the integral target domain. For instance,
converting an SFloat to an SInt8 is problematic. The rules are as follows:
If the input value is a finite point and when rounded in the given rounding mode to an integral value lies within the target bounds, then that result is returned. (This is the regular interpretation of rounding in IEEE754.)
Otherwise (i.e., if the integral value in the float or double domain) doesn't
fit into the target type, then the result is unspecified. Note that if the input
is +oo, -oo, or NaN, then the result is unspecified.
Due to the unspecified nature of conversions, SBV will never constant fold conversions from floats to integral values. That is, you will always get a symbolic value as output. (Conversions from floats to other floats will be constant folded. Conversions from integral values to floats will also be constant folded.)
Note that unspecified really means unspecified: In particular, SBV makes
no guarantees about matching the behavior between what you might get in
Haskell, via SMT-Lib, or the C-translation. If the input value is out-of-bounds
as defined above, or is NaN or oo or -oo, then all bets are off. In particular
C and SMTLib are decidedly undefine this case, though that doesn't mean they do the
same thing! Same goes for Haskell, which seems to convert via Int64, but we do
not model that behavior in SBV as it doesn't seem to be intentional nor well documented.
You can check for NaN, oo and -oo, using the predicates fpIsNaN, fpIsInfinite,
and fpIsPositive, fpIsNegative predicates, respectively; and do the proper conversion
based on your needs. (0 is a good choice, as are min/max bounds of the target type.)
Currently, SBV provides no predicates to check if a value would lie within range for a particular conversion task, as this depends on the rounding mode and the types involved and can be rather tricky to determine. (See http://github.com/LeventErkok/sbv/issues/456 for a discussion of the issues involved.) In a future release, we hope to be able to provide underflow and overflow predicates for these conversions as well.
Minimal complete definition
Nothing
Methods
fromSFloat :: SRoundingMode -> SFloat -> SBV a Source #
Convert from an IEEE74 single precision float.
toSFloat :: SRoundingMode -> SBV a -> SFloat Source #
Convert to an IEEE-754 Single-precision float.
>>>:{roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}
>>>prove $ roundTrip @Int8Q.E.D.>>>prove $ roundTrip @Word8Q.E.D.>>>prove $ roundTrip @Int16Q.E.D.>>>prove $ roundTrip @Word16Q.E.D.>>>prove $ roundTrip @Int32Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = -264306721 :: Int32
Note how we get a failure on Int32. The counter-example value is not representable exactly as a single precision float:
>>>toRational (-264306721 :: Float)(-264306720) % 1
Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.
toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat Source #
Convert to an IEEE-754 Single-precision float.
>>>:{roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}
>>>prove $ roundTrip @Int8Q.E.D.>>>prove $ roundTrip @Word8Q.E.D.>>>prove $ roundTrip @Int16Q.E.D.>>>prove $ roundTrip @Word16Q.E.D.>>>prove $ roundTrip @Int32Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = -264306721 :: Int32
Note how we get a failure on Int32. The counter-example value is not representable exactly as a single precision float:
>>>toRational (-264306721 :: Float)(-264306720) % 1
Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.
fromSDouble :: SRoundingMode -> SDouble -> SBV a Source #
Convert from an IEEE74 double precision float.
toSDouble :: SRoundingMode -> SBV a -> SDouble Source #
Convert to an IEEE-754 Double-precision float.
>>>:{roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}
>>>prove $ roundTrip @Int8Q.E.D.>>>prove $ roundTrip @Word8Q.E.D.>>>prove $ roundTrip @Int16Q.E.D.>>>prove $ roundTrip @Word16Q.E.D.>>>prove $ roundTrip @Int32Q.E.D.>>>prove $ roundTrip @Word32Q.E.D.>>>prove $ roundTrip @Int64Falsifiable. Counter-example: s0 = RoundTowardNegative :: RoundingMode s1 = -8069753317450726624 :: Int64
Just like in the SFloat case, once we reach 64-bits, we no longer can exactly represent the
integer value for all possible values:
>>>toRational ( -8069753317450726624 :: Double)(-8069753317450726400) % 1
In this case the numerator is off by 224!
toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble Source #
Convert to an IEEE-754 Double-precision float.
>>>:{roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}
>>>prove $ roundTrip @Int8Q.E.D.>>>prove $ roundTrip @Word8Q.E.D.>>>prove $ roundTrip @Int16Q.E.D.>>>prove $ roundTrip @Word16Q.E.D.>>>prove $ roundTrip @Int32Q.E.D.>>>prove $ roundTrip @Word32Q.E.D.>>>prove $ roundTrip @Int64Falsifiable. Counter-example: s0 = RoundTowardNegative :: RoundingMode s1 = -8069753317450726624 :: Int64
Just like in the SFloat case, once we reach 64-bits, we no longer can exactly represent the
integer value for all possible values:
>>>toRational ( -8069753317450726624 :: Double)(-8069753317450726400) % 1
In this case the numerator is off by 224!
Instances
Bit-pattern conversions
sFloatAsSWord32 :: SFloat -> SWord32 Source #
Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the
representation for NaNs are not unique, this function will return a symbolic value when given a
concrete NaN.
Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.
sWord32AsSFloat :: SWord32 -> SFloat Source #
Reinterpret the bits in a 32-bit word as a single-precision floating point number
sDoubleAsSWord64 :: SDouble -> SWord64 Source #
Convert an SDouble to an SWord64, preserving the bit-correspondence. Note that since the
representation for NaNs are not unique, this function will return a symbolic value when given a
concrete NaN.
See the implementation note for sFloatAsSWord32, as it applies here as well.
sWord64AsSDouble :: SWord64 -> SDouble Source #
Reinterpret the bits in a 32-bit word as a single-precision floating point number
blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a single-precision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a single-precision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
Enumerations
Uninterpreted sorts, axioms, constants, and functions
class Uninterpreted a where Source #
Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Minimal complete definition: sbvUninterpret. However, most instances in
practice are already provided by SBV, so end-users should not need to define their
own instances.
Minimal complete definition
Methods
uninterpret :: String -> a Source #
Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.
cgUninterpret :: String -> [String] -> a -> a Source #
Uninterpret a value, only for the purposes of code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.
sbvUninterpret :: Maybe ([String], a) -> String -> a Source #
Most generalized form of uninterpretation, this function should not be needed by end-user-code, but is rather useful for the library development.
Instances
addAxiom :: SolverContext m => 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 sensical by any means. A separate formalization of SMT-Lib would be very useful here.
Properties, proofs, and satisfiability
type Predicate = Symbolic SBool Source #
A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The Symbolic
monad captures the underlying representation, and can/should be ignored by the users of the library,
unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate
type when necessary.
type Goal = Symbolic () Source #
A goal is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as appropriate directives for sat/prove calls.
class ExtractIO m => MProvable m a where Source #
A type a is provable if we can turn it into a predicate.
Note that a predicate can be made from a curried function of arbitrary arity, where
each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So
predicates can be constructed from almost arbitrary Haskell functions that have arbitrary
shapes. (See the instance declarations below.)
Methods
forAll_ :: a -> SymbolicT m SBool Source #
Generalization of forAll_
forAll :: [String] -> a -> SymbolicT m SBool Source #
Generalization of forAll
forSome_ :: a -> SymbolicT m SBool Source #
Generalization of forSome_
forSome :: [String] -> a -> SymbolicT m SBool Source #
Generalization of forSome
prove :: a -> m ThmResult Source #
Generalization of prove
proveWith :: SMTConfig -> a -> m ThmResult Source #
Generalization of proveWith
sat :: a -> m SatResult Source #
Generalization of sat
satWith :: SMTConfig -> a -> m SatResult Source #
Generalization of satWith
allSat :: a -> m AllSatResult Source #
Generalization of allSat
allSatWith :: SMTConfig -> a -> m AllSatResult Source #
Generalization of allSatWith
optimize :: OptimizeStyle -> a -> m OptimizeResult Source #
Generalization of optimize
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult Source #
Generalization of optimizeWith
isVacuous :: a -> m Bool Source #
Generalization of isVacuous
isVacuousWith :: SMTConfig -> a -> m Bool Source #
Generalization of isVacuousWith
isTheorem :: a -> m Bool Source #
Generalization of isTheorem
isTheoremWith :: SMTConfig -> a -> m Bool Source #
Generalization of isTheoremWith
isSatisfiable :: a -> m Bool Source #
Generalization of isSatisfiable
isSatisfiableWith :: SMTConfig -> a -> m Bool Source #
Generalization of isSatisfiableWith
validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult Source #
Validate a model obtained from the solver
Instances
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)] Source #
Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult) Source #
Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed. Note that we send an exception to the losing processes, but we do *not* actually wait for them to finish. In rare cases this can lead to zombie processes. In previous experiments, we found that some processes take their time to terminate. So, this solution favors quick turnaround.
satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)] Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult) Source #
Prove a property by running many queries each isolated to their own thread concurrently and return the first that finishes, killing the others
proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)] Source #
Prove a property by running many queries each isolated to their own thread concurrently and wait for each to finish returning all results
satConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult) Source #
Find a satisfying assignment to a property using a single solver, but providing several query problems of interest, with each query running in a separate thread and return the first one that returns. This can be useful to use symbolic mode to drive to a location in the search space of the solver and then refine the problem in query mode. If the computation is very hard to solve for the solver than running in concurrent mode may provide a large performance benefit.
satConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)] Source #
Find a satisfying assignment to a property using a single solver, but run
each query problem in a separate isolated thread and wait for each thread to
finish. See satConcurrentWithAny for more details.
satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult) Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed. Note that we send an exception to the losing processes, but we do *not* actually wait for them to finish. In rare cases this can lead to zombie processes. In previous experiments, we found that some processes take their time to terminate. So, this solution favors quick turnaround.
generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String Source #
Create an SMT-Lib2 benchmark. The Bool argument controls whether this is a SAT instance, i.e.,
translate the query directly, or a PROVE instance, i.e., translate the negated query.
Constraints
General constraints
constrain :: SolverContext m => SBool -> m () Source #
Add a constraint, any satisfying instance must satisfy this condition.
softConstrain :: SolverContext m => SBool -> m () Source #
Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
Constraint Vacuity
Named constraints and attributes
namedConstraint :: SolverContext m => String -> SBool -> m () Source #
Add a named constraint. The name is used in unsat-core extraction.
constrainWithAttribute :: SolverContext m => [(String, String)] -> SBool -> m () Source #
Add a constraint, with arbitrary attributes.
Unsat cores
Cardinality constraints
Checking safety
sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a Source #
Symbolic assert. Check that the given boolean condition is always sTrue in the given path. The
optional first argument can be used to provide call-stack info via GHC's location facilities.
isSafe :: SafeResult -> Bool Source #
Check if a safe-call was safe or not, turning a SafeResult to a Bool.
class ExtractIO m => SExecutable m a where Source #
Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use
cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.
Methods
sName_ :: a -> SymbolicT m () Source #
Generalization of sName_
sName :: [String] -> a -> SymbolicT m () Source #
Generalization of sName
safe :: a -> m [SafeResult] Source #
Generalization of safe
safeWith :: SMTConfig -> a -> m [SafeResult] Source #
Generalization of safeWith
Instances
Quick-checking
sbvQuickCheck :: Symbolic SBool -> IO Bool Source #
Quick check an SBV property. Note that a regular quickCheck call will work just as
well. Use this variant if you want to receive the boolean result.
Optimization
Multiple optimization goals
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
| Eq OptimizeStyle Source # | |
Defined in Data.SBV.Core.Symbolic Methods (==) :: OptimizeStyle -> OptimizeStyle -> Bool # (/=) :: OptimizeStyle -> OptimizeStyle -> Bool # | |
| 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 -> () # | |
Objectives
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 |
Class of metrics we can optimize for. Currently, booleans,
bounded signed/unsigned bit-vectors, unbounded integers,
algebraic reals and floats can be optimized. You can add
your instances, but bewared that the MetricSpace should
map your type to something the backend solver understands, which
are limited to unsigned bit-vectors, reals, and unbounded integers
for z3.
A good reference on these features is given in the following paper: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.
Minimal completion: None. However, if MetricSpace is not identical to the type, you want
to define toMetricSpace and possibly 'minimize'/'maximize' to add extra constraints as necessary.
Minimal complete definition
Nothing
Associated Types
type MetricSpace a :: * Source #
The metric space we optimize the goal over. Usually the same as the type itself, but not always!
For instance, signed bit-vectors are optimized over their unsigned counterparts, floats are
optimized over their Word32 comparable counterparts, etc.
Methods
toMetricSpace :: SBV a -> SBV (MetricSpace a) Source #
Compute the metric value to optimize.
fromMetricSpace :: SBV (MetricSpace a) -> SBV a Source #
Compute the value itself from the metric corresponding to it.
msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m () Source #
Minimizing a metric space
msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m () Source #
Maximizing a metric space
toMetricSpace :: a ~ MetricSpace a => SBV a -> SBV (MetricSpace a) Source #
Compute the metric value to optimize.
fromMetricSpace :: a ~ MetricSpace a => SBV (MetricSpace a) -> SBV a Source #
Compute the value itself from the metric corresponding to it.
Instances
Soft assumptions
assertWithPenalty :: MonadSymbolic m => String -> SBool -> Penalty -> m () Source #
Generalization of assertWithPenalty
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 |
Field extensions
If an optimization results in an infinity/epsilon value, the returned CV value will be in the corresponding extension field.
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
Model extraction
Inspecting proof results
Instances
| Show ThmResult Source # | |
| NFData ThmResult Source # | |
Defined in Data.SBV.SMT.SMT | |
| Modelable ThmResult Source # |
|
Defined in Data.SBV.SMT.SMT Methods modelExists :: ThmResult -> Bool Source # getModelAssignment :: SatModel b => ThmResult -> Either String (Bool, b) Source # getModelDictionary :: ThmResult -> Map String CV Source # getModelValue :: SymVal b => String -> ThmResult -> Maybe b Source # getModelUninterpretedValue :: String -> ThmResult -> Maybe String Source # extractModel :: SatModel b => ThmResult -> Maybe b Source # getModelObjectives :: ThmResult -> Map String GeneralizedCV Source # getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCV Source # getModelUIFuns :: ThmResult -> Map String (SBVType, ([([CV], CV)], CV)) Source # getModelUIFunValue :: String -> ThmResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source # | |
A sat call results in a SatResult
The reason for having a separate SatResult is to have a more meaningful Show instance.
Instances
| Show SatResult Source # | |
| NFData SatResult Source # | |
Defined in Data.SBV.SMT.SMT | |
| Modelable SatResult Source # |
|
Defined in Data.SBV.SMT.SMT Methods modelExists :: SatResult -> Bool Source # getModelAssignment :: SatModel b => SatResult -> Either String (Bool, b) Source # getModelDictionary :: SatResult -> Map String CV Source # getModelValue :: SymVal b => String -> SatResult -> Maybe b Source # getModelUninterpretedValue :: String -> SatResult -> Maybe String Source # extractModel :: SatModel b => SatResult -> Maybe b Source # getModelObjectives :: SatResult -> Map String GeneralizedCV Source # getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCV Source # getModelUIFuns :: SatResult -> Map String (SBVType, ([([CV], CV)], CV)) Source # getModelUIFunValue :: String -> SatResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source # | |
newtype AllSatResult Source #
An allSat call results in a AllSatResult. The first boolean says whether we
hit the max-model limit as we searched. The second boolean says whether
there were prefix-existentials. The third boolean says whether we stopped because
the solver returned Unknown.
Constructors
| AllSatResult (Bool, Bool, Bool, [SMTResult]) |
Instances
| Show AllSatResult Source # | |
Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> AllSatResult -> ShowS # show :: AllSatResult -> String # showList :: [AllSatResult] -> ShowS # | |
newtype SafeResult Source #
A safe call results in a SafeResult
Constructors
| SafeResult (Maybe String, String, SMTResult) |
Instances
| Show SafeResult Source # | |
Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> SafeResult -> ShowS # show :: SafeResult -> String # showList :: [SafeResult] -> ShowS # | |
data OptimizeResult Source #
An optimize call results in a OptimizeResult. In the ParetoResult case, the boolean is True
if we reached pareto-query limit and so there might be more unqueried results remaining. If False,
it means that we have all the pareto fronts returned. See the Pareto OptimizeStyle for details.
Constructors
| LexicographicResult SMTResult | |
| ParetoResult (Bool, [SMTResult]) | |
| IndependentResult [(String, SMTResult)] |
Instances
| Show OptimizeResult Source # | |
Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> OptimizeResult -> ShowS # show :: OptimizeResult -> String # showList :: [OptimizeResult] -> ShowS # | |
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 |
| 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 # | |
data SMTReasonUnknown Source #
Reason for reporting unknown.
Constructors
| UnknownMemOut | |
| UnknownIncomplete | |
| UnknownTimeOut | |
| UnknownOther String |
Instances
Observing expressions
observe :: SymVal a => String -> SBV a -> SBV a Source #
Observe the value of an expression, uncoditionally. See observeIf for a generalized version.
Programmable model extraction
class SatModel a where Source #
Instances of SatModel can be automatically extracted from models returned by the
solvers. The idea is that the sbv infrastructure provides a stream of CV's (constant values)
coming from the solver, and the type a is interpreted based on these constants. Many typical
instances are already provided, so new instances can be declared with relative ease.
Minimum complete definition: parseCVs
Minimal complete definition
Nothing
Methods
parseCVs :: [CV] -> Maybe (a, [CV]) Source #
Given a sequence of constant-words, extract one instance of the type a, returning
the remaining elements untouched. If the next element is not what's expected for this
type you should return Nothing
cvtModel :: (a -> Maybe b) -> Maybe (a, [CV]) -> Maybe (b, [CV]) Source #
Given a parsed model instance, transform it using f, and return the result.
The default definition for this method should be sufficient in most use cases.
parseCVs :: Read a => [CV] -> Maybe (a, [CV]) Source #
Given a sequence of constant-words, extract one instance of the type a, returning
the remaining elements untouched. If the next element is not what's expected for this
type you should return Nothing
Instances
| SatModel Bool Source # |
|
| SatModel Double Source # |
|
| SatModel Float Source # |
|
| SatModel Int8 Source # |
|
| SatModel Int16 Source # |
|
| SatModel Int32 Source # |
|
| SatModel Int64 Source # |
|
| SatModel Integer Source # |
|
| SatModel Word8 Source # |
|
| SatModel Word16 Source # |
|
| SatModel Word32 Source # |
|
| SatModel Word64 Source # |
|
| SatModel () Source # | Base case for |
| SatModel AlgReal Source # |
|
| SatModel CV Source # |
|
| SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices) |
Defined in Data.SBV.SMT.SMT | |
| SatModel State Source # | Make |
| SatModel E Source # | Make |
| SatModel Day Source # | Make |
| SatModel Color Source # | Make |
| SatModel Nationality Source # | Make |
Defined in Documentation.SBV.Examples.Puzzles.Fish | |
| SatModel Beverage Source # | Make |
| SatModel Pet Source # | Make |
| SatModel Sport Source # | Make |
| SatModel Color Source # | Make |
| SatModel Color Source # | Make |
| SatModel U2Member Source # | Make |
| SatModel Location Source # | Make |
| SatModel Day Source # | Make |
| SatModel BinOp Source # | Make |
| SatModel UnOp Source # | Make |
| SatModel a => SatModel [a] Source # | A list of values as extracted from a model. When reading a list, we go as long as we can (maximal-munch). Note that this never fails, as we can always return the empty list! |
| (KnownNat n, IsNonZero n) => SatModel (IntN n) Source # | Constructing models for |
| (KnownNat n, IsNonZero n) => SatModel (WordN n) Source # | Constructing models for |
| (SatModel a, SatModel b) => SatModel (a, b) Source # | Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) Source # | 3-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) Source # | 4-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) Source # | 5-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) Source # | 6-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) Source # | 7-Tuples extracted from a model |
class Modelable a where Source #
Various SMT results that we can extract models out of.
Minimal complete definition
modelExists, getModelAssignment, getModelDictionary, getModelObjectives, getModelUIFuns
Methods
modelExists :: a -> Bool Source #
Is there a model?
getModelAssignment :: SatModel b => a -> Either String (Bool, b) Source #
Extract assignments of a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModelDictionary :: a -> Map String CV Source #
Extract a model dictionary. Extract a dictionary mapping the variables to
their respective values as returned by the SMT solver. Also see getModelDictionaries.
getModelValue :: SymVal b => String -> a -> Maybe b Source #
Extract a model value for a given element. Also see getModelValues.
getModelUninterpretedValue :: String -> a -> Maybe String Source #
Extract a representative name for the model value of an uninterpreted kind.
This is supposed to correspond to the value as computed internally by the
SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues.
extractModel :: SatModel b => a -> Maybe b Source #
A simpler variant of getModelAssignment to get a model out without the fuss.
getModelObjectives :: a -> Map String GeneralizedCV Source #
Extract model objective values, for all optimization goals.
getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV Source #
Extract the value of an objective
getModelUIFuns :: a -> Map String (SBVType, ([([CV], CV)], CV)) Source #
Extract model uninterpreted-functions
getModelUIFunValue :: String -> a -> Maybe (SBVType, ([([CV], CV)], CV)) Source #
Extract the value of an uninterpreted-function as an association list
Instances
displayModels :: SatModel a => ([(Bool, a)] -> [(Bool, a)]) -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int Source #
Given an allSat call, we typically want to iterate over it and print the results in sequence. The
displayModels function automates this task by calling disp on each result, consecutively. The first
Int argument to disp 'is the current model number. The second argument is a tuple, where the first
element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown).
The arrange argument can sort the results in any way you like, if necessary.
extractModels :: SatModel a => AllSatResult -> [a] Source #
Return all the models from an allSat call, similar to extractModel but
is suitable for the case of multiple results.
getModelDictionaries :: AllSatResult -> [Map String CV] Source #
Get dictionaries from an all-sat call. Similar to getModelDictionary.
getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b] Source #
Extract value of a variable from an all-sat call. Similar to getModelValue.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] Source #
Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.
SMT Interface
Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc.
which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be
created by varying those values. (Such as z3{verbose=True}.)
Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after
the decimal point. The default value is 16, but it can be set to any positive integer.
When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value
exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
of the real value is not finite, i.e., if it is not rational.
The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
Constructors
| SMTConfig | |
Fields
| |
Specify how to save timing information, if at all.
Constructors
| NoTiming | |
| PrintTiming | |
| SaveTiming (IORef NominalDiffTime) |
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] # | |
| Eq SMTLibVersion Source # | |
Defined in Data.SBV.Core.Symbolic Methods (==) :: SMTLibVersion -> SMTLibVersion -> Bool # (/=) :: SMTLibVersion -> SMTLibVersion -> Bool # | |
| 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 -> () # | |
Solvers that SBV is aware of
An SMT solver
Constructors
| SMTSolver | |
Fields
| |
Controlling verbosity
Solvers
Configurations
defaultSolverConfig :: Solver -> SMTConfig Source #
The default configs corresponding to supported SMT solvers
defaultSMTCfg :: SMTConfig Source #
The default solver used by SBV. This is currently set to z3.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool Source #
Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.
sbvAvailableSolvers :: IO [SMTConfig] Source #
Return the known available solver configs, installed on your machine.
setLogic :: SolverContext m => Logic -> m () Source #
Set the logic.
SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
user can override this choice using a call to setLogic This is especially handy if one is experimenting with custom
logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for the official list.
Constructors
| AUFLIA | Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values. |
| AUFLIRA | Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. |
| AUFNIRA | Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. |
| LRA | Linear formulas in linear real arithmetic. |
| QF_ABV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays. |
| QF_AUFBV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols. |
| QF_AUFLIA | Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols. |
| QF_AX | Quantifier-free formulas over the theory of arrays with extensionality. |
| QF_BV | Quantifier-free formulas over the theory of fixed-size bitvectors. |
| QF_IDL | Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant. |
| QF_LIA | Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables. |
| QF_LRA | Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. |
| QF_NIA | Quantifier-free integer arithmetic. |
| QF_NRA | Quantifier-free real arithmetic. |
| QF_RDL | Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant. |
| QF_UF | Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. |
| QF_UFBV | Unquantified formulas over bitvectors with uninterpreted sort function and symbols. |
| QF_UFIDL | Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. |
| QF_UFLIA | Unquantified linear integer arithmetic with uninterpreted sort and function symbols. |
| QF_UFLRA | Unquantified linear real arithmetic with uninterpreted sort and function symbols. |
| QF_UFNRA | Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. |
| QF_UFNIRA | Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols. |
| UFLRA | Linear real arithmetic with uninterpreted sort and function symbols. |
| UFNIA | Non-linear integer arithmetic with uninterpreted sort and function symbols. |
| QF_FPBV | Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors. |
| QF_FP | Quantifier-free formulas over the theory of floating point numbers. |
| QF_FD | Quantifier-free finite domains. |
| QF_S | Quantifier-free formulas over the theory of strings. |
| Logic_ALL | The catch-all value. |
| Logic_NONE | Use this value when you want SBV to simply not set the logic. |
| CustomLogic String | In case you need a really custom string! |
Instances
setOption :: SolverContext m => SMTOption -> m () Source #
Set an option.
setInfo :: SolverContext m => String -> [String] -> m () Source #
Set info. Example: setInfo ":status" ["unsat"].
setTimeOut :: SolverContext m => 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.
SBV exceptions
data SBVException Source #
An exception thrown from SBV. If the solver ever responds with a non-success value for a command,
SBV will throw an SBVException, it so the user can process it as required. The provided Show instance
will render the failure nicely. Note that if you ever catch this exception, the solver is no longer alive:
You should either -- throw the exception up, or do other proper clean-up before continuing.
Constructors
Instances
| Show SBVException Source # | A fairly nice rendering of the exception, for display purposes. |
Defined in Data.SBV.SMT.Utils Methods showsPrec :: Int -> SBVException -> ShowS # show :: SBVException -> String # showList :: [SBVException] -> ShowS # | |
| Exception SBVException Source # | SBVExceptions are throwable. A simple "show" will render this exception nicely though of course you can inspect the individual fields as necessary. |
Defined in Data.SBV.SMT.Utils Methods toException :: SBVException -> SomeException # fromException :: SomeException -> Maybe SBVException # displayException :: SBVException -> String # | |
Abstract SBV type
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
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 #
isUnbounded :: a -> Bool Source #
isUninterpreted :: a -> Bool Source #
isString :: a -> Bool Source #
isEither :: a -> Bool Source #
Instances
Kind of symbolic value
Constructors
| KBool | |
| KBounded !Bool !Int | |
| KUnbounded | |
| KReal | |
| KUninterpreted String (Either String [String]) | |
| KFloat | |
| KDouble | |
| KChar | |
| KString | |
| KList Kind | |
| KSet Kind | |
| KTuple [Kind] | |
| KMaybe Kind | |
| KEither Kind Kind |
Instances
| Eq Kind Source # | |
| Ord Kind Source # | |
| 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 | |
| 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 # isUnbounded :: Kind -> Bool Source # isUninterpreted :: 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 (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
class MonadIO m => MonadSymbolic m where Source #
A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.
Computations which support symbolic operations
Minimal complete definition
Nothing
Methods
symbolicEnv :: m State Source #
symbolicEnv :: (MonadTrans t, MonadSymbolic m', m ~ t m') => m State Source #
Instances
A generalization of Symbolic.
Instances
label :: SymVal a => String -> SBV a -> SBV a Source #
label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code.
Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. Compare this to observe
which is good for printing counter-examples.
output :: (Outputtable a, MonadSymbolic m) => a -> m a Source #
Generalization of output
runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a Source #
Generalization of runSMTWith
Module exports
module Data.Bits
module Data.Word
module Data.Int
module Data.Ratio