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.FPRef.__add__()

• - : cvc5.pythonic.FPRef.__sub__()

• * : cvc5.pythonic.FPRef.__mul__()

• unary - : cvc5.pythonic.FPRef.__neg__()

• / : cvc5.pythonic.FPRef.__div__()

• % : cvc5.pythonic.FPRef.__mod__()

• <= : cvc5.pythonic.FPRef.__le__()

• < : cvc5.pythonic.FPRef.__lt__()

• >= : cvc5.pythonic.FPRef.__ge__()

• > : cvc5.pythonic.FPRef.__gt__()

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.