Eliminated unspecified operators for fp.to_*bv, fp.to_real. Also fixes #1191.

src/api/api_ast.cpp

@@ -1210,10 +1210,6 @@ extern "C" {
             case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM;
             case OP_FPA_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED;
             case OP_FPA_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED;
-            case OP_FPA_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED;
-            case OP_FPA_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED;
-            case OP_FPA_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED;
-            case OP_FPA_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED;
                 return Z3_OP_UNINTERPRETED;
             default:
                 return Z3_OP_INTERNAL;

src/api/z3_api.h

@@ -1005,18 +1005,6 @@ typedef enum
       - Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the
         arguments are expected to be zeroes with different signs.
 
-      - Z3_OP_FPA_TO_UBV_UNSPECIFIED: A term representing the unspecified
-        results of Z3_OP_FPA_TO_UBV.
-
-      - Z3_OP_FPA_TO_SBV_UNSPECIFIED: A term representing the unspecified
-        results of Z3_OP_FPA_TO_SBV.
-
-      - Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED: A term representing the unspecified
-        results of Z3_OP_FPA_TO_IEEE_BV.
-
-      - Z3_OP_FPA_TO_REAL_UNSPECIFIED: A term representing the unspecified
-        results of Z3_OP_FPA_TO_IEEE_BV.
-
       - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
         information is exposed. Tools may use the string representation of the
         function declaration to obtain more information.
@@ -1310,10 +1298,6 @@ typedef enum {
     Z3_OP_FPA_BV2RM,
     Z3_OP_FPA_MIN_UNSPECIFIED,
     Z3_OP_FPA_MAX_UNSPECIFIED,
-    Z3_OP_FPA_TO_UBV_UNSPECIFIED,
-    Z3_OP_FPA_TO_SBV_UNSPECIFIED,
-    Z3_OP_FPA_TO_REAL_UNSPECIFIED,
-    Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED,
 
     Z3_OP_INTERNAL,
 

src/ast/fpa/bv2fpa_converter.cpp

@@ -291,9 +291,11 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
         app_ref bv_els(m);
         expr_ref ft_els(m);
         bv_els = (app*)bv_fi->get_else();
-        ft_els = rebuild_floats(mc, rng, bv_els);
+        if (bv_els != 0) {
-        m_th_rw(ft_els);
+            ft_els = rebuild_floats(mc, rng, bv_els);
-        result->set_else(ft_els);
+            m_th_rw(ft_els);
+            result->set_else(ft_els);
+        }
     }
 
     return result;
@@ -447,8 +449,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
             }
         }
         else {
-            func_interp * fmv = convert_func_interp(mc, f, it->m_value);
+            if (it->get_key().get_family_id() == m_fpa_util.get_fid()) {
-            if (fmv) target_model->register_decl(f, fmv);
+                // it->m_value contains the model for the unspecified cases of it->m_key.
+                continue;
+
+                // Upon request, add this 'recursive' definition?
+                func_interp * fmv = convert_func_interp(mc, f, it->m_value);
+                unsigned n = fmv->get_arity();
+                expr_ref_vector args(m);
+                for (unsigned i = 0; i < n; i++)
+                    args.push_back(m.mk_var(i, f->get_domain()[i]));
+                fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
+            }
+            else {
+                func_interp * fmv = convert_func_interp(mc, f, it->m_value);
+                if (fmv) target_model->register_decl(f, fmv);
+            }
         }
     }
 }

src/ast/fpa/fpa2bv_converter.cpp

@@ -2855,8 +2855,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
 
     expr_ref unspec(m);
-    unspec = mk_to_real_unspecified(ebits, sbits);
+    mk_to_real_unspecified(f, num, args, unspec);
-
     result = m.mk_ite(x_is_zero, zero, res);
     result = m.mk_ite(x_is_inf, unspec, result);
     result = m.mk_ite(x_is_nan, unspec, result);
@@ -3141,11 +3140,12 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
 
 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
-    expr_ref x(m), x_is_nan(m);
+    expr_ref x(m), x_is_nan(m), x_flat(m);
     expr * sgn, * s, * e;
     x = args[0];
     split_fp(x, sgn, e, s);
     mk_is_nan(x, x_is_nan);
+    join_fp(x, x_flat);
 
     sort * fp_srt = m.get_sort(x);
     unsigned ebits = m_util.get_ebits(fp_srt);
@@ -3159,13 +3159,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
                 m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
                     m_bv_util.mk_numeral(1, 1))));
     else {
-        app_ref unspec(m);
+        expr * x_flatp = x_flat.get();
-        unspec = m_util.mk_to_ieee_bv_unspecified(ebits, sbits);
+        mk_to_ieee_bv_unspecified(f, 1, &x_flatp, nanv);
-        mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv);
     }
 
     expr_ref sgn_e_s(m);
-    sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
+    join_fp(x, sgn_e_s);
     m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
 
     TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
@@ -3173,7 +3172,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
 }
 
 void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    SASSERT(num == 0);
+    SASSERT(num == 1);
+    SASSERT(m_util.is_float(args[0]));
     unsigned ebits = f->get_parameter(0).get_int();
     unsigned sbits = f->get_parameter(1).get_int();
 
@@ -3184,26 +3184,30 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
                     m_bv_util.mk_numeral(1, sbits-1));
     }
     else {
-        func_decl * fd;
+        expr * n = args[0];
-        if (m_uf2bvuf.find(f, fd))
+        expr_ref n_bv(m);
-            result = m.mk_const(fd);
+        join_fp(n, n_bv);
-        else {
+
-            fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
+        func_decl * f_bv;
-            m_uf2bvuf.insert(f, fd);
+        if (!m_uf2bvuf.find(f, f_bv)) {
+            sort * domain[2] = { m.get_sort(n_bv) };
+            f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
+            m_uf2bvuf.insert(f, f_bv);
             m.inc_ref(f);
-            m.inc_ref(fd);
+            m.inc_ref(f_bv);
-            result = m.mk_const(fd);
-
-            expr_ref exp_bv(m), exp_all_ones(m);
-            exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
-            exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
-            m_extra_assertions.push_back(exp_all_ones);
-
-            expr_ref sig_bv(m), sig_is_non_zero(m);
-            sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
-            sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
-            m_extra_assertions.push_back(sig_is_non_zero);
         }
+
+        result = m.mk_app(f_bv, n_bv);
+
+        expr_ref exp_bv(m), exp_all_ones(m);
+        exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
+        exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
+        m_extra_assertions.push_back(exp_all_ones);
+
+        expr_ref sig_bv(m), sig_is_non_zero(m);
+        sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
+        sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
+        m_extra_assertions.push_back(sig_is_non_zero);
     }
 
     TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
@@ -3238,15 +3242,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     mk_is_nzero(x, x_is_nzero);
 
     // NaN, Inf, or negative (except -0) -> unspecified
-    expr_ref c1(m), v1(m);
+    expr_ref c1(m), v1(m), unspec_v(m);
-    if (!is_signed) {
+    if (!is_signed)
         c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
-        v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
+    else
-    }
-    else {
         c1 = m.mk_or(x_is_nan, x_is_inf);
-        v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz);
+    mk_to_bv_unspecified(f, num, args, unspec_v);
-    }
+    v1 = unspec_v;
     dbg_decouple("fpa2bv_to_bv_c1", c1);
 
     // +-Zero  -> 0
@@ -3355,11 +3357,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
 
     dbg_decouple("fpa2bv_to_bv_rnd", rnd);
 
-    expr_ref unspec(m);
+    result = m.mk_ite(rnd_has_overflown, unspec_v, rnd);
-    unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) :
+    result = m.mk_ite(c_in_limits, result, unspec_v);
-                         mk_to_ubv_unspecified(ebits, sbits, bv_sz);
-    result = m.mk_ite(rnd_has_overflown, unspec, rnd);
-    result = m.mk_ite(c_in_limits, result, unspec);
     result = m.mk_ite(c2, v2, result);
     result = m.mk_ite(c1, v1, result);
 
@@ -3378,85 +3377,54 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     mk_to_bv(f, num, args, true, result);
 }
 
-void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    SASSERT(num == 0);
+    SASSERT(num == 2);
-    unsigned width = m_bv_util.get_bv_size(f->get_range());
+    SASSERT(m_util.is_bv2rm(args[0]));
+    SASSERT(m_util.is_float(args[1]));
 
     if (m_hi_fp_unspecified)
-        result = m_bv_util.mk_numeral(0, width);
+        result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range()));
     else {
-        func_decl * fd;
+        expr * rm_bv = to_app(args[0])->get_arg(0);
-        if (!m_uf2bvuf.find(f, fd)) {
+        expr * n = args[1];
-            fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
+        expr_ref n_bv(m);
-            m_uf2bvuf.insert(f, fd);
+        join_fp(n, n_bv);
+
+        func_decl * f_bv;
+        if (!m_uf2bvuf.find(f, f_bv)) {
+            sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) };
+            f_bv = m.mk_fresh_func_decl(0, 2, domain, f->get_range());
+            m_uf2bvuf.insert(f, f_bv);
             m.inc_ref(f);
-            m.inc_ref(fd);
+            m.inc_ref(f_bv);
         }
-        result = m.mk_const(fd);
+        result = m.mk_app(f_bv, rm_bv, n_bv);
     }
 
-    TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
+    TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
     SASSERT(is_well_sorted(m, result));
 }
 
-expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    expr_ref res(m);
-    app_ref u(m);
-    u = m_util.mk_to_ubv_unspecified(ebits, sbits, width);
-    mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
-    return res;
-}
-
-void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    SASSERT(num == 0);
-    unsigned width = m_bv_util.get_bv_size(f->get_range());
-
-    if (m_hi_fp_unspecified)
-        result = m_bv_util.mk_numeral(0, width);
-    else {
-        func_decl * fd;
-        if (!m_uf2bvuf.find(f, fd)) {
-            fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
-            m_uf2bvuf.insert(f, fd);
-            m.inc_ref(f);
-            m.inc_ref(fd);
-        }
-        result = m.mk_const(fd);
-    }
-
-    TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
-    SASSERT(is_well_sorted(m, result));
-}
-
-expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    expr_ref res(m);
-    app_ref u(m);
-    u = m_util.mk_to_sbv_unspecified(ebits, sbits, width);
-    mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
-    return res;
-}
-
 void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+
     if (m_hi_fp_unspecified)
         result = m_arith_util.mk_numeral(rational(0), false);
     else {
-        func_decl * fd;
+        expr * n = args[0];
-        if (!m_uf2bvuf.find(f, fd)) {
+        expr_ref n_bv(m);
-            fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
+        join_fp(n, n_bv);
-            m_uf2bvuf.insert(f, fd);
-            m.inc_ref(f);
-            m.inc_ref(fd);
-        }
-        result = m.mk_const(fd);
-    }
-}
 
-expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
+        func_decl * f_bv;
-    expr_ref res(m);
+        if (!m_uf2bvuf.find(f, f_bv)) {
-    app_ref u(m);
+            sort * domain[2] = { m.get_sort(n_bv) };
-    u = m_util.mk_to_real_unspecified(ebits, sbits);
+            f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
-    mk_to_real_unspecified(u->get_decl(), 0, 0, res);
+            m_uf2bvuf.insert(f, f_bv);
-    return res;
+            m.inc_ref(f);
+            m.inc_ref(f_bv);
+        }
+        result = m.mk_app(f_bv, n_bv);
+    }
 }
 
 void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -3467,6 +3435,7 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
     result = m_util.mk_fp(args[0], args[1], args[2]);
     TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
 }
+
 void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
     SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
@@ -3485,6 +3454,14 @@ void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_r
     sig = e_sig;
 }
 
+void fpa2bv_converter::join_fp(expr * e, expr_ref & res) {
+    SASSERT(m_util.is_fp(e));
+    SASSERT(to_app(e)->get_num_args() == 3);
+    expr *sgn, *exp, *sig;
+    split_fp(e, sgn, exp, sig);
+    res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig);
+}
+
 void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split_fp(e, sgn, exp, sig);
@@ -4051,7 +4028,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     // put the sticky bit into the significand.
     expr_ref ext_sticky(m);
     ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky);
-    expr * tmp[] = { sig, ext_sticky };
+    expr * tmp[2] = { sig, ext_sticky };
     sig = m_bv_util.mk_bv_or(2, tmp);
     SASSERT(is_well_sorted(m, sig));
     SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);

src/ast/fpa/fpa2bv_converter.h

@@ -76,6 +76,7 @@ public:
 
     void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
     void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
+    void join_fp(expr * e, expr_ref & res);
 
     void mk_eq(expr * a, expr * b, expr_ref & result);
     void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
@@ -138,9 +139,8 @@ public:
     void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
     void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
@@ -226,10 +226,6 @@ private:
     void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
 
     void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
-
-    expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
 };
 
 #endif

src/ast/fpa/fpa2bv_rewriter.cpp

@@ -143,13 +143,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
         case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
-        case OP_FPA_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
-        case OP_FPA_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
-        case OP_FPA_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
-        case OP_FPA_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
 
         case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
         case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;

src/ast/fpa_decl_plugin.cpp

@@ -711,65 +711,6 @@ func_decl * fpa_decl_plugin::mk_bv_wrap(decl_kind k, unsigned num_parameters, pa
     }
 }
 
-func_decl * fpa_decl_plugin::mk_to_ubv_unspecified(
-    decl_kind k, unsigned num_parameters, parameter const * parameters,
-    unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 0)
-        m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified");
-    if (num_parameters != 3)
-        m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3");
-    if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers");
-
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
-    return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
-}
-
-func_decl * fpa_decl_plugin::mk_to_sbv_unspecified(
-    decl_kind k, unsigned num_parameters, parameter const * parameters,
-    unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 0)
-        m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified");
-    if (num_parameters != 3)
-        m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3");
-    if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers");
-
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
-    return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
-}
-
-func_decl * fpa_decl_plugin::mk_to_real_unspecified(
-    decl_kind k, unsigned num_parameters, parameter const * parameters,
-    unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 0)
-        m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified");
-    if (num_parameters != 2)
-        m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2");
-    if (!parameters[0].is_int() || !parameters[1].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers");
-    if (!is_sort_of(range, m_arith_fid, REAL_SORT))
-        m_manager->raise_exception("sort mismatch, expected range of Real sort");
-
-    return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters));
-}
-
-func_decl * fpa_decl_plugin::mk_to_ieee_bv_unspecified(
-    decl_kind k, unsigned num_parameters, parameter const * parameters,
-    unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 0)
-        m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified; expecting none");
-    if (num_parameters != 2)
-        m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 2");
-    if (!parameters[0].is_int() || !parameters[1].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting 2 integers");
-
-    parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) };
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p);
-    return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
-}
-
-
 func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                             unsigned arity, sort * const * domain, sort * range) {
     switch (k) {
@@ -846,14 +787,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_MAX_UNSPECIFIED:
         return mk_binary_decl(k, num_parameters, parameters, arity, domain, range);
 
-    case OP_FPA_TO_UBV_UNSPECIFIED:
-        return mk_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range);
-    case OP_FPA_TO_SBV_UNSPECIFIED:
-        return mk_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range);
-    case OP_FPA_TO_REAL_UNSPECIFIED:
-        return mk_to_real_unspecified(k, num_parameters, parameters, arity, domain, range);
-    case OP_FPA_TO_IEEE_BV_UNSPECIFIED:
-        return mk_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range);
     default:
         m_manager->raise_exception("unsupported floating point operator");
         return 0;
@@ -1054,30 +987,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
     return mk_value(v);
 }
 
-app * fpa_util::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
-    sort * range = m_bv_util.mk_sort(width);
-    return m().mk_app(get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range);
-}
-
-app * fpa_util::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
-    sort * range = m_bv_util.mk_sort(width);
-    return m().mk_app(get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range);
-}
-
-app * fpa_util::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
-    parameter ps[] = { parameter(ebits), parameter(sbits) };
-    sort * range = m_bv_util.mk_sort(ebits+sbits);
-    return m().mk_app(get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range);
-}
-
-app * fpa_util::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
-    parameter ps[] = { parameter(ebits), parameter(sbits) };
-    sort * range = m_a_util.mk_real();
-    return m().mk_app(get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range);
-}
-
 bool fpa_util::contains_floats(ast * a) {
     switch (a->get_kind()) {
     case AST_APP: {

src/ast/fpa_decl_plugin.h

@@ -93,10 +93,6 @@ enum fpa_op_kind {
     OP_FPA_MAX_I,
     OP_FPA_MIN_UNSPECIFIED,
     OP_FPA_MAX_UNSPECIFIED,
-    OP_FPA_TO_UBV_UNSPECIFIED,
-    OP_FPA_TO_SBV_UNSPECIFIED,
-    OP_FPA_TO_IEEE_BV_UNSPECIFIED,
-    OP_FPA_TO_REAL_UNSPECIFIED,
 
     LAST_FLOAT_OP
 };
@@ -167,34 +163,12 @@ class fpa_decl_plugin : public decl_plugin {
                                   unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                               unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                               unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                                unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                                   unsigned arity, sort * const * domain, sort * range);
 
     virtual void set_manager(ast_manager * m, family_id id);
     unsigned mk_id(mpf const & v);
     void recycled_id(unsigned id);
 
-    virtual bool is_considered_uninterpreted(func_decl * f) {
+    virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
-        if (f->get_family_id() != get_family_id())
-            return false;
-        switch (f->get_decl_kind())
-        {
-        case OP_FPA_TO_UBV_UNSPECIFIED:
-        case OP_FPA_TO_SBV_UNSPECIFIED:
-        case OP_FPA_TO_REAL_UNSPECIFIED:
-        case OP_FPA_TO_IEEE_BV_UNSPECIFIED:
-            return true;
-        default:
-            return false;
-        }
-        return false;
-    }
 
 public:
     fpa_decl_plugin();
@@ -374,10 +348,6 @@ public:
         SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
         return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort());
     }
-    app * mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    app * mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    app * mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
-    app * mk_to_real_unspecified(unsigned ebits, unsigned sbits);
 
     bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); }
     bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; }
@@ -388,19 +358,15 @@ public:
     bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); }
     bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); }
     bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); }
-    bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED); }
+    bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); }
-    bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED); }
+    bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); }
-    bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED); }
-    bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED); }
 
     bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_I; }
     bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_UNSPECIFIED; }
     bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_I; }
     bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_UNSPECIFIED; }
-    bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV_UNSPECIFIED; }
+    bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; }
-    bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV_UNSPECIFIED; }
+    bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; }
-    bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV_UNSPECIFIED; }
-    bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_REAL_UNSPECIFIED; }
 
     bool contains_floats(ast * a);
 };

src/ast/rewriter/fpa_rewriter.cpp

@@ -103,57 +103,12 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
     case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
 
-    case OP_FPA_TO_UBV_UNSPECIFIED:
-    case OP_FPA_TO_SBV_UNSPECIFIED:
-    case OP_FPA_TO_REAL_UNSPECIFIED:
-    case OP_FPA_TO_IEEE_BV_UNSPECIFIED:
-        st = BR_FAILED;
-        break;
-
     default:
         NOT_IMPLEMENTED_YET();
     }
     return st;
 }
 
-br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
-    bv_util bu(m());
-    if (m_hi_fp_unspecified) {
-        // The "hardware interpretation" is 0.
-        result = bu.mk_numeral(0, width);
-        return BR_DONE;
-    }
-    else {
-        result = m_util.mk_to_ubv_unspecified(ebits, sbits, width);
-        return BR_REWRITE1;
-    }
-}
-
-br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
-    bv_util bu(m());
-    if (m_hi_fp_unspecified) {
-        // The "hardware interpretation" is 0.
-        result = bu.mk_numeral(0, width);
-        return BR_DONE;
-    }
-    else {
-        result = m_util.mk_to_sbv_unspecified(ebits, sbits, width);
-        return BR_REWRITE1;
-    }
-}
-
-br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
-    if (m_hi_fp_unspecified) {
-        // The "hardware interpretation" is 0.
-        result = m_util.au().mk_numeral(rational(0), false);
-        return BR_DONE;
-    }
-    else {
-        result = m_util.mk_to_real_unspecified(ebits, sbits);
-        return BR_REWRITE1;
-    }
-}
-
 br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_num_parameters() == 2);
     SASSERT(f->get_parameter(0).is_int());
@@ -808,7 +763,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
         const mpf & x = v.get();
 
         if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v))
-            return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
+            return BR_FAILED;
 
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
@@ -822,9 +777,6 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
             result = bu.mk_numeral(r, bv_sz);
             return BR_DONE;
         }
-        else
-            return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
-
     }
 
     return BR_FAILED;
@@ -842,7 +794,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
         const mpf & x = v.get();
 
         if (m_fm.is_nan(v) || m_fm.is_inf(v))
-            return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
+            return BR_FAILED;
 
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
@@ -856,8 +808,6 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
             result = bu.mk_numeral(r, bv_sz);
             return BR_DONE;
         }
-        else
-            return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
     }
 
     return BR_FAILED;
@@ -881,7 +831,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
                 result = bu.mk_concat(4, args);
             }
             else
-                result = m_util.mk_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
+                return BR_FAILED;
 
             return BR_REWRITE1;
         }
@@ -900,16 +850,12 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
     scoped_mpf v(m_fm);
 
     if (m_util.is_numeral(arg, v)) {
-        if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
+        if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) {
-            const mpf & x = v.get();
-            result = m_util.mk_to_real_unspecified(x.get_ebits(), x.get_sbits());
-        }
-        else {
             scoped_mpq r(m_fm.mpq_manager());
             m_fm.to_rational(v, r);
             result = m_util.au().mk_numeral(r.get(), false);
+            return BR_DONE;
         }
-        return BR_DONE;
     }
 
     return BR_FAILED;

src/ast/rewriter/fpa_rewriter.h

@@ -88,9 +88,7 @@ public:
     br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
 
-    br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
+    br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr * n, expr_ref & result);
-    br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
-    br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
 
     br_status mk_bvwrap(expr * arg, expr_ref & result);
 };

src/smt/theory_fpa.cpp

@@ -119,6 +119,7 @@ namespace smt {
         SASSERT(m_conversions.empty());
         SASSERT(m_is_added_to_model.empty());
     }
+
     void theory_fpa::init(context * ctx) {
         smt::theory::init(ctx);
         m_is_initialized = true;
@@ -890,14 +891,10 @@ namespace smt {
         if (f->get_family_id() == get_family_id()) {
             bool include =
                 m_fpa_util.is_min_unspecified(f) ||
-                m_fpa_util.is_max_unspecified(f) ||
+                m_fpa_util.is_max_unspecified(f) ;
-                m_fpa_util.is_to_ubv_unspecified(f) ||
-                m_fpa_util.is_to_sbv_unspecified(f) ||
-                m_fpa_util.is_to_ieee_bv_unspecified(f) ||
-                m_fpa_util.is_to_real_unspecified(f);
             if (include && !m_is_added_to_model.contains(f)) {
-                m_is_added_to_model.insert(f);
+                //m_is_added_to_model.insert(f);
-                get_manager().inc_ref(f);
+                //get_manager().inc_ref(f);
                 return true;
             }
             return false;