sbv-8.12: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Uninterpreted.Sort

Description

Demonstrates uninterpreted sorts, together with axioms.

Synopsis

Documentation

data Q Source #

A new data-type that we expect to use in an uninterpreted fashion in the backend SMT solver.

Instances

Instances details
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 #

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

toConstr :: Q -> Constr #

dataTypeOf :: Q -> DataType #

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

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

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

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

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

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

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

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

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

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

Read Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Show Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

showsPrec :: Int -> Q -> ShowS #

show :: Q -> String #

showList :: [Q] -> ShowS #

HasKind Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

SymVal Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

SatModel Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

parseCVs :: [CV] -> Maybe (Q, [CV]) Source #

cvtModel :: (Q -> Maybe b) -> Maybe (Q, [CV]) -> Maybe (b, [CV]) Source #

type SQ = SBV Q Source #

Make Q an uinterpreted sort. This will automatically introduce the type SQ into our environment, which is the symbolic version of the carrier type Q.

f :: SQ -> SQ 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

  f :: Q -> Q
  f _ = Q!val!1

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