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

Safe Haskell None Haskell2010

Documentation.SBV.Examples.Uninterpreted.Sort

Description

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

Demonstrates uninterpreted sorts, together with axioms.

Synopsis

# 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
 Source # Instance details Methods(==) :: Q -> Q -> Bool #(/=) :: Q -> Q -> Bool # Source # Instance details Methodsgfoldl :: (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 #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 :: (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 # Source # Instance details Methodscompare :: Q -> Q -> Ordering #(<) :: Q -> Q -> Bool #(<=) :: Q -> Q -> Bool #(>) :: Q -> Q -> Bool #(>=) :: Q -> Q -> Bool #max :: Q -> Q -> Q #min :: Q -> Q -> Q # Source # Instance details MethodsreadList :: ReadS [Q] # Source # Instance details MethodsshowsPrec :: Int -> Q -> ShowS #show :: Q -> String #showList :: [Q] -> ShowS # Source # Instance details Methods Source # Instance details MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Q) Source #fromCV :: CV -> Q Source #isConcretely :: SBV Q -> (Q -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Q) Source #forall_ :: MonadSymbolic m => m (SBV Q) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Q] Source #exists :: MonadSymbolic m => String -> m (SBV Q) Source #exists_ :: MonadSymbolic m => m (SBV Q) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Q] Source #free :: MonadSymbolic m => String -> m (SBV Q) Source #free_ :: MonadSymbolic m => m (SBV Q) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Q] Source #symbolic :: MonadSymbolic m => String -> m (SBV Q) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Q] Source #

f :: SBV Q -> SBV Q Source #

Declare an uninterpreted function that works over Q's

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


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