Floating Point

Basic FP Term Builders

cvc5.pythonic.FP(name, fpsort, ctx=None)

Return a floating-point constant named name. fpsort is the floating-point sort. If ctx=None, then the global context is used.

>>> x  = FP('x', FPSort(8, 24))
>>> is_fp(x)
True
>>> x.ebits()
8
>>> x.sort()
FPSort(8, 24)
>>> word = FPSort(8, 24)
>>> x2 = FP('x', word)
>>> eq(x, x2)
True
cvc5.pythonic.FPs(names, fpsort, ctx=None)

Return an array of floating-point constants.

>>> x, y, z = FPs('x y z', FPSort(8, 24))
>>> x.sort()
FPSort(8, 24)
>>> x.sbits()
24
>>> x.ebits()
8
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
fpMul(RNE(), fpAdd(RNE(), x, y), z)
cvc5.pythonic.FPVal(val, exp=None, fps=None, ctx=None)

Return a floating-point value of value val and sort fps. If ctx=None, then the global context is used.

>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
1.25*(2**4)
>>> print("0x%.8x" % v.exponent_as_long())
0x00000004
>>> v = FPVal(2.25, FPSort(8, 24))
>>> v
1.125*(2**1)
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-1.125*(2**1)
>>> FPVal(-0.0, FPSort(8, 24))
-0.0
>>> FPVal(0.0, FPSort(8, 24))
+0.0
>>> FPVal(+0.0, FPSort(8, 24))
+0.0
cvc5.pythonic.fpNaN(s)

Create a SMT floating-point NaN term.

>>> s = FPSort(8, 24)
>>> set_fpa_pretty(True)
>>> fpNaN(s)
NaN
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(False)
>>> fpNaN(s)
fpNaN(FPSort(8, 24))
>>> set_fpa_pretty(pb)
cvc5.pythonic.fpPlusInfinity(s)

Create a SMT floating-point +oo term.

>>> s = FPSort(8, 24)
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(True)
>>> fpPlusInfinity(s)
+oo
>>> set_fpa_pretty(False)
>>> fpPlusInfinity(s)
fpPlusInfinity(FPSort(8, 24))
>>> set_fpa_pretty(pb)
cvc5.pythonic.fpMinusInfinity(s)

Create a SMT floating-point -oo term.

cvc5.pythonic.fpInfinity(s, negative)

Create a SMT floating-point +oo or -oo term.

cvc5.pythonic.fpPlusZero(s)

Create a SMT floating-point +0.0 term.

cvc5.pythonic.fpMinusZero(s)

Create a SMT floating-point -0.0 term.

cvc5.pythonic.fpZero(s, negative)

Create a SMT floating-point +0.0 or -0.0 term.

cvc5.pythonic.FPSort(ebits, sbits, ctx=None)

Return a SMT floating-point sort of the given sizes. If ctx=None, then the global context is used.

>>> Single = FPSort(8, 24)
>>> Double = FPSort(11, 53)
>>> Single
FPSort(8, 24)
>>> x = Const('x', Single)
>>> eq(x, FP('x', FPSort(8, 24)))
True
cvc5.pythonic.Float16(ctx=None)

Floating-point 16-bit (half) sort.

cvc5.pythonic.FloatHalf(ctx=None)

Floating-point 16-bit (half) sort.

cvc5.pythonic.Float32(ctx=None)

Floating-point 32-bit (single) sort.

cvc5.pythonic.FloatSingle(ctx=None)

Floating-point 32-bit (single) sort.

cvc5.pythonic.Float64(ctx=None)

Floating-point 64-bit (double) sort.

cvc5.pythonic.FloatDouble(ctx=None)

Floating-point 64-bit (double) sort.

cvc5.pythonic.Float128(ctx=None)

Floating-point 128-bit (quadruple) sort.

cvc5.pythonic.FloatQuadruple(ctx=None)

Floating-point 128-bit (quadruple) sort.

FP Operators

See the following operator overloads for building basic floating-point terms:

cvc5.pythonic.fpAbs(a, ctx=None)

Create a SMT floating-point absolute value expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FPVal(1.0, s)
>>> fpAbs(x)
fpAbs(1)
>>> y = FPVal(-20.0, s)
>>> y
-1.25*(2**4)
>>> fpAbs(y)
fpAbs(-1.25*(2**4))
>>> fpAbs(-1.25*(2**4))
fpAbs(-1.25*(2**4))
>>> fpAbs(x).sort()
FPSort(8, 24)
cvc5.pythonic.fpNeg(a, ctx=None)

Create a SMT floating-point addition expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> fpNeg(x)
-x
>>> fpNeg(x).sort()
FPSort(8, 24)
cvc5.pythonic.fpAdd(rm, a, b, ctx=None)

Create a SMT floating-point addition expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpAdd(rm, x, y)
fpAdd(RNE(), x, y)
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
x + y
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpSub(rm, a, b, ctx=None)

Create a SMT floating-point subtraction expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpSub(rm, x, y)
fpSub(RNE(), x, y)
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpMul(rm, a, b, ctx=None)

Create a SMT floating-point multiplication expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMul(rm, x, y)
fpMul(RNE(), x, y)
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpDiv(rm, a, b, ctx=None)

Create a SMT floating-point division expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpDiv(rm, x, y)
fpDiv(RNE(), x, y)
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpRem(a, b, ctx=None)

Create a SMT floating-point remainder expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpRem(x, y)
fpRem(x, y)
>>> fpRem(x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpMin(a, b, ctx=None)

Create a SMT floating-point minimum expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMin(x, y)
fpMin(x, y)
>>> fpMin(x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpMax(a, b, ctx=None)

Create a SMT floating-point maximum expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMax(x, y)
fpMax(x, y)
>>> fpMax(x, y).sort()
FPSort(8, 24)
cvc5.pythonic.fpFMA(rm, a, b, c, ctx=None)

Create a SMT floating-point fused multiply-add expression.

cvc5.pythonic.fpSqrt(rm, a, ctx=None)

Create a SMT floating-point square root expression.

cvc5.pythonic.fpRoundToIntegral(rm, a, ctx=None)

Create a SMT floating-point roundToIntegral expression.

cvc5.pythonic.fpIsNaN(a, ctx=None)

Create a SMT floating-point isNaN expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpIsNaN(x)
fpIsNaN(x)
cvc5.pythonic.fpIsInf(a, ctx=None)

Create a SMT floating-point isInfinite expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> fpIsInf(x)
fpIsInf(x)
cvc5.pythonic.fpIsZero(a, ctx=None)

Create a SMT floating-point isZero expression.

cvc5.pythonic.fpIsNormal(a, ctx=None)

Create a SMT floating-point isNormal expression.

cvc5.pythonic.fpIsSubnormal(a, ctx=None)

Create a SMT floating-point isSubnormal expression.

cvc5.pythonic.fpIsNegative(a, ctx=None)

Create a SMT floating-point isNegative expression.

cvc5.pythonic.fpIsPositive(a, ctx=None)

Create a SMT floating-point isPositive expression.

cvc5.pythonic.fpLT(a, b, ctx=None)

Create the SMT floating-point expression other < self.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLT(x, y)
x < y
>>> (x < y).sexpr()
'(fp.lt x y)'
cvc5.pythonic.fpLEQ(a, b, ctx=None)

Create the SMT floating-point expression other <= self.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLEQ(x, y)
x <= y
>>> (x <= y).sexpr()
'(fp.leq x y)'
cvc5.pythonic.fpGT(a, b, ctx=None)

Create the SMT floating-point expression other > self.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGT(x, y)
x > y
>>> (x > y).sexpr()
'(fp.gt x y)'
cvc5.pythonic.fpGEQ(a, b, ctx=None)

Create the SMT floating-point expression other >= self.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGEQ(x, y)
x >= y
>>> (x >= y).sexpr()
'(fp.geq x y)'
cvc5.pythonic.fpEQ(a, b, ctx=None)

Create the SMT floating-point expression fpEQ(other, self).

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpEQ(x, y)
fpEQ(x, y)
>>> fpEQ(x, y).sexpr()
'(fp.eq x y)'
cvc5.pythonic.fpNEQ(a, b, ctx=None)

Create the SMT floating-point expression Not(fpEQ(other, self)).

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpNEQ(x, y)
Not(fpEQ(x, y))
>>> (x != y).sexpr()
'(distinct x y)'
cvc5.pythonic.fpFP(sgn, exp, sig, ctx=None)

Create the SMT floating-point value fpFP(sgn, sig, exp) from the three bit-vectors sgn, sig, and exp.

>>> s = FPSort(8, 24)
>>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
>>> print(x)
fpToFP(Concat(1, 127, 4194304))
>>> xv = FPVal(-1.5, s)
>>> print(xv)
-1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
sat
>>> xv = FPVal(+1.5, s)
>>> print(xv)
1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
unsat
cvc5.pythonic.fpToFP(a1, a2=None, a3=None, ctx=None)

Create a SMT floating-point conversion expression from other term sorts to floating-point.

From a floating-point term with different precision:

>>> x = FPVal(1.0, Float32())
>>> x_db = fpToFP(RNE(), x, Float64())
>>> x_db.sort()
FPSort(11, 53)

From a real term:

>>> x_r = RealVal(1.5)
>>> simplify(fpToFP(RNE(), x_r, Float32()))
1.5

From a signed bit-vector term:

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> simplify(fpToFP(RNE(), x_signed, Float32()))
-1.25*(2**2)
cvc5.pythonic.fpBVToFP(v, sort, ctx=None)

Create a SMT floating-point conversion expression that represents the conversion from a bit-vector term to a floating-point term.

>>> x_bv = BitVecVal(0x3F800000, 32)
>>> x_fp = fpBVToFP(x_bv, Float32())
>>> x_fp
fpToFP(1065353216)
>>> simplify(x_fp)
1
cvc5.pythonic.fpFPToFP(rm, v, sort, ctx=None)

Create a SMT floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision.

>>> x_sgl = FPVal(1.0, Float32())
>>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
>>> x_dbl
fpToFP(RNE(), 1)
>>> simplify(x_dbl)
1
>>> x_dbl.sort()
FPSort(11, 53)
cvc5.pythonic.fpRealToFP(rm, v, sort, ctx=None)

Create a SMT floating-point conversion expression that represents the conversion from a real term to a floating-point term.

>>> x_r = RealVal(1.5)
>>> x_fp = fpRealToFP(RNE(), x_r, Float32())
>>> x_fp
fpToFP(RNE(), 3/2)
>>> simplify(x_fp)
1.5
cvc5.pythonic.fpSignedToFP(rm, v, sort, ctx=None)

Create a SMT floating-point conversion expression that represents the conversion from a signed bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFP(RNE(), 4294967291)
>>> simplify(x_fp)
-1.25*(2**2)
cvc5.pythonic.fpUnsignedToFP(rm, v, sort, ctx=None)

Create a SMT floating-point conversion expression that represents the conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFP(RNE(), 4294967291)
>>> simplify(x_fp)
1*(2**32)
cvc5.pythonic.fpToFPUnsigned(rm, x, s, ctx=None)

Create a SMT floating-point conversion expression, from unsigned bit-vector to floating-point expression.

cvc5.pythonic.fpToSBV(rm, x, s, ctx=None)

Create a SMT floating-point conversion expression, from floating-point expression to signed bit-vector.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToSBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False
cvc5.pythonic.fpToUBV(rm, x, s, ctx=None)

Create a SMT floating-point conversion expression, from floating-point expression to unsigned bit-vector.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToUBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False
cvc5.pythonic.fpToReal(x, ctx=None)

Create a SMT floating-point conversion expression, from floating-point expression to real.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToReal(x)
>>> print(is_fp(x))
True
>>> print(is_real(y))
True
>>> print(is_fp(y))
False
>>> print(is_real(x))
False

Testers

cvc5.pythonic.is_fp_sort(s)

Return True if s is a SMT floating-point sort.

>>> is_fp_sort(FPSort(8, 24))
True
>>> is_fp_sort(IntSort())
False
cvc5.pythonic.is_fp(a)

Return True if a is a SMT floating-point expression.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp(b)
True
>>> is_fp(b + 1.0)
True
>>> is_fp(Int('x'))
False
cvc5.pythonic.is_fp_value(a)

Return True if a is a SMT floating-point numeral value.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp_value(b)
False
>>> b = FPVal(1.0, FPSort(8, 24))
>>> b
1
>>> is_fp_value(b)
True
cvc5.pythonic.is_fprm_sort(s)

Return True if s is a SMT floating-point rounding mode sort.

>>> is_fprm_sort(FPSort(8, 24))
False
>>> is_fprm_sort(RNE().sort())
True
cvc5.pythonic.is_fprm(a)

Return True if a is a SMT floating-point rounding mode expression.

>>> rm = RNE()
>>> is_fprm(rm)
True
>>> rm = 1.0
>>> is_fprm(rm)
False
cvc5.pythonic.is_fprm_value(a)

Return True if a is a SMT floating-point rounding mode numeral value.

FP Rounding Modes

cvc5.pythonic.RoundNearestTiesToEven(ctx=None)

Round to nearest, with ties broken towards even.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RoundNearestTiesToEven(), x, y)
fpMul(RNE(), x, y)
cvc5.pythonic.RNE(ctx=None)

Round to nearest, with ties broken towards even.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RNE(), x, y)
fpMul(RNE(), x, y)
cvc5.pythonic.RoundNearestTiesToAway(ctx=None)

Round to nearest, with ties broken away from zero.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RoundNearestTiesToAway(), x, y)
fpMul(RNA(), x, y)
cvc5.pythonic.RNA(ctx=None)

Round to nearest, with ties broken away from zero.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RNA(), x, y)
fpMul(RNA(), x, y)
cvc5.pythonic.RoundTowardPositive(ctx=None)

Round towards more positive values.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RoundTowardPositive(), x, y)
fpMul(RTP(), x, y)
cvc5.pythonic.RTP(ctx=None)

Round towards more positive values.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RTP(), x, y)
fpMul(RTP(), x, y)
cvc5.pythonic.RoundTowardNegative(ctx=None)

Round towards more negative values.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RoundTowardNegative(), x, y)
fpMul(RTN(), x, y)
cvc5.pythonic.RTN(ctx=None)

Round towards more negative values.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RTN(), x, y)
fpMul(RTN(), x, y)
cvc5.pythonic.RoundTowardZero(ctx=None)

Round towards zero.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RoundTowardZero(), x, y)
x * y
cvc5.pythonic.RTZ(ctx=None)

Round towards zero.

See Section 4.2 of the IEEE standard <https://doi.org/10.1109/IEEESTD.2019.8766229> or wikipedia <https://en.wikipedia.org/wiki/Floating-point_arithmetic#Rounding_modes> for details on rounding modes.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpMul(RTZ(), x, y)
x * y
cvc5.pythonic.get_default_rounding_mode(ctx=None)

Retrieves the global default rounding mode.

cvc5.pythonic.set_default_rounding_mode(rm, ctx=None)

Set the default rounding mode

>>> x, y = FPs('x y', Float32())
>>> set_default_rounding_mode(RTN())
>>> sum1 = x + y
>>> set_default_rounding_mode(RTP())
>>> sum2 = x + y
>>> print((sum1 == sum2).sexpr())
(= (fp.add roundTowardNegative x y) (fp.add roundTowardPositive x y))
>>> s = SolverFor("QF_FP")
>>> s += sum1 != sum2
>>> s.check()
sat
>>> m = s.model()
>>> assert str(m[sum1]) != str(m[sum2])

Note the the FP term builders can take an explicit rounding mode.

cvc5.pythonic.get_default_fp_sort(ctx=None)
cvc5.pythonic.set_default_fp_sort(ebits, sbits, ctx=None)

Classes (with overloads)

class cvc5.pythonic.FPSortRef(ast, ctx=None)

Floating-point sort.

cast(val)

Try to cast val as a floating-point expression. >>> b = FPSort(8, 24) >>> b.cast(1.0) 1 >>> b.cast(1.0).sexpr() ‘(fp #b0 #b01111111 #b00000000000000000000000)’

ebits()

Retrieves the number of bits reserved for the exponent in the FloatingPoint sort self. >>> b = FPSort(8, 24) >>> b.ebits() 8

sbits()

Retrieves the number of bits reserved for the significand in the FloatingPoint sort self. >>> b = FPSort(8, 24) >>> b.sbits() 24

class cvc5.pythonic.FPRef(ast, ctx=None, reverse_children=False)

Floating-point expressions.

__add__(other)

Create the SMT expression self + other.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x + y
x + y
>>> (x + y).sort()
FPSort(8, 24)
__div__(other)

Create the SMT expression self / other.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x / y
x / y
>>> (x / y).sort()
FPSort(8, 24)
>>> 10 / y
1.25*(2**3) / y
__ge__(other)

Return self>=value.

__gt__(other)

Return self>value.

__le__(other)

Return self<=value.

__lt__(other)

Return self<value.

__mod__(other)

Create the SMT expression mod self % other.

__mul__(other)

Create the SMT expression self * other.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> (x * y).sort()
FPSort(8, 24)
>>> 10 * y
1.25*(2**3) * y
__neg__()

Create the SMT expression -self.

>>> x = FP('x', Float32())
>>> -x
-x
__pos__()

Create the SMT expression +self.

__radd__(other)

Create the SMT expression other + self.

>>> x = FP('x', FPSort(8, 24))
>>> 10 + x
1.25*(2**3) + x
__rdiv__(other)

Create the SMT expression other / self.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x / y
x / y
>>> x / 10
x / 1.25*(2**3)
__rmod__(other)

Create the SMT expression mod other % self.

__rmul__(other)

Create the SMT expression other * self.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> x * 10
x * 1.25*(2**3)
__rsub__(other)

Create the SMT expression other - self.

>>> x = FP('x', FPSort(8, 24))
>>> 10 - x
1.25*(2**3) - x
__rtruediv__(other)

Create the SMT expression division other / self.

__sub__(other)

Create the SMT expression self - other.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x - y
x - y
>>> (x - y).sort()
FPSort(8, 24)
__truediv__(other)

Create the SMT expression division self / other.

as_string()

Return a SMT floating point expression as a Python string.

ebits()

Retrieves the number of bits reserved for the exponent in the FloatingPoint expression self. >>> b = FPSort(8, 24) >>> b.ebits() 8

sbits()

Retrieves the number of bits reserved for the exponent in the FloatingPoint expression self. >>> b = FPSort(8, 24) >>> b.sbits() 24

sort()

Return the sort of the floating-point expression self.

>>> x = FP('1.0', FPSort(8, 24))
>>> x.sort()
FPSort(8, 24)
>>> x.sort() == FPSort(8, 24)
True
class cvc5.pythonic.FPNumRef(ast, ctx=None, reverse_children=False)
as_string()

The string representation of the numeral.

>>> x = FPVal(20, FPSort(8, 24))
>>> print(x.as_string())
1.25*(2**4)
exponent(biased=True)

The exponent of the numeral.

>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.exponent()
1
exponent_as_long()

The exponent of the numeral as a long.

>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.exponent_as_long()
1
isInf()

Indicates whether the numeral is +oo or -oo.

isNaN()

Indicates whether the numeral is a NaN.

isNegative()

Indicates whether the numeral is negative.

isNormal()

Indicates whether the numeral is normal.

isPositive()

Indicates whether the numeral is positive.

isSubnormal()

Indicates whether the numeral is subnormal.

isZero()

Indicates whether the numeral is +zero or -zero.

sign()

The sign of the numeral.

>>> x = FPVal(+1.0, FPSort(8, 24))
>>> x.sign()
False
>>> x = FPVal(-1.0, FPSort(8, 24))
>>> x.sign()
True
significand()

The significand of the numeral, as a double

>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.significand()
1.25
significand_as_long()

The significand of the numeral as a long.

This is missing the 1

>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.significand_as_long()
2097152
class cvc5.pythonic.FPRMRef(ast, ctx=None, reverse_children=False)

Floating-point rounding mode expressions

as_string()

Return a SMT floating point expression as a Python string.