sbv-7.13: 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

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

- data E
  - = A
  - | B
  - | C
- type SE = SBV E
- elts :: IO AllSatResult
- four :: IO SatResult
- maxE :: IO SatResult
- minE :: IO SatResult

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

Also note that we need to have the following `LANGUAGE` options defined: `TemplateHaskell`, `StandaloneDeriving`, `DeriveDataTypeable`, `DeriveAnyClass` for this to work.

Constructors

A |
B |
C |

Instances

Eq E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods (==) :: E -> E -> Bool Source # (/=) :: E -> E -> Bool Source #
Data E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

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

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

toConstr :: E -> Constr Source #

dataTypeOf :: E -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods compare :: E -> E -> Ordering Source # (<) :: E -> E -> Bool Source # (<=) :: E -> E -> Bool Source # (>) :: E -> E -> Bool Source # (>=) :: E -> E -> Bool Source # max :: E -> E -> E Source # min :: E -> E -> E Source #
Read E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods readsPrec :: Int -> ReadS E Source # readList :: ReadS [E] Source # readPrec :: ReadPrec E Source # readListPrec :: ReadPrec [E] Source #
Show E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods showsPrec :: Int -> E -> ShowS Source # show :: E -> String Source # showList :: [E] -> ShowS 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 #

isInteger :: E -> Bool Source #

isUninterpreted :: E -> Bool Source #

isChar :: E -> Bool Source #

isString :: E -> Bool Source #

isList :: E -> Bool Source #

showType :: E -> String Source #

SymWord E Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

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 #

SatModel E Source # | Make `E` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods parseCWs :: [CW] -> Maybe (E, [CW]) Source # cvtModel :: (E -> Maybe b) -> Maybe (E, [CW]) -> Maybe (b, [CW]) Source #
SMTValue E Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods sexprToVal :: SExpr -> Maybe E Source #

type SE = SBV E Source #

Give a name to the symbolic variants of `E`, for convenience

elts :: IO AllSatResult Source #

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

    >>> elts
    Solution #1:
      s0 = B :: E
    Solution #2:
      s0 = A :: E
    Solution #3:
      s0 = C :: 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 minumum element. We have:

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