mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add shortcuts to convert to python objects in cases of numerals and strings

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-05 12:17:38 -08:00
parent cd41b21fa2
commit 71a4801c1d
1 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/api/python/z3/z3.py
View file

@ -3057,7 +3057,7 @@ class IntNumRef(ArithRef):
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 @@ class BitVecNumRef(BitVecRef):
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 @@ class FPNumRef(FPRef):
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.