bitvec.go

Bit-vector operations and constraints

← Back to Index Complete API Reference (markdown) README All Languages

Functions

MkBV

func (c *Context) MkBV(value int, size uint) *Expr

MkBV creates a bit-vector numeral from an integer.

MkBVAShr

func (c *Context) MkBVAShr(lhs, rhs *Expr) *Expr

MkBVAShr creates a bit-vector arithmetic shift right.

MkBVAdd

func (c *Context) MkBVAdd(lhs, rhs *Expr) *Expr

MkBVAdd creates a bit-vector addition.

MkBVAddNoOverflow

func (c *Context) MkBVAddNoOverflow(t1, t2 *Expr, isSigned bool) *Expr

MkBVAddNoOverflow creates a predicate that checks that the bit-wise addition of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.

MkBVAddNoUnderflow

func (c *Context) MkBVAddNoUnderflow(t1, t2 *Expr) *Expr

MkBVAddNoUnderflow creates a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

MkBVAnd

func (c *Context) MkBVAnd(lhs, rhs *Expr) *Expr

MkBVAnd creates a bit-vector bitwise AND.

MkBVConst

func (c *Context) MkBVConst(name string, size uint) *Expr

Bit-vector operations MkBVConst creates a bit-vector constant with the given name and size.

MkBVExtRotateLeft

func (c *Context) MkBVExtRotateLeft(t1, t2 *Expr) *Expr

MkBVExtRotateLeft rotates the bits of t1 to the left by the number of bits given by t2. Both t1 and t2 must be bit-vectors of the same width.

MkBVExtRotateRight

func (c *Context) MkBVExtRotateRight(t1, t2 *Expr) *Expr

MkBVExtRotateRight rotates the bits of t1 to the right by the number of bits given by t2. Both t1 and t2 must be bit-vectors of the same width.

MkBVFromInt64

func (c *Context) MkBVFromInt64(value int64, size uint) *Expr

MkBVFromInt64 creates a bit-vector from an int64.

MkBVLShr

func (c *Context) MkBVLShr(lhs, rhs *Expr) *Expr

MkBVLShr creates a bit-vector logical shift right.

MkBVMul

func (c *Context) MkBVMul(lhs, rhs *Expr) *Expr

MkBVMul creates a bit-vector multiplication.

MkBVMulNoOverflow

func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr

MkBVMulNoOverflow creates a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.

MkBVMulNoUnderflow

func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr

MkBVMulNoUnderflow creates a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

MkBVNeg

func (c *Context) MkBVNeg(expr *Expr) *Expr

MkBVNeg creates a bit-vector negation.

MkBVNegNoOverflow

func (c *Context) MkBVNegNoOverflow(t1 *Expr) *Expr

MkBVNegNoOverflow creates a predicate that checks that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

MkBVNot

func (c *Context) MkBVNot(expr *Expr) *Expr

MkBVNot creates a bit-vector bitwise NOT.

MkBVOr

func (c *Context) MkBVOr(lhs, rhs *Expr) *Expr

MkBVOr creates a bit-vector bitwise OR.

MkBVRedAnd

func (c *Context) MkBVRedAnd(t *Expr) *Expr

MkBVRedAnd computes the bitwise AND reduction of a bit-vector, returning a 1-bit vector.

MkBVRedOr

func (c *Context) MkBVRedOr(t *Expr) *Expr

MkBVRedOr computes the bitwise OR reduction of a bit-vector, returning a 1-bit vector.

MkBVRotateLeft

func (c *Context) MkBVRotateLeft(i uint, t *Expr) *Expr

MkBVRotateLeft rotates the bits of t to the left by i positions.

MkBVRotateRight

func (c *Context) MkBVRotateRight(i uint, t *Expr) *Expr

MkBVRotateRight rotates the bits of t to the right by i positions.

MkBVSDiv

func (c *Context) MkBVSDiv(lhs, rhs *Expr) *Expr

MkBVSDiv creates a signed bit-vector division.

MkBVSGE

func (c *Context) MkBVSGE(lhs, rhs *Expr) *Expr

MkBVSGE creates a signed bit-vector greater-than-or-equal.

MkBVSGT

func (c *Context) MkBVSGT(lhs, rhs *Expr) *Expr

MkBVSGT creates a signed bit-vector greater-than.

MkBVSLE

func (c *Context) MkBVSLE(lhs, rhs *Expr) *Expr

MkBVSLE creates a signed bit-vector less-than-or-equal.

MkBVSLT

func (c *Context) MkBVSLT(lhs, rhs *Expr) *Expr

MkBVSLT creates a signed bit-vector less-than.

MkBVSRem

func (c *Context) MkBVSRem(lhs, rhs *Expr) *Expr

MkBVSRem creates a signed bit-vector remainder.

MkBVSdivNoOverflow

func (c *Context) MkBVSdivNoOverflow(t1, t2 *Expr) *Expr

MkBVSdivNoOverflow creates a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

MkBVShl

func (c *Context) MkBVShl(lhs, rhs *Expr) *Expr

MkBVShl creates a bit-vector shift left.

MkBVSub

func (c *Context) MkBVSub(lhs, rhs *Expr) *Expr

MkBVSub creates a bit-vector subtraction.

MkBVSubNoOverflow

func (c *Context) MkBVSubNoOverflow(t1, t2 *Expr) *Expr

MkBVSubNoOverflow creates a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

MkBVSubNoUnderflow

func (c *Context) MkBVSubNoUnderflow(t1, t2 *Expr, isSigned bool) *Expr

MkBVSubNoUnderflow creates a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow. If isSigned is true, checks for signed underflow.

MkBVUDiv

func (c *Context) MkBVUDiv(lhs, rhs *Expr) *Expr

MkBVUDiv creates an unsigned bit-vector division.

MkBVUGE

func (c *Context) MkBVUGE(lhs, rhs *Expr) *Expr

MkBVUGE creates an unsigned bit-vector greater-than-or-equal.

MkBVUGT

func (c *Context) MkBVUGT(lhs, rhs *Expr) *Expr

MkBVUGT creates an unsigned bit-vector greater-than.

MkBVULE

func (c *Context) MkBVULE(lhs, rhs *Expr) *Expr

MkBVULE creates an unsigned bit-vector less-than-or-equal.

MkBVULT

func (c *Context) MkBVULT(lhs, rhs *Expr) *Expr

MkBVULT creates an unsigned bit-vector less-than.

MkBVURem

func (c *Context) MkBVURem(lhs, rhs *Expr) *Expr

MkBVURem creates an unsigned bit-vector remainder.

MkBVXor

func (c *Context) MkBVXor(lhs, rhs *Expr) *Expr

MkBVXor creates a bit-vector bitwise XOR.

MkConcat

func (c *Context) MkConcat(lhs, rhs *Expr) *Expr

MkConcat creates a bit-vector concatenation.

MkExtract

func (c *Context) MkExtract(high, low uint, expr *Expr) *Expr

MkExtract creates a bit-vector extraction.

MkRepeat

func (c *Context) MkRepeat(i uint, t *Expr) *Expr

MkRepeat repeats the given bit-vector t a total of i times.

MkSignExt

func (c *Context) MkSignExt(i uint, expr *Expr) *Expr

MkSignExt creates a bit-vector sign extension.

MkZeroExt

func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr

MkZeroExt creates a bit-vector zero extension.

← Back to Index