Documentation.SBV.Examples.Misc.Enumerate

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.

Documentation

data E

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

Data E

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

Read E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

readsPrec :: Int -> ReadS E

readList :: ReadS [E]

readPrec :: ReadPrec E

readListPrec :: ReadPrec [E]

Show E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

showsPrec :: Int -> E -> ShowS

show :: E -> String

showList :: [E] -> ShowS

Eq E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

(==) :: E -> E -> Bool

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

Ord E

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

SymVal E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV E)

literal :: E -> SBV E

fromCV :: CV -> E

isConcretely :: SBV E -> (E -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV E)

sbvForall_ :: MonadSymbolic m => m (SBV E)

mkForallVars :: MonadSymbolic m => Int -> m [SBV E]

sbvExists :: MonadSymbolic m => String -> m (SBV E)

sbvExists_ :: MonadSymbolic m => m (SBV E)

mkExistVars :: MonadSymbolic m => Int -> m [SBV E]

free :: MonadSymbolic m => String -> m (SBV E)

free_ :: MonadSymbolic m => m (SBV E)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV E]

symbolic :: MonadSymbolic m => String -> m (SBV E)

symbolics :: MonadSymbolic m => [String] -> m [SBV E]

unliteral :: SBV E -> Maybe E

isConcrete :: SBV E -> Bool

isSymbolic :: SBV E -> Bool

HasKind E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

kindOf :: E -> Kind

hasSign :: E -> Bool

intSizeOf :: E -> Int

isBoolean :: E -> Bool

isBounded :: E -> Bool

isReal :: E -> Bool

isFloat :: E -> Bool

isDouble :: E -> Bool

isRational :: E -> Bool

isFP :: E -> Bool

isUnbounded :: E -> Bool

isUserSort :: E -> Bool

isChar :: E -> Bool

isString :: E -> Bool

isList :: E -> Bool

isSet :: E -> Bool

isTuple :: E -> Bool

isMaybe :: E -> Bool

isEither :: E -> Bool

showType :: E -> String

SatModel E

Defined in Documentation.SBV.Examples.Misc.Enumerate

Methods

parseCVs :: [CV] -> Maybe (E, [CV])

cvtModel :: (E -> Maybe b) -> Maybe (E, [CV]) -> Maybe (b, [CV])

type SE = SBV E

Symbolic version of the type E.

sC :: SBV E

Symbolic version of the constructor C.

sB :: SBV E

Symbolic version of the constructor B.

sA :: SBV E

Symbolic version of the constructor A.

elts :: IO AllSatResult

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

>>> elts
Solution #1:
  s0 = C :: E
Solution #2:
  s0 = B :: E
Solution #3:
  s0 = A :: E
Found 3 different solutions.

four :: IO SatResult

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

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

Similarly, we get the minimum element. We have:

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