From d731ec7cbaf88bb464b8b9f1e0c7e82cd8fdd59f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 08:44:15 -0700
Subject: [PATCH] Revert "Cpp api fp to bv (#5218)" (#5221)

This reverts commit fa2d59373933f9be9112749fbdb00c7ffb6cfbba.
---
 src/api/c++/z3++.h | 36 +-----------------------------------
 1 file changed, 1 insertion(+), 35 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 51654abd5..24547891e 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -895,7 +895,7 @@ namespace z3 {
         */
         expr mk_to_ieee_bv() const {
             assert(is_fpa());
-            Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
+            Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast),
             check_error();
             return expr(ctx(), r);
         }
@@ -1307,19 +1307,6 @@ namespace z3 {
           */
         friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);
 
-        /**
-           \brief Create an expression of FloatingPoint sort from three bit-vector expressions.
-        */
-        friend expr fpa_fp(expr const& rm, expr const& fp, unsigned bv_len);
-        /**
-           \brief Conversion of a floating-point term into a signed bit-vector
-        */
-        friend expr fpa_to_sbv(sort const& rm, expr const& fp, unsigned bv_len);
-        /**
-           \brief Conversion of a floating-point term into a unsigned bit-vector
-        */
-        friend expr fpa_to_ubv(sort const& rm, expr const& fp, unsigned bv_len);
-
         /**
            \brief sequence and regular expression operations.
            + is overloaded as sequence concatenation and regular expression union.
@@ -1817,27 +1804,6 @@ namespace z3 {
         return expr(a.ctx(), r);
     }
 
-    inline expr fpa_fp(expr const& sgn, expr const& exp, expr const & sig) {
-        check_context(sgn, exp); check_context(exp, sig);
-        Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
-        sgn.check_error();
-        return expr(sgn.ctx(), r);
-    }
-    inline expr fpa_to_sbv(sort const& rm, expr const& fp, unsigned bv_len) {
-        check_context(rm, fp);
-        assert(fp.is_fpa());
-        Z3_ast r = Z3_mk_fpa_to_sbv(fp.ctx(), rm.m_ast, fp.m_ast, bv_len);
-        fp.check_error();
-        return expr(fp.ctx(), r);
-    }
-    inline expr fpa_to_ubv(sort const& rm, expr const& fp, unsigned bv_len) {
-        check_context(rm, fp);
-        assert(fp.is_fpa());
-        Z3_ast r = Z3_mk_fpa_to_ubv(fp.ctx(), rm.m_ast, fp.m_ast, bv_len);
-        fp.check_error();
-        return expr(fp.ctx(), r);
-    }
-
 
     /**
        \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>