Bugfixes for UFs in theory_fpa.

Fixes #591, but performance issues remain.

src/ast/fpa/fpa2bv_converter.cpp

@@ -2235,14 +2235,17 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     SASSERT(is_well_sorted(m, result));
 }
 
+
 void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
+    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result);
+}
+
+void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_ref & result) {
     unsigned from_sbits = m_util.get_sbits(m.get_sort(x));
     unsigned from_ebits = m_util.get_ebits(m.get_sort(x));
-    unsigned to_sbits = m_util.get_sbits(s);
+    unsigned to_sbits = m_util.get_sbits(to_srt);
-    unsigned to_ebits = m_util.get_ebits(s);
+    unsigned to_ebits = m_util.get_ebits(to_srt);
-
-    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
-    expr * bv_rm = to_app(rm)->get_arg(0);
 
     if (from_sbits == to_sbits && from_ebits == to_ebits)
         result = x;
@@ -2253,20 +2256,20 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
 
         one1 = m_bv_util.mk_numeral(1, 1);
         expr_ref ninf(m), pinf(m);
-        mk_pinf(f, pinf);
+        mk_pinf(to_srt, pinf);
-        mk_ninf(f, ninf);
+        mk_ninf(to_srt, ninf);
 
         // NaN -> NaN
         mk_is_nan(x, c1);
-        mk_nan(f, v1);
+        mk_nan(to_srt, v1);
 
         // +0 -> +0
         mk_is_pzero(x, c2);
-        mk_pzero(f, v2);
+        mk_pzero(to_srt, v2);
 
         // -0 -> -0
         mk_is_nzero(x, c3);
-        mk_nzero(f, v3);
+        mk_nzero(to_srt, v3);
 
         // +oo -> +oo
         mk_is_pinf(x, c4);
@@ -2380,8 +2383,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
         dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
 
         expr_ref rounded(m);
-        expr_ref rm_e(bv_rm, m);
+        expr_ref rm_e(rm, m);
-        round(s, rm_e, res_sgn, res_sig, res_exp, rounded);
+        round(to_srt, rm_e, res_sgn, res_sig, res_exp, rounded);
 
         expr_ref is_neg(m), sig_inf(m);
         m_simp.mk_eq(sgn, one1, is_neg);

src/ast/fpa/fpa2bv_converter.h

@@ -144,6 +144,9 @@ public:
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;
 
+    bool is_special(func_decl * f) { return m_specials.contains(f); }
+    bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }
+
 protected:
     void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);
 
@@ -201,6 +204,8 @@ private:
     void mk_div(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
     void mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result);
     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);
 };
 
 #endif

src/smt/theory_fpa.cpp

@@ -85,8 +85,63 @@ namespace smt {
     }
 
     void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-        // TODO: This introduces temporary variables/func_decls that should be filtered in the end.
+        // TODO: This introduces temporary func_decls that should be filtered in the end.
-        fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
+
+        TRACE("t_fpa", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
+        SASSERT(f->get_arity() == num);
+        
+        expr_ref_buffer new_args(m);
+
+        for (unsigned i = 0; i < num; i++) {
+            if (is_float(args[i]) || is_rm(args[i])) {
+                expr_ref ai(m), wrapped(m);
+                ai = args[i];                
+                wrapped = m_th.wrap(ai);
+                new_args.push_back(wrapped);
+                m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai));
+            }
+            else
+                new_args.push_back(args[i]);
+        }
+
+        func_decl * fd;
+        if (m_uf2bvuf.find(f, fd))
+            mk_uninterpreted_output(f->get_range(), fd, new_args, result);
+        else {
+            sort_ref_buffer new_domain(m);
+
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                sort * di = f->get_domain()[i];
+                if (is_float(di))
+                    new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(di) + m_util.get_ebits(di)));
+                else if (is_rm(di))
+                    new_domain.push_back(m_bv_util.mk_sort(3));
+                else
+                    new_domain.push_back(di);
+            }
+
+            sort * frng = f->get_range();
+            sort_ref rng(frng, m);
+            if (m_util.is_float(frng))
+                rng = m_bv_util.mk_sort(m_util.get_ebits(frng) + m_util.get_sbits(frng));
+            else if (m_util.is_rm(frng))
+                rng = m_bv_util.mk_sort(3);
+
+            func_decl_ref fbv(m);
+            fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), rng);            
+            TRACE("t_fpa", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl;);
+
+            m_uf2bvuf.insert(f, fbv);
+            m.inc_ref(f);
+            m.inc_ref(fbv);
+
+            mk_uninterpreted_output(frng, fbv, new_args, result);
+        }
+
+        expr_ref fapp(m);
+        fapp = m.mk_app(f, num, args);
+        m_extra_assertions.push_back(m.mk_eq(fapp, result));        
+        TRACE("t_fpa", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
     }
 
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@@ -284,8 +339,17 @@ namespace smt {
     app_ref theory_fpa::wrap(expr * e) {
         SASSERT(!m_fpa_util.is_wrap(e));
         ast_manager & m = get_manager();
-        sort * e_srt = m.get_sort(e);
+        app_ref res(m);
 
+        if (is_app(e) &&
+            to_app(e)->get_family_id() == get_family_id() &&
+            to_app(e)->get_decl_kind() == OP_FPA_FP) {
+            expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };            
+            res = m_bv_util.mk_concat(3, cargs);
+            m_th_rw((expr_ref&)res);
+        }
+        else {
+            sort * e_srt = m.get_sort(e);
             func_decl * w;
 
             if (!m_wraps.find(e_srt, w)) {
@@ -306,8 +370,9 @@ namespace smt {
                 m.inc_ref(w);
             }
 
-        app_ref res(m);
             res = m.mk_app(w, e);
+        }
+        
         return res;
     }
 
@@ -389,59 +454,6 @@ namespace smt {
         return res;
     }
 
-#if 0
-    expr_ref theory_fpa::convert_uf(expr * e) {
-        SASSERT(is_app(e));
-        ast_manager & m = get_manager();
-        expr_ref res(m);
-
-        app * a = to_app(e);
-        func_decl * f = a->get_decl();
-        sort * const * domain = f->get_domain();
-        unsigned arity = f->get_arity();
-
-        expr_ref_buffer new_args(m);
-        expr_ref unwrapped(m);
-
-        for (unsigned i = 0; i < arity; i++) {
-            expr * ai = a->get_arg(i);
-            if (m_fpa_util.is_float(ai) || m_fpa_util.is_rm(ai)) {
-                if (m_fpa_util.is_unwrap(ai))
-                    unwrapped = ai;
-                else {
-                    // unwrapped = unwrap(wrap(ai), domain[i]);
-                    // assert_cnstr(m.mk_eq(unwrapped, ai));
-                    // assert_cnstr();
-                    unwrapped = convert_term(ai);
-                }
-
-                new_args.push_back(unwrapped);
-                TRACE("t_fpa_detail", tout << "UF arg(" << i << ") = " << mk_ismt2_pp(unwrapped, get_manager()) << "\n";);
-            }
-            else
-                new_args.push_back(ai);
-        }
-
-        sort * rng = f->get_range();
-        if (m_fpa_util.is_float(rng)) {
-            unsigned sbits = m_fpa_util.get_sbits(rng);
-            unsigned bv_sz = m_fpa_util.get_ebits(rng) + sbits;
-            expr_ref wrapped(m);
-            wrapped = wrap(m.mk_app(f, new_args.size(), new_args.c_ptr()));
-
-            m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
-                              m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
-                              m_bv_util.mk_extract(sbits - 2, 0, wrapped),
-                              res);
-        }
-        else
-            res = m.mk_app(f, new_args.size(), new_args.c_ptr());
-
-        TRACE("t_fpa_detail", tout << "UF call = " << mk_ismt2_pp(res, get_manager()) << "\n";);
-        return res;
-    }
-#endif
-
     expr_ref theory_fpa::convert_conversion_term(expr * e) {
         /* This is for the conversion functions fp.to_* */
         ast_manager & m = get_manager();
@@ -606,6 +618,7 @@ namespace smt {
         // Therefore, we translate and assert them here.
         fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
         switch (k) {
+        case OP_FPA_TO_FP:
         case OP_FPA_TO_UBV:
         case OP_FPA_TO_SBV:
         case OP_FPA_TO_REAL:
@@ -966,4 +979,16 @@ namespace smt {
             out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
         }
     }
+
+    bool theory_fpa::include_func_interp(func_decl * f) {
+        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
+        func_decl * wt;
+
+        if (m_wraps.find(f->get_range(), wt) || m_unwraps.find(f->get_range(), wt))
+            return wt == f;
+        else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f))
+            return false;
+        else
+            return true;
+    }
 };

src/smt/theory_fpa.h

@@ -163,6 +163,7 @@ namespace smt {
         virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+        virtual bool include_func_interp(func_decl * f);
 
         void assign_eh(bool_var v, bool is_true);
         virtual void relevant_eh(app * n);