smtlib2-1.0: A type-safe interface to communicate with an SMT solver.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Interface

Contents

Synopsis

Documentation

class Same tps Source

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)) Source 
Same ((:) Type tp ([] Type)) Source 

class IsSMTNumber tp Source

Minimal complete definition

smtNumRepr, smtFromInteger

class HasMonad a where Source

Associated Types

type MatchMonad a m :: Constraint Source

type MonadResult a :: * Source

Methods

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

Instances

HasMonad (m (List Type e tp)) Source 
HasMonad (m (e tp)) Source 
HasMonad (e tp) Source 
HasMonad (List Type e tp) Source 

Expressions

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

Constants

class SMTType t Source

Minimal complete definition

toSMTConst, fromSMTConst

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

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

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

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

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

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

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

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

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

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

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

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

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 Source

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

Equality

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

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

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

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

(.==.) :: (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 Source

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

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

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

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

(./=.) :: (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 Source

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)) Source

Comparison

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

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

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

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

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

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) Source

(.>=.) :: (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 Source

(.>.) :: (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 Source

(.<=.) :: (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 Source

(.<.) :: (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 Source

Arithmetic

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

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 Source

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

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

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

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 Source

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

(.+.) :: (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 Source

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

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

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 Source

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

(.*.) :: (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 Source

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

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

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 Source

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 Source

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

(.-.) :: (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 Source

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

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

(./.) :: (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 Source

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

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

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 Source

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

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

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 Source

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

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

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 Source

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

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

(.&.) :: (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 Source

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

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 Source

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

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

(.|.) :: (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 Source

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

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 Source

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

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

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 Source

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

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

(.=>.) :: (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 Source

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 Source

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 Source

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

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

If-then-else

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

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) Source

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 Source

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

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

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

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

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

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

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

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

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) Source

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) Source

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) Source

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) Source

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) Source

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) Source

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) Source

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) Source

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) Source

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 Source

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

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

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

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

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

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

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

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

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

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

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

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

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

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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)) Source

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

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

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

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)) Source

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

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

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 Source

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 Source

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))) Source

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)) Source

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 Source

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 Source

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 Source

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) Source

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) Source

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)) Source

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')) Source

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

Misc

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

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

Lists

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

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