sbv-7.13: 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.Sort

Description

Demonstrates uninterpreted sorts, together with axioms.

Synopsis

- newtype Q = Q ()
- f :: SBV Q -> SBV Q
- t1 :: IO SatResult
- t2 :: IO SatResult

# Documentation

newtype Q Source #

A new data-type that we expect to use in an uninterpreted fashion in the backend SMT solver. Note the custom `deriving` clause, which takes care of most of the boilerplate. The () field is needed so SBV will not translate it to an enumerated data-type

Constructors

Q () |

Instances

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

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Q -> c Q Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q Source #

toConstr :: Q -> Constr Source #

dataTypeOf :: Q -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q) Source #

gmapT :: (forall b. Data b => b -> b) -> Q -> Q Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Q -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Q -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q -> m Q Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q -> m Q Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q -> m Q Source #

Ord Q Source # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods compare :: Q -> Q -> Ordering Source # (<) :: Q -> Q -> Bool Source # (<=) :: Q -> Q -> Bool Source # (>) :: Q -> Q -> Bool Source # (>=) :: Q -> Q -> Bool Source # max :: Q -> Q -> Q Source # min :: Q -> Q -> Q Source #
Read Q Source # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods readsPrec :: Int -> ReadS Q Source # readList :: ReadS [Q] Source # readPrec :: ReadPrec Q Source # readListPrec :: ReadPrec [Q] Source #
Show Q Source # |
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods showsPrec :: Int -> Q -> ShowS Source # show :: Q -> String Source # showList :: [Q] -> ShowS Source #
HasKind Q Source # |

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

kindOf :: Q -> Kind Source #

hasSign :: Q -> Bool Source #

intSizeOf :: Q -> Int Source #

isBoolean :: Q -> Bool Source #

isBounded :: Q -> Bool Source #

isReal :: Q -> Bool Source #

isFloat :: Q -> Bool Source #

isDouble :: Q -> Bool Source #

isInteger :: Q -> Bool Source #

isUninterpreted :: Q -> Bool Source #

isChar :: Q -> Bool Source #

isString :: Q -> Bool Source #

isList :: Q -> Bool Source #

showType :: Q -> String Source #

SymWord Q Source # |

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

forall :: String -> Symbolic (SBV Q) Source #

forall_ :: Symbolic (SBV Q) Source #

mkForallVars :: Int -> Symbolic [SBV Q] Source #

exists :: String -> Symbolic (SBV Q) Source #

exists_ :: Symbolic (SBV Q) Source #

mkExistVars :: Int -> Symbolic [SBV Q] Source #

free :: String -> Symbolic (SBV Q) Source #

free_ :: Symbolic (SBV Q) Source #

mkFreeVars :: Int -> Symbolic [SBV Q] Source #

symbolic :: String -> Symbolic (SBV Q) Source #

symbolics :: [String] -> Symbolic [SBV Q] Source #

literal :: Q -> SBV Q Source #

unliteral :: SBV Q -> Maybe Q Source #

fromCW :: CW -> Q Source #

isConcrete :: SBV Q -> Bool Source #

isSymbolic :: SBV Q -> Bool Source #

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

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Q) Source #

f :: SBV Q -> SBV Q Source #

Declare an uninterpreted function that works over Q's

t1 :: IO SatResult Source #

A satisfiable example, stating that there is an element of the domain `Q` such that `f` returns a different element. Note that this is valid only when the domain `Q` has at least two elements. We have:

    >>> t1
    Satisfiable. Model:
      x = Q!val!0 :: Q

t2 :: IO SatResult Source #

This is a variant on the first example, except we also add an axiom for the sort, stating that the domain `Q` has only one element. In this case the problem naturally becomes unsat. We have:

    >>> t2
    Unsatisfiable