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

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Bitvector

Contents

Sizes
Operators
BitVector Sort Constructor
BitVector Expression Constructor

Synopsis

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