Inheritance diagram for FPNumRef:

Public Member Functions
	sign (self)

	sign_as_bv (self)

	significand (self)

	significand_as_long (self)

	significand_as_bv (self)

	exponent (self, biased=True)

	exponent_as_long (self, biased=True)

	exponent_as_bv (self, biased=True)

	isNaN (self)

	isInf (self)

	isZero (self)

	isNormal (self)

	isSubnormal (self)

	isPositive (self)

	isNegative (self)

	as_string (self)

	py_value (self)

Public Member Functions inherited from FPRef
	sort (self)

	ebits (self)

	sbits (self)

	__le__ (self, other)

	__lt__ (self, other)

	__ge__ (self, other)

	__gt__ (self, other)

	__add__ (self, other)

	__radd__ (self, other)

	__sub__ (self, other)

	__rsub__ (self, other)

	__mul__ (self, other)

	__rmul__ (self, other)

	__pos__ (self)

	__neg__ (self)

	__div__ (self, other)

	__rdiv__ (self, other)

	__truediv__ (self, other)

	__rtruediv__ (self, other)

	__mod__ (self, other)

	__rmod__ (self, other)

Public Member Functions inherited from ExprRef
	as_ast (self)

	get_id (self)

	sort_kind (self)

	__eq__ (self, other)

	__hash__ (self)

	__ne__ (self, other)

	params (self)

	decl (self)

	kind (self)

	num_args (self)

	arg (self, idx)

	children (self)

	from_string (self, s)

	serialize (self)

Public Member Functions inherited from AstRef
	__init__ (self, ast, ctx=None)

	__del__ (self)

	__deepcopy__ (self, memo={})

	__str__ (self)

	__repr__ (self)

	__nonzero__ (self)

	__bool__ (self)

	sexpr (self)

	ctx_ref (self)

	eq (self, other)

	translate (self, target)

	__copy__ (self)

	hash (self)

Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx

Data Fields inherited from FPRef
	ctx

Data Fields inherited from ExprRef
	ctx

	ast

Data Fields inherited from AstRef
	ast

	ctx

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

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

Definition at line 10030 of file z3py.py.

Member Function Documentation

◆ as_string()

as_string ( self )

Return a Z3 floating point expression as a Python string.

Reimplemented from FPRef.

Definition at line 10161 of file z3py.py.

    def as_string(self):
        s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
        return ("FPVal(%s, %s)" % (s, self.sort()))
 

Referenced by BitVecNumRef.as_long(), and IntNumRef.as_long().

◆ exponent()

exponent	(		self,
			biased = True )

Definition at line 10094 of file z3py.py.

    def exponent(self, biased=True):
        return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
 

◆ exponent_as_bv()

exponent_as_bv	(		self,
			biased = True )

Definition at line 10115 of file z3py.py.

    def exponent_as_bv(self, biased=True):
        return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
 

◆ exponent_as_long()

exponent_as_long	(		self,
			biased = True )

Definition at line 10104 of file z3py.py.

    def exponent_as_long(self, biased=True):
        ptr = (ctypes.c_longlong * 1)()
        if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
            raise Z3Exception("error retrieving the exponent of a numeral.")
        return ptr[0]
 

◆ isInf()

isInf ( self )

Definition at line 10125 of file z3py.py.

    def isInf(self):
        return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
 

◆ isNaN()

isNaN ( self )

Definition at line 10120 of file z3py.py.

    def isNaN(self):
        return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
 

◆ isNegative()

isNegative ( self )

Definition at line 10150 of file z3py.py.

    def isNegative(self):
        return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
 

◆ isNormal()

isNormal ( self )

Definition at line 10135 of file z3py.py.

    def isNormal(self):
        return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
 

◆ isPositive()

isPositive ( self )

Definition at line 10145 of file z3py.py.

    def isPositive(self):
        return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
 

◆ isSubnormal()

isSubnormal ( self )

Definition at line 10140 of file z3py.py.

    def isSubnormal(self):
        return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
 

◆ isZero()

isZero ( self )

Definition at line 10130 of file z3py.py.

    def isZero(self):
        return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
 

◆ py_value()

py_value ( self )

Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 10165 of file z3py.py.

    def py_value(self):
        bv = simplify(fpToIEEEBV(self))
        binary = bv.py_value()
        if not isinstance(binary, int):
            return None
        # Decode the IEEE 754 binary representation
        import struct
        bytes_rep = binary.to_bytes(8, byteorder='big')
        return struct.unpack('>d', bytes_rep)[0]
 
 

◆ sign()

sign ( self )

Definition at line 10041 of file z3py.py.

    def sign(self):
        num = (ctypes.c_int)()
        nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
        if nsign is False:
            raise Z3Exception("error retrieving the sign of a numeral.")
        return num.value != 0
 

◆ sign_as_bv()

sign_as_bv ( self )

Definition at line 10053 of file z3py.py.

    def sign_as_bv(self):
        return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
 

◆ significand()

significand ( self )

Definition at line 10063 of file z3py.py.

    def significand(self):
        return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
 

◆ significand_as_bv()

significand_as_bv ( self )

Definition at line 10084 of file z3py.py.

    def significand_as_bv(self):
        return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
 

◆ significand_as_long()

significand_as_long ( self )

Definition at line 10073 of file z3py.py.

    def significand_as_long(self):
        ptr = (ctypes.c_ulonglong * 1)()
        if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
            raise Z3Exception("error retrieving the significand of a numeral.")
        return ptr[0]
 

Field Documentation

◆ ctx

ctx

Definition at line 10054 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

Public Member Functions

Data Fields

Additional Inherited Members