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 9595 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 9614 of file z3py.py.

9614 def cast(self, val):
9615 """Try to cast `val` as a floating-point expression.
9616 >>> b = FPSort(8, 24)
9617 >>> b.cast(1.0)
9618 1
9619 >>> b.cast(1.0).sexpr()
9620 '(fp #b0 #x7f #b00000000000000000000000)'
9621 """
9622 if is_expr(val):
9623 if z3_debug():
9624 _z3_assert(self.ctx == val.ctx, "Context mismatch")
9625 return val
9626 else:
9627 return FPVal(val, None, self, self.ctx)
9628
9629

◆ 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 9598 of file z3py.py.

9598 def ebits(self):
9599 """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
9600 >>> b = FPSort(8, 24)
9601 >>> b.ebits()
9602 8
9603 """
9604 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
9605
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 9606 of file z3py.py.

9606 def sbits(self):
9607 """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
9608 >>> b = FPSort(8, 24)
9609 >>> b.sbits()
9610 24
9611 """
9612 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
9613
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.