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`.