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 9599 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 9618 of file z3py.py.

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

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

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

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