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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Bitvector

Contents

Synopsis

Constructor

data Bv Source

Constructors

Bv BvSize String 

Instances

Expression Bv

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

Sizes

data BvSize Source

Constructors

S32 
S64 

Instances

Operators

data BvOp Source

Constructors

BvAnd 
BvOr 

Instances

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