Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Description

Demonstrates uninterpreted sorts and how all-sat behaves for them. Thanks to Eric Seidel for the idea.

Synopsis

Documentation

data L Source #

A "list-like" data type, but one we plan to uninterpret at the SMT level. The actual shape is really immaterial for us, but could be used as a proxy to generate test cases or explore data-space in some other part of a program. Note that we neither rely on the shape of this data, nor need the actual constructors.

Constructors

Nil
Cons Int L

Instances

Eq L Source #
Methods (==) :: L -> L -> Bool # (/=) :: L -> L -> Bool #
Data L Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> L -> c L # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c L # toConstr :: L -> Constr # dataTypeOf :: L -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c L) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L) # gmapT :: (forall b. Data b => b -> b) -> L -> L # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r # gmapQ :: (forall d. Data d => d -> u) -> L -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> L -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> L -> m L # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> L -> m L # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> L -> m L #
Ord L Source #
Methods compare :: L -> L -> Ordering # (<) :: L -> L -> Bool # (<=) :: L -> L -> Bool # (>) :: L -> L -> Bool # (>=) :: L -> L -> Bool # max :: L -> L -> L # min :: L -> L -> L #
Read L Source #
Methods readsPrec :: Int -> ReadS L # readList :: ReadS [L] # readPrec :: ReadPrec L # readListPrec :: ReadPrec [L] #
Show L Source #
Methods showsPrec :: Int -> L -> ShowS # show :: L -> String # showList :: [L] -> ShowS #
HasKind L Source #	Similarly, `HasKind`s default implementation is sufficient.
Methods kindOf :: L -> Kind Source # hasSign :: L -> Bool Source # intSizeOf :: L -> Int Source # isBoolean :: L -> Bool Source # isBounded :: L -> Bool Source # isReal :: L -> Bool Source # isFloat :: L -> Bool Source # isDouble :: L -> Bool Source # isInteger :: L -> Bool Source # isUninterpreted :: L -> Bool Source # isChar :: L -> Bool Source # isString :: L -> Bool Source # showType :: L -> String Source #
SymWord L Source #	Declare instances to make `L` a usable uninterpreted sort. First we need the `SymWord` instance, with the default definition sufficing.
Methods forall :: String -> Symbolic (SBV L) Source # forall_ :: Symbolic (SBV L) Source # mkForallVars :: Int -> Symbolic [SBV L] Source # exists :: String -> Symbolic (SBV L) Source # exists_ :: Symbolic (SBV L) Source # mkExistVars :: Int -> Symbolic [SBV L] Source # free :: String -> Symbolic (SBV L) Source # free_ :: Symbolic (SBV L) Source # mkFreeVars :: Int -> Symbolic [SBV L] Source # symbolic :: String -> Symbolic (SBV L) Source # symbolics :: [String] -> Symbolic [SBV L] Source # literal :: L -> SBV L Source # unliteral :: SBV L -> Maybe L Source # fromCW :: CW -> L Source # isConcrete :: SBV L -> Bool Source # isSymbolic :: SBV L -> Bool Source # isConcretely :: SBV L -> (L -> Bool) -> Bool Source # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV L) Source #

classify :: SBV L -> SInteger Source #

An uninterpreted "classify" function. Really, we only care about the fact that such a function exists, not what it does.

genLs :: IO AllSatResult Source #

Formulate a query that essentially asserts a cardinality constraint on the uninterpreted sort L. The goal is to say there are precisely 3 such things, as it might be the case. We manage this by declaring four elements, and asserting that for a free variable of this sort, the shape of the data matches one of these three instances. That is, we assert that all the instances of the data L can be classified into 3 equivalence classes. Then, allSat returns all the possible instances, which of course are all uninterpreted.

As expected, we have:

>>> genLs
Solution #1:
  l  = L!val!0 :: L
  l0 = L!val!0 :: L
  l1 = L!val!1 :: L
  l2 = L!val!2 :: L
Solution #2:
  l  = L!val!1 :: L
  l0 = L!val!0 :: L
  l1 = L!val!1 :: L
  l2 = L!val!2 :: L
Solution #3:
  l  = L!val!2 :: L
  l0 = L!val!0 :: L
  l1 = L!val!1 :: L
  l2 = L!val!2 :: L
Found 3 different solutions.