Documentation.SBV.Examples.Uninterpreted.Sort

Demonstrates uninterpreted sorts, together with axioms.

Documentation

data Q

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

Instances

Data Q

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

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

readsPrec :: Int -> ReadS Q

readList :: ReadS [Q]

readPrec :: ReadPrec Q

readListPrec :: ReadPrec [Q]

Show Q

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

showsPrec :: Int -> Q -> ShowS

show :: Q -> String

showList :: [Q] -> ShowS

HasKind Q

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

kindOf :: Q -> Kind

hasSign :: Q -> Bool

intSizeOf :: Q -> Int

isBoolean :: Q -> Bool

isBounded :: Q -> Bool

isReal :: Q -> Bool

isFloat :: Q -> Bool

isDouble :: Q -> Bool

isRational :: Q -> Bool

isFP :: Q -> Bool

isUnbounded :: Q -> Bool

isUserSort :: Q -> Bool

isChar :: Q -> Bool

isString :: Q -> Bool

isList :: Q -> Bool

isSet :: Q -> Bool

isTuple :: Q -> Bool

isMaybe :: Q -> Bool

isEither :: Q -> Bool

showType :: Q -> String

SymVal Q

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Q)

literal :: Q -> SBV Q

fromCV :: CV -> Q

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

forall :: MonadSymbolic m => String -> m (SBV Q)

forall_ :: MonadSymbolic m => m (SBV Q)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Q]

exists :: MonadSymbolic m => String -> m (SBV Q)

exists_ :: MonadSymbolic m => m (SBV Q)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Q]

free :: MonadSymbolic m => String -> m (SBV Q)

free_ :: MonadSymbolic m => m (SBV Q)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Q]

symbolic :: MonadSymbolic m => String -> m (SBV Q)

symbolics :: MonadSymbolic m => [String] -> m [SBV Q]

unliteral :: SBV Q -> Maybe Q

isConcrete :: SBV Q -> Bool

isSymbolic :: SBV Q -> Bool

SatModel Q

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

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

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

type SQ = SBV Q

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

Declare an uninterpreted function that works over Q's

t1 :: IO SatResult

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

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