Z3
Loading...
Searching...
No Matches
FPSortRef Class Reference
Inheritance diagram for FPSortRef:

Public Member Functions

 ebits (self)
 sbits (self)
 cast (self, val)
Public Member Functions inherited from SortRef
 as_ast (self)
 get_id (self)
 kind (self)
 subsort (self, other)
 name (self)
 __eq__ (self, other)
 __ne__ (self, other)
 __hash__ (self)
Public Member Functions inherited from AstRef
 __init__ (self, ast, ctx=None)
 __del__ (self)
 __deepcopy__ (self, memo={})
 __str__ (self)
 __repr__ (self)
 __eq__ (self, other)
 __hash__ (self)
 __nonzero__ (self)
 __bool__ (self)
 sexpr (self)
 ctx_ref (self)
 eq (self, other)
 translate (self, target)
 __copy__ (self)
 hash (self)
 py_value (self)
Public Member Functions inherited from Z3PPObject
 use_pp (self)

Additional Inherited Members

Data Fields inherited from AstRef
 ast = ast
 ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)

Detailed Description

Floating-point sort.

Definition at line 9604 of file z3py.py.

Member Function Documentation

◆ cast()

cast ( self,
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 #x7f #b00000000000000000000000)'

Reimplemented from SortRef.

Definition at line 9623 of file z3py.py.

9623 def cast(self, val):
9624 """Try to cast `val` as a floating-point expression.
9625 >>> b = FPSort(8, 24)
9626 >>> b.cast(1.0)
9627 1
9628 >>> b.cast(1.0).sexpr()
9629 '(fp #b0 #x7f #b00000000000000000000000)'
9630 """
9631 if is_expr(val):
9632 if z3_debug():
9633 _z3_assert(self.ctx == val.ctx, "Context mismatch")
9634 return val
9635 else:
9636 return FPVal(val, None, self, self.ctx)
9637
9638

◆ ebits()

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

Definition at line 9607 of file z3py.py.

9607 def ebits(self):
9608 """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
9609 >>> b = FPSort(8, 24)
9610 >>> b.ebits()
9611 8
9612 """
9613 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
9614
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

◆ sbits()

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

Definition at line 9615 of file z3py.py.

9615 def sbits(self):
9616 """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
9617 >>> b = FPSort(8, 24)
9618 >>> b.sbits()
9619 24
9620 """
9621 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
9622
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.