| Copyright | (c) Brian Schroeder Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.SBV.Trans
Contents
- Symbolic types
- Arrays of symbolic values
- Creating symbolic values
- Symbolic Equality and Comparisons
- Conditionals: Mergeable values
- Symbolic integral numbers
- Division and Modulus
- Bit-vector operations
- IEEE-floating point numbers
- Enumerations
- Uninterpreted sorts, axioms, constants, and functions
- Properties, proofs, and satisfiability
- Constraints
- Checking safety
- Quick-checking
- Optimization
- Model extraction
- SMT Interface
- Abstract SBV type
- Module exports
Description
More generalized alternative to Data.SBV for advanced client use
Synopsis
- type SBool = SBV Bool
- sTrue :: SBool
- sFalse :: SBool
- sNot :: SBool -> SBool
- (.&&) :: SBool -> SBool -> SBool
- (.||) :: SBool -> SBool -> SBool
- (.<+>) :: SBool -> SBool -> SBool
- (.~&) :: SBool -> SBool -> SBool
- (.~|) :: SBool -> SBool -> SBool
- (.=>) :: SBool -> SBool -> SBool
- (.<=>) :: SBool -> SBool -> SBool
- fromBool :: Bool -> SBool
- oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a
- sAnd :: [SBool] -> SBool
- sOr :: [SBool] -> SBool
- sAny :: (a -> SBool) -> [a] -> SBool
- sAll :: (a -> SBool) -> [a] -> SBool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SWord (n :: Nat) = SBV (WordN n)
- data WordN (n :: Nat)
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInt (n :: Nat) = SBV (IntN n)
- data IntN (n :: Nat)
- type family BVIsNonZero (arg :: Nat) :: Constraint where ...
- type family FromSized (t :: Type) :: Type where ...
- type family ToSized (t :: Type) :: Type where ...
- fromSized :: FromSizedBV a => a -> FromSized a
- toSized :: ToSizedBV a => a -> ToSized a
- type SInteger = SBV Integer
- type SFloat = SBV Float
- type SDouble = SBV Double
- type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSInteger :: SReal -> SInteger
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- class SymArray array where
- newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
- newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
- readArray :: array a b -> SBV a -> SBV b
- writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b
- mergeArrays :: SymVal b => SBV Bool -> array a b -> array a b -> array a b
- data SArray a b
- sBool :: MonadSymbolic m => String -> m SBool
- sWord8 :: MonadSymbolic m => String -> m SWord8
- sWord16 :: MonadSymbolic m => String -> m SWord16
- sWord32 :: MonadSymbolic m => String -> m SWord32
- sWord64 :: MonadSymbolic m => String -> m SWord64
- sWord :: (KnownNat n, 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 :: (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)
- sBools :: MonadSymbolic m => [String] -> m [SBool]
- sWord8s :: MonadSymbolic m => [String] -> m [SWord8]
- sWord16s :: MonadSymbolic m => [String] -> m [SWord16]
- sWord32s :: MonadSymbolic m => [String] -> m [SWord32]
- sWord64s :: MonadSymbolic m => [String] -> m [SWord64]
- sWords :: (KnownNat n, 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 :: (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]
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class Equality a where