Language.SMTLib2.Internals.Interface

Documentation

class Same tps

All elements of this list must be of the same type

Minimal complete definition

sameType, sameToAllEq

Instances

(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps))

Same ((:) Type tp ([] Type))

class IsSMTNumber tp

Minimal complete definition

smtNumRepr, smtFromInteger

Instances

IsSMTNumber IntType

IsSMTNumber RealType

class HasMonad a where

Associated Types

type MatchMonad a m :: Constraint

type MonadResult a :: *

Methods

embedM :: (Monad m, MatchMonad a m) => a -> m (MonadResult a)

Instances

HasMonad (m (List Type e tp))

HasMonad (m (e tp))

HasMonad (e tp)

HasMonad (List Type e tp)

Expressions

pattern Var :: (~) Type tp rtp => v tp -> Expression v qv fun con field fv lv e rtp

Constants

class SMTType t

Minimal complete definition

toSMTConst, fromSMTConst

Instances

SMTType Bool

SMTType Integer

SMTType (Ratio Integer)

pattern ConstBool :: (~) Type rtp BoolType => Bool -> Expression v qv fun con field fv lv e rtp

pattern ConstInt :: (~) Type rtp IntType => Integer -> Expression v qv fun con field fv lv e rtp

pattern ConstReal :: (~) Type rtp RealType => Rational -> Expression v qv fun con field fv lv e rtp

pattern ConstBV :: (~) Type rtp (BitVecType bw) => Integer -> Natural bw -> Expression v qv fun con field fv lv e rtp

constant :: (Embed m e, SMTType tp) => tp -> m (e (SMTReprType tp))

asConstant :: SMTType tp => Expression v qv fun con field fv lv e (SMTReprType tp) -> Maybe tp

true :: Embed m e => m (e BoolType)

false :: Embed m e => m (e BoolType)

cbool :: Embed m e => Bool -> m (e BoolType)

cint :: Embed m e => Integer -> m (e IntType)

creal :: Embed m e => Rational -> m (e RealType)

cbv :: Embed m e => Integer -> Natural bw -> m (e (BitVecType bw))

Functions

pattern Fun :: (~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type arg res) => t ((,) [Type] Type arg res) -> List Type t arg -> Expression t t t t t t t t t

fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e `(args, res)` -> a -> m (e res)

Equality

pattern EqLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp

pattern Eq :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:==:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

pattern DistinctLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp

pattern Distinct :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:/=:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

Map

map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e), GetFieldType (EmField m e), GetConType (EmConstr m e)) => Function (EmFun m e) (EmConstr m e) (EmField m e) `(tps, res)` -> arg -> m (e (ArrayType idx res))

Comparison

pattern Ord :: ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:>=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:>:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:<=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

pattern (:<:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp

ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType)

(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4

Arithmetic

pattern ArithLst :: IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun con field fv lv e tp

pattern Arith :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun con field fv lv e tp

arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp)

pattern PlusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Plus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:+:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6

pattern MultLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Mult :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:*:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 7

pattern MinusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp

pattern Minus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp

pattern (:-:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp

pattern Neg :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> Expression v qv fun con field fv lv e tp

minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)

(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6

neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

pattern Div :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

pattern Mod :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

pattern Rem :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7

pattern (:/:) :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t

(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType) infixl 7

pattern Abs :: IsSMTNumber tp => e tp -> Expression v qv fun con field fv lv e tp

abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

Logic

pattern Not :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)

pattern LogicLst :: (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Logic :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun con field fv lv e rtp

logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)

pattern AndLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern And :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:&:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 3

pattern OrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Or :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:|:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2

pattern XOrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern XOr :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

pattern ImpliesLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp

pattern Implies :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp

pattern (:=>:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp

implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2

Conversion

pattern ToReal :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

pattern ToInt :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t

toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType)

toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType)

If-then-else

pattern ITE :: () => GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun con field fv lv e tp

ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp)

Bitvectors

pattern BVComp :: (~) Type rtp BoolType => GetType e => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVULE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVULT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSLE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSLT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType)

bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)

pattern BVBin :: (~) Type rtp (BitVecType bw) => GetType e => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVAdd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSub :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVMul :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVURem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSRem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVUDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVSHL :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVLSHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVASHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVXor :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVAnd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVOr :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw))

bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))

pattern BVUn :: (~) Type rtp (BitVecType bw) => GetType e => BVUnOp -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVNot :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

pattern BVNeg :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw))

bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))

bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))

pattern Concat :: (~) Type rtp (BitVecType ((+) n1 n2)) => GetType e => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun con field fv lv e rtp

pattern Extract :: ((~) Type rtp (BitVecType len), (~) Bool ((<=) ((+) start len) bw) True) => GetType e => Natural start -> Natural len -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp

concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2)))

extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), ((start + len) <= bw) ~ True) => Natural start -> Natural len -> a -> m (e (BitVecType len))

Arrays

pattern Select :: (~) Type rtp val => GetType e => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun con field fv lv e rtp

pattern Store :: (~) Type rtp (ArrayType idx val) => GetType e => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun con field fv lv e rtp

pattern ConstArray :: (~) Type rtp (ArrayType idx val) => GetType e => List Type Repr idx -> e val -> Expression v qv fun con field fv lv e rtp

select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el)

select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType `[idx']` el), MonadResult idx ~ e idx') => arr -> idx -> m (e el)

store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el))

store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType `[idx']` el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType `[idx']` el'))

constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))

Misc

pattern Divisible :: (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun con field fv lv e rtp

divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)

Lists

(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Monad m) => a -> m (List e tps) -> m (List e (tp : tps)) infixr 5

nil :: Monad m => m (List e `[]`)