sbv-13.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Misc.Enumerate

Description

Demonstrates how enumerations can be translated to their SMT-Lib counterparts, without losing any information content. Also see Documentation.SBV.Examples.Puzzles.U2Bridge for a more detailed example involving enumerations.

Synopsis

Documentation

data E Source #

A simple enumerated type, that we'd like to translate to SMT-Lib intact; i.e., this type will not be uninterpreted but rather preserved and will be just like any other symbolic type SBV provides.

Constructors

A 
B 
C 

Instances

Instances details
Arbitrary E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

arbitrary :: Gen E #

shrink :: E -> [E] #

SymVal E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV E) Source #

mkSymValInit :: State -> SBV E -> IO () Source #

literal :: E -> SBV E Source #

fromCV :: CV -> E Source #

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

minMaxBound :: Maybe (E, E) Source #

free :: MonadSymbolic m => String -> m (SBV E) Source #

free_ :: MonadSymbolic m => m (SBV E) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV E] Source #

symbolic :: MonadSymbolic m => String -> m (SBV E) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV E] Source #

unliteral :: SBV E -> Maybe E Source #

unlitCV :: SBV E -> Maybe (Kind, CVal) Source #

isConcrete :: SBV E -> Bool Source #

isSymbolic :: SBV E -> Bool Source #

HasKind E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

kindOf :: E -> Kind Source #

hasSign :: E -> Bool Source #

intSizeOf :: E -> Int Source #

isBoolean :: E -> Bool Source #

isBounded :: E -> Bool Source #

isReal :: E -> Bool Source #

isFloat :: E -> Bool Source #

isDouble :: E -> Bool Source #

isRational :: E -> Bool Source #

isFP :: E -> Bool Source #

isUnbounded :: E -> Bool Source #

isADT :: E -> Bool Source #

isChar :: E -> Bool Source #

isString :: E -> Bool Source #

isList :: E -> Bool Source #

isSet :: E -> Bool Source #

isTuple :: E -> Bool Source #

isArray :: E -> Bool Source #

isRoundingMode :: E -> Bool Source #

isUninterpreted :: E -> Bool Source #

showType :: E -> String Source #

EnumSymbolic E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

succ :: SBV E -> SBV E Source #

pred :: SBV E -> SBV E Source #

toEnum :: SInteger -> SBV E Source #

fromEnum :: SBV E -> SInteger Source #

enumFrom :: SBV E -> SList E Source #

enumFromThen :: SBV E -> SBV E -> SList E Source #

enumFromTo :: SBV E -> SBV E -> SList E Source #

enumFromThenTo :: SBV E -> SBV E -> SBV E -> SList E Source #

SatModel E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

parseCVs :: [CV] -> Maybe (E, [CV]) Source #

cvtModel :: (E -> Maybe b) -> Maybe (E, [CV]) -> Maybe (b, [CV]) Source #

OrdSymbolic (SBV E) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

(.<) :: SBV E -> SBV E -> SBool Source #

(.<=) :: SBV E -> SBV E -> SBool Source #

(.>) :: SBV E -> SBV E -> SBool Source #

(.>=) :: SBV E -> SBV E -> SBool Source #

smin :: SBV E -> SBV E -> SBV E Source #

smax :: SBV E -> SBV E -> SBV E Source #

inRange :: SBV E -> (SBV E, SBV E) -> SBool Source #

HasInductionSchema (Forall ta E -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta E -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

inductionSchema :: (Forall ta E -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2E :: String -> [CV] -> E Source #

Conversion from SMT values to E values.

_undefiner_E :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SE = SBV E Source #

Symbolic version of the type E.

sA :: SBV E Source #

Symbolic version of the constructor A.

sB :: SBV E Source #

Symbolic version of the constructor B.

sC :: SBV E Source #

Symbolic version of the constructor C.

isA :: SBV E -> SBool Source #

Field recognizer predicate.

isB :: SBV E -> SBool Source #

Field recognizer predicate.

isC :: SBV E -> SBool Source #

Field recognizer predicate.

sCaseE :: Mergeable result => SBV E -> result -> result -> result -> result Source #

Case analyzer for the type E.

elts :: IO AllSatResult Source #

Have the SMT solver enumerate the elements of the domain. We have:

>>> elts
Solution #1:
  s0 = C :: E
Solution #2:
  s0 = A :: E
Solution #3:
  s0 = B :: E
Found 3 different solutions.

four :: IO SatResult Source #

Shows that if we require 4 distinct elements of the type E, we shall fail; as the domain only has three elements. We have:

>>> four
Unsatisfiable

maxE :: IO SatResult Source #

Enumerations are automatically ordered, so we can ask for the maximum element. Note the use of quantification. We have:

>>> maxE
Satisfiable. Model:
  maxE = C :: E

minE :: IO SatResult Source #

Similarly, we get the minimum element. We have:

>>> minE
Satisfiable. Model:
  minE = A :: E