sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Brian Huffman
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Dynamic

Contents

- Programming with symbolic values
  - Symbolic types
    - Abstract symbolic value type
    - SMT Arrays of symbolic values
    - Functional arrays of symbolic values
  - Creating a symbolic variable
  - Operations on symbolic values
    - Boolean literals
    - Integer literals
    - Float literals
    - Algebraic reals (only from rationals)
    - Symbolic equality
    - Constructing concrete lists
    - Symbolic ordering
    - Arithmetic operations
    - Logical operations
    - Splitting, joining, and extending
    - Sign-casting
    - Numeric conversions
    - Indexed lookups
    - Word-level operations
  - Conditionals: Mergeable values
- Uninterpreted sorts, constants, and functions
- Properties, proofs, and satisfiability
  - Proving properties
  - Checking satisfiability
  - Checking safety
- Proving properties using multiple solvers
- Proving properties using multiple threads
- Quick-check
- Model extraction
  - Inspecting proof results
  - Programmable model extraction
- SMT Interface: Configurations and solvers
- Symbolic computations
- Code generation from symbolic programs
  - Setting code-generation options
  - Designating inputs
  - Designating outputs
  - Designating return values
  - Code generation with uninterpreted functions
  - Code generation with `SInteger` and `SReal` types
  - Compilation to C
  - Compilation to SMTLib

Description

Dynamically typed low-level API to the SBV library, for users who want to generate symbolic values at run-time. Note that with this API it is possible to create terms that are not type correct; use at your own risk!

Synopsis

- data SVal
- class HasKind a where
  - kindOf :: a -> Kind
  - hasSign :: a -> Bool
  - intSizeOf :: a -> Int
  - isBoolean :: a -> Bool
  - isBounded :: a -> Bool
  - isReal :: a -> Bool
  - isFloat :: a -> Bool
  - isDouble :: a -> Bool
  - isUnbounded :: a -> Bool
  - isUninterpreted :: a -> Bool
  - isChar :: a -> Bool
  - isString :: a -> Bool
  - isList :: a -> Bool
  - isSet :: a -> Bool
  - isTuple :: a -> Bool
  - isMaybe :: a -> Bool
  - isEither :: a -> Bool
  - showType :: a -> String
- data Kind
  - = KBool
  - | KBounded !Bool !Int
  - | KUnbounded
  - | KReal
  - | KUninterpreted String (Either String [String])
  - | KFloat
  - | KDouble
  - | KChar
  - | KString
  - | KList Kind
  - | KSet Kind
  - | KTuple [Kind]
  - | KMaybe Kind
  - | KEither Kind Kind
- data CV = CV {
  - _cvKind :: !Kind
  - cvVal :: !CVal
  }
- data CVal
  - = CAlgReal !AlgReal
  - | CInteger !Integer
  - | CFloat !Float
  - | CDouble !Double
  - | CChar !Char
  - | CString !String
  - | CList ![CVal]
  - | CSet !(RCSet CVal)
  - | CUserSort !(Maybe Int, String)
  - | CTuple ![CVal]
  - | CMaybe !(Maybe CVal)
  - | CEither !(Either CVal CVal)
- cvToBool :: CV -> Bool
- data SArr
- readSArr :: SArr -> SVal -> SVal
- writeSArr :: SArr -> SVal -> SVal -> SArr
- mergeSArr :: SVal -> SArr -> SArr -> SArr
- newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr
- eqSArr :: SArr -> SArr -> SVal
- data SFunArr
- readSFunArr :: SFunArr -> SVal -> SVal
- writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr
- mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr
- newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr
- type Symbolic = SymbolicT IO
- data Quantifier
  - = ALL
  - | EX
- svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
- sWordN :: MonadSymbolic m => Int -> String -> m SVal
- sWordN_ :: MonadSymbolic m => Int -> m SVal
- sIntN :: MonadSymbolic m => Int -> String -> m SVal
- sIntN_ :: MonadSymbolic m => Int -> m SVal
- svTrue :: SVal
- svFalse :: SVal
- svBool :: Bool -> SVal
- svAsBool :: SVal -> Maybe Bool
- svInteger :: Kind -> Integer -> SVal
- svAsInteger :: SVal -> Maybe Integer
- svFloat :: Float -> SVal
- svDouble :: Double -> SVal
- svReal :: Rational -> SVal
- svNumerator :: SVal -> Maybe Integer
- svDenominator :: SVal -> Maybe Integer
- svEqual :: SVal -> SVal -> SVal
- svNotEqual :: SVal -> SVal -> SVal
- svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
- svLessThan :: SVal -> SVal -> SVal
- svGreaterThan :: SVal -> SVal -> SVal
- svLessEq :: SVal -> SVal -> SVal
- svGreaterEq :: SVal -> SVal -> SVal
- svStructuralLessThan :: SVal -> SVal -> SVal
- svPlus :: SVal -> SVal -> SVal
- svTimes :: SVal -> SVal -> SVal
- svMinus :: SVal -> SVal -> SVal
- svUNeg :: SVal -> SVal
- svAbs :: SVal -> SVal
- svDivide :: SVal -> SVal -> SVal
- svQuot :: SVal -> SVal -> SVal
- svRem :: SVal -> SVal -> SVal
- svQuotRem :: SVal -> SVal -> (SVal, SVal)
- svExp :: SVal -> SVal -> SVal
- svAddConstant :: Integral a => SVal -> a -> SVal
- svIncrement :: SVal -> SVal
- svDecrement :: SVal -> SVal
- svAnd :: SVal -> SVal -> SVal
- svOr :: SVal -> SVal -> SVal
- svXOr :: SVal -> SVal -> SVal
- svNot :: SVal -> SVal
- svShl :: SVal -> Int -> SVal
- svShr :: SVal -> Int -> SVal
- svRol :: SVal -> Int -> SVal
- svRor :: SVal -> Int -> SVal
- svExtract :: Int -> Int -> SVal -> SVal
- svJoin :: SVal -> SVal -> SVal
- svSign :: SVal -> SVal
- svUnsign :: SVal -> SVal
- svFromIntegral :: Kind -> SVal -> SVal
- svSelect :: [SVal] -> SVal -> SVal -> SVal
- svToWord1 :: SVal -> SVal
- svFromWord1 :: SVal -> SVal
- svTestBit :: SVal -> Int -> SVal
- svSetBit :: SVal -> Int -> SVal
- svShiftLeft :: SVal -> SVal -> SVal
- svShiftRight :: SVal -> SVal -> SVal
- svRotateLeft :: SVal -> SVal -> SVal
- svRotateRight :: SVal -> SVal -> SVal
- svBarrelRotateLeft :: SVal -> SVal -> SVal
- svBarrelRotateRight :: SVal -> SVal -> SVal
- svWordFromBE :: [SVal] -> SVal
- svWordFromLE :: [SVal] -> SVal
- svBlastLE :: SVal -> [SVal]
- svBlastBE :: SVal -> [SVal]
- svIte :: SVal -> SVal -> SVal -> SVal
- svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
- svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
- svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
- proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
- satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
- allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
- safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
- proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
- satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
- satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
- proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
- satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
- satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
- svQuickCheck :: Symbolic SVal -> IO Bool
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
  - = LexicographicResult SMTResult
  - | ParetoResult (Bool, [SMTResult])
  - | IndependentResult [(String, SMTResult)]
- data SMTResult
  - = Unsatisfiable SMTConfig (Maybe [String])
  - | Satisfiable SMTConfig SMTModel
  - | SatExtField SMTConfig SMTModel
  - | Unknown SMTConfig SMTReasonUnknown
  - | ProofError SMTConfig [String] (Maybe SMTResult)
- genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV])
- getModelAssignment :: SMTResult -> Either String (Bool, [CV])
- getModelDictionary :: SMTResult -> Map String CV
- data SMTConfig = SMTConfig {
  - verbose :: Bool
  - timing :: Timing
  - printBase :: Int
  - printRealPrec :: Int
  - satCmd :: String
  - allSatMaxModelCount :: Maybe Int
  - allSatPrintAlong :: Bool
  - satTrackUFs :: Bool
  - isNonModelVar :: String -> Bool
  - validateModel :: Bool
  - optimizeValidateConstraints :: Bool
  - transcript :: Maybe FilePath
  - smtLibVersion :: SMTLibVersion
  - solver :: SMTSolver
  - allowQuantifiedQueries :: Bool
  - roundingMode :: RoundingMode
  - solverSetOptions :: [SMTOption]
  - ignoreExitCode :: Bool
  - redirectVerbose :: Maybe FilePath
  }
- data SMTLibVersion = SMTLib2
- data Solver
  - = Z3
  - | Yices
  - | Boolector
  - | CVC4
  - | MathSAT
  - | ABC
- data SMTSolver = SMTSolver {
  - name :: Solver
  - executable :: String
  - preprocess :: String -> String
  - options :: SMTConfig -> [String]
  - engine :: SMTEngine
  - capabilities :: SolverCapabilities
  }
- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- outputSVal :: MonadSymbolic m => SVal -> m ()
- data SBVCodeGen a
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- svCgInput :: Kind -> String -> SBVCodeGen SVal
- svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
- svCgOutput :: String -> SVal -> SBVCodeGen ()
- svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
- svCgReturn :: SVal -> SBVCodeGen ()
- svCgReturnArr :: [SVal] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
  - = CgFloat
  - | CgDouble
  - | CgLongDouble
- compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a]
- generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String

# Programming with symbolic values

## Symbolic types

### Abstract symbolic value type

data SVal Source #

The Symbolic value. Either a constant (`Left`) or a symbolic value (`Right Cached`). Note that caching is essential for making sure sharing is preserved.

#### Instances

Instances details

Eq SVal Source # | This instance is only defined so that we can define an instance for `Bits`. `==` and `/=` simply throw an error.
Instance details Defined in Data.SBV.Core.Symbolic Methods (==) :: SVal -> SVal -> Bool (/=) :: SVal -> SVal -> Bool
Show SVal Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> SVal -> ShowS show :: SVal -> String showList :: [SVal] -> ShowS
NFData SVal Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: SVal -> ()
HasKind SVal Source # |

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

kindOf :: SVal -> Kind Source #

hasSign :: SVal -> Bool Source #

intSizeOf :: SVal -> Int Source #

isBoolean :: SVal -> Bool Source #

isBounded :: SVal -> Bool Source #

isReal :: SVal -> Bool Source #

isFloat :: SVal -> Bool Source #

isDouble :: SVal -> Bool Source #

isUnbounded :: SVal -> Bool Source #

isUninterpreted :: SVal -> Bool Source #

isChar :: SVal -> Bool Source #

isString :: SVal -> Bool Source #

isList :: SVal -> Bool Source #

isSet :: SVal -> Bool Source #

isTuple :: SVal -> Bool Source #

isMaybe :: SVal -> Bool Source #

isEither :: SVal -> Bool Source #

showType :: SVal -> String Source #

ArithOverflow SVal Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SVal -> SVal -> (SBool, SBool) Source # bvSubO :: SVal -> SVal -> (SBool, SBool) Source # bvMulO :: SVal -> SVal -> (SBool, SBool) Source # bvMulOFast :: SVal -> SVal -> (SBool, SBool) Source # bvDivO :: SVal -> SVal -> (SBool, SBool) Source # bvNegO :: SVal -> (SBool, SBool) Source #
Testable (Symbolic SVal) Source # |
Instance details Defined in Data.SBV.Core.Model Methods property :: Symbolic SVal -> Property Source # propertyForAllShrinkShow :: Gen a -> (a -> [a]) -> (a -> [String]) -> (a -> Symbolic SVal) -> Property Source #

class HasKind a where Source #

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf, unless you can take advantage of the default signature: This class can be automatically derived for data-types that have a `Data` instance; this is useful for creating uninterpreted sorts. So, in reality, end users should almost never need to define any methods.

Minimal complete definition

Nothing

Methods

kindOf :: a -> Kind Source #

default kindOf :: (Read a, Data a) => a -> Kind Source #

hasSign :: a -> Bool Source #

intSizeOf :: a -> Int Source #

isBoolean :: a -> Bool Source #

isBounded :: a -> Bool Source #

isReal :: a -> Bool Source #

isFloat :: a -> Bool Source #

isDouble :: a -> Bool Source #

isUnbounded :: a -> Bool Source #

isUninterpreted :: a -> Bool Source #

isChar :: a -> Bool Source #

isString :: a -> Bool Source #

isList :: a -> Bool Source #

isSet :: a -> Bool Source #

isTuple :: a -> Bool Source #

isMaybe :: a -> Bool Source #

isEither :: a -> Bool Source #

showType :: a -> String Source #

#### Instances

Instances details

HasKind Bool Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Bool -> Kind Source #

hasSign :: Bool -> Bool Source #

intSizeOf :: Bool -> Int Source #

isBoolean :: Bool -> Bool Source #

isBounded :: Bool -> Bool Source #

isReal :: Bool -> Bool Source #

isFloat :: Bool -> Bool Source #

isDouble :: Bool -> Bool Source #

isUnbounded :: Bool -> Bool Source #

isUninterpreted :: Bool -> Bool Source #

isChar :: Bool -> Bool Source #

isString :: Bool -> Bool Source #

isList :: Bool -> Bool Source #

isSet :: Bool -> Bool Source #

isTuple :: Bool -> Bool Source #

isMaybe :: Bool -> Bool Source #

isEither :: Bool -> Bool Source #

showType :: Bool -> String Source #

HasKind Char Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Char -> Kind Source #

hasSign :: Char -> Bool Source #

intSizeOf :: Char -> Int Source #

isBoolean :: Char -> Bool Source #

isBounded :: Char -> Bool Source #

isReal :: Char -> Bool Source #

isFloat :: Char -> Bool Source #

isDouble :: Char -> Bool Source #

isUnbounded :: Char -> Bool Source #

isUninterpreted :: Char -> Bool Source #

isChar :: Char -> Bool Source #

isString :: Char -> Bool Source #

isList :: Char -> Bool Source #

isSet :: Char -> Bool Source #

isTuple :: Char -> Bool Source #

isMaybe :: Char -> Bool Source #

isEither :: Char -> Bool Source #

showType :: Char -> String Source #

HasKind Double Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Double -> Kind Source #

hasSign :: Double -> Bool Source #

intSizeOf :: Double -> Int Source #

isBoolean :: Double -> Bool Source #

isBounded :: Double -> Bool Source #

isReal :: Double -> Bool Source #

isFloat :: Double -> Bool Source #

isDouble :: Double -> Bool Source #

isUnbounded :: Double -> Bool Source #

isUninterpreted :: Double -> Bool Source #

isChar :: Double -> Bool Source #

isString :: Double -> Bool Source #

isList :: Double -> Bool Source #

isSet :: Double -> Bool Source #

isTuple :: Double -> Bool Source #

isMaybe :: Double -> Bool Source #

isEither :: Double -> Bool Source #

showType :: Double -> String Source #

HasKind Float Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Float -> Kind Source #

hasSign :: Float -> Bool Source #

intSizeOf :: Float -> Int Source #

isBoolean :: Float -> Bool Source #

isBounded :: Float -> Bool Source #

isReal :: Float -> Bool Source #

isFloat :: Float -> Bool Source #

isDouble :: Float -> Bool Source #

isUnbounded :: Float -> Bool Source #

isUninterpreted :: Float -> Bool Source #

isChar :: Float -> Bool Source #

isString :: Float -> Bool Source #

isList :: Float -> Bool Source #

isSet :: Float -> Bool Source #

isTuple :: Float -> Bool Source #

isMaybe :: Float -> Bool Source #

isEither :: Float -> Bool Source #

showType :: Float -> String Source #

HasKind Int8 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Int8 -> Kind Source #

hasSign :: Int8 -> Bool Source #

intSizeOf :: Int8 -> Int Source #

isBoolean :: Int8 -> Bool Source #

isBounded :: Int8 -> Bool Source #

isReal :: Int8 -> Bool Source #

isFloat :: Int8 -> Bool Source #

isDouble :: Int8 -> Bool Source #

isUnbounded :: Int8 -> Bool Source #

isUninterpreted :: Int8 -> Bool Source #

isChar :: Int8 -> Bool Source #

isString :: Int8 -> Bool Source #

isList :: Int8 -> Bool Source #

isSet :: Int8 -> Bool Source #

isTuple :: Int8 -> Bool Source #

isMaybe :: Int8 -> Bool Source #

isEither :: Int8 -> Bool Source #

showType :: Int8 -> String Source #

HasKind Int16 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Int16 -> Kind Source #

hasSign :: Int16 -> Bool Source #

intSizeOf :: Int16 -> Int Source #

isBoolean :: Int16 -> Bool Source #

isBounded :: Int16 -> Bool Source #

isReal :: Int16 -> Bool Source #

isFloat :: Int16 -> Bool Source #

isDouble :: Int16 -> Bool Source #

isUnbounded :: Int16 -> Bool Source #

isUninterpreted :: Int16 -> Bool Source #

isChar :: Int16 -> Bool Source #

isString :: Int16 -> Bool Source #

isList :: Int16 -> Bool Source #

isSet :: Int16 -> Bool Source #

isTuple :: Int16 -> Bool Source #

isMaybe :: Int16 -> Bool Source #

isEither :: Int16 -> Bool Source #

showType :: Int16 -> String Source #

HasKind Int32 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Int32 -> Kind Source #

hasSign :: Int32 -> Bool Source #

intSizeOf :: Int32 -> Int Source #

isBoolean :: Int32 -> Bool Source #

isBounded :: Int32 -> Bool Source #

isReal :: Int32 -> Bool Source #

isFloat :: Int32 -> Bool Source #

isDouble :: Int32 -> Bool Source #

isUnbounded :: Int32 -> Bool Source #

isUninterpreted :: Int32 -> Bool Source #

isChar :: Int32 -> Bool Source #

isString :: Int32 -> Bool Source #

isList :: Int32 -> Bool Source #

isSet :: Int32 -> Bool Source #

isTuple :: Int32 -> Bool Source #

isMaybe :: Int32 -> Bool Source #

isEither :: Int32 -> Bool Source #

showType :: Int32 -> String Source #

HasKind Int64 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Int64 -> Kind Source #

hasSign :: Int64 -> Bool Source #

intSizeOf :: Int64 -> Int Source #

isBoolean :: Int64 -> Bool Source #

isBounded :: Int64 -> Bool Source #

isReal :: Int64 -> Bool Source #

isFloat :: Int64 -> Bool Source #

isDouble :: Int64 -> Bool Source #

isUnbounded :: Int64 -> Bool Source #

isUninterpreted :: Int64 -> Bool Source #

isChar :: Int64 -> Bool Source #

isString :: Int64 -> Bool Source #

isList :: Int64 -> Bool Source #

isSet :: Int64 -> Bool Source #

isTuple :: Int64 -> Bool Source #

isMaybe :: Int64 -> Bool Source #

isEither :: Int64 -> Bool Source #

showType :: Int64 -> String Source #

HasKind Integer Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Integer -> Kind Source #

hasSign :: Integer -> Bool Source #

intSizeOf :: Integer -> Int Source #

isBoolean :: Integer -> Bool Source #

isBounded :: Integer -> Bool Source #

isReal :: Integer -> Bool Source #

isFloat :: Integer -> Bool Source #

isDouble :: Integer -> Bool Source #

isUnbounded :: Integer -> Bool Source #

isUninterpreted :: Integer -> Bool Source #

isChar :: Integer -> Bool Source #

isString :: Integer -> Bool Source #

isList :: Integer -> Bool Source #

isSet :: Integer -> Bool Source #

isTuple :: Integer -> Bool Source #

isMaybe :: Integer -> Bool Source #

isEither :: Integer -> Bool Source #

showType :: Integer -> String Source #

HasKind Word8 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Word8 -> Kind Source #

hasSign :: Word8 -> Bool Source #

intSizeOf :: Word8 -> Int Source #

isBoolean :: Word8 -> Bool Source #

isBounded :: Word8 -> Bool Source #

isReal :: Word8 -> Bool Source #

isFloat :: Word8 -> Bool Source #

isDouble :: Word8 -> Bool Source #

isUnbounded :: Word8 -> Bool Source #

isUninterpreted :: Word8 -> Bool Source #

isChar :: Word8 -> Bool Source #

isString :: Word8 -> Bool Source #

isList :: Word8 -> Bool Source #

isSet :: Word8 -> Bool Source #

isTuple :: Word8 -> Bool Source #

isMaybe :: Word8 -> Bool Source #

isEither :: Word8 -> Bool Source #

showType :: Word8 -> String Source #

HasKind Word16 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Word16 -> Kind Source #

hasSign :: Word16 -> Bool Source #

intSizeOf :: Word16 -> Int Source #

isBoolean :: Word16 -> Bool Source #

isBounded :: Word16 -> Bool Source #

isReal :: Word16 -> Bool Source #

isFloat :: Word16 -> Bool Source #

isDouble :: Word16 -> Bool Source #

isUnbounded :: Word16 -> Bool Source #

isUninterpreted :: Word16 -> Bool Source #

isChar :: Word16 -> Bool Source #

isString :: Word16 -> Bool Source #

isList :: Word16 -> Bool Source #

isSet :: Word16 -> Bool Source #

isTuple :: Word16 -> Bool Source #

isMaybe :: Word16 -> Bool Source #

isEither :: Word16 -> Bool Source #

showType :: Word16 -> String Source #

HasKind Word32 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Word32 -> Kind Source #

hasSign :: Word32 -> Bool Source #

intSizeOf :: Word32 -> Int Source #

isBoolean :: Word32 -> Bool Source #

isBounded :: Word32 -> Bool Source #

isReal :: Word32 -> Bool Source #

isFloat :: Word32 -> Bool Source #

isDouble :: Word32 -> Bool Source #

isUnbounded :: Word32 -> Bool Source #

isUninterpreted :: Word32 -> Bool Source #

isChar :: Word32 -> Bool Source #

isString :: Word32 -> Bool Source #

isList :: Word32 -> Bool Source #

isSet :: Word32 -> Bool Source #

isTuple :: Word32 -> Bool Source #

isMaybe :: Word32 -> Bool Source #

isEither :: Word32 -> Bool Source #

showType :: Word32 -> String Source #

HasKind Word64 Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Word64 -> Kind Source #

hasSign :: Word64 -> Bool Source #

intSizeOf :: Word64 -> Int Source #

isBoolean :: Word64 -> Bool Source #

isBounded :: Word64 -> Bool Source #

isReal :: Word64 -> Bool Source #

isFloat :: Word64 -> Bool Source #

isDouble :: Word64 -> Bool Source #

isUnbounded :: Word64 -> Bool Source #

isUninterpreted :: Word64 -> Bool Source #

isChar :: Word64 -> Bool Source #

isString :: Word64 -> Bool Source #

isList :: Word64 -> Bool Source #

isSet :: Word64 -> Bool Source #

isTuple :: Word64 -> Bool Source #

isMaybe :: Word64 -> Bool Source #

isEither :: Word64 -> Bool Source #

showType :: Word64 -> String Source #

HasKind () Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: () -> Kind Source #

hasSign :: () -> Bool Source #

intSizeOf :: () -> Int Source #

isBoolean :: () -> Bool Source #

isBounded :: () -> Bool Source #

isReal :: () -> Bool Source #

isFloat :: () -> Bool Source #

isDouble :: () -> Bool Source #

isUnbounded :: () -> Bool Source #

isUninterpreted :: () -> Bool Source #

isChar :: () -> Bool Source #

isString :: () -> Bool Source #

isList :: () -> Bool Source #

isSet :: () -> Bool Source #

isTuple :: () -> Bool Source #

isMaybe :: () -> Bool Source #

isEither :: () -> Bool Source #

showType :: () -> String Source #

HasKind AlgReal Source # |

Instance details

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 #

isUnbounded :: AlgReal -> Bool Source #

isUninterpreted :: AlgReal -> Bool Source #

isChar :: AlgReal -> Bool Source #

isString :: AlgReal -> Bool Source #

isList :: AlgReal -> Bool Source #

isSet :: AlgReal -> Bool Source #

isTuple :: AlgReal -> Bool Source #

isMaybe :: AlgReal -> Bool Source #

isEither :: AlgReal -> Bool Source #

showType :: AlgReal -> String Source #

HasKind Kind Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Kind -> Kind Source #

hasSign :: Kind -> Bool Source #

intSizeOf :: Kind -> Int Source #

isBoolean :: Kind -> Bool Source #

isBounded :: Kind -> Bool Source #

isReal :: Kind -> Bool Source #

isFloat :: Kind -> Bool Source #

isDouble :: Kind -> Bool Source #

isUnbounded :: Kind -> Bool Source #

isUninterpreted :: Kind -> Bool Source #

isChar :: Kind -> Bool Source #

isString :: Kind -> Bool Source #

isList :: Kind -> Bool Source #

isSet :: Kind -> Bool Source #

isTuple :: Kind -> Bool Source #

isMaybe :: Kind -> Bool Source #

isEither :: Kind -> Bool Source #

showType :: Kind -> String Source #

HasKind ExtCV Source # | Kind instance for Extended CV

Instance details

Defined in Data.SBV.Core.Concrete

Methods

kindOf :: ExtCV -> Kind Source #

hasSign :: ExtCV -> Bool Source #

intSizeOf :: ExtCV -> Int Source #

isBoolean :: ExtCV -> Bool Source #

isBounded :: ExtCV -> Bool Source #

isReal :: ExtCV -> Bool Source #

isFloat :: ExtCV -> Bool Source #

isDouble :: ExtCV -> Bool Source #

isUnbounded :: ExtCV -> Bool Source #

isUninterpreted :: ExtCV -> Bool Source #

isChar :: ExtCV -> Bool Source #

isString :: ExtCV -> Bool Source #

isList :: ExtCV -> Bool Source #

isSet :: ExtCV -> Bool Source #

isTuple :: ExtCV -> Bool Source #

isMaybe :: ExtCV -> Bool Source #

isEither :: ExtCV -> Bool Source #

showType :: ExtCV -> String Source #

HasKind GeneralizedCV Source # | `Kind` instance for generalized CV

Instance details

Defined in Data.SBV.Core.Concrete

Methods

kindOf :: GeneralizedCV -> Kind Source #

hasSign :: GeneralizedCV -> Bool Source #

intSizeOf :: GeneralizedCV -> Int Source #

isBoolean :: GeneralizedCV -> Bool Source #

isBounded :: GeneralizedCV -> Bool Source #

isReal :: GeneralizedCV -> Bool Source #

isFloat :: GeneralizedCV -> Bool Source #

isDouble :: GeneralizedCV -> Bool Source #

isUnbounded :: GeneralizedCV -> Bool Source #

isUninterpreted :: GeneralizedCV -> Bool Source #

isChar :: GeneralizedCV -> Bool Source #

isString :: GeneralizedCV -> Bool Source #

isList :: GeneralizedCV -> Bool Source #

isSet :: GeneralizedCV -> Bool Source #

isTuple :: GeneralizedCV -> Bool Source #

isMaybe :: GeneralizedCV -> Bool Source #

isEither :: GeneralizedCV -> Bool Source #

showType :: GeneralizedCV -> String Source #

HasKind CV Source # | `Kind` instance for CV

Instance details

Defined in Data.SBV.Core.Concrete

Methods

kindOf :: CV -> Kind Source #

hasSign :: CV -> Bool Source #

intSizeOf :: CV -> Int Source #

isBoolean :: CV -> Bool Source #

isBounded :: CV -> Bool Source #

isReal :: CV -> Bool Source #

isFloat :: CV -> Bool Source #

isDouble :: CV -> Bool Source #

isUnbounded :: CV -> Bool Source #

isUninterpreted :: CV -> Bool Source #

isChar :: CV -> Bool Source #

isString :: CV -> Bool Source #

isList :: CV -> Bool Source #

isSet :: CV -> Bool Source #

isTuple :: CV -> Bool Source #

isMaybe :: CV -> Bool Source #

isEither :: CV -> Bool Source #

showType :: CV -> String Source #

HasKind RoundingMode Source # | `RoundingMode` kind

Instance details

Defined in Data.SBV.Core.Symbolic

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 #

isUnbounded :: RoundingMode -> Bool Source #

isUninterpreted :: RoundingMode -> Bool Source #

isChar :: RoundingMode -> Bool Source #

isString :: RoundingMode -> Bool Source #

isList :: RoundingMode -> Bool Source #

isSet :: RoundingMode -> Bool Source #

isTuple :: RoundingMode -> Bool Source #

isMaybe :: RoundingMode -> Bool Source #

isEither :: RoundingMode -> Bool Source #

showType :: RoundingMode -> String Source #

HasKind SVal Source # |

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

kindOf :: SVal -> Kind Source #

hasSign :: SVal -> Bool Source #

intSizeOf :: SVal -> Int Source #

isBoolean :: SVal -> Bool Source #

isBounded :: SVal -> Bool Source #

isReal :: SVal -> Bool Source #

isFloat :: SVal -> Bool Source #

isDouble :: SVal -> Bool Source #

isUnbounded :: SVal -> Bool Source #

isUninterpreted :: SVal -> Bool Source #

isChar :: SVal -> Bool Source #

isString :: SVal -> Bool Source #

isList :: SVal -> Bool Source #

isSet :: SVal -> Bool Source #

isTuple :: SVal -> Bool Source #

isMaybe :: SVal -> Bool Source #

isEither :: SVal -> Bool Source #

showType :: SVal -> String Source #

HasKind SV Source # |

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

kindOf :: SV -> Kind Source #

hasSign :: SV -> Bool Source #

intSizeOf :: SV -> Int Source #

isBoolean :: SV -> Bool Source #

isBounded :: SV -> Bool Source #

isReal :: SV -> Bool Source #

isFloat :: SV -> Bool Source #

isDouble :: SV -> Bool Source #

isUnbounded :: SV -> Bool Source #

isUninterpreted :: SV -> Bool Source #

isChar :: SV -> Bool Source #

isString :: SV -> Bool Source #

isList :: SV -> Bool Source #

isSet :: SV -> Bool Source #

isTuple :: SV -> Bool Source #

isMaybe :: SV -> Bool Source #

isEither :: SV -> Bool Source #

showType :: SV -> String Source #

HasKind State Source # |

Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

kindOf :: State -> Kind Source #

hasSign :: State -> Bool Source #

intSizeOf :: State -> Int Source #

isBoolean :: State -> Bool Source #

isBounded :: State -> Bool Source #

isReal :: State -> Bool Source #

isFloat :: State -> Bool Source #

isDouble :: State -> Bool Source #

isUnbounded :: State -> Bool Source #

isUninterpreted :: State -> Bool Source #

isChar :: State -> Bool Source #

isString :: State -> Bool Source #

isList :: State -> Bool Source #

isSet :: State -> Bool Source #

isTuple :: State -> Bool Source #

isMaybe :: State -> Bool Source #

isEither :: State -> Bool Source #

showType :: State -> String Source #

HasKind E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

kindOf :: E -> Kind Source #

hasSign :: E -> Bool Source #

intSizeOf :: E -> Int Source #

isBoolean :: E -> Bool Source #

isBounded :: E -> Bool Source #

isReal :: E -> Bool Source #

isFloat :: E -> Bool Source #

isDouble :: E -> Bool Source #

isUnbounded :: E -> Bool Source #

isUninterpreted :: E -> Bool Source #

isChar :: E -> Bool Source #

isString :: E -> Bool Source #

isList :: E -> Bool Source #

isSet :: E -> Bool Source #

isTuple :: E -> Bool Source #

isMaybe :: E -> Bool Source #

isEither :: E -> Bool Source #

showType :: E -> String Source #

HasKind HumanHeightInCm Source # | Symbolic instance simply follows the underlying type, just like `Metres`.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: HumanHeightInCm -> Kind Source #

hasSign :: HumanHeightInCm -> Bool Source #

intSizeOf :: HumanHeightInCm -> Int Source #

isBoolean :: HumanHeightInCm -> Bool Source #

isBounded :: HumanHeightInCm -> Bool Source #

isReal :: HumanHeightInCm -> Bool Source #

isFloat :: HumanHeightInCm -> Bool Source #

isDouble :: HumanHeightInCm -> Bool Source #

isUnbounded :: HumanHeightInCm -> Bool Source #

isUninterpreted :: HumanHeightInCm -> Bool Source #

isChar :: HumanHeightInCm -> Bool Source #

isString :: HumanHeightInCm -> Bool Source #

isList :: HumanHeightInCm -> Bool Source #

isSet :: HumanHeightInCm -> Bool Source #

isTuple :: HumanHeightInCm -> Bool Source #

isMaybe :: HumanHeightInCm -> Bool Source #

isEither :: HumanHeightInCm -> Bool Source #

showType :: HumanHeightInCm -> String Source #

HasKind Metres Source # | To use `Metres` symbolically, we associate it with the underlying symbolic type's kind.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: Metres -> Kind Source #

hasSign :: Metres -> Bool Source #

intSizeOf :: Metres -> Int Source #

isBoolean :: Metres -> Bool Source #

isBounded :: Metres -> Bool Source #

isReal :: Metres -> Bool Source #

isFloat :: Metres -> Bool Source #

isDouble :: Metres -> Bool Source #

isUnbounded :: Metres -> Bool Source #

isUninterpreted :: Metres -> Bool Source #

isChar :: Metres -> Bool Source #

isString :: Metres -> Bool Source #

isList :: Metres -> Bool Source #

isSet :: Metres -> Bool Source #

isTuple :: Metres -> Bool Source #

isMaybe :: Metres -> Bool Source #

isEither :: Metres -> Bool Source #

showType :: Metres -> String Source #

HasKind Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

Methods

kindOf :: Day -> Kind Source #

hasSign :: Day -> Bool Source #

intSizeOf :: Day -> Int Source #

isBoolean :: Day -> Bool Source #

isBounded :: Day -> Bool Source #

isReal :: Day -> Bool Source #

isFloat :: Day -> Bool Source #

isDouble :: Day -> Bool Source #

isUnbounded :: Day -> Bool Source #

isUninterpreted :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

isSet :: Day -> Bool Source #

isTuple :: Day -> Bool Source #

isMaybe :: Day -> Bool Source #

isEither :: Day -> Bool Source #

showType :: Day -> String Source #

HasKind Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Color -> Kind Source #

hasSign :: Color -> Bool Source #

intSizeOf :: Color -> Int Source #

isBoolean :: Color -> Bool Source #

isBounded :: Color -> Bool Source #

isReal :: Color -> Bool Source #

isFloat :: Color -> Bool Source #

isDouble :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUninterpreted :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

isList :: Color -> Bool Source #

isSet :: Color -> Bool Source #

isTuple :: Color -> Bool Source #

isMaybe :: Color -> Bool Source #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

HasKind Nationality Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Nationality -> Kind Source #

hasSign :: Nationality -> Bool Source #

intSizeOf :: Nationality -> Int Source #

isBoolean :: Nationality -> Bool Source #

isBounded :: Nationality -> Bool Source #

isReal :: Nationality -> Bool Source #

isFloat :: Nationality -> Bool Source #

isDouble :: Nationality -> Bool Source #

isUnbounded :: Nationality -> Bool Source #

isUninterpreted :: Nationality -> Bool Source #

isChar :: Nationality -> Bool Source #

isString :: Nationality -> Bool Source #

isList :: Nationality -> Bool Source #

isSet :: Nationality -> Bool Source #

isTuple :: Nationality -> Bool Source #

isMaybe :: Nationality -> Bool Source #

isEither :: Nationality -> Bool Source #

showType :: Nationality -> String Source #

HasKind Beverage Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Beverage -> Kind Source #

hasSign :: Beverage -> Bool Source #

intSizeOf :: Beverage -> Int Source #

isBoolean :: Beverage -> Bool Source #

isBounded :: Beverage -> Bool Source #

isReal :: Beverage -> Bool Source #

isFloat :: Beverage -> Bool Source #

isDouble :: Beverage -> Bool Source #

isUnbounded :: Beverage -> Bool Source #

isUninterpreted :: Beverage -> Bool Source #

isChar :: Beverage -> Bool Source #

isString :: Beverage -> Bool Source #

isList :: Beverage -> Bool Source #

isSet :: Beverage -> Bool Source #

isTuple :: Beverage -> Bool Source #

isMaybe :: Beverage -> Bool Source #

isEither :: Beverage -> Bool Source #

showType :: Beverage -> String Source #

HasKind Pet Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Pet -> Kind Source #

hasSign :: Pet -> Bool Source #

intSizeOf :: Pet -> Int Source #

isBoolean :: Pet -> Bool Source #

isBounded :: Pet -> Bool Source #

isReal :: Pet -> Bool Source #

isFloat :: Pet -> Bool Source #

isDouble :: Pet -> Bool Source #

isUnbounded :: Pet -> Bool Source #

isUninterpreted :: Pet -> Bool Source #

isChar :: Pet -> Bool Source #

isString :: Pet -> Bool Source #

isList :: Pet -> Bool Source #

isSet :: Pet -> Bool Source #

isTuple :: Pet -> Bool Source #

isMaybe :: Pet -> Bool Source #

isEither :: Pet -> Bool Source #

showType :: Pet -> String Source #

HasKind Sport Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Sport -> Kind Source #

hasSign :: Sport -> Bool Source #

intSizeOf :: Sport -> Int Source #

isBoolean :: Sport -> Bool Source #

isBounded :: Sport -> Bool Source #

isReal :: Sport -> Bool Source #

isFloat :: Sport -> Bool Source #

isDouble :: Sport -> Bool Source #

isUnbounded :: Sport -> Bool Source #

isUninterpreted :: Sport -> Bool Source #

isChar :: Sport -> Bool Source #

isString :: Sport -> Bool Source #

isList :: Sport -> Bool Source #

isSet :: Sport -> Bool Source #

isTuple :: Sport -> Bool Source #

isMaybe :: Sport -> Bool Source #

isEither :: Sport -> Bool Source #

showType :: Sport -> String Source #

HasKind Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

kindOf :: Color -> Kind Source #

hasSign :: Color -> Bool Source #

intSizeOf :: Color -> Int Source #

isBoolean :: Color -> Bool Source #

isBounded :: Color -> Bool Source #

isReal :: Color -> Bool Source #

isFloat :: Color -> Bool Source #

isDouble :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUninterpreted :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

isList :: Color -> Bool Source #

isSet :: Color -> Bool Source #

isTuple :: Color -> Bool Source #

isMaybe :: Color -> Bool Source #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

HasKind Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

kindOf :: Color -> Kind Source #

hasSign :: Color -> Bool Source #

intSizeOf :: Color -> Int Source #

isBoolean :: Color -> Bool Source #

isBounded :: Color -> Bool Source #

isReal :: Color -> Bool Source #

isFloat :: Color -> Bool Source #

isDouble :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUninterpreted :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

isList :: Color -> Bool Source #

isSet :: Color -> Bool Source #

isTuple :: Color -> Bool Source #

isMaybe :: Color -> Bool Source #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

HasKind U2Member Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

kindOf :: U2Member -> Kind Source #

hasSign :: U2Member -> Bool Source #

intSizeOf :: U2Member -> Int Source #

isBoolean :: U2Member -> Bool Source #

isBounded :: U2Member -> Bool Source #

isReal :: U2Member -> Bool Source #

isFloat :: U2Member -> Bool Source #

isDouble :: U2Member -> Bool Source #

isUnbounded :: U2Member -> Bool Source #

isUninterpreted :: U2Member -> Bool Source #

isChar :: U2Member -> Bool Source #

isString :: U2Member -> Bool Source #

isList :: U2Member -> Bool Source #

isSet :: U2Member -> Bool Source #

isTuple :: U2Member -> Bool Source #

isMaybe :: U2Member -> Bool Source #

isEither :: U2Member -> Bool Source #

showType :: U2Member -> String Source #

HasKind Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

kindOf :: Location -> Kind Source #

hasSign :: Location -> Bool Source #

intSizeOf :: Location -> Int Source #

isBoolean :: Location -> Bool Source #

isBounded :: Location -> Bool Source #

isReal :: Location -> Bool Source #

isFloat :: Location -> Bool Source #

isDouble :: Location -> Bool Source #

isUnbounded :: Location -> Bool Source #

isUninterpreted :: Location -> Bool Source #

isChar :: Location -> Bool Source #

isString :: Location -> Bool Source #

isList :: Location -> Bool Source #

isSet :: Location -> Bool Source #

isTuple :: Location -> Bool Source #

isMaybe :: Location -> Bool Source #

isEither :: Location -> Bool Source #

showType :: Location -> String Source #

HasKind Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

kindOf :: Day -> Kind Source #

hasSign :: Day -> Bool Source #

intSizeOf :: Day -> Int Source #

isBoolean :: Day -> Bool Source #

isBounded :: Day -> Bool Source #

isReal :: Day -> Bool Source #

isFloat :: Day -> Bool Source #

isDouble :: Day -> Bool Source #

isUnbounded :: Day -> Bool Source #

isUninterpreted :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

isSet :: Day -> Bool Source #

isTuple :: Day -> Bool Source #

isMaybe :: Day -> Bool Source #

isEither :: Day -> Bool Source #

showType :: Day -> String Source #

HasKind BinOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: BinOp -> Kind Source #

hasSign :: BinOp -> Bool Source #

intSizeOf :: BinOp -> Int Source #

isBoolean :: BinOp -> Bool Source #

isBounded :: BinOp -> Bool Source #

isReal :: BinOp -> Bool Source #

isFloat :: BinOp -> Bool Source #

isDouble :: BinOp -> Bool Source #

isUnbounded :: BinOp -> Bool Source #

isUninterpreted :: BinOp -> Bool Source #

isChar :: BinOp -> Bool Source #

isString :: BinOp -> Bool Source #

isList :: BinOp -> Bool Source #

isSet :: BinOp -> Bool Source #

isTuple :: BinOp -> Bool Source #

isMaybe :: BinOp -> Bool Source #

isEither :: BinOp -> Bool Source #

showType :: BinOp -> String Source #

HasKind UnOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: UnOp -> Kind Source #

hasSign :: UnOp -> Bool Source #

intSizeOf :: UnOp -> Int Source #

isBoolean :: UnOp -> Bool Source #

isBounded :: UnOp -> Bool Source #

isReal :: UnOp -> Bool Source #

isFloat :: UnOp -> Bool Source #

isDouble :: UnOp -> Bool Source #

isUnbounded :: UnOp -> Bool Source #

isUninterpreted :: UnOp -> Bool Source #

isChar :: UnOp -> Bool Source #

isString :: UnOp -> Bool Source #

isList :: UnOp -> Bool Source #

isSet :: UnOp -> Bool Source #

isTuple :: UnOp -> Bool Source #

isMaybe :: UnOp -> Bool Source #

isEither :: UnOp -> Bool Source #

showType :: UnOp -> String Source #

HasKind B Source # |

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Deduce

Methods

kindOf :: B -> Kind Source #

hasSign :: B -> Bool Source #

intSizeOf :: B -> Int Source #

isBoolean :: B -> Bool Source #

isBounded :: B -> Bool Source #

isReal :: B -> Bool Source #

isFloat :: B -> Bool Source #

isDouble :: B -> Bool Source #

isUnbounded :: B -> Bool Source #

isUninterpreted :: B -> Bool Source #

isChar :: B -> Bool Source #

isString :: B -> Bool Source #

isList :: B -> Bool Source #

isSet :: B -> Bool Source #

isTuple :: B -> Bool Source #

isMaybe :: B -> Bool Source #

isEither :: B -> Bool Source #

showType :: B -> String Source #

HasKind Q Source # |

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

kindOf :: Q -> Kind Source #

hasSign :: Q -> Bool Source #

intSizeOf :: Q -> Int Source #

isBoolean :: Q -> Bool Source #

isBounded :: Q -> Bool Source #

isReal :: Q -> Bool Source #

isFloat :: Q -> Bool Source #

isDouble :: Q -> Bool Source #

isUnbounded :: Q -> Bool Source #

isUninterpreted :: Q -> Bool Source #

isChar :: Q -> Bool Source #

isString :: Q -> Bool Source #

isList :: Q -> Bool Source #

isSet :: Q -> Bool Source #

isTuple :: Q -> Bool Source #

isMaybe :: Q -> Bool Source #

isEither :: Q -> Bool Source #

showType :: Q -> String Source #

HasKind L Source # | Similarly, `HasKind`s default implementation is sufficient.

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

kindOf :: L -> Kind Source #

hasSign :: L -> Bool Source #

intSizeOf :: L -> Int Source #

isBoolean :: L -> Bool Source #

isBounded :: L -> Bool Source #

isReal :: L -> Bool Source #

isFloat :: L -> Bool Source #

isDouble :: L -> Bool Source #

isUnbounded :: L -> Bool Source #

isUninterpreted :: L -> Bool Source #

isChar :: L -> Bool Source #

isString :: L -> Bool Source #

isList :: L -> Bool Source #

isSet :: L -> Bool Source #

isTuple :: L -> Bool Source #

isMaybe :: L -> Bool Source #

isEither :: L -> Bool Source #

showType :: L -> String Source #

(Typeable a, HasKind a) => HasKind [a] Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: [a] -> Kind Source #

hasSign :: [a] -> Bool Source #

intSizeOf :: [a] -> Int Source #

isBoolean :: [a] -> Bool Source #

isBounded :: [a] -> Bool Source #

isReal :: [a] -> Bool Source #

isFloat :: [a] -> Bool Source #

isDouble :: [a] -> Bool Source #

isUnbounded :: [a] -> Bool Source #

isUninterpreted :: [a] -> Bool Source #

isChar :: [a] -> Bool Source #

isString :: [a] -> Bool Source #

isList :: [a] -> Bool Source #

isSet :: [a] -> Bool Source #

isTuple :: [a] -> Bool Source #

isMaybe :: [a] -> Bool Source #

isEither :: [a] -> Bool Source #

showType :: [a] -> String Source #

HasKind a => HasKind (Maybe a) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Maybe a -> Kind Source #

hasSign :: Maybe a -> Bool Source #

intSizeOf :: Maybe a -> Int Source #

isBoolean :: Maybe a -> Bool Source #

isBounded :: Maybe a -> Bool Source #

isReal :: Maybe a -> Bool Source #

isFloat :: Maybe a -> Bool Source #

isDouble :: Maybe a -> Bool Source #

isUnbounded :: Maybe a -> Bool Source #

isUninterpreted :: Maybe a -> Bool Source #

isChar :: Maybe a -> Bool Source #

isString :: Maybe a -> Bool Source #

isList :: Maybe a -> Bool Source #

isSet :: Maybe a -> Bool Source #

isTuple :: Maybe a -> Bool Source #

isMaybe :: Maybe a -> Bool Source #

isEither :: Maybe a -> Bool Source #

showType :: Maybe a -> String Source #

HasKind a => HasKind (RCSet a) Source # |

Instance details

Defined in Data.SBV.Core.Concrete

Methods

kindOf :: RCSet a -> Kind Source #

hasSign :: RCSet a -> Bool Source #

intSizeOf :: RCSet a -> Int Source #

isBoolean :: RCSet a -> Bool Source #

isBounded :: RCSet a -> Bool Source #

isReal :: RCSet a -> Bool Source #

isFloat :: RCSet a -> Bool Source #

isDouble :: RCSet a -> Bool Source #

isUnbounded :: RCSet a -> Bool Source #

isUninterpreted :: RCSet a -> Bool Source #

isChar :: RCSet a -> Bool Source #

isString :: RCSet a -> Bool Source #

isList :: RCSet a -> Bool Source #

isSet :: RCSet a -> Bool Source #

isTuple :: RCSet a -> Bool Source #

isMaybe :: RCSet a -> Bool Source #

isEither :: RCSet a -> Bool Source #

showType :: RCSet a -> String Source #

HasKind a => HasKind (SBV a) Source # |

Instance details

Defined in Data.SBV.Core.Data

Methods

kindOf :: SBV a -> Kind Source #

hasSign :: SBV a -> Bool Source #

intSizeOf :: SBV a -> Int Source #

isBoolean :: SBV a -> Bool Source #

isBounded :: SBV a -> Bool Source #

isReal :: SBV a -> Bool Source #

isFloat :: SBV a -> Bool Source #

isDouble :: SBV a -> Bool Source #

isUnbounded :: SBV a -> Bool Source #

isUninterpreted :: SBV a -> Bool Source #

isChar :: SBV a -> Bool Source #

isString :: SBV a -> Bool Source #

isList :: SBV a -> Bool Source #

isSet :: SBV a -> Bool Source #

isTuple :: SBV a -> Bool Source #

isMaybe :: SBV a -> Bool Source #

isEither :: SBV a -> Bool Source #

showType :: SBV a -> String Source #

(KnownNat n, IsNonZero n) => HasKind (IntN n) Source # | `IntN` has a kind

Instance details

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 #

isUnbounded :: IntN n -> Bool Source #

isUninterpreted :: 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 #

isMaybe :: IntN n -> Bool Source #

isEither :: IntN n -> Bool Source #

showType :: IntN n -> String Source #

(KnownNat n, IsNonZero n) => HasKind (WordN n) Source # | `WordN` has a kind

Instance details

Defined in Data.SBV.Core.Sized

Methods

kindOf :: WordN n -> Kind Source #

hasSign :: WordN n -> Bool Source #

intSizeOf :: WordN n -> Int Source #

isBoolean :: WordN n -> Bool Source #

isBounded :: WordN n -> Bool Source #

isReal :: WordN n -> Bool Source #

isFloat :: WordN n -> Bool Source #

isDouble :: WordN n -> Bool Source #

isUnbounded :: WordN n -> Bool Source #

isUninterpreted :: WordN n -> Bool Source #

isChar :: WordN n -> Bool Source #

isString :: WordN n -> Bool Source #

isList :: WordN n -> Bool Source #

isSet :: WordN n -> Bool Source #

isTuple :: WordN n -> Bool Source #

isMaybe :: WordN n -> Bool Source #

isEither :: WordN n -> Bool Source #

showType :: WordN n -> String Source #

(HasKind a, HasKind b) => HasKind (Either a b) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Either a b -> Kind Source #

hasSign :: Either a b -> Bool Source #

intSizeOf :: Either a b -> Int Source #

isBoolean :: Either a b -> Bool Source #

isBounded :: Either a b -> Bool Source #

isReal :: Either a b -> Bool Source #

isFloat :: Either a b -> Bool Source #

isDouble :: Either a b -> Bool Source #

isUnbounded :: Either a b -> Bool Source #

isUninterpreted :: Either a b -> Bool Source #

isChar :: Either a b -> Bool Source #

isString :: Either a b -> Bool Source #

isList :: Either a b -> Bool Source #

isSet :: Either a b -> Bool Source #

isTuple :: Either a b -> Bool Source #

isMaybe :: Either a b -> Bool Source #

isEither :: Either a b -> Bool Source #

showType :: Either a b -> String Source #

(HasKind a, HasKind b) => HasKind (a, b) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b) -> Kind Source #

hasSign :: (a, b) -> Bool Source #

intSizeOf :: (a, b) -> Int Source #

isBoolean :: (a, b) -> Bool Source #

isBounded :: (a, b) -> Bool Source #

isReal :: (a, b) -> Bool Source #

isFloat :: (a, b) -> Bool Source #

isDouble :: (a, b) -> Bool Source #

isUnbounded :: (a, b) -> Bool Source #

isUninterpreted :: (a, b) -> Bool Source #

isChar :: (a, b) -> Bool Source #

isString :: (a, b) -> Bool Source #

isList :: (a, b) -> Bool Source #

isSet :: (a, b) -> Bool Source #

isTuple :: (a, b) -> Bool Source #

isMaybe :: (a, b) -> Bool Source #

isEither :: (a, b) -> Bool Source #

showType :: (a, b) -> String Source #

HasKind a => HasKind (Proxy a) Source # | This instance allows us to use the `kindOf (Proxy @a)` idiom instead of the `kindOf (undefined :: a)`, which is safer and looks more idiomatic.

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Proxy a -> Kind Source #

hasSign :: Proxy a -> Bool Source #

intSizeOf :: Proxy a -> Int Source #

isBoolean :: Proxy a -> Bool Source #

isBounded :: Proxy a -> Bool Source #

isReal :: Proxy a -> Bool Source #

isFloat :: Proxy a -> Bool Source #

isDouble :: Proxy a -> Bool Source #

isUnbounded :: Proxy a -> Bool Source #

isUninterpreted :: Proxy a -> Bool Source #

isChar :: Proxy a -> Bool Source #

isString :: Proxy a -> Bool Source #

isList :: Proxy a -> Bool Source #

isSet :: Proxy a -> Bool Source #

isTuple :: Proxy a -> Bool Source #

isMaybe :: Proxy a -> Bool Source #

isEither :: Proxy a -> Bool Source #

showType :: Proxy a -> String Source #

(HasKind a, HasKind b, HasKind c) => HasKind (a, b, c) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c) -> Kind Source #

hasSign :: (a, b, c) -> Bool Source #

intSizeOf :: (a, b, c) -> Int Source #

isBoolean :: (a, b, c) -> Bool Source #

isBounded :: (a, b, c) -> Bool Source #

isReal :: (a, b, c) -> Bool Source #

isFloat :: (a, b, c) -> Bool Source #

isDouble :: (a, b, c) -> Bool Source #

isUnbounded :: (a, b, c) -> Bool Source #

isUninterpreted :: (a, b, c) -> Bool Source #

isChar :: (a, b, c) -> Bool Source #

isString :: (a, b, c) -> Bool Source #

isList :: (a, b, c) -> Bool Source #

isSet :: (a, b, c) -> Bool Source #

isTuple :: (a, b, c) -> Bool Source #

isMaybe :: (a, b, c) -> Bool Source #

isEither :: (a, b, c) -> Bool Source #

showType :: (a, b, c) -> String Source #

(HasKind a, HasKind b, HasKind c, HasKind d) => HasKind (a, b, c, d) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c, d) -> Kind Source #

hasSign :: (a, b, c, d) -> Bool Source #

intSizeOf :: (a, b, c, d) -> Int Source #

isBoolean :: (a, b, c, d) -> Bool Source #

isBounded :: (a, b, c, d) -> Bool Source #

isReal :: (a, b, c, d) -> Bool Source #

isFloat :: (a, b, c, d) -> Bool Source #

isDouble :: (a, b, c, d) -> Bool Source #

isUnbounded :: (a, b, c, d) -> Bool Source #

isUninterpreted :: (a, b, c, d) -> Bool Source #

isChar :: (a, b, c, d) -> Bool Source #

isString :: (a, b, c, d) -> Bool Source #

isList :: (a, b, c, d) -> Bool Source #

isSet :: (a, b, c, d) -> Bool Source #

isTuple :: (a, b, c, d) -> Bool Source #

isMaybe :: (a, b, c, d) -> Bool Source #

isEither :: (a, b, c, d) -> Bool Source #

showType :: (a, b, c, d) -> String Source #

(HasKind a, HasKind b, HasKind c, HasKind d, HasKind e) => HasKind (a, b, c, d, e) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c, d, e) -> Kind Source #

hasSign :: (a, b, c, d, e) -> Bool Source #

intSizeOf :: (a, b, c, d, e) -> Int Source #

isBoolean :: (a, b, c, d, e) -> Bool Source #

isBounded :: (a, b, c, d, e) -> Bool Source #

isReal :: (a, b, c, d, e) -> Bool Source #

isFloat :: (a, b, c, d, e) -> Bool Source #

isDouble :: (a, b, c, d, e) -> Bool Source #

isUnbounded :: (a, b, c, d, e) -> Bool Source #

isUninterpreted :: (a, b, c, d, e) -> Bool Source #

isChar :: (a, b, c, d, e) -> Bool Source #

isString :: (a, b, c, d, e) -> Bool Source #

isList :: (a, b, c, d, e) -> Bool Source #

isSet :: (a, b, c, d, e) -> Bool Source #

isTuple :: (a, b, c, d, e) -> Bool Source #

isMaybe :: (a, b, c, d, e) -> Bool Source #

isEither :: (a, b, c, d, e) -> Bool Source #

showType :: (a, b, c, d, e) -> String Source #

(HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f) => HasKind (a, b, c, d, e, f) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c, d, e, f) -> Kind Source #

hasSign :: (a, b, c, d, e, f) -> Bool Source #

intSizeOf :: (a, b, c, d, e, f) -> Int Source #

isBoolean :: (a, b, c, d, e, f) -> Bool Source #

isBounded :: (a, b, c, d, e, f) -> Bool Source #

isReal :: (a, b, c, d, e, f) -> Bool Source #

isFloat :: (a, b, c, d, e, f) -> Bool Source #

isDouble :: (a, b, c, d, e, f) -> Bool Source #

isUnbounded :: (a, b, c, d, e, f) -> Bool Source #

isUninterpreted :: (a, b, c, d, e, f) -> Bool Source #

isChar :: (a, b, c, d, e, f) -> Bool Source #

isString :: (a, b, c, d, e, f) -> Bool Source #

isList :: (a, b, c, d, e, f) -> Bool Source #

isSet :: (a, b, c, d, e, f) -> Bool Source #

isTuple :: (a, b, c, d, e, f) -> Bool Source #

isMaybe :: (a, b, c, d, e, f) -> Bool Source #

isEither :: (a, b, c, d, e, f) -> Bool Source #

showType :: (a, b, c, d, e, f) -> String Source #

(HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g) => HasKind (a, b, c, d, e, f, g) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c, d, e, f, g) -> Kind Source #

hasSign :: (a, b, c, d, e, f, g) -> Bool Source #

intSizeOf :: (a, b, c, d, e, f, g) -> Int Source #

isBoolean :: (a, b, c, d, e, f, g) -> Bool Source #

isBounded :: (a, b, c, d, e, f, g) -> Bool Source #

isReal :: (a, b, c, d, e, f, g) -> Bool Source #

isFloat :: (a, b, c, d, e, f, g) -> Bool Source #

isDouble :: (a, b, c, d, e, f, g) -> Bool Source #

isUnbounded :: (a, b, c, d, e, f, g) -> Bool Source #

isUninterpreted :: (a, b, c, d, e, f, g) -> Bool Source #

isChar :: (a, b, c, d, e, f, g) -> Bool Source #

isString :: (a, b, c, d, e, f, g) -> Bool Source #

isList :: (a, b, c, d, e, f, g) -> Bool Source #

isSet :: (a, b, c, d, e, f, g) -> Bool Source #

isTuple :: (a, b, c, d, e, f, g) -> Bool Source #

isMaybe :: (a, b, c, d, e, f, g) -> Bool Source #

isEither :: (a, b, c, d, e, f, g) -> Bool Source #

showType :: (a, b, c, d, e, f, g) -> String Source #

(HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h) => HasKind (a, b, c, d, e, f, g, h) Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: (a, b, c, d, e, f, g, h) -> Kind Source #

hasSign :: (a, b, c, d, e, f, g, h) -> Bool Source #

intSizeOf :: (a, b, c, d, e, f, g, h) -> Int Source #

isBoolean :: (a, b, c, d, e, f, g, h) -> Bool Source #

isBounded :: (a, b, c, d, e, f, g, h) -> Bool Source #

isReal :: (a, b, c, d, e, f, g, h) -> Bool Source #

isFloat :: (a, b, c, d, e, f, g, h) -> Bool Source #

isDouble :: (a, b, c, d, e, f, g, h) -> Bool Source #

isUnbounded :: (a, b, c, d, e, f, g, h) -> Bool Source #

isUninterpreted :: (a, b, c, d, e, f, g, h) -> Bool Source #

isChar :: (a, b, c, d, e, f, g, h) -> Bool Source #

isString :: (a, b, c, d, e, f, g, h) -> Bool Source #

isList :: (a, b, c, d, e, f, g, h) -> Bool Source #

isSet :: (a, b, c, d, e, f, g, h) -> Bool Source #

isTuple :: (a, b, c, d, e, f, g, h) -> Bool Source #

isMaybe :: (a, b, c, d, e, f, g, h) -> Bool Source #

isEither :: (a, b, c, d, e, f, g, h) -> Bool Source #

showType :: (a, b, c, d, e, f, g, h) -> String Source #

data Kind Source #

Kind of symbolic value

Constructors

KBool |
KBounded !Bool !Int |
KUnbounded |
KReal |
KUninterpreted String (Either String [String]) |
KFloat |
KDouble |
KChar |
KString |
KList Kind |
KSet Kind |
KTuple [Kind] |
KMaybe Kind |
KEither Kind Kind |

#### Instances

Instances details

Eq Kind Source # |
Instance details Defined in Data.SBV.Core.Kind Methods (==) :: Kind -> Kind -> Bool (/=) :: Kind -> Kind -> Bool
Ord Kind Source # |
Instance details Defined in Data.SBV.Core.Kind Methods compare :: Kind -> Kind -> Ordering (<) :: Kind -> Kind -> Bool (<=) :: Kind -> Kind -> Bool (>) :: Kind -> Kind -> Bool (>=) :: Kind -> Kind -> Bool max :: Kind -> Kind -> Kind min :: Kind -> Kind -> Kind
Show Kind Source # | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently ignores the enumeration constructors. Also, when we construct a `KUninterpreted`, we make sure we don't use any of the reserved names; see `constructUKind` for details.
Instance details Defined in Data.SBV.Core.Kind Methods showsPrec :: Int -> Kind -> ShowS show :: Kind -> String showList :: [Kind] -> ShowS
NFData Kind |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: Kind -> ()
HasKind Kind Source # |

Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: Kind -> Kind Source #

hasSign :: Kind -> Bool Source #

intSizeOf :: Kind -> Int Source #

isBoolean :: Kind -> Bool Source #

isBounded :: Kind -> Bool Source #

isReal :: Kind -> Bool Source #

isFloat :: Kind -> Bool Source #

isDouble :: Kind -> Bool Source #

isUnbounded :: Kind -> Bool Source #

isUninterpreted :: Kind -> Bool Source #

isChar :: Kind -> Bool Source #

isString :: Kind -> Bool Source #

isList :: Kind -> Bool Source #

isSet :: Kind -> Bool Source #

isTuple :: Kind -> Bool Source #

isMaybe :: Kind -> Bool Source #

isEither :: Kind -> Bool Source #

showType :: Kind -> String Source #

data CV Source #

`CV` represents a concrete word of a fixed size: For signed words, the most significant digit is considered to be the sign.

Constructors

CV |

Fields

- _cvKind :: !Kind
- cvVal :: !CVal

#### Instances

Instances details

Eq CV Source # |
Instance details Defined in Data.SBV.Core.Concrete Methods (==) :: CV -> CV -> Bool (/=) :: CV -> CV -> Bool
Ord CV Source # |
Instance details Defined in Data.SBV.Core.Concrete Methods compare :: CV -> CV -> Ordering (<) :: CV -> CV -> Bool (<=) :: CV -> CV -> Bool (>) :: CV -> CV -> Bool (>=) :: CV -> CV -> Bool max :: CV -> CV -> CV min :: CV -> CV -> CV
Show CV Source # | Show instance for `CV`.
Instance details Defined in Data.SBV.Core.Concrete Methods showsPrec :: Int -> CV -> ShowS show :: CV -> String showList :: [CV] -> ShowS
NFData CV |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: CV -> ()
HasKind CV Source # | `Kind` instance for CV

Instance details

Defined in Data.SBV.Core.Concrete

Methods

kindOf :: CV -> Kind Source #

hasSign :: CV -> Bool Source #

intSizeOf :: CV -> Int Source #

isBoolean :: CV -> Bool Source #

isBounded :: CV -> Bool Source #

isReal :: CV -> Bool Source #

isFloat :: CV -> Bool Source #

isDouble :: CV -> Bool Source #

isUnbounded :: CV -> Bool Source #

isUninterpreted :: CV -> Bool Source #

isChar :: CV -> Bool Source #

isString :: CV -> Bool Source #

isList :: CV -> Bool Source #

isSet :: CV -> Bool Source #

isTuple :: CV -> Bool Source #

isMaybe :: CV -> Bool Source #

isEither :: CV -> Bool Source #

showType :: CV -> String Source #

PrettyNum CV Source # |
Instance details Defined in Data.SBV.Utils.PrettyNum Methods hexS :: CV -> String Source # binS :: CV -> String Source # hexP :: CV -> String Source # binP :: CV -> String Source # hex :: CV -> String Source # bin :: CV -> String Source #
SatModel CV Source # | `CV` as extracted from a model; trivial definition
Instance details Defined in Data.SBV.SMT.SMT Methods parseCVs :: [CV] -> Maybe (CV, [CV]) Source # cvtModel :: (CV -> Maybe b) -> Maybe (CV, [CV]) -> Maybe (b, [CV]) Source #
SDivisible CV Source # |
Instance details Defined in Data.SBV.Core.Model Methods sQuotRem :: CV -> CV -> (CV, CV) Source # sDivMod :: CV -> CV -> (CV, CV) Source # sQuot :: CV -> CV -> CV Source # sRem :: CV -> CV -> CV Source # sDiv :: CV -> CV -> CV Source # sMod :: CV -> CV -> CV Source #

data CVal Source #

A constant value

Constructors

CAlgReal !AlgReal | Algebraic real
CInteger !Integer | Bit-vector/unbounded integer
CFloat !Float | Float
CDouble !Double | Double
CChar !Char | Character
CString !String | String
CList ![CVal] | List
CSet !(RCSet CVal) | Set. Can be regular or complemented.
CUserSort !(Maybe Int, String) | Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
CTuple ![CVal] | Tuple
CMaybe !(Maybe CVal) | Maybe
CEither !(Either CVal CVal) | Disjoint union

#### Instances

Instances details

Eq CVal Source # | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper instances for these when values are infinitely precise reals. However, we do need a structural eq/ord for Map indexes; so define custom ones here:
Instance details Defined in Data.SBV.Core.Concrete Methods (==) :: CVal -> CVal -> Bool (/=) :: CVal -> CVal -> Bool
Ord CVal Source # | Ord instance for VWVal. Same comments as the `Eq` instance why this cannot be derived.
Instance details Defined in Data.SBV.Core.Concrete Methods compare :: CVal -> CVal -> Ordering (<) :: CVal -> CVal -> Bool (<=) :: CVal -> CVal -> Bool (>) :: CVal -> CVal -> Bool (>=) :: CVal -> CVal -> Bool max :: CVal -> CVal -> CVal min :: CVal -> CVal -> CVal

cvToBool :: CV -> Bool Source #

Convert a CV to a Haskell boolean (NB. Assumes input is well-kinded)

### SMT Arrays of symbolic values

data SArr Source #

Arrays in terms of SMT-Lib arrays

readSArr :: SArr -> SVal -> SVal Source #

Read the array element at `a`

writeSArr :: SArr -> SVal -> SVal -> SArr Source #

Update the element at `a` to be `b`

mergeSArr :: SVal -> SArr -> SArr -> SArr Source #

Merge two given arrays on the symbolic condition Intuitively: `mergeArrays cond a b = if cond then a else b`. Merging pushes the if-then-else choice down on to elements

newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr Source #

Create a named new array

eqSArr :: SArr -> SArr -> SVal Source #

Compare two arrays for equality

### Functional arrays of symbolic values

data SFunArr Source #

Arrays managed internally

readSFunArr :: SFunArr -> SVal -> SVal Source #

Read the array element at `a`. For efficiency purposes, we create a memo-table as we go along, as otherwise we suffer significant performance penalties. See: http://github.com/LeventErkok/sbv/issues/402 and http://github.com/LeventErkok/sbv/issues/396.

writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr Source #

Update the element at `address` to be `b`

mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr Source #

Merge two given arrays on the symbolic condition Intuitively: `mergeArrays cond a b = if cond then a else b`. Merging pushes the if-then-else choice down on to elements

newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr Source #

Create a named new array

## Creating a symbolic variable

type Symbolic = SymbolicT IO Source #

`Symbolic` is specialization of `SymbolicT` to the `IO` monad. Unless you are using transformers explicitly, this is the type you should prefer.

data Quantifier Source #

Quantifiers: forall or exists. Note that we allow arbitrary nestings.

Constructors

ALL |
EX |

#### Instances

Instances details

Eq Quantifier Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods (==) :: Quantifier -> Quantifier -> Bool (/=) :: Quantifier -> Quantifier -> Bool
Show Quantifier Source # | Show instance for `Quantifier`
Instance details Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> Quantifier -> ShowS show :: Quantifier -> String showList :: [Quantifier] -> ShowS
NFData Quantifier Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: Quantifier -> ()

svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal Source #

Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. If not, then we pick the quantifier appropriately based on the run-mode. `randomCV` is used for generating random values for this variable when used for `quickCheck` or `genTest` purposes.

sWordN :: MonadSymbolic m => Int -> String -> m SVal Source #

Generalization of `sWordN`

sWordN_ :: MonadSymbolic m => Int -> m SVal Source #

Generalization of `sWordN_`

sIntN :: MonadSymbolic m => Int -> String -> m SVal Source #

Generalization of `sIntN`

sIntN_ :: MonadSymbolic m => Int -> m SVal Source #

Generalization of `sIntN_`

## Operations on symbolic values

### Boolean literals

svTrue :: SVal Source #

Boolean True.

svFalse :: SVal Source #

Boolean False.

svBool :: Bool -> SVal Source #

Convert from a Boolean.

svAsBool :: SVal -> Maybe Bool Source #

Extract a bool, by properly interpreting the integer stored.

### Integer literals

svInteger :: Kind -> Integer -> SVal Source #

Convert from an Integer.

svAsInteger :: SVal -> Maybe Integer Source #

Extract an integer from a concrete value.

### Float literals

svFloat :: Float -> SVal Source #

Convert from a Float

svDouble :: Double -> SVal Source #

Convert from a Float

### Algebraic reals (only from rationals)

svReal :: Rational -> SVal Source #

Convert from a Rational

svNumerator :: SVal -> Maybe Integer Source #

Grab the numerator of an SReal, if available

svDenominator :: SVal -> Maybe Integer Source #

Grab the denominator of an SReal, if available

### Symbolic equality

svEqual :: SVal -> SVal -> SVal Source #

Equality.

svNotEqual :: SVal -> SVal -> SVal Source #

Inequality.

### Constructing concrete lists

svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal] Source #

Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like `[1, 5 .. 200] :: [SInt8]` work just fine (end evaluate to empty list), since we see `[1, 5 .. -56]` in the `Integer` domain. Also note the explicit check for `s /= f` below to make sure we don't stutter and produce an infinite list.

### Symbolic ordering

svLessThan :: SVal -> SVal -> SVal Source #

Less than.

svGreaterThan :: SVal -> SVal -> SVal Source #

Greater than.

svLessEq :: SVal -> SVal -> SVal Source #

Less than or equal to.

svGreaterEq :: SVal -> SVal -> SVal Source #

Greater than or equal to.

svStructuralLessThan :: SVal -> SVal -> SVal Source #

Given a composite structure, figure out how to compare for less than

### Arithmetic operations

svPlus :: SVal -> SVal -> SVal Source #

Addition.

svTimes :: SVal -> SVal -> SVal Source #

Multiplication.

svMinus :: SVal -> SVal -> SVal Source #

Subtraction.

svUNeg :: SVal -> SVal Source #

Unary minus.

svAbs :: SVal -> SVal Source #

Absolute value.

svDivide :: SVal -> SVal -> SVal Source #

Division.

svQuot :: SVal -> SVal -> SVal Source #

Quotient: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "div" operator (Euclidean division, which always has a non-negative remainder). For unsigned bitvectors, it is "bvudiv"; and for signed bitvectors it is "bvsdiv", which rounds toward zero. Division by 0 is defined s.t. `x/0 = 0`, which holds even when `x` itself is `0`.

svRem :: SVal -> SVal -> SVal Source #

Remainder: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "mod" operator (always non-negative). For unsigned bitvectors, it is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds toward zero (sign of remainder matches that of `x`). Division by 0 is defined s.t. `x/0 = 0`, which holds even when `x` itself is `0`.

svQuotRem :: SVal -> SVal -> (SVal, SVal) Source #

Combination of quot and rem

svExp :: SVal -> SVal -> SVal Source #

Exponentiation.

svAddConstant :: Integral a => SVal -> a -> SVal Source #

Add a constant value:

svIncrement :: SVal -> SVal Source #

Increment:

svDecrement :: SVal -> SVal Source #

Decrement:

### Logical operations

svAnd :: SVal -> SVal -> SVal Source #

Bitwise and.

svOr :: SVal -> SVal -> SVal Source #

Bitwise or.

svXOr :: SVal -> SVal -> SVal Source #

Bitwise xor.

svNot :: SVal -> SVal Source #

Bitwise complement.

svShl :: SVal -> Int -> SVal Source #

Shift left by a constant amount. Translates to the "bvshl" operation in SMT-Lib.

NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.

svShr :: SVal -> Int -> SVal Source #

Shift right by a constant amount. Translates to either "bvlshr" (logical shift right) or "bvashr" (arithmetic shift right) in SMT-Lib, depending on whether `x` is a signed bitvector.

NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.

svRol :: SVal -> Int -> SVal Source #

Rotate-left, by a constant.

NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.

svRor :: SVal -> Int -> SVal Source #

Rotate-right, by a constant.

NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.

### Splitting, joining, and extending

svExtract :: Int -> Int -> SVal -> SVal Source #

Extract bit-sequences.

svJoin :: SVal -> SVal -> SVal Source #

Join two words, by concataneting

### Sign-casting

svSign :: SVal -> SVal Source #

Convert a symbolic bitvector from unsigned to signed.

svUnsign :: SVal -> SVal Source #

Convert a symbolic bitvector from signed to unsigned.

### Numeric conversions

svFromIntegral :: Kind -> SVal -> SVal Source #

Convert a symbolic bitvector from one integral kind to another.

### Indexed lookups

svSelect :: [SVal] -> SVal -> SVal -> SVal Source #

Total indexing operation. `svSelect xs default index` is intuitively the same as `xs !! index`, except it evaluates to `default` if `index` overflows. Translates to SMT-Lib tables.

### Word-level operations

svToWord1 :: SVal -> SVal Source #

Convert an SVal from kind Bool to an unsigned bitvector of size 1.

svFromWord1 :: SVal -> SVal Source #

Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.

svTestBit :: SVal -> Int -> SVal Source #

Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.

svSetBit :: SVal -> Int -> SVal Source #

Set a given bit at index

svShiftLeft :: SVal -> SVal -> SVal Source #

Generalization of `svShl`, where the shift-amount is symbolic.

svShiftRight :: SVal -> SVal -> SVal Source #

Generalization of `svShr`, where the shift-amount is symbolic.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical.

svRotateLeft :: SVal -> SVal -> SVal Source #

Generalization of `svRol`, where the rotation amount is symbolic. If the first argument is not bounded, then the this is the same as shift.

svRotateRight :: SVal -> SVal -> SVal Source #

Generalization of `svRor`, where the rotation amount is symbolic. If the first argument is not bounded, then the this is the same as shift.

svBarrelRotateLeft :: SVal -> SVal -> SVal Source #

A variant of `svRotateLeft` that uses a barrel-rotate design, which can lead to better verification code. Only works when both arguments are finite and the second argument is unsigned.

svBarrelRotateRight :: SVal -> SVal -> SVal Source #

A variant of `svRotateLeft` that uses a barrel-rotate design, which can lead to better verification code. Only works when both arguments are finite and the second argument is unsigned.

svWordFromBE :: [SVal] -> SVal Source #

Un-bit-blast from little-endian representation to a word of the right size. The input is assumed to be unsigned.

svWordFromLE :: [SVal] -> SVal Source #

Un-bit-blast from big-endian representation to a word of the right size. The input is assumed to be unsigned.

svBlastLE :: SVal -> [SVal] Source #

Bit-blast: Little-endian. Assumes the input is a bit-vector.

svBlastBE :: SVal -> [SVal] Source #

Bit-blast: Big-endian. Assumes the input is a bit-vector.

## Conditionals: Mergeable values

svIte :: SVal -> SVal -> SVal -> SVal Source #

If-then-else. This one will force branches.

svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal Source #

Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.

svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal Source #

Merge two symbolic values, at kind `k`, possibly `force`'ing the branches to make sure they do not evaluate to the same result.

# Uninterpreted sorts, constants, and functions

svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal Source #

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.

# Properties, proofs, and satisfiability

## Proving properties

proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult Source #

Proves the predicate using the given SMT-solver

## Checking satisfiability

satWith :: SMTConfig -> Symbolic SVal -> IO SatResult Source #

Find a satisfying assignment using the given SMT-solver

allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult Source #

Find all satisfying assignments using the given SMT-solver

## Checking safety

safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult] Source #

Check safety using the given SMT-solver

# Proving properties using multiple solvers

proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult) Source #

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)] Source #

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult) Source #

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

# Proving properties using multiple threads

proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

Prove a property with query mode using multiple threads. Each query computation will spawn a thread and a unique instance of your solver to run asynchronously. The `Symbolic` `SVal` is duplicated for each thread. This function will block until all child threads return.

proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult) Source #

Prove a property with query mode using multiple threads. Each query computation will spawn a thread and a unique instance of your solver to run asynchronously. The `Symbolic` `SVal` is duplicated for each thread. This function will return the first query computation that completes, killing the others.

satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult) Source #

Find a satisfying assignment to a property with multiple threads in query mode. The `Symbolic` `SVal` represents what is known to all child query threads. Each query thread will spawn a unique instance of the solver. Only the first one to finish will be returned and the other threads will be killed.

satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)] Source #

Find a satisfying assignment to a property with multiple threads in query mode. The `Symbolic` `SVal` represents what is known to all child query threads. Each query thread will spawn a unique instance of the solver. This function will block until all child threads have completed.

# Quick-check

svQuickCheck :: Symbolic SVal -> IO Bool Source #

Dynamic variant of quick-check

# Model extraction

## Inspecting proof results

newtype ThmResult Source #

A `prove` call results in a `ThmResult`

Constructors

ThmResult SMTResult |

#### Instances

Instances details

Show ThmResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> ThmResult -> ShowS show :: ThmResult -> String showList :: [ThmResult] -> ShowS
NFData ThmResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods rnf :: ThmResult -> ()
Modelable ThmResult Source # | `ThmResult` as a generic model provider

Instance details

Defined in Data.SBV.SMT.SMT

Methods

modelExists :: ThmResult -> Bool Source #

getModelAssignment :: SatModel b => ThmResult -> Either String (Bool, b) Source #

getModelDictionary :: ThmResult -> Map String CV Source #

getModelValue :: SymVal b => String -> ThmResult -> Maybe b Source #

getModelUninterpretedValue :: String -> ThmResult -> Maybe String Source #

extractModel :: SatModel b => ThmResult -> Maybe b Source #

getModelObjectives :: ThmResult -> Map String GeneralizedCV Source #

getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCV Source #

getModelUIFuns :: ThmResult -> Map String (SBVType, ([([CV], CV)], CV)) Source #

getModelUIFunValue :: String -> ThmResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source #

newtype SatResult Source #

A `sat` call results in a `SatResult` The reason for having a separate `SatResult` is to have a more meaningful `Show` instance.

Constructors

SatResult SMTResult |

#### Instances

Instances details

Show SatResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> SatResult -> ShowS show :: SatResult -> String showList :: [SatResult] -> ShowS
NFData SatResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods rnf :: SatResult -> ()
Modelable SatResult Source # | `SatResult` as a generic model provider

Instance details

Defined in Data.SBV.SMT.SMT

Methods

modelExists :: SatResult -> Bool Source #

getModelAssignment :: SatModel b => SatResult -> Either String (Bool, b) Source #

getModelDictionary :: SatResult -> Map String CV Source #

getModelValue :: SymVal b => String -> SatResult -> Maybe b Source #

getModelUninterpretedValue :: String -> SatResult -> Maybe String Source #

extractModel :: SatModel b => SatResult -> Maybe b Source #

getModelObjectives :: SatResult -> Map String GeneralizedCV Source #

getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCV Source #

getModelUIFuns :: SatResult -> Map String (SBVType, ([([CV], CV)], CV)) Source #

getModelUIFunValue :: String -> SatResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source #

newtype AllSatResult Source #

An `allSat` call results in a `AllSatResult`. The first boolean says whether we hit the max-model limit as we searched. The second boolean says whether there were prefix-existentials. The third boolean says whether we stopped because the solver returned `Unknown`.

Constructors

AllSatResult (Bool, Bool, Bool, [SMTResult]) |

#### Instances

Instances details

Show AllSatResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> AllSatResult -> ShowS show :: AllSatResult -> String showList :: [AllSatResult] -> ShowS

newtype SafeResult Source #

A `safe` call results in a `SafeResult`

Constructors

SafeResult (Maybe String, String, SMTResult) |

#### Instances

Instances details

Show SafeResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> SafeResult -> ShowS show :: SafeResult -> String showList :: [SafeResult] -> ShowS

data OptimizeResult Source #

An `optimize` call results in a `OptimizeResult`. In the `ParetoResult` case, the boolean is `True` if we reached pareto-query limit and so there might be more unqueried results remaining. If `False`, it means that we have all the pareto fronts returned. See the `Pareto` `OptimizeStyle` for details.

Constructors

LexicographicResult SMTResult |
ParetoResult (Bool, [SMTResult]) |
IndependentResult [(String, SMTResult)] |

#### Instances

Instances details

Show OptimizeResult Source # |
Instance details Defined in Data.SBV.SMT.SMT Methods showsPrec :: Int -> OptimizeResult -> ShowS show :: OptimizeResult -> String showList :: [OptimizeResult] -> ShowS

data SMTResult Source #

The result of an SMT solver call. Each constructor is tagged with the `SMTConfig` that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

Unsatisfiable SMTConfig (Maybe [String]) | Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.
Satisfiable SMTConfig SMTModel | Satisfiable with model
SatExtField SMTConfig SMTModel | Prover returned a model, but in an extension field containing Infinite/epsilon
Unknown SMTConfig SMTReasonUnknown | Prover returned unknown, with the given reason
ProofError SMTConfig [String] (Maybe SMTResult) | Prover errored out, with possibly a bogus result

#### Instances

Instances details

NFData SMTResult Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: SMTResult -> ()
Modelable SMTResult Source # | `SMTResult` as a generic model provider

Instance details

Defined in Data.SBV.SMT.SMT

Methods

modelExists :: SMTResult -> Bool Source #

getModelAssignment :: SatModel b => SMTResult -> Either String (Bool, b) Source #

getModelDictionary :: SMTResult -> Map String CV Source #

getModelValue :: SymVal b => String -> SMTResult -> Maybe b Source #

getModelUninterpretedValue :: String -> SMTResult -> Maybe String Source #

extractModel :: SatModel b => SMTResult -> Maybe b Source #

getModelObjectives :: SMTResult -> Map String GeneralizedCV Source #

getModelObjectiveValue :: String -> SMTResult -> Maybe GeneralizedCV Source #

getModelUIFuns :: SMTResult -> Map String (SBVType, ([([CV], CV)], CV)) Source #

getModelUIFunValue :: String -> SMTResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source #

## Programmable model extraction

genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV]) Source #

Parse a signed/sized value from a sequence of CVs

getModelAssignment :: SMTResult -> Either String (Bool, [CV]) Source #

Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)

getModelDictionary :: SMTResult -> Map String CV Source #

Extract a model dictionary. Extract a dictionary mapping the variables to their respective values as returned by the SMT solver. Also see `getModelDictionaries`.

# SMT Interface: Configurations and solvers

data SMTConfig Source #

Solver configuration. See also `z3`, `yices`, `cvc4`, `boolector`, `mathSAT`, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as `z3{verbose=True}`.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field `printRealPrec` controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix `...` at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

The `printBase` field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.

Constructors

SMTConfig |

Fields

- verbose :: Bool

  Debug mode

- timing :: Timing

  Print timing information on how long different phases took (construction, solving, etc.)

- printBase :: Int

  Print integral literals in this base (2, 10, and 16 are supported.)

- printRealPrec :: Int

  Print algebraic real values with this precision. (SReal, default: 16)

- satCmd :: String

  Usually "(check-sat)". However, users might tweak it based on solver characteristics.

- allSatMaxModelCount :: Maybe Int

  In a `allSat` call, return at most this many models. If nothing, return all.

- allSatPrintAlong :: Bool

  In a `allSat` call, print models as they are found.

- satTrackUFs :: Bool

  In a `sat` call, should we try to extract values of uninterpreted functions?

- isNonModelVar :: String -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

- validateModel :: Bool

  If set, SBV will attempt to validate the model it gets back from the solver.

- optimizeValidateConstraints :: Bool

  Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.

- transcript :: Maybe FilePath

  If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)

- smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

- solver :: SMTSolver

  The actual SMT solver.

- allowQuantifiedQueries :: Bool

  Should we permit use of quantifiers in the query mode? (Default: False. See http://github.com/LeventErkok/sbv/issues/459 for why.)

- roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

- solverSetOptions :: [SMTOption]

  Options to set as we start the solver

- ignoreExitCode :: Bool

  If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.

- redirectVerbose :: Maybe FilePath

  Redirect the verbose output to this file if given. If Nothing, stdout is implied.

#### Instances

Instances details

NFData SMTConfig Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: SMTConfig -> ()

data SMTLibVersion Source #

Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.

Constructors

SMTLib2 |

#### Instances

Instances details

Bounded SMTLibVersion Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods minBound :: SMTLibVersion maxBound :: SMTLibVersion
Enum SMTLibVersion Source # |

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

succ :: SMTLibVersion -> SMTLibVersion

pred :: SMTLibVersion -> SMTLibVersion

toEnum :: Int -> SMTLibVersion

fromEnum :: SMTLibVersion -> Int

enumFrom :: SMTLibVersion -> [SMTLibVersion]

enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

Eq SMTLibVersion Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods (==) :: SMTLibVersion -> SMTLibVersion -> Bool (/=) :: SMTLibVersion -> SMTLibVersion -> Bool
Show SMTLibVersion Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> SMTLibVersion -> ShowS show :: SMTLibVersion -> String showList :: [SMTLibVersion] -> ShowS
NFData SMTLibVersion Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods rnf :: SMTLibVersion -> ()

data Solver Source #

Solvers that SBV is aware of

Constructors

Z3 |
Yices |
Boolector |
CVC4 |
MathSAT |
ABC |

#### Instances

Instances details

Bounded Solver Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods minBound :: Solver maxBound :: Solver
Enum Solver Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods succ :: Solver -> Solver pred :: Solver -> Solver toEnum :: Int -> Solver fromEnum :: Solver -> Int enumFrom :: Solver -> [Solver] enumFromThen :: Solver -> Solver -> [Solver] enumFromTo :: Solver -> Solver -> [Solver] enumFromThenTo :: Solver -> Solver -> Solver -> [Solver]
Show Solver Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> Solver -> ShowS show :: Solver -> String showList :: [Solver] -> ShowS

data SMTSolver Source #

An SMT solver

Constructors

SMTSolver |

Fields

- name :: Solver

  The solver in use

- executable :: String

  The path to its executable

- preprocess :: String -> String

  Each line sent to the solver will be passed through this function (typically id)

- options :: SMTConfig -> [String]

  Options to provide to the solver

- engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

- capabilities :: SolverCapabilities

  Various capabilities of the solver

boolector :: SMTConfig Source #

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig Source #

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig Source #

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig Source #

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig Source #

Default configuration for the MathSAT SMT solver

abc :: SMTConfig Source #

Default configuration for the ABC synthesis and verification tool.

defaultSolverConfig :: Solver -> SMTConfig Source #

The default configs corresponding to supported SMT solvers

defaultSMTCfg :: SMTConfig Source #

The default solver used by SBV. This is currently set to z3.

sbvCheckSolverInstallation :: SMTConfig -> IO Bool Source #

Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.

sbvAvailableSolvers :: IO [SMTConfig] Source #

Return the known available solver configs, installed on your machine.

# Symbolic computations

outputSVal :: MonadSymbolic m => SVal -> m () Source #

Generalization of `outputSVal`

# Code generation from symbolic programs

data SBVCodeGen a Source #

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

#### Instances

Instances details

Monad SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods (>>=) :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b (>>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b return :: a -> SBVCodeGen a
Functor SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b (<$) :: a -> SBVCodeGen b -> SBVCodeGen a
MonadFail SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods fail :: String -> SBVCodeGen a
Applicative SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods pure :: a -> SBVCodeGen a (<*>) :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c (*>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b (<*) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
MonadIO SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods liftIO :: IO a -> SBVCodeGen a
MonadSymbolic SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods symbolicEnv :: SBVCodeGen State Source #
MonadState CgState SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods get :: SBVCodeGen CgState put :: CgState -> SBVCodeGen () state :: (CgState -> (a, CgState)) -> SBVCodeGen a

## Setting code-generation options

cgPerformRTCs :: Bool -> SBVCodeGen () Source #

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: `False`.

cgSetDriverValues :: [Integer] -> SBVCodeGen () Source #

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgGenerateDriver :: Bool -> SBVCodeGen () Source #

Should we generate a driver program? Default: `True`. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See `compileToCLib`.)

cgGenerateMakefile :: Bool -> SBVCodeGen () Source #

Should we generate a Makefile? Default: `True`.

## Designating inputs

svCgInput :: Kind -> String -> SBVCodeGen SVal Source #

Creates an atomic input in the generated code.

svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] Source #

Creates an array input in the generated code.

## Designating outputs

svCgOutput :: String -> SVal -> SBVCodeGen () Source #

Creates an atomic output in the generated code.

svCgOutputArr :: String -> [SVal] -> SBVCodeGen () Source #

Creates an array output in the generated code.

## Designating return values

svCgReturn :: SVal -> SBVCodeGen () Source #

Creates a returned (unnamed) value in the generated code.

svCgReturnArr :: [SVal] -> SBVCodeGen () Source #

Creates a returned (unnamed) array value in the generated code.

## Code generation with uninterpreted functions

cgAddPrototype :: [String] -> SBVCodeGen () Source #

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () Source #

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () Source #

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

cgIgnoreSAssert :: Bool -> SBVCodeGen () Source #

Ignore assertions (those generated by `sAssert` calls) in the generated C code

## Code generation with `SInteger` and `SReal` types

cgIntegerSize :: Int -> SBVCodeGen () Source #

Sets number of bits to be used for representing the `SInteger` type in the generated C code. The argument must be one of `8`, `16`, `32`, or `64`. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () Source #

Sets the C type to be used for representing the `SReal` type in the generated C code. The setting can be one of C's `"float"`, `"double"`, or `"long double"`, types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType Source #

Possible mappings for the `SReal` type when translated to C. Used in conjunction with the function `cgSRealType`. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat

    float

CgDouble

    double

CgLongDouble

    long double

#### Instances

Instances details

Eq CgSRealType Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods (==) :: CgSRealType -> CgSRealType -> Bool (/=) :: CgSRealType -> CgSRealType -> Bool
Show CgSRealType Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods showsPrec :: Int -> CgSRealType -> ShowS show :: CgSRealType -> String showList :: [CgSRealType] -> ShowS

## Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a Source #

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the C function to generate.
- The final argument is the function to be compiled.

Compilation will also generate a `Makefile`, a header file, and a driver (test) program, etc. As a result, we return whatever the code-gen function returns. Most uses should simply have `()` as the return type here, but the value can be useful if you want to chain the result of one compilation act to the next.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a] Source #

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the archive to generate.
- The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of `compileToC`, except in a list.

## Compilation to SMTLib

generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String Source #

Create SMT-Lib benchmarks. The first argument is the basename of the file, we will automatically add ".smt2" per SMT-Lib2 convention. The `Bool` argument controls whether this is a SAT instance, i.e., translate the query directly, or a PROVE instance, i.e., translate the negated query.