From a951ff076976587dcadfd863ca779c0c215cc8b7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 8 Oct 2015 16:04:17 +0100
Subject: [PATCH] Fix for FP UFs and conversion functions.

---
 src/ast/fpa/fpa2bv_rewriter.h | 52 ++++++++++++++++-------------------
 src/smt/theory_fpa.cpp        | 22 +++++++++++----
 2 files changed, 40 insertions(+), 34 deletions(-)

diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 41b6c0ca9..1b7d55173 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -79,36 +79,16 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
 
-        if (f->get_family_id() == null_family_id) {
-            if (num == 0) {
-                if (m_conv.is_float(f->get_range())) {
-                    m_conv.mk_const(f, result);
-                    return BR_DONE;
-                }
-                else if (m_conv.is_rm(f->get_range())) {
-                    m_conv.mk_rm_const(f, result);
-                    return BR_DONE;
-                }
-                else
-                    return BR_FAILED;
-            }
-            else {
-                bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
-                
-                for (unsigned i = 0; i < f->get_arity(); i++) {
-                    sort * di = f->get_domain()[i];
-                    is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
-                }
-                
-                if (is_float_uf) {
-                    m_conv.mk_uninterpreted_function(f, num, args, result);
-                    return BR_DONE;
-                }
-                else
-                    return BR_FAILED;
-            }            
+        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
+            m_conv.mk_const(f, result);
+            return BR_DONE;
         }
-        
+
+        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
+            m_conv.mk_rm_const(f, result);
+            return BR_DONE;
+        }
+
         if (m().is_eq(f)) {
             SASSERT(num == 2);
             TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << 
@@ -199,6 +179,20 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
                 NOT_IMPLEMENTED_YET();
             }
         }
+        else {
+            SASSERT(!m_conv.is_float_family(f));
+            bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
+
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                sort * di = f->get_domain()[i];
+                is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
+            }
+
+            if (is_float_uf) {
+                m_conv.mk_uninterpreted_function(f, num, args, result);
+                return BR_DONE;
+            }
+        }
 
         return BR_FAILED;
     }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 46c9d962d..cf6a367a9 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -331,8 +331,21 @@ namespace smt {
         proof_ref pr(m);
         m_rw(e, e_conv);
         
-        if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
-            m_th_rw(e_conv, res);
+        if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {            
+            if (!m_fpa_util.is_float(e_conv))
+                m_th_rw(e_conv, res);
+            else {
+                expr_ref bv(m);            
+                bv = wrap(e_conv);
+                unsigned bv_sz = m_bv_util.get_bv_size(bv);
+                unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
+                unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv));
+                SASSERT(bv_sz == ebits + sbits);
+                m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
+                    m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
+                    m_bv_util.mk_extract(sbits - 2, 0, bv),
+                    res);
+            }
         }
         else if (m_fpa_util.is_rm(e)) {
             SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
@@ -464,7 +477,7 @@ namespace smt {
             else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
                 res = convert_term(e);
             else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
-                res = convert_conversion_term(e);
+                res = convert_conversion_term(e);            
             else
                 UNREACHABLE();
 
@@ -643,13 +656,12 @@ namespace smt {
         expr_ref xc(m), yc(m);
         xc = convert(xe);
         yc = convert(ye);
-        
 
         TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl <<
                                       "yc = " << mk_ismt2_pp(yc, m) << std::endl;);
 
         expr_ref c(m);
-               
+        
         if (fu.is_float(xe) && fu.is_float(ye))
             m_converter.mk_eq(xc, yc, c);
         else