fp.go

IEEE 754 floating-point operations

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

Functions

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.

MkFPFMA

func (c *Context) MkFPFMA(rm, t1, t2, t3 *Expr) *Expr

MkFPFMA creates a floating-point fused multiply-add: round((t1 * t2) + t3, rm).

MkFPFP

func (c *Context) MkFPFP(sgn, exp, sig *Expr) *Expr

MkFPFP creates a floating-point number from a sign bit (1-bit BV), exponent BV, and significand BV.

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.

MkFPIsNegative

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

MkFPIsNegative creates a predicate checking if a floating-point number is negative.

MkFPIsNormal

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

MkFPIsNormal creates a predicate checking if a floating-point number is normal.

MkFPIsPositive

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

MkFPIsPositive creates a predicate checking if a floating-point number is positive.

MkFPIsSubnormal

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

MkFPIsSubnormal creates a predicate checking if a floating-point number is subnormal.

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.

MkFPMax

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

MkFPMax creates the maximum of two floating-point values.

MkFPMin

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

MkFPMin creates the minimum of two floating-point values.

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.

MkFPNumeralDouble

func (c *Context) MkFPNumeralDouble(v float64, sort *Sort) *Expr

MkFPNumeralDouble creates a floating-point numeral from a float64 value.

MkFPNumeralFloat

func (c *Context) MkFPNumeralFloat(v float32, sort *Sort) *Expr

MkFPNumeralFloat creates a floating-point numeral from a float32 value.

MkFPNumeralInt

func (c *Context) MkFPNumeralInt(v int, sort *Sort) *Expr

MkFPNumeralInt creates a floating-point numeral from a signed integer.

MkFPNumeralInt64Uint64

func (c *Context) MkFPNumeralInt64Uint64(sgn bool, exp int64, sig uint64, sort *Sort) *Expr

MkFPNumeralInt64Uint64 creates a floating-point numeral from a sign, int64 exponent, and uint64 significand.

MkFPNumeralIntUint

func (c *Context) MkFPNumeralIntUint(sgn bool, exp int, sig uint, sort *Sort) *Expr

MkFPNumeralIntUint creates a floating-point numeral from a sign, signed exponent, and unsigned significand.

MkFPRNA

func (c *Context) MkFPRNA() *Expr

MkFPRNA creates the round-nearest-ties-to-away rounding mode.

MkFPRNE

func (c *Context) MkFPRNE() *Expr

MkFPRNE creates the round-nearest-ties-to-even rounding mode.

MkFPRTN

func (c *Context) MkFPRTN() *Expr

MkFPRTN creates the round-toward-negative rounding mode.

MkFPRTP

func (c *Context) MkFPRTP() *Expr

MkFPRTP creates the round-toward-positive rounding mode.

MkFPRTZ

func (c *Context) MkFPRTZ() *Expr

MkFPRTZ creates the round-toward-zero rounding mode.

MkFPRem

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

MkFPRem creates a floating-point remainder.

MkFPRoundToIntegral

func (c *Context) MkFPRoundToIntegral(rm, t *Expr) *Expr

MkFPRoundToIntegral creates a floating-point round-to-integral operation.

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.

MkFPToFPBV

func (c *Context) MkFPToFPBV(bv *Expr, sort *Sort) *Expr

MkFPToFPBV converts a bit-vector to a floating-point number (reinterpretation of IEEE 754 bits).

MkFPToFPFloat

func (c *Context) MkFPToFPFloat(rm, t *Expr, sort *Sort) *Expr

MkFPToFPFloat converts a floating-point number to another floating-point sort with rounding.

MkFPToFPReal

func (c *Context) MkFPToFPReal(rm, t *Expr, sort *Sort) *Expr

MkFPToFPReal converts a real number to a floating-point number with rounding.

MkFPToFPSigned

func (c *Context) MkFPToFPSigned(rm, t *Expr, sort *Sort) *Expr

MkFPToFPSigned converts a signed bit-vector to a floating-point number with rounding.

MkFPToFPUnsigned

func (c *Context) MkFPToFPUnsigned(rm, t *Expr, sort *Sort) *Expr

MkFPToFPUnsigned converts an unsigned bit-vector to a floating-point number with rounding.

MkFPToIEEEBV

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

MkFPToIEEEBV converts a floating-point number to its IEEE 754 bit-vector representation.

MkFPToReal

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

MkFPToReal converts a floating-point number to a real number.

MkFPToSBV

func (c *Context) MkFPToSBV(rm, t *Expr, sz uint) *Expr

MkFPToSBV converts a floating-point number to a signed bit-vector with rounding.

MkFPToUBV

func (c *Context) MkFPToUBV(rm, t *Expr, sz uint) *Expr

MkFPToUBV converts a floating-point number to an unsigned bit-vector with rounding.

MkFPZero

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

MkFPZero creates a floating-point zero.

← Back to Index