Bug and performance fixes for FP UFs.

src/ast/rewriter/fpa_rewriter.cpp

@@ -100,18 +100,17 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2); st = BR_FAILED; break;
 
     case OP_FPA_INTERNAL_RM:
-        SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
+        SASSERT(num_args == 1);  SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
     case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
     case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
     case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
     case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
         st = BR_FAILED;
-
-    case OP_FPA_INTERNAL_BVWRAP:
-    case OP_FPA_INTERNAL_BVUNWRAP:
-        st = BR_FAILED;
         break;
 
+    case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
+    case OP_FPA_INTERNAL_BVUNWRAP: SASSERT(num_args == 1); st = mk_bvunwrap(args[0], result); break;
+
     default:
         NOT_IMPLEMENTED_YET();
     }
@@ -892,3 +891,42 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
 
     return BR_FAILED;
 }
+
+
+br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
+    if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) {
+        bv_util bu(m());
+        SASSERT(to_app(arg)->get_num_args() == 3);
+        sort_ref fpsrt(m());
+        fpsrt = to_app(arg)->get_decl()->get_range();
+        expr_ref a0(m()), a1(m()), a2(m());
+        a0 = to_app(arg)->get_arg(0);
+        a1 = to_app(arg)->get_arg(1);
+        a2 = to_app(arg)->get_arg(2);
+        if (bu.is_extract(a0) && bu.is_extract(a1) && bu.is_extract(a2)) {
+            unsigned w0 = bu.get_extract_high(a0) - bu.get_extract_low(a0) + 1;
+            unsigned w1 = bu.get_extract_high(a1) - bu.get_extract_low(a1) + 1;
+            unsigned w2 = bu.get_extract_high(a2) - bu.get_extract_low(a2) + 1;
+            unsigned cw = w0 + w1 + w2;
+            if (cw == m_util.get_ebits(fpsrt) + m_util.get_sbits(fpsrt)) {
+                expr_ref aa0(m()), aa1(m()), aa2(m());
+                aa0 = to_app(a0)->get_arg(0);
+                aa1 = to_app(a1)->get_arg(0);
+                aa2 = to_app(a2)->get_arg(0);
+                if (aa0 == aa1 && aa1 == aa2 && bu.get_bv_size(aa0) == cw) {
+                    result = aa0;
+                    return BR_DONE;
+                }
+            }
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status fpa_rewriter::mk_bvunwrap(expr * arg, expr_ref & result) {
+    if (is_app_of(arg, m_util.get_family_id(), OP_FPA_INTERNAL_BVWRAP))
+        result = to_app(arg)->get_arg(0);
+    
+    return BR_FAILED;
+}

src/ast/rewriter/fpa_rewriter.h

@@ -89,6 +89,9 @@ public:
     br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, 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);
+    br_status mk_bvunwrap(expr * arg, expr_ref & result);
 };
 
 #endif

src/smt/theory_fpa.cpp

@@ -84,6 +84,28 @@ namespace smt {
         }
     }
 
+    void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result) {
+        if (m_util.is_float(rng)) {
+            unsigned ebits = m_util.get_ebits(rng);
+            unsigned sbits = m_util.get_sbits(rng);
+            unsigned bv_sz = ebits + sbits;
+
+            app_ref na(m);
+            na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+            mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
+                  m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
+                  m_bv_util.mk_extract(sbits - 2, 0, na),
+                  result);
+        }
+        else if (m_util.is_rm(rng)) {
+            app_ref na(m);
+            na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+            mk_rm(na, result);
+        }
+        else
+            result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+    }
+
     void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
         // TODO: This introduces temporary func_decls that should be filtered in the end.
 
@@ -93,11 +115,13 @@ namespace smt {
         expr_ref_buffer new_args(m);
 
         for (unsigned i = 0; i < num; i++) {
+            TRACE("t_fpa", tout << "UF arg[" << i << "]: " << mk_ismt2_pp(args[i], m) << std::endl; );
             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);
+                TRACE("t_fpa", tout << "UF wrap ai: " << mk_ismt2_pp(ai, m) << " --> " << mk_ismt2_pp(wrapped, m) << std::endl; );
                 m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai));
             }
             else
@@ -105,8 +129,10 @@ namespace smt {
         }
 
         func_decl * fd;
-        if (m_uf2bvuf.find(f, fd))
+        if (m_uf2bvuf.find(f, fd)) {
+            TRACE("t_fpa", tout << "UF reused: " << mk_ismt2_pp(fd, m) << std::endl; );
             mk_uninterpreted_output(f->get_range(), fd, new_args, result);
+        }
         else {
             sort_ref_buffer new_domain(m);
 
@@ -373,6 +399,10 @@ namespace smt {
             res = m.mk_app(w, e);
         }
 
+        TRACE("t_fpa", tout << "e: " << mk_ismt2_pp(e, m) << "\n";
+                       tout << "r: " << mk_ismt2_pp(res, m) << "\n";);
+
+        
         return res;
     }
 
@@ -415,6 +445,9 @@ namespace smt {
         proof_ref pr(m);
         m_rw(e, e_conv);
 
+        TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << "\n";
+                              tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << "\n";);
+
         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);

src/smt/theory_fpa.h

@@ -83,6 +83,7 @@ namespace smt {
             virtual ~fpa2bv_converter_wrapped() {}
             virtual void mk_const(func_decl * f, expr_ref & result);
             virtual void mk_rm_const(func_decl * f, expr_ref & result);
+            void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result);
             virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);            
 
             virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -322,10 +322,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         sort * rng = f->get_range();
 
         if (arity > 0) {
-            func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
-
             func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value);            
-            SASSERT(bv_fi->args_are_values());
+
+            if (bv_fi != 0) {
+                func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
 
                 for (unsigned i = 0; i < bv_fi->num_entries(); i++) {
                     func_entry const * bv_fe = bv_fi->get_entry(i);
@@ -335,19 +335,23 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
                     for (unsigned j = 0; j < arity; j++) {
                         sort * dj = f->get_domain(j);
                         expr * aj = bv_args[j];
+                        expr_ref saj(m);
+                        bv_mdl->eval(aj, saj, true);
+
                         if (fu.is_float(dj))
-                        new_args.push_back(convert_bv2fp(bv_mdl, dj, aj));
+                            new_args.push_back(convert_bv2fp(bv_mdl, dj, saj));
                         else if (fu.is_rm(dj)) {
                             expr_ref fv(m);
-                        fv = convert_bv2rm(aj);
+                            fv = convert_bv2rm(saj);
                             new_args.push_back(fv);
                         }
                         else
-                        new_args.push_back(aj);
+                            new_args.push_back(saj);                        
                     }
 
                     expr_ref ret(m);
                     ret = bv_fe->get_result();
+                    bv_mdl->eval(ret, ret);
                     if (fu.is_float(rng))
                         ret = convert_bv2fp(bv_mdl, rng, ret);
                     else if (fu.is_rm(rng))
@@ -367,6 +371,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 
                 float_mdl->register_decl(f, flt_fi);
             }
+        }
         else {
             func_decl * bvf = it->m_value;
             expr_ref c(m), e(m);