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.
Documentation
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.
Instances
Eq E Source # | |
Data E Source # | |
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 # 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 Source # | |
Read E Source # | |
Show E Source # | |
HasKind E Source # | |
Defined in Documentation.SBV.Examples.Misc.Enumerate | |
SymVal E Source # | |
Defined in Documentation.SBV.Examples.Misc.Enumerate Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV E) Source # literal :: E -> SBV 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 # | |
SatModel E Source # | Make |
SMTValue E Source # | |
Defined in Documentation.SBV.Examples.Misc.Enumerate Methods sexprToVal :: SExpr -> Maybe 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.
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
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