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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Queries.Enums

Description

Demonstrates the use of enumeration values during queries.

Synopsis

Documentation

data Day #

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

Instances

Eq Day # 

Methods

(==) :: Day -> Day -> Bool #

(/=) :: Day -> Day -> Bool #

Data Day # 

Methods

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

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

toConstr :: Day -> Constr #

dataTypeOf :: Day -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Day # 

Methods

compare :: Day -> Day -> Ordering #

(<) :: Day -> Day -> Bool #

(<=) :: Day -> Day -> Bool #

(>) :: Day -> Day -> Bool #

(>=) :: Day -> Day -> Bool #

max :: Day -> Day -> Day #

min :: Day -> Day -> Day #

Read Day # 
Show Day # 

Methods

showsPrec :: Int -> Day -> ShowS #

show :: Day -> String #

showList :: [Day] -> ShowS #

HasKind Day # 
SymWord Day # 
SatModel Day # 

Methods

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

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

SMTValue Day # 

Methods

sexprToVal :: SExpr -> Maybe Day #

type SDay = SBV Day #

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

findDays :: IO [Day] #

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]