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
sC :: SBV E
sB :: SBV E
sA :: 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

Instances details

Eq E Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods (==) :: E -> E -> Bool # (/=) :: E -> E -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c E # toConstr :: E -> Constr # dataTypeOf :: E -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c E) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c E) # gmapT :: (forall b. Data b => b -> b) -> E -> E # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> E -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> E -> r # gmapQ :: (forall d. Data d => d -> u) -> E -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> E -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> E -> m E # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> E -> m E # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> E -> m E #
Ord E Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods compare :: E -> E -> Ordering # (<) :: E -> E -> Bool # (<=) :: E -> E -> Bool # (>) :: E -> E -> Bool # (>=) :: E -> E -> Bool # max :: E -> E -> E # min :: E -> E -> E #
Read E Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods readsPrec :: Int -> ReadS E # readList :: ReadS [E] # readPrec :: ReadPrec E # readListPrec :: ReadPrec [E] #
Show E Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods showsPrec :: Int -> E -> ShowS # show :: E -> String # showList :: [E] -> ShowS #
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 # isFP :: E -> Bool Source # isUnbounded :: E -> Bool Source # isUserSort :: E -> Bool Source # isChar :: E -> Bool Source # isString :: E -> Bool Source # isList :: E -> Bool Source # isSet :: E -> Bool Source # isTuple :: E -> Bool Source # isMaybe :: E -> Bool Source # isEither :: E -> Bool Source # showType :: E -> String Source #
SymVal E Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Enumerate Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV E) Source # literal :: E -> SBV E Source # fromCV :: CV -> E Source # isConcretely :: SBV E -> (E -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV E) Source # forall_ :: MonadSymbolic m => m (SBV E) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV E] Source # exists :: MonadSymbolic m => String -> m (SBV E) Source # exists_ :: MonadSymbolic m => m (SBV E) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV 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 # isConcrete :: SBV E -> Bool Source # isSymbolic :: SBV E -> Bool 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 #

type SE = SBV E Source #

Make E a symbolic value.

sC :: SBV E Source #

sB :: SBV E Source #

sA :: SBV E Source #

elts :: IO AllSatResult Source #

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

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

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