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.Internals

Contents

- Running symbolic programs manually
- Internal structures useful for low-level programming
- Operations useful for instantiating SBV type classes
- Polynomial operations that operate on bit-vectors
- Compilation to C
- Code generation primitives
- Various math utilities around floats

Description

Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.

Synopsis

- data Result = Result {
  - reskinds :: Set Kind
  - resTraces :: [(String, CW)]
  - resUISegs :: [(String, [String])]
  - resInputs :: [(Quantifier, NamedSymVar)]
  - resConsts :: [(SW, CW)]
  - resTables :: [((Int, Kind, Kind), [SW])]
  - resArrays :: [(Int, ArrayInfo)]
  - resUIConsts :: [(String, SBVType)]
  - resAxioms :: [(String, [String])]
  - resAsgns :: SBVPgm
  - resConstraints :: [SW]
  - resAssertions :: [(String, Maybe CallStack, SW)]
  - resOutputs :: [SW]
  }
- data SBVRunMode
  - = Proof (Bool, SMTConfig)
  - | CodeGen
  - | Concrete StdGen
- 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 SReal = SBV AlgReal
- type SFloat = SBV Float
- type SDouble = SBV Double
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymWord a) => SBV a
- sInfinity :: (Floating a, SymWord a) => SBV a
- data RoundingMode
  - = RoundNearestTiesToEven
  - | RoundNearestTiesToAway
  - | RoundTowardPositive
  - | RoundTowardNegative
  - | RoundTowardZero
- type SRoundingMode = SBV RoundingMode
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class (HasKind a, Ord a) => SymWord a where
- data CW = CW {
  - _cwKind :: !Kind
  - cwVal :: !CWVal
  }
- data CWVal
  - = CWAlgReal !AlgReal
  - | CWInteger !Integer
  - | CWFloat !Float
  - | CWDouble !Double
  - | CWUserSort !(Maybe Int, String)
- data AlgReal
  - = AlgRational Bool Rational
  - | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- cwSameType :: CW -> CW -> Bool
- cwToBool :: CW -> Bool
- mkConstCW :: Integral a => Kind -> a -> CW
- liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b
- mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW
- mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW
- data SW = SW !Kind !NodeId
- trueSW :: SW
- falseSW :: SW
- trueCW :: CW
- falseCW :: CW
- normCW :: CW -> CW
- data SVal = SVal !Kind !(Either CW (Cached SW))
- newtype SBV a = SBV {
  - unSBV :: SVal
  }
- newtype NodeId = NodeId Int
- mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
- data ArrayContext
  - = ArrayFree (Maybe SW)
  - | ArrayReset Int SW
  - | ArrayMutate Int SW SW
  - | ArrayMerge SW Int Int
- type ArrayInfo = (String, (Kind, Kind), ArrayContext)
- class SymArray array where
- newtype SFunArray a b = SFunArray (SBV a -> SBV b)
- mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
- newtype SArray a b = SArray {
  - unSArray :: SArr
  }
- sbvToSW :: State -> SBV a -> IO SW
- sbvToSymSW :: SBV a -> Symbolic SW
- forceSWArg :: SW -> IO ()
- data SBVExpr = SBVApp !Op ![SW]
- newExpr :: State -> Kind -> SBVExpr -> IO SW
- cache :: (State -> IO a) -> Cached a
- data Cached a
- uncache :: Cached SW -> State -> IO SW
- uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
- class HasKind a where
- data Op
  - = Plus
  - | Times
  - | Minus
  - | UNeg
  - | Abs
  - | Quot
  - | Rem
  - | Equal
  - | NotEqual
  - | LessThan
  - | GreaterThan
  - | LessEq
  - | GreaterEq
  - | Ite
  - | And
  - | Or
  - | XOr
  - | Not
  - | Shl Int
  - | Shr Int
  - | Rol Int
  - | Ror Int
  - | Extract Int Int
  - | Join
  - | LkUp (Int, Kind, Kind, Int) !SW !SW
  - | ArrEq Int Int
  - | ArrRead Int
  - | KindCast Kind Kind
  - | Uninterpreted String
  - | Label String
  - | IEEEFP FPOp
- data FPOp
  - = FP_Cast Kind Kind SW
  - | FP_Reinterpret Kind Kind
  - | FP_Abs
  - | FP_Neg
  - | FP_Add
  - | FP_Sub
  - | FP_Mul
  - | FP_Div
  - | FP_FMA
  - | FP_Sqrt
  - | FP_Rem
  - | FP_RoundToIntegral
  - | FP_Min
  - | FP_Max
  - | FP_ObjEqual
  - | FP_IsNormal
  - | FP_IsSubnormal
  - | FP_IsZero
  - | FP_IsInfinite
  - | FP_IsNaN
  - | FP_IsNegative
  - | FP_IsPositive
- type NamedSymVar = (SW, String)
- getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
- newtype SBVPgm = SBVPgm {
  - pgmAssignments :: Seq (SW, SBVExpr)
  }
- data Symbolic a
- class SExecutable a where
- runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result
- runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
- data State
- getPathCondition :: State -> SBool
- extendPathCondition :: State -> (SBool -> SBool) -> State
- inProofMode :: State -> Bool
- data SBVRunMode
  - = Proof (Bool, SMTConfig)
  - | CodeGen
  - | Concrete StdGen
- data Kind
  - = KBool
  - | KBounded !Bool !Int
  - | KUnbounded
  - | KReal
  - | KUserSort String (Either String [String])
  - | KFloat
  - | KDouble
- class Outputtable a where
- data Result = Result {
  - reskinds :: Set Kind
  - resTraces :: [(String, CW)]
  - resUISegs :: [(String, [String])]
  - resInputs :: [(Quantifier, NamedSymVar)]
  - resConsts :: [(SW, CW)]
  - resTables :: [((Int, Kind, Kind), [SW])]
  - resArrays :: [(Int, ArrayInfo)]
  - resUIConsts :: [(String, SBVType)]
  - resAxioms :: [(String, [String])]
  - resAsgns :: SBVPgm
  - resConstraints :: [SW]
  - resAssertions :: [(String, Maybe CallStack, SW)]
  - resOutputs :: [SW]
  }
- data Logic
  - = PredefinedLogic SMTLibLogic
  - | CustomLogic String
- 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
- addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic ()
- internalVariable :: State -> Kind -> IO SW
- internalConstraint :: State -> SVal -> IO ()
- isCodeGenMode :: State -> Bool
- newtype SBVType = SBVType [Kind]
- newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
- addAxiom :: String -> [String] -> Symbolic ()
- data Quantifier
  - = ALL
  - | EX
- needsExistentials :: [Quantifier] -> Bool
- data SMTLibPgm = SMTLibPgm SMTLibVersion ([(String, SW)], [String], [String])
- data SMTLibVersion = SMTLib2
- smtLibVersionExtension :: SMTLibVersion -> String
- smtLibReservedNames :: [String]
- data SolverCapabilities = SolverCapabilities {
  - capSolverName :: String
  - mbDefaultLogic :: Bool -> Maybe String
  - supportsMacros :: Bool
  - supportsProduceModels :: Bool
  - supportsQuantifiers :: Bool
  - supportsUninterpretedSorts :: Bool
  - supportsUnboundedInts :: Bool
  - supportsReals :: Bool
  - supportsFloats :: Bool
  - supportsDoubles :: Bool
  }
- extractSymbolicSimulationState :: State -> IO Result
- data SMTScript = SMTScript {
  - scriptBody :: String
  - scriptModel :: Maybe String
  }
- data Solver
  - = Z3
  - | Yices
  - | Boolector
  - | CVC4
  - | MathSAT
  - | ABC
- data SMTSolver = SMTSolver {
  - name :: Solver
  - executable :: String
  - options :: [String]
  - engine :: SMTEngine
  - capabilities :: SolverCapabilities
  }
- data SMTResult
  - = Unsatisfiable SMTConfig
  - | Satisfiable SMTConfig SMTModel
  - | Unknown SMTConfig SMTModel
  - | ProofError SMTConfig [String]
  - | TimeOut SMTConfig
- newtype SMTModel = SMTModel {
  - modelAssocs :: [(String, CW)]
  }
- 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
  }
- getSBranchRunConfig :: State -> Maybe SMTConfig
- declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b)
- declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b)
- genLiteral :: Integral a => Kind -> a -> SBV b
- genFromCW :: Integral a => CW -> a
- genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
- checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- showModel :: SMTConfig -> SMTModel -> String
- newtype SMTModel = SMTModel {
  - modelAssocs :: [(String, CW)]
  }
- liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
- ites :: SBool -> [SBool] -> [SBool] -> [SBool]
- mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
- addPoly :: [SBool] -> [SBool] -> [SBool]
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- class CgTarget a where
- data CgConfig = CgConfig {
  - cgRTC :: Bool
  - cgInteger :: Maybe Int
  - cgReal :: Maybe CgSRealType
  - cgDriverVals :: [Integer]
  - cgGenDriver :: Bool
  - cgGenMakefile :: Bool
  - cgIgnoreAsserts :: Bool
  }
- defaultCgConfig :: CgConfig
- data CgVal
  - = CgAtomic SW
  - | CgArray [SW]
- data CgState = CgState {
  - cgInputs :: [(String, CgVal)]
  - cgOutputs :: [(String, CgVal)]
  - cgReturns :: [CgVal]
  - cgPrototypes :: [String]
  - cgDecls :: [String]
  - cgLDFlags :: [String]
  - cgFinalConfig :: CgConfig
  }
- initCgState :: CgState
- newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
- liftSymbolic :: Symbolic a -> SBVCodeGen a
- cgSBVToSW :: SBV a -> SBVCodeGen SW
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- data CgSRealType
  - = CgFloat
  - | CgDouble
  - | CgLongDouble
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- svCgInput :: Kind -> String -> SBVCodeGen SVal
- svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
- svCgOutput :: String -> SVal -> SBVCodeGen ()
- svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
- svCgReturn :: SVal -> SBVCodeGen ()
- svCgReturnArr :: [SVal] -> SBVCodeGen ()
- 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 ()
- data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
  - = CgMakefile [String]
  - | CgHeader [Doc]
  - | CgSource
  - | CgDriver
- isCgDriver :: CgPgmKind -> Bool
- isCgMakefile :: CgPgmKind -> Bool
- codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
- renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
- render' :: Doc -> String
- fpRound0 :: (RealFloat a, Integral b) => a -> b
- fpRatio0 :: RealFloat a => a -> Rational
- fpMaxH :: RealFloat a => a -> a -> a
- fpMinH :: RealFloat a => a -> a -> a
- fp2fp :: (RealFloat a, RealFloat b) => a -> b
- fpRemH :: RealFloat a => a -> a -> a
- fpRoundToIntegralH :: RealFloat a => a -> a
- fpIsEqualObjectH :: RealFloat a => a -> a -> Bool
- fpIsNormalizedH :: RealFloat a => a -> Bool

# Running symbolic programs manually

data Result Source #

Result of running a symbolic computation

Constructors

Result |

Fields

- reskinds :: Set Kind

  kinds used in the program

- resTraces :: [(String, CW)]

  quick-check counter-example information (if any)

- resUISegs :: [(String, [String])]

  uninterpeted code segments

- resInputs :: [(Quantifier, NamedSymVar)]

  inputs (possibly existential)

- resConsts :: [(SW, CW)]

  constants

- resTables :: [((Int, Kind, Kind), [SW])]

  tables (automatically constructed) (tableno, index-type, result-type) elts

- resArrays :: [(Int, ArrayInfo)]

  arrays (user specified)

- resUIConsts :: [(String, SBVType)]

  uninterpreted constants

- resAxioms :: [(String, [String])]

  axioms

- resAsgns :: SBVPgm

  assignments

- resConstraints :: [SW]

  additional constraints (boolean)

- resAssertions :: [(String, Maybe CallStack, SW)]

  assertions

- resOutputs :: [SW]

  outputs

Instances

Show Result Source # | Show instance for `Result`. Only for debugging purposes.
Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #
NFData Result Source # |
Methods rnf :: Result -> () #

data SBVRunMode Source #

Different means of running a symbolic piece of code

Constructors

Proof (Bool, SMTConfig) | Fully Symbolic, proof mode.
CodeGen | Code generation mode.
Concrete StdGen | Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs.

# Internal structures useful for low-level programming

type SBool = SBV Bool Source #

A symbolic boolean/bit

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

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

type SInteger = SBV Integer Source #

Infinite precision signed symbolic value

type SReal = SBV AlgReal Source #

Infinite precision symbolic algebraic real value

type SFloat = SBV Float Source #

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double Source #

IEEE-754 double-precision floating point numbers

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`.

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`

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`

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 #

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 #

data CWVal Source #

A constant value

Constructors

CWAlgReal !AlgReal | algebraic real
CWInteger !Integer | bit-vector/unbounded integer
CWFloat !Float | float
CWDouble !Double | double
CWUserSort !(Maybe Int, String) | value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations

Instances

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

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

Constructors

AlgRational Bool Rational |
AlgPolyRoot (Integer, Polynomial) (Maybe String) |

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 #

cwSameType :: CW -> CW -> Bool Source #

Are two CW's of the same type?

cwToBool :: CW -> Bool Source #

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

mkConstCW :: Integral a => Kind -> a -> CW Source #

Create a constant word from an integral.

liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b Source #

Lift a binary function through a CW

mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW Source #

Map a unary function through a CW.

mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW Source #

Map a binary function through a CW.

data SW Source #

A symbolic word, tracking it's signedness and size.

Constructors

SW !Kind !NodeId |

Instances

Eq SW Source # |
Methods (==) :: SW -> SW -> Bool # (/=) :: SW -> SW -> Bool #
Ord SW Source # |
Methods compare :: SW -> SW -> Ordering # (<) :: SW -> SW -> Bool # (<=) :: SW -> SW -> Bool # (>) :: SW -> SW -> Bool # (>=) :: SW -> SW -> Bool # max :: SW -> SW -> SW # min :: SW -> SW -> SW #
Show SW Source # |
Methods showsPrec :: Int -> SW -> ShowS # show :: SW -> String # showList :: [SW] -> ShowS #
NFData SW Source # |
Methods rnf :: SW -> () #
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 #

trueSW :: SW Source #

Constant True as an SW. Note that this value always occupies slot -1.

falseSW :: SW Source #

Constant False as an SW. Note that this value always occupies slot -2.

trueCW :: CW Source #

Constant True as a CW. We represent it using the integer value 1.

falseCW :: CW Source #

Constant False as a CW. We represent it using the integer value 0.

normCW :: CW -> CW Source #

Normalize a CW. Essentially performs modular arithmetic to make sure the value can fit in the given bit-size. Note that this is rather tricky for negative values, due to asymmetry. (i.e., an 8-bit negative number represents values in the range -128 to 127; thus we have to be careful on the negative side.)

data SVal Source #

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

Constructors

SVal !Kind !(Either CW (Cached SW)) |

Instances

Eq SVal Source # | Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do.
Methods (==) :: SVal -> SVal -> Bool # (/=) :: SVal -> SVal -> Bool #
Show SVal Source # | Show instance for `SVal`. Not particularly "desirable", but will do if needed NB. We do not show the type info on constant KBool values, since there's no implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)
Methods showsPrec :: Int -> SVal -> ShowS # show :: SVal -> String # showList :: [SVal] -> ShowS #
NFData SVal Source # |
Methods rnf :: SVal -> () #
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 #

newtype SBV a Source #

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

Constructors

SBV |

Fields

- unSBV :: SVal

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 #

newtype NodeId Source #

A symbolic node id

Constructors

NodeId Int |

Instances

Eq NodeId Source # |
Methods (==) :: NodeId -> NodeId -> Bool # (/=) :: NodeId -> NodeId -> Bool #
Ord NodeId Source # |
Methods compare :: NodeId -> NodeId -> Ordering # (<) :: NodeId -> NodeId -> Bool # (<=) :: NodeId -> NodeId -> Bool # (>) :: NodeId -> NodeId -> Bool # (>=) :: NodeId -> NodeId -> Bool # max :: NodeId -> NodeId -> NodeId # min :: NodeId -> NodeId -> NodeId #

mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) Source #

Create a symbolic variable.

data ArrayContext Source #

The context of a symbolic array as created

Constructors

ArrayFree (Maybe SW) | A new array, with potential initializer for each cell
ArrayReset Int SW | An array created from another array by fixing each element to another value
ArrayMutate Int SW SW | An array created by mutating another array at a given cell
ArrayMerge SW Int Int | An array created by symbolically merging two other arrays

Instances

Show ArrayContext Source # |
Methods showsPrec :: Int -> ArrayContext -> ShowS # show :: ArrayContext -> String # showList :: [ArrayContext] -> ShowS #
NFData ArrayContext Source # |
Methods rnf :: ArrayContext -> () #

type ArrayInfo = (String, (Kind, Kind), ArrayContext) Source #

Representation for symbolic arrays

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 #

newtype 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

Constructors

SFunArray (SBV a -> SBV b) |

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

newtype 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

Constructors

SArray |

Fields

- unSArray :: SArr

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 #

sbvToSW :: State -> SBV a -> IO SW Source #

Convert a symbolic value to a symbolic-word

sbvToSymSW :: SBV a -> Symbolic SW Source #

Convert a symbolic value to an SW, inside the Symbolic monad

forceSWArg :: SW -> IO () Source #

Forcing an argument; this is a necessary evil to make sure all the arguments to an uninterpreted function and sBranch test conditions are evaluated before called; the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's

data SBVExpr Source #

A symbolic expression

Constructors

SBVApp !Op ![SW] |

Instances

Eq SBVExpr Source # |
Methods (==) :: SBVExpr -> SBVExpr -> Bool # (/=) :: SBVExpr -> SBVExpr -> Bool #
Ord SBVExpr Source # |
Methods compare :: SBVExpr -> SBVExpr -> Ordering # (<) :: SBVExpr -> SBVExpr -> Bool # (<=) :: SBVExpr -> SBVExpr -> Bool # (>) :: SBVExpr -> SBVExpr -> Bool # (>=) :: SBVExpr -> SBVExpr -> Bool # max :: SBVExpr -> SBVExpr -> SBVExpr # min :: SBVExpr -> SBVExpr -> SBVExpr #
Show SBVExpr Source # | Show instance for `SBVExpr`. Again, only for debugging purposes.
Methods showsPrec :: Int -> SBVExpr -> ShowS # show :: SBVExpr -> String # showList :: [SBVExpr] -> ShowS #
NFData SBVExpr Source # |
Methods rnf :: SBVExpr -> () #

newExpr :: State -> Kind -> SBVExpr -> IO SW Source #

Create a new expression; hash-cons as necessary

cache :: (State -> IO a) -> Cached a Source #

Cache a state-based computation

data Cached a Source #

We implement a peculiar caching mechanism, applicable to the use case in implementation of SBV's. Whenever we do a state based computation, we do not want to keep on evaluating it in the then-current state. That will produce essentially a semantically equivalent value. Thus, we want to run it only once, and reuse that result, capturing the sharing at the Haskell level. This is similar to the "type-safe observable sharing" work, but also takes into the account of how symbolic simulation executes.

See Andy Gill's type-safe obervable sharing trick for the inspiration behind this technique: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09

Note that this is *not* a general memo utility!

Instances

NFData (Cached a) Source # |
Methods rnf :: Cached a -> () #

uncache :: Cached SW -> State -> IO SW Source #

Uncache a previously cached computation

uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex Source #

Uncache, retrieving array indexes

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 Op Source #

Symbolic operations

Constructors

Plus |
Times |
Minus |
UNeg |
Abs |
Quot |
Rem |
Equal |
NotEqual |
LessThan |
GreaterThan |
LessEq |
GreaterEq |
Ite |
And |
Or |
XOr |
Not |
Shl Int |
Shr Int |
Rol Int |
Ror Int |
Extract Int Int |
Join |
LkUp (Int, Kind, Kind, Int) !SW !SW |
ArrEq Int Int |
ArrRead Int |
KindCast Kind Kind |
Uninterpreted String |
Label String |
IEEEFP FPOp |

Instances

Eq Op Source # |
Methods (==) :: Op -> Op -> Bool # (/=) :: Op -> Op -> Bool #
Ord Op Source # |
Methods compare :: Op -> Op -> Ordering # (<) :: Op -> Op -> Bool # (<=) :: Op -> Op -> Bool # (>) :: Op -> Op -> Bool # (>=) :: Op -> Op -> Bool # max :: Op -> Op -> Op # min :: Op -> Op -> Op #
Show Op Source # | Show instance for `Op`. Note that this is largely for debugging purposes, not used for being read by any tool.
Methods showsPrec :: Int -> Op -> ShowS # show :: Op -> String # showList :: [Op] -> ShowS #

data FPOp Source #

Floating point operations

Constructors

FP_Cast Kind Kind SW |
FP_Reinterpret Kind Kind |
FP_Abs |
FP_Neg |
FP_Add |
FP_Sub |
FP_Mul |
FP_Div |
FP_FMA |
FP_Sqrt |
FP_Rem |
FP_RoundToIntegral |
FP_Min |
FP_Max |
FP_ObjEqual |
FP_IsNormal |
FP_IsSubnormal |
FP_IsZero |
FP_IsInfinite |
FP_IsNaN |
FP_IsNegative |
FP_IsPositive |

Instances

Eq FPOp Source # |
Methods (==) :: FPOp -> FPOp -> Bool # (/=) :: FPOp -> FPOp -> Bool #
Ord FPOp Source # |
Methods compare :: FPOp -> FPOp -> Ordering # (<) :: FPOp -> FPOp -> Bool # (<=) :: FPOp -> FPOp -> Bool # (>) :: FPOp -> FPOp -> Bool # (>=) :: FPOp -> FPOp -> Bool # max :: FPOp -> FPOp -> FPOp # min :: FPOp -> FPOp -> FPOp #
Show FPOp Source # | Note that the show instance maps to the SMTLib names. We need to make sure this mapping stays correct through SMTLib changes. The only exception is FP_Cast; where we handle different source/origins explicitly later on.
Methods showsPrec :: Int -> FPOp -> ShowS # show :: FPOp -> String # showList :: [FPOp] -> ShowS #

type NamedSymVar = (SW, String) Source #

`NamedSymVar` pairs symbolic words and user given/automatically generated names

getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int Source #

Create a new table; hash-cons as necessary

newtype SBVPgm Source #

A program is a sequence of assignments

Constructors

SBVPgm |

Fields

- pgmAssignments :: Seq (SW, SBVExpr)

Instances

NFData SBVPgm Source # |
Methods rnf :: SBVPgm -> () #

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 #

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 #

runSymbolic :: (Bool, SMTConfig) -> Symbolic a -> IO Result Source #

Run a symbolic computation in Proof mode and return a `Result`. The boolean argument indicates if this is a sat instance or not.

runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result) Source #

Run a symbolic computation, and return a extra value paired up with the `Result`

data State Source #

The state of the symbolic interpreter

Instances

MonadReader State Symbolic Source # |
Methods ask :: Symbolic State # local :: (State -> State) -> Symbolic a -> Symbolic a # reader :: (State -> a) -> Symbolic a #

getPathCondition :: State -> SBool Source #

Get the current path condition

extendPathCondition :: State -> (SBool -> SBool) -> State Source #

Extend the path condition with the given test value.

inProofMode :: State -> Bool Source #

Are we running in proof mode?

data SBVRunMode Source #

Different means of running a symbolic piece of code

Constructors

Proof (Bool, SMTConfig) | Fully Symbolic, proof mode.
CodeGen | Code generation mode.
Concrete StdGen | Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs.

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 #

class Outputtable a where Source #

A class representing what can be returned from a symbolic computation.

Minimal complete definition

output

Methods

output :: 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.

Instances

Outputtable () Source # |
Methods output :: () -> Symbolic () Source #
Outputtable a => Outputtable [a] Source # |
Methods output :: [a] -> Symbolic [a] Source #
Outputtable (SBV a) Source # |
Methods output :: SBV a -> Symbolic (SBV a) Source #
(Outputtable a, Outputtable b) => Outputtable (a, b) Source # |
Methods output :: (a, b) -> Symbolic (a, b) Source #
(Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) Source # |
Methods output :: (a, b, c) -> Symbolic (a, b, c) Source #
(Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) Source # |
Methods output :: (a, b, c, d) -> Symbolic (a, b, c, d) Source #
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) Source # |
Methods output :: (a, b, c, d, e) -> Symbolic (a, b, c, d, e) Source #
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) Source # |
Methods output :: (a, b, c, d, e, f) -> Symbolic (a, b, c, d, e, f) Source #
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) Source # |
Methods output :: (a, b, c, d, e, f, g) -> Symbolic (a, b, c, d, e, f, g) Source #
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) Source # |
Methods output :: (a, b, c, d, e, f, g, h) -> Symbolic (a, b, c, d, e, f, g, h) Source #

data Result Source #

Result of running a symbolic computation

Constructors

Result |

Fields

- reskinds :: Set Kind

  kinds used in the program

- resTraces :: [(String, CW)]

  quick-check counter-example information (if any)

- resUISegs :: [(String, [String])]

  uninterpeted code segments

- resInputs :: [(Quantifier, NamedSymVar)]

  inputs (possibly existential)

- resConsts :: [(SW, CW)]

  constants

- resTables :: [((Int, Kind, Kind), [SW])]

  tables (automatically constructed) (tableno, index-type, result-type) elts

- resArrays :: [(Int, ArrayInfo)]

  arrays (user specified)

- resUIConsts :: [(String, SBVType)]

  uninterpreted constants

- resAxioms :: [(String, [String])]

  axioms

- resAsgns :: SBVPgm

  assignments

- resConstraints :: [SW]

  additional constraints (boolean)

- resAssertions :: [(String, Maybe CallStack, SW)]

  assertions

- resOutputs :: [SW]

  outputs

Instances

Show Result Source # | Show instance for `Result`. Only for debugging purposes.
Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #
NFData Result Source # |
Methods rnf :: Result -> () #

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

addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic () Source #

Add a constraint with a given probability

internalVariable :: State -> Kind -> IO SW Source #

Create an internal variable, which acts as an input but isn't visible to the user. Such variables are existentially quantified in a SAT context, and universally quantified in a proof context.

internalConstraint :: State -> SVal -> IO () Source #

Require a boolean condition to be true in the state. Only used for internal purposes.

isCodeGenMode :: State -> Bool Source #

Is this a CodeGen run? (i.e., generating code)

newtype SBVType Source #

A simple type for SBV computations, used mainly for uninterpreted constants. We keep track of the signedness/size of the arguments. A non-function will have just one entry in the list.

Constructors

SBVType [Kind] |

Instances

Eq SBVType Source # |
Methods (==) :: SBVType -> SBVType -> Bool # (/=) :: SBVType -> SBVType -> Bool #
Ord SBVType Source # |
Methods compare :: SBVType -> SBVType -> Ordering # (<) :: SBVType -> SBVType -> Bool # (<=) :: SBVType -> SBVType -> Bool # (>) :: SBVType -> SBVType -> Bool # (>=) :: SBVType -> SBVType -> Bool # max :: SBVType -> SBVType -> SBVType # min :: SBVType -> SBVType -> SBVType #
Show SBVType Source # |
Methods showsPrec :: Int -> SBVType -> ShowS # show :: SBVType -> String # showList :: [SBVType] -> ShowS #
NFData SBVType Source # |
Methods rnf :: SBVType -> () #

newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () Source #

Create a new uninterpreted symbol, possibly with user given code

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.

data Quantifier Source #

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

Constructors

ALL |
EX |

Instances

Eq Quantifier Source # |
Methods (==) :: Quantifier -> Quantifier -> Bool # (/=) :: Quantifier -> Quantifier -> Bool #
NFData Quantifier Source # |
Methods rnf :: Quantifier -> () #

needsExistentials :: [Quantifier] -> Bool Source #

Are there any existential quantifiers?

data SMTLibPgm Source #

Representation of an SMT-Lib program. In between pre and post goes the refuted models

Constructors

SMTLibPgm SMTLibVersion ([(String, SW)], [String], [String]) |

Instances

Show SMTLibPgm Source # |
Methods showsPrec :: Int -> SMTLibPgm -> ShowS # show :: SMTLibPgm -> String # showList :: [SMTLibPgm] -> ShowS #
NFData SMTLibPgm Source # |
Methods rnf :: SMTLibPgm -> () #

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

smtLibVersionExtension :: SMTLibVersion -> String Source #

The extension associated with the version

smtLibReservedNames :: [String] Source #

Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course there's no guarantee it'll stay that way.

data SolverCapabilities Source #

Translation tricks needed for specific capabilities afforded by each solver

Constructors

SolverCapabilities |

Fields

- capSolverName :: String

  Name of the solver

- mbDefaultLogic :: Bool -> Maybe String

  set-logic string to use in case not automatically determined (if any). If Bool is True, then reals are present.

- supportsMacros :: Bool

  Does the solver understand SMT-Lib2 macros?

- supportsProduceModels :: Bool

  Does the solver understand produce-models option setting

- supportsQuantifiers :: Bool

  Does the solver understand SMT-Lib2 style quantifiers?

- supportsUninterpretedSorts :: Bool

  Does the solver understand SMT-Lib2 style uninterpreted-sorts

- supportsUnboundedInts :: Bool

  Does the solver support unbounded integers?

- supportsReals :: Bool

  Does the solver support reals?

- supportsFloats :: Bool

  Does the solver support single-precision floating point numbers?

- supportsDoubles :: Bool

  Does the solver support double-precision floating point numbers?

extractSymbolicSimulationState :: State -> IO Result Source #

Grab the program from a running symbolic simulation state. This is useful for internal purposes, for instance when implementing `sBranch`.

data SMTScript Source #

A script, to be passed to the solver.

Constructors

SMTScript |

Fields

- scriptBody :: String

  Initial feed

- scriptModel :: Maybe String

  Optional continuation script, if the result is sat

Instances

NFData SMTScript Source # |
Methods rnf :: SMTScript -> () #

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 #

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 #

newtype SMTModel Source #

A model, as returned by a solver

Constructors

SMTModel |

Fields

- modelAssocs :: [(String, CW)]

  Mapping of symbolic values to constants.

Instances

Show SMTModel Source # |
Methods showsPrec :: Int -> SMTModel -> ShowS # show :: SMTModel -> String # showList :: [SMTModel] -> ShowS #
NFData SMTModel Source # |
Methods rnf :: SMTModel -> () #

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 #

getSBranchRunConfig :: State -> Maybe SMTConfig Source #

If in proof mode, get the underlying configuration (used for `sBranch`)

declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b) Source #

Declare a new symbolic array, with a potential initial value

declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b) Source #

Declare a new functional symbolic array, with a potential initial value. Note that a read from an uninitialized cell will result in an error.

# Operations useful for instantiating SBV type classes

genLiteral :: Integral a => Kind -> a -> SBV b Source #

Generate a finite constant bitvector

genFromCW :: Integral a => CW -> a Source #

Convert a constant to an integral value

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

Generically make a symbolic var

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

Perform a sanity check that we should receive precisely the same number of bits as required by the resulting type. The input is little-endian

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

Parse a signed/sized value from a sequence of CWs

showModel :: SMTConfig -> SMTModel -> String Source #

Show a model in human readable form. Ignore bindings to those variables that start with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes

newtype SMTModel Source #

A model, as returned by a solver

Constructors

SMTModel |

Fields

- modelAssocs :: [(String, CW)]

  Mapping of symbolic values to constants.

Instances

Show SMTModel Source # |
Methods showsPrec :: Int -> SMTModel -> ShowS # show :: SMTModel -> String # showList :: [SMTModel] -> ShowS #
NFData SMTModel Source # |
Methods rnf :: SMTModel -> () #

liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) Source #

Lift `QRem` to symbolic words. Division by 0 is defined s.t. `x/0 = 0`; which holds even when `x` is `0` itself.

liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) Source #

Lift `DMod` to symbolic words. Division by 0 is defined s.t. `x/0 = 0`; which holds even when `x` is `0` itself. Essentially, this is conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)

# Polynomial operations that operate on bit-vectors

ites :: SBool -> [SBool] -> [SBool] -> [SBool] Source #

Run down a boolean condition over two lists. Note that this is different than zipWith as shorter list is assumed to be filled with false at the end (i.e., zero-bits); which nicely pads it when considered as an unsigned number in little-endian form.

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) Source #

Compute modulus/remainder of polynomials on bit-vectors.

addPoly :: [SBool] -> [SBool] -> [SBool] Source #

Add two polynomials

# Compilation to C

compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle Source #

Lower level version of `compileToC`, producing a `CgPgmBundle`

compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle Source #

Lower level version of `compileToCLib`, producing a `CgPgmBundle`

# Code generation primitives

class CgTarget a where Source #

Abstract over code generation for different languages

Minimal complete definition

targetName, translate

Methods

targetName :: a -> String Source #

translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle Source #

data CgConfig Source #

Options for code-generation.

Constructors

CgConfig |

Fields

- cgRTC :: Bool

  If `True`, perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.

- cgInteger :: Maybe Int

  Bit-size to use for representing SInteger (if any)

- cgReal :: Maybe CgSRealType

  Type to use for representing SReal (if any)

- cgDriverVals :: [Integer]

  Values to use for the driver program generated, useful for generating non-random drivers.

- cgGenDriver :: Bool

  If `True`, will generate a driver program

- cgGenMakefile :: Bool

  If `True`, will generate a makefile

- cgIgnoreAsserts :: Bool

  If `True`, will ignore `sAssert` calls

defaultCgConfig :: CgConfig Source #

Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.

data CgVal Source #

Abstraction of target language values

Constructors

CgAtomic SW |
CgArray [SW] |

data CgState Source #

Code-generation state

Constructors

CgState |

Fields

- cgInputs :: [(String, CgVal)]
- cgOutputs :: [(String, CgVal)]
- cgReturns :: [CgVal]
- cgPrototypes :: [String]
- cgDecls :: [String]
- cgLDFlags :: [String]
- cgFinalConfig :: CgConfig

Instances

MonadState CgState SBVCodeGen Source # |
Methods get :: SBVCodeGen CgState # put :: CgState -> SBVCodeGen () # state :: (CgState -> (a, CgState)) -> SBVCodeGen a #

initCgState :: CgState Source #

Initial configuration for code-generation

newtype 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.

Constructors

SBVCodeGen (StateT CgState Symbolic a) |

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 #

liftSymbolic :: Symbolic a -> SBVCodeGen a Source #

Reach into symbolic monad from code-generation

cgSBVToSW :: SBV a -> SBVCodeGen SW Source #

Reach into symbolic monad and output a value. Returns the corresponding SW

cgPerformRTCs :: Bool -> SBVCodeGen () Source #

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

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.

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 #

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.

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`.

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.

cgIgnoreSAssert :: Bool -> SBVCodeGen () Source #

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

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.

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

Creates an atomic input in the generated code.

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

Creates an array input in the generated code.

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

Creates an atomic output in the generated code.

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

Creates an array output in the generated code.

svCgReturn :: SVal -> SBVCodeGen () Source #

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

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

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

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.

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.

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.

data CgPgmBundle Source #

Representation of a collection of generated programs.

Constructors

CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |

Instances

Show CgPgmBundle Source # | A simple way to print bundles, mostly for debugging purposes.
Methods showsPrec :: Int -> CgPgmBundle -> ShowS # show :: CgPgmBundle -> String # showList :: [CgPgmBundle] -> ShowS #

data CgPgmKind Source #

Different kinds of "files" we can produce. Currently this is quite C specific.

Constructors

CgMakefile [String] |
CgHeader [Doc] |
CgSource |
CgDriver |

isCgDriver :: CgPgmKind -> Bool Source #

Is this a driver program?

isCgMakefile :: CgPgmKind -> Bool Source #

Is this a make file?

codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle Source #

Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection of makefiles, source code, headers, etc.

renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO () Source #

Render a code-gen bundle to a directory or to stdout

render' :: Doc -> String Source #

An alternative to Pretty's `render`, which might have "leading" white-space in empty lines. This version eliminates such whitespace.

# Various math utilities around floats

fpRound0 :: (RealFloat a, Integral b) => a -> b Source #

A variant of round; except defaulting to 0 when fed NaN or Infinity

fpRatio0 :: RealFloat a => a -> Rational Source #

A variant of toRational; except defaulting to 0 when fed NaN or Infinity

fpMaxH :: RealFloat a => a -> a -> a Source #

The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with Haskell's; and also it does not agree with what the hardware does. Sigh.. See: https://ghc.haskell.org/trac/ghc/ticket/10378 https://github.com/Z3Prover/z3/issues/68 So, we codify here what the Z3 (SMTLib) is implementing for fpMax. The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic

fpMinH :: RealFloat a => a -> a -> a Source #

SMTLib compliant definition for `fpMin`. See the comments for `fpMax`.

fp2fp :: (RealFloat a, RealFloat b) => a -> b Source #

Convert double to float and back. Essentially `fromRational . toRational` except careful on NaN, Infinities, and -0.

fpRemH :: RealFloat a => a -> a -> a Source #

Compute the "floating-point" remainder function, the float/double value that remains from the division of `x` and `y`. There are strict rules around 0's, Infinities, and NaN's as coded below, See http://smt-lib.org/papers/BTRW14.pdf, towards the end of section 4.c.

fpRoundToIntegralH :: RealFloat a => a -> a Source #

Convert a float to the nearest integral representable in that type

fpIsEqualObjectH :: RealFloat a => a -> a -> Bool Source #

Check that two floats are the exact same values, i.e., +0/-0 does not compare equal, and NaN's compare equal to themselves.

fpIsNormalizedH :: RealFloat a => a -> Bool Source #

Check if a number is "normal." Note that +0/-0 is not considered a normal-number and also this is not simply the negation of isDenormalized!