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

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

Data.SBV

Contents

- Programming with symbolic values
  - Symbolic types
    - Symbolic bit
    - Unsigned symbolic bit-vectors
    - Signed symbolic bit-vectors
    - Signed unbounded integers
    - IEEE-floating point numbers
      - Rounding modes
      - Bit-pattern conversions
    - Signed algebraic reals
  - Creating a symbolic variable
  - Creating a list of symbolic variables
    - Abstract SBV type
    - Arrays of symbolic values
    - Full binary trees
  - Operations on symbolic values
    - Word level
    - Predicates
    - Addition and Multiplication with high-bits
    - Exponentiation
    - Blasting/Unblasting
    - Splitting, joining, and extending
  - Polynomial arithmetic and CRCs
  - Conditionals: Mergeable values
  - Symbolic equality
  - Symbolic ordering
  - Symbolic integral numbers
  - Division
  - The Boolean class
    - Generalizations of boolean operations
  - Pretty-printing and reading numbers in Hex & Binary
- Checking satisfiability in path conditions
- Uninterpreted sorts, constants, and functions
- Enumerations
- Properties, proofs, satisfiability, and safety
  - Predicates
  - Proving properties
  - Checking satisfiability
  - Checking safety
  - Finding all satisfying assignments
  - Satisfying a sequence of boolean conditions
  - Adding constraints
  - Checking constraint vacuity
  - Quick-checking
- Proving properties using multiple solvers
- Optimization
- Computing expected values
- Model extraction
  - Inspecting proof results
  - Programmable model extraction
- SMT Interface: Configurations and solvers
- Symbolic computations
- Getting SMT-Lib output (for offline analysis)
- Test case generation
- 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
- Module exports

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: SMT Based Verification

Express properties about Haskell programs and automatically prove them using SMT solvers.

    >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
    Q.E.D.

    >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
    Falsifiable. Counter-example:
      s0 = 32 :: Word8

The function `prove` has the following type:

        prove :: Provable a => a -> IO ThmResult

The class `Provable` comes with instances for n-ary predicates, for arbitrary n. The predicates are just regular Haskell functions over symbolic types listed below. Functions for checking satisfiability (`sat` and `allSat`) are also provided.

The sbv library introduces the following symbolic types:

- `SBool`: Symbolic Booleans (bits).
- `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned).
- `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed).
- `SInteger`: Unbounded signed integers.
- `SReal`: Algebraic-real numbers
- `SFloat`: IEEE-754 single-precision floating point values
- `SDouble`: IEEE-754 double-precision floating point values
- `SArray`, `SFunArray`: Flat arrays of symbolic values.
- Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
- Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
- Uninterpreted sorts, and proofs over such sorts, potentially with axioms.

The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the standard classes `Num`, `Bits`, custom versions of `Eq` (`EqSymbolic`) and `Ord` (`OrdSymbolic`), along with several other custom classes for simplifying programming with symbolic values. The framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return `SBool`) built out of these types can also be:

- proven correct via an external SMT solver (the `prove` function)
- checked for satisfiability (the `sat`, `allSat` functions)
- used in synthesis (the `sat` function with existentials)
- quick-checked

If a predicate is not valid, `prove` will return a counterexample: An assignment to inputs such that the predicate fails. The `sat` function will return a satisfying assignment, if there is one. The `allSat` function returns all satisfying assignments, lazily.

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://smtlib.cs.uiowa.edu/

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the following SMT-Solvers out-of-the box:

- ABC from University of Berkeley: http://www.eecs.berkeley.edu/~alanmi/abc/
- CVC4 from New York University and University of Iowa: http://cvc4.cs.nyu.edu/
- Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
- MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
- Yices from SRI: http://yices.csl.sri.com/
- Z3 from Microsoft: http://github.com/Z3Prover/z3/wiki

SBV also allows calling these solvers in parallel, either getting results from multiple solvers or returning the fastest one. (See `proveWithAll`, `proveWithAny`, etc.)

Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.

Synopsis

- type SBool = SBV Bool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInteger = SBV Integer
- type SFloat = SBV Float
- type SDouble = SBV Double
- class (SymWord a, RealFloat a) => IEEEFloating a where
- class IEEEFloatConvertable a where
- data RoundingMode
  - = RoundNearestTiesToEven
  - | RoundNearestTiesToAway
  - | RoundTowardPositive
  - | RoundTowardNegative
  - | RoundTowardZero
- type SRoundingMode = SBV RoundingMode
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymWord a) => SBV a
- sInfinity :: (Floating a, SymWord a) => SBV a
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- sFloatAsSWord32 :: SFloat -> SWord32
- sWord32AsSFloat :: SWord32 -> SFloat
- sDoubleAsSWord64 :: SDouble -> SWord64
- sWord64AsSDouble :: SWord64 -> SDouble
- blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
- blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSInteger :: SReal -> SInteger
- sBool :: String -> Symbolic SBool
- sWord8 :: String -> Symbolic SWord8
- sWord16 :: String -> Symbolic SWord16
- sWord32 :: String -> Symbolic SWord32
- sWord64 :: String -> Symbolic SWord64
- sInt8 :: String -> Symbolic SInt8
- sInt16 :: String -> Symbolic SInt16
- sInt32 :: String -> Symbolic SInt32
- sInt64 :: String -> Symbolic SInt64
- sInteger :: String -> Symbolic SInteger
- sReal :: String -> Symbolic SReal
- sFloat :: String -> Symbolic SFloat
- sDouble :: String -> Symbolic SDouble
- sBools :: [String] -> Symbolic [SBool]
- sWord8s :: [String] -> Symbolic [SWord8]
- sWord16s :: [String] -> Symbolic [SWord16]
- sWord32s :: [String] -> Symbolic [SWord32]
- sWord64s :: [String] -> Symbolic [SWord64]
- sInt8s :: [String] -> Symbolic [SInt8]
- sInt16s :: [String] -> Symbolic [SInt16]
- sInt32s :: [String] -> Symbolic [SInt32]
- sInt64s :: [String] -> Symbolic [SInt64]
- sIntegers :: [String] -> Symbolic [SInteger]
- sReals :: [String] -> Symbolic [SReal]
- sFloats :: [String] -> Symbolic [SFloat]
- sDoubles :: [String] -> Symbolic [SDouble]
- data SBV a
- class SymArray array where
- data SArray a b
- data SFunArray a b
- mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
- type STree i e = STreeInternal (SBV i) (SBV e)
- readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e
- writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e
- mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e
- sTestBit :: SBV a -> Int -> SBool
- sExtractBits :: SBV a -> [Int] -> [SBool]
- sPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8
- sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
- sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
- sSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b
- setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
- oneIf :: (Num a, SymWord a) => SBool -> SBV a
- lsb :: SBV a -> SBool
- msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool
- label :: SymWord a => String -> SBV a -> SBV a
- allEqual :: EqSymbolic a => [a] -> SBool
- allDifferent :: EqSymbolic a => [a] -> SBool
- inRange :: OrdSymbolic a => a -> (a, a) -> SBool
- sElem :: EqSymbolic a => a -> [a] -> SBool
- fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a)
- fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)
- (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
- blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
- blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
- class FromBits a where
- class Splittable a b | b -> a where
- class (Num a, Bits a) => Polynomial a where
- crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
- crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
- class Mergeable a where
- ite :: Mergeable a => SBool -> a -> a -> a
- iteLazy :: Mergeable a => SBool -> a -> a -> a
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class (SymWord a, Num a, Bits a) => SIntegral a
- class SDivisible a where
- class Boolean b where
- bAnd :: Boolean b => [b] -> b
- bOr :: Boolean b => [b] -> b
- bAny :: Boolean b => (a -> b) -> [a] -> b
- bAll :: Boolean b => (a -> b) -> [a] -> b
- class PrettyNum a where
- readBin :: Num a => String -> a
- isSatisfiableInCurrentPath :: SBool -> Symbolic Bool
- class Uninterpreted a where
- addAxiom :: String -> [String] -> Symbolic ()
- type Predicate = Symbolic SBool
- class Provable a where
- class Equality a where
- prove :: Provable a => a -> IO ThmResult
- proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
- isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- isTheoremWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)
- sat :: Provable a => a -> IO SatResult
- satWith :: Provable a => SMTConfig -> a -> IO SatResult
- isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
- isSatisfiableWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)
- sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a
- safe :: SExecutable a => a -> IO [SafeResult]
- safeWith :: SExecutable a => SMTConfig -> a -> IO [SafeResult]
- isSafe :: SafeResult -> Bool
- class SExecutable a where
- allSat :: Provable a => a -> IO AllSatResult
- allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
- solve :: [SBool] -> Symbolic SBool
- constrain :: SBool -> Symbolic ()
- pConstrain :: Double -> SBool -> Symbolic ()
- isVacuous :: Provable a => a -> IO Bool
- isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
- sbvQuickCheck :: Symbolic SBool -> IO Bool
- proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)]
- proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult)
- satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)]
- satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult)
- minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
- expectedValue :: Outputtable a => Symbolic a -> IO [Double]
- expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- newtype AllSatResult = AllSatResult (Bool, [SMTResult])
- data SMTResult
  - = Unsatisfiable SMTConfig
  - | Satisfiable SMTConfig SMTModel
  - | Unknown SMTConfig SMTModel
  - | ProofError SMTConfig [String]
  - | TimeOut SMTConfig
- class SatModel a where
- class Modelable a where
- displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
- extractModels :: SatModel a => AllSatResult -> [a]
- getModelDictionaries :: AllSatResult -> [Map String CW]
- getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
- getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
- data SMTConfig = SMTConfig {
  - verbose :: Bool
  - timing :: Bool
  - sBranchTimeOut :: Maybe Int
  - timeOut :: Maybe Int
  - printBase :: Int
  - printRealPrec :: Int
  - solverTweaks :: [String]
  - satCmd :: String
  - isNonModelVar :: String -> Bool
  - smtFile :: Maybe FilePath
  - smtLibVersion :: SMTLibVersion
  - solver :: SMTSolver
  - roundingMode :: RoundingMode
  - useLogic :: Maybe Logic
  }
- data SMTLibVersion = SMTLib2
- data SMTLibLogic
  - = AUFLIA
  - | AUFLIRA
  - | AUFNIRA
  - | LRA
  - | QF_ABV
  - | QF_AUFBV
  - | QF_AUFLIA
  - | QF_AX
  - | QF_BV
  - | QF_IDL
  - | QF_LIA
  - | QF_LRA
  - | QF_NIA
  - | QF_NRA
  - | QF_RDL
  - | QF_UF
  - | QF_UFBV
  - | QF_UFIDL
  - | QF_UFLIA
  - | QF_UFLRA
  - | QF_UFNRA
  - | UFLRA
  - | UFNIA
  - | QF_FPBV
  - | QF_FP
- data Logic
  - = PredefinedLogic SMTLibLogic
  - | CustomLogic String
- data OptimizeOpts
  - = Iterative Bool
  - | Quantified
- data Solver
  - = Z3
  - | Yices
  - | Boolector
  - | CVC4
  - | MathSAT
  - | ABC
- data SMTSolver = SMTSolver {
  - name :: Solver
  - executable :: String
  - options :: [String]
  - engine :: SMTEngine
  - capabilities :: SolverCapabilities
  }
- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- sbvCurrentSolver :: SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- data Symbolic a
- output :: Outputtable a => a -> Symbolic a
- class (HasKind a, Ord a) => SymWord a where
- compileToSMTLib :: Provable a => SMTLibVersion -> Bool -> a -> IO String
- generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()
- genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors
- getTestValues :: TestVectors -> [([CW], [CW])]
- data TestVectors
- data TestStyle
  - = Haskell String
  - | C String
  - | Forte String Bool ([Int], [Int])
- renderTest :: TestStyle -> TestVectors -> String
- data CW = CW {
  - _cwKind :: !Kind
  - cwVal :: !CWVal
  }
- class HasKind a where
- data Kind
  - = KBool
  - | KBounded !Bool !Int
  - | KUnbounded
  - | KReal
  - | KUserSort String (Either String [String])
  - | KFloat
  - | KDouble
- cwToBool :: CW -> Bool
- data SBVCodeGen a
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
- cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]
- cgOutput :: String -> SBV a -> SBVCodeGen ()
- cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()
- cgReturn :: SBV a -> SBVCodeGen ()
- cgReturnArr :: SymWord a => [SBV a] -> 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 () -> IO ()
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
- module Data.Bits
- module Data.Word
- module Data.Int
- module Data.Ratio

# Programming with symbolic values

The SBV library is really two things:

- A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
- A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a seamless experience, i.e., let people program in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the `Num` and `Bits` classes simplify coding), it makes life harder in others. For instance, `if-then-else` only takes `Bool` as a test in Haskell, and comparisons (`>` etc.) only return `Bool`s. Clearly we would like these values to be symbolic (i.e., `SBool`), thus stopping us from using some native Haskell constructs. When symbolic versions of operators are needed, they are typically obtained by prepending a dot, for instance `==` becomes `.==`. Care has been taken to make the transition painless. In particular, any Haskell program you build out of symbolic components is fully concretely executable within Haskell, without the need for any custom interpreters. (They are truly Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated feel of the system, one of the original design goals for SBV.

## Symbolic types

### Symbolic bit

type SBool = SBV Bool Source #

A symbolic boolean/bit

### Unsigned symbolic bit-vectors

type SWord8 = SBV Word8 Source #

8-bit unsigned symbolic value

type SWord16 = SBV Word16 Source #

16-bit unsigned symbolic value

type SWord32 = SBV Word32 Source #

32-bit unsigned symbolic value

type SWord64 = SBV Word64 Source #

64-bit unsigned symbolic value

### Signed symbolic bit-vectors

type SInt8 = SBV Int8 Source #

8-bit signed symbolic value, 2's complement representation

type SInt16 = SBV Int16 Source #

16-bit signed symbolic value, 2's complement representation

type SInt32 = SBV Int32 Source #

32-bit signed symbolic value, 2's complement representation

type SInt64 = SBV Int64 Source #

64-bit signed symbolic value, 2's complement representation

### Signed unbounded integers

The SBV library supports unbounded signed integers with the type `SInteger`, which are not subject to overflow/underflow as it is the case with the bounded types, such as `SWord8`, `SInt16`, etc. However, some bit-vector based operations are not supported for the `SInteger` type while in the verification mode. That is, you can use these operations on `SInteger` values during normal programming/simulation. but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are:

- Rotations and shifts: `rotateL`, `rotateR`, `shiftL`, `shiftR`
- Bitwise logical ops: `.&.`, `.|.`, `xor`, `complement`
- Extraction and concatenation: `split`, `#`, and `extend` (see the `Splittable` class)

Usual arithmetic (`+`, `-`, `*`, `sQuotRem`, `sQuot`, `sRem`, `sDivMod`, `sDiv`, `sMod`) and logical operations (`.<`, `.<=`, `.>`, `.>=`, `.==`, `./=`) operations are supported for `SInteger` fully, both in programming and verification modes.

type SInteger = SBV Integer Source #

Infinite precision signed symbolic value

### IEEE-floating point numbers

Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's `Float` and `Double` types. For SMT support with floating-point numbers, see the paper by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.

type SFloat = SBV Float Source #

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double Source #

IEEE-754 double-precision floating point numbers

class (SymWord a, RealFloat a) => IEEEFloating a where Source #

A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.

Methods

fpAbs :: SBV a -> SBV a Source #

Compute the floating point absolute value.

fpNeg :: SBV a -> SBV a Source #

Compute the unary negation. Note that `0 - x` is not equivalent to `-x` for floating-point, since `-0` and `0` are different.

fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Add two floating point values, using the given rounding mode

fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Subtract two floating point values, using the given rounding mode

fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Multiply two floating point values, using the given rounding mode

fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a Source #

Divide two floating point values, using the given rounding mode

fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a Source #

Fused-multiply-add three floating point values, using the given rounding mode. `fpFMA x y z = x*y+z` but with only one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since Haskell lacks an FMA implementation.

fpSqrt :: SRoundingMode -> SBV a -> SBV a Source #

Compute the square-root of a float, using the given rounding mode

fpRem :: SBV a -> SBV a -> SBV a Source #

Compute the remainder: `x - y * n`, where `n` is the truncated integer nearest to x/y. The rounding mode is implicitly assumed to be `RoundNearestTiesToEven`.

fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a Source #

Round to the nearest integral value, using the given rounding mode.

fpMin :: SBV a -> SBV a -> SBV a Source #

Compute the minimum of two floats, respects `infinity` and `NaN` values

fpMax :: SBV a -> SBV a -> SBV a Source #

Compute the maximum of two floats, respects `infinity` and `NaN` values

fpIsEqualObject :: SBV a -> SBV a -> SBool Source #

Are the two given floats exactly the same. That is, `NaN` will compare equal to itself, `+0` will not compare equal to `-0` etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use `.==`.)

fpIsNormal :: SBV a -> SBool Source #

Is the floating-point number a normal value. (i.e., not denormalized.)

fpIsSubnormal :: SBV a -> SBool Source #

Is the floating-point number a subnormal value. (Also known as denormal.)

fpIsZero :: SBV a -> SBool Source #

Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)

fpIsInfinite :: SBV a -> SBool Source #

Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)

fpIsNaN :: SBV a -> SBool Source #

Is the floating-point number a NaN value?

fpIsNegative :: SBV a -> SBool Source #

Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.

fpIsPositive :: SBV a -> SBool Source #

Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.

fpIsNegativeZero :: SBV a -> SBool Source #

Is the floating point number -0?

fpIsPositiveZero :: SBV a -> SBool Source #

Is the floating point number +0?

fpIsPoint :: SBV a -> SBool Source #

Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.

Instances

IEEEFloating Double Source # | SDouble instance

Methods

fpAbs :: SBV Double -> SBV Double Source #

fpNeg :: SBV Double -> SBV Double Source #

fpAdd :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source #

fpSub :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source #

fpMul :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source #

fpDiv :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double Source #

fpFMA :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double -> SBV Double Source #

fpSqrt :: SRoundingMode -> SBV Double -> SBV Double Source #

fpRem :: SBV Double -> SBV Double -> SBV Double Source #

fpRoundToIntegral :: SRoundingMode -> SBV Double -> SBV Double Source #

fpMin :: SBV Double -> SBV Double -> SBV Double Source #

fpMax :: SBV Double -> SBV Double -> SBV Double Source #

fpIsEqualObject :: SBV Double -> SBV Double -> SBool Source #

fpIsNormal :: SBV Double -> SBool Source #

fpIsSubnormal :: SBV Double -> SBool Source #

fpIsZero :: SBV Double -> SBool Source #

fpIsInfinite :: SBV Double -> SBool Source #

fpIsNaN :: SBV Double -> SBool Source #

fpIsNegative :: SBV Double -> SBool Source #

fpIsPositive :: SBV Double -> SBool Source #

fpIsNegativeZero :: SBV Double -> SBool Source #

fpIsPositiveZero :: SBV Double -> SBool Source #

fpIsPoint :: SBV Double -> SBool Source #

IEEEFloating Float Source # | SFloat instance

Methods

fpAbs :: SBV Float -> SBV Float Source #

fpNeg :: SBV Float -> SBV Float Source #

fpAdd :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source #

fpSub :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source #

fpMul :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source #

fpDiv :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float Source #

fpFMA :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float -> SBV Float Source #

fpSqrt :: SRoundingMode -> SBV Float -> SBV Float Source #

fpRem :: SBV Float -> SBV Float -> SBV Float Source #

fpRoundToIntegral :: SRoundingMode -> SBV Float -> SBV Float Source #

fpMin :: SBV Float -> SBV Float -> SBV Float Source #

fpMax :: SBV Float -> SBV Float -> SBV Float Source #

fpIsEqualObject :: SBV Float -> SBV Float -> SBool Source #

fpIsNormal :: SBV Float -> SBool Source #

fpIsSubnormal :: SBV Float -> SBool Source #

fpIsZero :: SBV Float -> SBool Source #

fpIsInfinite :: SBV Float -> SBool Source #

fpIsNaN :: SBV Float -> SBool Source #

fpIsNegative :: SBV Float -> SBool Source #

fpIsPositive :: SBV Float -> SBool Source #

fpIsNegativeZero :: SBV Float -> SBool Source #

fpIsPositiveZero :: SBV Float -> SBool Source #

fpIsPoint :: SBV Float -> SBool Source #

class IEEEFloatConvertable a where Source #

Capture convertability from/to FloatingPoint representations NB. `fromSFloat` and `fromSDouble` are underspecified when given when given a `NaN`, `+oo`, or `-oo` value that cannot be represented in the target domain. For these inputs, we define the result to be +0, arbitrarily.

Minimal complete definition

fromSFloat, toSFloat, fromSDouble, toSDouble

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV a Source #

toSFloat :: SRoundingMode -> SBV a -> SFloat Source #

fromSDouble :: SRoundingMode -> SDouble -> SBV a Source #

toSDouble :: SRoundingMode -> SBV a -> SDouble Source #

Instances

IEEEFloatConvertable Double Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Double Source # toSFloat :: SRoundingMode -> SBV Double -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Double Source # toSDouble :: SRoundingMode -> SBV Double -> SDouble Source #
IEEEFloatConvertable Float Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Float Source # toSFloat :: SRoundingMode -> SBV Float -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Float Source # toSDouble :: SRoundingMode -> SBV Float -> SDouble Source #
IEEEFloatConvertable Int8 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int8 Source # toSFloat :: SRoundingMode -> SBV Int8 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int8 Source # toSDouble :: SRoundingMode -> SBV Int8 -> SDouble Source #
IEEEFloatConvertable Int16 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int16 Source # toSFloat :: SRoundingMode -> SBV Int16 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int16 Source # toSDouble :: SRoundingMode -> SBV Int16 -> SDouble Source #
IEEEFloatConvertable Int32 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int32 Source # toSFloat :: SRoundingMode -> SBV Int32 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int32 Source # toSDouble :: SRoundingMode -> SBV Int32 -> SDouble Source #
IEEEFloatConvertable Int64 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Int64 Source # toSFloat :: SRoundingMode -> SBV Int64 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Int64 Source # toSDouble :: SRoundingMode -> SBV Int64 -> SDouble Source #
IEEEFloatConvertable Integer Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Integer Source # toSFloat :: SRoundingMode -> SBV Integer -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Integer Source # toSDouble :: SRoundingMode -> SBV Integer -> SDouble Source #
IEEEFloatConvertable Word8 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word8 Source # toSFloat :: SRoundingMode -> SBV Word8 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word8 Source # toSDouble :: SRoundingMode -> SBV Word8 -> SDouble Source #
IEEEFloatConvertable Word16 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word16 Source # toSFloat :: SRoundingMode -> SBV Word16 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word16 Source # toSDouble :: SRoundingMode -> SBV Word16 -> SDouble Source #
IEEEFloatConvertable Word32 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word32 Source # toSFloat :: SRoundingMode -> SBV Word32 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word32 Source # toSDouble :: SRoundingMode -> SBV Word32 -> SDouble Source #
IEEEFloatConvertable Word64 Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV Word64 Source # toSFloat :: SRoundingMode -> SBV Word64 -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV Word64 Source # toSDouble :: SRoundingMode -> SBV Word64 -> SDouble Source #
IEEEFloatConvertable AlgReal Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal Source # toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal Source # toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble Source #

data RoundingMode Source #

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is `RoundNearestTiesToEven`. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Constructors

RoundNearestTiesToEven | Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.)
RoundNearestTiesToAway | Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.)
RoundTowardPositive | Round towards positive infinity. (Also known as rounding-up or ceiling.)
RoundTowardNegative | Round towards negative infinity. (Also known as rounding-down or floor.)
RoundTowardZero | Round towards zero. (Also known as truncation.)

Instances

Bounded RoundingMode Source # |
Methods minBound :: RoundingMode # maxBound :: RoundingMode #
Enum RoundingMode Source # |

Methods

succ :: RoundingMode -> RoundingMode #

pred :: RoundingMode -> RoundingMode #

toEnum :: Int -> RoundingMode #

fromEnum :: RoundingMode -> Int #

enumFrom :: RoundingMode -> [RoundingMode] #

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] #

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] #

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] #

Eq RoundingMode Source # |
Methods (==) :: RoundingMode -> RoundingMode -> Bool # (/=) :: RoundingMode -> RoundingMode -> Bool #
Data RoundingMode Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RoundingMode #

toConstr :: RoundingMode -> Constr #

dataTypeOf :: RoundingMode -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c RoundingMode) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RoundingMode) #

gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

Ord RoundingMode Source # |
Methods compare :: RoundingMode -> RoundingMode -> Ordering # (<) :: RoundingMode -> RoundingMode -> Bool # (<=) :: RoundingMode -> RoundingMode -> Bool # (>) :: RoundingMode -> RoundingMode -> Bool # (>=) :: RoundingMode -> RoundingMode -> Bool # max :: RoundingMode -> RoundingMode -> RoundingMode # min :: RoundingMode -> RoundingMode -> RoundingMode #
Read RoundingMode Source # |
Methods readsPrec :: Int -> ReadS RoundingMode # readList :: ReadS [RoundingMode] # readPrec :: ReadPrec RoundingMode # readListPrec :: ReadPrec [RoundingMode] #
Show RoundingMode Source # |
Methods showsPrec :: Int -> RoundingMode -> ShowS # show :: RoundingMode -> String # showList :: [RoundingMode] -> ShowS #
HasKind RoundingMode Source # | `RoundingMode` kind

Methods

kindOf :: RoundingMode -> Kind Source #

hasSign :: RoundingMode -> Bool Source #

intSizeOf :: RoundingMode -> Int Source #

isBoolean :: RoundingMode -> Bool Source #

isBounded :: RoundingMode -> Bool Source #

isReal :: RoundingMode -> Bool Source #

isFloat :: RoundingMode -> Bool Source #

isDouble :: RoundingMode -> Bool Source #

isInteger :: RoundingMode -> Bool Source #

isUninterpreted :: RoundingMode -> Bool Source #

showType :: RoundingMode -> String Source #

SymWord RoundingMode Source # | `RoundingMode` can be used symbolically

Methods

forall :: String -> Symbolic (SBV RoundingMode) Source #

forall_ :: Symbolic (SBV RoundingMode) Source #

mkForallVars :: Int -> Symbolic [SBV RoundingMode] Source #

exists :: String -> Symbolic (SBV RoundingMode) Source #

exists_ :: Symbolic (SBV RoundingMode) Source #

mkExistVars :: Int -> Symbolic [SBV RoundingMode] Source #

free :: String -> Symbolic (SBV RoundingMode) Source #

free_ :: Symbolic (SBV RoundingMode) Source #

mkFreeVars :: Int -> Symbolic [SBV RoundingMode] Source #

symbolic :: String -> Symbolic (SBV RoundingMode) Source #

symbolics :: [String] -> Symbolic [SBV RoundingMode] Source #

literal :: RoundingMode -> SBV RoundingMode Source #

unliteral :: SBV RoundingMode -> Maybe RoundingMode Source #

fromCW :: CW -> RoundingMode Source #

isConcrete :: SBV RoundingMode -> Bool Source #

isSymbolic :: SBV RoundingMode -> Bool Source #

isConcretely :: SBV RoundingMode -> (RoundingMode -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV RoundingMode) Source #

SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices)
Methods parseCWs :: [CW] -> Maybe (RoundingMode, [CW]) Source # cvtModel :: (RoundingMode -> Maybe b) -> Maybe (RoundingMode, [CW]) -> Maybe (b, [CW]) Source #

type SRoundingMode = SBV RoundingMode Source #

The symbolic variant of `RoundingMode`

nan :: Floating a => a Source #

Not-A-Number for `Double` and `Float`. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

infinity :: Floating a => a Source #

Infinity for `Double` and `Float`. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

sNaN :: (Floating a, SymWord a) => SBV a Source #

Symbolic variant of Not-A-Number. This value will inhabit both `SDouble` and `SFloat`.

sInfinity :: (Floating a, SymWord a) => SBV a Source #

Symbolic variant of infinity. This value will inhabit both `SDouble` and `SFloat`.

#### Rounding modes

sRoundNearestTiesToEven :: SRoundingMode Source #

Symbolic variant of `RoundNearestTiesToEven`

sRoundNearestTiesToAway :: SRoundingMode Source #

Symbolic variant of `RoundNearestTiesToAway`

sRoundTowardPositive :: SRoundingMode Source #

Symbolic variant of `RoundNearestPositive`

sRoundTowardNegative :: SRoundingMode Source #

Symbolic variant of `RoundTowardNegative`

sRoundTowardZero :: SRoundingMode Source #

Symbolic variant of `RoundTowardZero`

sRNE :: SRoundingMode Source #

Alias for `sRoundNearestTiesToEven`

sRNA :: SRoundingMode Source #

Alias for `sRoundNearestTiesToAway`

sRTP :: SRoundingMode Source #

Alias for `sRoundTowardPositive`

sRTN :: SRoundingMode Source #

Alias for `sRoundTowardNegative`

sRTZ :: SRoundingMode Source #

Alias for `sRoundTowardZero`

#### Bit-pattern conversions

sFloatAsSWord32 :: SFloat -> SWord32 Source #

Convert an `SFloat` to an `SWord32`, preserving the bit-correspondence. Note that since the representation for `NaN`s are not unique, this function will return a symbolic value when given a concrete `NaN`.

Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.

sWord32AsSFloat :: SWord32 -> SFloat Source #

Reinterpret the bits in a 32-bit word as a single-precision floating point number

sDoubleAsSWord64 :: SDouble -> SWord64 Source #

Convert an `SDouble` to an `SWord64`, preserving the bit-correspondence. Note that since the representation for `NaN`s are not unique, this function will return a symbolic value when given a concrete `NaN`.

See the implementation note for `sFloatAsSWord32`, as it applies here as well.

sWord64AsSDouble :: SWord64 -> SDouble Source #

Reinterpret the bits in a 32-bit word as a single-precision floating point number

blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) Source #

Extract the sign/exponent/mantissa of a single-precision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.

blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) Source #

Extract the sign/exponent/mantissa of a single-precision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.

### Signed algebraic reals

Algebraic reals are roots of single-variable polynomials with rational coefficients. (See http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite precision numbers, but they do not cover all real numbers. (In particular, they cannot represent transcendentals.) Some irrational numbers are algebraic (such as `sqrt 2`), while others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://smtlib.cs.uiowa.edu/theories-Reals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)

type SReal = SBV AlgReal Source #

Infinite precision symbolic algebraic real value

data AlgReal Source #

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

Instances

Eq AlgReal Source # |
Methods (==) :: AlgReal -> AlgReal -> Bool # (/=) :: AlgReal -> AlgReal -> Bool #
Fractional AlgReal Source # | NB: Following the other types we have, we require `a/0` to be `0` for all a.
Methods (/) :: AlgReal -> AlgReal -> AlgReal # recip :: AlgReal -> AlgReal # fromRational :: Rational -> AlgReal #
Num AlgReal Source # |
Methods (+) :: AlgReal -> AlgReal -> AlgReal # (-) :: AlgReal -> AlgReal -> AlgReal # (*) :: AlgReal -> AlgReal -> AlgReal # negate :: AlgReal -> AlgReal # abs :: AlgReal -> AlgReal # signum :: AlgReal -> AlgReal # fromInteger :: Integer -> AlgReal #
Ord AlgReal Source # |
Methods compare :: AlgReal -> AlgReal -> Ordering # (<) :: AlgReal -> AlgReal -> Bool # (<=) :: AlgReal -> AlgReal -> Bool # (>) :: AlgReal -> AlgReal -> Bool # (>=) :: AlgReal -> AlgReal -> Bool # max :: AlgReal -> AlgReal -> AlgReal # min :: AlgReal -> AlgReal -> AlgReal #
Real AlgReal Source # |
Methods toRational :: AlgReal -> Rational #
Show AlgReal Source # |
Methods showsPrec :: Int -> AlgReal -> ShowS # show :: AlgReal -> String # showList :: [AlgReal] -> ShowS #
Arbitrary AlgReal Source # |
Methods arbitrary :: Gen AlgReal # shrink :: AlgReal -> [AlgReal] #
Random AlgReal Source # |
Methods randomR :: RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g) # random :: RandomGen g => g -> (AlgReal, g) # randomRs :: RandomGen g => (AlgReal, AlgReal) -> g -> [AlgReal] # randoms :: RandomGen g => g -> [AlgReal] # randomRIO :: (AlgReal, AlgReal) -> IO AlgReal # randomIO :: IO AlgReal #
HasKind AlgReal Source # |

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 #

isInteger :: AlgReal -> Bool Source #

isUninterpreted :: AlgReal -> Bool Source #

showType :: AlgReal -> String Source #

SatModel AlgReal Source # | `AlgReal` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (AlgReal, [CW]) Source # cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CW]) -> Maybe (b, [CW]) Source #
IEEEFloatConvertable AlgReal Source # |
Methods fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal Source # toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat Source # fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal Source # toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble Source #

sRealToSInteger :: SReal -> SInteger Source #

Convert an SReal to an SInteger. That is, it computes the largest integer `n` that satisfies `sIntegerToSReal n <= r` essentially giving us the `floor`.

For instance, `1.3` will be `1`, but `-1.3` will be `-2`.

## Creating a symbolic variable

These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms for `free` (specialized at the given type), but they might be easier to use.

sBool :: String -> Symbolic SBool Source #

Declare an `SBool`

sWord8 :: String -> Symbolic SWord8 Source #

Declare an `SWord8`

sWord16 :: String -> Symbolic SWord16 Source #

Declare an `SWord16`

sWord32 :: String -> Symbolic SWord32 Source #

Declare an `SWord32`

sWord64 :: String -> Symbolic SWord64 Source #

Declare an `SWord64`

sInt8 :: String -> Symbolic SInt8 Source #

Declare an `SInt8`

sInt16 :: String -> Symbolic SInt16 Source #

Declare an `SInt16`

sInt32 :: String -> Symbolic SInt32 Source #

Declare an `SInt32`

sInt64 :: String -> Symbolic SInt64 Source #

Declare an `SInt64`

sInteger :: String -> Symbolic SInteger Source #

Declare an `SInteger`

sReal :: String -> Symbolic SReal Source #

Declare an `SReal`

sFloat :: String -> Symbolic SFloat Source #

Declare an `SFloat`

sDouble :: String -> Symbolic SDouble Source #

Declare an `SDouble`

## Creating a list of symbolic variables

These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms for `mapM` `free` (specialized at the given type), but they might be easier to use.

sBools :: [String] -> Symbolic [SBool] Source #

Declare a list of `SBool`s

sWord8s :: [String] -> Symbolic [SWord8] Source #

Declare a list of `SWord8`s

sWord16s :: [String] -> Symbolic [SWord16] Source #

Declare a list of `SWord16`s

sWord32s :: [String] -> Symbolic [SWord32] Source #

Declare a list of `SWord32`s

sWord64s :: [String] -> Symbolic [SWord64] Source #

Declare a list of `SWord64`s

sInt8s :: [String] -> Symbolic [SInt8] Source #

Declare a list of `SInt8`s

sInt16s :: [String] -> Symbolic [SInt16] Source #

Declare a list of `SInt16`s

sInt32s :: [String] -> Symbolic [SInt32] Source #

Declare a list of `SInt32`s

sInt64s :: [String] -> Symbolic [SInt64] Source #

Declare a list of `SInt64`s

sIntegers :: [String] -> Symbolic [SInteger] Source #

Declare a list of `SInteger`s

sReals :: [String] -> Symbolic [SReal] Source #

Declare a list of `SReal`s

sFloats :: [String] -> Symbolic [SFloat] Source #

Declare a list of `SFloat`s

sDoubles :: [String] -> Symbolic [SDouble] Source #

Declare a list of `SDouble`s

### Abstract SBV type

data SBV a Source #

The Symbolic value. The parameter `a` is phantom, but is extremely important in keeping the user interface strongly typed.

Instances

Provable SBool Source # |
Methods forAll_ :: SBool -> Predicate Source # forAll :: [String] -> SBool -> Predicate Source # forSome_ :: SBool -> Predicate Source # forSome :: [String] -> SBool -> Predicate Source #
Provable Predicate Source # |
Methods forAll_ :: Predicate -> Predicate Source # forAll :: [String] -> Predicate -> Predicate Source # forSome_ :: Predicate -> Predicate Source # forSome :: [String] -> Predicate -> Predicate Source #
SDivisible SInteger Source # |
Methods sQuotRem :: SInteger -> SInteger -> (SInteger, SInteger) Source # sDivMod :: SInteger -> SInteger -> (SInteger, SInteger) Source # sQuot :: SInteger -> SInteger -> SInteger Source # sRem :: SInteger -> SInteger -> SInteger Source # sDiv :: SInteger -> SInteger -> SInteger Source # sMod :: SInteger -> SInteger -> SInteger Source #
SDivisible SInt64 Source # |
Methods sQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # sQuot :: SInt64 -> SInt64 -> SInt64 Source # sRem :: SInt64 -> SInt64 -> SInt64 Source # sDiv :: SInt64 -> SInt64 -> SInt64 Source # sMod :: SInt64 -> SInt64 -> SInt64 Source #
SDivisible SInt32 Source # |
Methods sQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # sQuot :: SInt32 -> SInt32 -> SInt32 Source # sRem :: SInt32 -> SInt32 -> SInt32 Source # sDiv :: SInt32 -> SInt32 -> SInt32 Source # sMod :: SInt32 -> SInt32 -> SInt32 Source #
SDivisible SInt16 Source # |
Methods sQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # sQuot :: SInt16 -> SInt16 -> SInt16 Source # sRem :: SInt16 -> SInt16 -> SInt16 Source # sDiv :: SInt16 -> SInt16 -> SInt16 Source # sMod :: SInt16 -> SInt16 -> SInt16 Source #
SDivisible SInt8 Source # |
Methods sQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # sQuot :: SInt8 -> SInt8 -> SInt8 Source # sRem :: SInt8 -> SInt8 -> SInt8 Source # sDiv :: SInt8 -> SInt8 -> SInt8 Source # sMod :: SInt8 -> SInt8 -> SInt8 Source #
SDivisible SWord64 Source # |
Methods sQuotRem :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # sDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # sQuot :: SWord64 -> SWord64 -> SWord64 Source # sRem :: SWord64 -> SWord64 -> SWord64 Source # sDiv :: SWord64 -> SWord64 -> SWord64 Source # sMod :: SWord64 -> SWord64 -> SWord64 Source #
SDivisible SWord32 Source # |
Methods sQuotRem :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # sDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # sQuot :: SWord32 -> SWord32 -> SWord32 Source # sRem :: SWord32 -> SWord32 -> SWord32 Source # sDiv :: SWord32 -> SWord32 -> SWord32 Source # sMod :: SWord32 -> SWord32 -> SWord32 Source #
SDivisible SWord16 Source # |
Methods sQuotRem :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # sDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # sQuot :: SWord16 -> SWord16 -> SWord16 Source # sRem :: SWord16 -> SWord16 -> SWord16 Source # sDiv :: SWord16 -> SWord16 -> SWord16 Source # sMod :: SWord16 -> SWord16 -> SWord16 Source #
SDivisible SWord8 Source # |
Methods sQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # sQuot :: SWord8 -> SWord8 -> SWord8 Source # sRem :: SWord8 -> SWord8 -> SWord8 Source # sDiv :: SWord8 -> SWord8 -> SWord8 Source # sMod :: SWord8 -> SWord8 -> SWord8 Source #
SDivisible SWord4 Source # | SDvisible instance, using default methods
Methods sQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4) Source # sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4) Source # sQuot :: SWord4 -> SWord4 -> SWord4 Source # sRem :: SWord4 -> SWord4 -> SWord4 Source # sDiv :: SWord4 -> SWord4 -> SWord4 Source # sMod :: SWord4 -> SWord4 -> SWord4 Source #
FromBits SInt64 Source # |
Methods fromBitsLE :: [SBool] -> SInt64 Source # fromBitsBE :: [SBool] -> SInt64 Source #
FromBits SInt32 Source # |
Methods fromBitsLE :: [SBool] -> SInt32 Source # fromBitsBE :: [SBool] -> SInt32 Source #
FromBits SInt16 Source # |
Methods fromBitsLE :: [SBool] -> SInt16 Source # fromBitsBE :: [SBool] -> SInt16 Source #
FromBits SInt8 Source # |
Methods fromBitsLE :: [SBool] -> SInt8 Source # fromBitsBE :: [SBool] -> SInt8 Source #
FromBits SWord64 Source # |
Methods fromBitsLE :: [SBool] -> SWord64 Source # fromBitsBE :: [SBool] -> SWord64 Source #
FromBits SWord32 Source # |
Methods fromBitsLE :: [SBool] -> SWord32 Source # fromBitsBE :: [SBool] -> SWord32 Source #
FromBits SWord16 Source # |
Methods fromBitsLE :: [SBool] -> SWord16 Source # fromBitsBE :: [SBool] -> SWord16 Source #
FromBits SWord8 Source # |
Methods fromBitsLE :: [SBool] -> SWord8 Source # fromBitsBE :: [SBool] -> SWord8 Source #
FromBits SBool Source # |
Methods fromBitsLE :: [SBool] -> SBool Source # fromBitsBE :: [SBool] -> SBool Source #
FromBits SWord4 Source # | Conversion from bits
Methods fromBitsLE :: [SBool] -> SWord4 Source # fromBitsBE :: [SBool] -> SWord4 Source #
Polynomial SWord64 Source # |
Methods polynomial :: [Int] -> SWord64 Source # pAdd :: SWord64 -> SWord64 -> SWord64 Source # pMult :: (SWord64, SWord64, [Int]) -> SWord64 Source # pDiv :: SWord64 -> SWord64 -> SWord64 Source # pMod :: SWord64 -> SWord64 -> SWord64 Source # pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # showPoly :: SWord64 -> String Source # showPolynomial :: Bool -> SWord64 -> String Source #
Polynomial SWord32 Source # |
Methods polynomial :: [Int] -> SWord32 Source # pAdd :: SWord32 -> SWord32 -> SWord32 Source # pMult :: (SWord32, SWord32, [Int]) -> SWord32 Source # pDiv :: SWord32 -> SWord32 -> SWord32 Source # pMod :: SWord32 -> SWord32 -> SWord32 Source # pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # showPoly :: SWord32 -> String Source # showPolynomial :: Bool -> SWord32 -> String Source #
Polynomial SWord16 Source # |
Methods polynomial :: [Int] -> SWord16 Source # pAdd :: SWord16 -> SWord16 -> SWord16 Source # pMult :: (SWord16, SWord16, [Int]) -> SWord16 Source # pDiv :: SWord16 -> SWord16 -> SWord16 Source # pMod :: SWord16 -> SWord16 -> SWord16 Source # pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # showPoly :: SWord16 -> String Source # showPolynomial :: Bool -> SWord16 -> String Source #
Polynomial SWord8 Source # |
Methods polynomial :: [Int] -> SWord8 Source # pAdd :: SWord8 -> SWord8 -> SWord8 Source # pMult :: (SWord8, SWord8, [Int]) -> SWord8 Source # pDiv :: SWord8 -> SWord8 -> SWord8 Source # pMod :: SWord8 -> SWord8 -> SWord8 Source # pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # showPoly :: SWord8 -> String Source # showPolynomial :: Bool -> SWord8 -> String Source #
Splittable SWord64 SWord32 Source # |
Methods split :: SWord64 -> (SWord32, SWord32) Source # (#) :: SWord32 -> SWord32 -> SWord64 Source # extend :: SWord32 -> SWord64 Source #
Splittable SWord32 SWord16 Source # |
Methods split :: SWord32 -> (SWord16, SWord16) Source # (#) :: SWord16 -> SWord16 -> SWord32 Source # extend :: SWord16 -> SWord32 Source #
Splittable SWord16 SWord8 Source # |
Methods split :: SWord16 -> (SWord8, SWord8) Source # (#) :: SWord8 -> SWord8 -> SWord16 Source # extend :: SWord8 -> SWord16 Source #
Eq (SBV a) Source # |
Methods (==) :: SBV a -> SBV a -> Bool # (/=) :: SBV a -> SBV a -> Bool #
Show (SBV a) Source # |
Methods showsPrec :: Int -> SBV a -> ShowS # show :: SBV a -> String # showList :: [SBV a] -> ShowS #
NFData (SBV a) Source # |
Methods rnf :: SBV a -> () #
(Random a, SymWord a) => Random (SBV a) Source # |
Methods randomR :: RandomGen g => (SBV a, SBV a) -> g -> (SBV a, g) # random :: RandomGen g => g -> (SBV a, g) # randomRs :: RandomGen g => (SBV a, SBV a) -> g -> [SBV a] # randoms :: RandomGen g => g -> [SBV a] # randomRIO :: (SBV a, SBV a) -> IO (SBV a) # randomIO :: IO (SBV a) #
HasKind (SBV a) Source # |
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 # isInteger :: SBV a -> Bool Source # isUninterpreted :: SBV a -> Bool Source # showType :: SBV a -> String Source #
SExecutable [SBV a] Source # |
Methods sName_ :: [SBV a] -> Symbolic () Source # sName :: [String] -> [SBV a] -> Symbolic () Source #
SExecutable (SBV a) Source # |
Methods sName_ :: SBV a -> Symbolic () Source # sName :: [String] -> SBV a -> Symbolic () Source #
Outputtable (SBV a) Source # |
Methods output :: SBV a -> Symbolic (SBV a) Source #
(SymWord a, PrettyNum a) => PrettyNum (SBV a) Source # |
Methods hexS :: SBV a -> String Source # binS :: SBV a -> String Source # hex :: SBV a -> String Source # bin :: SBV a -> String Source #
HasKind a => Uninterpreted (SBV a) Source # |
Methods uninterpret :: String -> SBV a Source # cgUninterpret :: String -> [String] -> SBV a -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV a) -> String -> SBV a Source #
SymWord a => Mergeable (SBV a) Source # |
Methods symbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a Source # select :: (SymWord b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a Source #
SymWord a => OrdSymbolic (SBV a) Source # |
Methods (.<) :: SBV a -> SBV a -> SBool Source # (.<=) :: SBV a -> SBV a -> SBool Source # (.>) :: SBV a -> SBV a -> SBool Source # (.>=) :: SBV a -> SBV a -> SBool Source # smin :: SBV a -> SBV a -> SBV a Source # smax :: SBV a -> SBV a -> SBV a Source #
EqSymbolic (SBV a) Source # |
Methods (.==) :: SBV a -> SBV a -> SBool Source # (./=) :: SBV a -> SBV a -> SBool Source #
(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () Source #
(SymWord a, SExecutable p) => SExecutable (SBV a -> p) Source # |
Methods sName_ :: (SBV a -> p) -> Symbolic () Source # sName :: [String] -> (SBV a -> p) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) Source # |
Methods sName_ :: (SBV a, SBV b) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b) -> Symbolic () Source #
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #
(SymWord a, Provable p) => Provable (SBV a -> p) Source # |
Methods forAll_ :: (SBV a -> p) -> Predicate Source # forAll :: [String] -> (SBV a -> p) -> Predicate Source # forSome_ :: (SBV a -> p) -> Predicate Source # forSome :: [String] -> (SBV a -> p) -> Predicate Source #
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a Source #
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |

Methods

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

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

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

Methods

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

cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

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

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

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

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # |

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a Source #
(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a Source #
(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV b -> SBV a) -> String -> SBV b -> SBV a Source #
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) Source # |
Methods symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e Source # select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e Source #
(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # |
Methods (===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult Source #
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) Source # |
Methods (===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () Source #

### Arrays of symbolic values

class SymArray array where Source #

Flat arrays of symbolic values An `array a b` is an array indexed by the type ``SBV` a`, with elements of type ``SBV` b` If an initial value is not provided in `newArray_` and `newArray` methods, then the elements are left unspecified, i.e., the solver is free to choose any value. This is the right thing to do if arrays are used as inputs to functions to be verified, typically.

While it's certainly possible for user to create instances of `SymArray`, the `SArray` and `SFunArray` instances already provided should cover most use cases in practice. (There are some differences between these models, however, see the corresponding declaration.)

Minimal complete definition: All methods are required, no defaults.

Minimal complete definition

newArray_, newArray, readArray, resetArray, writeArray, mergeArrays

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source #

Create a new array, with an optional initial value

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) Source #

Create a named new array, with an optional initial value

readArray :: array a b -> SBV a -> SBV b Source #

Read the array element at `a`

resetArray :: SymWord b => array a b -> SBV b -> array a b Source #

Reset all the elements of the array to the value `b`

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b Source #

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

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b Source #

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

Instances

SymArray SArray Source # |

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

resetArray :: SymWord b => SArray a b -> SBV b -> SArray a b Source #

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

data SArray a b Source #

Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

- Maps directly to SMT-lib arrays
- Reading from an unintialized value is OK and yields an unspecified result
- Can check for equality of these arrays
- Cannot quick-check theorems using `SArray` values
- Typically slower as it heavily relies on SMT-solving for the array theory

Instances

SymArray SArray Source # |

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

resetArray :: SymWord b => SArray a b -> SBV b -> SArray a b Source #

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

(HasKind a, HasKind b) => Show (SArray a b) Source # |
Methods showsPrec :: Int -> SArray a b -> ShowS # show :: SArray a b -> String # showList :: [SArray a b] -> ShowS #
(HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) Source # |
Methods forAll_ :: (SArray a b -> p) -> Predicate Source # forAll :: [String] -> (SArray a b -> p) -> Predicate Source # forSome_ :: (SArray a b -> p) -> Predicate Source # forSome :: [String] -> (SArray a b -> p) -> Predicate Source #
SymWord b => Mergeable (SArray a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source # select :: (SymWord b, Num b) => [SArray a b] -> SArray a b -> SBV b -> SArray a b Source #
EqSymbolic (SArray a b) Source # |
Methods (.==) :: SArray a b -> SArray a b -> SBool Source # (./=) :: SArray a b -> SArray a b -> SBool Source #

data SFunArray a b Source #

Arrays implemented internally as functions

- Internally handled by the library and not mapped to SMT-Lib
- Reading an uninitialized value is considered an error (will throw exception)
- Cannot check for equality (internally represented as functions)
- Can quick-check
- Typically faster as it gets compiled away during translation

Instances

(HasKind a, HasKind b) => Show (SFunArray a b) Source # |
Methods showsPrec :: Int -> SFunArray a b -> ShowS # show :: SFunArray a b -> String # showList :: [SFunArray a b] -> ShowS #
(HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) Source # |
Methods forAll_ :: (SFunArray a b -> p) -> Predicate Source # forAll :: [String] -> (SFunArray a b -> p) -> Predicate Source # forSome_ :: (SFunArray a b -> p) -> Predicate Source # forSome :: [String] -> (SFunArray a b -> p) -> Predicate Source #
SymWord b => Mergeable (SFunArray a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source # select :: (SymWord b, Num b) => [SFunArray a b] -> SFunArray a b -> SBV b -> SFunArray a b Source #

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source #

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use `newArray`.)

### Full binary trees

type STree i e = STreeInternal (SBV i) (SBV e) Source #

A symbolic tree containing values of type e, indexed by elements of type i. Note that these are full-trees, and their their shapes remain constant. There is no API provided that can change the shape of the tree. These structures are useful when dealing with data-structures that are indexed with symbolic values where access time is important. `STree` structures provide logarithmic time reads and writes.

readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e Source #

Reading a value. We bit-blast the index and descend down the full tree according to bit-values.

writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e Source #

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e Source #

Construct the fully balanced initial tree using the given values.

## Operations on symbolic values

### Word level

sTestBit :: SBV a -> Int -> SBool Source #

Replacement for `testBit`. Since `testBit` requires a `Bool` to be returned, we cannot implement it for symbolic words. Index 0 is the least-significant bit.

sExtractBits :: SBV a -> [Int] -> [SBool] Source #

Variant of `sTestBit`, where we want to extract multiple bit positions.

sPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8 Source #

Replacement for `popCount`. Since `popCount` returns an `Int`, we cannot implement it for symbolic words. Here, we return an `SWord8`, which can overflow when used on quantities that have more than 255 bits. Currently, that's only the `SInteger` type that SBV supports, all other types are safe. Even with `SInteger`, this will only overflow if there are at least 256-bits set in the number, and the smallest such number is 2^256-1, which is a pretty darn big number to worry about for practical purposes. In any case, we do not support `sPopCount` for unbounded symbolic integers, as the only possible implementation wouldn't symbolically terminate. So the only overflow issue is with really-really large concrete `SInteger` values.

sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Generalization of `shiftL`, when the shift-amount is symbolic. Since Haskell's `shiftL` only takes an `Int` as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Generalization of `shiftR`, when the shift-amount is symbolic. Since Haskell's `shiftR` only takes an `Int` as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, following the usual Haskell convention. See `sSignedShiftArithRight` for a variant that explicitly uses the msb as the sign bit, even for unsigned underlying types.

sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a Source #

Generalization of `rotateL`, when the shift-amount is symbolic. Since Haskell's `rotateL` only takes an `Int` as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a Source #

Generalization of `rotateR`, when the shift-amount is symbolic. Since Haskell's `rotateR` only takes an `Int` as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent to `sShiftRight` when the argument is signed. However, if the argument is unsigned, then it explicitly treats its msb as a sign-bit, and uses it as the bit that gets shifted in. Useful when using the underlying unsigned bit representation to implement custom signed operations. Note that there is no direct Haskell analogue of this function.

sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b Source #

Conversion between integral-symbolic values, akin to Haskell's fromIntegral

setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a Source #

Generalization of `setBit` based on a symbolic boolean. Note that `setBit` and `clearBit` are still available on Symbolic words, this operation comes handy when the condition to set/clear happens to be symbolic.

oneIf :: (Num a, SymWord a) => SBool -> SBV a Source #

Returns 1 if the boolean is true, otherwise 0.

lsb :: SBV a -> SBool Source #

Least significant bit of a word, always stored at index 0.

msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool Source #

Most significant bit of a word, always stored at the last position.

label :: SymWord a => String -> SBV a -> SBV a Source #

label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy.

### Predicates

allEqual :: EqSymbolic a => [a] -> SBool Source #

Returns (symbolic) true if all the elements of the given list are the same.

allDifferent :: EqSymbolic a => [a] -> SBool Source #

Returns (symbolic) true if all the elements of the given list are different.

inRange :: OrdSymbolic a => a -> (a, a) -> SBool Source #

Returns (symbolic) true if the argument is in range

sElem :: EqSymbolic a => a -> [a] -> SBool Source #

Symbolic membership test

### Addition and Multiplication with high-bits

fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a) Source #

Full adder. Returns the carry-out from the addition.

N.B. Only works for unsigned types. Signed arguments will be rejected.

fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a) Source #

Full multiplier: Returns both the high-order and the low-order bits in a tuple, thus fully accounting for the overflow.

N.B. Only works for unsigned types. Signed arguments will be rejected.

N.B. The higher-order bits are determined using a simple shift-add multiplier, thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently with properties involving this function, at least with the current state of the art.

### Exponentiation

(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b Source #

Symbolic exponentiation using bit blasting and repeated squaring.

N.B. The exponent must be unsigned. Signed exponents will be rejected.

### Blasting/Unblasting

blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] Source #

Big-endian blasting of a word into its bits. Also see the `FromBits` class.

blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] Source #

Little-endian blasting of a word into its bits. Also see the `FromBits` class.

class FromBits a where Source #

Unblasting a value from symbolic-bits. The bits can be given little-endian or big-endian. For a signed number in little-endian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the "reverse" view of little-big-endian representations

Minimal complete definition: `fromBitsLE`

Minimal complete definition

fromBitsLE

Methods

fromBitsLE, fromBitsBE :: [SBool] -> a Source #

Instances

FromBits SInt64 Source # |
Methods fromBitsLE :: [SBool] -> SInt64 Source # fromBitsBE :: [SBool] -> SInt64 Source #
FromBits SInt32 Source # |
Methods fromBitsLE :: [SBool] -> SInt32 Source # fromBitsBE :: [SBool] -> SInt32 Source #
FromBits SInt16 Source # |
Methods fromBitsLE :: [SBool] -> SInt16 Source # fromBitsBE :: [SBool] -> SInt16 Source #
FromBits SInt8 Source # |
Methods fromBitsLE :: [SBool] -> SInt8 Source # fromBitsBE :: [SBool] -> SInt8 Source #
FromBits SWord64 Source # |
Methods fromBitsLE :: [SBool] -> SWord64 Source # fromBitsBE :: [SBool] -> SWord64 Source #
FromBits SWord32 Source # |
Methods fromBitsLE :: [SBool] -> SWord32 Source # fromBitsBE :: [SBool] -> SWord32 Source #
FromBits SWord16 Source # |
Methods fromBitsLE :: [SBool] -> SWord16 Source # fromBitsBE :: [SBool] -> SWord16 Source #
FromBits SWord8 Source # |
Methods fromBitsLE :: [SBool] -> SWord8 Source # fromBitsBE :: [SBool] -> SWord8 Source #
FromBits SBool Source # |
Methods fromBitsLE :: [SBool] -> SBool Source # fromBitsBE :: [SBool] -> SBool Source #
FromBits SWord4 Source # | Conversion from bits
Methods fromBitsLE :: [SBool] -> SWord4 Source # fromBitsBE :: [SBool] -> SWord4 Source #

### Splitting, joining, and extending

class Splittable a b | b -> a where Source #

Splitting an `a` into two `b`'s and joining back. Intuitively, `a` is a larger bit-size word than `b`, typically double. The `extend` operation captures embedding of a `b` value into an `a` without changing its semantic value.

Minimal complete definition: All, no defaults.

Minimal complete definition

split, (#), extend

Methods

split :: a -> (b, b) Source #

(#) :: b -> b -> a infixr 5 Source #

extend :: b -> a Source #

Instances

Splittable Word8 Word4 Source # | Joiningsplitting tofrom Word8
Methods split :: Word8 -> (Word4, Word4) Source # (#) :: Word4 -> Word4 -> Word8 Source # extend :: Word4 -> Word8 Source #
Splittable Word16 Word8 Source # |
Methods split :: Word16 -> (Word8, Word8) Source # (#) :: Word8 -> Word8 -> Word16 Source # extend :: Word8 -> Word16 Source #
Splittable Word32 Word16 Source # |
Methods split :: Word32 -> (Word16, Word16) Source # (#) :: Word16 -> Word16 -> Word32 Source # extend :: Word16 -> Word32 Source #
Splittable Word64 Word32 Source # |
Methods split :: Word64 -> (Word32, Word32) Source # (#) :: Word32 -> Word32 -> Word64 Source # extend :: Word32 -> Word64 Source #
Splittable SWord64 SWord32 Source # |
Methods split :: SWord64 -> (SWord32, SWord32) Source # (#) :: SWord32 -> SWord32 -> SWord64 Source # extend :: SWord32 -> SWord64 Source #
Splittable SWord32 SWord16 Source # |
Methods split :: SWord32 -> (SWord16, SWord16) Source # (#) :: SWord16 -> SWord16 -> SWord32 Source # extend :: SWord16 -> SWord32 Source #
Splittable SWord16 SWord8 Source # |
Methods split :: SWord16 -> (SWord8, SWord8) Source # (#) :: SWord8 -> SWord8 -> SWord16 Source # extend :: SWord8 -> SWord16 Source #

## Polynomial arithmetic and CRCs

class (Num a, Bits a) => Polynomial a where Source #

Implements polynomial addition, multiplication, division, and modulus operations over GF(2^n). NB. Similar to `sQuotRem`, division by `0` is interpreted as follows:

    x pDivMod 0 = (0, x)

for all `x` (including `0`)

Minimal complete definition: `pMult`, `pDivMod`, `showPolynomial`

Minimal complete definition

pMult, pDivMod, showPolynomial

Methods

polynomial :: [Int] -> a Source #

Given bit-positions to be set, create a polynomial For instance

    polynomial [0, 1, 3] :: SWord8

will evaluate to `11`, since it sets the bits `0`, `1`, and `3`. Mathematicans would write this polynomial as `x^3 + x + 1`. And in fact, `showPoly` will show it like that.

pAdd :: a -> a -> a Source #

Add two polynomials in GF(2^n).

pMult :: (a, a, [Int]) -> a Source #

Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)

Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.

pDiv :: a -> a -> a Source #

Divide two polynomials in GF(2^n), see above note for division by 0.

pMod :: a -> a -> a Source #

Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0.

pDivMod :: a -> a -> (a, a) Source #

Division and modulus packed together.

showPoly :: a -> String Source #

Display a polynomial like a mathematician would (over the monomial `x`), with a type.

showPolynomial :: Bool -> a -> String Source #

Display a polynomial like a mathematician would (over the monomial `x`), the first argument controls if the final type is shown as well.

Instances

Polynomial Word8 Source # |
Methods polynomial :: [Int] -> Word8 Source # pAdd :: Word8 -> Word8 -> Word8 Source # pMult :: (Word8, Word8, [Int]) -> Word8 Source # pDiv :: Word8 -> Word8 -> Word8 Source # pMod :: Word8 -> Word8 -> Word8 Source # pDivMod :: Word8 -> Word8 -> (Word8, Word8) Source # showPoly :: Word8 -> String Source # showPolynomial :: Bool -> Word8 -> String Source #
Polynomial Word16 Source # |
Methods polynomial :: [Int] -> Word16 Source # pAdd :: Word16 -> Word16 -> Word16 Source # pMult :: (Word16, Word16, [Int]) -> Word16 Source # pDiv :: Word16 -> Word16 -> Word16 Source # pMod :: Word16 -> Word16 -> Word16 Source # pDivMod :: Word16 -> Word16 -> (Word16, Word16) Source # showPoly :: Word16 -> String Source # showPolynomial :: Bool -> Word16 -> String Source #
Polynomial Word32 Source # |
Methods polynomial :: [Int] -> Word32 Source # pAdd :: Word32 -> Word32 -> Word32 Source # pMult :: (Word32, Word32, [Int]) -> Word32 Source # pDiv :: Word32 -> Word32 -> Word32 Source # pMod :: Word32 -> Word32 -> Word32 Source # pDivMod :: Word32 -> Word32 -> (Word32, Word32) Source # showPoly :: Word32 -> String Source # showPolynomial :: Bool -> Word32 -> String Source #
Polynomial Word64 Source # |
Methods polynomial :: [Int] -> Word64 Source # pAdd :: Word64 -> Word64 -> Word64 Source # pMult :: (Word64, Word64, [Int]) -> Word64 Source # pDiv :: Word64 -> Word64 -> Word64 Source # pMod :: Word64 -> Word64 -> Word64 Source # pDivMod :: Word64 -> Word64 -> (Word64, Word64) Source # showPoly :: Word64 -> String Source # showPolynomial :: Bool -> Word64 -> String Source #
Polynomial SWord64 Source # |
Methods polynomial :: [Int] -> SWord64 Source # pAdd :: SWord64 -> SWord64 -> SWord64 Source # pMult :: (SWord64, SWord64, [Int]) -> SWord64 Source # pDiv :: SWord64 -> SWord64 -> SWord64 Source # pMod :: SWord64 -> SWord64 -> SWord64 Source # pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # showPoly :: SWord64 -> String Source # showPolynomial :: Bool -> SWord64 -> String Source #
Polynomial SWord32 Source # |
Methods polynomial :: [Int] -> SWord32 Source # pAdd :: SWord32 -> SWord32 -> SWord32 Source # pMult :: (SWord32, SWord32, [Int]) -> SWord32 Source # pDiv :: SWord32 -> SWord32 -> SWord32 Source # pMod :: SWord32 -> SWord32 -> SWord32 Source # pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # showPoly :: SWord32 -> String Source # showPolynomial :: Bool -> SWord32 -> String Source #
Polynomial SWord16 Source # |
Methods polynomial :: [Int] -> SWord16 Source # pAdd :: SWord16 -> SWord16 -> SWord16 Source # pMult :: (SWord16, SWord16, [Int]) -> SWord16 Source # pDiv :: SWord16 -> SWord16 -> SWord16 Source # pMod :: SWord16 -> SWord16 -> SWord16 Source # pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # showPoly :: SWord16 -> String Source # showPolynomial :: Bool -> SWord16 -> String Source #
Polynomial SWord8 Source # |
Methods polynomial :: [Int] -> SWord8 Source # pAdd :: SWord8 -> SWord8 -> SWord8 Source # pMult :: (SWord8, SWord8, [Int]) -> SWord8 Source # pDiv :: SWord8 -> SWord8 -> SWord8 Source # pMod :: SWord8 -> SWord8 -> SWord8 Source # pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # showPoly :: SWord8 -> String Source # showPolynomial :: Bool -> SWord8 -> String Source #

crcBV :: Int -> [SBool] -> [SBool] -> [SBool] Source #

Compute CRCs over bit-vectors. The call `crcBV n m p` computes the CRC of the message `m` with respect to polynomial `p`. The inputs are assumed to be blasted big-endian. The number `n` specifies how many bits of CRC is needed. Note that `n` is actually the degree of the polynomial `p`, and thus it seems redundant to pass it in. However, in a typical proof context, the polynomial can be symbolic, so we cannot compute the degree easily. While this can be worked-around by generating code that accounts for all possible degrees, the resulting code would be unnecessarily big and complicated, and much harder to reason with. (Also note that a CRC is just the remainder from the polynomial division, but this routine is much faster in practice.)

NB. The `n`th bit of the polynomial `p` must be set for the CRC to be computed correctly. Note that the polynomial argument `p` will not even have this bit present most of the time, as it will typically contain bits `0` through `n-1` as usual in the CRC literature. The higher order `n`th bit is simply assumed to be set, as it does not make sense to use a polynomial of a lesser degree. This is usually not a problem since CRC polynomials are designed and expressed this way.

NB. The literature on CRC's has many variants on how CRC's are computed. We follow the following simple procedure:

- Extend the message `m` by adding `n` 0 bits on the right
- Divide the polynomial thus obtained by the `p`
- The remainder is the CRC value.

There are many variants on final XOR's, reversed polynomials etc., so it is essential to double check you use the correct algorithm.

crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b Source #

Compute CRC's over polynomials, i.e., symbolic words. The first `Int` argument plays the same role as the one in the `crcBV` function.

## Conditionals: Mergeable values

class Mergeable a where Source #

Symbolic conditionals are modeled by the `Mergeable` class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed.

A `Mergeable` instance may be automatically derived for a custom data-type with a single constructor where the type of each field is an instance of `Mergeable`, such as a record of symbolic values. Users only need to add `Generic` and `Mergeable` to the `deriving` clause for the data-type. See `Status` for an example and an illustration of what the instance would look like if written by hand.

The function `select` is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way generalization of the `ite` function.

Minimal complete definition: None, if the type is instance of `Generic`. Otherwise `symbolicMerge`. Note that most types subject to merging are likely to be trivial instances of `Generic`.

Methods

symbolicMerge :: Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a Source #

Total indexing operation. `select xs default index` is intuitively the same as `xs !! index`, except it evaluates to `default` if `index` underflows/overflows.

symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

Instances

Mergeable () Source # |
Methods symbolicMerge :: Bool -> SBool -> () -> () -> () Source # select :: (SymWord b, Num b) => [()] -> () -> SBV b -> () Source #
Mergeable Mostek Source # |
Methods symbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek Source # select :: (SymWord b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source #
Mergeable Status Source # |
Methods symbolicMerge :: Bool -> SBool -> Status -> Status -> Status Source # select :: (SymWord b, Num b) => [Status] -> Status -> SBV b -> Status Source #
Mergeable a => Mergeable [a] Source # |
Methods symbolicMerge :: Bool -> SBool -> [a] -> [a] -> [a] Source # select :: (SymWord b, Num b) => [[a]] -> [a] -> SBV b -> [a] Source #
Mergeable a => Mergeable (Maybe a) Source # |
Methods symbolicMerge :: Bool -> SBool -> Maybe a -> Maybe a -> Maybe a Source # select :: (SymWord b, Num b) => [Maybe a] -> Maybe a -> SBV b -> Maybe a Source #
SymWord a => Mergeable (SBV a) Source # |
Methods symbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a Source # select :: (SymWord b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a Source #
Mergeable a => Mergeable (Move a) Source # | Mergeable instance for `Move` simply pushes the merging the data after run of each branch starting from the same state.
Methods symbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a Source # select :: (SymWord b, Num b) => [Move a] -> Move a -> SBV b -> Move a Source #
Mergeable b => Mergeable (a -> b) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a -> b) -> (a -> b) -> a -> b Source # select :: (SymWord b, Num b) => [a -> b] -> (a -> b) -> SBV b -> a -> b Source #
(Mergeable a, Mergeable b) => Mergeable (Either a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> Either a b -> Either a b -> Either a b Source # select :: (SymWord b, Num b) => [Either a b] -> Either a b -> SBV b -> Either a b Source #
(Mergeable a, Mergeable b) => Mergeable (a, b) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b) -> (a, b) -> (a, b) Source # select :: (SymWord b, Num b) => [(a, b)] -> (a, b) -> SBV b -> (a, b) Source #
(Ix a, Mergeable b) => Mergeable (Array a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> Array a b -> Array a b -> Array a b Source # select :: (SymWord b, Num b) => [Array a b] -> Array a b -> SBV b -> Array a b Source #
SymWord b => Mergeable (SFunArray a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source # select :: (SymWord b, Num b) => [SFunArray a b] -> SFunArray a b -> SBV b -> SFunArray a b Source #
SymWord b => Mergeable (SArray a b) Source # |
Methods symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source # select :: (SymWord b, Num b) => [SArray a b] -> SArray a b -> SBV b -> SArray a b Source #
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) Source # |
Methods symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e Source # select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e Source #
(Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b, c) -> (a, b, c) -> (a, b, c) Source # select :: (SymWord b, Num b) => [(a, b, c)] -> (a, b, c) -> SBV b -> (a, b, c) Source #
(Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # select :: (SymWord b, Num b) => [(a, b, c, d)] -> (a, b, c, d) -> SBV b -> (a, b, c, d) Source #
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # select :: (SymWord b, Num b) => [(a, b, c, d, e)] -> (a, b, c, d, e) -> SBV b -> (a, b, c, d, e) Source #
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # select :: (SymWord b, Num b) => [(a, b, c, d, e, f)] -> (a, b, c, d, e, f) -> SBV b -> (a, b, c, d, e, f) Source #
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) Source # |
Methods symbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # select :: (SymWord b, Num b) => [(a, b, c, d, e, f, g)] -> (a, b, c, d, e, f, g) -> SBV b -> (a, b, c, d, e, f, g) Source #

ite :: Mergeable a => SBool -> a -> a -> a Source #

If-then-else. This is by definition `symbolicMerge` with both branches forced. This is typically the desired behavior, but also see `iteLazy` should you need more laziness.

iteLazy :: Mergeable a => SBool -> a -> a -> a Source #

A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.

## Symbolic equality

class EqSymbolic a where Source #

Symbolic Equality. Note that we can't use Haskell's `Eq` class since Haskell insists on returning Bool Comparing symbolic values will necessarily return a symbolic value.

Minimal complete definition: `.==`

Minimal complete definition

(.==)

Methods

(.==), (./=) :: a -> a -> SBool infix 4 .==, ./= Source #

Instances

EqSymbolic Bool Source # |
Methods (.==) :: Bool -> Bool -> SBool Source # (./=) :: Bool -> Bool -> SBool Source #
EqSymbolic a => EqSymbolic [a] Source # |
Methods (.==) :: [a] -> [a] -> SBool Source # (./=) :: [a] -> [a] -> SBool Source #
EqSymbolic a => EqSymbolic (Maybe a) Source # |
Methods (.==) :: Maybe a -> Maybe a -> SBool Source # (./=) :: Maybe a -> Maybe a -> SBool Source #
EqSymbolic (SBV a) Source # |
Methods (.==) :: SBV a -> SBV a -> SBool Source # (./=) :: SBV a -> SBV a -> SBool Source #
(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # |
Methods (.==) :: Either a b -> Either a b -> SBool Source # (./=) :: Either a b -> Either a b -> SBool Source #
(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # |
Methods (.==) :: (a, b) -> (a, b) -> SBool Source # (./=) :: (a, b) -> (a, b) -> SBool Source #
EqSymbolic (SArray a b) Source # |
Methods (.==) :: SArray a b -> SArray a b -> SBool Source # (./=) :: SArray a b -> SArray a b -> SBool Source #
(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # |
Methods (.==) :: (a, b, c) -> (a, b, c) -> SBool Source # (./=) :: (a, b, c) -> (a, b, c) -> SBool Source #
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # |
Methods (.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # |
Methods (.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source # |
Methods (.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source # |
Methods (.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

## Symbolic ordering

class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #

Symbolic Comparisons. Similar to `Eq`, we cannot implement Haskell's `Ord` class since there is no way to return an `Ordering` value from a symbolic comparison. Furthermore, `OrdSymbolic` requires `Mergeable` to implement if-then-else, for the benefit of implementing symbolic versions of `max` and `min` functions.

Minimal complete definition: `.<`

Minimal complete definition

(.<)

Methods

(.<), (.<=), (.>), (.>=) :: a -> a -> SBool infix 4 .<, .<=, .>, .>= Source #

smin, smax :: a -> a -> a Source #

Instances

OrdSymbolic a => OrdSymbolic [a] Source # |
Methods (.<) :: [a] -> [a] -> SBool Source # (.<=) :: [a] -> [a] -> SBool Source # (.>) :: [a] -> [a] -> SBool Source # (.>=) :: [a] -> [a] -> SBool Source # smin :: [a] -> [a] -> [a] Source # smax :: [a] -> [a] -> [a] Source #
OrdSymbolic a => OrdSymbolic (Maybe a) Source # |
Methods (.<) :: Maybe a -> Maybe a -> SBool Source # (.<=) :: Maybe a -> Maybe a -> SBool Source # (.>) :: Maybe a -> Maybe a -> SBool Source # (.>=) :: Maybe a -> Maybe a -> SBool Source # smin :: Maybe a -> Maybe a -> Maybe a Source # smax :: Maybe a -> Maybe a -> Maybe a Source #
SymWord a => OrdSymbolic (SBV a) Source # |
Methods (.<) :: SBV a -> SBV a -> SBool Source # (.<=) :: SBV a -> SBV a -> SBool Source # (.>) :: SBV a -> SBV a -> SBool Source # (.>=) :: SBV a -> SBV a -> SBool Source # smin :: SBV a -> SBV a -> SBV a Source # smax :: SBV a -> SBV a -> SBV a Source #
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # |
Methods (.<) :: Either a b -> Either a b -> SBool Source # (.<=) :: Either a b -> Either a b -> SBool Source # (.>) :: Either a b -> Either a b -> SBool Source # (.>=) :: Either a b -> Either a b -> SBool Source # smin :: Either a b -> Either a b -> Either a b Source # smax :: Either a b -> Either a b -> Either a b Source #
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # |
Methods (.<) :: (a, b) -> (a, b) -> SBool Source # (.<=) :: (a, b) -> (a, b) -> SBool Source # (.>) :: (a, b) -> (a, b) -> SBool Source # (.>=) :: (a, b) -> (a, b) -> SBool Source # smin :: (a, b) -> (a, b) -> (a, b) Source # smax :: (a, b) -> (a, b) -> (a, b) Source #
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # |
Methods (.<) :: (a, b, c) -> (a, b, c) -> SBool Source # (.<=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>=) :: (a, b, c) -> (a, b, c) -> SBool Source # smin :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # smax :: (a, b, c) -> (a, b, c) -> (a, b, c) Source #
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # |
Methods (.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # |
Methods (.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source # |

Methods

(.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #

(.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #

(.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #

(.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #

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

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

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

Methods

(.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

(.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #

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

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

## Symbolic integral numbers

class (SymWord a, Num a, Bits a) => SIntegral a Source #

Symbolic Numbers. This is a simple class that simply incorporates all number like base types together, simplifying writing polymorphic type-signatures that work for all symbolic numbers, such as `SWord8`, `SInt8` etc. For instance, we can write a generic list-minimum function as follows:

       mm :: SIntegral a => [SBV a] -> SBV a
       mm = foldr1 (a b -> ite (a .<= b) a b)

It is similar to the standard `Integral` class, except ranging over symbolic instances.

Instances

SIntegral Int8 Source # |
SIntegral Int16 Source # |
SIntegral Int32 Source # |
SIntegral Int64 Source # |
SIntegral Integer Source # |
SIntegral Word8 Source # |
SIntegral Word16 Source # |
SIntegral Word32 Source # |
SIntegral Word64 Source # |
SIntegral Word4 Source # | SIntegral instance, using default methods

## Division

class SDivisible a where Source #

The `SDivisible` class captures the essence of division. Unfortunately we cannot use Haskell's `Integral` class since the `Real` and `Enum` superclasses are not implementable for symbolic bit-vectors. However, `quotRem` and `divMod` makes perfect sense, and the `SDivisible` class captures this operation. One issue is how division by 0 behaves. The verification technology requires total functions, and there are several design choices here. We follow Isabelle/HOL approach of assigning the value 0 for division by 0. Therefore, we impose the following pair of laws:

         x sQuotRem 0 = (0, x)
         x sDivMod  0 = (0, x)

Note that our instances implement this law even when `x` is `0` itself.

NB. `quot` truncates toward zero, while `div` truncates toward negative infinity.

Minimal complete definition: `sQuotRem`, `sDivMod`

Minimal complete definition

sQuotRem, sDivMod

Methods

sQuotRem :: a -> a -> (a, a) Source #

sDivMod :: a -> a -> (a, a) Source #

sQuot :: a -> a -> a Source #

sRem :: a -> a -> a Source #

sDiv :: a -> a -> a Source #

sMod :: a -> a -> a Source #

Instances

SDivisible Int8 Source # |
Methods sQuotRem :: Int8 -> Int8 -> (Int8, Int8) Source # sDivMod :: Int8 -> Int8 -> (Int8, Int8) Source # sQuot :: Int8 -> Int8 -> Int8 Source # sRem :: Int8 -> Int8 -> Int8 Source # sDiv :: Int8 -> Int8 -> Int8 Source # sMod :: Int8 -> Int8 -> Int8 Source #
SDivisible Int16 Source # |
Methods sQuotRem :: Int16 -> Int16 -> (Int16, Int16) Source # sDivMod :: Int16 -> Int16 -> (Int16, Int16) Source # sQuot :: Int16 -> Int16 -> Int16 Source # sRem :: Int16 -> Int16 -> Int16 Source # sDiv :: Int16 -> Int16 -> Int16 Source # sMod :: Int16 -> Int16 -> Int16 Source #
SDivisible Int32 Source # |
Methods sQuotRem :: Int32 -> Int32 -> (Int32, Int32) Source # sDivMod :: Int32 -> Int32 -> (Int32, Int32) Source # sQuot :: Int32 -> Int32 -> Int32 Source # sRem :: Int32 -> Int32 -> Int32 Source # sDiv :: Int32 -> Int32 -> Int32 Source # sMod :: Int32 -> Int32 -> Int32 Source #
SDivisible Int64 Source # |
Methods sQuotRem :: Int64 -> Int64 -> (Int64, Int64) Source # sDivMod :: Int64 -> Int64 -> (Int64, Int64) Source # sQuot :: Int64 -> Int64 -> Int64 Source # sRem :: Int64 -> Int64 -> Int64 Source # sDiv :: Int64 -> Int64 -> Int64 Source # sMod :: Int64 -> Int64 -> Int64 Source #
SDivisible Integer Source # |
Methods sQuotRem :: Integer -> Integer -> (Integer, Integer) Source # sDivMod :: Integer -> Integer -> (Integer, Integer) Source # sQuot :: Integer -> Integer -> Integer Source # sRem :: Integer -> Integer -> Integer Source # sDiv :: Integer -> Integer -> Integer Source # sMod :: Integer -> Integer -> Integer Source #
SDivisible Word8 Source # |
Methods sQuotRem :: Word8 -> Word8 -> (Word8, Word8) Source # sDivMod :: Word8 -> Word8 -> (Word8, Word8) Source # sQuot :: Word8 -> Word8 -> Word8 Source # sRem :: Word8 -> Word8 -> Word8 Source # sDiv :: Word8 -> Word8 -> Word8 Source # sMod :: Word8 -> Word8 -> Word8 Source #
SDivisible Word16 Source # |
Methods sQuotRem :: Word16 -> Word16 -> (Word16, Word16) Source # sDivMod :: Word16 -> Word16 -> (Word16, Word16) Source # sQuot :: Word16 -> Word16 -> Word16 Source # sRem :: Word16 -> Word16 -> Word16 Source # sDiv :: Word16 -> Word16 -> Word16 Source # sMod :: Word16 -> Word16 -> Word16 Source #
SDivisible Word32 Source # |
Methods sQuotRem :: Word32 -> Word32 -> (Word32, Word32) Source # sDivMod :: Word32 -> Word32 -> (Word32, Word32) Source # sQuot :: Word32 -> Word32 -> Word32 Source # sRem :: Word32 -> Word32 -> Word32 Source # sDiv :: Word32 -> Word32 -> Word32 Source # sMod :: Word32 -> Word32 -> Word32 Source #
SDivisible Word64 Source # |
Methods sQuotRem :: Word64 -> Word64 -> (Word64, Word64) Source # sDivMod :: Word64 -> Word64 -> (Word64, Word64) Source # sQuot :: Word64 -> Word64 -> Word64 Source # sRem :: Word64 -> Word64 -> Word64 Source # sDiv :: Word64 -> Word64 -> Word64 Source # sMod :: Word64 -> Word64 -> Word64 Source #
SDivisible CW Source # |
Methods sQuotRem :: CW -> CW -> (CW, CW) Source # sDivMod :: CW -> CW -> (CW, CW) Source # sQuot :: CW -> CW -> CW Source # sRem :: CW -> CW -> CW Source # sDiv :: CW -> CW -> CW Source # sMod :: CW -> CW -> CW Source #
SDivisible SInteger Source # |
Methods sQuotRem :: SInteger -> SInteger -> (SInteger, SInteger) Source # sDivMod :: SInteger -> SInteger -> (SInteger, SInteger) Source # sQuot :: SInteger -> SInteger -> SInteger Source # sRem :: SInteger -> SInteger -> SInteger Source # sDiv :: SInteger -> SInteger -> SInteger Source # sMod :: SInteger -> SInteger -> SInteger Source #
SDivisible SInt64 Source # |
Methods sQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # sQuot :: SInt64 -> SInt64 -> SInt64 Source # sRem :: SInt64 -> SInt64 -> SInt64 Source # sDiv :: SInt64 -> SInt64 -> SInt64 Source # sMod :: SInt64 -> SInt64 -> SInt64 Source #
SDivisible SInt32 Source # |
Methods sQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # sQuot :: SInt32 -> SInt32 -> SInt32 Source # sRem :: SInt32 -> SInt32 -> SInt32 Source # sDiv :: SInt32 -> SInt32 -> SInt32 Source # sMod :: SInt32 -> SInt32 -> SInt32 Source #
SDivisible SInt16 Source # |
Methods sQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # sQuot :: SInt16 -> SInt16 -> SInt16 Source # sRem :: SInt16 -> SInt16 -> SInt16 Source # sDiv :: SInt16 -> SInt16 -> SInt16 Source # sMod :: SInt16 -> SInt16 -> SInt16 Source #
SDivisible SInt8 Source # |
Methods sQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # sQuot :: SInt8 -> SInt8 -> SInt8 Source # sRem :: SInt8 -> SInt8 -> SInt8 Source # sDiv :: SInt8 -> SInt8 -> SInt8 Source # sMod :: SInt8 -> SInt8 -> SInt8 Source #
SDivisible SWord64 Source # |
Methods sQuotRem :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # sDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64) Source # sQuot :: SWord64 -> SWord64 -> SWord64 Source # sRem :: SWord64 -> SWord64 -> SWord64 Source # sDiv :: SWord64 -> SWord64 -> SWord64 Source # sMod :: SWord64 -> SWord64 -> SWord64 Source #
SDivisible SWord32 Source # |
Methods sQuotRem :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # sDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32) Source # sQuot :: SWord32 -> SWord32 -> SWord32 Source # sRem :: SWord32 -> SWord32 -> SWord32 Source # sDiv :: SWord32 -> SWord32 -> SWord32 Source # sMod :: SWord32 -> SWord32 -> SWord32 Source #
SDivisible SWord16 Source # |
Methods sQuotRem :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # sDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16) Source # sQuot :: SWord16 -> SWord16 -> SWord16 Source # sRem :: SWord16 -> SWord16 -> SWord16 Source # sDiv :: SWord16 -> SWord16 -> SWord16 Source # sMod :: SWord16 -> SWord16 -> SWord16 Source #
SDivisible SWord8 Source # |
Methods sQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # sQuot :: SWord8 -> SWord8 -> SWord8 Source # sRem :: SWord8 -> SWord8 -> SWord8 Source # sDiv :: SWord8 -> SWord8 -> SWord8 Source # sMod :: SWord8 -> SWord8 -> SWord8 Source #
SDivisible SWord4 Source # | SDvisible instance, using default methods
Methods sQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4) Source # sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4) Source # sQuot :: SWord4 -> SWord4 -> SWord4 Source # sRem :: SWord4 -> SWord4 -> SWord4 Source # sDiv :: SWord4 -> SWord4 -> SWord4 Source # sMod :: SWord4 -> SWord4 -> SWord4 Source #
SDivisible Word4 Source # | SDvisible instance, using 0-extension
Methods sQuotRem :: Word4 -> Word4 -> (Word4, Word4) Source # sDivMod :: Word4 -> Word4 -> (Word4, Word4) Source # sQuot :: Word4 -> Word4 -> Word4 Source # sRem :: Word4 -> Word4 -> Word4 Source # sDiv :: Word4 -> Word4 -> Word4 Source # sMod :: Word4 -> Word4 -> Word4 Source #

## The Boolean class

class Boolean b where Source #

The `Boolean` class: a generalization of Haskell's `Bool` type Haskell `Bool` and SBV's `SBool` are instances of this class, unifying the treatment of boolean values.

Minimal complete definition: `true`, `bnot`, `&&&` However, it's advisable to define `false`, and `|||` as well (typically), for clarity.

Minimal complete definition

true, bnot, (&&&)

Methods

true :: b Source #

logical true

false :: b Source #

logical false

bnot :: b -> b Source #

complement

(&&&) :: b -> b -> b infixr 3 Source #

and

(|||) :: b -> b -> b infixr 2 Source #

or

(~&) :: b -> b -> b infixr 3 Source #

nand

(~|) :: b -> b -> b infixr 2 Source #

nor

(<+>) :: b -> b -> b infixl 6 Source #

xor

(==>) :: b -> b -> b infixr 1 Source #

implies

(<=>) :: b -> b -> b infixr 1 Source #

equivalence

fromBool :: Bool -> b Source #

cast from Bool

Instances

Boolean Bool Source # |
Methods true :: Bool Source # false :: Bool Source # bnot :: Bool -> Bool Source # (&&&) :: Bool -> Bool -> Bool Source # (|||) :: Bool -> Bool -> Bool Source # (~&) :: Bool -> Bool -> Bool Source # (~|) :: Bool -> Bool -> Bool Source # (<+>) :: Bool -> Bool -> Bool Source # (==>) :: Bool -> Bool -> Bool Source # (<=>) :: Bool -> Bool -> Bool Source # fromBool :: Bool -> Bool Source #

### Generalizations of boolean operations

bAnd :: Boolean b => [b] -> b Source #

Generalization of `and`

bOr :: Boolean b => [b] -> b Source #

Generalization of `or`

bAny :: Boolean b => (a -> b) -> [a] -> b Source #

Generalization of `any`

bAll :: Boolean b => (a -> b) -> [a] -> b Source #

Generalization of `all`

## Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a where Source #

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: `hexS` and `binS`

Minimal complete definition

hexS, binS, hex, bin

Methods

hexS :: a -> String Source #

Show a number in hexadecimal (starting with `0x` and type.)

binS :: a -> String Source #

Show a number in binary (starting with `0b` and type.)

hex :: a -> String Source #

Show a number in hex, without prefix, or types.

bin :: a -> String Source #

Show a number in bin, without prefix, or types.

Instances

PrettyNum Bool Source # |
Methods hexS :: Bool -> String Source # binS :: Bool -> String Source # hex :: Bool -> String Source # bin :: Bool -> String Source #
PrettyNum Int8 Source # |
Methods hexS :: Int8 -> String Source # binS :: Int8 -> String Source # hex :: Int8 -> String Source # bin :: Int8 -> String Source #
PrettyNum Int16 Source # |
Methods hexS :: Int16 -> String Source # binS :: Int16 -> String Source # hex :: Int16 -> String Source # bin :: Int16 -> String Source #
PrettyNum Int32 Source # |
Methods hexS :: Int32 -> String Source # binS :: Int32 -> String Source # hex :: Int32 -> String Source # bin :: Int32 -> String Source #
PrettyNum Int64 Source # |
Methods hexS :: Int64 -> String Source # binS :: Int64 -> String Source # hex :: Int64 -> String Source # bin :: Int64 -> String Source #
PrettyNum Integer Source # |
Methods hexS :: Integer -> String Source # binS :: Integer -> String Source # hex :: Integer -> String Source # bin :: Integer -> String Source #
PrettyNum Word8 Source # |
Methods hexS :: Word8 -> String Source # binS :: Word8 -> String Source # hex :: Word8 -> String Source # bin :: Word8 -> String Source #
PrettyNum Word16 Source # |
Methods hexS :: Word16 -> String Source # binS :: Word16 -> String Source # hex :: Word16 -> String Source # bin :: Word16 -> String Source #
PrettyNum Word32 Source # |
Methods hexS :: Word32 -> String Source # binS :: Word32 -> String Source # hex :: Word32 -> String Source # bin :: Word32 -> String Source #
PrettyNum Word64 Source # |
Methods hexS :: Word64 -> String Source # binS :: Word64 -> String Source # hex :: Word64 -> String Source # bin :: Word64 -> String Source #
PrettyNum CW Source # |
Methods hexS :: CW -> String Source # binS :: CW -> String Source # hex :: CW -> String Source # bin :: CW -> String Source #
(SymWord a, PrettyNum a) => PrettyNum (SBV a) Source # |
Methods hexS :: SBV a -> String Source # binS :: SBV a -> String Source # hex :: SBV a -> String Source # bin :: SBV a -> String Source #

readBin :: Num a => String -> a Source #

A more convenient interface for reading binary numbers, also supports negative numbers

# Checking satisfiability in path conditions

isSatisfiableInCurrentPath :: SBool -> Symbolic Bool Source #

Check if a boolean condition is satisfiable in the current state. This function can be useful in contexts where an interpreter implemented on top of SBV needs to decide if a particular stae (represented by the boolean) is reachable in the current if-then-else paths implied by the `ite` calls.

# Uninterpreted sorts, constants, and functions

Users can introduce new uninterpreted sorts simply by defining a data-type in Haskell and registering it as such. The following example demonstrates:

        data B = B () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SatModel)

(Note that you'll also need to use the language pragmas `DeriveDataTypeable`, `DeriveAnyClass`, and import `Data.Generics` for the above to work.)

This is all it takes to introduce `B` as an uninterpreted sort in SBV, which makes the type `SBV B` automagically become available as the type of symbolic values that ranges over `B` values. Note that the `()` argument is important to distinguish it from enumerations.

Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by the `Uninterpreted` class.

class Uninterpreted a where Source #

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

Minimal complete definition: `sbvUninterpret`. However, most instances in practice are already provided by SBV, so end-users should not need to define their own instances.

Minimal complete definition

sbvUninterpret

Methods

uninterpret :: String -> a Source #

Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.

cgUninterpret :: String -> [String] -> a -> a Source #

Uninterpret a value, only for the purposes of code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.

sbvUninterpret :: Maybe ([String], a) -> String -> a Source #

Most generalized form of uninterpretation, this function should not be needed by end-user-code, but is rather useful for the library development.

Instances

HasKind a => Uninterpreted (SBV a) Source # |
Methods uninterpret :: String -> SBV a Source # cgUninterpret :: String -> [String] -> SBV a -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV a) -> String -> SBV a Source #
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a Source #
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |
Methods uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source # sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # |

Methods

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

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

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

Methods

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

cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

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

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

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

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # |

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a Source #
(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV c -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a Source #
(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) Source # |
Methods uninterpret :: String -> SBV b -> SBV a Source # cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a Source # sbvUninterpret :: Maybe ([String], SBV b -> SBV a) -> String -> SBV b -> SBV a Source #

addAxiom :: String -> [String] -> Symbolic () Source #

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

# Enumerations

If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually translate that as just such a data-type to SMT-Lib, and will use the constructors as the inhabitants of the said sort. A simple example is:

       data X = A | B | C deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SatModel)

Now, the user can define

       type SX = SBV X

and treat `SX` as a regular symbolic type ranging over the values `A`, `B`, and `C`. Such values can be compared for equality, and with the usual other comparison operators, such as `.==`, `./=`, `.>`, `.>=`, `<`, and `<=`.

Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple query would look like:

        allSat $ x -> x .== (x :: SX)

which would list all three elements of this domain as satisfying solutions.

        Solution #1:
          s0 = A :: X
        Solution #2:
          s0 = B :: X
        Solution #3:
          s0 = C :: X
        Found 3 different solutions.

Note that the result is properly typed as `X` elements; these are not mere strings. So, in a `getModel` scenario, the user can recover actual elements of the domain and program further with those values as usual.

# Properties, proofs, satisfiability, and safety

The SBV library provides a "push-button" verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://smtlib.cs.uiowa.edu/) to communicate with arbitrary SMT solvers.

## Predicates

type Predicate = Symbolic SBool Source #

A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The `Symbolic` monad captures the underlying representation, and can/should be ignored by the users of the library, unless you are building further utilities on top of SBV itself. Instead, simply use the `Predicate` type when necessary.

class Provable a where Source #

A type `a` is provable if we can turn it into a predicate. Note that a predicate can be made from a curried function of arbitrary arity, where each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So predicates can be constructed from almost arbitrary Haskell functions that have arbitrary shapes. (See the instance declarations below.)

Minimal complete definition

forAll_, forAll, forSome_, forSome

Methods

forAll_ :: a -> Predicate Source #

Turns a value into a universally quantified predicate, internally naming the inputs. In this case the sbv library will use names of the form `s1, s2`, etc. to name these variables Example:

     forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y

is a predicate with two arguments, captured using an ordinary Haskell function. Internally, `x` will be named `s0` and `y` will be named `s1`.

forAll :: [String] -> a -> Predicate Source #

Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:

     forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y

This is the same as above, except the variables will be named `x` and `y` respectively, simplifying the counter-examples when they are printed.

forSome_ :: a -> Predicate Source #

Turns a value into an existentially quantified predicate. (Indeed, `exists` would have been a better choice here for the name, but alas it's already taken.)

forSome :: [String] -> a -> Predicate Source #

Version of `forSome` that allows user defined names

Instances

Provable SBool Source # |
Methods forAll_ :: SBool -> Predicate Source # forAll :: [String] -> SBool -> Predicate Source # forSome_ :: SBool -> Predicate Source # forSome :: [String] -> SBool -> Predicate Source #
Provable Predicate Source # |
Methods forAll_ :: Predicate -> Predicate Source # forAll :: [String] -> Predicate -> Predicate Source # forSome_ :: Predicate -> Predicate Source # forSome :: [String] -> Predicate -> Predicate Source #
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # |
Methods forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source # forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #
(HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) Source # |
Methods forAll_ :: (SFunArray a b -> p) -> Predicate Source # forAll :: [String] -> (SFunArray a b -> p) -> Predicate Source # forSome_ :: (SFunArray a b -> p) -> Predicate Source # forSome :: [String] -> (SFunArray a b -> p) -> Predicate Source #
(HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) Source # |
Methods forAll_ :: (SArray a b -> p) -> Predicate Source # forAll :: [String] -> (SArray a b -> p) -> Predicate Source # forSome_ :: (SArray a b -> p) -> Predicate Source # forSome :: [String] -> (SArray a b -> p) -> Predicate Source #
(SymWord a, Provable p) => Provable (SBV a -> p) Source # |
Methods forAll_ :: (SBV a -> p) -> Predicate Source # forAll :: [String] -> (SBV a -> p) -> Predicate Source # forSome_ :: (SBV a -> p) -> Predicate Source # forSome :: [String] -> (SBV a -> p) -> Predicate Source #

class Equality a where Source #

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

Minimal complete definition

(===)

Methods

(===) :: a -> a -> IO ThmResult infix 4 Source #

Instances

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # |
Methods (===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) Source # |
Methods (===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult Source #
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # |
Methods (===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult Source #
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) Source # |
Methods (===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source #

## Proving properties

prove :: Provable a => a -> IO ThmResult Source #

Prove a predicate, equivalent to ``proveWith` `defaultSMTCfg``

proveWith :: Provable a => SMTConfig -> a -> IO ThmResult Source #

Proves the predicate using the given SMT-solver

isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool) Source #

Checks theoremhood within the given optional time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

isTheoremWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool) Source #

Check whether a given property is a theorem, with an optional time out and the given solver. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Checking satisfiability

sat :: Provable a => a -> IO SatResult Source #

Find a satisfying assignment for a predicate, equivalent to ``satWith` `defaultSMTCfg``

satWith :: Provable a => SMTConfig -> a -> IO SatResult Source #

Find a satisfying assignment using the given SMT-solver

isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool) Source #

Checks satisfiability within the given optional time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

isSatisfiableWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool) Source #

Check whether a given property is satisfiable, with an optional time out and the given solver. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Checking safety

The `sAssert` function allows users to introduce invariants to make sure certain properties hold at all times. This is another mechanism to provide further documentation/contract info into SBV code. The functions `safe` and `safeWith` can be used to statically discharge these proof assumptions. If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.

Here's a simple example. Let's assume we have a function that does subtraction, and requires its first argument to be larger than the second:

    >>> let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y)

Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument. We can use `safe` to statically see if such a violation is possible before we use this function elsewhere.

    >>> safe (sub :: SInt8 -> SInt8 -> SInt8)
    [sub: x >= y must hold!: Violated. Model:
      s0 = -128 :: Int8
      s1 = -127 :: Int8]

What happens if we make sure to arrange for this invariant? Consider this version:

    >>> let safeSub x y = ite (x .>= y) (sub x y) 0

Clearly, `safeSub` must be safe. And indeed, SBV can prove that:

    >>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)
    [sub: x >= y must hold!: No violations detected]

Note how we used `sub` and `safeSub` polymorphically. We only need to monomorphise our types when a proof attempt is done, as we did in the `safe` calls.

If required, the user can pass a `CallStack` through the first argument to `sAssert`, which will be used by SBV to print a diagnostic info to pinpoint the failure.

Also see Data.SBV.Examples.Misc.NoDiv0 for the classic div-by-zero example.

sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a Source #

Symbolic assert. Check that the given boolean condition is always true in the given path. The optional first argument can be used to provide call-stack info via GHC's location facilities.

safe :: SExecutable a => a -> IO [SafeResult] Source #

Check that all the `sAssert` calls are safe, equivalent to ``safeWith` `defaultSMTCfg``

safeWith :: SExecutable a => SMTConfig -> a -> IO [SafeResult] Source #

Check if any of the assertions can be violated

isSafe :: SafeResult -> Bool Source #

Check if a safe-call was safe or not, turning a `SafeResult` to a Bool.

class SExecutable a where Source #

Symbolically executable program fragments. This class is mainly used for `safe` calls, and is sufficently populated internally to cover most use cases. Users can extend it as they wish to allow `safe` checks for SBV programs that return/take types that are user-defined.

Minimal complete definition

sName_, sName

Methods

sName_ :: a -> Symbolic () Source #

sName :: [String] -> a -> Symbolic () Source #

Instances

SExecutable () Source # |
Methods sName_ :: () -> Symbolic () Source # sName :: [String] -> () -> Symbolic () Source #
SExecutable [SBV a] Source # |
Methods sName_ :: [SBV a] -> Symbolic () Source # sName :: [String] -> [SBV a] -> Symbolic () Source #
NFData a => SExecutable (Symbolic a) Source # |
Methods sName_ :: Symbolic a -> Symbolic () Source # sName :: [String] -> Symbolic a -> Symbolic () Source #
SExecutable (SBV a) Source # |
Methods sName_ :: SBV a -> Symbolic () Source # sName :: [String] -> SBV a -> Symbolic () Source #
(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic () Source #
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # |
Methods sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () Source # sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic () Source #
(SymWord a, SExecutable p) => SExecutable (SBV a -> p) Source # |
Methods sName_ :: (SBV a -> p) -> Symbolic () Source # sName :: [String] -> (SBV a -> p) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) Source # |
Methods sName_ :: (SBV a, SBV b) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic () Source #
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) Source # |
Methods sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () Source # sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic () Source #

## Finding all satisfying assignments

allSat :: Provable a => a -> IO AllSatResult Source #

Return all satisfying assignments for a predicate, equivalent to ``allSatWith` `defaultSMTCfg``. Satisfying assignments are constructed lazily, so they will be available as returned by the solver and on demand.

NB. Uninterpreted constant/function values and counter-examples for array values are ignored for the purposes of ``allSat``. That is, only the satisfying assignments modulo uninterpreted functions and array inputs will be returned. This is due to the limitation of not having a robust means of getting a function counter-example back from the SMT solver.

allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult Source #

Find all satisfying assignments using the given SMT-solver

## Satisfying a sequence of boolean conditions

solve :: [SBool] -> Symbolic SBool Source #

Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:

      do [x, y, z] <- sIntegers ["x", "y", "z"]
         solve [x .> 5, y + z .< x]

## Adding constraints

A constraint is a means for restricting the input domain of a formula. Here's a simple example:

       do x <- exists "x"
          y <- exists "y"
          constrain $ x .> y
          constrain $ x + y .>= 12
          constrain $ y .>= 3
          ...

The first constraint requires `x` to be larger than `y`. The scond one says that sum of `x` and `y` must be at least `12`, and the final one says that `y` to be at least `3`. Constraints provide an easy way to assert additional properties on the input domain, right at the point of the introduction of variables.

Note that the proper reading of a constraint depends on the context:

- In a `sat` (or `allSat`) call: The constraint added is asserted conjunctively. That is, the resulting satisfying model (if any) will always satisfy all the constraints given.
- In a `prove` call: In this case, the constraint acts as an implication. The property is proved under the assumption that the constraint holds. In other words, the constraint says that we only care about the input space that satisfies the constraint.
- In a `quickCheck` call: The constraint acts as a filter for `quickCheck`; if the constraint does not hold, then the input value is considered to be irrelevant and is skipped. Note that this is similar to `prove`, but is stronger: We do not accept a test case to be valid just because the constraints fail on them, although semantically the implication does hold. We simply skip that test case as a bad test vector.
- In a `genTest` call: Similar to `quickCheck` and `prove`: If a constraint does not hold, the input value is ignored and is not included in the test set.

A good use case (in fact the motivating use case) for `constrain` is attaching a constraint to a `forall` or `exists` variable at the time of its creation. Also, the conjunctive semantics for `sat` and the implicative semantics for `prove` simplify programming by choosing the correct interpretation automatically. However, one should be aware of the semantic difference. For instance, in the presence of constraints, formulas that are provable are not necessarily satisfiable. To wit, consider:

       do x <- exists "x"
          constrain $ x .< x
          return $ x .< (x :: SWord8)

This predicate is unsatisfiable since no element of `SWord8` is less than itself. But it's (vacuously) true, since it excludes the entire domain of values, thus making the proof trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given constraints are not vacuous, the functions `isVacuous` (and `isVacuousWith`) can be used.

Also note that this semantics imply that test case generation (`genTest`) and quick-check can take arbitrarily long in the presence of constraints, if the random input values generated rarely satisfy the constraints. (As an extreme case, consider ``constrain` `false``.)

A probabilistic constraint (see `pConstrain`) attaches a probability threshold for the constraint to be considered. For instance:

        pConstrain 0.8 c

will make sure that the condition `c` is satisfied 80% of the time (and correspondingly, falsified 20% of the time), in expectation. This variant is useful for `genTest` and `quickCheck` functions, where we want to filter the test cases according to some probability distribution, to make sure that the test-vectors are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases with the above constraint, we'd expect about 80 of them to satisfy the condition `c`, while about 20 of them will fail it.

The following properties hold:

       constrain      = pConstrain 1
       pConstrain t c = pConstrain (1-t) (not c)

Note that while `constrain` can be used freely, `pConstrain` is only allowed in the contexts of `genTest` or `quickCheck`. Calls to `pConstrain` in a prove/sat call will be rejected as SBV does not deal with probabilistic constraints when it comes to satisfiability and proofs. Also, both `constrain` and `pConstrain` calls during code-generation will also be rejected, for similar reasons.

constrain :: SBool -> Symbolic () Source #

Adding arbitrary constraints. When adding constraints, one has to be careful about making sure they are not inconsistent. The function `isVacuous` can be use for this purpose. Here is an example. Consider the following predicate:

    >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }

This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the values considered satisfy `x .< x`, i.e., they are less than themselves. Since there are no values that satisfy this constraint, the proof will pass vacuously:

    >>> prove pred
    Q.E.D.

We can use `isVacuous` to make sure to see that the pass was vacuous:

    >>> isVacuous pred
    True

While the above example is trivial, things can get complicated if there are multiple constraints with non-straightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:

    >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }

This time the proof passes as expected:

    >>> prove pred'
    Q.E.D.

And the proof is not vacuous:

    >>> isVacuous pred'
    False

pConstrain :: Double -> SBool -> Symbolic () Source #

Adding a probabilistic constraint. The `Double` argument is the probability threshold. Probabilistic constraints are useful for `genTest` and `quickCheck` calls where we restrict our attention to interesting parts of the input domain.

## Checking constraint vacuity

isVacuous :: Provable a => a -> IO Bool Source #

Check if the given constraints are satisfiable, equivalent to ``isVacuousWith` `defaultSMTCfg``. See the function `constrain` for an example use of `isVacuous`.

isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool Source #

Determine if the constraints are vacuous using the given SMT-solver

## Quick-checking

sbvQuickCheck :: Symbolic SBool -> IO Bool Source #

Quick check an SBV property. Note that a regular `quickCheck` call will work just as well. Use this variant if you want to receive the boolean result.

# Proving properties using multiple solvers

On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers, using parallel threads. Even with machines with single-cores, threading can be helpful if you want to try out multiple-solvers but do not know which one would work the best for the problem at hand ahead of time.

The functions in this section allow proving/satisfiability-checking with multiple backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one.

The `All` variants, (i.e., `proveWithAll`, `satWithAll`) run all solvers and return all the results. SBV internally makes sure that the result is lazily generated; so, the order of solvers given does not matter. In other words, the order of results will follow the order of the solvers as they finish, not as given by the user. These variants are useful when you want to make sure multiple-solvers agree (or disagree!) on a given problem.

The `Any` variants, (i.e., `proveWithAny`, `satWithAny`) will run all the solvers in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants are useful when you do not care if the solvers produce the same result, but rather want to get the solution as quickly as possible, taking advantage of modern many-core machines.

Note that the function `sbvAvailableSolvers` will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine.

proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)] Source #

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

proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, 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 :: Provable a => [SMTConfig] -> a -> IO [(Solver, 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 :: Provable a => [SMTConfig] -> a -> IO (Solver, 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.

# Optimization

Symbolic optimization. A call of the form:

    minimize Quantified cost n valid

returns `Just xs`, such that:

- `xs` has precisely `n` elements
- `valid xs` holds
- `cost xs` is minimal. That is, for all sequences `ys` that satisfy the first two criteria above, `cost xs .<= cost ys` holds.

If there is no such sequence, then `minimize` will return `Nothing`.

The function `maximize` is similar, except the comparator is `.>=`. So the value returned has the largest cost (or value, in that case).

The function `optimize` allows the user to give a custom comparison function.

The `OptimizeOpts` argument controls how the optimization is done. If `Quantified` is used, then the SBV optimization engine satisfies the following predicate:

    exists xs. forall ys. valid xs && (valid ys `implies` (cost xs `cmp` cost ys))

Note that this may cause efficiency problems as it involves alternating quantifiers. If `OptimizeOpts` is set to `Iterative` `True`, then SBV will programmatically search for an optimal solution, by repeatedly calling the solver appropriately. (The boolean argument controls whether progress reports are given. Use `False` for quiet operation.)

### Quantified vs Iterative

Note that the quantified and iterative versions are two different optimization approaches and may not necessarily yield the same results. In particular, the quantified version can tell us no such solution exists if there is no global optimum value, while the iterative version might simply loop forever for such a problem. To wit, consider the example:

     maximize Quantified head 1 (const true :: [SInteger] -> SBool)

which asks for the largest `SInteger` value. The SMT solver will happily answer back saying there is no such value with the `Quantified` call, but the `Iterative` variant will simply loop forever as it would search through an infinite chain of ascending `SInteger` values.

In practice, however, the iterative version is usually the more effective choice since alternating quantifiers are hard to deal with for many SMT-solvers and thus will likely result in an `unknown` result. While the `Iterative` variant can loop for a long time, one can simply use the boolean flag `True` and see how the search is progressing.

minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source #

Minimizes a cost function with respect to a constraint. Examples:

    >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
    Just [11,11,11]

maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source #

Maximizes a cost function with respect to a constraint. Examples:

    >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
    Just [9,9,9]

optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source #

Variant of `optimizeWith` using the default solver. See `optimizeWith` for parameter descriptions.

minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source #

Variant of `minimize` allowing the use of a user specified solver. See `optimizeWith` for parameter descriptions.

maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source #

Variant of `maximize` allowing the use of a user specified solver. See `optimizeWith` for parameter descriptions.

optimizeWith Source #

Arguments

:: (SatModel a, SymWord a, Show a, SymWord c, Show c) |
=> SMTConfig | SMT configuration
-> OptimizeOpts | Optimization options
-> (SBV c -> SBV c -> SBool) | comparator
-> ([SBV a] -> SBV c) | cost function
-> Int | how many elements?
-> ([SBV a] -> SBool) | validity constraint
-> IO (Maybe [a]) |

Symbolic optimization. Generalization on `minimize` and `maximize` that allows arbitrary cost functions and comparisons.

# Computing expected values

expectedValue :: Outputtable a => Symbolic a -> IO [Double] Source #

Given a symbolic computation that produces a value, compute the expected value that value would take if this computation is run with its free variables drawn from uniform distributions of its respective values, satisfying the given constraints specified by `constrain` and `pConstrain` calls. This is equivalent to calling `expectedValueWith` the following parameters: verbose, warm-up round count of `10000`, no maximum iteration count, and with convergence margin `0.0001`.

expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double] Source #

Generalized version of `expectedValue`, allowing the user to specify the warm-up count and the convergence factor. Maximum iteration count can also be specified, at which point convergence won't be sought. The boolean controls verbosity.

# Model extraction

The default `Show` instances for prover calls provide all the counter-example information in a human-readable form and should be sufficient for most casual uses of sbv. However, tools built on top of sbv will inevitably need to look into the constructed models more deeply, programmatically extracting their results and performing actions based on them. The API provided in this section aims at simplifying this task.

## Inspecting proof results

`ThmResult`, `SatResult`, and `AllSatResult` are simple newtype wrappers over `SMTResult`. Their main purpose is so that we can provide custom `Show` instances to print results accordingly.

newtype ThmResult Source #

A `prove` call results in a `ThmResult`

Constructors

ThmResult SMTResult |

Instances

Show ThmResult Source # | User friendly way of printing theorem results
Methods showsPrec :: Int -> ThmResult -> ShowS # show :: ThmResult -> String # showList :: [ThmResult] -> ShowS #
Modelable ThmResult Source # | `ThmResult` as a generic model provider
Methods modelExists :: ThmResult -> Bool Source # getModel :: SatModel b => ThmResult -> Either String (Bool, b) Source # getModelDictionary :: ThmResult -> Map String CW Source # getModelValue :: SymWord b => String -> ThmResult -> Maybe b Source # getModelUninterpretedValue :: String -> ThmResult -> Maybe String Source # extractModel :: SatModel b => ThmResult -> Maybe b 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

Show SatResult Source # | User friendly way of printing satisfiablity results
Methods showsPrec :: Int -> SatResult -> ShowS # show :: SatResult -> String # showList :: [SatResult] -> ShowS #
Modelable SatResult Source # | `SatResult` as a generic model provider
Methods modelExists :: SatResult -> Bool Source # getModel :: SatModel b => SatResult -> Either String (Bool, b) Source # getModelDictionary :: SatResult -> Map String CW Source # getModelValue :: SymWord b => String -> SatResult -> Maybe b Source # getModelUninterpretedValue :: String -> SatResult -> Maybe String Source # extractModel :: SatModel b => SatResult -> Maybe b Source #

newtype SafeResult Source #

A `safe` call results in a `SafeResult`

Constructors

SafeResult (Maybe String, String, SMTResult) |

Instances

Show SafeResult Source # | User friendly way of printing safety results
Methods showsPrec :: Int -> SafeResult -> ShowS # show :: SafeResult -> String # showList :: [SafeResult] -> ShowS #

newtype AllSatResult Source #

An `allSat` call results in a `AllSatResult`. The boolean says whether we should warn the user about prefix-existentials.

Constructors

AllSatResult (Bool, [SMTResult]) |

Instances

Show AllSatResult Source # | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available.
Methods showsPrec :: Int -> AllSatResult -> ShowS # show :: AllSatResult -> String # showList :: [AllSatResult] -> 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 | Unsatisfiable
Satisfiable SMTConfig SMTModel | Satisfiable with model
Unknown SMTConfig SMTModel | Prover returned unknown, with a potential (possibly bogus) model
ProofError SMTConfig [String] | Prover errored out
TimeOut SMTConfig | Computation timed out (see the `timeout` combinator)

Instances

NFData SMTResult Source # |
Methods rnf :: SMTResult -> () #
Modelable SMTResult Source # | `SMTResult` as a generic model provider
Methods modelExists :: SMTResult -> Bool Source # getModel :: SatModel b => SMTResult -> Either String (Bool, b) Source # getModelDictionary :: SMTResult -> Map String CW Source # getModelValue :: SymWord b => String -> SMTResult -> Maybe b Source # getModelUninterpretedValue :: String -> SMTResult -> Maybe String Source # extractModel :: SatModel b => SMTResult -> Maybe b Source #

## Programmable model extraction

While default `Show` instances are sufficient for most use cases, it is sometimes desirable (especially for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable extraction allows getting arbitrarily typed models out of SMT models.

class SatModel a where Source #

Instances of `SatModel` can be automatically extracted from models returned by the solvers. The idea is that the sbv infrastructure provides a stream of `CW'`s (constant-words) coming from the solver, and the type `a` is interpreted based on these constants. Many typical instances are already provided, so new instances can be declared with relative ease.

Minimum complete definition: `parseCWs`

Methods

parseCWs :: [CW] -> Maybe (a, [CW]) Source #

Given a sequence of constant-words, extract one instance of the type `a`, returning the remaining elements untouched. If the next element is not what's expected for this type you should return `Nothing`

cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW]) Source #

Given a parsed model instance, transform it using `f`, and return the result. The default definition for this method should be sufficient in most use cases.

parseCWs :: Read a => [CW] -> Maybe (a, [CW]) Source #

Given a sequence of constant-words, extract one instance of the type `a`, returning the remaining elements untouched. If the next element is not what's expected for this type you should return `Nothing`

Instances

SatModel Bool Source # | `Bool` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Bool, [CW]) Source # cvtModel :: (Bool -> Maybe b) -> Maybe (Bool, [CW]) -> Maybe (b, [CW]) Source #
SatModel Double Source # | `Double` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Double, [CW]) Source # cvtModel :: (Double -> Maybe b) -> Maybe (Double, [CW]) -> Maybe (b, [CW]) Source #
SatModel Float Source # | `Float` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Float, [CW]) Source # cvtModel :: (Float -> Maybe b) -> Maybe (Float, [CW]) -> Maybe (b, [CW]) Source #
SatModel Int8 Source # | `Int8` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Int8, [CW]) Source # cvtModel :: (Int8 -> Maybe b) -> Maybe (Int8, [CW]) -> Maybe (b, [CW]) Source #
SatModel Int16 Source # | `Int16` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Int16, [CW]) Source # cvtModel :: (Int16 -> Maybe b) -> Maybe (Int16, [CW]) -> Maybe (b, [CW]) Source #
SatModel Int32 Source # | `Int32` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Int32, [CW]) Source # cvtModel :: (Int32 -> Maybe b) -> Maybe (Int32, [CW]) -> Maybe (b, [CW]) Source #
SatModel Int64 Source # | `Int64` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Int64, [CW]) Source # cvtModel :: (Int64 -> Maybe b) -> Maybe (Int64, [CW]) -> Maybe (b, [CW]) Source #
SatModel Integer Source # | `Integer` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Integer, [CW]) Source # cvtModel :: (Integer -> Maybe b) -> Maybe (Integer, [CW]) -> Maybe (b, [CW]) Source #
SatModel Word8 Source # | `Word8` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Word8, [CW]) Source # cvtModel :: (Word8 -> Maybe b) -> Maybe (Word8, [CW]) -> Maybe (b, [CW]) Source #
SatModel Word16 Source # | `Word16` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Word16, [CW]) Source # cvtModel :: (Word16 -> Maybe b) -> Maybe (Word16, [CW]) -> Maybe (b, [CW]) Source #
SatModel Word32 Source # | `Word32` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Word32, [CW]) Source # cvtModel :: (Word32 -> Maybe b) -> Maybe (Word32, [CW]) -> Maybe (b, [CW]) Source #
SatModel Word64 Source # | `Word64` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (Word64, [CW]) Source # cvtModel :: (Word64 -> Maybe b) -> Maybe (Word64, [CW]) -> Maybe (b, [CW]) Source #
SatModel () Source # | Base case for `SatModel` at unit type. Comes in handy if there are no real variables.
Methods parseCWs :: [CW] -> Maybe ((), [CW]) Source # cvtModel :: (() -> Maybe b) -> Maybe ((), [CW]) -> Maybe (b, [CW]) Source #
SatModel AlgReal Source # | `AlgReal` as extracted from a model
Methods parseCWs :: [CW] -> Maybe (AlgReal, [CW]) Source # cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CW]) -> Maybe (b, [CW]) Source #
SatModel CW Source # | `CW` as extracted from a model; trivial definition
Methods parseCWs :: [CW] -> Maybe (CW, [CW]) Source # cvtModel :: (CW -> Maybe b) -> Maybe (CW, [CW]) -> Maybe (b, [CW]) Source #
SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices)
Methods parseCWs :: [CW] -> Maybe (RoundingMode, [CW]) Source # cvtModel :: (RoundingMode -> Maybe b) -> Maybe (RoundingMode, [CW]) -> Maybe (b, [CW]) Source #
SatModel Word4 Source # | SatModel instance, merely uses the generic parsing method.
Methods parseCWs :: [CW] -> Maybe (Word4, [CW]) Source # cvtModel :: (Word4 -> Maybe b) -> Maybe (Word4, [CW]) -> Maybe (b, [CW]) Source #
SatModel Location Source # |
Methods parseCWs :: [CW] -> Maybe (Location, [CW]) Source # cvtModel :: (Location -> Maybe b) -> Maybe (Location, [CW]) -> Maybe (b, [CW]) Source #
SatModel U2Member Source # |
Methods parseCWs :: [CW] -> Maybe (U2Member, [CW]) Source # cvtModel :: (U2Member -> Maybe b) -> Maybe (U2Member, [CW]) -> Maybe (b, [CW]) Source #
SatModel a => SatModel [a] Source # | A list of values as extracted from a model. When reading a list, we go as long as we can (maximal-munch). Note that this never fails, as we can always return the empty list!
Methods parseCWs :: [CW] -> Maybe ([a], [CW]) Source # cvtModel :: ([a] -> Maybe b) -> Maybe ([a], [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b) => SatModel (a, b) Source # | Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b), [CW]) Source # cvtModel :: ((a, b) -> Maybe b) -> Maybe ((a, b), [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) Source # | 3-Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b, c), [CW]) Source # cvtModel :: ((a, b, c) -> Maybe b) -> Maybe ((a, b, c), [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) Source # | 4-Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b, c, d), [CW]) Source # cvtModel :: ((a, b, c, d) -> Maybe b) -> Maybe ((a, b, c, d), [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) Source # | 5-Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b, c, d, e), [CW]) Source # cvtModel :: ((a, b, c, d, e) -> Maybe b) -> Maybe ((a, b, c, d, e), [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) Source # | 6-Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b, c, d, e, f), [CW]) Source # cvtModel :: ((a, b, c, d, e, f) -> Maybe b) -> Maybe ((a, b, c, d, e, f), [CW]) -> Maybe (b, [CW]) Source #
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) Source # | 7-Tuples extracted from a model
Methods parseCWs :: [CW] -> Maybe ((a, b, c, d, e, f, g), [CW]) Source # cvtModel :: ((a, b, c, d, e, f, g) -> Maybe b) -> Maybe ((a, b, c, d, e, f, g), [CW]) -> Maybe (b, [CW]) Source #

class Modelable a where Source #

Various SMT results that we can extract models out of.

Minimal complete definition

modelExists, getModel, getModelDictionary

Methods

modelExists :: a -> Bool Source #

Is there a model?

getModel :: SatModel b => a -> Either String (Bool, b) 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 :: a -> Map String CW Source #

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

getModelValue :: SymWord b => String -> a -> Maybe b Source #

Extract a model value for a given element. Also see `getModelValues`.

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

Extract a representative name for the model value of an uninterpreted kind. This is supposed to correspond to the value as computed internally by the SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`.

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

A simpler variant of `getModel` to get a model out without the fuss.

Instances

Modelable SMTResult Source # | `SMTResult` as a generic model provider
Methods modelExists :: SMTResult -> Bool Source # getModel :: SatModel b => SMTResult -> Either String (Bool, b) Source # getModelDictionary :: SMTResult -> Map String CW Source # getModelValue :: SymWord b => String -> SMTResult -> Maybe b Source # getModelUninterpretedValue :: String -> SMTResult -> Maybe String Source # extractModel :: SatModel b => SMTResult -> Maybe b Source #
Modelable SatResult Source # | `SatResult` as a generic model provider
Methods modelExists :: SatResult -> Bool Source # getModel :: SatModel b => SatResult -> Either String (Bool, b) Source # getModelDictionary :: SatResult -> Map String CW Source # getModelValue :: SymWord b => String -> SatResult -> Maybe b Source # getModelUninterpretedValue :: String -> SatResult -> Maybe String Source # extractModel :: SatModel b => SatResult -> Maybe b Source #
Modelable ThmResult Source # | `ThmResult` as a generic model provider
Methods modelExists :: ThmResult -> Bool Source # getModel :: SatModel b => ThmResult -> Either String (Bool, b) Source # getModelDictionary :: ThmResult -> Map String CW Source # getModelValue :: SymWord b => String -> ThmResult -> Maybe b Source # getModelUninterpretedValue :: String -> ThmResult -> Maybe String Source # extractModel :: SatModel b => ThmResult -> Maybe b Source #

displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int Source #

Given an `allSat` call, we typically want to iterate over it and print the results in sequence. The `displayModels` function automates this task by calling `disp` on each result, consecutively. The first `Int` argument to `disp` 'is the current model number. The second argument is a tuple, where the first element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)

extractModels :: SatModel a => AllSatResult -> [a] Source #

Return all the models from an `allSat` call, similar to `extractModel` but is suitable for the case of multiple results.

getModelDictionaries :: AllSatResult -> [Map String CW] Source #

Get dictionaries from an all-sat call. Similar to `getModelDictionary`.

getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b] Source #

Extract value of a variable from an all-sat call. Similar to `getModelValue`.

getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] Source #

Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`.

# SMT Interface: 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 :: Bool

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

- sBranchTimeOut :: Maybe Int

  How much time to give to the solver for each call of `sBranch` check. (In seconds. Default: No limit.)

- timeOut :: Maybe Int

  How much time to give to the solver. (In seconds. Default: No limit.)

- 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)

- solverTweaks :: [String]

  Additional lines of script to give to the solver (user specified)

- satCmd :: String

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

- isNonModelVar :: String -> Bool

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

- smtFile :: Maybe FilePath

  If Just, the generated SMT script will be put in this file (for debugging purposes mostly)

- smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

- solver :: SMTSolver

  The actual SMT solver.

- roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

- useLogic :: Maybe Logic

  If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.

Instances

Show SMTConfig Source # |
Methods showsPrec :: Int -> SMTConfig -> ShowS # show :: SMTConfig -> String # showList :: [SMTConfig] -> ShowS #

data SMTLibVersion Source #

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

Constructors

SMTLib2 |

Instances

Bounded SMTLibVersion Source # |
Methods minBound :: SMTLibVersion # maxBound :: SMTLibVersion #
Enum SMTLibVersion Source # |

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 # |
Methods (==) :: SMTLibVersion -> SMTLibVersion -> Bool # (/=) :: SMTLibVersion -> SMTLibVersion -> Bool #
Show SMTLibVersion Source # |
Methods showsPrec :: Int -> SMTLibVersion -> ShowS # show :: SMTLibVersion -> String # showList :: [SMTLibVersion] -> ShowS #
NFData SMTLibVersion Source # |
Methods rnf :: SMTLibVersion -> () #

data SMTLibLogic Source #

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the user can override this choice using the `useLogic` parameter to the configuration. This is especially handy if one is experimenting with custom logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for the official list.

Constructors

AUFLIA | Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values
AUFLIRA | Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value
AUFNIRA | Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value
LRA | Linear formulas in linear real arithmetic
QF_ABV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays
QF_AUFBV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols
QF_AUFLIA | Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols
QF_AX | Quantifier-free formulas over the theory of arrays with extensionality
QF_BV | Quantifier-free formulas over the theory of fixed-size bitvectors
QF_IDL | Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant
QF_LIA | Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables
QF_LRA | Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
QF_NIA | Quantifier-free integer arithmetic.
QF_NRA | Quantifier-free real arithmetic.
QF_RDL | Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.
QF_UF | Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.
QF_UFBV | Unquantified formulas over bitvectors with uninterpreted sort function and symbols.
QF_UFIDL | Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.
QF_UFLIA | Unquantified linear integer arithmetic with uninterpreted sort and function symbols.
QF_UFLRA | Unquantified linear real arithmetic with uninterpreted sort and function symbols.
QF_UFNRA | Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.
UFLRA | Linear real arithmetic with uninterpreted sort and function symbols.
UFNIA | Non-linear integer arithmetic with uninterpreted sort and function symbols.
QF_FPBV | Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors
QF_FP | Quantifier-free formulas over the theory of floating point numbers

Instances

Show SMTLibLogic Source # |
Methods showsPrec :: Int -> SMTLibLogic -> ShowS # show :: SMTLibLogic -> String # showList :: [SMTLibLogic] -> ShowS #

data Logic Source #

Chosen logic for the solver

Constructors

PredefinedLogic SMTLibLogic | Use one of the logics as defined by the standard
CustomLogic String | Use this name for the logic

Instances

Show Logic Source # |
Methods showsPrec :: Int -> Logic -> ShowS # show :: Logic -> String # showList :: [Logic] -> ShowS #

data OptimizeOpts Source #

Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.

Constructors

Iterative Bool | Iteratively search. if True, it will be reporting progress
Quantified | Use quantifiers

data Solver Source #

Solvers that SBV is aware of

Constructors

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

Instances

Bounded Solver Source # |
Methods minBound :: Solver # maxBound :: Solver #
Enum Solver Source # |
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 # |
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

- options :: [String]

  Options to provide to the solver

- engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

- capabilities :: SolverCapabilities

  Various capabilities of the solver

Instances

Show SMTSolver Source # |
Methods showsPrec :: Int -> SMTSolver -> ShowS # show :: SMTSolver -> String # showList :: [SMTSolver] -> ShowS #

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

sbvCurrentSolver :: SMTConfig Source #

The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.

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

data Symbolic a Source #

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

Instances

Monad Symbolic Source # |
Methods (>>=) :: Symbolic a -> (a -> Symbolic b) -> Symbolic b # (>>) :: Symbolic a -> Symbolic b -> Symbolic b # return :: a -> Symbolic a # fail :: String -> Symbolic a #
Functor Symbolic Source # |
Methods fmap :: (a -> b) -> Symbolic a -> Symbolic b # (<$) :: a -> Symbolic b -> Symbolic a #
Applicative Symbolic Source # |
Methods pure :: a -> Symbolic a # (<*>) :: Symbolic (a -> b) -> Symbolic a -> Symbolic b # (*>) :: Symbolic a -> Symbolic b -> Symbolic b # (<*) :: Symbolic a -> Symbolic b -> Symbolic a #
MonadIO Symbolic Source # |
Methods liftIO :: IO a -> Symbolic a #
Provable Predicate Source # |
Methods forAll_ :: Predicate -> Predicate Source # forAll :: [String] -> Predicate -> Predicate Source # forSome_ :: Predicate -> Predicate Source # forSome :: [String] -> Predicate -> Predicate Source #
MonadReader State Symbolic Source # |
Methods ask :: Symbolic State # local :: (State -> State) -> Symbolic a -> Symbolic a # reader :: (State -> a) -> Symbolic a #
NFData a => SExecutable (Symbolic a) Source # |
Methods sName_ :: Symbolic a -> Symbolic () Source # sName :: [String] -> Symbolic a -> Symbolic () Source #

output :: Outputtable a => a -> Symbolic a Source #

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

class (HasKind a, Ord a) => SymWord a where Source #

A `SymWord` is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with `prove`, `sat`, `allSat` etc, as default instances automatically provide the necessary bits.

Methods

forall :: String -> Symbolic (SBV a) Source #

Create a user named input (universal)

forall_ :: Symbolic (SBV a) Source #

Create an automatically named input

mkForallVars :: Int -> Symbolic [SBV a] Source #

Get a bunch of new words

exists :: String -> Symbolic (SBV a) Source #

Create an existential variable

exists_ :: Symbolic (SBV a) Source #

Create an automatically named existential variable

mkExistVars :: Int -> Symbolic [SBV a] Source #

Create a bunch of existentials

free :: String -> Symbolic (SBV a) Source #

Create a free variable, universal in a proof, existential in sat

free_ :: Symbolic (SBV a) Source #

Create an unnamed free variable, universal in proof, existential in sat

mkFreeVars :: Int -> Symbolic [SBV a] Source #

Create a bunch of free vars

symbolic :: String -> Symbolic (SBV a) Source #

Similar to free; Just a more convenient name

symbolics :: [String] -> Symbolic [SBV a] Source #

Similar to mkFreeVars; but automatically gives names based on the strings

literal :: a -> SBV a Source #

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe a Source #

Extract a literal, if the value is concrete

fromCW :: CW -> a Source #

Extract a literal, from a CW representation

isConcrete :: SBV a -> Bool Source #

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool Source #

Is the symbolic word really symbolic?

isConcretely :: SBV a -> (a -> Bool) -> Bool Source #

Does it concretely satisfy the given predicate?

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #

One stop allocator

literal :: Show a => a -> SBV a Source #

Turn a literal constant to symbolic

fromCW :: Read a => CW -> a Source #

Extract a literal, from a CW representation

mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #

One stop allocator

Instances

SymWord RoundingMode Source # | `RoundingMode` can be used symbolically

Methods

forall :: String -> Symbolic (SBV RoundingMode) Source #

forall_ :: Symbolic (SBV RoundingMode) Source #

mkForallVars :: Int -> Symbolic [SBV RoundingMode] Source #

exists :: String -> Symbolic (SBV RoundingMode) Source #

exists_ :: Symbolic (SBV RoundingMode) Source #

mkExistVars :: Int -> Symbolic [SBV RoundingMode] Source #

free :: String -> Symbolic (SBV RoundingMode) Source #

free_ :: Symbolic (SBV RoundingMode) Source #

mkFreeVars :: Int -> Symbolic [SBV RoundingMode] Source #

symbolic :: String -> Symbolic (SBV RoundingMode) Source #

symbolics :: [String] -> Symbolic [SBV RoundingMode] Source #

literal :: RoundingMode -> SBV RoundingMode Source #

unliteral :: SBV RoundingMode -> Maybe RoundingMode Source #

fromCW :: CW -> RoundingMode Source #

isConcrete :: SBV RoundingMode -> Bool Source #

isSymbolic :: SBV RoundingMode -> Bool Source #

isConcretely :: SBV RoundingMode -> (RoundingMode -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV RoundingMode) Source #

SymWord E Source # |

Methods

forall :: String -> Symbolic (SBV E) Source #

forall_ :: Symbolic (SBV E) Source #

mkForallVars :: Int -> Symbolic [SBV E] Source #

exists :: String -> Symbolic (SBV E) Source #

exists_ :: Symbolic (SBV E) Source #

mkExistVars :: Int -> Symbolic [SBV E] Source #

free :: String -> Symbolic (SBV E) Source #

free_ :: Symbolic (SBV E) Source #

mkFreeVars :: Int -> Symbolic [SBV E] Source #

symbolic :: String -> Symbolic (SBV E) Source #

symbolics :: [String] -> Symbolic [SBV E] Source #

literal :: E -> SBV E Source #

unliteral :: SBV E -> Maybe E Source #

fromCW :: CW -> E Source #

isConcrete :: SBV E -> Bool Source #

isSymbolic :: SBV E -> Bool Source #

isConcretely :: SBV E -> (E -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV E) Source #

SymWord Word4 Source # | SymWord instance, allowing this type to be used in proofs/sat etc.

Methods

forall :: String -> Symbolic (SBV Word4) Source #

forall_ :: Symbolic (SBV Word4) Source #

mkForallVars :: Int -> Symbolic [SBV Word4] Source #

exists :: String -> Symbolic (SBV Word4) Source #

exists_ :: Symbolic (SBV Word4) Source #

mkExistVars :: Int -> Symbolic [SBV Word4] Source #

free :: String -> Symbolic (SBV Word4) Source #

free_ :: Symbolic (SBV Word4) Source #

mkFreeVars :: Int -> Symbolic [SBV Word4] Source #

symbolic :: String -> Symbolic (SBV Word4) Source #

symbolics :: [String] -> Symbolic [SBV Word4] Source #

literal :: Word4 -> SBV Word4 Source #

unliteral :: SBV Word4 -> Maybe Word4 Source #

fromCW :: CW -> Word4 Source #

isConcrete :: SBV Word4 -> Bool Source #

isSymbolic :: SBV Word4 -> Bool Source #

isConcretely :: SBV Word4 -> (Word4 -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Word4) Source #

SymWord Sport Source # |

Methods

forall :: String -> Symbolic (SBV Sport) Source #

forall_ :: Symbolic (SBV Sport) Source #

mkForallVars :: Int -> Symbolic [SBV Sport] Source #

exists :: String -> Symbolic (SBV Sport) Source #

exists_ :: Symbolic (SBV Sport) Source #

mkExistVars :: Int -> Symbolic [SBV Sport] Source #

free :: String -> Symbolic (SBV Sport) Source #

free_ :: Symbolic (SBV Sport) Source #

mkFreeVars :: Int -> Symbolic [SBV Sport] Source #

symbolic :: String -> Symbolic (SBV Sport) Source #

symbolics :: [String] -> Symbolic [SBV Sport] Source #

literal :: Sport -> SBV Sport Source #

unliteral :: SBV Sport -> Maybe Sport Source #

fromCW :: CW -> Sport Source #

isConcrete :: SBV Sport -> Bool Source #

isSymbolic :: SBV Sport -> Bool Source #

isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Sport) Source #

SymWord Pet Source # |

Methods

forall :: String -> Symbolic (SBV Pet) Source #

forall_ :: Symbolic (SBV Pet) Source #

mkForallVars :: Int -> Symbolic [SBV Pet] Source #

exists :: String -> Symbolic (SBV Pet) Source #

exists_ :: Symbolic (SBV Pet) Source #

mkExistVars :: Int -> Symbolic [SBV Pet] Source #

free :: String -> Symbolic (SBV Pet) Source #

free_ :: Symbolic (SBV Pet) Source #

mkFreeVars :: Int -> Symbolic [SBV Pet] Source #

symbolic :: String -> Symbolic (SBV Pet) Source #

symbolics :: [String] -> Symbolic [SBV Pet] Source #

literal :: Pet -> SBV Pet Source #

unliteral :: SBV Pet -> Maybe Pet Source #

fromCW :: CW -> Pet Source #

isConcrete :: SBV Pet -> Bool Source #

isSymbolic :: SBV Pet -> Bool Source #

isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Pet) Source #

SymWord Beverage Source # |

Methods

forall :: String -> Symbolic (SBV Beverage) Source #

forall_ :: Symbolic (SBV Beverage) Source #

mkForallVars :: Int -> Symbolic [SBV Beverage] Source #

exists :: String -> Symbolic (SBV Beverage) Source #

exists_ :: Symbolic (SBV Beverage) Source #

mkExistVars :: Int -> Symbolic [SBV Beverage] Source #

free :: String -> Symbolic (SBV Beverage) Source #

free_ :: Symbolic (SBV Beverage) Source #

mkFreeVars :: Int -> Symbolic [SBV Beverage] Source #

symbolic :: String -> Symbolic (SBV Beverage) Source #

symbolics :: [String] -> Symbolic [SBV Beverage] Source #

literal :: Beverage -> SBV Beverage Source #

unliteral :: SBV Beverage -> Maybe Beverage Source #

fromCW :: CW -> Beverage Source #

isConcrete :: SBV Beverage -> Bool Source #

isSymbolic :: SBV Beverage -> Bool Source #

isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Beverage) Source #

SymWord Nationality Source # |

Methods

forall :: String -> Symbolic (SBV Nationality) Source #

forall_ :: Symbolic (SBV Nationality) Source #

mkForallVars :: Int -> Symbolic [SBV Nationality] Source #

exists :: String -> Symbolic (SBV Nationality) Source #

exists_ :: Symbolic (SBV Nationality) Source #

mkExistVars :: Int -> Symbolic [SBV Nationality] Source #

free :: String -> Symbolic (SBV Nationality) Source #

free_ :: Symbolic (SBV Nationality) Source #

mkFreeVars :: Int -> Symbolic [SBV Nationality] Source #

symbolic :: String -> Symbolic (SBV Nationality) Source #

symbolics :: [String] -> Symbolic [SBV Nationality] Source #

literal :: Nationality -> SBV Nationality Source #

unliteral :: SBV Nationality -> Maybe Nationality Source #

fromCW :: CW -> Nationality Source #

isConcrete :: SBV Nationality -> Bool Source #

isSymbolic :: SBV Nationality -> Bool Source #

isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Nationality) Source #

SymWord Color Source # |

Methods

forall :: String -> Symbolic (SBV Color) Source #

forall_ :: Symbolic (SBV Color) Source #

mkForallVars :: Int -> Symbolic [SBV Color] Source #

exists :: String -> Symbolic (SBV Color) Source #

exists_ :: Symbolic (SBV Color) Source #

mkExistVars :: Int -> Symbolic [SBV Color] Source #

free :: String -> Symbolic (SBV Color) Source #

free_ :: Symbolic (SBV Color) Source #

mkFreeVars :: Int -> Symbolic [SBV Color] Source #

symbolic :: String -> Symbolic (SBV Color) Source #

symbolics :: [String] -> Symbolic [SBV Color] Source #

literal :: Color -> SBV Color Source #

unliteral :: SBV Color -> Maybe Color Source #

fromCW :: CW -> Color Source #

isConcrete :: SBV Color -> Bool Source #

isSymbolic :: SBV Color -> Bool Source #

isConcretely :: SBV Color -> (Color -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color) Source #

SymWord Location Source # |

Methods

forall :: String -> Symbolic (SBV Location) Source #

forall_ :: Symbolic (SBV Location) Source #

mkForallVars :: Int -> Symbolic [SBV Location] Source #

exists :: String -> Symbolic (SBV Location) Source #

exists_ :: Symbolic (SBV Location) Source #

mkExistVars :: Int -> Symbolic [SBV Location] Source #

free :: String -> Symbolic (SBV Location) Source #

free_ :: Symbolic (SBV Location) Source #

mkFreeVars :: Int -> Symbolic [SBV Location] Source #

symbolic :: String -> Symbolic (SBV Location) Source #

symbolics :: [String] -> Symbolic [SBV Location] Source #

literal :: Location -> SBV Location Source #

unliteral :: SBV Location -> Maybe Location Source #

fromCW :: CW -> Location Source #

isConcrete :: SBV Location -> Bool Source #

isSymbolic :: SBV Location -> Bool Source #

isConcretely :: SBV Location -> (Location -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Location) Source #

SymWord U2Member Source # |

Methods

forall :: String -> Symbolic (SBV U2Member) Source #

forall_ :: Symbolic (SBV U2Member) Source #

mkForallVars :: Int -> Symbolic [SBV U2Member] Source #

exists :: String -> Symbolic (SBV U2Member) Source #

exists_ :: Symbolic (SBV U2Member) Source #

mkExistVars :: Int -> Symbolic [SBV U2Member] Source #

free :: String -> Symbolic (SBV U2Member) Source #

free_ :: Symbolic (SBV U2Member) Source #

mkFreeVars :: Int -> Symbolic [SBV U2Member] Source #

symbolic :: String -> Symbolic (SBV U2Member) Source #

symbolics :: [String] -> Symbolic [SBV U2Member] Source #

literal :: U2Member -> SBV U2Member Source #

unliteral :: SBV U2Member -> Maybe U2Member Source #

fromCW :: CW -> U2Member Source #

isConcrete :: SBV U2Member -> Bool Source #

isSymbolic :: SBV U2Member -> Bool Source #

isConcretely :: SBV U2Member -> (U2Member -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV U2Member) Source #

SymWord B Source # |

Methods

forall :: String -> Symbolic (SBV B) Source #

forall_ :: Symbolic (SBV B) Source #

mkForallVars :: Int -> Symbolic [SBV B] Source #

exists :: String -> Symbolic (SBV B) Source #

exists_ :: Symbolic (SBV B) Source #

mkExistVars :: Int -> Symbolic [SBV B] Source #

free :: String -> Symbolic (SBV B) Source #

free_ :: Symbolic (SBV B) Source #

mkFreeVars :: Int -> Symbolic [SBV B] Source #

symbolic :: String -> Symbolic (SBV B) Source #

symbolics :: [String] -> Symbolic [SBV B] Source #

literal :: B -> SBV B Source #

unliteral :: SBV B -> Maybe B Source #

fromCW :: CW -> B Source #

isConcrete :: SBV B -> Bool Source #

isSymbolic :: SBV B -> Bool Source #

isConcretely :: SBV B -> (B -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV B) Source #

SymWord Q Source # |

Methods

forall :: String -> Symbolic (SBV Q) Source #

forall_ :: Symbolic (SBV Q) Source #

mkForallVars :: Int -> Symbolic [SBV Q] Source #

exists :: String -> Symbolic (SBV Q) Source #

exists_ :: Symbolic (SBV Q) Source #

mkExistVars :: Int -> Symbolic [SBV Q] Source #

free :: String -> Symbolic (SBV Q) Source #

free_ :: Symbolic (SBV Q) Source #

mkFreeVars :: Int -> Symbolic [SBV Q] Source #

symbolic :: String -> Symbolic (SBV Q) Source #

symbolics :: [String] -> Symbolic [SBV Q] Source #

literal :: Q -> SBV Q Source #

unliteral :: SBV Q -> Maybe Q Source #

fromCW :: CW -> Q Source #

isConcrete :: SBV Q -> Bool Source #

isSymbolic :: SBV Q -> Bool Source #

isConcretely :: SBV Q -> (Q -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Q) Source #

SymWord L Source # | Declare instances to make `L` a usable uninterpreted sort. First we need the `SymWord` instance, with the default definition sufficing.

Methods

forall :: String -> Symbolic (SBV L) Source #

forall_ :: Symbolic (SBV L) Source #

mkForallVars :: Int -> Symbolic [SBV L] Source #

exists :: String -> Symbolic (SBV L) Source #

exists_ :: Symbolic (SBV L) Source #

mkExistVars :: Int -> Symbolic [SBV L] Source #

free :: String -> Symbolic (SBV L) Source #

free_ :: Symbolic (SBV L) Source #

mkFreeVars :: Int -> Symbolic [SBV L] Source #

symbolic :: String -> Symbolic (SBV L) Source #

symbolics :: [String] -> Symbolic [SBV L] Source #

literal :: L -> SBV L Source #

unliteral :: SBV L -> Maybe L Source #

fromCW :: CW -> L Source #

isConcrete :: SBV L -> Bool Source #

isSymbolic :: SBV L -> Bool Source #

isConcretely :: SBV L -> (L -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV L) Source #

# Getting SMT-Lib output (for offline analysis)

compileToSMTLib Source #

Arguments

:: Provable a |
=> SMTLibVersion | Version of SMTLib to compile to. (Only SMTLib2 supported currently.)
-> Bool | If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.)
-> a |
-> IO String |

Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library. It takes two arguments:

- version: The SMTLib-version to produce. Note that we currently only support SMTLib2.
- isSat : If `True`, will translate it as a SAT query, i.e., in the positive. If `False`, will translate as a PROVE query, i.e., it will negate the result. (In this case, the check-sat call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)

generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO () Source #

Create SMT-Lib benchmarks, for supported versions of SMTLib. The first argument is the basename of the file. 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. (See the second boolean argument to `compileToSMTLib` for details.)

# Test case generation

genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors Source #

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function `output` call to indicate what fields should be in the test result. (Also see `constrain` and `pConstrain` for filtering acceptable test values.)

getTestValues :: TestVectors -> [([CW], [CW])] Source #

Retrieve the test vectors for further processing. This function is useful in cases where `renderTest` is not sufficient and custom output (or further preprocessing) is needed.

data TestVectors Source #

Type of test vectors (abstract)

data TestStyle Source #

Test output style

Constructors

Haskell String | As a Haskell value with given name
C String | As a C array of structs with given name
Forte String Bool ([Int], [Int]) | As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values

renderTest :: TestStyle -> TestVectors -> String Source #

Render the test as a Haskell value with the given name `n`.

data CW Source #

`CW` represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the `FromBits` class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW |

Fields

- _cwKind :: !Kind
- cwVal :: !CWVal

Instances

Eq CW Source # |
Methods (==) :: CW -> CW -> Bool # (/=) :: CW -> CW -> Bool #
Ord CW Source # |
Methods compare :: CW -> CW -> Ordering # (<) :: CW -> CW -> Bool # (<=) :: CW -> CW -> Bool # (>) :: CW -> CW -> Bool # (>=) :: CW -> CW -> Bool # max :: CW -> CW -> CW # min :: CW -> CW -> CW #
Show CW Source # | Show instance for `CW`.
Methods showsPrec :: Int -> CW -> ShowS # show :: CW -> String # showList :: [CW] -> ShowS #
HasKind CW Source # | `Kind` instance for CW
Methods kindOf :: CW -> Kind Source # hasSign :: CW -> Bool Source # intSizeOf :: CW -> Int Source # isBoolean :: CW -> Bool Source # isBounded :: CW -> Bool Source # isReal :: CW -> Bool Source # isFloat :: CW -> Bool Source # isDouble :: CW -> Bool Source # isInteger :: CW -> Bool Source # isUninterpreted :: CW -> Bool Source # showType :: CW -> String Source #
PrettyNum CW Source # |
Methods hexS :: CW -> String Source # binS :: CW -> String Source # hex :: CW -> String Source # bin :: CW -> String Source #
SatModel CW Source # | `CW` as extracted from a model; trivial definition
Methods parseCWs :: [CW] -> Maybe (CW, [CW]) Source # cvtModel :: (CW -> Maybe b) -> Maybe (CW, [CW]) -> Maybe (b, [CW]) Source #
SDivisible CW Source # |
Methods sQuotRem :: CW -> CW -> (CW, CW) Source # sDivMod :: CW -> CW -> (CW, CW) Source # sQuot :: CW -> CW -> CW Source # sRem :: CW -> CW -> CW Source # sDiv :: CW -> CW -> CW Source # sMod :: CW -> CW -> CW 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. This class can be automatically derived for data-types that have a `Data` instance; this is useful for creating uninterpreted sorts.

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 #

isInteger :: a -> Bool Source #

isUninterpreted :: a -> Bool Source #

showType :: a -> String Source #

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

Instances

HasKind Bool Source # |
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 # isInteger :: Bool -> Bool Source # isUninterpreted :: Bool -> Bool Source # showType :: Bool -> String Source #
HasKind Double Source # |

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 #

isInteger :: Double -> Bool Source #

isUninterpreted :: Double -> Bool Source #

showType :: Double -> String Source #

HasKind Float Source # |
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 # isInteger :: Float -> Bool Source # isUninterpreted :: Float -> Bool Source # showType :: Float -> String Source #
HasKind Int8 Source # |
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 # isInteger :: Int8 -> Bool Source # isUninterpreted :: Int8 -> Bool Source # showType :: Int8 -> String Source #
HasKind Int16 Source # |
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 # isInteger :: Int16 -> Bool Source # isUninterpreted :: Int16 -> Bool Source # showType :: Int16 -> String Source #
HasKind Int32 Source # |
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 # isInteger :: Int32 -> Bool Source # isUninterpreted :: Int32 -> Bool Source # showType :: Int32 -> String Source #
HasKind Int64 Source # |
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 # isInteger :: Int64 -> Bool Source # isUninterpreted :: Int64 -> Bool Source # showType :: Int64 -> String Source #
HasKind Integer Source # |

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 #

isInteger :: Integer -> Bool Source #

isUninterpreted :: Integer -> Bool Source #

showType :: Integer -> String Source #

HasKind Word8 Source # |
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 # isInteger :: Word8 -> Bool Source # isUninterpreted :: Word8 -> Bool Source # showType :: Word8 -> String Source #
HasKind Word16 Source # |

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 #

isInteger :: Word16 -> Bool Source #

isUninterpreted :: Word16 -> Bool Source #

showType :: Word16 -> String Source #

HasKind Word32 Source # |

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 #

isInteger :: Word32 -> Bool Source #

isUninterpreted :: Word32 -> Bool Source #

showType :: Word32 -> String Source #

HasKind Word64 Source # |

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 #

isInteger :: Word64 -> Bool Source #

isUninterpreted :: Word64 -> Bool Source #

showType :: Word64 -> String Source #

HasKind AlgReal Source # |

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 #

isInteger :: AlgReal -> Bool Source #

isUninterpreted :: AlgReal -> Bool Source #

showType :: AlgReal -> String Source #

HasKind Kind Source # |
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 # isInteger :: Kind -> Bool Source # isUninterpreted :: Kind -> Bool Source # showType :: Kind -> String Source #
HasKind CW Source # | `Kind` instance for CW
Methods kindOf :: CW -> Kind Source # hasSign :: CW -> Bool Source # intSizeOf :: CW -> Int Source # isBoolean :: CW -> Bool Source # isBounded :: CW -> Bool Source # isReal :: CW -> Bool Source # isFloat :: CW -> Bool Source # isDouble :: CW -> Bool Source # isInteger :: CW -> Bool Source # isUninterpreted :: CW -> Bool Source # showType :: CW -> String Source #
HasKind RoundingMode Source # | `RoundingMode` kind

Methods

kindOf :: RoundingMode -> Kind Source #

hasSign :: RoundingMode -> Bool Source #

intSizeOf :: RoundingMode -> Int Source #

isBoolean :: RoundingMode -> Bool Source #

isBounded :: RoundingMode -> Bool Source #

isReal :: RoundingMode -> Bool Source #

isFloat :: RoundingMode -> Bool Source #

isDouble :: RoundingMode -> Bool Source #

isInteger :: RoundingMode -> Bool Source #

isUninterpreted :: RoundingMode -> Bool Source #

showType :: RoundingMode -> String Source #

HasKind SVal Source # |
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 # isInteger :: SVal -> Bool Source # isUninterpreted :: SVal -> Bool Source # showType :: SVal -> String Source #
HasKind SW Source # |
Methods kindOf :: SW -> Kind Source # hasSign :: SW -> Bool Source # intSizeOf :: SW -> Int Source # isBoolean :: SW -> Bool Source # isBounded :: SW -> Bool Source # isReal :: SW -> Bool Source # isFloat :: SW -> Bool Source # isDouble :: SW -> Bool Source # isInteger :: SW -> Bool Source # isUninterpreted :: SW -> Bool Source # showType :: SW -> String Source #
HasKind E Source # |
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 # isInteger :: E -> Bool Source # isUninterpreted :: E -> Bool Source # showType :: E -> String Source #
HasKind Word4 Source # | HasKind instance; simply returning the underlying kind for the type
Methods kindOf :: Word4 -> Kind Source # hasSign :: Word4 -> Bool Source # intSizeOf :: Word4 -> Int Source # isBoolean :: Word4 -> Bool Source # isBounded :: Word4 -> Bool Source # isReal :: Word4 -> Bool Source # isFloat :: Word4 -> Bool Source # isDouble :: Word4 -> Bool Source # isInteger :: Word4 -> Bool Source # isUninterpreted :: Word4 -> Bool Source # showType :: Word4 -> String Source #
HasKind Sport Source # |
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 # isInteger :: Sport -> Bool Source # isUninterpreted :: Sport -> Bool Source # showType :: Sport -> String Source #
HasKind Pet Source # |
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 # isInteger :: Pet -> Bool Source # isUninterpreted :: Pet -> Bool Source # showType :: Pet -> String Source #
HasKind Beverage Source # |

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 #

isInteger :: Beverage -> Bool Source #

isUninterpreted :: Beverage -> Bool Source #

showType :: Beverage -> String Source #

HasKind Nationality Source # |

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 #

isInteger :: Nationality -> Bool Source #

isUninterpreted :: Nationality -> Bool Source #

showType :: Nationality -> String Source #

HasKind Color Source # |
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 # isInteger :: Color -> Bool Source # isUninterpreted :: Color -> Bool Source # showType :: Color -> String Source #
HasKind Location Source # |

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 #

isInteger :: Location -> Bool Source #

isUninterpreted :: Location -> Bool Source #

showType :: Location -> String Source #

HasKind U2Member Source # |

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 #

isInteger :: U2Member -> Bool Source #

isUninterpreted :: U2Member -> Bool Source #

showType :: U2Member -> String Source #

HasKind B Source # |
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 # isInteger :: B -> Bool Source # isUninterpreted :: B -> Bool Source # showType :: B -> String Source #
HasKind Q Source # |
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 # isInteger :: Q -> Bool Source # isUninterpreted :: Q -> Bool Source # showType :: Q -> String Source #
HasKind L Source # | Similarly, `HasKind`s default implementation is sufficient.
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 # isInteger :: L -> Bool Source # isUninterpreted :: L -> Bool Source # showType :: L -> String Source #
HasKind (SBV a) Source # |
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 # isInteger :: SBV a -> Bool Source # isUninterpreted :: SBV a -> Bool Source # showType :: SBV a -> String Source #

data Kind Source #

Kind of symbolic value

Constructors

KBool |
KBounded !Bool !Int |
KUnbounded |
KReal |
KUserSort String (Either String [String]) |
KFloat |
KDouble |

Instances

Eq Kind Source # | We want to equate user-sorts only by name
Methods (==) :: Kind -> Kind -> Bool # (/=) :: Kind -> Kind -> Bool #
Ord Kind Source # | We want to order user-sorts only by name
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 # |
Methods showsPrec :: Int -> Kind -> ShowS # show :: Kind -> String # showList :: [Kind] -> ShowS #
HasKind Kind Source # |
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 # isInteger :: Kind -> Bool Source # isUninterpreted :: Kind -> Bool Source # showType :: Kind -> String Source #

cwToBool :: CW -> Bool Source #

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

# Code generation from symbolic programs

The SBV library can generate straight-line executable code in C. (While other target languages are certainly possible, currently only C is supported.) The generated code will perform no run-time memory-allocations, (no calls to `malloc`), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the same instructions in all calls, so they have predictable timing properties as well. The generated code has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling, these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing.

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

Monad SBVCodeGen Source # |
Methods (>>=) :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b # (>>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b # return :: a -> SBVCodeGen a # fail :: String -> SBVCodeGen a #
Functor SBVCodeGen Source # |
Methods fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b # (<$) :: a -> SBVCodeGen b -> SBVCodeGen a #
Applicative SBVCodeGen Source # |
Methods pure :: a -> SBVCodeGen a # (<*>) :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b # (*>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b # (<*) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a #
MonadIO SBVCodeGen Source # |
Methods liftIO :: IO a -> SBVCodeGen a #
MonadState CgState SBVCodeGen Source # |
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

cgInput :: SymWord a => String -> SBVCodeGen (SBV a) Source #

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] Source #

Creates an array input in the generated code.

## Designating outputs

cgOutput :: String -> SBV a -> SBVCodeGen () Source #

Creates an atomic output in the generated code.

cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen () Source #

Creates an array output in the generated code.

## Designating return values

cgReturn :: SBV a -> SBVCodeGen () Source #

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

cgReturnArr :: SymWord a => [SBV a] -> 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

The types `SInteger` and `SReal` are unbounded quantities that have no direct counterparts in the C language. Therefore, it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to overflow/underflows for `SInteger`, and rounding for `SReal`, so there is an implicit loss of precision.

If the user does not specify these mappings, then SBV will refuse to compile programs that involve these 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

Eq CgSRealType Source # |
Methods (==) :: CgSRealType -> CgSRealType -> Bool # (/=) :: CgSRealType -> CgSRealType -> Bool #
Show CgSRealType Source # | `Show` instance for `cgSRealType` displays values as they would be used in a C program
Methods showsPrec :: Int -> CgSRealType -> ShowS # show :: CgSRealType -> String # showList :: [CgSRealType] -> ShowS #

## Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO () 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.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO () 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.

# Module exports

The SBV library exports the following modules wholesale, as user programs will have to import these modules to make any sensible use of the SBV functionality.

module Data.Bits

module Data.Word

module Data.Int

module Data.Ratio