sbv-8.6: 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.Queries.Enums

Description

Demonstrates the use of enumeration values during queries.

Synopsis

Documentation

data Day Source #

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

Instances

Instances details
Eq Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

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

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

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

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 :: forall r r'. (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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

readsPrec :: Int -> ReadS Day

readList :: ReadS [Day]

readPrec :: ReadPrec Day

readListPrec :: ReadPrec [Day]

Show Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

showsPrec :: Int -> Day -> ShowS

show :: Day -> String

showList :: [Day] -> ShowS

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 #

isUnbounded :: Day -> Bool Source #

isUninterpreted :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

isSet :: Day -> Bool Source #

isTuple :: Day -> Bool Source #

isMaybe :: Day -> Bool Source #

isEither :: Day -> Bool Source #

showType :: Day -> String Source #

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Day) Source #

literal :: Day -> SBV Day Source #

fromCV :: CV -> Day Source #

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

forall :: MonadSymbolic m => String -> m (SBV Day) Source #

forall_ :: MonadSymbolic m => m (SBV Day) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV Day] Source #

exists :: MonadSymbolic m => String -> m (SBV Day) Source #

exists_ :: MonadSymbolic m => m (SBV Day) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV Day] Source #

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

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

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

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

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

unliteral :: SBV Day -> Maybe Day Source #

isConcrete :: SBV Day -> Bool Source #

isSymbolic :: SBV Day -> Bool Source #

SatModel Day Source #

Make Day a symbolic value.

Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

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

cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) 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]