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. SMTArith 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

Orphan instances

IsBitVector BVUntyped

Methods

getBVSize :: Proxy * BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Integer

SMTOrd Integer

Methods

(.<.) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Bool

(.>=.) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Bool

(.>.) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Bool

(.<=.) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Bool

SMTArith Integer

SMTValue Bool

Methods

unmangle :: Unmangling Bool

mangle :: Mangling Bool

SMTValue Integer

Methods

unmangle :: Unmangling Integer

mangle :: Mangling Integer

SMTValue UntypedValue

Methods

unmangle :: Unmangling UntypedValue

mangle :: Mangling UntypedValue

SMTType Bool

Associated Types

type SMTAnnotation Bool :: *

Methods

getSort :: Bool -> SMTAnnotation Bool -> Sort

asDataType :: Bool -> SMTAnnotation Bool -> Maybe (String, TypeCollection)

asValueType :: Bool -> SMTAnnotation Bool -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: Bool -> SMTAnnotation Bool -> [ProxyArg]

additionalConstraints :: Bool -> SMTAnnotation Bool -> Maybe (SMTExpr Bool -> [SMTExpr Bool])

annotationFromSort :: Bool -> Sort -> SMTAnnotation Bool

defaultExpr :: SMTAnnotation Bool -> SMTExpr Bool

SMTType Integer

Associated Types

type SMTAnnotation Integer :: *

Methods

getSort :: Integer -> SMTAnnotation Integer -> Sort

asDataType :: Integer -> SMTAnnotation Integer -> Maybe (String, TypeCollection)

asValueType :: Integer -> SMTAnnotation Integer -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: Integer -> SMTAnnotation Integer -> [ProxyArg]

additionalConstraints :: Integer -> SMTAnnotation Integer -> Maybe (SMTExpr Integer -> [SMTExpr Bool])

annotationFromSort :: Integer -> Sort -> SMTAnnotation Integer

defaultExpr :: SMTAnnotation Integer -> SMTExpr Integer

SMTType UntypedValue

Associated Types

type SMTAnnotation UntypedValue :: *

Methods

getSort :: UntypedValue -> SMTAnnotation UntypedValue -> Sort

asDataType :: UntypedValue -> SMTAnnotation UntypedValue -> Maybe (String, TypeCollection)

asValueType :: UntypedValue -> SMTAnnotation UntypedValue -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: UntypedValue -> SMTAnnotation UntypedValue -> [ProxyArg]

additionalConstraints :: UntypedValue -> SMTAnnotation UntypedValue -> Maybe (SMTExpr UntypedValue -> [SMTExpr Bool])

annotationFromSort :: UntypedValue -> Sort -> SMTAnnotation UntypedValue

defaultExpr :: SMTAnnotation UntypedValue -> SMTExpr UntypedValue

SMTType Untyped

Associated Types

type SMTAnnotation Untyped :: *

Methods

getSort :: Untyped -> SMTAnnotation Untyped -> Sort

asDataType :: Untyped -> SMTAnnotation Untyped -> Maybe (String, TypeCollection)

asValueType :: Untyped -> SMTAnnotation Untyped -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: Untyped -> SMTAnnotation Untyped -> [ProxyArg]

additionalConstraints :: Untyped -> SMTAnnotation Untyped -> Maybe (SMTExpr Untyped -> [SMTExpr Bool])

annotationFromSort :: Untyped -> Sort -> SMTAnnotation Untyped

defaultExpr :: SMTAnnotation Untyped -> SMTExpr Untyped

Extractable BVUntyped BVUntyped

Methods

extractAnn :: BVUntyped -> BVUntyped -> Integer -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector BVUntyped)

getExtractLen :: BVUntyped -> BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Integer

Concatable BVUntyped BVUntyped

Associated Types

type ConcatResult BVUntyped BVUntyped :: *

Methods

concatAnnotation :: BVUntyped -> BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector (ConcatResult BVUntyped BVUntyped))

TypeableNat n => Extractable BVUntyped (BVTyped n)

Methods

extractAnn :: BVUntyped -> BVTyped n -> Integer -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector (BVTyped n))

getExtractLen :: BVUntyped -> BVTyped n -> SMTAnnotation (BitVector (BVTyped n)) -> Integer

TypeableNat n2 => Concatable BVUntyped (BVTyped n2)

Associated Types

type ConcatResult BVUntyped (BVTyped n2) :: *

Methods

concatAnnotation :: BVUntyped -> BVTyped n2 -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector (BVTyped n2)) -> SMTAnnotation (BitVector (ConcatResult BVUntyped (BVTyped n2)))

Enum (SMTExpr Integer)

Methods

succ :: SMTExpr Integer -> SMTExpr Integer

pred :: SMTExpr Integer -> SMTExpr Integer

toEnum :: Int -> SMTExpr Integer

fromEnum :: SMTExpr Integer -> Int

enumFrom :: SMTExpr Integer -> [SMTExpr Integer]

enumFromThen :: SMTExpr Integer -> SMTExpr Integer -> [SMTExpr Integer]

enumFromTo :: SMTExpr Integer -> SMTExpr Integer -> [SMTExpr Integer]

enumFromThenTo :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer -> [SMTExpr Integer]

Eq a => Eq (SMTExpr a)

Methods

(==) :: SMTExpr a -> SMTExpr a -> Bool

(/=) :: SMTExpr a -> SMTExpr a -> Bool

Fractional (SMTExpr (Ratio Integer))

Methods

(/) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

recip :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

fromRational :: Rational -> SMTExpr (Ratio Integer)

TypeableNat n => Num (BitVector (BVTyped n))

Methods

(+) :: BitVector (BVTyped n) -> BitVector (BVTyped n) -> BitVector (BVTyped n)

(-) :: BitVector (BVTyped n) -> BitVector (BVTyped n) -> BitVector (BVTyped n)

(*) :: BitVector (BVTyped n) -> BitVector (BVTyped n) -> BitVector (BVTyped n)

negate :: BitVector (BVTyped n) -> BitVector (BVTyped n)

abs :: BitVector (BVTyped n) -> BitVector (BVTyped n)

signum :: BitVector (BVTyped n) -> BitVector (BVTyped n)

fromInteger :: Integer -> BitVector (BVTyped n)

Num (SMTExpr Integer)

Methods

(+) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

(-) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

(*) :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

negate :: SMTExpr Integer -> SMTExpr Integer

abs :: SMTExpr Integer -> SMTExpr Integer

signum :: SMTExpr Integer -> SMTExpr Integer

fromInteger :: Integer -> SMTExpr Integer

Num (SMTExpr (Ratio Integer))

Methods

(+) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

(-) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

(*) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

negate :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

abs :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

signum :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer)

fromInteger :: Integer -> SMTExpr (Ratio Integer)

TypeableNat n => Num (SMTExpr (BitVector (BVTyped n)))

Methods

(+) :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

(-) :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

(*) :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

negate :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

abs :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

signum :: SMTExpr (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

fromInteger :: Integer -> SMTExpr (BitVector (BVTyped n))

SMTType t => Ord (SMTExpr t)

Methods

compare :: SMTExpr t -> SMTExpr t -> Ordering

(<) :: SMTExpr t -> SMTExpr t -> Bool

(<=) :: SMTExpr t -> SMTExpr t -> Bool

(>) :: SMTExpr t -> SMTExpr t -> Bool

(>=) :: SMTExpr t -> SMTExpr t -> Bool

max :: SMTExpr t -> SMTExpr t -> SMTExpr t

min :: SMTExpr t -> SMTExpr t -> SMTExpr t

LiftArgs a => LiftArgs [a]

Associated Types

type Unpacked [a] :: *

Methods

liftArgs :: Unpacked [a] -> ArgAnnotation [a] -> [a]

unliftArgs :: Monad m => [a] -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked [a])

LiftArgs a => LiftArgs (Maybe a)

Associated Types

type Unpacked (Maybe a) :: *

Methods

liftArgs :: Unpacked (Maybe a) -> ArgAnnotation (Maybe a) -> Maybe a

unliftArgs :: Monad m => Maybe a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (Maybe a))

SMTValue a => LiftArgs (SMTExpr a)

Associated Types

type Unpacked (SMTExpr a) :: *

Methods

liftArgs :: Unpacked (SMTExpr a) -> ArgAnnotation (SMTExpr a) -> SMTExpr a

unliftArgs :: Monad m => SMTExpr a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (SMTExpr a))

SMTType a => Liftable [SMTExpr a]

Associated Types

type Lifted [SMTExpr a] i :: *

Methods

getLiftedArgumentAnn :: [SMTExpr a] -> i -> ArgAnnotation [SMTExpr a] -> ArgAnnotation i -> ArgAnnotation (Lifted [SMTExpr a] i)

inferLiftedAnnotation :: [SMTExpr a] -> i -> ArgAnnotation (Lifted [SMTExpr a] i) -> (ArgAnnotation i, ArgAnnotation [SMTExpr a])

getConstraint :: Args i => p ([SMTExpr a], i) -> Dict (Liftable (Lifted [SMTExpr a] i))

SMTType a => Liftable (SMTExpr a)

Associated Types

type Lifted (SMTExpr a) i :: *

Methods

getLiftedArgumentAnn :: SMTExpr a -> i -> ArgAnnotation (SMTExpr a) -> ArgAnnotation i -> ArgAnnotation (Lifted (SMTExpr a) i)

inferLiftedAnnotation :: SMTExpr a -> i -> ArgAnnotation (Lifted (SMTExpr a) i) -> (ArgAnnotation i, ArgAnnotation (SMTExpr a))

getConstraint :: Args i => p (SMTExpr a, i) -> Dict (Liftable (Lifted (SMTExpr a) i))

Args a => Args [a]

Associated Types

type ArgAnnotation [a] :: *

Methods

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

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [([a], b)] -> ArgAnnotation [a] -> m (s, [[a]], [a])

extractArgAnnotation :: [a] -> ArgAnnotation [a]

toArgs :: ArgAnnotation [a] -> [SMTExpr Untyped] -> Maybe ([a], [SMTExpr Untyped])

fromArgs :: [a] -> [SMTExpr Untyped]

getTypes :: [a] -> ArgAnnotation [a] -> [ProxyArg]

getArgAnnotation :: [a] -> [Sort] -> (ArgAnnotation [a], [Sort])

Args a => Args (Maybe a)

Associated Types

type ArgAnnotation (Maybe a) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> Maybe a -> ArgAnnotation (Maybe a) -> m (s, Maybe a)

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(Maybe a, b)] -> ArgAnnotation (Maybe a) -> m (s, [Maybe a], Maybe a)

extractArgAnnotation :: Maybe a -> ArgAnnotation (Maybe a)

toArgs :: ArgAnnotation (Maybe a) -> [SMTExpr Untyped] -> Maybe (Maybe a, [SMTExpr Untyped])

fromArgs :: Maybe a -> [SMTExpr Untyped]

getTypes :: Maybe a -> ArgAnnotation (Maybe a) -> [ProxyArg]

getArgAnnotation :: Maybe a -> [Sort] -> (ArgAnnotation (Maybe a), [Sort])

SMTType a => Args (SMTExpr a)

Associated Types

type ArgAnnotation (SMTExpr a) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> SMTExpr a -> ArgAnnotation (SMTExpr a) -> m (s, SMTExpr a)

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(SMTExpr a, b)] -> ArgAnnotation (SMTExpr a) -> m (s, [SMTExpr a], SMTExpr a)

extractArgAnnotation :: SMTExpr a -> ArgAnnotation (SMTExpr a)

toArgs :: ArgAnnotation (SMTExpr a) -> [SMTExpr Untyped] -> Maybe (SMTExpr a, [SMTExpr Untyped])

fromArgs :: SMTExpr a -> [SMTExpr Untyped]

getTypes :: SMTExpr a -> ArgAnnotation (SMTExpr a) -> [ProxyArg]

getArgAnnotation :: SMTExpr a -> [Sort] -> (ArgAnnotation (SMTExpr a), [Sort])

TypeableNat n => IsBitVector (BVTyped n)

Methods

getBVSize :: Proxy * (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> Integer

SMTOrd (Ratio Integer)

Methods

(.<.) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr Bool

(.>=.) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr Bool

(.>.) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr Bool

(.<=.) :: SMTExpr (Ratio Integer) -> SMTExpr (Ratio Integer) -> SMTExpr Bool

SMTArith (Ratio Integer)

(Typeable * a, SMTValue a) => SMTValue [a]

Methods

unmangle :: Unmangling [a]

mangle :: Mangling [a]

SMTValue a => SMTValue (Maybe a)

Methods

unmangle :: Unmangling (Maybe a)

mangle :: Mangling (Maybe a)

SMTValue (Ratio Integer)

Methods

unmangle :: Unmangling (Ratio Integer)

mangle :: Mangling (Ratio Integer)

TypeableNat n => SMTValue (BitVector (BVTyped n))

Methods

unmangle :: Unmangling (BitVector (BVTyped n))

mangle :: Mangling (BitVector (BVTyped n))

SMTValue (BitVector BVUntyped)

Methods

unmangle :: Unmangling (BitVector BVUntyped)

mangle :: Mangling (BitVector BVUntyped)

(Typeable * a, SMTType a) => SMTType [a]

Associated Types

type SMTAnnotation [a] :: *

Methods

getSort :: [a] -> SMTAnnotation [a] -> Sort

asDataType :: [a] -> SMTAnnotation [a] -> Maybe (String, TypeCollection)

asValueType :: [a] -> SMTAnnotation [a] -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: [a] -> SMTAnnotation [a] -> [ProxyArg]

additionalConstraints :: [a] -> SMTAnnotation [a] -> Maybe (SMTExpr [a] -> [SMTExpr Bool])

annotationFromSort :: [a] -> Sort -> SMTAnnotation [a]

defaultExpr :: SMTAnnotation [a] -> SMTExpr [a]

SMTType a => SMTType (Maybe a)

Associated Types

type SMTAnnotation (Maybe a) :: *

Methods

getSort :: Maybe a -> SMTAnnotation (Maybe a) -> Sort

asDataType :: Maybe a -> SMTAnnotation (Maybe a) -> Maybe (String, TypeCollection)

asValueType :: Maybe a -> SMTAnnotation (Maybe a) -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: Maybe a -> SMTAnnotation (Maybe a) -> [ProxyArg]

additionalConstraints :: Maybe a -> SMTAnnotation (Maybe a) -> Maybe (SMTExpr (Maybe a) -> [SMTExpr Bool])

annotationFromSort :: Maybe a -> Sort -> SMTAnnotation (Maybe a)

defaultExpr :: SMTAnnotation (Maybe a) -> SMTExpr (Maybe a)

SMTType (Ratio Integer)

Associated Types

type SMTAnnotation (Ratio Integer) :: *

Methods

getSort :: Ratio Integer -> SMTAnnotation (Ratio Integer) -> Sort

asDataType :: Ratio Integer -> SMTAnnotation (Ratio Integer) -> Maybe (String, TypeCollection)

asValueType :: Ratio Integer -> SMTAnnotation (Ratio Integer) -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: Ratio Integer -> SMTAnnotation (Ratio Integer) -> [ProxyArg]

additionalConstraints :: Ratio Integer -> SMTAnnotation (Ratio Integer) -> Maybe (SMTExpr (Ratio Integer) -> [SMTExpr Bool])

annotationFromSort :: Ratio Integer -> Sort -> SMTAnnotation (Ratio Integer)

defaultExpr :: SMTAnnotation (Ratio Integer) -> SMTExpr (Ratio Integer)

TypeableNat n => SMTType (BitVector (BVTyped n))

Associated Types

type SMTAnnotation (BitVector (BVTyped n)) :: *

Methods

getSort :: BitVector (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> Sort

asDataType :: BitVector (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> Maybe (String, TypeCollection)

asValueType :: BitVector (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: BitVector (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> [ProxyArg]

additionalConstraints :: BitVector (BVTyped n) -> SMTAnnotation (BitVector (BVTyped n)) -> Maybe (SMTExpr (BitVector (BVTyped n)) -> [SMTExpr Bool])

annotationFromSort :: BitVector (BVTyped n) -> Sort -> SMTAnnotation (BitVector (BVTyped n))

defaultExpr :: SMTAnnotation (BitVector (BVTyped n)) -> SMTExpr (BitVector (BVTyped n))

SMTType (BitVector BVUntyped)

Associated Types

type SMTAnnotation (BitVector BVUntyped) :: *

Methods

getSort :: BitVector BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Sort

asDataType :: BitVector BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Maybe (String, TypeCollection)

asValueType :: BitVector BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: BitVector BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> [ProxyArg]

additionalConstraints :: BitVector BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Maybe (SMTExpr (BitVector BVUntyped) -> [SMTExpr Bool])

annotationFromSort :: BitVector BVUntyped -> Sort -> SMTAnnotation (BitVector BVUntyped)

defaultExpr :: SMTAnnotation (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)

TypeableNat n => Extractable (BVTyped n) BVUntyped

Methods

extractAnn :: BVTyped n -> BVUntyped -> Integer -> SMTAnnotation (BitVector (BVTyped n)) -> SMTAnnotation (BitVector BVUntyped)

getExtractLen :: BVTyped n -> BVUntyped -> SMTAnnotation (BitVector BVUntyped) -> Integer

TypeableNat n1 => Concatable (BVTyped n1) BVUntyped

Associated Types

type ConcatResult (BVTyped n1) BVUntyped :: *

Methods

concatAnnotation :: BVTyped n1 -> BVUntyped -> SMTAnnotation (BitVector (BVTyped n1)) -> SMTAnnotation (BitVector BVUntyped) -> SMTAnnotation (BitVector (ConcatResult (BVTyped n1) BVUntyped))

(TypeableNat n1, TypeableNat n2) => Extractable (BVTyped n1) (BVTyped n2)

Methods

extractAnn :: BVTyped n1 -> BVTyped n2 -> Integer -> SMTAnnotation (BitVector (BVTyped n1)) -> SMTAnnotation (BitVector (BVTyped n2))

getExtractLen :: BVTyped n1 -> BVTyped n2 -> SMTAnnotation (BitVector (BVTyped n2)) -> Integer

(TypeableNat n1, TypeableNat n2, TypeableNat (Add n1 n2)) => Concatable (BVTyped n1) (BVTyped n2)

Associated Types

type ConcatResult (BVTyped n1) (BVTyped n2) :: *

Methods

concatAnnotation :: BVTyped n1 -> BVTyped n2 -> SMTAnnotation (BitVector (BVTyped n1)) -> SMTAnnotation (BitVector (BVTyped n2)) -> SMTAnnotation (BitVector (ConcatResult (BVTyped n1) (BVTyped n2)))

Eq (Field a f)

Methods

(==) :: Field a f -> Field a f -> Bool

(/=) :: Field a f -> Field a f -> Bool

Eq (Constructor arg res)

Methods

(==) :: Constructor arg res -> Constructor arg res -> Bool

(/=) :: Constructor arg res -> Constructor arg res -> Bool

Args arg => Eq (SMTFunction arg res)

Methods

(==) :: SMTFunction arg res -> SMTFunction arg res -> Bool

(/=) :: SMTFunction arg res -> SMTFunction arg res -> Bool

Ord (Field a f)

Methods

compare :: Field a f -> Field a f -> Ordering

(<) :: Field a f -> Field a f -> Bool

(<=) :: Field a f -> Field a f -> Bool

(>) :: Field a f -> Field a f -> Bool

(>=) :: Field a f -> Field a f -> Bool

max :: Field a f -> Field a f -> Field a f

min :: Field a f -> Field a f -> Field a f

Ord (Constructor arg res)

Methods

compare :: Constructor arg res -> Constructor arg res -> Ordering

(<) :: Constructor arg res -> Constructor arg res -> Bool

(<=) :: Constructor arg res -> Constructor arg res -> Bool

(>) :: Constructor arg res -> Constructor arg res -> Bool

(>=) :: Constructor arg res -> Constructor arg res -> Bool

max :: Constructor arg res -> Constructor arg res -> Constructor arg res

min :: Constructor arg res -> Constructor arg res -> Constructor arg res

Args arg => Ord (SMTFunction arg res)

Methods

compare :: SMTFunction arg res -> SMTFunction arg res -> Ordering

(<) :: SMTFunction arg res -> SMTFunction arg res -> Bool

(<=) :: SMTFunction arg res -> SMTFunction arg res -> Bool

(>) :: SMTFunction arg res -> SMTFunction arg res -> Bool

(>=) :: SMTFunction arg res -> SMTFunction arg res -> Bool

max :: SMTFunction arg res -> SMTFunction arg res -> SMTFunction arg res

min :: SMTFunction arg res -> SMTFunction arg res -> SMTFunction arg res

(LiftArgs a, LiftArgs b) => LiftArgs (Either a b)

Associated Types

type Unpacked (Either a b) :: *

Methods

liftArgs :: Unpacked (Either a b) -> ArgAnnotation (Either a b) -> Either a b

unliftArgs :: Monad m => Either a b -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (Either a b))

(LiftArgs a, LiftArgs b) => LiftArgs (a, b)

Associated Types

type Unpacked (a, b) :: *

Methods

liftArgs :: Unpacked (a, b) -> ArgAnnotation (a, b) -> (a, b)

unliftArgs :: Monad m => (a, b) -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (a, b))

(Typeable * a, Show a, Ord a, LiftArgs b) => LiftArgs (Map a b)

Associated Types

type Unpacked (Map a b) :: *

Methods

liftArgs :: Unpacked (Map a b) -> ArgAnnotation (Map a b) -> Map a b

unliftArgs :: Monad m => Map a b -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (Map a b))

(Liftable a, Liftable b) => Liftable (a, b)

Associated Types

type Lifted (a, b) i :: *

Methods

getLiftedArgumentAnn :: (a, b) -> i -> ArgAnnotation (a, b) -> ArgAnnotation i -> ArgAnnotation (Lifted (a, b) i)

inferLiftedAnnotation :: (a, b) -> i -> ArgAnnotation (Lifted (a, b) i) -> (ArgAnnotation i, ArgAnnotation (a, b))

getConstraint :: Args i => p ((a, b), i) -> Dict (Liftable (Lifted (a, b) i))

(Args a, Args b) => Args (Either a b)

Associated Types

type ArgAnnotation (Either a b) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> Either a b -> ArgAnnotation (Either a b) -> m (s, Either a b)

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(Either a b, b)] -> ArgAnnotation (Either a b) -> m (s, [Either a b], Either a b)

extractArgAnnotation :: Either a b -> ArgAnnotation (Either a b)

toArgs :: ArgAnnotation (Either a b) -> [SMTExpr Untyped] -> Maybe (Either a b, [SMTExpr Untyped])

fromArgs :: Either a b -> [SMTExpr Untyped]

getTypes :: Either a b -> ArgAnnotation (Either a b) -> [ProxyArg]

getArgAnnotation :: Either a b -> [Sort] -> (ArgAnnotation (Either a b), [Sort])

(Args a, Args b) => Args (a, b)

Associated Types

type ArgAnnotation (a, b) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> (a, b) -> ArgAnnotation (a, b) -> m (s, (a, b))

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((a, b), b)] -> ArgAnnotation (a, b) -> m (s, [(a, b)], (a, b))

extractArgAnnotation :: (a, b) -> ArgAnnotation (a, b)

toArgs :: ArgAnnotation (a, b) -> [SMTExpr Untyped] -> Maybe ((a, b), [SMTExpr Untyped])

fromArgs :: (a, b) -> [SMTExpr Untyped]

getTypes :: (a, b) -> ArgAnnotation (a, b) -> [ProxyArg]

getArgAnnotation :: (a, b) -> [Sort] -> (ArgAnnotation (a, b), [Sort])

(Typeable * a, Show a, Args b, Ord a) => Args (Map a b)

Associated Types

type ArgAnnotation (Map a b) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> Map a b -> ArgAnnotation (Map a b) -> m (s, Map a b)

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(Map a b, b)] -> ArgAnnotation (Map a b) -> m (s, [Map a b], Map a b)

extractArgAnnotation :: Map a b -> ArgAnnotation (Map a b)

toArgs :: ArgAnnotation (Map a b) -> [SMTExpr Untyped] -> Maybe (Map a b, [SMTExpr Untyped])

fromArgs :: Map a b -> [SMTExpr Untyped]

getTypes :: Map a b -> ArgAnnotation (Map a b) -> [ProxyArg]

getArgAnnotation :: Map a b -> [Sort] -> (ArgAnnotation (Map a b), [Sort])

(Args idx, SMTType val) => SMTType (SMTArray idx val)

Associated Types

type SMTAnnotation (SMTArray idx val) :: *

Methods

getSort :: SMTArray idx val -> SMTAnnotation (SMTArray idx val) -> Sort

asDataType :: SMTArray idx val -> SMTAnnotation (SMTArray idx val) -> Maybe (String, TypeCollection)

asValueType :: SMTArray idx val -> SMTAnnotation (SMTArray idx val) -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: SMTArray idx val -> SMTAnnotation (SMTArray idx val) -> [ProxyArg]

additionalConstraints :: SMTArray idx val -> SMTAnnotation (SMTArray idx val) -> Maybe (SMTExpr (SMTArray idx val) -> [SMTExpr Bool])

annotationFromSort :: SMTArray idx val -> Sort -> SMTAnnotation (SMTArray idx val)

defaultExpr :: SMTAnnotation (SMTArray idx val) -> SMTExpr (SMTArray idx val)

(LiftArgs a, LiftArgs b, LiftArgs c) => LiftArgs (a, b, c)

Associated Types

type Unpacked (a, b, c) :: *

Methods

liftArgs :: Unpacked (a, b, c) -> ArgAnnotation (a, b, c) -> (a, b, c)

unliftArgs :: Monad m => (a, b, c) -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (a, b, c))

(Liftable a, Liftable b, Liftable c) => Liftable (a, b, c)

Associated Types

type Lifted (a, b, c) i :: *

Methods

getLiftedArgumentAnn :: (a, b, c) -> i -> ArgAnnotation (a, b, c) -> ArgAnnotation i -> ArgAnnotation (Lifted (a, b, c) i)

inferLiftedAnnotation :: (a, b, c) -> i -> ArgAnnotation (Lifted (a, b, c) i) -> (ArgAnnotation i, ArgAnnotation (a, b, c))

getConstraint :: Args i => p ((a, b, c), i) -> Dict (Liftable (Lifted (a, b, c) i))

(Args a, Args b, Args c) => Args (a, b, c)

Associated Types

type ArgAnnotation (a, b, c) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> (a, b, c) -> ArgAnnotation (a, b, c) -> m (s, (a, b, c))

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((a, b, c), b)] -> ArgAnnotation (a, b, c) -> m (s, [(a, b, c)], (a, b, c))

extractArgAnnotation :: (a, b, c) -> ArgAnnotation (a, b, c)

toArgs :: ArgAnnotation (a, b, c) -> [SMTExpr Untyped] -> Maybe ((a, b, c), [SMTExpr Untyped])

fromArgs :: (a, b, c) -> [SMTExpr Untyped]

getTypes :: (a, b, c) -> ArgAnnotation (a, b, c) -> [ProxyArg]

getArgAnnotation :: (a, b, c) -> [Sort] -> (ArgAnnotation (a, b, c), [Sort])

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d) => LiftArgs (a, b, c, d)

Associated Types

type Unpacked (a, b, c, d) :: *

Methods

liftArgs :: Unpacked (a, b, c, d) -> ArgAnnotation (a, b, c, d) -> (a, b, c, d)

unliftArgs :: Monad m => (a, b, c, d) -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (a, b, c, d))

(Liftable a, Liftable b, Liftable c, Liftable d) => Liftable (a, b, c, d)

Associated Types

type Lifted (a, b, c, d) i :: *

Methods

getLiftedArgumentAnn :: (a, b, c, d) -> i -> ArgAnnotation (a, b, c, d) -> ArgAnnotation i -> ArgAnnotation (Lifted (a, b, c, d) i)

inferLiftedAnnotation :: (a, b, c, d) -> i -> ArgAnnotation (Lifted (a, b, c, d) i) -> (ArgAnnotation i, ArgAnnotation (a, b, c, d))

getConstraint :: Args i => p ((a, b, c, d), i) -> Dict (Liftable (Lifted (a, b, c, d) i))

(Args a, Args b, Args c, Args d) => Args (a, b, c, d)

Associated Types

type ArgAnnotation (a, b, c, d) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> (a, b, c, d) -> ArgAnnotation (a, b, c, d) -> m (s, (a, b, c, d))

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((a, b, c, d), b)] -> ArgAnnotation (a, b, c, d) -> m (s, [(a, b, c, d)], (a, b, c, d))

extractArgAnnotation :: (a, b, c, d) -> ArgAnnotation (a, b, c, d)

toArgs :: ArgAnnotation (a, b, c, d) -> [SMTExpr Untyped] -> Maybe ((a, b, c, d), [SMTExpr Untyped])

fromArgs :: (a, b, c, d) -> [SMTExpr Untyped]

getTypes :: (a, b, c, d) -> ArgAnnotation (a, b, c, d) -> [ProxyArg]

getArgAnnotation :: (a, b, c, d) -> [Sort] -> (ArgAnnotation (a, b, c, d), [Sort])

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d, LiftArgs e) => LiftArgs (a, b, c, d, e)

Associated Types

type Unpacked (a, b, c, d, e) :: *

Methods

liftArgs :: Unpacked (a, b, c, d, e) -> ArgAnnotation (a, b, c, d, e) -> (a, b, c, d, e)

unliftArgs :: Monad m => (a, b, c, d, e) -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (a, b, c, d, e))

(Liftable a, Liftable b, Liftable c, Liftable d, Liftable e) => Liftable (a, b, c, d, e)

Associated Types

type Lifted (a, b, c, d, e) i :: *

Methods

getLiftedArgumentAnn :: (a, b, c, d, e) -> i -> ArgAnnotation (a, b, c, d, e) -> ArgAnnotation i -> ArgAnnotation (Lifted (a, b, c, d, e) i)

inferLiftedAnnotation :: (a, b, c, d, e) -> i -> ArgAnnotation (Lifted (a, b, c, d, e) i) -> (ArgAnnotation i, ArgAnnotation (a, b, c, d, e))

getConstraint :: Args i => p ((a, b, c, d, e), i) -> Dict (Liftable (Lifted (a, b, c, d, e) i))

(Args a, Args b, Args c, Args d, Args e) => Args (a, b, c, d, e)

Associated Types

type ArgAnnotation (a, b, c, d, e) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> (a, b, c, d, e) -> ArgAnnotation (a, b, c, d, e) -> m (s, (a, b, c, d, e))

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((a, b, c, d, e), b)] -> ArgAnnotation (a, b, c, d, e) -> m (s, [(a, b, c, d, e)], (a, b, c, d, e))

extractArgAnnotation :: (a, b, c, d, e) -> ArgAnnotation (a, b, c, d, e)

toArgs :: ArgAnnotation (a, b, c, d, e) -> [SMTExpr Untyped] -> Maybe ((a, b, c, d, e), [SMTExpr Untyped])

fromArgs :: (a, b, c, d, e) -> [SMTExpr Untyped]

getTypes :: (a, b, c, d, e) -> ArgAnnotation (a, b, c, d, e) -> [ProxyArg]

getArgAnnotation :: (a, b, c, d, e) -> [Sort] -> (ArgAnnotation (a, b, c, d, e), [Sort])

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d, LiftArgs e, LiftArgs f) => LiftArgs (a, b, c, d, e, f)

Associated Types

type Unpacked (a, b, c, d, e, f) :: *

Methods

liftArgs :: Unpacked (a, b, c, d, e, f) -> ArgAnnotation (a, b, c, d, e, f) -> (a, b, c, d, e, f)

unliftArgs :: Monad m => (a, b, c, d, e, f) -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked (a, b, c, d, e, f))

(Liftable a, Liftable b, Liftable c, Liftable d, Liftable e, Liftable f) => Liftable (a, b, c, d, e, f)

Associated Types

type Lifted (a, b, c, d, e, f) i :: *

Methods

getLiftedArgumentAnn :: (a, b, c, d, e, f) -> i -> ArgAnnotation (a, b, c, d, e, f) -> ArgAnnotation i -> ArgAnnotation (Lifted (a, b, c, d, e, f) i)

inferLiftedAnnotation :: (a, b, c, d, e, f) -> i -> ArgAnnotation (Lifted (a, b, c, d, e, f) i) -> (ArgAnnotation i, ArgAnnotation (a, b, c, d, e, f))

getConstraint :: Args i => p ((a, b, c, d, e, f), i) -> Dict (Liftable (Lifted (a, b, c, d, e, f) i))

(Args a, Args b, Args c, Args d, Args e, Args f) => Args (a, b, c, d, e, f)

Associated Types

type ArgAnnotation (a, b, c, d, e, f) :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> (a, b, c, d, e, f) -> ArgAnnotation (a, b, c, d, e, f) -> m (s, (a, b, c, d, e, f))

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((a, b, c, d, e, f), b)] -> ArgAnnotation (a, b, c, d, e, f) -> m (s, [(a, b, c, d, e, f)], (a, b, c, d, e, f))

extractArgAnnotation :: (a, b, c, d, e, f) -> ArgAnnotation (a, b, c, d, e, f)

toArgs :: ArgAnnotation (a, b, c, d, e, f) -> [SMTExpr Untyped] -> Maybe ((a, b, c, d, e, f), [SMTExpr Untyped])

fromArgs :: (a, b, c, d, e, f) -> [SMTExpr Untyped]

getTypes :: (a, b, c, d, e, f) -> ArgAnnotation (a, b, c, d, e, f) -> [ProxyArg]

getArgAnnotation :: (a, b, c, d, e, f) -> [Sort] -> (ArgAnnotation (a, b, c, d, e, f), [Sort])