FPA refactoring in preparation for FPA support in the kernel.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

scripts/mk_project.py

@@ -42,17 +42,18 @@ def init_project_def():
     # Simplifier module will be deleted in the future.
     # It has been replaced with rewriter module.
     add_lib('simplifier', ['rewriter'], 'ast/simplifier')
+    add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa')
     add_lib('macros', ['simplifier'], 'ast/macros')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
     add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
     add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
     add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
-                    'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
+                    'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
     add_lib('user_plugin', ['smt'], 'smt/user_plugin')
     add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
-    add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
     add_lib('qe', ['smt','sat'], 'qe')
@@ -68,7 +69,7 @@ def init_project_def():
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp')
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
-    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
 #    add_dll('foci2', ['util'], 'interp/foci2stub', 
 #            dll_name='foci2', 

src/ast/fpa/fpa2bv_converter.cpp

@@ -2754,215 +2754,3 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
 
     TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
 }
-
-void fpa2bv_model_converter::display(std::ostream & out) {
-    out << "(fpa2bv-model-converter";
-    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
-         it != m_const2bv.end();
-         it++) {
-             const symbol & n = it->m_key->get_name();
-             out << "\n  (" << n << " ";
-             unsigned indent = n.size() + 4;
-             out << mk_ismt2_pp(it->m_value, m, indent) << ")";
-    }
-    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
-         it != m_rm_const2bv.end();
-         it++) {
-             const symbol & n = it->m_key->get_name();
-             out << "\n  (" << n << " ";
-             unsigned indent = n.size() + 4;
-             out << mk_ismt2_pp(it->m_value, m, indent) << ")";
-    }
-    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
-         it != m_uf2bvuf.end();
-         it++) {
-             const symbol & n = it->m_key->get_name();
-             out << "\n  (" << n << " ";
-             unsigned indent = n.size() + 4;
-             out << mk_ismt2_pp(it->m_value, m, indent) << ")";
-    }
-    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-         it != m_uf23bvuf.end();
-         it++) {
-             const symbol & n = it->m_key->get_name();
-             out << "\n  (" << n << " ";
-             unsigned indent = n.size() + 4;
-             out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " << 
-             mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " << 
-             mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
-             ")";
-    }
-    out << ")" << std::endl;
-}
-
-model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
-    fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
-    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
-         it != m_const2bv.end();
-         it++)
-    {
-        func_decl * k = translator(it->m_key);
-        expr * v = translator(it->m_value);
-        res->m_const2bv.insert(k, v);
-        translator.to().inc_ref(k);
-        translator.to().inc_ref(v);
-    }
-    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
-         it != m_rm_const2bv.end();
-         it++)
-    {
-        func_decl * k = translator(it->m_key);
-        expr * v = translator(it->m_value);
-        res->m_rm_const2bv.insert(k, v);
-        translator.to().inc_ref(k);
-        translator.to().inc_ref(v);        
-    }
-    return res;
-}
-
-void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
-    float_util fu(m);
-    bv_util bu(m);
-    mpf fp_val;
-    unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
-    unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
-
-    TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
-        for (unsigned i = 0 ; i < bv_mdl->get_num_constants(); i++)
-            tout << bv_mdl->get_constant(i)->get_name() << " --> " << 
-                mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
-        );
-    
-    obj_hashtable<func_decl> seen;
-
-    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
-         it != m_const2bv.end();
-         it++) 
-    {
-        func_decl * var = it->m_key;
-        app * a = to_app(it->m_value);
-        SASSERT(fu.is_float(var->get_range()));
-        SASSERT(var->get_range()->get_num_parameters() == 2);
-        
-        unsigned ebits = fu.get_ebits(var->get_range());
-        unsigned sbits = fu.get_sbits(var->get_range());
-
-        expr_ref sgn(m), sig(m), exp(m);
-        sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
-        sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
-        exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
-
-        seen.insert(to_app(a->get_arg(0))->get_decl());
-        seen.insert(to_app(a->get_arg(1))->get_decl());
-        seen.insert(to_app(a->get_arg(2))->get_decl());
-
-        if (!sgn && !sig && !exp)
-            continue;
-        
-        unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));
-        unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1;
-        unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2)));
-
-        rational sgn_q(0), sig_q(0), exp_q(0);
-
-        if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
-        if (sig) bu.is_numeral(sig, sig_q, sig_sz);
-        if (exp) bu.is_numeral(exp, exp_q, exp_sz);        
-
-        // un-bias exponent
-        rational exp_unbiased_q;
-        exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits-1);
-        
-        mpz sig_z; mpf_exp_t exp_z;
-        mpzm.set(sig_z, sig_q.to_mpq().numerator());
-        exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
-
-        TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " << 
-            mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl; );
-        
-        fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
-
-        float_mdl->register_decl(var, fu.mk_value(fp_val));
-        
-        mpzm.del(sig_z);
-    }
-
-    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
-         it != m_rm_const2bv.end();
-         it++) 
-    {
-        func_decl * var = it->m_key;
-        app * a = to_app(it->m_value);
-        SASSERT(fu.is_rm(var->get_range()));        
-        rational val(0);
-        unsigned sz = 0;
-        if (a && bu.is_numeral(a, val, sz)) {
-            TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; );
-            SASSERT(val.is_uint64());
-            switch (val.get_uint64())
-            {
-            case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
-            case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
-            case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
-            case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
-            case BV_RM_TO_ZERO: 
-            default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
-            }
-            seen.insert(var);
-        }        
-    }
-
-    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
-         it != m_uf2bvuf.end();
-         it++) 
-        seen.insert(it->m_value);
-
-    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-         it != m_uf23bvuf.end();
-         it++) 
-    {
-        seen.insert(it->m_value.f_sgn);
-        seen.insert(it->m_value.f_sig);
-        seen.insert(it->m_value.f_exp);
-    }
-
-    fu.fm().del(fp_val);
-
-    // Keep all the non-float constants.
-    unsigned sz = bv_mdl->get_num_constants();
-    for (unsigned i = 0; i < sz; i++)
-    {
-        func_decl * c = bv_mdl->get_constant(i);
-        if (!seen.contains(c))
-            float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
-    }
-
-    // And keep everything else
-    sz = bv_mdl->get_num_functions();
-    for (unsigned i = 0; i < sz; i++)
-    {
-        func_decl * f = bv_mdl->get_function(i);
-        if (!seen.contains(f))
-        {
-            TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; );
-            func_interp * val = bv_mdl->get_func_interp(f);
-            float_mdl->register_decl(f, val);
-        }
-    }
-
-    sz = bv_mdl->get_num_uninterpreted_sorts();
-    for (unsigned i = 0; i < sz; i++)
-    {
-        sort * s = bv_mdl->get_uninterpreted_sort(i);
-        ptr_vector<expr> u = bv_mdl->get_universe(s);
-        float_mdl->register_usort(s, u.size(), u.c_ptr());
-    }
-}
-
-model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
-                                            obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv,
-                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
-                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
-    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
-}

src/ast/fpa/fpa2bv_converter.h

@@ -24,13 +24,10 @@ Notes:
 #include"ref_util.h"
 #include"float_decl_plugin.h"
 #include"bv_decl_plugin.h"
-#include"model_converter.h"
 #include"basic_simplifier_plugin.h"
 
 typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2, BV_RM_TO_POSITIVE=3, BV_RM_TO_ZERO=4 } BV_RM_VAL;
 
-class fpa2bv_model_converter;
-
 struct func_decl_triple {
         func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
         func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
@@ -173,86 +170,4 @@ protected:
         expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
 };
 
-
-class fpa2bv_model_converter : public model_converter {
-    ast_manager               & m;
-    obj_map<func_decl, expr*>   m_const2bv;
-    obj_map<func_decl, expr*>   m_rm_const2bv;
-    obj_map<func_decl, func_decl*>  m_uf2bvuf;        
-    obj_map<func_decl, func_decl_triple>  m_uf23bvuf;
-
-public:
-    fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv,
-                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
-                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) : 
-      m(m) {
-          // Just create a copy?
-          for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
-               it != const2bv.end();
-               it++) 
-          {
-               m_const2bv.insert(it->m_key, it->m_value);
-               m.inc_ref(it->m_key);
-               m.inc_ref(it->m_value);
-          }
-          for (obj_map<func_decl, expr*>::iterator it = rm_const2bv.begin();
-               it != rm_const2bv.end();
-               it++) 
-          {
-               m_rm_const2bv.insert(it->m_key, it->m_value);
-               m.inc_ref(it->m_key);
-               m.inc_ref(it->m_value);
-          }
-          for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
-               it != uf2bvuf.end();
-               it++) 
-          {
-               m_uf2bvuf.insert(it->m_key, it->m_value);
-               m.inc_ref(it->m_key);
-               m.inc_ref(it->m_value);
-          }
-          for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
-               it != uf23bvuf.end();
-               it++) 
-          {
-               m_uf23bvuf.insert(it->m_key, it->m_value);
-               m.inc_ref(it->m_key);               
-          }
-      }
-
-    virtual ~fpa2bv_model_converter() {
-        dec_ref_map_key_values(m, m_const2bv);
-        dec_ref_map_key_values(m, m_rm_const2bv);
-    }
-
-    virtual void operator()(model_ref & md, unsigned goal_idx) {
-        SASSERT(goal_idx == 0);
-        model * new_model = alloc(model, m);
-        obj_hashtable<func_decl> bits;
-        convert(md.get(), new_model);
-        md = new_model;
-    }
-
-    virtual void operator()(model_ref & md) {
-        operator()(md, 0);
-    }
-
-    void display(std::ostream & out);
-
-    virtual model_converter * translate(ast_translation & translator);
-
-protected:
-    fpa2bv_model_converter(ast_manager & m) : m(m) { }
-    
-    void convert(model * bv_mdl, model * float_mdl);
-};
-
-
-model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
-                                            obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv,
-                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
-                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf);
-
 #endif

src/smt/theory_fpa.cpp

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    theory_fpa.cpp
+
+Abstract:
+
+    Floating-Point Theory Plugin
+
+Author:
+
+    Christoph (cwinter) 2014-04-23
+
+Revision History:
+
+--*/
+#include"ast_smt2_pp.h"
+#include"theory_fpa.h"
+
+namespace smt {
+
+    bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
+        TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
+        SASSERT(atom->get_family_id() == get_family_id());
+        NOT_IMPLEMENTED_YET();
+        return true;
+    }
+
+    void theory_fpa::new_eq_eh(theory_var, theory_var) {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    void theory_fpa::new_diseq_eh(theory_var, theory_var) {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    void theory_fpa::push_scope_eh() {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    void theory_fpa::pop_scope_eh(unsigned num_scopes) {
+        NOT_IMPLEMENTED_YET();
+    }
+};

src/smt/theory_fpa.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    theory_fpa.h
+
+Abstract:
+
+    Floating-Point Theory Plugin
+
+Author:
+
+    Christoph (cwinter) 2014-04-23
+
+Revision History:
+
+--*/
+#ifndef _THEORY_FPA_H_
+#define _THEORY_FPA_H_
+
+#include"smt_theory.h"
+#include"fpa2bv_converter.h"
+
+namespace smt {
+    class theory_fpa : public theory {
+        fpa2bv_converter m_converter;
+
+        virtual final_check_status final_check_eh() { return FC_DONE; }
+        virtual bool internalize_atom(app*, bool);
+        virtual bool internalize_term(app*) { return internalize_atom(0, false); }
+        virtual void new_eq_eh(theory_var, theory_var);
+        virtual void new_diseq_eh(theory_var, theory_var);
+        virtual void push_scope_eh();
+        virtual void pop_scope_eh(unsigned num_scopes);
+        virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
+        virtual char const * get_name() const { return "fpa"; }
+    public:
+        theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {}
+    };
+
+};
+
+#endif /* _THEORY_FPA_H_ */
+

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -0,0 +1,232 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    fpa2bv_model_converter.h
+
+Abstract:
+
+    Model conversion for fpa2bv_converter
+
+Author:
+
+    Christoph (cwinter) 2012-02-09
+
+Notes:
+
+--*/
+#include"ast_smt2_pp.h"
+#include"fpa2bv_model_converter.h"
+
+void fpa2bv_model_converter::display(std::ostream & out) {
+    out << "(fpa2bv-model-converter";
+    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
+         it != m_const2bv.end();
+         it++) {
+        const symbol & n = it->m_key->get_name();
+        out << "\n  (" << n << " ";
+        unsigned indent = n.size() + 4;
+        out << mk_ismt2_pp(it->m_value, m, indent) << ")";
+    }
+    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
+         it != m_rm_const2bv.end();
+         it++) {
+        const symbol & n = it->m_key->get_name();
+        out << "\n  (" << n << " ";
+        unsigned indent = n.size() + 4;
+        out << mk_ismt2_pp(it->m_value, m, indent) << ")";
+    }
+    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
+         it != m_uf2bvuf.end();
+         it++) {
+        const symbol & n = it->m_key->get_name();
+        out << "\n  (" << n << " ";
+        unsigned indent = n.size() + 4;
+        out << mk_ismt2_pp(it->m_value, m, indent) << ")";
+    }
+    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
+         it != m_uf23bvuf.end();
+         it++) {
+        const symbol & n = it->m_key->get_name();
+        out << "\n  (" << n << " ";
+        unsigned indent = n.size() + 4;
+        out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " <<
+            mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
+            mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
+            ")";
+    }
+    out << ")" << std::endl;
+}
+
+model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
+    fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
+    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
+         it != m_const2bv.end();
+         it++)
+    {
+        func_decl * k = translator(it->m_key);
+        expr * v = translator(it->m_value);
+        res->m_const2bv.insert(k, v);
+        translator.to().inc_ref(k);
+        translator.to().inc_ref(v);
+    }
+    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
+         it != m_rm_const2bv.end();
+         it++)
+    {
+        func_decl * k = translator(it->m_key);
+        expr * v = translator(it->m_value);
+        res->m_rm_const2bv.insert(k, v);
+        translator.to().inc_ref(k);
+        translator.to().inc_ref(v);
+    }
+    return res;
+}
+
+void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
+    float_util fu(m);
+    bv_util bu(m);
+    mpf fp_val;
+    unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
+    unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
+
+    TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
+    for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)
+        tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
+        mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
+    );
+
+    obj_hashtable<func_decl> seen;
+
+    for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
+         it != m_const2bv.end();
+         it++)
+    {
+        func_decl * var = it->m_key;
+        app * a = to_app(it->m_value);
+        SASSERT(fu.is_float(var->get_range()));
+        SASSERT(var->get_range()->get_num_parameters() == 2);
+
+        unsigned ebits = fu.get_ebits(var->get_range());
+        unsigned sbits = fu.get_sbits(var->get_range());
+
+        expr_ref sgn(m), sig(m), exp(m);
+        sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
+        sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
+        exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
+
+        seen.insert(to_app(a->get_arg(0))->get_decl());
+        seen.insert(to_app(a->get_arg(1))->get_decl());
+        seen.insert(to_app(a->get_arg(2))->get_decl());
+
+        if (!sgn && !sig && !exp)
+            continue;
+
+        unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));
+        unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1;
+        unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2)));
+
+        rational sgn_q(0), sig_q(0), exp_q(0);
+
+        if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
+        if (sig) bu.is_numeral(sig, sig_q, sig_sz);
+        if (exp) bu.is_numeral(exp, exp_q, exp_sz);
+
+        // un-bias exponent
+        rational exp_unbiased_q;
+        exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits - 1);
+
+        mpz sig_z; mpf_exp_t exp_z;
+        mpzm.set(sig_z, sig_q.to_mpq().numerator());
+        exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
+
+        TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " <<
+              mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl;);
+
+        fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
+
+        float_mdl->register_decl(var, fu.mk_value(fp_val));
+
+        mpzm.del(sig_z);
+    }
+
+    for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
+         it != m_rm_const2bv.end();
+         it++)
+    {
+        func_decl * var = it->m_key;
+        app * a = to_app(it->m_value);
+        SASSERT(fu.is_rm(var->get_range()));
+        rational val(0);
+        unsigned sz = 0;
+        if (a && bu.is_numeral(a, val, sz)) {
+            TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl;);
+            SASSERT(val.is_uint64());
+            switch (val.get_uint64())
+            {
+            case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
+            case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
+            case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
+            case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
+            case BV_RM_TO_ZERO:
+            default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
+            }
+            seen.insert(var);
+        }
+    }
+
+    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
+         it != m_uf2bvuf.end();
+         it++)
+         seen.insert(it->m_value);
+
+    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
+         it != m_uf23bvuf.end();
+         it++)
+    {
+        seen.insert(it->m_value.f_sgn);
+        seen.insert(it->m_value.f_sig);
+        seen.insert(it->m_value.f_exp);
+    }
+
+    fu.fm().del(fp_val);
+
+    // Keep all the non-float constants.
+    unsigned sz = bv_mdl->get_num_constants();
+    for (unsigned i = 0; i < sz; i++)
+    {
+        func_decl * c = bv_mdl->get_constant(i);
+        if (!seen.contains(c))
+            float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
+    }
+
+    // And keep everything else
+    sz = bv_mdl->get_num_functions();
+    for (unsigned i = 0; i < sz; i++)
+    {
+        func_decl * f = bv_mdl->get_function(i);
+        if (!seen.contains(f))
+        {
+            TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
+            func_interp * val = bv_mdl->get_func_interp(f);
+            float_mdl->register_decl(f, val);
+        }
+    }
+
+    sz = bv_mdl->get_num_uninterpreted_sorts();
+    for (unsigned i = 0; i < sz; i++)
+    {
+        sort * s = bv_mdl->get_uninterpreted_sort(i);
+        ptr_vector<expr> u = bv_mdl->get_universe(s);
+        float_mdl->register_usort(s, u.size(), u.c_ptr());
+    }
+}
+
+model_converter * mk_fpa2bv_model_converter(ast_manager & m,
+                                            obj_map<func_decl, expr*> const & const2bv,
+                                            obj_map<func_decl, expr*> const & rm_const2bv,
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf,
+                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
+    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
+}

src/tactic/fpa/fpa2bv_model_converter.h

@@ -0,0 +1,106 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    fpa2bv_model_converter.h
+
+Abstract:
+
+    Model conversion for fpa2bv_converter
+
+Author:
+
+    Christoph (cwinter) 2012-02-09
+
+Notes:
+
+--*/
+#ifndef _FPA2BV_MODEL_CONVERTER_H_
+#define _FPA2BV_MODEL_CONVERTER_H_
+
+#include"fpa2bv_converter.h"
+#include"model_converter.h"
+
+class fpa2bv_model_converter : public model_converter {
+    ast_manager               & m;
+    obj_map<func_decl, expr*>   m_const2bv;
+    obj_map<func_decl, expr*>   m_rm_const2bv;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;
+    obj_map<func_decl, func_decl_triple>  m_uf23bvuf;
+
+public:
+    fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
+                           obj_map<func_decl, expr*> const & rm_const2bv,
+                           obj_map<func_decl, func_decl*> const & uf2bvuf,
+                           obj_map<func_decl, func_decl_triple> const & uf23bvuf) :
+                           m(m) {
+        // Just create a copy?
+        for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
+             it != const2bv.end();
+             it++)
+        {
+            m_const2bv.insert(it->m_key, it->m_value);
+            m.inc_ref(it->m_key);
+            m.inc_ref(it->m_value);
+        }
+        for (obj_map<func_decl, expr*>::iterator it = rm_const2bv.begin();
+             it != rm_const2bv.end();
+             it++)
+        {
+            m_rm_const2bv.insert(it->m_key, it->m_value);
+            m.inc_ref(it->m_key);
+            m.inc_ref(it->m_value);
+        }
+        for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
+             it != uf2bvuf.end();
+             it++)
+        {
+            m_uf2bvuf.insert(it->m_key, it->m_value);
+            m.inc_ref(it->m_key);
+            m.inc_ref(it->m_value);
+        }
+        for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
+             it != uf23bvuf.end();
+             it++)
+        {
+            m_uf23bvuf.insert(it->m_key, it->m_value);
+            m.inc_ref(it->m_key);
+        }
+    }
+
+    virtual ~fpa2bv_model_converter() {
+        dec_ref_map_key_values(m, m_const2bv);
+        dec_ref_map_key_values(m, m_rm_const2bv);
+    }
+
+    virtual void operator()(model_ref & md, unsigned goal_idx) {
+        SASSERT(goal_idx == 0);
+        model * new_model = alloc(model, m);
+        obj_hashtable<func_decl> bits;
+        convert(md.get(), new_model);
+        md = new_model;
+    }
+
+    virtual void operator()(model_ref & md) {
+        operator()(md, 0);
+    }
+
+    void display(std::ostream & out);
+
+    virtual model_converter * translate(ast_translation & translator);
+
+protected:
+    fpa2bv_model_converter(ast_manager & m) : m(m) { }
+
+    void convert(model * bv_mdl, model * float_mdl);
+};
+
+
+model_converter * mk_fpa2bv_model_converter(ast_manager & m,
+                                            obj_map<func_decl, expr*> const & const2bv,
+                                            obj_map<func_decl, expr*> const & rm_const2bv,
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf,
+                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf);
+
+#endif

src/tactic/fpa/fpa2bv_tactic.cpp

@@ -20,6 +20,7 @@ Notes:
 #include"fpa2bv_rewriter.h"
 #include"simplify_tactic.h"
 #include"fpa2bv_tactic.h"
+#include"fpa2bv_model_converter.h"
 
 class fpa2bv_tactic : public tactic {
     struct imp {