arith.go - Z3 Go API

MkAdd

func (c *Context) MkAdd(exprs ...*Expr) *Expr

MkAdd creates an addition.

MkDiv

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

MkDiv creates a division.

MkGe

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

MkGe creates a greater-than-or-equal constraint.

MkGt

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

MkGt creates a greater-than constraint.

MkInt

func (c *Context) MkInt(value int, sort *Sort) *Expr

MkInt creates an integer constant from an int.

MkInt64

func (c *Context) MkInt64(value int64, sort *Sort) *Expr

MkInt64 creates an integer constant from an int64.

MkIntConst

func (c *Context) MkIntConst(name string) *Expr

MkIntConst creates an integer constant (variable) with the given name.

MkIntSort

func (c *Context) MkIntSort() *Sort

Arithmetic operations and sorts MkIntSort creates the integer sort.

MkLe

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

MkLe creates a less-than-or-equal constraint.

MkLt

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

MkLt creates a less-than constraint.

MkMod

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

MkMod creates a modulo operation.

MkMul

func (c *Context) MkMul(exprs ...*Expr) *Expr

MkMul creates a multiplication.

MkReal

func (c *Context) MkReal(num, den int) *Expr

MkReal creates a real constant from numerator and denominator.

MkRealConst

func (c *Context) MkRealConst(name string) *Expr

MkRealConst creates a real constant (variable) with the given name.

MkRealSort

func (c *Context) MkRealSort() *Sort

MkRealSort creates the real number sort.

MkRem

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

MkRem creates a remainder operation.

MkSub

func (c *Context) MkSub(exprs ...*Expr) *Expr

MkSub creates a subtraction.

Functions