fp.go - Z3 Go API

MkFPAbs

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

MkFPAbs creates a floating-point absolute value.

MkFPAdd

func (c *Context) MkFPAdd(rm, lhs, rhs *Expr) *Expr

MkFPAdd creates a floating-point addition.

MkFPDiv

func (c *Context) MkFPDiv(rm, lhs, rhs *Expr) *Expr

MkFPDiv creates a floating-point division.

MkFPEq

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

MkFPEq creates a floating-point equality.

MkFPGE

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

MkFPGE creates a floating-point greater-than-or-equal.

MkFPGT

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

MkFPGT creates a floating-point greater-than.

MkFPInf

func (c *Context) MkFPInf(sort *Sort, negative bool) *Expr

MkFPInf creates a floating-point infinity.

MkFPIsInf

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

MkFPIsInf creates a predicate checking if a floating-point number is infinite.

MkFPIsNaN

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

MkFPIsNaN creates a predicate checking if a floating-point number is NaN.

MkFPIsZero

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

MkFPIsZero creates a predicate checking if a floating-point number is zero.

MkFPLE

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

MkFPLE creates a floating-point less-than-or-equal.

MkFPLT

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

MkFPLT creates a floating-point less-than.

MkFPMul

func (c *Context) MkFPMul(rm, lhs, rhs *Expr) *Expr

MkFPMul creates a floating-point multiplication.

MkFPNaN

func (c *Context) MkFPNaN(sort *Sort) *Expr

MkFPNaN creates a floating-point NaN.

MkFPNeg

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

MkFPNeg creates a floating-point negation.

MkFPNumeral

func (c *Context) MkFPNumeral(value string, sort *Sort) *Expr

MkFPNumeral creates a floating-point numeral from a string.

MkFPRoundingModeSort

func (c *Context) MkFPRoundingModeSort() *Sort

MkFPRoundingModeSort creates the rounding mode sort.

MkFPSort

func (c *Context) MkFPSort(ebits, sbits uint) *Sort

Floating-point operations MkFPSort creates a floating-point sort.

MkFPSort128

func (c *Context) MkFPSort128() *Sort

MkFPSort128 creates a 128-bit floating-point sort (quadruple precision).

MkFPSort16

func (c *Context) MkFPSort16() *Sort

MkFPSort16 creates a 16-bit floating-point sort.

MkFPSort32

func (c *Context) MkFPSort32() *Sort

MkFPSort32 creates a 32-bit floating-point sort (single precision).

MkFPSort64

func (c *Context) MkFPSort64() *Sort

MkFPSort64 creates a 64-bit floating-point sort (double precision).

MkFPSqrt

func (c *Context) MkFPSqrt(rm, expr *Expr) *Expr

MkFPSqrt creates a floating-point square root.

MkFPSub

func (c *Context) MkFPSub(rm, lhs, rhs *Expr) *Expr

MkFPSub creates a floating-point subtraction.

MkFPZero

func (c *Context) MkFPZero(sort *Sort, negative bool) *Expr

MkFPZero creates a floating-point zero.

Functions