From 5bd00d3f8350e1930741318ef9d4e72791926dc8 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 21 Oct 2016 15:39:02 +0100
Subject: [PATCH] Bugfixes for the FPA  API

---
 src/api/api_fpa.cpp     | 25 ++++++++-----------------
 src/api/python/z3/z3.py |  6 +++---
 2 files changed, 11 insertions(+), 20 deletions(-)

diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 37197e730..5d423c725 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -914,7 +914,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         family_id fid = mk_c(c)->get_fpa_fid();
         expr * e = to_expr(t);
-        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
@@ -933,6 +933,8 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_significand_string(c, t);
         RESET_ERROR_CODE();
+        CHECK_NON_NULL(t, 0);
+        CHECK_VALID_AST(t, 0);
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
@@ -940,10 +942,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
@@ -958,6 +957,7 @@ extern "C" {
         mpqm.set(q, mpfm.sig(val));
         if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q);
         mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
+        if (mpfm.is_inf(val)) mpqm.set(q, 0);
         std::stringstream ss;
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
@@ -975,10 +975,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             *n = 0;
             return 0;
@@ -1008,10 +1005,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
@@ -1040,10 +1034,7 @@ extern "C" {
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         SASSERT(plugin != 0);
         expr * e = to_expr(t);
-        if (!is_app(e) ||
-            is_app_of(e, fid, OP_FPA_NAN) ||
-            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
-            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+        if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             *n = 0;
             return 0;
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index c360a9bdc..361171b56 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8496,7 +8496,7 @@ class FPNumRef(FPRef):
     """
     def as_string(self):
         s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
-        return ("FPVal(%s, %s)" % (s, FPSortRef(self.sort()).as_string()))
+        return ("FPVal(%s, %s)" % (s, self.sort()))
 
 def is_fp(a):
     """Return `True` if `a` is a Z3 floating-point expression.
@@ -8536,7 +8536,7 @@ def FPSort(ebits, sbits, ctx=None):
     >>> eq(x, FP('x', FPSort(8, 24)))
     True
     """
-    ctx = z3._get_ctx(ctx)
+    ctx = _get_ctx(ctx)
     return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
 
 def _to_float_str(val, exp=0):
@@ -8722,7 +8722,7 @@ def FPs(names, fpsort, ctx=None):
     >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
     fpMul(RNE(), fpAdd(RNE(), x, y), z)
     """
-    ctx = z3._get_ctx(ctx)
+    ctx = _get_ctx(ctx)
     if isinstance(names, str):
         names = names.split(" ")
     return [FP(name, fpsort, ctx) for name in names]