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.Queries.Enums

Description

Demonstrates the use of enumeration values during queries.

Synopsis

- data Day
  - = Monday
  - | Tuesday
  - | Wednesday
  - | Thursday
  - | Friday
  - | Saturday
  - | Sunday
- type SDay = SBV Day
- findDays :: IO [Day]

# Documentation

data Day Source #

Days of the week. We make it symbolic using the `mkSymbolicEnumeration` splice.

Constructors

Monday |
Tuesday |
Wednesday |
Thursday |
Friday |
Saturday |
Sunday |

Instances

Eq Day Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods (==) :: Day -> Day -> Bool Source # (/=) :: Day -> Day -> Bool Source #
Data Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

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

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

toConstr :: Day -> Constr Source #

dataTypeOf :: Day -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord Day Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods compare :: Day -> Day -> Ordering Source # (<) :: Day -> Day -> Bool Source # (<=) :: Day -> Day -> Bool Source # (>) :: Day -> Day -> Bool Source # (>=) :: Day -> Day -> Bool Source # max :: Day -> Day -> Day Source # min :: Day -> Day -> Day Source #
Read Day Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods readsPrec :: Int -> ReadS Day Source # readList :: ReadS [Day] Source # readPrec :: ReadPrec Day Source # readListPrec :: ReadPrec [Day] Source #
Show Day Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods showsPrec :: Int -> Day -> ShowS Source # show :: Day -> String Source # showList :: [Day] -> ShowS Source #
HasKind Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

kindOf :: Day -> Kind Source #

hasSign :: Day -> Bool Source #

intSizeOf :: Day -> Int Source #

isBoolean :: Day -> Bool Source #

isBounded :: Day -> Bool Source #

isReal :: Day -> Bool Source #

isFloat :: Day -> Bool Source #

isDouble :: Day -> Bool Source #

isInteger :: Day -> Bool Source #

isUninterpreted :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

showType :: Day -> String Source #

SymWord Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

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

forall_ :: Symbolic (SBV Day) Source #

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

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

exists_ :: Symbolic (SBV Day) Source #

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

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

free_ :: Symbolic (SBV Day) Source #

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

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

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

literal :: Day -> SBV Day Source #

unliteral :: SBV Day -> Maybe Day Source #

fromCW :: CW -> Day Source #

isConcrete :: SBV Day -> Bool Source #

isSymbolic :: SBV Day -> Bool Source #

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

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

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

type SDay = SBV Day Source #

The type synonym `SDay` is the symbolic variant of `Day`. (Similar to 'SInteger'/'Integer' and others.)

findDays :: IO [Day] Source #

A trivial query to find three consecutive days that's all before `Thursday`. The point here is that we can perform queries on such enumerated values and use `getValue` on them and return their values from queries just like any other value. We have:

    >>> findDays
    [Monday,Tuesday,Wednesday]