diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 0fbe2a5c3d..97aa34a1a5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3057,7 +3057,7 @@ def as_binary_string(self): return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast()) def py_value(self): - return Z3_get_numeral_double(self.ctx_ref(), self.as_ast()) + return self.as_long() class RatNumRef(ArithRef): @@ -4012,6 +4012,11 @@ def as_string(self): def as_binary_string(self): return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast()) + def py_value(self): + """Return the Python value of a Z3 bit-vector numeral.""" + return self.as_long() + + def is_bv(a): """Return `True` if `a` is a Z3 bit-vector expression. @@ -10085,6 +10090,16 @@ def as_string(self): s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) return ("FPVal(%s, %s)" % (s, self.sort())) + 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] + def is_fp(a): """Return `True` if `a` is a Z3 floating-point expression.