| 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
- Symbolic types
- 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 (SBV 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 BVIsNonZero (arg :: Nat) where ...
- type family FromSized t where ...
- type family ToSized t 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 SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSIntegerFloor :: SReal -> SInteger
- sRealToSIntegerCeiling :: SReal -> SInteger
- sRealToSIntegerTruncate :: SReal -> SInteger
- sRealToSIntegerRoundAway :: SReal -> SInteger
- sRealToSIntegerRoundToEven :: SReal -> SInteger
- sRealToSIntegerRM :: SRoundingMode -> SReal -> SInteger
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- readArray :: (SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val
- writeArray :: (HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val
- type SArray a b = SBV (ArrayModel 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 :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero 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 :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero 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)
- sArray :: (SymVal a, SymVal b, MonadSymbolic m) => String -> m (SArray a b)
- 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 :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero 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 :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero 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]
- sArrays :: (SymVal a, SymVal b, MonadSymbolic m) => [String] -> m [SArray a b]
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class OrdSymbolic (SBV a) => Zero a where
- type family MeasureOf f r 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, Num (SBV a), Bits a, Integral a) => SIntegral a
- class SDivisible a where
- sFromIntegral :: (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, Num (SBV a), OrdSymbolic (SBV 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
- sSetBitTo :: SBV a -> SBV a -> 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 :: Nat) (j :: Nat) (n :: Nat) bv proxy. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) => proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
- (#) :: forall (n :: Nat) bv (m :: Nat). (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m)) => SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
- zeroExtend :: forall (n :: Nat) (m :: Nat) bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), BVIsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- signExtend :: forall (n :: Nat) (m :: Nat) bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), BVIsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Natural) bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, BVIsNonZero (n - i)) => proxy i -> SBV (bv n) -> SBV (bv m)
- bvTake :: forall (i :: Nat) (n :: Nat) bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero 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
- sCaseRoundingMode :: Mergeable r => r -> r -> r -> r -> r -> SRoundingMode -> r
- 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
- fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a
- toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb
- sFloatAsSWord32 :: SFloat -> SWord32
- sWord32AsSFloat :: SWord32 -> SFloat
- sDoubleAsSWord64 :: SDouble -> SWord64
- sWord64AsSDouble :: SWord64 -> SDouble
- sFloatingPointAsSWord :: forall (eb :: Nat) (sb :: Nat). (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
- sWordAsSFloatingPoint :: forall (eb :: Natural) (sb :: Natural). (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
- blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
- blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
- blastSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
- mkSymbolic :: [Name] -> Q [Dec]
- class SMTDefinable a where
- smtFunctionDef :: String -> Measure a -> a -> a
- registerFunction :: a -> Symbolic ()
- uninterpret :: String -> a
- uninterpretWithArgs :: String -> [String] -> a
- cgUninterpret :: String -> [String] -> a -> a
- sbvDefineValue :: UIName -> Maybe [String] -> UIKind a -> a
- sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> a) -> SBVs as -> a
- sym :: String -> a
- symWithKind :: String -> a
- sbv2smt :: ExtractIO m => a -> m String
- sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> a) -> m String
- mkADTConstructor :: String -> a
- mkADTTester :: String -> a
- mkADTAccessor :: String -> a
- smtFunction :: (SMTDefinable a, Typeable a, Lambda Symbolic a) => String -> a -> a
- smtFunctionWithMeasure :: (SMTDefinable f, Typeable f, Lambda Symbolic f, Zero r, OrdSymbolic (SBV r), SymVal r, ApplyMeasure f r) => String -> (MeasureOf f r, [MeasureHelper]) -> f -> f
- type Predicate = Symbolic SBool
- type ConstraintSet = Symbolic ()
- class ExtractIO m => ProvableM (m :: Type -> Type) a where
- proofArgReduce :: a -> SymbolicT m SBool
- prove :: a -> m ThmResult
- proveWith :: SMTConfig -> a -> m ThmResult
- dprove :: a -> m ThmResult
- dproveWith :: SMTConfig -> a -> m ThmResult
- isVacuousProof :: a -> m Bool
- isVacuousProofWith :: SMTConfig -> a -> m Bool
- isTheorem :: a -> m Bool
- isTheoremWith :: SMTConfig -> a -> m Bool
- type Provable = ProvableM IO
- class ExtractIO m => SatisfiableM (m :: Type -> Type) a where
- satArgReduce :: a -> SymbolicT m SBool
- sat :: a -> m SatResult
- satWith :: SMTConfig -> a -> m SatResult
- dsat :: a -> m SatResult
- dsatWith :: SMTConfig -> a -> m SatResult
- allSat :: a -> m AllSatResult
- allSatWith :: SMTConfig -> a -> m AllSatResult
- isSatisfiable :: a -> m Bool
- isSatisfiableWith :: SMTConfig -> a -> m Bool
- optimize :: OptimizeStyle -> a -> m OptimizeResult
- optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
- type Satisfiable = SatisfiableM IO
- generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String
- generateSMTBenchmarkProof :: ProvableM m a => a -> m String
- solve :: MonadSymbolic m => [SBool] -> m SBool
- constrain :: (SolverContext m, QuantifiedBool a) => a -> m ()
- softConstrain :: (SolverContext m, QuantifiedBool a) => a -> m ()
- namedConstraint :: (SolverContext m, QuantifiedBool a) => String -> a -> m ()
- constrainWithAttribute :: (SolverContext m, QuantifiedBool a) => [(String, String)] -> a -> 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 :: Type -> Type) a where
- sName :: 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
- assertWithPenalty :: MonadSymbolic m => String -> SBool -> Penalty -> m ()
- data Penalty
- data ExtCV
- data GeneralizedCV
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- data AllSatResult = AllSatResult {}
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- data SMTResult
- data SMTReasonUnknown
- observe :: SymVal a => String -> SBV a -> SBV a
- sObserve :: MonadSymbolic m => String -> SVal -> m ()
- 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
- extractModel :: SatModel b => a -> Maybe b
- getModelObjectives :: a -> Map String GeneralizedCV
- getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
- getModelUIFuns :: a -> Map String (Bool, SBVType, Either String ([([CV], CV)], CV))
- getModelUIFunValue :: String -> a -> Maybe (Bool, SBVType, Either String ([([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]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- crackNum :: Bool
- crackNumSurfaceVals :: [(String, Integer)]
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- allSatTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- dsatPrecision :: Maybe Double
- solver :: SMTSolver
- extraArgs :: [String]
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- smtLib2Compliant :: Bool
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath
- firstifyUniqueLen :: Int
- tpOptions :: TPOptions
- data Timing
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: Text -> Text
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- boolector :: SMTConfig
- bitwuzla :: SMTConfig
- cvc4 :: SMTConfig
- cvc5 :: SMTConfig
- dReal :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- getAvailableSolvers :: 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
- isRational :: a -> Bool
- isFP :: a -> Bool
- isUnbounded :: a -> Bool
- isADT :: a -> Bool
- isChar :: a -> Bool
- isString :: a -> Bool
- isList :: a -> Bool
- isSet :: a -> Bool
- isTuple :: a -> Bool
- isArray :: a -> Bool
- isRoundingMode :: a -> Bool
- isUninterpreted :: a -> Bool
- showType :: a -> String
- data Kind
- class (HasKind a, Typeable a, Arbitrary a) => SymVal a where
- mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV a)
- mkSymValInit :: State -> SBV a -> IO ()
- literal :: a -> SBV a
- fromCV :: CV -> a
- isConcretely :: SBV a -> (a -> Bool) -> Bool
- minMaxBound :: Maybe (a, 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
- unlitCV :: SBV a -> Maybe (Kind, CVal)
- isConcrete :: SBV a -> Bool
- isSymbolic :: SBV a -> Bool
- class MonadIO m => MonadSymbolic (m :: Type -> Type) where
- symbolicEnv :: m State
- type Symbolic = SymbolicT IO
- data SymbolicT (m :: Type -> Type) 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 (SBV 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
| KnownNat n => Arbitrary (IntN n) Source # | Quickcheck instance for IntN | ||||
| (KnownNat n, BVIsNonZero n) => Bits (IntN n) Source # | |||||
Defined in Data.SBV.Core.Sized Methods (.&.) :: IntN n -> IntN n -> IntN n # (.|.) :: IntN n -> IntN n -> IntN n # xor :: IntN n -> IntN n -> IntN n # complement :: IntN n -> IntN n # shift :: IntN n -> Int -> IntN n # rotate :: IntN n -> Int -> IntN n # setBit :: IntN n -> Int -> IntN n # clearBit :: IntN n -> Int -> IntN n # complementBit :: IntN n -> Int -> IntN n # testBit :: IntN n -> Int -> Bool # bitSizeMaybe :: IntN n -> Maybe Int # shiftL :: IntN n -> Int -> IntN n # unsafeShiftL :: IntN n -> Int -> IntN n # shiftR :: IntN n -> Int -> IntN n # unsafeShiftR :: IntN n -> Int -> IntN n # rotateL :: IntN n -> Int -> IntN n # | |||||
| (KnownNat n, BVIsNonZero n) => Bounded (IntN n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => Enum (IntN n) Source # | |||||
Defined in Data.SBV.Core.Sized | |||||
| KnownNat n => Num (SInt n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => Num (IntN n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => Integral (IntN n) Source # | |||||
Defined in Data.SBV.Core.Sized | |||||
| (KnownNat n, BVIsNonZero n) => Real (IntN n) Source # | |||||
Defined in Data.SBV.Core.Sized Methods toRational :: IntN n -> Rational # | |||||
| Show (IntN n) Source # | Show instance for | ||||
| Eq (IntN n) Source # | |||||
| Ord (IntN n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => SymVal (IntN n) Source # | |||||
Defined in Data.SBV.Core.Model Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (IntN n)) Source # mkSymValInit :: State -> SBV (IntN n) -> IO () Source # literal :: IntN n -> SBV (IntN n) Source # fromCV :: CV -> IntN n Source # isConcretely :: SBV (IntN n) -> (IntN n -> Bool) -> Bool Source # minMaxBound :: Maybe (IntN n, IntN n) Source # free :: MonadSymbolic m => String -> m (SBV (IntN n)) Source # free_ :: MonadSymbolic m => m (SBV (IntN n)) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV (IntN n)] Source # symbolic :: MonadSymbolic m => String -> m (SBV (IntN n)) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV (IntN n)] Source # unliteral :: SBV (IntN n) -> Maybe (IntN n) Source # unlitCV :: SBV (IntN n) -> Maybe (Kind, CVal) Source # | |||||
| (KnownNat n, BVIsNonZero n) => HasKind (IntN n) Source # |
| ||||
Defined in Data.SBV.Core.Sized Methods kindOf :: IntN n -> Kind Source # hasSign :: IntN n -> Bool Source # intSizeOf :: IntN n -> Int Source # isBoolean :: IntN n -> Bool Source # isBounded :: IntN n -> Bool Source # isReal :: IntN n -> Bool Source # isFloat :: IntN n -> Bool Source # isDouble :: IntN n -> Bool Source # isRational :: IntN n -> Bool Source # isFP :: IntN n -> Bool Source # isUnbounded :: IntN n -> Bool Source # isADT :: IntN n -> Bool Source # isChar :: IntN n -> Bool Source # isString :: IntN n -> Bool Source # isList :: IntN n -> Bool Source # isSet :: IntN n -> Bool Source # isTuple :: IntN n -> Bool Source # isArray :: IntN n -> Bool Source # isRoundingMode :: IntN n -> Bool Source # isUninterpreted :: IntN n -> Bool Source # | |||||
| (KnownNat n, BVIsNonZero n) => Metric (IntN n) Source # | Optimizing | ||||
Defined in Data.SBV.Core.Model Associated Types
Methods toMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n)) Source # fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n) Source # annotateForMS :: Proxy (IntN n) -> String -> String Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (IntN n) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (IntN n) -> m () Source # | |||||
| (KnownNat n, BVIsNonZero n) => OrdSymbolic (SInt n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) Source # |
| ||||
Defined in Data.SBV.Core.Model | |||||
| (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) Source # |
| ||||
Defined in Data.SBV.Core.Model | |||||
| (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) Source # | |||||
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV (IntN n) -> Int Source # lsb :: SBV (IntN n) -> SBool Source # msb :: SBV (IntN n) -> SBool Source # blastBE :: SBV (IntN n) -> [SBool] Source # blastLE :: SBV (IntN n) -> [SBool] Source # fromBitsBE :: [SBool] -> SBV (IntN n) Source # fromBitsLE :: [SBool] -> SBV (IntN n) Source # sTestBit :: SBV (IntN n) -> Int -> SBool Source # sExtractBits :: SBV (IntN n) -> [Int] -> [SBool] Source # sPopCount :: SBV (IntN n) -> SWord8 Source # setBitTo :: SBV (IntN n) -> Int -> SBool -> SBV (IntN n) Source # sSetBitTo :: SBV (IntN n) -> SBV (IntN n) -> SBool -> SBV (IntN n) Source # fullAdder :: SBV (IntN n) -> SBV (IntN n) -> (SBool, SBV (IntN n)) Source # fullMultiplier :: SBV (IntN n) -> SBV (IntN n) -> (SBV (IntN n), SBV (IntN n)) Source # | |||||
| (KnownNat n, BVIsNonZero n) => SIntegral (IntN n) Source # | |||||
Defined in Data.SBV.Core.Model | |||||
| (KnownNat n, BVIsNonZero n) => Zero (IntN n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => SatModel (IntN n) Source # | Constructing models for | ||||
| (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) Source # | |||||
| (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) Source # | |||||
| type MetricSpace (IntN n) Source # | |||||
Defined in Data.SBV.Core.Model | |||||
Converting between fixed-size and arbitrary bit-vectors
type family BVIsNonZero (arg :: Nat) where ... Source #
Type family to create the appropriate non-zero constraint
Equations
| BVIsNonZero 0 = TypeError BVZeroWidth :: Constraint | |
| BVIsNonZero _1 = () |
type family FromSized t 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 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
type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) Source #
A symbolic arbitrary precision floating point value
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
| Arbitrary AlgReal Source # | |||||
| Data AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AlgReal -> c AlgReal # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AlgReal # toConstr :: AlgReal -> Constr # dataTypeOf :: AlgReal -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AlgReal) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AlgReal) # gmapT :: (forall b. Data b => b -> b) -> AlgReal -> AlgReal # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AlgReal -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AlgReal -> r # gmapQ :: (forall d. Data d => d -> u) -> AlgReal -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AlgReal -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AlgReal -> m AlgReal # | |||||
| Enum AlgReal Source # | |||||
| Floating SReal Source # | SReal Floating instance, used in conjunction with the dReal solver for delta-satisfiability. Note that we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing them for arbitrary rationals. | ||||
| Generic AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals Associated Types
| |||||
| Num AlgReal Source # | |||||
| Num SReal Source # | |||||
| Fractional AlgReal Source # | NB: Following the other types we have, we require `a/0` to be `0` for all a. | ||||
| Real AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals Methods toRational :: AlgReal -> Rational # | |||||
| Show AlgReal Source # | |||||
| NFData AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals | |||||
| Eq AlgReal Source # | |||||
| Ord AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals | |||||
| Random AlgReal Source # | Random generates a rational, so perhaps not as random as one wants | ||||
| SymVal AlgReal Source # | |||||
Defined in Data.SBV.Core.Model Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV AlgReal) Source # mkSymValInit :: State -> SBV AlgReal -> IO () Source # literal :: AlgReal -> SBV AlgReal Source # fromCV :: CV -> AlgReal Source # isConcretely :: SBV AlgReal -> (AlgReal -> Bool) -> Bool Source # minMaxBound :: Maybe (AlgReal, AlgReal) Source # free :: MonadSymbolic m => String -> m (SBV AlgReal) Source # free_ :: MonadSymbolic m => m (SBV AlgReal) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV AlgReal] Source # symbolic :: MonadSymbolic m => String -> m (SBV AlgReal) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV AlgReal] Source # unliteral :: SBV AlgReal -> Maybe AlgReal Source # unlitCV :: SBV AlgReal -> Maybe (Kind, CVal) Source # | |||||
| IEEEFloatConvertible AlgReal Source # | |||||
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal Source # toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal Source # toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV AlgReal Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb Source # | |||||
| HasKind AlgReal Source # | |||||
Defined in Data.SBV.Core.Kind Methods kindOf :: AlgReal -> Kind Source # hasSign :: AlgReal -> Bool Source # intSizeOf :: AlgReal -> Int Source # isBoolean :: AlgReal -> Bool Source # isBounded :: AlgReal -> Bool Source # isReal :: AlgReal -> Bool Source # isFloat :: AlgReal -> Bool Source # isDouble :: AlgReal -> Bool Source # isRational :: AlgReal -> Bool Source # isFP :: AlgReal -> Bool Source # isUnbounded :: AlgReal -> Bool Source # isADT :: AlgReal -> Bool Source # isChar :: AlgReal -> Bool Source # isString :: AlgReal -> Bool Source # isList :: AlgReal -> Bool Source # isSet :: AlgReal -> Bool Source # isTuple :: AlgReal -> Bool Source # isArray :: AlgReal -> Bool Source # isRoundingMode :: AlgReal -> Bool Source # isUninterpreted :: AlgReal -> Bool Source # | |||||
| Metric AlgReal Source # | |||||
Defined in Data.SBV.Core.Model Associated Types
Methods toMetricSpace :: SBV AlgReal -> SBV (MetricSpace AlgReal) Source # fromMetricSpace :: SBV (MetricSpace AlgReal) -> SBV AlgReal Source # annotateForMS :: Proxy AlgReal -> String -> String Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV AlgReal -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV AlgReal -> m () Source # | |||||
| OrdSymbolic SReal Source # | |||||
| (TypeError (((((('Text "A termination measure may not have a real-valued result." ':$$: 'Text "") ':$$: 'Text "The reals are not well-ordered: an infinite descending chain such as") ':$$: 'Text "1, 1/2, 1/4, ... has no least element, so a non-negative and strictly") ':$$: 'Text "decreasing real measure does not imply termination.") ':$$: 'Text "") ':$$: 'Text "Use an integer-valued measure instead (e.g. a count of remaining steps).") :: Constraint) => Zero AlgReal Source # | Algebraic reals are not permitted as measures, and we reject them at compile time.
The reals are dense, hence not well-ordered: a merely non-negative and strictly-decreasing
real measure does not imply termination (e.g. the chain | ||||
| EnumSymbolic AlgReal Source # | 'EnumSymbolic instance for arbitrary AlgReal. We don't have to use the multiplicative trick here
since alg-reals are precise. But, following rational in Haskell, we do use the stopping point of | ||||
Defined in Data.SBV.List Methods succ :: SBV AlgReal -> SBV AlgReal Source # pred :: SBV AlgReal -> SBV AlgReal Source # toEnum :: SInteger -> SBV AlgReal Source # fromEnum :: SBV AlgReal -> SInteger Source # enumFrom :: SBV AlgReal -> SList AlgReal Source # enumFromThen :: SBV AlgReal -> SBV AlgReal -> SList AlgReal Source # enumFromTo :: SBV AlgReal -> SBV AlgReal -> SList AlgReal Source # enumFromThenTo :: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> SList AlgReal Source # enumFromThenToH :: SBV AlgReal -> SBV AlgReal -> SBV AlgReal -> Maybe Integer -> SList AlgReal Source # | |||||
| SatModel AlgReal Source # |
| ||||
| type Rep AlgReal Source # | |||||
Defined in Data.SBV.Core.AlgReals type Rep AlgReal = D1 ('MetaData "AlgReal" "Data.SBV.Core.AlgReals" "sbv-14.5-IBEFSqbfTM3Hrq5kB21pv3" 'False) (C1 ('MetaCons "AlgRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: (C1 ('MetaCons "AlgPolyRoot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Integer, AlgRealPoly)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))) :+: C1 ('MetaCons "AlgInterval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RealPoint Rational)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RealPoint Rational))))) | |||||
| type MetricSpace AlgReal Source # | |||||
Defined in Data.SBV.Core.Model | |||||
sRealToSIntegerFloor :: SReal -> SInteger Source #
Convert an SReal to an SInteger, floor version. That is, it computes the
largest integer n that satisfies sIntegerToSReal n <= r.
For instance, 1.3 will be 1, but -1.3 will be -2.
See sRealToSIntegerRM to select the rounding mode with a symbolic SRoundingMode.
sRealToSIntegerCeiling :: SReal -> SInteger Source #
Convert an SReal to an SInteger, ceiling version. That is, it computes
the smallest integer n that satisfies r <= sIntegerToSReal n.
For instance, 1.3 will be 2, but -1.3 will be -1.
See sRealToSIntegerRM to select the rounding mode with a symbolic SRoundingMode.
sRealToSIntegerTruncate :: SReal -> SInteger Source #
Convert an SReal to an SInteger, truncating version. Truncate simply chops off the fractional part, essentially rounding towards zero.
For instance, 1.3 will be 1, and -1.3 will be -1.
See sRealToSIntegerRM to select the rounding mode with a symbolic SRoundingMode.
sRealToSIntegerRoundAway :: SReal -> SInteger Source #
Convert an SReal to an SInteger by converting to the nearest integer. If there is a tie (i.e., if the fractional component of the SReal is equal to 0.5), then round away from zero.
For instance:
1.3will be11.5will be2(becauseabs 1 < abs 2)1.7will be22.3will be22.5will be3(becauseabs 2 < abs 3)2.7will be3-1.3will be-1-1.5will be-2(becauseabs (-1) < abs (-2))-1.7will be-2-2.3will be-2-2.5will be-3(becauseabs (-2) < abs (-3))-2.7will be-3
See sRealToSIntegerRM to select the rounding mode with a symbolic SRoundingMode.
sRealToSIntegerRoundToEven :: SReal -> SInteger Source #
Convert an SReal to an SInteger by converting to the nearest integer. If there is a tie (i.e., if the fractional component of the SReal is equal to 0.5), then round to the nearest even integer.
For instance:
1.3will be11.5will be2(because2is even)1.7will be22.3will be22.5will be2(because2is even)2.7will be3-1.3will be-1-1.5will be-2(because-2is even)-1.7will be-2-2.3will be-2-2.5will be-2(because-2is even)-2.7will be-3
See sRealToSIntegerRM to select the rounding mode with a symbolic SRoundingMode.
sRealToSIntegerRM :: SRoundingMode -> SReal -> SInteger Source #
Convert an SReal to an SInteger according to the supplied
SRoundingMode. This dispatches to sRealToSIntegerRoundToEven,
sRealToSIntegerRoundAway, sRealToSIntegerCeiling, sRealToSIntegerFloor,
and sRealToSIntegerTruncate for the round-nearest-even, round-nearest-away,
round-toward-positive, round-toward-negative, and round-toward-zero modes
respectively.
Note that we re-use the SRoundingMode type here, even though
SRoundingMode is normally associated with floating-point operations. The
floating-point resemblance is superficial, as this function does not use any
floating-point functionality behind the scenes.
Characters, Strings and Regular Expressions
type SChar = SBV Char Source #
A symbolic character. Note that this is the full unicode character set. see: https://smt-lib.org/theories-UnicodeStrings.shtml for details.
type SString = SBV String Source #
A symbolic string. Note that a symbolic string is not a list of symbolic characters,
that is, it is not the case that SString = [SChar], unlike what one might expect following
Haskell strings. An SString is a symbolic value of its own, of possibly arbitrary but finite length,
and internally processed as one unit as opposed to a fixed-length list of characters.
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
readArray :: (SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val Source #
Reading a value from an array.
writeArray :: (HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val Source #
Writing a value to an array. For the concrete case, we don't bother deleting earlier entries, we keep a history. The earlier a value is in the list, the "later" it happened; in a stack fashion.
type SArray a b = SBV (ArrayModel a b) Source #
Symbolic arrays. A symbolic array is more akin to a function in SMTLib (and thus in SBV),
as opposed to contagious-storage with a finite range as found in many programming languages.
Additionally, the domain uses object-equality in the SMTLib semantics. Object equality is
the same as regular equality for most types, except for IEEE-Floats, where NaN doesn't compare
equal to itself and +0 and -0 are not distinguished. So, if your index type is a float,
then NaN can be stored correctly, and 0 and -0 will be distinguished. If you don't use
floats, then you can treat this the same as regular equality in Haskell.
Creating symbolic values
Single value
sWord :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero n, MonadSymbolic m) => String -> m (SWord n) Source #
Generalization of sWord
sInt :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero n, MonadSymbolic m) => String -> m (SInt n) Source #
Generalization of sInt
sArray :: (SymVal a, SymVal b, MonadSymbolic m) => String -> m (SArray a b) Source #
Generalization of sAray
List of values
sWords :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero n, MonadSymbolic m) => [String] -> m [SWord n] Source #
Generalization of sWord64s
sInts :: forall (n :: Nat) m. (KnownNat n, BVIsNonZero n, MonadSymbolic m) => [String] -> m [SInt n] Source #
Generalization of sInts
sArrays :: (SymVal a, SymVal b, MonadSymbolic m) => [String] -> m [SArray a b] Source #
Generalization of sLists
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.
NB. Equality is a built-in notion in SMTLib, and is object-equality. While this mostly matches Haskell's
notion of equality, the correspondence isn't exact. This mostly shows up in containers with floats inside,
such as sequences of floats, sets of doubles, and arrays of doubles. While SBV tries to maintain Haskell
semantics, it does resort to container equality for compound types. For instance, for an IEEE-float,
-0 == 0. But for an SMTLib sequence, equals is done over objects. i.e., [0] == [-0] in Haskell, but
literal [0] ./= literal [-0] when used as SMTLib sequences. The rabbit-hole goes deep here, especially
when NaN is involved, which does not compare equal to itself per IEEE-semantics.
If you are not using floats, then you can ignore all this. If you do, then SBV will do the right thing for them when checking equality directly, but not when you use containers with floating-point elements. In the latter case, object-equality will be used.
Minimal complete definition: None, if the type is instance of Generic. Otherwise (.==).
Minimal complete definition
Nothing
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.
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 RegExp Source # | Regular expressions can be compared for equality. Note that we diverge here from the equality in the concrete sense; i.e., the Eq instance does not match the symbolic case. This is a bit unfortunate, but unavoidable with the current design of how we "distinguish" operators. Hopefully shouldn't be a big deal, though one should be careful. |
Defined in Data.SBV.Core.Model Methods (.==) :: RegExp -> RegExp -> SBool Source # (./=) :: RegExp -> RegExp -> SBool Source # (.===) :: RegExp -> RegExp -> SBool Source # (./==) :: RegExp -> RegExp -> SBool Source # distinct :: [RegExp] -> SBool Source # distinctExcept :: [RegExp] -> [RegExp] -> SBool Source # allEqual :: [RegExp] -> SBool Source # | |
| 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 (NonEmpty a) Source # | |
Defined in Data.SBV.Core.Model Methods (.==) :: NonEmpty a -> NonEmpty a -> SBool Source # (./=) :: NonEmpty a -> NonEmpty a -> SBool Source # (.===) :: NonEmpty a -> NonEmpty a -> SBool Source # (./==) :: NonEmpty a -> NonEmpty a -> SBool Source # distinct :: [NonEmpty a] -> SBool Source # distinctExcept :: [NonEmpty a] -> [NonEmpty a] -> SBool Source # allEqual :: [NonEmpty a] -> SBool Source # | |
| (HasKind a, SymVal a) => 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 (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 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 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 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 within the allowed inclusive range?
Instances
| OrdSymbolic SChar Source # | |
| OrdSymbolic SDouble Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic SFloat Source # | |
| OrdSymbolic SInt16 Source # | |
| OrdSymbolic SInt32 Source # | |
| OrdSymbolic SInt64 Source # | |
| OrdSymbolic SInt8 Source # | |
| OrdSymbolic SInteger Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SInteger -> SInteger -> SBool Source # (.<=) :: SInteger -> SInteger -> SBool Source # (.>) :: SInteger -> SInteger -> SBool Source # (.>=) :: SInteger -> SInteger -> SBool Source # smin :: SInteger -> SInteger -> SInteger Source # smax :: SInteger -> SInteger -> SInteger Source # inRange :: SInteger -> (SInteger, SInteger) -> SBool Source # | |
| OrdSymbolic SRational Source # | Symbolic ordering for SRational. Note that denominators are always positive. |
Defined in Data.SBV.Rational Methods (.<) :: SRational -> SRational -> SBool Source # (.<=) :: SRational -> SRational -> SBool Source # (.>) :: SRational -> SRational -> SBool Source # (.>=) :: SRational -> SRational -> SBool Source # smin :: SRational -> SRational -> SRational Source # smax :: SRational -> SRational -> SRational Source # inRange :: SRational -> (SRational, SRational) -> SBool Source # | |
| OrdSymbolic SReal Source # | |
| OrdSymbolic SWord16 Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic SWord32 Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic SWord64 Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic SWord8 Source # | |
| OrdSymbolic SNat Source # | Symbolic ordering. We only define less-than, other methods use the defaults. |
Defined in Documentation.SBV.Examples.TP.Peano | |
| OrdSymbolic a => OrdSymbolic (NonEmpty a) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: NonEmpty a -> NonEmpty a -> SBool Source # (.<=) :: NonEmpty a -> NonEmpty a -> SBool Source # (.>) :: NonEmpty a -> NonEmpty a -> SBool Source # (.>=) :: NonEmpty a -> NonEmpty a -> SBool Source # smin :: NonEmpty a -> NonEmpty a -> NonEmpty a Source # smax :: NonEmpty a -> NonEmpty a -> NonEmpty a Source # inRange :: NonEmpty a -> (NonEmpty a, NonEmpty a) -> SBool Source # | |
| (OrdSymbolic (SBV a), OrdSymbolic (SBV b), SymVal a, SymVal b) => OrdSymbolic (SBV (Either a b)) Source # | Custom |
Defined in Data.SBV.Either Methods (.<) :: SBV (Either a b) -> SBV (Either a b) -> SBool Source # (.<=) :: SBV (Either a b) -> SBV (Either a b) -> SBool Source # (.>) :: SBV (Either a b) -> SBV (Either a b) -> SBool Source # (.>=) :: SBV (Either a b) -> SBV (Either a b) -> SBool Source # smin :: SBV (Either a b) -> SBV (Either a b) -> SBV (Either a b) Source # smax :: SBV (Either a b) -> SBV (Either a b) -> SBV (Either a b) Source # inRange :: SBV (Either a b) -> (SBV (Either a b), SBV (Either a b)) -> SBool Source # | |
| OrdSymbolic (SBV State) Source # | |
Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods (.<) :: SBV State -> SBV State -> SBool Source # (.<=) :: SBV State -> SBV State -> SBool Source # (.>) :: SBV State -> SBV State -> SBool Source # (.>=) :: SBV State -> SBV State -> SBool Source # smin :: SBV State -> SBV State -> SBV State Source # smax :: SBV State -> SBV State -> SBV State Source # inRange :: SBV State -> (SBV State, SBV State) -> SBool Source # | |
| OrdSymbolic (SBV E) Source # | |
Defined in Documentation.SBV.Examples.Misc.Enumerate | |
| OrdSymbolic (SBV E) Source # | |
| OrdSymbolic (SBV Day) Source # | |
Defined in Documentation.SBV.Examples.Optimization.Enumerate | |
| OrdSymbolic (SBV Day) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Birthday | |
| OrdSymbolic (SBV Month) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods (.<) :: SBV Month -> SBV Month -> SBool Source # (.<=) :: SBV Month -> SBV Month -> SBool Source # (.>) :: SBV Month -> SBV Month -> SBool Source # (.>=) :: SBV Month -> SBV Month -> SBool Source # smin :: SBV Month -> SBV Month -> SBV Month Source # smax :: SBV Month -> SBV Month -> SBV Month Source # inRange :: SBV Month -> (SBV Month, SBV Month) -> SBool Source # | |
| OrdSymbolic (SBV Action) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.DieHard Methods (.<) :: SBV Action -> SBV Action -> SBool Source # (.<=) :: SBV Action -> SBV Action -> SBool Source # (.>) :: SBV Action -> SBV Action -> SBool Source # (.>=) :: SBV Action -> SBV Action -> SBool Source # smin :: SBV Action -> SBV Action -> SBV Action Source # smax :: SBV Action -> SBV Action -> SBV Action Source # inRange :: SBV Action -> (SBV Action, SBV Action) -> SBool Source # | |
| OrdSymbolic (SBV Beverage) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Beverage -> SBV Beverage -> SBool Source # (.<=) :: SBV Beverage -> SBV Beverage -> SBool Source # (.>) :: SBV Beverage -> SBV Beverage -> SBool Source # (.>=) :: SBV Beverage -> SBV Beverage -> SBool Source # smin :: SBV Beverage -> SBV Beverage -> SBV Beverage Source # smax :: SBV Beverage -> SBV Beverage -> SBV Beverage Source # inRange :: SBV Beverage -> (SBV Beverage, SBV Beverage) -> SBool Source # | |
| OrdSymbolic (SBV Color) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Color -> SBV Color -> SBool Source # (.<=) :: SBV Color -> SBV Color -> SBool Source # (.>) :: SBV Color -> SBV Color -> SBool Source # (.>=) :: SBV Color -> SBV Color -> SBool Source # smin :: SBV Color -> SBV Color -> SBV Color Source # smax :: SBV Color -> SBV Color -> SBV Color Source # inRange :: SBV Color -> (SBV Color, SBV Color) -> SBool Source # | |
| OrdSymbolic (SBV Nationality) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Nationality -> SBV Nationality -> SBool Source # (.<=) :: SBV Nationality -> SBV Nationality -> SBool Source # (.>) :: SBV Nationality -> SBV Nationality -> SBool Source # (.>=) :: SBV Nationality -> SBV Nationality -> SBool Source # smin :: SBV Nationality -> SBV Nationality -> SBV Nationality Source # smax :: SBV Nationality -> SBV Nationality -> SBV Nationality Source # inRange :: SBV Nationality -> (SBV Nationality, SBV Nationality) -> SBool Source # | |
| OrdSymbolic (SBV Pet) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish | |
| OrdSymbolic (SBV Sport) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Sport -> SBV Sport -> SBool Source # (.<=) :: SBV Sport -> SBV Sport -> SBool Source # (.>) :: SBV Sport -> SBV Sport -> SBool Source # (.>=) :: SBV Sport -> SBV Sport -> SBool Source # smin :: SBV Sport -> SBV Sport -> SBV Sport Source # smax :: SBV Sport -> SBV Sport -> SBV Sport Source # inRange :: SBV Sport -> (SBV Sport, SBV Sport) -> SBool Source # | |
| OrdSymbolic (SBV Color) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Garden Methods (.<) :: SBV Color -> SBV Color -> SBool Source # (.<=) :: SBV Color -> SBV Color -> SBool Source # (.>) :: SBV Color -> SBV Color -> SBool Source # (.>=) :: SBV Color -> SBV Color -> SBool Source # smin :: SBV Color -> SBV Color -> SBV Color Source # smax :: SBV Color -> SBV Color -> SBV Color Source # inRange :: SBV Color -> (SBV Color, SBV Color) -> SBool Source # | |
| OrdSymbolic (SBV Color) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods (.<) :: SBV Color -> SBV Color -> SBool Source # (.<=) :: SBV Color -> SBV Color -> SBool Source # (.>) :: SBV Color -> SBV Color -> SBool Source # (.>=) :: SBV Color -> SBV Color -> SBool Source # smin :: SBV Color -> SBV Color -> SBV Color Source # smax :: SBV Color -> SBV Color -> SBV Color Source # inRange :: SBV Color -> (SBV Color, SBV Color) -> SBool Source # | |
| OrdSymbolic (SBV Identity) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods (.<) :: SBV Identity -> SBV Identity -> SBool Source # (.<=) :: SBV Identity -> SBV Identity -> SBool Source # (.>) :: SBV Identity -> SBV Identity -> SBool Source # (.>=) :: SBV Identity -> SBV Identity -> SBool Source # smin :: SBV Identity -> SBV Identity -> SBV Identity Source # smax :: SBV Identity -> SBV Identity -> SBV Identity Source # inRange :: SBV Identity -> (SBV Identity, SBV Identity) -> SBool Source # | |
| OrdSymbolic (SBV Statement) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods (.<) :: SBV Statement -> SBV Statement -> SBool Source # (.<=) :: SBV Statement -> SBV Statement -> SBool Source # (.>) :: SBV Statement -> SBV Statement -> SBool Source # (.>=) :: SBV Statement -> SBV Statement -> SBool Source # smin :: SBV Statement -> SBV Statement -> SBV Statement Source # smax :: SBV Statement -> SBV Statement -> SBV Statement Source # inRange :: SBV Statement -> (SBV Statement, SBV Statement) -> SBool Source # | |
| OrdSymbolic (SBV Location) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (.<) :: SBV Location -> SBV Location -> SBool Source # (.<=) :: SBV Location -> SBV Location -> SBool Source # (.>) :: SBV Location -> SBV Location -> SBool Source # (.>=) :: SBV Location -> SBV Location -> SBool Source # smin :: SBV Location -> SBV Location -> SBV Location Source # smax :: SBV Location -> SBV Location -> SBV Location Source # inRange :: SBV Location -> (SBV Location, SBV Location) -> SBool Source # | |
| OrdSymbolic (SBV Role) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (.<) :: SBV Role -> SBV Role -> SBool Source # (.<=) :: SBV Role -> SBV Role -> SBool Source # (.>) :: SBV Role -> SBV Role -> SBool Source # (.>=) :: SBV Role -> SBV Role -> SBool Source # smin :: SBV Role -> SBV Role -> SBV Role Source # smax :: SBV Role -> SBV Role -> SBV Role Source # inRange :: SBV Role -> (SBV Role, SBV Role) -> SBool Source # | |
| OrdSymbolic (SBV Sex) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Murder | |
| OrdSymbolic (SBV Handler) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods (.<) :: SBV Handler -> SBV Handler -> SBool Source # (.<=) :: SBV Handler -> SBV Handler -> SBool Source # (.>) :: SBV Handler -> SBV Handler -> SBool Source # (.>=) :: SBV Handler -> SBV Handler -> SBool Source # smin :: SBV Handler -> SBV Handler -> SBV Handler Source # smax :: SBV Handler -> SBV Handler -> SBV Handler Source # inRange :: SBV Handler -> (SBV Handler, SBV Handler) -> SBool Source # | |
| OrdSymbolic (SBV Location) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods (.<) :: SBV Location -> SBV Location -> SBool Source # (.<=) :: SBV Location -> SBV Location -> SBool Source # (.>) :: SBV Location -> SBV Location -> SBool Source # (.>=) :: SBV Location -> SBV Location -> SBool Source # smin :: SBV Location -> SBV Location -> SBV Location Source # smax :: SBV Location -> SBV Location -> SBV Location Source # inRange :: SBV Location -> (SBV Location, SBV Location) -> SBool Source # | |
| OrdSymbolic (SBV Orangutan) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods (.<) :: SBV Orangutan -> SBV Orangutan -> SBool Source # (.<=) :: SBV Orangutan -> SBV Orangutan -> SBool Source # (.>) :: SBV Orangutan -> SBV Orangutan -> SBool Source # (.>=) :: SBV Orangutan -> SBV Orangutan -> SBool Source # smin :: SBV Orangutan -> SBV Orangutan -> SBV Orangutan Source # smax :: SBV Orangutan -> SBV Orangutan -> SBV Orangutan Source # inRange :: SBV Orangutan -> (SBV Orangutan, SBV Orangutan) -> SBool Source # | |
| OrdSymbolic (SBV Month) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.SquareBirthday Methods (.<) :: SBV Month -> SBV Month -> SBool Source # (.<=) :: SBV Month -> SBV Month -> SBool Source # (.>) :: SBV Month -> SBV Month -> SBool Source # (.>=) :: SBV Month -> SBV Month -> SBool Source # smin :: SBV Month -> SBV Month -> SBV Month Source # smax :: SBV Month -> SBV Month -> SBV Month Source # inRange :: SBV Month -> (SBV Month, SBV Month) -> SBool Source # | |
| OrdSymbolic (SBV Location) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods (.<) :: SBV Location -> SBV Location -> SBool Source # (.<=) :: SBV Location -> SBV Location -> SBool Source # (.>) :: SBV Location -> SBV Location -> SBool Source # (.>=) :: SBV Location -> SBV Location -> SBool Source # smin :: SBV Location -> SBV Location -> SBV Location Source # smax :: SBV Location -> SBV Location -> SBV Location Source # inRange :: SBV Location -> (SBV Location, SBV Location) -> SBool Source # | |
| OrdSymbolic (SBV U2Member) Source # | |
Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods (.<) :: SBV U2Member -> SBV U2Member -> SBool Source # (.<=) :: SBV U2Member -> SBV U2Member -> SBool Source # (.>) :: SBV U2Member -> SBV U2Member -> SBool Source # (.>=) :: SBV U2Member -> SBV U2Member -> SBool Source # smin :: SBV U2Member -> SBV U2Member -> SBV U2Member Source # smax :: SBV U2Member -> SBV U2Member -> SBV U2Member Source # inRange :: SBV U2Member -> (SBV U2Member, SBV U2Member) -> SBool Source # | |
| OrdSymbolic (SBV Day) Source # | |
Defined in Documentation.SBV.Examples.Queries.Enums | |
| OrdSymbolic (SBV BinOp) Source # | |
Defined in Documentation.SBV.Examples.Queries.FourFours Methods (.<) :: SBV BinOp -> SBV BinOp -> SBool Source # (.<=) :: SBV BinOp -> SBV BinOp -> SBool Source # (.>) :: SBV BinOp -> SBV BinOp -> SBool Source # (.>=) :: SBV BinOp -> SBV BinOp -> SBool Source # smin :: SBV BinOp -> SBV BinOp -> SBV BinOp Source # smax :: SBV BinOp -> SBV BinOp -> SBV BinOp Source # inRange :: SBV BinOp -> (SBV BinOp, SBV BinOp) -> SBool Source # | |
| OrdSymbolic (SBV UnOp) Source # | |
Defined in Documentation.SBV.Examples.Queries.FourFours Methods (.<) :: SBV UnOp -> SBV UnOp -> SBool Source # (.<=) :: SBV UnOp -> SBV UnOp -> SBool Source # (.>) :: SBV UnOp -> SBV UnOp -> SBool Source # (.>=) :: SBV UnOp -> SBV UnOp -> SBool Source # smin :: SBV UnOp -> SBV UnOp -> SBV UnOp Source # smax :: SBV UnOp -> SBV UnOp -> SBV UnOp Source # inRange :: SBV UnOp -> (SBV UnOp, SBV UnOp) -> SBool Source # | |
| (OrdSymbolic (SBV a), SymVal a) => OrdSymbolic (SBV (Maybe a)) Source # | Custom |
Defined in Data.SBV.Maybe Methods (.<) :: SBV (Maybe a) -> SBV (Maybe a) -> SBool Source # (.<=) :: SBV (Maybe a) -> SBV (Maybe a) -> SBool Source # (.>) :: SBV (Maybe a) -> SBV (Maybe a) -> SBool Source # (.>=) :: SBV (Maybe a) -> SBV (Maybe a) -> SBool Source # smin :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a) Source # smax :: SBV (Maybe a) -> SBV (Maybe a) -> SBV (Maybe a) Source # inRange :: SBV (Maybe a) -> (SBV (Maybe a), SBV (Maybe a)) -> SBool Source # | |
| (SymVal a, SymVal b) => OrdSymbolic (SBV (a, b)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b) -> SBV (a, b) -> SBool Source # (.<=) :: SBV (a, b) -> SBV (a, b) -> SBool Source # (.>) :: SBV (a, b) -> SBV (a, b) -> SBool Source # (.>=) :: SBV (a, b) -> SBV (a, b) -> SBool Source # smin :: SBV (a, b) -> SBV (a, b) -> SBV (a, b) Source # smax :: SBV (a, b) -> SBV (a, b) -> SBV (a, b) Source # inRange :: SBV (a, b) -> (SBV (a, b), SBV (a, b)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c) => OrdSymbolic (SBV (a, b, c)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c) -> SBV (a, b, c) -> SBool Source # (.<=) :: SBV (a, b, c) -> SBV (a, b, c) -> SBool Source # (.>) :: SBV (a, b, c) -> SBV (a, b, c) -> SBool Source # (.>=) :: SBV (a, b, c) -> SBV (a, b, c) -> SBool Source # smin :: SBV (a, b, c) -> SBV (a, b, c) -> SBV (a, b, c) Source # smax :: SBV (a, b, c) -> SBV (a, b, c) -> SBV (a, b, c) Source # inRange :: SBV (a, b, c) -> (SBV (a, b, c), SBV (a, b, c)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d) => OrdSymbolic (SBV (a, b, c, d)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBool Source # (.<=) :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBool Source # (.>) :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBool Source # (.>=) :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBool Source # smin :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBV (a, b, c, d) Source # smax :: SBV (a, b, c, d) -> SBV (a, b, c, d) -> SBV (a, b, c, d) Source # inRange :: SBV (a, b, c, d) -> (SBV (a, b, c, d), SBV (a, b, c, d)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e) => OrdSymbolic (SBV (a, b, c, d, e)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBool Source # (.<=) :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBool Source # (.>) :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBool Source # (.>=) :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBool Source # smin :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) Source # smax :: SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) -> SBV (a, b, c, d, e) Source # inRange :: SBV (a, b, c, d, e) -> (SBV (a, b, c, d, e), SBV (a, b, c, d, e)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f) => OrdSymbolic (SBV (a, b, c, d, e, f)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBool Source # (.<=) :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBool Source # (.>) :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBool Source # (.>=) :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBool Source # smin :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) Source # smax :: SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) Source # inRange :: SBV (a, b, c, d, e, f) -> (SBV (a, b, c, d, e, f), SBV (a, b, c, d, e, f)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g) => OrdSymbolic (SBV (a, b, c, d, e, f, g)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBool Source # (.<=) :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBool Source # (.>) :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBool Source # (.>=) :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBool Source # smin :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) Source # smax :: SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) Source # inRange :: SBV (a, b, c, d, e, f, g) -> (SBV (a, b, c, d, e, f, g), SBV (a, b, c, d, e, f, g)) -> SBool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h) => OrdSymbolic (SBV (a, b, c, d, e, f, g, h)) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBool Source # (.<=) :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBool Source # (.>) :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBool Source # (.>=) :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBool Source # smin :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) Source # smax :: SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) Source # inRange :: SBV (a, b, c, d, e, f, g, h) -> (SBV (a, b, c, d, e, f, g, h), SBV (a, b, c, d, e, f, g, h)) -> SBool Source # | |
| (KnownNat n, BVIsNonZero n) => OrdSymbolic (SInt n) Source # | |
| SymVal a => OrdSymbolic (SList a) Source # | |
Defined in Data.SBV.Core.Model | |
| (KnownNat n, BVIsNonZero n) => OrdSymbolic (SWord n) Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic a => OrdSymbolic (Maybe a) Source # | |
Defined in Data.SBV.Core.Model | |
| OrdSymbolic a => OrdSymbolic [a] Source # | |
| (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 # | |
| ValidFloat eb sb => OrdSymbolic (SFloatingPoint eb sb) Source # | |
Defined in Data.SBV.Core.Model Methods (.<) :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool Source # (.<=) :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool Source # (.>) :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool Source # (.>=) :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SBool Source # smin :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source # smax :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb Source # inRange :: SFloatingPoint eb sb -> (SFloatingPoint eb sb, SFloatingPoint eb sb) -> 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 OrdSymbolic (SBV a) => Zero a where Source #
A class of values that capture the notion of a zero for measure values. Used in termination checking for recursive SMT functions.
Minimal complete definition
Methods
nonNeg :: SBV a -> SBool Source #
Component-wise non-negativity check. For scalars this is simply >= 0.
For tuples, every component must be >= 0, which is stronger than
lexicographic >= (0, 0, ..). This is required for well-foundedness
of the lexicographic ordering on the non-negative part.
Instances
| Zero Int16 Source # | |
| Zero Int32 Source # | |
| Zero Int64 Source # | |
| Zero Int8 Source # | |
| Zero Word16 Source # | |
| Zero Word32 Source # | |
| Zero Word64 Source # | |
| Zero Word8 Source # | Bounded bit-vectors as measures. These are all sound: each is a finite type, so a
non-negative, strictly-decreasing chain of values is necessarily finite. (The default
|
| (TypeError (((((('Text "A termination measure may not have a real-valued result." ':$$: 'Text "") ':$$: 'Text "The reals are not well-ordered: an infinite descending chain such as") ':$$: 'Text "1, 1/2, 1/4, ... has no least element, so a non-negative and strictly") ':$$: 'Text "decreasing real measure does not imply termination.") ':$$: 'Text "") ':$$: 'Text "Use an integer-valued measure instead (e.g. a count of remaining steps).") :: Constraint) => Zero AlgReal Source # | Algebraic reals are not permitted as measures, and we reject them at compile time.
The reals are dense, hence not well-ordered: a merely non-negative and strictly-decreasing
real measure does not imply termination (e.g. the chain |
| Zero Integer Source # | An integer as a measure |
| Zero Double Source # | A double as a measure |
| Zero Float Source # | A float as a measure |
| (KnownNat n, BVIsNonZero n) => Zero (IntN n) Source # | |
| (KnownNat n, BVIsNonZero n) => Zero (WordN n) Source # | |
| ValidFloat eb sb => Zero (FloatingPoint eb sb) Source # | A floating-point as a measure |
Defined in Data.SBV.Core.Model | |
| Zero (Integer, Integer) Source # | A tuple of integers as a measure |
| Zero (Integer, Integer, Integer) Source # | A triple of integers as a measure |
| Zero (Integer, Integer, Integer, Integer) Source # | A quadruple of integers as a measure |
| Zero (Integer, Integer, Integer, Integer, Integer) Source # | A quintuple of integers as a measure |
type family MeasureOf f r where ... Source #
Type family that maps a function type to its corresponding measure type. The measure function takes the same arguments but returns a different type.
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
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # | |
| (SymVal a, SymVal b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # | |
| (SymVal a, EqSymbolic z) => Equality (SBV a -> z) Source # | |
| (SymVal a, SymVal b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) Source # | |
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, Num (SBV b), OrdSymbolic (SBV 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.
Instances
| Mergeable Int16 Source # | |
| Mergeable Int32 Source # | |
| Mergeable Int64 Source # | |
| Mergeable Int8 Source # | |
| Mergeable Word16 Source # | |
| Mergeable Word32 Source # | |
| Mergeable Word64 Source # | |
| Mergeable Word8 Source # | |
| Mergeable Mostek Source # | |
| Mergeable Jug Source # | |
| Mergeable Assignment Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods symbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment Source # select :: (Ord b, SymVal b, Num b, Num (SBV b), OrdSymbolic (SBV b)) => [Assignment] -> Assignment -> SBV b -> Assignment Source # | |
| Mergeable Status Source # | |
| Mergeable Integer Source # | |
| Mergeable () Source # | |
| Mergeable Bool Source # | |
| Mergeable Char Source # | |
| Mergeable Double Source # | |
| Mergeable Float Source # | |
| Mergeable a => Mergeable (ZipList a) Source # | |
| Mergeable a => Mergeable (NonEmpty a) Source # | |
| SymVal a => Mergeable (SBV a) Source # | |
| Mergeable a => Mergeable (Move a) Source # | Mergeable instance for |
| Mergeable a => Mergeable (AppS a) Source # | |
| Mergeable a => Mergeable (IncS a) Source # | |
| Mergeable a => Mergeable (FibS a) Source # | |
| Mergeable a => Mergeable (GCDS a) Source # | |
| Mergeable a => Mergeable (DivS a) Source # | |
| Mergeable a => Mergeable (SqrtS a) Source # | |
| Mergeable a => Mergeable (SumS a) Source # | |
| Mergeable a => Mergeable (Maybe a) Source # | |
| Mergeable a => Mergeable [a] Source # | |
| (Mergeable a, Mergeable b) => Mergeable (Either a b) Source # | |
| (Ix a, Mergeable b) => Mergeable (Array a b) Source # | |
| SymVal e => Mergeable (STree i e) Source # | |
| (Mergeable a, Mergeable b) => Mergeable (LenS a b) Source # | |
| (Mergeable a, Mergeable b) => Mergeable (a, b) Source # | |
| Mergeable b => Mergeable (a -> b) Source # | |
| (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) Source # | |
| (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) Source # | |
| (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) Source # | |
| (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) Source # | |
Defined in Data.SBV.Core.Model | |
| (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) Source # | |
Defined in Data.SBV.Core.Model | |
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, Num (SBV 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 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 Int8 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 | |
| SIntegral Word8 Source # | |
Defined in Data.SBV.Core.Model | |
| SIntegral Integer Source # | |
Defined in Data.SBV.Core.Model | |
| (KnownNat n, BVIsNonZero n) => SIntegral (IntN n) Source # | |
Defined in Data.SBV.Core.Model | |
| (KnownNat n, BVIsNonZero n) => SIntegral (WordN n) Source # | |
Defined in Data.SBV.Core.Model | |
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. sQuot truncates toward zero (i.e., it implements truncating division),
while sDiv truncates toward negative infinity (i.e., it implements
flooring division). These match the conventions of Haskell's quot and
div functions, respectively.
Similarly, sRem and sMod match the conventions of Haskell's rem and
mod functions, respectively. That is:
(xsQuoty)*y + (xsRemy) .== x (xsDivy)*y + (xsMody) .== x
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
| SDivisible Int16 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Int32 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Int64 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Int8 Source # | |
| SDivisible Word16 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Word32 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Word64 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Word8 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible CV Source # | |
| SDivisible SInt16 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible SInt32 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible SInt64 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible SInt8 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible SInteger Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible SWord16 Source # | |
| SDivisible SWord32 Source # | |
| SDivisible SWord64 Source # | |
| SDivisible SWord8 Source # | |
Defined in Data.SBV.Core.Model | |
| SDivisible Integer Source # | |
| (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) Source # |
|
Defined in Data.SBV.Core.Model | |
| (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) Source # |
|
| (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) Source # |
|
Defined in Data.SBV.Core.Model | |
| (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) Source # |
|
Bit-vector operations
Conversions
sFromIntegral :: (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 bit-vectors, 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.
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.
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, Num (SBV a), OrdSymbolic (SBV 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 #
sSetBitTo :: SBV a -> SBV a -> SBool -> SBV a Source #
Variant of setBitTo when the index is symbolic. If the index it out-of-bounds,
then the result is underspecified.
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 multiplier, 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
| SFiniteBits Int16 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Int16 -> Int Source # lsb :: SBV Int16 -> SBool Source # msb :: SBV Int16 -> SBool Source # blastBE :: SBV Int16 -> [SBool] Source # blastLE :: SBV Int16 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Int16 Source # fromBitsLE :: [SBool] -> SBV Int16 Source # sTestBit :: SBV Int16 -> Int -> SBool Source # sExtractBits :: SBV Int16 -> [Int] -> [SBool] Source # sPopCount :: SBV Int16 -> SWord8 Source # setBitTo :: SBV Int16 -> Int -> SBool -> SBV Int16 Source # sSetBitTo :: SBV Int16 -> SBV Int16 -> SBool -> SBV Int16 Source # fullAdder :: SBV Int16 -> SBV Int16 -> (SBool, SBV Int16) Source # fullMultiplier :: SBV Int16 -> SBV Int16 -> (SBV Int16, SBV Int16) Source # | |
| SFiniteBits Int32 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Int32 -> Int Source # lsb :: SBV Int32 -> SBool Source # msb :: SBV Int32 -> SBool Source # blastBE :: SBV Int32 -> [SBool] Source # blastLE :: SBV Int32 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Int32 Source # fromBitsLE :: [SBool] -> SBV Int32 Source # sTestBit :: SBV Int32 -> Int -> SBool Source # sExtractBits :: SBV Int32 -> [Int] -> [SBool] Source # sPopCount :: SBV Int32 -> SWord8 Source # setBitTo :: SBV Int32 -> Int -> SBool -> SBV Int32 Source # sSetBitTo :: SBV Int32 -> SBV Int32 -> SBool -> SBV Int32 Source # fullAdder :: SBV Int32 -> SBV Int32 -> (SBool, SBV Int32) Source # fullMultiplier :: SBV Int32 -> SBV Int32 -> (SBV Int32, SBV Int32) Source # | |
| SFiniteBits Int64 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Int64 -> Int Source # lsb :: SBV Int64 -> SBool Source # msb :: SBV Int64 -> SBool Source # blastBE :: SBV Int64 -> [SBool] Source # blastLE :: SBV Int64 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Int64 Source # fromBitsLE :: [SBool] -> SBV Int64 Source # sTestBit :: SBV Int64 -> Int -> SBool Source # sExtractBits :: SBV Int64 -> [Int] -> [SBool] Source # sPopCount :: SBV Int64 -> SWord8 Source # setBitTo :: SBV Int64 -> Int -> SBool -> SBV Int64 Source # sSetBitTo :: SBV Int64 -> SBV Int64 -> SBool -> SBV Int64 Source # fullAdder :: SBV Int64 -> SBV Int64 -> (SBool, SBV Int64) Source # fullMultiplier :: SBV Int64 -> SBV Int64 -> (SBV Int64, SBV Int64) Source # | |
| SFiniteBits Int8 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Int8 -> Int Source # lsb :: SBV Int8 -> SBool Source # msb :: SBV Int8 -> SBool Source # blastBE :: SBV Int8 -> [SBool] Source # blastLE :: SBV Int8 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Int8 Source # fromBitsLE :: [SBool] -> SBV Int8 Source # sTestBit :: SBV Int8 -> Int -> SBool Source # sExtractBits :: SBV Int8 -> [Int] -> [SBool] Source # sPopCount :: SBV Int8 -> SWord8 Source # setBitTo :: SBV Int8 -> Int -> SBool -> SBV Int8 Source # sSetBitTo :: SBV Int8 -> SBV Int8 -> SBool -> SBV Int8 Source # fullAdder :: SBV Int8 -> SBV Int8 -> (SBool, SBV Int8) Source # fullMultiplier :: SBV Int8 -> SBV Int8 -> (SBV Int8, SBV Int8) Source # | |
| SFiniteBits Word16 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Word16 -> Int Source # lsb :: SBV Word16 -> SBool Source # msb :: SBV Word16 -> SBool Source # blastBE :: SBV Word16 -> [SBool] Source # blastLE :: SBV Word16 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Word16 Source # fromBitsLE :: [SBool] -> SBV Word16 Source # sTestBit :: SBV Word16 -> Int -> SBool Source # sExtractBits :: SBV Word16 -> [Int] -> [SBool] Source # sPopCount :: SBV Word16 -> SWord8 Source # setBitTo :: SBV Word16 -> Int -> SBool -> SBV Word16 Source # sSetBitTo :: SBV Word16 -> SBV Word16 -> SBool -> SBV Word16 Source # fullAdder :: SBV Word16 -> SBV Word16 -> (SBool, SBV Word16) Source # fullMultiplier :: SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16) Source # | |
| SFiniteBits Word32 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Word32 -> Int Source # lsb :: SBV Word32 -> SBool Source # msb :: SBV Word32 -> SBool Source # blastBE :: SBV Word32 -> [SBool] Source # blastLE :: SBV Word32 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Word32 Source # fromBitsLE :: [SBool] -> SBV Word32 Source # sTestBit :: SBV Word32 -> Int -> SBool Source # sExtractBits :: SBV Word32 -> [Int] -> [SBool] Source # sPopCount :: SBV Word32 -> SWord8 Source # setBitTo :: SBV Word32 -> Int -> SBool -> SBV Word32 Source # sSetBitTo :: SBV Word32 -> SBV Word32 -> SBool -> SBV Word32 Source # fullAdder :: SBV Word32 -> SBV Word32 -> (SBool, SBV Word32) Source # fullMultiplier :: SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32) Source # | |
| SFiniteBits Word64 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Word64 -> Int Source # lsb :: SBV Word64 -> SBool Source # msb :: SBV Word64 -> SBool Source # blastBE :: SBV Word64 -> [SBool] Source # blastLE :: SBV Word64 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Word64 Source # fromBitsLE :: [SBool] -> SBV Word64 Source # sTestBit :: SBV Word64 -> Int -> SBool Source # sExtractBits :: SBV Word64 -> [Int] -> [SBool] Source # sPopCount :: SBV Word64 -> SWord8 Source # setBitTo :: SBV Word64 -> Int -> SBool -> SBV Word64 Source # sSetBitTo :: SBV Word64 -> SBV Word64 -> SBool -> SBV Word64 Source # fullAdder :: SBV Word64 -> SBV Word64 -> (SBool, SBV Word64) Source # fullMultiplier :: SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64) Source # | |
| SFiniteBits Word8 Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV Word8 -> Int Source # lsb :: SBV Word8 -> SBool Source # msb :: SBV Word8 -> SBool Source # blastBE :: SBV Word8 -> [SBool] Source # blastLE :: SBV Word8 -> [SBool] Source # fromBitsBE :: [SBool] -> SBV Word8 Source # fromBitsLE :: [SBool] -> SBV Word8 Source # sTestBit :: SBV Word8 -> Int -> SBool Source # sExtractBits :: SBV Word8 -> [Int] -> [SBool] Source # sPopCount :: SBV Word8 -> SWord8 Source # setBitTo :: SBV Word8 -> Int -> SBool -> SBV Word8 Source # sSetBitTo :: SBV Word8 -> SBV Word8 -> SBool -> SBV Word8 Source # fullAdder :: SBV Word8 -> SBV Word8 -> (SBool, SBV Word8) Source # fullMultiplier :: SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8) Source # | |
| (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV (IntN n) -> Int Source # lsb :: SBV (IntN n) -> SBool Source # msb :: SBV (IntN n) -> SBool Source # blastBE :: SBV (IntN n) -> [SBool] Source # blastLE :: SBV (IntN n) -> [SBool] Source # fromBitsBE :: [SBool] -> SBV (IntN n) Source # fromBitsLE :: [SBool] -> SBV (IntN n) Source # sTestBit :: SBV (IntN n) -> Int -> SBool Source # sExtractBits :: SBV (IntN n) -> [Int] -> [SBool] Source # sPopCount :: SBV (IntN n) -> SWord8 Source # setBitTo :: SBV (IntN n) -> Int -> SBool -> SBV (IntN n) Source # sSetBitTo :: SBV (IntN n) -> SBV (IntN n) -> SBool -> SBV (IntN n) Source # fullAdder :: SBV (IntN n) -> SBV (IntN n) -> (SBool, SBV (IntN n)) Source # fullMultiplier :: SBV (IntN n) -> SBV (IntN n) -> (SBV (IntN n), SBV (IntN n)) Source # | |
| (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) Source # | |
Defined in Data.SBV.Core.Model Methods sFiniteBitSize :: SBV (WordN n) -> Int Source # lsb :: SBV (WordN n) -> SBool Source # msb :: SBV (WordN n) -> SBool Source # blastBE :: SBV (WordN n) -> [SBool] Source # blastLE :: SBV (WordN n) -> [SBool] Source # fromBitsBE :: [SBool] -> SBV (WordN n) Source # fromBitsLE :: [SBool] -> SBV (WordN n) Source # sTestBit :: SBV (WordN n) -> Int -> SBool Source # sExtractBits :: SBV (WordN n) -> [Int] -> [SBool] Source # sPopCount :: SBV (WordN n) -> SWord8 Source # setBitTo :: SBV (WordN n) -> Int -> SBool -> SBV (WordN n) Source # sSetBitTo :: SBV (WordN n) -> SBV (WordN n) -> SBool -> SBV (WordN n) Source # fullAdder :: SBV (WordN n) -> SBV (WordN n) -> (SBool, SBV (WordN n)) Source # fullMultiplier :: SBV (WordN n) -> SBV (WordN n) -> (SBV (WordN n), SBV (WordN n)) Source # | |
Splitting, joining, and extending bit-vectors
Arguments
| :: forall (i :: Nat) (j :: Nat) (n :: Nat) bv proxy. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, BVIsNonZero ((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.
Arguments
| :: forall (n :: Nat) bv (m :: Nat). (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero 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 bit-vectors.
Arguments
| :: forall (n :: Nat) (m :: Nat) bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), BVIsNonZero (m - n)) | |
| => SBV (bv n) | Input, of size |
| -> SBV (bv m) | Output, of size |
Zero extend a bit-vector.
Arguments
| :: forall (n :: Nat) (m :: Nat) bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), BVIsNonZero (m - n)) | |
| => SBV (bv n) | Input, of size |
| -> SBV (bv m) | Output, of size |
Sign extend a bit-vector.
Arguments
| :: forall (i :: Nat) (n :: Nat) (m :: Natural) bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, BVIsNonZero (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.
Arguments
| :: forall (i :: Nat) (n :: Nat) bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero 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.
Exponentiation
(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b infixr 8 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
| IEEEFloating Double Source # | SDouble instance |
Defined in Data.SBV.Core.Floating Methods fpAbs :: SBV Double -> SBV Double Source # fpNeg :: SBV Double -> SBV Double Source # fpAdd :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source # fpSub :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source # fpMul :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source # fpDiv :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source # fpFMA :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double -> SBV Double Source # fpSqrt :: SRoundingMode -> SBV Double -> SBV Double Source # fpRem :: SBV Double -> SBV Double -> SBV Double Source # fpRoundToIntegral :: SRoundingMode -> SBV Double -> SBV Double Source # fpMin :: SBV Double -> SBV Double -> SBV Double Source # fpMax :: SBV Double -> SBV Double -> SBV Double Source # fpIsEqualObject :: SBV Double -> SBV Double -> SBool Source # fpIsNormal :: SBV Double -> SBool Source # fpIsSubnormal :: SBV Double -> SBool Source # fpIsZero :: SBV Double -> SBool Source # fpIsInfinite :: SBV Double -> SBool Source # fpIsNaN :: SBV Double -> SBool Source # fpIsNegative :: SBV Double -> SBool Source # fpIsPositive :: SBV Double -> SBool Source # fpIsNegativeZero :: SBV Double -> SBool Source # | |
| IEEEFloating Float Source # | SFloat instance |
Defined in Data.SBV.Core.Floating Methods fpAbs :: SBV Float -> SBV Float Source # fpNeg :: SBV Float -> SBV Float Source # fpAdd :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source # fpSub :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source # fpMul :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source # fpDiv :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source # fpFMA :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float -> SBV Float Source # fpSqrt :: SRoundingMode -> SBV Float -> SBV Float Source # fpRem :: SBV Float -> SBV Float -> SBV Float Source # fpRoundToIntegral :: SRoundingMode -> SBV Float -> SBV Float Source # fpMin :: SBV Float -> SBV Float -> SBV Float Source # fpMax :: SBV Float -> SBV Float -> SBV Float Source # fpIsEqualObject :: SBV Float -> SBV Float -> SBool Source # fpIsNormal :: SBV Float -> SBool Source # fpIsSubnormal :: SBV Float -> SBool Source # fpIsZero :: SBV Float -> SBool Source # fpIsInfinite :: SBV Float -> SBool Source # fpIsNaN :: SBV Float -> SBool Source # fpIsNegative :: SBV Float -> SBool Source # fpIsPositive :: SBV Float -> SBool Source # fpIsNegativeZero :: SBV Float -> SBool Source # | |
| ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) Source # | |
Defined in Data.SBV.Core.Floating Methods fpAbs :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpNeg :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpAdd :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpSub :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpMul :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpDiv :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpFMA :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpSqrt :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpRem :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpRoundToIntegral :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpMin :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpMax :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) Source # fpIsEqualObject :: SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool Source # fpIsNormal :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsSubnormal :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsZero :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsInfinite :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsNaN :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsNegative :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsPositive :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsNegativeZero :: SBV (FloatingPoint eb sb) -> SBool Source # fpIsPositiveZero :: SBV (FloatingPoint eb sb) -> SBool Source # | |
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
| Arbitrary RoundingMode Source # | Arbitrary instance for |
Defined in Data.SBV.Utils.Numeric | |
| Bounded RoundingMode Source # | |
Defined in Data.SBV.Utils.Numeric | |
| Enum RoundingMode Source # | |
Defined in Data.SBV.Utils.Numeric Methods succ :: RoundingMode -> RoundingMode # pred :: RoundingMode -> RoundingMode # toEnum :: Int -> RoundingMode # fromEnum :: RoundingMode -> Int # enumFrom :: RoundingMode -> [RoundingMode] # enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] # enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] # enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] # | |
| Show RoundingMode Source # | |
Defined in Data.SBV.Utils.Numeric Methods showsPrec :: Int -> RoundingMode -> ShowS # show :: RoundingMode -> String # showList :: [RoundingMode] -> ShowS # | |
| SymVal RoundingMode Source # | |
Defined in Data.SBV.Core.Model Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV RoundingMode) Source # mkSymValInit :: State -> SBV RoundingMode -> IO () Source # literal :: RoundingMode -> SBV RoundingMode Source # fromCV :: CV -> RoundingMode Source # isConcretely :: SBV RoundingMode -> (RoundingMode -> Bool) -> Bool Source # minMaxBound :: Maybe (RoundingMode, RoundingMode) Source # free :: MonadSymbolic m => String -> m (SBV RoundingMode) Source # free_ :: MonadSymbolic m => m (SBV RoundingMode) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV RoundingMode] Source # symbolic :: MonadSymbolic m => String -> m (SBV RoundingMode) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV RoundingMode] Source # unliteral :: SBV RoundingMode -> Maybe RoundingMode Source # unlitCV :: SBV RoundingMode -> Maybe (Kind, CVal) Source # isConcrete :: SBV RoundingMode -> Bool Source # isSymbolic :: SBV RoundingMode -> Bool Source # | |
| HasKind RoundingMode Source # | |
Defined in Data.SBV.Core.Kind Methods kindOf :: RoundingMode -> Kind Source # hasSign :: RoundingMode -> Bool Source # intSizeOf :: RoundingMode -> Int Source # isBoolean :: RoundingMode -> Bool Source # isBounded :: RoundingMode -> Bool Source # isReal :: RoundingMode -> Bool Source # isFloat :: RoundingMode -> Bool Source # isDouble :: RoundingMode -> Bool Source # isRational :: RoundingMode -> Bool Source # isFP :: RoundingMode -> Bool Source # isUnbounded :: RoundingMode -> Bool Source # isADT :: RoundingMode -> Bool Source # isChar :: RoundingMode -> Bool Source # isString :: RoundingMode -> Bool Source # isList :: RoundingMode -> Bool Source # isSet :: RoundingMode -> Bool Source # isTuple :: RoundingMode -> Bool Source # isArray :: RoundingMode -> Bool Source # isRoundingMode :: RoundingMode -> Bool Source # isUninterpreted :: RoundingMode -> Bool Source # showType :: RoundingMode -> String Source # | |
| SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices) |
Defined in Data.SBV.SMT.SMT | |
type SRoundingMode = SBV RoundingMode Source #
The symbolic variant of RoundingMode
sNaN :: (Floating a, SymVal a) => SBV a Source #
Symbolic variant of Not-A-Number. This value will inhabit
SFloat, SDouble and SFloatingPoint. types.
sInfinity :: (Floating a, SymVal a) => SBV a Source #
Symbolic variant of infinity. This value will inhabit both
SFloat, SDouble and SFloatingPoint. types.
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
Arguments
| :: Mergeable r | |
| => r | What to return in the |
| -> r | What to return in the |
| -> r | What to return in the |
| -> r | What to return in the |
| -> r | What to return in the |
| -> SRoundingMode | |
| -> r |
Case analyzer for the type RoundingMode.
Conversion to/from floats
class SymVal a => IEEEFloatConvertible a where Source #
Conversion to and from floats
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.
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.
fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a Source #
Convert from an arbitrary floating point.
toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb Source #
Convert to an arbitrary floating point.
default toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). (Integral a, ValidFloat eb sb) => SRoundingMode -> SBV a -> SFloatingPoint eb sb Source #
Instances
| IEEEFloatConvertible Int16 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int16 Source # toSFloat :: SRoundingMode -> SBV Int16 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int16 Source # toSDouble :: SRoundingMode -> SBV Int16 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Int16 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Int16 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Int32 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int32 Source # toSFloat :: SRoundingMode -> SBV Int32 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int32 Source # toSDouble :: SRoundingMode -> SBV Int32 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Int32 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Int32 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Int64 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int64 Source # toSFloat :: SRoundingMode -> SBV Int64 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int64 Source # toSDouble :: SRoundingMode -> SBV Int64 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Int64 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Int64 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Int8 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int8 Source # toSFloat :: SRoundingMode -> SBV Int8 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int8 Source # toSDouble :: SRoundingMode -> SBV Int8 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Int8 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Int8 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Word16 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word16 Source # toSFloat :: SRoundingMode -> SBV Word16 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word16 Source # toSDouble :: SRoundingMode -> SBV Word16 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Word16 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Word16 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Word32 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word32 Source # toSFloat :: SRoundingMode -> SBV Word32 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word32 Source # toSDouble :: SRoundingMode -> SBV Word32 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Word32 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Word32 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Word64 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word64 Source # toSFloat :: SRoundingMode -> SBV Word64 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word64 Source # toSDouble :: SRoundingMode -> SBV Word64 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Word64 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Word64 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Word8 Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word8 Source # toSFloat :: SRoundingMode -> SBV Word8 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word8 Source # toSDouble :: SRoundingMode -> SBV Word8 -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Word8 Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Word8 -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible AlgReal Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal Source # toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal Source # toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV AlgReal Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV AlgReal -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Integer Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Integer Source # toSFloat :: SRoundingMode -> SBV Integer -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Integer Source # toSDouble :: SRoundingMode -> SBV Integer -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Integer Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Integer -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Double Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Double Source # toSFloat :: SRoundingMode -> SBV Double -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Double Source # toSDouble :: SRoundingMode -> SBV Double -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Double Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Double -> SFloatingPoint eb sb Source # | |
| IEEEFloatConvertible Float Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Float Source # toSFloat :: SRoundingMode -> SBV Float -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Float Source # toSDouble :: SRoundingMode -> SBV Float -> SDouble Source # fromSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV Float Source # toSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). ValidFloat eb sb => SRoundingMode -> SBV Float -> SFloatingPoint eb sb Source # | |
| ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) Source # | |
Defined in Data.SBV.Core.Floating Methods fromSFloat :: SRoundingMode -> SFloat -> SBV (FloatingPoint eb sb) Source # toSFloat :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV (FloatingPoint eb sb) Source # toSDouble :: SRoundingMode -> SBV (FloatingPoint eb sb) -> SDouble Source # fromSFloatingPoint :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFloat eb0 sb0 => SRoundingMode -> SFloatingPoint eb0 sb0 -> SBV (FloatingPoint eb sb) Source # toSFloatingPoint :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFloat eb0 sb0 => SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb0 sb0 Source # | |
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
sFloatingPointAsSWord :: forall (eb :: Nat) (sb :: Nat). (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb) Source #
Convert a float to the word containing the corresponding bit pattern
sWordAsSFloatingPoint :: forall (eb :: Natural) (sb :: Natural). (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb Source #
Convert a word to an arbitrary float, by reinterpreting the bits of the word as the corresponding bits of the float.
Extracting bit patterns from floats
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.
blastSFloatingPoint :: forall (eb :: Nat) (sb :: Nat). (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of an arbitrary precision float. The output will have
eb bits in the second argument for exponent, and sb-1 bits in the third for mantissa.
Symbolic types
class SMTDefinable a where Source #
SMT definable constants and functions, which can also be uninterpreted. This class captures functions that we can generate standalone-code for in the SMT solver. Note that we also allow uninterpreted constants and functions too. 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: sbvDefineValue. 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
smtFunctionDef :: String -> Measure a -> a -> a Source #
Generate the code for this value as an SMTLib function, instead of the usual unrolling semantics. This is useful for generating sub-functions in generated SMTLib problem, or handling recursive (and mutually-recursive) definitions that wouldn't terminate in an unrolling symbolic simulation context.
IMPORTANT NOTE The string argument names this function. SBV identifies
the function by this name: if you use this function twice (or use it recursively),
it will simply assume this name uniquely identifies the function being defined.
If two calls to smtFunction (or its variants) use the same name but different
bodies, SBV will raise an error at runtime.
Furthermore, if the call to smtFunction happens in the scope of a parameter, you
must make sure the string is chosen to keep it unique per parameter value. For instance,
if you have:
bar :: SInteger -> SInteger -> SInteger bar k = smtFunction "bar" (x -> x+k) -- Note the capture of k!
and you call bar 2 and bar 3, SBV will detect that the two bodies differ and
raise an error. You should use a concrete argument to make the name unique:
bar :: String -> SInteger -> SInteger -> SInteger
bar tag k = smtFunction ("bar_" ++ tag) (x -> x+k) -- Tag should make the name unique!
Then, make sure you use bar "two" 2 and bar "three" 3 etc. to preserve the invariant.
Additionally, the function argument must not capture any non-constant variables in the context.
You can also define higher-order functions, see smtHOFunction for that purpose.
registerFunction :: a -> Symbolic () Source #
Register a function. This function is typically not needed as SBV will register functions used automatically upon first use. However, there are scenarios (in particular query contexts) where the definition isn't used before query-mode starts, and SBV (for historical reasons) requires functions to be known before query-mode starts executing. In such cases, use this function to register them with the system.
uninterpret :: String -> a Source #
Uninterpret a value, i.e., add this value as a completely undefined value/function that the solver is free to instantiate to satisfy other constraints.
Known issues
Usually using an uninterpret function will register itself to the solver, but sometimes the laziness of the evaluation might render this unreliable.
For example, when working with quantifiers and uninterpreted functions with the following code:
runSMTWith z3 $ do
let f = uninterpret "f" :: SInteger -> SInteger
query $ do
constrain $ \(Forall (b :: SInteger)) -> f b .== f b
checkSatThe solver will complain about the unknown constant f (Int).
A workaround of this is to explicit register them with registerUISMTFunction:
runSMTWith z3 $ do
let f = uninterpret "f" :: SInteger -> SInteger
registerUISMTFunction f
query $ do
constrain $ \(Forall (b :: SInteger)) -> f b .== f b
checkSatSee https://github.com/LeventErkok/sbv/issues/711 for more info.
uninterpretWithArgs :: String -> [String] -> a Source #
Uninterpret a value, with named arguments in case of functions. SBV will use these names when it shows the values for the arguments. If the given names are more than needed we ignore the excess. If not enough, we add from a stock set of variables.
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.
sbvDefineValue :: UIName -> Maybe [String] -> UIKind a -> a Source #
More generalized form of uninterpretation that wraps sbvDefineValueFun;
this function should not be needed by end-user-code
sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> a) -> SBVs as -> a Source #
The most generalized form of uninterpretation, that generates an
uninterpreted function over a sequence of SBVs values; this function is
internal-only, and should not be needed by end-user-code
A synonym for uninterpret. Allows us to create variables without
having to call free explicitly, i.e., without being in the symbolic monad.
symWithKind :: String -> a Source #
Like sym, but appends the type's kind to the name, ensuring uniqueness across
different type instantiations of the same polymorphic definition. Used internally by sCase.
sbv2smt :: ExtractIO m => a -> m String Source #
Render an uninterpreted value as an SMTLib definition
sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> a) -> m String Source #
Render an uninterpreted value function as an SMTLib definition
mkADTConstructor :: String -> a Source #
Make this name a constructor, coming from an ADT. Only used internally
mkADTTester :: String -> a Source #
mkADTAccessor :: String -> a Source #
Instances
| SymVal a => SMTDefinable (SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure (SBV a) -> SBV a -> SBV a Source # registerFunction :: SBV a -> Symbolic () Source # uninterpret :: String -> SBV a Source # uninterpretWithArgs :: String -> [String] -> SBV a Source # cgUninterpret :: String -> [String] -> SBV a -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind (SBV a) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> SBV a) -> SBVs as -> SBV a Source # sym :: String -> SBV a Source # symWithKind :: String -> SBV a Source # sbv2smt :: ExtractIO m => SBV a -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> SBV a) -> m String Source # mkADTConstructor :: String -> SBV a Source # mkADTTester :: String -> SBV a Source # mkADTAccessor :: String -> SBV a Source # | |
| (SymVal a, SMTDefinable b) => SMTDefinable (SBV a -> b) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure (SBV a -> b) -> (SBV a -> b) -> SBV a -> b Source # registerFunction :: (SBV a -> b) -> Symbolic () Source # uninterpret :: String -> SBV a -> b Source # uninterpretWithArgs :: String -> [String] -> SBV a -> b Source # cgUninterpret :: String -> [String] -> (SBV a -> b) -> SBV a -> b Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind (SBV a -> b) -> SBV a -> b Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> SBV a -> b) -> SBVs as -> SBV a -> b Source # sym :: String -> SBV a -> b Source # symWithKind :: String -> SBV a -> b Source # sbv2smt :: ExtractIO m => (SBV a -> b) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> SBV a -> b) -> m String Source # mkADTConstructor :: String -> SBV a -> b Source # mkADTTester :: String -> SBV a -> b Source # mkADTAccessor :: String -> SBV a -> b Source # | |
| (SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal m, SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m0 => ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m0 String Source # sbvFun2smt :: forall (as :: RList Type) m0. (SymVals as, ExtractIO m0) => (SBVs as -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m0 String Source # mkADTConstructor :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV c, SBV b) -> SBV a) -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV c, SBV b) -> SBV a Source # | |
| (SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV d, SBV c, SBV b) -> SBV a) -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
| (SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # | |
Defined in Data.SBV.Core.Model Methods smtFunctionDef :: String -> Measure ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # registerFunction :: ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> Symbolic () Source # uninterpret :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # uninterpretWithArgs :: String -> [String] -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValue :: UIName -> Maybe [String] -> UIKind ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvDefineValueFun :: forall (as :: RList Type). UIName -> Maybe [String] -> SymValInsts as -> UIKind (SBVs as -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> SBVs as -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sym :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # symWithKind :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbv2smt :: ExtractIO m => ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # sbvFun2smt :: forall (as :: RList Type) m. (SymVals as, ExtractIO m) => (SBVs as -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> m String Source # mkADTConstructor :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTTester :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # mkADTAccessor :: String -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # | |
smtFunction :: (SMTDefinable a, Typeable a, Lambda Symbolic a) => String -> a -> a Source #
Define an SMT function. If the function is recursive, SBV will automatically try to
prove termination by guessing a measure based on argument types. If the guess fails,
use smtFunctionWithMeasure to provide an explicit measure.
smtFunctionWithMeasure :: (SMTDefinable f, Typeable f, Lambda Symbolic f, Zero r, OrdSymbolic (SBV r), SymVal r, ApplyMeasure f r) => String -> (MeasureOf f r, [MeasureHelper]) -> f -> f Source #
Define an SMT function with an explicit termination measure. Use this when smtFunction
cannot automatically determine a suitable measure. The measure function takes the same
arguments as the original function but returns a value that must be non-negative and
strictly decrease at each recursive call.
The pair (measure, helpers) provides the measure function and a list of auxiliary
MeasureHelper properties needed to verify the measure. Each helper is first proven
(by running its TP proof), then asserted as an axiom in the measure verification session.
Use measureLemma to create helpers from TP proofs. Pass [] when no helpers are needed.
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 ConstraintSet = Symbolic () Source #
A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as the collection of constraints that will be used for sat/optimize calls.
class ExtractIO m => ProvableM (m :: Type -> Type) a where Source #
A type a is provable if we can turn it into a predicate, i.e., it has to return a boolean.
This class captures essentially prove calls.
Minimal complete definition
Methods
proofArgReduce :: a -> SymbolicT m SBool Source #
Reduce an arg, for proof purposes.
prove :: a -> m ThmResult Source #
Generalization of prove
proveWith :: SMTConfig -> a -> m ThmResult Source #
Generalization of proveWith
dprove :: a -> m ThmResult Source #
Generalization of dprove
dproveWith :: SMTConfig -> a -> m ThmResult Source #
Generalization of dproveWith
isVacuousProof :: a -> m Bool Source #
Generalization of isVacuousProof
isVacuousProofWith :: SMTConfig -> a -> m Bool Source #
Generalization of isVacuousProofWith
isTheorem :: a -> m Bool Source #
Generalization of isTheorem
isTheoremWith :: SMTConfig -> a -> m Bool Source #
Generalization of isTheoremWith
Instances
| ExtractIO m => ProvableM m SBool Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: SBool -> SymbolicT m SBool Source # prove :: SBool -> m ThmResult Source # proveWith :: SMTConfig -> SBool -> m ThmResult Source # dprove :: SBool -> m ThmResult Source # dproveWith :: SMTConfig -> SBool -> m ThmResult Source # isVacuousProof :: SBool -> m Bool Source # isVacuousProofWith :: SMTConfig -> SBool -> m Bool Source # | |
| ExtractIO m => ProvableM m (SymbolicT m SBool) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: SymbolicT m SBool -> SymbolicT m SBool Source # prove :: SymbolicT m SBool -> m ThmResult Source # proveWith :: SMTConfig -> SymbolicT m SBool -> m ThmResult Source # dprove :: SymbolicT m SBool -> m ThmResult Source # dproveWith :: SMTConfig -> SymbolicT m SBool -> m ThmResult Source # isVacuousProof :: SymbolicT m SBool -> m Bool Source # isVacuousProofWith :: SMTConfig -> SymbolicT m SBool -> m Bool Source # isTheorem :: SymbolicT m SBool -> m Bool Source # isTheoremWith :: SMTConfig -> SymbolicT m SBool -> m Bool Source # | |
| (ExtractIO m, ProvableM m a) => ProvableM m (SymbolicT m a) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: SymbolicT m a -> SymbolicT m SBool Source # prove :: SymbolicT m a -> m ThmResult Source # proveWith :: SMTConfig -> SymbolicT m a -> m ThmResult Source # dprove :: SymbolicT m a -> m ThmResult Source # dproveWith :: SMTConfig -> SymbolicT m a -> m ThmResult Source # isVacuousProof :: SymbolicT m a -> m Bool Source # isVacuousProofWith :: SMTConfig -> SymbolicT m a -> m Bool Source # isTheorem :: SymbolicT m a -> m Bool Source # isTheoremWith :: SMTConfig -> SymbolicT m a -> m Bool Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Exists nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool Source # prove :: (Exists nm a -> r) -> m ThmResult Source # proveWith :: SMTConfig -> (Exists nm a -> r) -> m ThmResult Source # dprove :: (Exists nm a -> r) -> m ThmResult Source # dproveWith :: SMTConfig -> (Exists nm a -> r) -> m ThmResult Source # isVacuousProof :: (Exists nm a -> r) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (Exists nm a -> r) -> m Bool Source # isTheorem :: (Exists nm a -> r) -> m Bool Source # isTheoremWith :: SMTConfig -> (Exists nm a -> r) -> m Bool Source # | |
| (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ExistsN n nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool Source # prove :: (ExistsN n nm a -> r) -> m ThmResult Source # proveWith :: SMTConfig -> (ExistsN n nm a -> r) -> m ThmResult Source # dprove :: (ExistsN n nm a -> r) -> m ThmResult Source # dproveWith :: SMTConfig -> (ExistsN n nm a -> r) -> m ThmResult Source # isVacuousProof :: (ExistsN n nm a -> r) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (ExistsN n nm a -> r) -> m Bool Source # isTheorem :: (ExistsN n nm a -> r) -> m Bool Source # isTheoremWith :: SMTConfig -> (ExistsN n nm a -> r) -> m Bool Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r, EqSymbolic (SBV a)) => ProvableM m (ExistsUnique nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool Source # prove :: (ExistsUnique nm a -> r) -> m ThmResult Source # proveWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m ThmResult Source # dprove :: (ExistsUnique nm a -> r) -> m ThmResult Source # dproveWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m ThmResult Source # isVacuousProof :: (ExistsUnique nm a -> r) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m Bool Source # isTheorem :: (ExistsUnique nm a -> r) -> m Bool Source # isTheoremWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m Bool Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Forall nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool Source # prove :: (Forall nm a -> r) -> m ThmResult Source # proveWith :: SMTConfig -> (Forall nm a -> r) -> m ThmResult Source # dprove :: (Forall nm a -> r) -> m ThmResult Source # dproveWith :: SMTConfig -> (Forall nm a -> r) -> m ThmResult Source # isVacuousProof :: (Forall nm a -> r) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (Forall nm a -> r) -> m Bool Source # isTheorem :: (Forall nm a -> r) -> m Bool Source # isTheoremWith :: SMTConfig -> (Forall nm a -> r) -> m Bool Source # | |
| (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ForallN n nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool Source # prove :: (ForallN n nm a -> r) -> m ThmResult Source # proveWith :: SMTConfig -> (ForallN n nm a -> r) -> m ThmResult Source # dprove :: (ForallN n nm a -> r) -> m ThmResult Source # dproveWith :: SMTConfig -> (ForallN n nm a -> r) -> m ThmResult Source # isVacuousProof :: (ForallN n nm a -> r) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (ForallN n nm a -> r) -> m Bool Source # isTheorem :: (ForallN n nm a -> r) -> m Bool Source # isTheoremWith :: SMTConfig -> (ForallN n nm a -> r) -> m Bool Source # | |
| (SymVal a, ProvableM m p) => ProvableM m (SBV a -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (SBV a -> p) -> SymbolicT m SBool Source # prove :: (SBV a -> p) -> m ThmResult Source # proveWith :: SMTConfig -> (SBV a -> p) -> m ThmResult Source # dprove :: (SBV a -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> (SBV a -> p) -> m ThmResult Source # isVacuousProof :: (SBV a -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (SBV a -> p) -> m Bool Source # isTheorem :: (SBV a -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> (SBV a -> p) -> m Bool Source # | |
| (SymVals as, ProvableM m p) => ProvableM m (SBVs as -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: (SBVs as -> p) -> SymbolicT m SBool Source # prove :: (SBVs as -> p) -> m ThmResult Source # proveWith :: SMTConfig -> (SBVs as -> p) -> m ThmResult Source # dprove :: (SBVs as -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> (SBVs as -> p) -> m ThmResult Source # isVacuousProof :: (SBVs as -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> (SBVs as -> p) -> m Bool Source # isTheorem :: (SBVs as -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> (SBVs as -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, ProvableM m p) => ProvableM m ((SBV a, SBV b) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> SymbolicT m SBool Source # prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m ThmResult Source # proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m ThmResult Source # dprove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m ThmResult Source # dproveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m ThmResult Source # isVacuousProof :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # isVacuousProofWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # | |
class ExtractIO m => SatisfiableM (m :: Type -> Type) a where Source #
A type a is satisfiable if it has constraints, potentially returning a boolean. This class
captures essentially sat and optimize calls.
Minimal complete definition
Methods
satArgReduce :: a -> SymbolicT m SBool Source #
Reduce an arg, for sat purposes.
sat :: a -> m SatResult Source #
Generalization of sat
satWith :: SMTConfig -> a -> m SatResult Source #
Generalization of satWith
dsat :: a -> m SatResult Source #
Generalization of sat
dsatWith :: 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
isSatisfiable :: a -> m Bool Source #
Generalization of isSatisfiable
isSatisfiableWith :: SMTConfig -> a -> m Bool Source #
Generalization of isSatisfiableWith
optimize :: OptimizeStyle -> a -> m OptimizeResult Source #
Generalization of optimize
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult Source #
Generalization of optimizeWith
Instances
| ExtractIO m => SatisfiableM m SBool Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: SBool -> SymbolicT m SBool Source # sat :: SBool -> m SatResult Source # satWith :: SMTConfig -> SBool -> m SatResult Source # dsat :: SBool -> m SatResult Source # dsatWith :: SMTConfig -> SBool -> m SatResult Source # allSat :: SBool -> m AllSatResult Source # allSatWith :: SMTConfig -> SBool -> m AllSatResult Source # isSatisfiable :: SBool -> m Bool Source # isSatisfiableWith :: SMTConfig -> SBool -> m Bool Source # optimize :: OptimizeStyle -> SBool -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> SBool -> m OptimizeResult Source # | |
| ExtractIO m => SatisfiableM m (SymbolicT m SBool) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: SymbolicT m SBool -> SymbolicT m SBool Source # sat :: SymbolicT m SBool -> m SatResult Source # satWith :: SMTConfig -> SymbolicT m SBool -> m SatResult Source # dsat :: SymbolicT m SBool -> m SatResult Source # dsatWith :: SMTConfig -> SymbolicT m SBool -> m SatResult Source # allSat :: SymbolicT m SBool -> m AllSatResult Source # allSatWith :: SMTConfig -> SymbolicT m SBool -> m AllSatResult Source # isSatisfiable :: SymbolicT m SBool -> m Bool Source # isSatisfiableWith :: SMTConfig -> SymbolicT m SBool -> m Bool Source # optimize :: OptimizeStyle -> SymbolicT m SBool -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> SymbolicT m SBool -> m OptimizeResult Source # | |
| ExtractIO m => SatisfiableM m (SymbolicT m ()) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: SymbolicT m () -> SymbolicT m SBool Source # sat :: SymbolicT m () -> m SatResult Source # satWith :: SMTConfig -> SymbolicT m () -> m SatResult Source # dsat :: SymbolicT m () -> m SatResult Source # dsatWith :: SMTConfig -> SymbolicT m () -> m SatResult Source # allSat :: SymbolicT m () -> m AllSatResult Source # allSatWith :: SMTConfig -> SymbolicT m () -> m AllSatResult Source # isSatisfiable :: SymbolicT m () -> m Bool Source # isSatisfiableWith :: SMTConfig -> SymbolicT m () -> m Bool Source # optimize :: OptimizeStyle -> SymbolicT m () -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> SymbolicT m () -> m OptimizeResult Source # | |
| (ExtractIO m, SatisfiableM m a) => SatisfiableM m (SymbolicT m a) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: SymbolicT m a -> SymbolicT m SBool Source # sat :: SymbolicT m a -> m SatResult Source # satWith :: SMTConfig -> SymbolicT m a -> m SatResult Source # dsat :: SymbolicT m a -> m SatResult Source # dsatWith :: SMTConfig -> SymbolicT m a -> m SatResult Source # allSat :: SymbolicT m a -> m AllSatResult Source # allSatWith :: SMTConfig -> SymbolicT m a -> m AllSatResult Source # isSatisfiable :: SymbolicT m a -> m Bool Source # isSatisfiableWith :: SMTConfig -> SymbolicT m a -> m Bool Source # optimize :: OptimizeStyle -> SymbolicT m a -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> SymbolicT m a -> m OptimizeResult Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Exists nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool Source # sat :: (Exists nm a -> r) -> m SatResult Source # satWith :: SMTConfig -> (Exists nm a -> r) -> m SatResult Source # dsat :: (Exists nm a -> r) -> m SatResult Source # dsatWith :: SMTConfig -> (Exists nm a -> r) -> m SatResult Source # allSat :: (Exists nm a -> r) -> m AllSatResult Source # allSatWith :: SMTConfig -> (Exists nm a -> r) -> m AllSatResult Source # isSatisfiable :: (Exists nm a -> r) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (Exists nm a -> r) -> m Bool Source # optimize :: OptimizeStyle -> (Exists nm a -> r) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (Exists nm a -> r) -> m OptimizeResult Source # | |
| (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ExistsN n nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool Source # sat :: (ExistsN n nm a -> r) -> m SatResult Source # satWith :: SMTConfig -> (ExistsN n nm a -> r) -> m SatResult Source # dsat :: (ExistsN n nm a -> r) -> m SatResult Source # dsatWith :: SMTConfig -> (ExistsN n nm a -> r) -> m SatResult Source # allSat :: (ExistsN n nm a -> r) -> m AllSatResult Source # allSatWith :: SMTConfig -> (ExistsN n nm a -> r) -> m AllSatResult Source # isSatisfiable :: (ExistsN n nm a -> r) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (ExistsN n nm a -> r) -> m Bool Source # optimize :: OptimizeStyle -> (ExistsN n nm a -> r) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (ExistsN n nm a -> r) -> m OptimizeResult Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r, EqSymbolic (SBV a)) => SatisfiableM m (ExistsUnique nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool Source # sat :: (ExistsUnique nm a -> r) -> m SatResult Source # satWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m SatResult Source # dsat :: (ExistsUnique nm a -> r) -> m SatResult Source # dsatWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m SatResult Source # allSat :: (ExistsUnique nm a -> r) -> m AllSatResult Source # allSatWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m AllSatResult Source # isSatisfiable :: (ExistsUnique nm a -> r) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (ExistsUnique nm a -> r) -> m Bool Source # optimize :: OptimizeStyle -> (ExistsUnique nm a -> r) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (ExistsUnique nm a -> r) -> m OptimizeResult Source # | |
| (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Forall nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool Source # sat :: (Forall nm a -> r) -> m SatResult Source # satWith :: SMTConfig -> (Forall nm a -> r) -> m SatResult Source # dsat :: (Forall nm a -> r) -> m SatResult Source # dsatWith :: SMTConfig -> (Forall nm a -> r) -> m SatResult Source # allSat :: (Forall nm a -> r) -> m AllSatResult Source # allSatWith :: SMTConfig -> (Forall nm a -> r) -> m AllSatResult Source # isSatisfiable :: (Forall nm a -> r) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (Forall nm a -> r) -> m Bool Source # optimize :: OptimizeStyle -> (Forall nm a -> r) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (Forall nm a -> r) -> m OptimizeResult Source # | |
| (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ForallN n nm a -> r) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool Source # sat :: (ForallN n nm a -> r) -> m SatResult Source # satWith :: SMTConfig -> (ForallN n nm a -> r) -> m SatResult Source # dsat :: (ForallN n nm a -> r) -> m SatResult Source # dsatWith :: SMTConfig -> (ForallN n nm a -> r) -> m SatResult Source # allSat :: (ForallN n nm a -> r) -> m AllSatResult Source # allSatWith :: SMTConfig -> (ForallN n nm a -> r) -> m AllSatResult Source # isSatisfiable :: (ForallN n nm a -> r) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (ForallN n nm a -> r) -> m Bool Source # optimize :: OptimizeStyle -> (ForallN n nm a -> r) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (ForallN n nm a -> r) -> m OptimizeResult Source # | |
| (SymVal a, SatisfiableM m p) => SatisfiableM m (SBV a -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (SBV a -> p) -> SymbolicT m SBool Source # sat :: (SBV a -> p) -> m SatResult Source # satWith :: SMTConfig -> (SBV a -> p) -> m SatResult Source # dsat :: (SBV a -> p) -> m SatResult Source # dsatWith :: SMTConfig -> (SBV a -> p) -> m SatResult Source # allSat :: (SBV a -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> (SBV a -> p) -> m AllSatResult Source # isSatisfiable :: (SBV a -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (SBV a -> p) -> m Bool Source # optimize :: OptimizeStyle -> (SBV a -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (SBV a -> p) -> m OptimizeResult Source # | |
| (SymVals as, SatisfiableM m p) => SatisfiableM m (SBVs as -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: (SBVs as -> p) -> SymbolicT m SBool Source # sat :: (SBVs as -> p) -> m SatResult Source # satWith :: SMTConfig -> (SBVs as -> p) -> m SatResult Source # dsat :: (SBVs as -> p) -> m SatResult Source # dsatWith :: SMTConfig -> (SBVs as -> p) -> m SatResult Source # allSat :: (SBVs as -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> (SBVs as -> p) -> m AllSatResult Source # isSatisfiable :: (SBVs as -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> (SBVs as -> p) -> m Bool Source # optimize :: OptimizeStyle -> (SBVs as -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> (SBVs as -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) -> m OptimizeResult Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) Source # | |
Defined in Data.SBV.Provers.Prover Methods satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> SymbolicT m SBool Source # sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m SatResult Source # satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m SatResult Source # dsat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m SatResult Source # dsatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m SatResult Source # allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m AllSatResult Source # allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m AllSatResult Source # isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m Bool Source # optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m OptimizeResult Source # optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) -> m OptimizeResult Source # | |
type Satisfiable = SatisfiableM IO Source #
Satisfiable is specialization of SatisfiableM to the IO monad. Unless you are using
transformers explicitly, this is the type you should prefer.
generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String Source #
Create an SMT-Lib2 benchmark, for a SAT query.
generateSMTBenchmarkProof :: ProvableM m a => a -> m String Source #
Create an SMT-Lib2 benchmark, for a Proof query.
Constraints
General constraints
constrain :: (SolverContext m, QuantifiedBool a) => a -> m () Source #
Add a constraint, any satisfying instance must satisfy this condition.
softConstrain :: (SolverContext m, QuantifiedBool a) => a -> 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, QuantifiedBool a) => String -> a -> m () Source #
Add a named constraint. The name is used in unsat-core extraction.
constrainWithAttribute :: (SolverContext m, QuantifiedBool a) => [(String, String)] -> a -> 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 :: Type -> Type) a where Source #
Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficiently 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.
Minimal complete definition
Methods
sName :: 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
| ExtractIO m => SExecutable m () Source # | |
Defined in Data.SBV.Provers.Prover | |
| ExtractIO m => SExecutable m (SBV a) Source # | |
| ExtractIO m => SExecutable m [SBV a] Source # | |
| (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) Source # | |
| (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) Source # | |
| (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) Source # | |
| (SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) Source # | |
| (SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d) -> p) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # | |
Defined in Data.SBV.Provers.Prover | |
| (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # | |
Defined in Data.SBV.Provers.Prover | |
| (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c) => SExecutable m (SBV a, SBV b, SBV c) Source # | |
| (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d) => SExecutable m (SBV a, SBV b, SBV c, SBV d) Source # | |
| (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e) Source # | |
| (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) Source # | |