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
cv2Q :: String -> [CV] -> Q
_undefiner_Q :: a
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

Arbitrary Q Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods arbitrary :: Gen Q # shrink :: Q -> [Q] #
SymVal Q Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Sort Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Q) Source # mkSymValInit :: State -> SBV Q -> IO () Source # literal :: Q -> SBV Q Source # fromCV :: CV -> Q Source # isConcretely :: SBV Q -> (Q -> Bool) -> Bool Source # minMaxBound :: Maybe (Q, 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 # unlitCV :: SBV Q -> Maybe (Kind, CVal) Source # isConcrete :: SBV Q -> Bool Source # isSymbolic :: SBV Q -> Bool Source #
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 # isRational :: Q -> Bool Source # isFP :: Q -> Bool Source # isUnbounded :: Q -> Bool Source # isADT :: Q -> Bool Source # isChar :: Q -> Bool Source # isString :: Q -> Bool Source # isList :: Q -> Bool Source # isSet :: Q -> Bool Source # isTuple :: Q -> Bool Source # isArray :: Q -> Bool Source # isRoundingMode :: Q -> Bool Source # isUninterpreted :: Q -> Bool Source # showType :: Q -> String Source #

cv2Q :: String -> [CV] -> Q Source #

Conversion from SMT values to Q values.

_undefiner_Q :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SQ = SBV Q Source #

Symbolic version of the 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_0 :: Q

  f :: Q -> Q
  f _ = Q_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