Language.SMTLib2.Internals.Instances

Implements various instance declarations for SMTType, SMTValue, etc.

Documentation

valueToHaskell :: DataTypeInfo -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> Maybe Sort -> Value -> r

extractAnnotation :: SMTExpr a -> SMTAnnotation a

Reconstruct the type annotation for a given SMT expression.

inferResAnnotation :: SMTFunction arg res -> ArgAnnotation arg -> SMTAnnotation res

entype :: (forall a. SMTType a => SMTExpr a -> b) -> SMTExpr Untyped -> b

entypeValue :: (forall a. SMTValue a => SMTExpr a -> b) -> SMTExpr UntypedValue -> b

castUntypedExpr :: SMTType t => SMTExpr Untyped -> SMTExpr t

castUntypedExprValue :: SMTType t => SMTExpr UntypedValue -> SMTExpr t

dtMaybe :: DataType

conNothing :: Constr

conJust :: Constr

nothing' :: SMTType a => SMTAnnotation a -> Constructor () (Maybe a)

just' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a) (Maybe a)

fieldFromJust :: DataField

undefArg :: b a -> a

Get an undefined value of the type argument of a type.

dtList :: DataType

conNil :: Constr

conInsert :: Constr

insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a, SMTExpr [a]) [a]

nil' :: SMTType a => SMTAnnotation a -> Constructor () [a]

fieldHead :: DataField

fieldTail :: DataField

bvUnsigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer

bvSigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer

bvRestrict :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> BitVector a

withSort :: DataTypeInfo -> Sort -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r

withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTType t, Num t) => t -> SMTAnnotation t -> r) -> Maybe r

withSorts :: DataTypeInfo -> [Sort] -> (forall arg. Liftable arg => arg -> ArgAnnotation arg -> r) -> r

withArraySort :: DataTypeInfo -> [Sort] -> Sort -> (forall i v. (Liftable i, SMTType v) => SMTArray i v -> (ArgAnnotation i, SMTAnnotation v) -> a) -> a

foldExprM :: (SMTType a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> SMTExpr a -> m (s, [SMTExpr a])

Recursively fold a monadic function over all sub-expressions of this expression

foldArgsM :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> a -> m (s, [a])

Recursively fold a monadic function over all sub-expressions of the argument

foldExpr :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> SMTExpr a -> (s, SMTExpr a)

Recursively fold a function over all sub-expressions of this expression. It is implemented as a special case of foldExprM.

foldExprMux :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, [SMTExpr t])) -> s -> SMTExpr a -> (s, [SMTExpr a])

foldArgs :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> a -> (s, a)

Recursively fold a function over all sub-expressions of the argument. It is implemented as a special case of foldArgsM.

foldArgsMux :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, [SMTExpr t])) -> s -> a -> (s, [a])

compareFun :: (Args a1, Args a2) => SMTFunction a1 r1 -> SMTFunction a2 r2 -> Ordering

compareConstructor :: Constructor arg1 res1 -> Constructor arg2 res2 -> Ordering

compareField :: Field a1 f1 -> Field a2 f2 -> Ordering

compareArgs :: (Args a1, Args a2) => a1 -> a2 -> Ordering

compareExprs :: (SMTType t1, SMTType t2) => SMTExpr t1 -> SMTExpr t2 -> Ordering

eqExpr :: SMTExpr a -> SMTExpr a -> Maybe Bool

valueToConst :: DataTypeInfo -> Value -> (forall a. SMTType a => [ProxyArg] -> a -> SMTAnnotation a -> b) -> b