Data.SBV.Examples.Misc.Enumerate

Demonstrates how enumerations can be translated to their SMT-Lib counterparts, without losing any information content. Also see Data.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. Note the automatically derived classes we need: Eq, Ord, Data, Read, Show, SymWord, HasKind, and SatModel. (The last one is only needed if getModel and friends are used.)

Also note that we need to import Data.Generics and have the LANGUAGE option DeriveDataTypeable and DeriveAnyClass set.

Constructors

A

B

C

Instances

Eq E

Methods

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

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

Data E

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 :: (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

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

Methods

readsPrec :: Int -> ReadS E

readList :: ReadS [E]

readPrec :: ReadPrec E

readListPrec :: ReadPrec [E]

Show E

Methods

showsPrec :: Int -> E -> ShowS

show :: E -> String

showList :: [E] -> ShowS

HasKind E

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

isInteger :: E -> Bool

isUninterpreted :: E -> Bool

showType :: E -> String

SymWord E

Methods

forall :: String -> Symbolic (SBV E)

forall_ :: Symbolic (SBV E)

mkForallVars :: Int -> Symbolic [SBV E]

exists :: String -> Symbolic (SBV E)

exists_ :: Symbolic (SBV E)

mkExistVars :: Int -> Symbolic [SBV E]

free :: String -> Symbolic (SBV E)

free_ :: Symbolic (SBV E)

mkFreeVars :: Int -> Symbolic [SBV E]

symbolic :: String -> Symbolic (SBV E)

symbolics :: [String] -> Symbolic [SBV E]

literal :: E -> SBV E

unliteral :: SBV E -> Maybe E

fromCW :: CW -> E

isConcrete :: SBV E -> Bool

isSymbolic :: SBV E -> Bool

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

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV E)

type SE = SBV E

Give a name to the symbolic variants of E, for convenience

elts :: IO AllSatResult

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

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

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