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 # (/=) :: Q -> Q -> Bool #
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 :: (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 #
Ord Q Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods compare :: Q -> Q -> Ordering # (<) :: Q -> Q -> Bool # (<=) :: Q -> Q -> Bool # (>) :: Q -> Q -> Bool # (>=) :: Q -> Q -> Bool # max :: Q -> Q -> Q # min :: Q -> Q -> 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 # isUninterpreted :: 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 => Maybe Quantifier -> 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 #

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

  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