From 59e695f2be96e586ebb7c9c7560ec12c7436f970 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 1 Mar 2016 21:21:25 +0000
Subject: [PATCH] Bugfixes for FP numerals in Python
Relates to #464, #470
---
src/api/python/z3.py | 43 +++++++++++++++++++++++++++++++++++++------
1 file changed, 37 insertions(+), 6 deletions(-)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 814198d22..531f2e8cd 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -48,6 +48,7 @@ from z3printer import *
from fractions import Fraction
import sys
import io
+import math
if sys.version < '3':
def _is_int(v):
@@ -8409,11 +8410,24 @@ def FPSort(ebits, sbits, ctx=None):
def _to_float_str(val, exp=0):
if isinstance(val, float):
- v = val.as_integer_ratio()
- num = v[0]
- den = v[1]
- rvs = str(num) + '/' + str(den)
- res = rvs + 'p' + _to_int_str(exp)
+ if math.isnan(val):
+ res = "NaN"
+ elif val == 0.0:
+ sone = math.copysign(1.0, val)
+ 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):
if val:
res = "1.0"
@@ -8511,6 +8525,12 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-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)
if is_fp_sort(exp):
@@ -8522,7 +8542,18 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
if exp == None:
exp = 0
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):
"""Return a floating-point constant named `name`.