liquid-fixpoint-0.4.0.0: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Bitvector

Contents

Constructor
Sizes
Operators
BitVector Sort Constructor
BitVector Expression Constructor
BitVector Type Constructor

Synopsis

Constructor

Constructors

Bv BvSize String

Instances

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

Sizes

data BvSize Source

Constructors

S32
S64

Instances

Eq BvSize
Data BvSize
Ord BvSize
Show BvSize
Generic BvSize
Typeable * BvSize
type Rep BvSize

Operators

data BvOp Source

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 Source

Construct the bitvector Sort from its BvSize

BitVector Expression Constructor

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

Apply some bitvector operator to a list of arguments

BitVector Type Constructor

bvTyCon :: FTycon Source