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

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

- data L
  - = Nil
  - | Cons Int L
- classify :: SBV L -> SInteger
- genLs :: Predicate

# 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

Instances details

Eq L Source # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods (==) :: L -> L -> Bool (/=) :: L -> L -> Bool
Data L Source # |

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

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 :: forall r r'. (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 # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat 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 # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods readsPrec :: Int -> ReadS L readList :: ReadS [L] readPrec :: ReadPrec L readListPrec :: ReadPrec [L]
Show L Source # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods showsPrec :: Int -> L -> ShowS show :: L -> String showList :: [L] -> ShowS
HasKind L Source # | Similarly, `HasKind`s default implementation is sufficient.

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

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 #

isUnbounded :: L -> Bool Source #

isUninterpreted :: L -> Bool Source #

isChar :: L -> Bool Source #

isString :: L -> Bool Source #

isList :: L -> Bool Source #

isSet :: L -> Bool Source #

isTuple :: L -> Bool Source #

isMaybe :: L -> Bool Source #

isEither :: L -> Bool Source #

showType :: L -> String Source #

SymVal L Source # | Declare instances to make `L` a usable uninterpreted sort. First we need the `SymVal` instance, with the default definition sufficing.

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV L) Source #

literal :: L -> 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 #

unliteral :: SBV L -> Maybe L Source #

isConcrete :: SBV L -> Bool Source #

isSymbolic :: SBV L -> Bool 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 :: Predicate 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:

    >>> allSat genLs
    Solution #1:
      l  = L!val!0 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L

      classify :: L -> Integer
      classify L!val!2 = 2
      classify L!val!1 = 1
      classify _       = 0
    Solution #2:
      l  = L!val!1 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L

      classify :: L -> Integer
      classify L!val!2 = 2
      classify L!val!1 = 1
      classify _       = 0
    Solution #3:
      l  = L!val!2 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L

      classify :: L -> Integer
      classify L!val!2 = 2
      classify L!val!1 = 1
      classify _       = 0
    Found 3 different solutions.