Language.Fixpoint.Bitvector

Constructor

data Bv

Constructors

Bv BvSize String

Instances

Expression Bv

Construct an Expr using a raw string, e.g. (Bv S32 "#x02000000")

Sizes

data BvSize

Constructors

S32

S64

Instances

Eq BvSize

Data BvSize

Ord BvSize

Show BvSize

Generic BvSize

Typeable * BvSize

type Rep BvSize

Operators

data BvOp

Constructors

BvAnd

BvOr

Instances

Eq BvOp

Data BvOp

Ord BvOp

Show BvOp

Generic BvOp

Typeable * BvOp

type Rep BvOp

BitVector Sort Constructor

mkSort :: BvSize -> Sort

Construct the bitvector Sort from its BvSize

BitVector Expression Constructor

eOp :: BvOp -> [Expr] -> Expr

Apply some bitvector operator to a list of arguments

BitVector Type Constructor

bvTyCon :: FTycon