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

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Bitvector

Contents

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

Synopsis

Constructor

Constructors

Bv BvSize String

Instances

Expression Bv Source

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

Sizes

data BvSize Source

Constructors

S32
S64

Instances

Eq BvSize Source
Data BvSize Source
Ord BvSize Source
Show BvSize Source
Generic BvSize Source
type Rep BvSize Source

Operators

data BvOp Source

Constructors

BvAnd
BvOr

Instances

Eq BvOp Source
Data BvOp Source
Ord BvOp Source
Show BvOp Source
Generic BvOp Source
type Rep BvOp Source

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