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

Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

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
 Source # Instance details Methods(==) :: L -> L -> Bool #(/=) :: L -> L -> Bool # Source # Instance details Methodsgfoldl :: (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 #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 # Source # Instance details Methodscompare :: L -> L -> Ordering #(<) :: L -> L -> Bool #(<=) :: L -> L -> Bool #(>) :: L -> L -> Bool #(>=) :: L -> L -> Bool #max :: L -> L -> L #min :: L -> L -> L # Source # Instance details MethodsreadList :: ReadS [L] # Source # Instance details MethodsshowsPrec :: Int -> L -> ShowS #show :: L -> String #showList :: [L] -> ShowS # Source # Similarly, HasKinds default implementation is sufficient. Instance details Methods Source # Declare instances to make L a usable uninterpreted sort. First we need the SymVal instance, with the default definition sufficing. Instance details MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV L) Source #fromCV :: CV -> L Source #isConcretely :: SBV L -> (L -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV L) Source #forall_ :: MonadSymbolic m => m (SBV L) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV L] Source #exists :: MonadSymbolic m => String -> m (SBV L) Source #exists_ :: MonadSymbolic m => m (SBV L) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV L] Source #free :: MonadSymbolic m => String -> m (SBV L) Source #free_ :: MonadSymbolic m => m (SBV L) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV L] Source #symbolic :: MonadSymbolic m => String -> m (SBV L) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV L] Source #

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

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.