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

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

Documentation.SBV.Examples.Misc.Newtypes

Description

Demonstrates how to create symbolic newtypes with the same behaviour as their wrapped type.

Synopsis

- newtype Metres = Metres Integer
- type SMetres = SBV Metres
- newtype HumanHeightInCm = HumanHeightInCm Word16
- type SHumanHeightInCm = SBV HumanHeightInCm
- tallestHumanEver :: SHumanHeightInCm
- ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool
- problem :: Predicate

# Documentation

newtype Metres Source #

A `Metres` is a newtype wrapper around `Integer`.

Constructors

Metres Integer |

#### Instances

Instances details

Enum Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods succ :: Metres -> Metres pred :: Metres -> Metres toEnum :: Int -> Metres fromEnum :: Metres -> Int enumFrom :: Metres -> [Metres] enumFromThen :: Metres -> Metres -> [Metres] enumFromTo :: Metres -> Metres -> [Metres] enumFromThenTo :: Metres -> Metres -> Metres -> [Metres]
Eq Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (==) :: Metres -> Metres -> Bool (/=) :: Metres -> Metres -> Bool
Integral Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods quot :: Metres -> Metres -> Metres rem :: Metres -> Metres -> Metres div :: Metres -> Metres -> Metres mod :: Metres -> Metres -> Metres quotRem :: Metres -> Metres -> (Metres, Metres) divMod :: Metres -> Metres -> (Metres, Metres) toInteger :: Metres -> Integer
Num Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (+) :: Metres -> Metres -> Metres (-) :: Metres -> Metres -> Metres (*) :: Metres -> Metres -> Metres negate :: Metres -> Metres abs :: Metres -> Metres signum :: Metres -> Metres fromInteger :: Integer -> Metres
Ord Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods compare :: Metres -> Metres -> Ordering (<) :: Metres -> Metres -> Bool (<=) :: Metres -> Metres -> Bool (>) :: Metres -> Metres -> Bool (>=) :: Metres -> Metres -> Bool max :: Metres -> Metres -> Metres min :: Metres -> Metres -> Metres
Real Metres Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods toRational :: Metres -> Rational
HasKind Metres Source # | To use `Metres` symbolically, we associate it with the underlying symbolic type's kind.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: Metres -> Kind Source #

hasSign :: Metres -> Bool Source #

intSizeOf :: Metres -> Int Source #

isBoolean :: Metres -> Bool Source #

isBounded :: Metres -> Bool Source #

isReal :: Metres -> Bool Source #

isFloat :: Metres -> Bool Source #

isDouble :: Metres -> Bool Source #

isUnbounded :: Metres -> Bool Source #

isUninterpreted :: Metres -> Bool Source #

isChar :: Metres -> Bool Source #

isString :: Metres -> Bool Source #

isList :: Metres -> Bool Source #

isSet :: Metres -> Bool Source #

isTuple :: Metres -> Bool Source #

isMaybe :: Metres -> Bool Source #

isEither :: Metres -> Bool Source #

showType :: Metres -> String Source #

SymVal Metres Source # | The `SymVal` instance simply uses stock definitions. This is always possible for newtypes that simply wrap over an existing symbolic type.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

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

literal :: Metres -> SBV Metres Source #

fromCV :: CV -> Metres Source #

isConcretely :: SBV Metres -> (Metres -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV Metres) Source #

forall_ :: MonadSymbolic m => m (SBV Metres) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV Metres] Source #

exists :: MonadSymbolic m => String -> m (SBV Metres) Source #

exists_ :: MonadSymbolic m => m (SBV Metres) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV Metres] Source #

free :: MonadSymbolic m => String -> m (SBV Metres) Source #

free_ :: MonadSymbolic m => m (SBV Metres) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Metres] Source #

symbolic :: MonadSymbolic m => String -> m (SBV Metres) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV Metres] Source #

unliteral :: SBV Metres -> Maybe Metres Source #

isConcrete :: SBV Metres -> Bool Source #

isSymbolic :: SBV Metres -> Bool Source #

type SMetres = SBV Metres Source #

Symbolic version of `Metres`.

newtype HumanHeightInCm Source #

Similarly, we can create another newtype, this time wrapping over `Word16`. As an example, consider measuring the human height in centimetres? The tallest person in history, Robert Wadlow, was 272 cm. We don't need negative values, so `Word16` is the smallest type that suits our needs.

Constructors

HumanHeightInCm Word16 |

#### Instances

Instances details

Enum HumanHeightInCm Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

succ :: HumanHeightInCm -> HumanHeightInCm

pred :: HumanHeightInCm -> HumanHeightInCm

toEnum :: Int -> HumanHeightInCm

fromEnum :: HumanHeightInCm -> Int

enumFrom :: HumanHeightInCm -> [HumanHeightInCm]

enumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]

enumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]

enumFromThenTo :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]

Eq HumanHeightInCm Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (==) :: HumanHeightInCm -> HumanHeightInCm -> Bool (/=) :: HumanHeightInCm -> HumanHeightInCm -> Bool
Integral HumanHeightInCm Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

quot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

rem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

div :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

mod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

quotRem :: HumanHeightInCm -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)

divMod :: HumanHeightInCm -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)

toInteger :: HumanHeightInCm -> Integer

Num HumanHeightInCm Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

(+) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

(-) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

(*) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

negate :: HumanHeightInCm -> HumanHeightInCm

abs :: HumanHeightInCm -> HumanHeightInCm

signum :: HumanHeightInCm -> HumanHeightInCm

fromInteger :: Integer -> HumanHeightInCm

Ord HumanHeightInCm Source # |

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

compare :: HumanHeightInCm -> HumanHeightInCm -> Ordering

(<) :: HumanHeightInCm -> HumanHeightInCm -> Bool

(<=) :: HumanHeightInCm -> HumanHeightInCm -> Bool

(>) :: HumanHeightInCm -> HumanHeightInCm -> Bool

(>=) :: HumanHeightInCm -> HumanHeightInCm -> Bool

max :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

min :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm

Real HumanHeightInCm Source # |
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods toRational :: HumanHeightInCm -> Rational
HasKind HumanHeightInCm Source # | Symbolic instance simply follows the underlying type, just like `Metres`.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: HumanHeightInCm -> Kind Source #

hasSign :: HumanHeightInCm -> Bool Source #

intSizeOf :: HumanHeightInCm -> Int Source #

isBoolean :: HumanHeightInCm -> Bool Source #

isBounded :: HumanHeightInCm -> Bool Source #

isReal :: HumanHeightInCm -> Bool Source #

isFloat :: HumanHeightInCm -> Bool Source #

isDouble :: HumanHeightInCm -> Bool Source #

isUnbounded :: HumanHeightInCm -> Bool Source #

isUninterpreted :: HumanHeightInCm -> Bool Source #

isChar :: HumanHeightInCm -> Bool Source #

isString :: HumanHeightInCm -> Bool Source #

isList :: HumanHeightInCm -> Bool Source #

isSet :: HumanHeightInCm -> Bool Source #

isTuple :: HumanHeightInCm -> Bool Source #

isMaybe :: HumanHeightInCm -> Bool Source #

isEither :: HumanHeightInCm -> Bool Source #

showType :: HumanHeightInCm -> String Source #

SymVal HumanHeightInCm Source # | Similarly here, for the `SymVal` instance.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

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

literal :: HumanHeightInCm -> SBV HumanHeightInCm Source #

fromCV :: CV -> HumanHeightInCm Source #

isConcretely :: SBV HumanHeightInCm -> (HumanHeightInCm -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source #

forall_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source #

exists :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source #

exists_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source #

free :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source #

free_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source #

symbolic :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV HumanHeightInCm] Source #

unliteral :: SBV HumanHeightInCm -> Maybe HumanHeightInCm Source #

isConcrete :: SBV HumanHeightInCm -> Bool Source #

isSymbolic :: SBV HumanHeightInCm -> Bool Source #

type SHumanHeightInCm = SBV HumanHeightInCm Source #

Symbolic version of `HumanHeightInCm`.

tallestHumanEver :: SHumanHeightInCm Source #

The tallest human ever was 272 cm. We can simply use `literal` to lift it to the symbolic space.

ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool Source #

Given a distance between a floor and a ceiling, we can see whether the human can stand in that room. Comparison is expressed using `sFromIntegral`.

problem :: Predicate Source #

Now, suppose we want to see whether we could design a room with a ceiling high enough that any human could stand in it. We have:

    >>> sat problem
    Satisfiable. Model:
      floorToCeiling =   3 :: Integer
      humanheight    = 255 :: Word16