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.

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.

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.

MkBVNeg

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

MkBVNeg creates a bit-vector negation.

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.

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.

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.

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.

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