Fixed and refactored fp.min/fp.max for theory_fpa.

Fixes #616

src/ast/fpa/fpa2bv_converter.cpp

@@ -1156,13 +1156,13 @@ void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args
     SASSERT(is_well_sorted(m, result));
 }
 
-expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
+expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) {
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());
     expr_ref res(m);
 
-    // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
+    // The only cases in which min/max is unspecified for is when the arguments are +0.0 and -0.0.
-    // There is no "hardware interpretation" for fp.min.
+    // There is no "hardware interpretation" for fp.min/fp.max.
 
     std::pair<app*, app*> decls(0, 0);
     if (!m_specials.find(f, decls)) {
@@ -1237,37 +1237,6 @@ void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args
     SASSERT(is_well_sorted(m, result));
 }
 
-expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
-    expr_ref res(m);
-
-    // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
-    // There is no "hardware interpretation" for fp.max.
-
-    std::pair<app*, app*> decls(0, 0);
-    if (!m_specials.find(f, decls)) {
-        decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
-        decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
-        m_specials.insert(f, decls);
-        m.inc_ref(f);
-        m.inc_ref(decls.first);
-        m.inc_ref(decls.second);
-    }
-
-    expr_ref pn(m), np(m);
-    pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
-    np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
-
-    expr_ref x_is_pzero(m), y_is_nzero(m), xyzero(m);
-    mk_is_pzero(x, x_is_pzero);
-    mk_is_nzero(y, y_is_nzero);
-    m_simp.mk_and(x_is_pzero, y_is_nzero, xyzero);
-    mk_ite(xyzero, pn, np, res);
-
-    return res;
-}
-
 void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 4);
     SASSERT(m_util.is_rm_bvwrap(args[0]));

src/ast/fpa/fpa2bv_converter.h

@@ -133,11 +133,10 @@ public:
 
     void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
+    virtual expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
 
     void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
 
     expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
     expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);

src/ast/fpa/fpa2bv_rewriter.cpp

@@ -150,8 +150,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         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;
 
-        case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
+        case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
-        case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
+        case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE;
         case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
         case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
 

src/ast/fpa_decl_plugin.h

@@ -297,7 +297,7 @@ public:
     app * mk_fp(expr * sgn, expr * exp, expr * sig) { 
         SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
         SASSERT(m_bv_util.is_bv(exp));
-        SASSERT(m_bv_util.is_bv(sig));
+        SASSERT(m_bv_util.is_bv(sig));        
         return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); 
     }
     
@@ -383,6 +383,24 @@ public:
     bool is_rm_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP); }
     bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }    
 
+    bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
+    bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
+    bool is_max_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
+    bool is_max_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
+    bool is_to_ubv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
+    bool is_to_sbv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
+    bool is_to_ieee_bv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
+    bool is_to_real_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
+
+    bool is_min_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
+    bool is_min_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
+    bool is_max_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
+    bool is_max_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
+    bool is_to_ubv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
+    bool is_to_sbv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
+    bool is_to_ieee_bv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
+    bool is_to_real_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
+
     bool contains_floats(ast * a);
 };
 

src/smt/theory_fpa.cpp

@@ -87,48 +87,23 @@ namespace smt {
         return fpa2bv_converter::mk_function(f, num, args, result);        
     }
 
-    expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
+    expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) {
-        // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
         unsigned ebits = m_util.get_ebits(f->get_range());
         unsigned sbits = m_util.get_sbits(f->get_range());
         unsigned bv_sz = ebits + sbits;
-        expr_ref res(m);
 
-        expr * args[] = { x, y };
+        expr_ref a(m), wrapped(m), wu(m), wu_eq(m);
-        func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range());
+        a = m.mk_app(f, x, y);
-        expr_ref a(m), wrapped(m);
-        a = m.mk_app(w, x, y);
         wrapped = m_th.wrap(a);
-        res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
+        wu = m_th.unwrap(wrapped, f->get_range());
-                           m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
+        wu_eq = m.mk_eq(wu, a);
-                           m_bv_util.mk_extract(sbits - 2, 0, wrapped));
+        m_extra_assertions.push_back(wu_eq);
 
         expr_ref sc(m);
-        m_th.m_converter.mk_is_zero(res, sc);
+        m_th.m_converter.mk_is_zero(wu, sc);
         m_extra_assertions.push_back(sc);
-        return res;
-    }
 
-    expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
+        return wu;
-        // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
-        unsigned ebits = m_util.get_ebits(f->get_range());
-        unsigned sbits = m_util.get_sbits(f->get_range());
-        unsigned bv_sz = ebits + sbits;
-        expr_ref res(m);
-
-        expr * args[] = { x, y };
-        func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range());
-        expr_ref a(m), wrapped(m);
-        a = m.mk_app(w, x, y);
-        wrapped = m_th.wrap(a);
-        res = m_util.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));
-
-        expr_ref sc(m);
-        m_th.m_converter.mk_is_zero(res, sc);
-        m_extra_assertions.push_back(sc);
-        return res;
     }
 
     theory_fpa::theory_fpa(ast_manager & m) :
@@ -579,13 +554,8 @@ namespace smt {
                 }
             }
             
-            if (!ctx.relevancy()) {
+            if (!ctx.relevancy())
                 relevant_eh(owner);
-                /*expr_ref wu(m);
-                wu = m.mk_eq(unwrap(wrap(owner), s), owner);
-                TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, get_manager()) << std::endl;);
-                assert_cnstr(wu);*/
-            }
         }
     }
 
@@ -798,7 +768,7 @@ namespace smt {
                 " (owner " << (!ctx.e_internalized(owner) ? "not" : "is") <<
                 " internalized)" << std::endl;);
 
-        if (is_app_of(owner, get_family_id(), OP_FPA_FP)) {
+        if (m_fpa_util.is_fp(owner)) {
             SASSERT(to_app(owner)->get_num_args() == 3);
             app_ref a0(m), a1(m), a2(m);
             a0 = to_app(owner->get_arg(0));
@@ -816,7 +786,7 @@ namespace smt {
                   mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
             res = vp;
         }
-        else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP)) {
+        else if (m_fpa_util.is_rm_bvwrap(owner)) {
             SASSERT(to_app(owner)->get_num_args() == 1);
             app_ref a0(m);
             a0 = to_app(owner->get_arg(0));
@@ -905,8 +875,20 @@ namespace smt {
     bool theory_fpa::include_func_interp(func_decl * f) {
         TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);        
         
-        if (f->get_family_id() == get_family_id())
+        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_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);
+                return true;
+            }
             return false;
+        }
         else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f))
             return false;
         else

src/smt/theory_fpa.h

@@ -85,8 +85,7 @@ namespace smt {
             virtual void mk_rm_const(func_decl * f, expr_ref & result);            
             virtual void mk_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);
+            virtual expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
-            virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
         };
 
         class fpa_value_proc : public model_value_proc {
@@ -149,6 +148,7 @@ namespace smt {
         obj_map<sort, func_decl*> m_unwraps;
         obj_map<expr, expr*>      m_conversions;
         bool                      m_is_initialized;
+        obj_hashtable<func_decl>  m_is_added_to_model;
 
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app * atom, bool gate_ctx);