Fix for partially interpreted floating-point functions. Relates to #2596, #2631.

src/ast/fpa/bv2fpa_converter.cpp

@@ -51,11 +51,10 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
     for (auto const& kv : conv.m_uf2bvuf) {
         m_uf2bvuf.insert(kv.m_key, kv.m_value);
         m.inc_ref(kv.m_key);
-        m.inc_ref(kv.m_value.first);
+        m.inc_ref(kv.m_value);
-        m.inc_ref(kv.m_value.second);
     }
     for (auto const& kv : conv.m_min_max_ufs) {
-        m_specials.insert(kv.m_key, kv.m_value);
+        m_min_max_specials.insert(kv.m_key, kv.m_value);
         m.inc_ref(kv.m_key);
         m.inc_ref(kv.m_value.first);
         m.inc_ref(kv.m_value.second);
@@ -67,16 +66,15 @@ bv2fpa_converter::~bv2fpa_converter() {
     dec_ref_map_key_values(m, m_rm_const2bv);
     for (auto const& kv : m_uf2bvuf) {
         m.dec_ref(kv.m_key);
-        m.dec_ref(kv.m_value.first);
+        m.dec_ref(kv.m_value);
-        m.dec_ref(kv.m_value.second);
     }
-    for (auto const& kv : m_specials) {
+    for (auto const& kv : m_min_max_specials) {
         m.dec_ref(kv.m_key);
         m.dec_ref(kv.m_value.first);
         m.dec_ref(kv.m_value.second);
     }
     m_uf2bvuf.reset();
-    m_specials.reset();
+    m_min_max_specials.reset();
 }
 
 expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
@@ -191,7 +189,7 @@ expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, expr * val) {
 
 expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) {
     expr_ref result(m);
-    TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
+    TRACE("bv2fpa_rebuild", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
                     if (e) tout << mk_ismt2_pp(e, m);
                     else tout << "nil";
                     tout << std::endl; );
@@ -288,13 +286,23 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
             expr_ref ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
             m_th_rw(ft_fres);
             TRACE("bv2fpa",
+                  tout << "func_interp entry #" << i << ":" << std::endl;
+                  tout << "(" << bv_f->get_name();
+                  for (unsigned i = 0; i < bv_f->get_arity(); i++)
+                      tout << " " << mk_ismt2_pp(bv_args[i], m);
+                  tout << ") = " << mk_ismt2_pp(bv_fres, m) << std::endl;
+                  tout << " --> " << std::endl;
+                  tout << "(" << f->get_name();
                   for (unsigned i = 0; i < new_args.size(); i++)
-                      tout << mk_ismt2_pp(bv_args[i], m) << " == " <<
+                      tout << " " << mk_ismt2_pp(new_args[i], m);
-                        mk_ismt2_pp(new_args[i], m) << std::endl;
+                  tout << ") = " << mk_ismt2_pp(ft_fres, m) << std::endl;);
-                  tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
             func_entry * fe = result->get_entry(new_args.c_ptr());
-            if (fe == nullptr)
+            if (fe == nullptr) {
-                result->insert_new_entry(new_args.c_ptr(), ft_fres);
+                // Avoid over-specification of a partially interpreted theory function
+                if (f->get_family_id() != m_fpa_util.get_family_id() ||
+                    m_fpa_util.is_considered_uninterpreted(f, new_args.size(), new_args.c_ptr()))
+                    result->insert_new_entry(new_args.c_ptr(), ft_fres);
+            }
             else {
                 // The BV model may have multiple equivalent entries using different
                 // representations of NaN. We can only keep one and we check that
@@ -309,6 +317,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
         if (bv_els) {
             expr_ref ft_els = rebuild_floats(mc, rng, bv_els);
             m_th_rw(ft_els);
+            TRACE("bv2fpa", tout << "else=" << mk_ismt2_pp(ft_els, m) << std::endl;);
             result->set_else(ft_els);
         }
     }
@@ -398,7 +407,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
 }
 
 void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
-    for (auto const& kv : m_specials) {
+    for (auto const& kv : m_min_max_specials) {
         func_decl * f = kv.m_key;
         app * pn_cnst = kv.m_value.first;
         app * np_cnst = kv.m_value.second;
@@ -432,8 +441,7 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
 void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
     for (auto const& kv : m_uf2bvuf) {
         func_decl * f = kv.m_key;
-        func_decl* f_uf = kv.m_value.first;
+        func_decl * f_uf = kv.m_value;
-        expr*      f_def = kv.m_value.second;
         seen.insert(f_uf);
 
         if (f->get_arity() == 0)
@@ -454,29 +462,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
             }
         }
         else if (f->get_family_id() == m_fpa_util.get_fid()) {
-            if (f_def) {
+            // kv.m_value contains the model for the unspecified cases of kv.m_key in terms of bit-vectors.
-                func_interp* fi = alloc(func_interp, m, f->get_arity());
+            // convert_func_interp rebuilds a func_interp on floats.
-                expr_ref def = rebuild_floats(mc, f->get_range(), to_app(f_def));
-                fi->set_else(def);
-                SASSERT(m.get_sort(def) == f->get_range());
-                target_model->register_decl(f, fi);
-                func_interp* fj = mc->get_func_interp(f_uf);
-                if (fj) {
-                    target_model->register_decl(f_uf, fj->copy());
-                }
-                continue;
-            }
-
 
             //  f is a floating point function: f(x,y) : Float
             //  f_uf is a bit-vector function: f_uf(xB,yB) : BitVec
             //  then there is f_def: f_Bv(xB, yB) := if(range(xB),.., f_uf(xB,yB))
             //  f(x,y) := to_float(if(range(to_bv(x)), ... f_uf(to_bv(xB), to_bv(yB)))) - not practical
-            //         := if(range_fp(x), ...., to_float(f_uf(...))                     - approach
+            //         := if(range_fp(x), ...., to_float(f_uf(...))                     - approach (via fpa_util::is_considered_uninterpreted)
-                                                               
+
-            target_model->register_decl(f, convert_func_interp(mc, f, f_uf));            
+            func_interp *fi = convert_func_interp(mc, f, f_uf);
+            if (fi->num_entries() > 0 || fi->get_else() != nullptr)
+                target_model->register_decl(f, fi);
         }
     }
+
+    TRACE("bv2fpa", tout << "Target model: " << *target_model; );
 }
 
 void bv2fpa_converter::display(std::ostream & out) {
@@ -496,9 +497,9 @@ void bv2fpa_converter::display(std::ostream & out) {
         const symbol & n = kv.m_key->get_name();
         out << "\n  (" << n << " ";
         unsigned indent = n.size() + 4;
-        out << mk_ismt2_pp(kv.m_value.first, m, indent) << ")";
+        out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
     }
-    for (auto const& kv : m_specials) {
+    for (auto const& kv : m_min_max_specials) {
         const symbol & n = kv.m_key->get_name();
         out << "\n  (" << n << " ";
         unsigned indent = n.size() + 4;
@@ -525,22 +526,19 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
     }
     for (auto const& kv : m_uf2bvuf) {
         func_decl * k = translator(kv.m_key);
-        func_decl * v = translator(kv.m_value.first);
+        func_decl * v = translator(kv.m_value);
-        expr*       d = translator(kv.m_value.second);
+        res->m_uf2bvuf.insert(k, v);
-        res->m_uf2bvuf.insert(k, std::make_pair(v, d));
         translator.to().inc_ref(k);
         translator.to().inc_ref(v);
-        translator.to().inc_ref(d);
     }
-    for (auto const& kv : m_specials) {
+    for (auto const& kv : m_min_max_specials) {
         func_decl * k = translator(kv.m_key);
         app * v1 = translator(kv.m_value.first);
         app * v2 = translator(kv.m_value.second);
-        res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
+        res->m_min_max_specials.insert(k, std::pair<app*, app*>(v1, v2));
         translator.to().inc_ref(k);
         translator.to().inc_ref(v1);
         translator.to().inc_ref(v2);
     }
     return res;
 }
-

src/ast/fpa/bv2fpa_converter.h

@@ -34,8 +34,8 @@ class bv2fpa_converter {
 
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
-    obj_map<func_decl, std::pair<func_decl*, expr*>>  m_uf2bvuf;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;
-    obj_map<func_decl, std::pair<app*, app*> > m_specials;
+    obj_map<func_decl, std::pair<app*, app*> > m_min_max_specials;
 
 public:
     bv2fpa_converter(ast_manager & m);

src/ast/fpa/fpa2bv_converter.cpp

@@ -3203,7 +3203,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
 
     expr_ref sgn(m), sig(m), exp(m), lz(m);
     unpack(x, sgn, sig, exp, lz, true);
-    
 
     unsigned ebits = m_util.get_ebits(xs);
     unsigned sbits = m_util.get_sbits(xs);
@@ -4166,8 +4165,7 @@ void fpa2bv_converter::reset() {
     dec_ref_map_key_values(m, m_rm_const2bv);
     for (auto const& kv : m_uf2bvuf) {
         m.dec_ref(kv.m_key);
-        m.dec_ref(kv.m_value.first);
+        m.dec_ref(kv.m_value);
-        m.dec_ref(kv.m_value.second);
     }
     for (auto const& kv : m_min_max_ufs) {
         m.dec_ref(kv.m_key);
@@ -4180,36 +4178,13 @@ void fpa2bv_converter::reset() {
 }
 
 func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
-    std::pair<func_decl*, expr*> res;
+    func_decl* res;
     if (!m_uf2bvuf.find(f, res)) {
-        res.first = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
+        res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
-        res.second = nullptr;
         m.inc_ref(f);
-        m.inc_ref(res.first);
+        m.inc_ref(res);
         m_uf2bvuf.insert(f, res);
-        TRACE("fpa2bv", tout << "New UF func_decl: " << res.first->get_id() << std::endl << mk_ismt2_pp(res.first, m) << std::endl;);
+        TRACE("fpa2bv", tout << "New UF func_decl: " << res->get_id() << std::endl << mk_ismt2_pp(res, m) << std::endl;);
     }
-    return res.first;
+    return res;
-}
-
-expr* fpa2bv_converter::get_bv_def(func_decl* f) {
-    std::pair<func_decl*, expr*> res(nullptr, nullptr);
-    m_uf2bvuf.find(f, res);
-    TRACE("fpa2bv", tout << "get_bv_def " << mk_ismt2_pp(res.first, m) << " " << res.second << std::endl;);
-    return res.second;
-}
-
-/**
-   \brief expand the definition of bit-vector function f
-   as an expression of what is defined and what is not
-   defined.
-*/
-void fpa2bv_converter::set_bv_def(func_decl* f, expr* def) {
-    auto res = m_uf2bvuf[f];
-    SASSERT(res.first);
-    SASSERT(!res.second);
-    res.second = def;
-    m.inc_ref(def);
-    m_uf2bvuf.insert(f, res);
-
 }

src/ast/fpa/fpa2bv_converter.h

@@ -35,7 +35,7 @@ class fpa2bv_converter {
 public:
     typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
     typedef obj_map<func_decl, expr*> const2bv_t;
-    typedef obj_map<func_decl, std::pair<func_decl*, expr*> > uf2bvuf_t;
+    typedef obj_map<func_decl, func_decl*> uf2bvuf_t;
 
 protected:
     ast_manager              & m;
@@ -219,8 +219,6 @@ private:
     void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
 
     func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
-    void set_bv_def(func_decl * f, expr* def);
-    expr* get_bv_def(func_decl * f);
 
     expr_ref nan_wrap(expr * n);
 

src/ast/fpa_decl_plugin.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
+#include "ast/ast_smt2_pp.h"
 
 fpa_decl_plugin::fpa_decl_plugin():
     m_values(m_fm),
@@ -68,6 +69,10 @@ void fpa_decl_plugin::recycled_id(unsigned id) {
     m_fm.del(m_values[id]);
 }
 
+bool fpa_decl_plugin::is_considered_uninterpreted(func_decl * f) {
+    return false;
+}
+
 func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
     sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
     func_decl * r = nullptr;
@@ -1044,3 +1049,44 @@ bool fpa_util::contains_floats(ast * a) {
 
     return false;
 }
+
+bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) {
+    TRACE("fpa_util", expr_ref t(m().mk_app(f, n, args), m()); tout << mk_ismt2_pp(t, m()) << std::endl; );
+
+    family_id ffid = plugin().get_family_id();
+    if (f->get_family_id() != ffid)
+        return false;
+
+    if (is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV)) {
+        SASSERT(n == 1);
+        expr* x = args[0];
+        return is_nan(x);
+    }
+    else if (is_decl_of(f, ffid, OP_FPA_TO_SBV) ||
+             is_decl_of(f, ffid, OP_FPA_TO_UBV)) {
+        SASSERT(n == 2);
+        SASSERT(f->get_num_parameters() == 1);
+        bool is_signed = f->get_decl_kind() == OP_FPA_TO_SBV;
+        expr* rm = args[0];
+        expr* x = args[1];
+        unsigned bv_sz = f->get_parameter(0).get_int();
+        mpf_rounding_mode rmv;
+        mpf v;
+        if (!is_rm_numeral(rm, rmv) || !is_numeral(x, v)) return false;
+        if (is_nan(x) || is_inf(x)) return true;
+        unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager();
+        scoped_mpq r(mpqm);
+        plugin().fm().to_sbv_mpq(rmv, v, r);
+        if (is_signed)
+            return mpqm.bitsize(r) >= bv_sz;
+        else
+            return mpqm.is_neg(r) || mpqm.bitsize(r) > bv_sz;
+    }
+    else if (is_decl_of(f, ffid, OP_FPA_TO_REAL)) {
+        SASSERT(n == 1);
+        expr* x = args[0];
+        return is_nan(x) || is_inf(x);
+    }
+
+    return plugin().is_considered_uninterpreted(f);
+}

src/ast/fpa_decl_plugin.h

@@ -163,8 +163,6 @@ class fpa_decl_plugin : public decl_plugin {
     unsigned mk_id(mpf const & v);
     void recycled_id(unsigned id);
 
-    bool is_considered_uninterpreted(func_decl * f) override { return false; }
-
 public:
     fpa_decl_plugin();
 
@@ -199,6 +197,8 @@ public:
 
     void del(parameter const & p) override;
     parameter translate(parameter const & p, decl_plugin & target) override;
+
+    bool is_considered_uninterpreted(func_decl * f) override;
 };
 
 class fpa_util {
@@ -358,6 +358,8 @@ public:
 
     bool contains_floats(ast * a);
 
+    bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args);
+
     MATCH_TERNARY(is_fp);
 };
 

src/model/model_evaluator.cpp

@@ -53,6 +53,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     seq_rewriter                    m_seq_rw;
     array_util                      m_ar;
     arith_util                      m_au;
+    fpa_util                        m_fpau;
     unsigned long long              m_max_memory;
     unsigned                        m_max_steps;
     bool                            m_model_completion;
@@ -78,6 +79,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_seq_rw(m),
         m_ar(m),
         m_au(m),
+        m_fpau(m),
         m_pinned(m) {
         bool flat = true;
         m_b_rw.set_flat(flat);
@@ -132,9 +134,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return false;
     }
 
-    bool reduce_quantifier(quantifier * old_q, 
+    bool reduce_quantifier(quantifier * old_q,
-                           expr * new_body, 
+                           expr * new_body,
-                           expr * const * new_patterns, 
+                           expr * const * new_patterns,
                            expr * const * new_no_patterns,
                            expr_ref & result,
                            proof_ref & result_pr) {
@@ -148,7 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         family_id fid = f->get_family_id();
         bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
-        TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";);        
+        TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";);
         if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
@@ -195,8 +197,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     result = m.mk_false();
                     st = BR_DONE;
                 }
-                TRACE("model_evaluator", 
+                TRACE("model_evaluator",
-                      tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " " 
+                      tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " "
                       << mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";);
                 if (st != BR_FAILED)
                     return st;
@@ -324,7 +326,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
         result = nullptr;
         result_pr = nullptr;
 
+        if (f->get_family_id() == m_fpau.get_family_id() &&
+            !m_fpau.is_considered_uninterpreted(f, num, args)) {
+            // cwinter: should this be unreachable?
+            return BR_FAILED;
+        }
+
         func_interp * fi = m_model.get_func_interp(f);
+
         if (fi) {
             if (fi->is_partial())
                 fi->set_else(m.get_some_value(f->get_range()));
@@ -338,6 +347,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
             result = m_au.mk_numeral(rational(0), f->get_range());
             return BR_DONE;
         }
+        else if (m_fpau.is_considered_uninterpreted(f, num, args)) {
+            result = m.get_some_value(f->get_range());
+            return BR_DONE;
+        }
         return BR_FAILED;
     }
 
@@ -524,7 +537,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
         func_interp* g = m_model.get_func_interp(f);
-        if (!g) return false;        
+        if (!g) return false;
         else_case = g->get_else();
         if (!else_case) {
             TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);