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

Bugfixes for FP numerals in Python

Browse source 
Relates to #464, #470
This commit is contained in:
Christoph M. Wintersteiger 2016-03-01 21:21:25 +00:00
parent 0cb8193cdd
commit 59e695f2be
1 changed files with 37 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -48,6 +48,7 @@ from z3printer import *
from fractions import Fraction from fractions import Fraction
import sys import sys
import io import io
import math
if sys.version < '3': if sys.version < '3':
def _is_int(v): def _is_int(v):
@ -8409,11 +8410,24 @@ def FPSort(ebits, sbits, ctx=None):
def _to_float_str(val, exp=0): def _to_float_str(val, exp=0):
if isinstance(val, float): if isinstance(val, float):
v = val.as_integer_ratio() if math.isnan(val):
num = v[0] res = "NaN"
den = v[1] elif val == 0.0:
rvs = str(num) + '/' + str(den) sone = math.copysign(1.0, val)
res = rvs + 'p' + _to_int_str(exp) if sone < 0.0:
return "-0.0"
else:
return "+0.0"
elif val == float("+inf"):
res = "+oo"
elif val == float("-inf"):
res = "-oo"
else:
v = val.as_integer_ratio()
num = v[0]
den = v[1]
rvs = str(num) + '/' + str(den)
res = rvs + 'p' + _to_int_str(exp)
elif isinstance(val, bool): elif isinstance(val, bool):
if val: if val:
res = "1.0" res = "1.0"
@ -8511,6 +8525,12 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(-2.25, FPSort(8, 24)) >>> v = FPVal(-2.25, FPSort(8, 24))
>>> v >>> v
-1.125*(2**1) -1.125*(2**1)
>>> v = FPVal(-0.0, FPSort(8, 24))
-0.0
>>> v = FPVal(0.0, FPSort(8, 24))
+0.0
>>> v = FPVal(+0.0, FPSort(8, 24))
+0.0
""" """
ctx = _get_ctx(ctx) ctx = _get_ctx(ctx)
if is_fp_sort(exp): if is_fp_sort(exp):
@ -8522,7 +8542,18 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
if exp == None: if exp == None:
exp = 0 exp = 0
val = _to_float_str(sig) val = _to_float_str(sig)
return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) if val == "NaN" or val == "nan":
return fpNaN(fps)
elif val == "-0.0":
return fpMinusZero(fps)
elif val == "0.0" or val == "+0.0":
return fpPlusZero(fps)
elif val == "+oo" or val == "+inf" or val == "+Inf":
return fpPlusInfinity(fps)
elif val == "-oo" or val == "-inf" or val == "-Inf":
return fpMinusInfinity(fps)
else:
return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
def FP(name, fpsort, ctx=None): def FP(name, fpsort, ctx=None):
"""Return a floating-point constant named `name`. """Return a floating-point constant named `name`.