arith.go - Z3 Go API

MkAbs

func (c *Context) MkAbs(arg *Expr) *Expr

MkAbs creates an absolute value expression.

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.

MkDivides

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

MkDivides creates an integer divisibility predicate (t1 divides t2).

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.

MkInt2Real

func (c *Context) MkInt2Real(arg *Expr) *Expr

MkInt2Real coerces an integer expression to a real.

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.

MkIsInt

func (c *Context) MkIsInt(arg *Expr) *Expr

MkIsInt creates a predicate that checks whether a real expression is an integer.

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.

MkPower

func (c *Context) MkPower(base, exp *Expr) *Expr

MkPower creates an exponentiation expression (base^exp).

MkReal

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

MkReal creates a real constant from numerator and denominator.

MkReal2Int

func (c *Context) MkReal2Int(arg *Expr) *Expr

MkReal2Int converts a real expression to an integer (floor).

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