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

data Q
type SQ = SBV Q
f :: SQ -> SQ
t1 :: IO SatResult
t2 :: IO SatResult

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 Methods readsPrec :: Int -> ReadS Q # readList :: ReadS [Q] # readPrec :: ReadPrec Q # readListPrec :: ReadPrec [Q] #
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 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 # isUnbounded :: Q -> Bool Source # isUserSort :: Q -> Bool Source # isChar :: Q -> Bool Source # isString :: Q -> Bool Source # isList :: Q -> Bool Source # isSet :: Q -> Bool Source # isTuple :: Q -> Bool Source # isMaybe :: Q -> Bool Source # isEither :: Q -> Bool Source # showType :: Q -> String Source #
SymVal Q Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Q) Source # literal :: Q -> 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 # unliteral :: SBV Q -> Maybe Q Source # isConcrete :: SBV Q -> Bool Source # isSymbolic :: SBV Q -> Bool Source #
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