sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Examples.Misc.Enumerate

Description

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.

Synopsis

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. 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

 Source # Methods(==) :: E -> E -> Bool #(/=) :: E -> E -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methodscompare :: E -> E -> Ordering #(<) :: E -> E -> Bool #(<=) :: E -> E -> Bool #(>) :: E -> E -> Bool #(>=) :: E -> E -> Bool #max :: E -> E -> E #min :: E -> E -> E # Source # MethodsreadList :: ReadS [E] # Source # MethodsshowsPrec :: Int -> E -> ShowS #show :: E -> String #showList :: [E] -> ShowS # Source # Methods Source # Methodssymbolics :: [String] -> Symbolic [SBV E] Source #fromCW :: CW -> E Source #isConcretely :: SBV E -> (E -> Bool) -> Bool Source #

type SE = SBV E Source #

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

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.

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

Similarly, we get the minumum element. We have:

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