Documentation.SBV.Examples.Uninterpreted.Sort

Demonstrates uninterpreted sorts, together with axioms.

Documentation

newtype Q

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

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

Methods

(==) :: Q -> Q -> Bool

(/=) :: Q -> Q -> Bool

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 :: (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

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

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

isUnbounded :: Q -> Bool

isUninterpreted :: 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 => Maybe Quantifier -> 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

f :: SBV Q -> SBV Q

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