From 9cbf45f689cc7d2722c869d830881136a48a6bc4 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 26 Mar 2015 14:48:55 +0000
Subject: [PATCH] Added int to float conversion.

---
 src/ast/fpa/fpa2bv_converter.cpp |  6 ++++--
 src/ast/fpa_decl_plugin.cpp      | 24 ++++++++++++++++++------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 8e2dd326a..89072a795 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1878,6 +1878,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     else if (num == 2 &&
              m_bv_util.is_bv(args[0]) &&
              m_bv_util.get_bv_size(args[0]) == 3 &&
+             m_arith_util.is_int(args[1]) || 
              m_arith_util.is_real(args[1])) {
         // rm + real -> float
         mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
@@ -2066,7 +2067,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
     TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << 
                                     "x: " << mk_ismt2_pp(x, m) << std::endl;);
     SASSERT(m_util.is_float(s));
-    SASSERT(au().is_real(x));
+    SASSERT(au().is_real(x) || au().is_int(x));
 
     unsigned ebits = m_util.get_ebits(s);
     unsigned sbits = m_util.get_sbits(s);
@@ -2089,7 +2090,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         }
 
         rational q;
-        m_util.au().is_numeral(x, q);
+        bool is_int;
+        m_util.au().is_numeral(x, q, is_int);
 
         scoped_mpf v(m_mpf_manager);
         m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index bd2676ee4..48b7adb8b 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -521,14 +521,26 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
         symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
+    else if (arity == 2 &&
+             is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+             is_sort_of(domain[1], m_arith_fid, INT_SORT)) {
+        // Rounding + 1 Int -> 1 FP
+        if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
+            m_manager->raise_exception("expecting two integer parameters to to_fp");
+
+        sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+        symbol name("to_fp");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
     else {
         m_manager->raise_exception("Unexpected argument combination for (_ to_fp eb sb). Supported argument combinations are: "
-                                   "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)),"
-                                   "(_ BitVec (eb+sb)),"
-                                   "(Real),"
-                                   "(RoundingMode (_ BitVec (eb+sb))),"
-                                   "(RoundingMode (_ FloatingPoint eb' sb')),"
-                                   "(RoundingMode Real Int), and"
+                                   "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)), "
+                                   "(_ BitVec (eb+sb)), "
+                                   "(Real), "
+                                   "(RoundingMode (_ BitVec (eb+sb))), "
+                                   "(RoundingMode (_ FloatingPoint eb' sb')), "
+                                   "(RoundingMode Real Int), "
+                                   "(RoundingMode Int), and "
                                    "(RoundingMode Real)."
                                    );
     }