new theory_fpa. plenty of bugs remain.

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

src/smt/theory_fpa.cpp

@@ -36,11 +36,60 @@ namespace smt {
         }
     };
 
+    void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) {
+        SASSERT(f->get_family_id() == null_family_id);
+        SASSERT(f->get_arity() == 0);
+        expr * r;
+        if (m_const2bv.find(f, r)) {
+            result = r;
+        }
+        else {            
+            sort * s = f->get_range();
+            func_decl *w, *u;
+            m_th.get_wrap(s, w, u);
+            expr_ref bv(m);
+            bv = m.mk_app(w, m.mk_const(f));
+            unsigned bv_sz = m_th.m_converter.bu().get_bv_size(bv);
+            unsigned ebits = m_th.m_converter.fu().get_ebits(f->get_range());
+            unsigned sbits = m_th.m_converter.fu().get_sbits(f->get_range());
+            SASSERT(bv_sz == ebits + sbits);
+            m_th.m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
+                                       m_bv_util.mk_extract(sbits - 2, 0, bv),
+                                       m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
+                                       result);
+
+            m_const2bv.insert(f, result);
+            m.inc_ref(f);
+            m.inc_ref(result);
+        }
+    }        
+
+    void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
+        SASSERT(f->get_family_id() == null_family_id);
+        SASSERT(f->get_arity() == 0);
+        expr * r;
+        if (m_rm_const2bv.find(f, r)) {
+            result = r;
+        }
+        else {
+            SASSERT(is_rm(f->get_range()));
+
+            sort * s = f->get_range();
+            func_decl *w, *u;
+            m_th.get_wrap(s, w, u);
+            result = m.mk_app(w, m.mk_const(f));
+            
+            m_rm_const2bv.insert(f, result);
+            m.inc_ref(f);
+            m.inc_ref(result);
+        }
+    }
+
     theory_fpa::theory_fpa(ast_manager & m) :
         theory(m.mk_family_id("float")),
-        m_converter(m),
+        m_converter(m, this),        
         m_rw(m, m_converter, params_ref()),
-        m_trans_map(m),
+        m_th_rw(m),
         m_trail_stack(*this)
     {
     }
@@ -49,45 +98,277 @@ namespace smt {
     {
     }
 
-    void theory_fpa::add_extra_assertions()
+    app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
+        TRACE("t_fpa", tout << "fpa_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";);
+        ast_manager & m = m_th.get_manager();
+        context & ctx = m_th.get_context();        
+        theory_id bv_id = m.mk_family_id("bv");
+        theory_bv * th_bv = dynamic_cast<theory_bv *>(ctx.get_theory(bv_id));
+        SASSERT(th_bv != 0);        
+        
+        float_util & fu = m_th.m_converter.fu();
+        bv_util & bu = m_th.m_converter.bu();
+        mpf_manager & mpfm = fu.fm();
+        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
+        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
+        
+        sort * s = m.get_sort(m_a);
+        unsigned ebits = fu.get_ebits(s);
+        unsigned sbits = fu.get_sbits(s);
+
+        scoped_mpz bias(mpzm);
+        mpzm.power(mpz(2), ebits - 1, bias);
+        mpzm.dec(bias);
+
+        app * result;
+        float_op_kind k = (float_op_kind) to_app(m_a)->get_decl_kind();
+        switch (k)
+        {        
+        case -1: {
+            func_decl *w, *u;
+            m_th.get_wrap(s, w, u);
+            rational bv_val(0);
+            scoped_mpz sgn(mpzm), sig(mpzm), exp(bias);
+            app_ref bv_w(m);
+            bv_w = m.mk_app(w, m_a);
+
+            if (!th_bv->get_fixed_value(bv_w, bv_val))
+                result = fu.mk_nan(ebits, sbits);
+            else {
+                scoped_mpz all_bits(mpzm);
+                all_bits = bv_val.to_mpq().numerator();
+                SASSERT(mpzm.is_one(bv_val.to_mpq().denominator()));
+                
+                mpzm.machine_div2k(all_bits, ebits + sbits - 1, sgn);
+
+                scoped_mpz tmp_p(mpzm);
+                mpzm.power(mpz(2), ebits + sbits - 1, tmp_p);
+
+                if (mpzm.is_one(sgn)) mpzm.sub(all_bits, tmp_p, all_bits);
+
+                mpzm.machine_div2k(all_bits, sbits - 1, exp);
+                scoped_mpz exp_u(mpzm);
+                mpzm.sub(exp, bias, exp_u);
+                SASSERT(mpzm.is_int64(exp_u));
+                
+                mpzm.power(mpz(2), sbits - 1, tmp_p);
+                mpzm.mod(all_bits, tmp_p, sig);
+
+                scoped_mpf f(mpfm);                
+                mpfm.set(f, ebits, sbits, mpzm.is_one(sgn), sig, mpzm.get_int64(exp_u));
+                result = fu.mk_value(f);
+            }
+            break;
+        }
+        case OP_FLOAT_FP: {         
+            bool is_internalized = ctx.e_internalized(m_a);
+            if (is_internalized) {
+                SASSERT(m_a->get_num_args() == 3);
+                app_ref a_sgn(m), a_sig(m), a_exp(m);
+                a_sgn = to_app(m_a->get_arg(0));
+                a_exp = to_app(m_a->get_arg(1));
+                a_sig = to_app(m_a->get_arg(2));
+
+                scoped_mpz bias(mpzm);
+                mpzm.power(mpz(2), ebits - 1, bias);
+                mpzm.dec(bias);
+
+                rational sgn(0), sig(0), exp(bias);
+                th_bv->get_fixed_value(a_sgn, sgn);
+                th_bv->get_fixed_value(a_sig, sig);
+                th_bv->get_fixed_value(a_exp, exp);
+
+                TRACE("t_fpa", tout << "sgn=" << sgn.to_string() << " ; " <<
+                                       "sig=" << sig.to_string() << " ; " <<
+                                       "exp=" << exp.to_string() << std::endl;);
+
+                rational exp_u = exp - rational(bias);
+                SASSERT(exp_u.is_int64());
+
+                scoped_mpf f(mpfm);
+                scoped_mpq sig_q(mpqm);
+                sig_q = sig.to_mpq();
+                mpfm.set(f, ebits, sbits, sgn.is_one(), sig_q.get().numerator(), exp_u.get_int64());
+                result = fu.mk_value(f);
+            }
+            else {            
+                result = fu.mk_nan(ebits, sbits);
+            }
+            break;
+        }
+        default:
+            NOT_IMPLEMENTED_YET();
+        }
+
+        TRACE("t_fpa", tout << "fpa_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
+        return result;
+    }
+
+    app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {        
+        TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";);
+        ast_manager & m = m_th.get_manager();
+        context & ctx = m_th.get_context();
+        theory_id bv_id = m.mk_family_id("bv");
+        theory_bv * th_bv = dynamic_cast<theory_bv *>(ctx.get_theory(bv_id));
+
+        app * result = 0;
+        mpf_rounding_mode rm;
+        if (m_th.m_converter.fu().is_rm_value(m_a, rm)) {
+            result = m_a.get();
+        }
+        else {
+            sort * s = m.get_sort(m_a);
+            func_decl *w, *u;
+            m_th.get_wrap(s, w, u);
+
+            app_ref bv_w(m);
+            bv_w = m.mk_app(w, m_a);
+
+            rational val(0);
+            if (ctx.e_internalized(bv_w))
+                if (!th_bv->get_fixed_value(bv_w, val))
+                    val = rational(0);
+            
+            switch (val.get_uint64())
+            {
+            case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
+            case BV_RM_TIES_TO_EVEN: result = m_fu.mk_round_nearest_ties_to_even(); break;
+            case BV_RM_TO_NEGATIVE: result = m_fu.mk_round_toward_negative(); break;
+            case BV_RM_TO_POSITIVE: result = m_fu.mk_round_toward_positive(); break;
+            case BV_RM_TO_ZERO:
+            default: result = m_fu.mk_round_toward_zero();
+            }
+        }
+
+        TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
+        return result;
+    }
+
+    void theory_fpa::get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap)
+    {
+        if (!m_wraps.find(s, wrap) || !m_unwraps.find(s, unwrap)) {
+            SASSERT(!m_wraps.contains(s));
+            ast_manager & m = get_manager();
+            sort * bv_srt = 0;
+
+            if (m_converter.is_rm(s))
+                bv_srt = m_converter.bu().mk_sort(3);
+            else {
+                SASSERT(m_converter.is_float(s));                
+                unsigned ebits = m_converter.fu().get_ebits(s);
+                unsigned sbits = m_converter.fu().get_sbits(s);
+                bv_srt = m_converter.bu().mk_sort(ebits + sbits);
+            }
+
+            wrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &s, bv_srt);
+            unwrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
+            m_wraps.insert(s, wrap);
+            m_unwraps.insert(s, unwrap);
+            get_context().push_trail(insert_obj_map<context, sort, func_decl*>(m_wraps, s));
+            get_context().push_trail(insert_obj_map<context, sort, func_decl*>(m_unwraps, s));
+        }
+    }
+    
+    expr_ref theory_fpa::convert_atom(expr * e) {
+        ast_manager & m = get_manager();
+        expr_ref res(m);
+        proof_ref pr(m);
+        m_rw(e, res);
+
+        TRACE("t_fpa", tout << "converted atom:" << std::endl;
+        tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
+            mk_ismt2_pp(res, m) << std::endl;);
+        return res;
+    }
+
+    expr_ref theory_fpa::convert_term(expr * e) {
+        ast_manager & m = get_manager();
+        expr_ref res(m);
+        proof_ref pr(m);
+        m_rw(e, res);
+        
+        SASSERT(is_app(res));
+        
+        if (m_converter.fu().is_rm(e)) {
+            SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT));
+            SASSERT(m_converter.bu().get_bv_size(res) == 3);
+        }
+        else {
+            SASSERT(to_app(res)->get_family_id() == get_family_id());
+            decl_kind k = to_app(res)->get_decl_kind();
+            if (k == OP_FLOAT_TO_FP) {
+                SASSERT(to_app(res)->get_num_args() == 3);
+                SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(0)), m_converter.bu().get_family_id(), BV_SORT));
+                SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(1)), m_converter.bu().get_family_id(), BV_SORT));
+                SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(2)), m_converter.bu().get_family_id(), BV_SORT));
+
+                expr *sgn, *sig, *exp;
+                expr_ref s_sgn(m), s_sig(m), s_exp(m);
+                m_converter.split_triple(res, sgn, sig, exp);
+                m_th_rw(sgn, s_sgn);
+                m_th_rw(sig, s_sig);
+                m_th_rw(exp, s_exp);
+
+                m_converter.mk_triple(s_sgn, s_sig, s_exp, res);
+            }
+            else {
+                SASSERT(is_sort_of(m.get_sort(e), get_family_id(), ROUNDING_MODE_SORT));
+                SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT));
+            }
+        }
+
+        TRACE("t_fpa", tout << "converted term:" << std::endl;
+                    tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
+                    mk_ismt2_pp(res, m) << std::endl;);
+        return res;
+    }
+
+    expr_ref theory_fpa::mk_side_conditions()
     {
         ast_manager & m = get_manager();
         context & ctx = get_context();
         simplifier & simp = ctx.get_simplifier();
         
-        expr_ref_vector::iterator it = m_converter.extra_assertions.begin();
+        expr_ref res(m), t(m);
-        expr_ref_vector::iterator end = m_converter.extra_assertions.end();
+        proof_ref t_pr(m);
+        res = m.mk_true();
+
+        expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin();
+        expr_ref_vector::iterator end = m_converter.m_extra_assertions.end();
         for (; it != end; it++) {
-            expr_ref t(m);
-            proof_ref t_pr(m);
             simp(*it, t, t_pr);
-            TRACE("t_fpa", tout << "extra: " << mk_ismt2_pp(t, m) << "\n";);            
+            res = m.mk_and(res, t);
-            ctx.internalize_assertion(t, t_pr, 0);
         }
-        m_converter.extra_assertions.reset();
+        m_converter.m_extra_assertions.reset();
+
+        TRACE("t_fpa", if (!m.is_true(res)) tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
+        return res;
     }
 
-    void theory_fpa::mk_bv_eq(expr * x, expr * y) {
+    void theory_fpa::assert_cnstr(expr * e) {
-        SASSERT(get_sort(x)->get_family_id() == m_converter.bu().get_family_id());
+        if (get_manager().is_true(e)) return;
-        SASSERT(get_sort(y)->get_family_id() == m_converter.bu().get_family_id());
+        TRACE("t_fpa", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
-        ast_manager & m = get_manager();
+        context& ctx = get_context();
+        ctx.internalize(e, false);
+        literal lit(ctx.get_literal(e));
+        ctx.mark_as_relevant(lit);
+        ctx.mk_th_axiom(get_id(), 1, &lit);
+    }    
+
+    void theory_fpa::attach_new_th_var(enode * n) {
         context & ctx = get_context();
-        theory_id bv_tid = ctx.get_theory(m.get_sort(x)->get_family_id())->get_id();
+        theory_var v = mk_var(n);
-        literal l = mk_eq(x, y, false);
+        ctx.attach_th_var(n, this, v);
-        ctx.mk_th_axiom(bv_tid, 1, &l);
+        m_tvars.push_back(v);        
-        ctx.mark_as_relevant(l);
+        TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);       
     }
 
     bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
-        TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
+        TRACE("t_fpa_detail", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
         SASSERT(atom->get_family_id() == get_family_id());
 
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        simplifier & simp = ctx.get_simplifier();
-        bv_util & bu = m_converter.bu();        
-        expr_ref bv_atom(m);
-        proof_ref pr(m);
 
         if (ctx.b_internalized(atom))
             return true;
@@ -96,187 +377,157 @@ namespace smt {
         for (unsigned i = 0; i < num_args; i++)
             ctx.internalize(atom->get_arg(i), false);
 
-        m_rw(atom, bv_atom);
-        simp(bv_atom, bv_atom, pr);
-
-        ctx.internalize(bv_atom, gate_ctx);
-        literal def = ctx.get_literal(bv_atom);
         literal l(ctx.mk_bool_var(atom));
         ctx.set_var_theory(l.var(), get_id());
-        pred_atom * a = new (get_region()) pred_atom(l, def);
-        insert_bv2a(l.var(), a);
-        m_trail_stack.push(fpa_atom_trail(l.var()));
 
-        if (!ctx.relevancy()) {
+        expr_ref bv_atom(m);
-            ctx.mk_th_axiom(get_id(), l, ~def);
+        bv_atom = convert_atom(atom);
-            ctx.mk_th_axiom(get_id(), ~l, def);
+        bv_atom = m.mk_and(bv_atom, mk_side_conditions());
-        }
-
-        add_extra_assertions();
         
+        expr_ref atom_iff(m);
+        assert_cnstr(m.mk_iff(atom, bv_atom));
         return true;
     }
 
     bool theory_fpa::internalize_term(app * term) {
-        TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
+        TRACE("t_fpa_detail", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
         SASSERT(term->get_family_id() == get_family_id());
         SASSERT(!get_context().e_internalized(term));
 
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        simplifier & simp = ctx.get_simplifier();
-        bv_util & bu = m_converter.bu();
-        sort * term_sort = m.get_sort(term);
-        expr_ref t(m), bv_term(m);
-        proof_ref pr(m);
 
         unsigned num_args = term->get_num_args();
         for (unsigned i = 0; i < num_args; i++)
             ctx.internalize(term->get_arg(i), false);
         
-        m_rw(term, t);
+        enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : 
-        simp(t, t, pr);
+                                                 ctx.mk_enode(term, false, false, true);
 
-        if (m_converter.is_rm(term_sort)) {            
+        if (is_attached_to_var(e))
-            SASSERT(is_app(t));
+            return false;
-            expr_ref bv_rm(m);
-            proof_ref bv_pr(m);
-            simp(t, bv_rm, bv_pr);
 
-            bv_term = bv_rm;
+        attach_new_th_var(e);
-        }
+        TRACE("t_fpa", tout << "internalized? " << (ctx.e_internalized(term)?"yes":"no") << std::endl;);
-        else if (m_converter.is_float(term_sort)) {
+        return true;
-            SASSERT(is_app(t) && to_app(t)->get_num_args() == 3);            
-            app * a = to_app(t);
-            expr_ref sgn(m), sig(m), exp(m);
-            proof_ref pr_sgn(m), pr_sig(m), pr_exp(m);
-            simp(a->get_arg(0), sgn, pr_sgn);
-            simp(a->get_arg(1), sig, pr_sig);
-            simp(a->get_arg(2), exp, pr_exp);
-
-            m_converter.mk_triple(sgn, sig, exp, bv_term);            
-        }   
-        else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV ||
-                 term->get_decl_kind() == OP_FLOAT_TO_REAL) {
-            SASSERT(is_app(t));
-            expr_ref bv_e(m);
-            proof_ref bv_pr(m);
-            simp(t, bv_term, bv_pr);
-        }
-        else
-            NOT_IMPLEMENTED_YET();
-
-        TRACE("t_fpa", tout << "converted: " << mk_ismt2_pp(bv_term, get_manager()) << "\n";);
-
-        SASSERT(!m_trans_map.contains(term));
-        m_trans_map.insert(term, bv_term, 0);
-
-        add_extra_assertions();
-
-        enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true);
-        theory_var v = mk_var(e);
-        ctx.attach_th_var(e, this, v);
-        m_tvars.push_back(v);
-        TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(term, get_manager()) << " := " << v << "\n";);
-        SASSERT(e->get_th_var(get_id()) != null_theory_var);
-        return v != null_theory_var;
     }    
 
     void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {        
-        if (!is_attached_to_var(n)) {
+        TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);        
-            TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
+        SASSERT(n->get_owner()->get_family_id() == get_family_id() ||
-            context & ctx = get_context();
+                n->get_owner()->get_family_id() == null_theory_id);
-            ast_manager & m = get_manager();
+        SASSERT(s->get_family_id() == get_family_id());
-            simplifier & simp = ctx.get_simplifier();
+        ast_manager & m = get_manager();        
-            app * owner = n->get_owner();
-            expr_ref converted(m);
-            proof_ref pr(m);
 
-            theory_var v = mk_var(n);            
+        if (!is_attached_to_var(n))
-            ctx.attach_th_var(n, this, v);
+            attach_new_th_var(n);
-            m_tvars.push_back(v);
-            m_rw(owner, converted);
-            simp(converted, converted, pr);
-            m_trans_map.insert(owner, converted, 0);
             
-            add_extra_assertions();
+        app * owner = n->get_owner();
-            
+        sort * owner_sort = m.get_sort(owner);
-            sort * owner_sort = m.get_sort(owner);
+        if (m_converter.is_rm(owner_sort)) {
-            if (m_converter.is_rm(owner_sort)) {
+            bv_util & bu = m_converter.bu();
-                bv_util & bu = m_converter.bu();
+            func_decl *wrap, *unwrap;
-                expr_ref t(m);
+            get_wrap(owner_sort, wrap, unwrap);
-                t = bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted)));
+            if (owner->get_decl() != unwrap)
-                ctx.internalize_assertion(t, proof_ref(m), 0);
+            {                
+                expr_ref converted(m), t(m);
+                m_rw(owner, converted);
+                t = bu.mk_ule(converted, bu.mk_numeral(4, 3));
+                assert_cnstr(t);
             }
-
-            TRACE("t_fpa", tout << "new theory var (const): " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";);
         }
     }
 
     void theory_fpa::new_eq_eh(theory_var x, theory_var y) {        
-        TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";);
         ast_manager & m = get_manager();
+
+        TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;
+                       tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " = " << 
+                               mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl; );
+        
         context & ctx = get_context();
         float_util & fu = m_converter.fu();
+        bv_util & bu = m_converter.bu();
+        mpf_manager & mpfm = fu.fm();
 
-        app * ax = get_enode(x)->get_owner();
+        app * xe = get_enode(x)->get_owner();
-        app * ay = get_enode(y)->get_owner();
+        app * ye = get_enode(y)->get_owner();        
-        expr * ex, *ey;
-        proof * px, *py;
-        m_trans_map.get(ax, ex, px);
-        m_trans_map.get(ay, ey, py);
 
-        if (fu.is_float(get_enode(x)->get_owner())) {
+        if (fu.is_float(xe) && fu.is_float(ye))
-            expr * sgn_x, *sig_x, *exp_x;
+        {
-            expr * sgn_y, *sig_y, *exp_y;
+            expr_ref xc(m), yc(m);
-            split_triple(ex, sgn_x, sig_x, exp_x);
+            xc = convert_term(xe);
-            split_triple(ey, sgn_y, sig_y, exp_y);
+            yc = convert_term(ye);
 
-            mk_bv_eq(sgn_x, sgn_y);
+            expr *x_sgn, *x_sig, *x_exp;
-            mk_bv_eq(sig_x, sig_y);
+            m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
-            mk_bv_eq(exp_x, exp_y);
+            expr *y_sgn, *y_sig, *y_exp;
+            m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
+
+            expr_ref c(m);
+            c = m.mk_and(m.mk_eq(x_sgn, y_sgn),
+                         m.mk_eq(x_sig, y_sig),
+                         m.mk_eq(x_exp, y_exp));
+            assert_cnstr(c);
+            assert_cnstr(mk_side_conditions());
         }
-        else if (fu.is_rm(get_enode(x)->get_owner())) {
+        else if (fu.is_rm(xe) && fu.is_rm(ye)) {
-            mk_bv_eq(ex, ey);
+            expr_ref xc(m), yc(m);
+            xc = convert_term(xe);
+            yc = convert_term(ye);
+            expr_ref c(m);
+            c = m.mk_eq(xc, yc);
+            assert_cnstr(c);
+            assert_cnstr(mk_side_conditions());
         }
-        else 
+        
-            UNREACHABLE();
+        return;
     }
 
     void theory_fpa::new_diseq_eh(theory_var x, theory_var y) {
-        TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << "\n";);
         ast_manager & m = get_manager();
+
+        TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;
+                       tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
+                               mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
+
         context & ctx = get_context();
         float_util & fu = m_converter.fu();
+        bv_util & bu = m_converter.bu();
+        mpf_manager & mpfm = fu.fm();
 
-        app * ax = get_enode(x)->get_owner();
+        app * xe = get_enode(x)->get_owner();
-        app * ay = get_enode(y)->get_owner();
+        app * ye = get_enode(y)->get_owner();
-        expr * ex, *ey;
-        proof * px, *py;
-        m_trans_map.get(ax, ex, px);
-        m_trans_map.get(ay, ey, py);
 
-        expr_ref deq(m);
+        if (fu.is_float(xe) && fu.is_float(ye))
+        {
+            expr_ref xc(m), yc(m);
+            xc = convert_term(xe);
+            yc = convert_term(ye);
 
-        if (fu.is_float(m.get_sort(get_enode(x)->get_owner()))) {
+            expr *x_sgn, *x_sig, *x_exp;
-            expr * sgn_x, *sig_x, *exp_x;
+            m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
-            expr * sgn_y, *sig_y, *exp_y;
+            expr *y_sgn, *y_sig, *y_exp;
-            split_triple(ex, sgn_x, sig_x, exp_x);
+            m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
-            split_triple(ex, sgn_y, sig_y, exp_y);
 
-            deq = m.mk_or(m.mk_not(m.mk_eq(sgn_x, sgn_y)),
+            expr_ref c(m);
-                          m.mk_not(m.mk_eq(sig_x, sig_y)),
+            c = m.mk_or(m.mk_not(m.mk_eq(x_sgn, y_sgn)),
-                          m.mk_not(m.mk_eq(exp_x, exp_y)));            
+                        m.mk_not(m.mk_eq(x_sig, y_sig)),
+                        m.mk_not(m.mk_eq(x_exp, y_exp)));
+            assert_cnstr(c);
+            assert_cnstr(mk_side_conditions());
         }
-        else if (fu.is_rm(m.get_sort(get_enode(x)->get_owner()))) {
+        else if (fu.is_rm(xe) && fu.is_rm(ye)) {
-            deq = m.mk_not(m.mk_eq(ex, ey));
+            expr_ref xc(m), yc(m);
+            xc = convert_term(xe);
+            yc = convert_term(ye);
+            expr_ref c(m);
+            c = m.mk_not(m.mk_eq(xc, yc));
+            assert_cnstr(c);
+            assert_cnstr(mk_side_conditions());
         }
-        else
-            UNREACHABLE();
 
-        ctx.internalize(deq, true);
+        return;
-        ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(deq));
-        ctx.mark_as_relevant(deq);
     }
 
     void theory_fpa::push_scope_eh() {
@@ -289,198 +540,117 @@ namespace smt {
         m_trail_stack.pop_scope(num_scopes);
         unsigned num_old_vars = get_old_num_vars(num_scopes);
         for (unsigned i = num_old_vars; i < get_num_vars(); i++) {
-            m_trans_map.erase(get_enode(m_tvars[i])->get_owner());
+            // m_trans_map.erase(get_enode(m_tvars[i])->get_owner());
         }
         m_tvars.shrink(num_old_vars);
         theory::pop_scope_eh(num_scopes);
     }    
 
-    model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
+    void theory_fpa::assign_eh(bool_var v, bool is_true) {
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        bv_util & bu = m_converter.bu();
+        expr * e = ctx.bool_var2expr(v);
-        float_util & fu = m_converter.fu();
-        mpf_manager & mpfm = fu.fm();
-        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
-        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         
-        theory_var v = n->get_th_var(get_id());
+        TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
-        SASSERT(v != null_theory_var);
-        expr * fpa_e = get_enode(v)->get_owner();
-        TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(fpa_e, m) << "\n";);
         
-        expr * bv_e;
+        expr_ref converted(m);
-        proof * bv_pr;
+        m_rw(e, converted);
-        m_trans_map.get(fpa_e, bv_e, bv_pr);
+        converted = m.mk_and(converted, mk_side_conditions());
-        sort * fpa_e_srt = m.get_sort(fpa_e);
+        if (!is_true) converted = m.mk_not(converted);
-        expr_wrapper_proc * res = 0;
+        assert_cnstr(converted);
-
-        if (fu.is_rm(fpa_e_srt)) {
-            if (!ctx.e_internalized(bv_e))
-                res = alloc(expr_wrapper_proc, fu.mk_round_nearest_ties_to_away());
-            else
-            {
-                theory_bv * bv_th = (theory_bv*)ctx.get_theory(m.get_family_id("bv"));
-                rational val;
-
-                bv_th->get_fixed_value(ctx.get_enode(bv_e)->get_owner(), val); // OK to fail
-                app * fp_val_e;
-                SASSERT(val.is_uint64());
-                switch (val.get_uint64())
-                {
-                case BV_RM_TIES_TO_AWAY: fp_val_e = fu.mk_round_nearest_ties_to_away(); break;
-                case BV_RM_TIES_TO_EVEN: fp_val_e = fu.mk_round_nearest_ties_to_even(); break;
-                case BV_RM_TO_NEGATIVE: fp_val_e = fu.mk_round_toward_negative(); break;
-                case BV_RM_TO_POSITIVE: fp_val_e = fu.mk_round_toward_positive(); break;
-                case BV_RM_TO_ZERO:
-                default: fp_val_e = fu.mk_round_toward_zero();
-                }
-
-                TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;);
-                res = alloc(expr_wrapper_proc, fp_val_e);
-            }
-        }
-        else if (fu.is_float(fpa_e_srt)) {
-            expr * bv_sgn, *bv_sig, *bv_exp;
-            split_triple(bv_e, bv_sgn, bv_sig, bv_exp);
-
-            family_id fid = m.get_family_id("bv");
-            theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid);            
-
-            app * e_sgn, *e_sig, *e_exp;
-            unsigned ebits = fpa_e_srt->get_parameter(0).get_int();
-            unsigned sbits = fpa_e_srt->get_parameter(1).get_int();
-            unsigned sig_sz = fpa_e_srt->get_parameter(1).get_int() - 1;
-
-            rational bias = mpfm.m_powers2.m1(ebits - 1);
-            rational sgn_r(0), sig_r(0), exp_r(bias);
-
-            e_sgn = (ctx.e_internalized(bv_sgn)) ? ctx.get_enode(bv_sgn)->get_owner() : 
-                                                   bu.mk_numeral(0, 1);
-            e_sig = (ctx.e_internalized(bv_sig)) ? ctx.get_enode(bv_sig)->get_owner() : 
-                                                   bu.mk_numeral(0, sig_sz);
-            e_exp = (ctx.e_internalized(bv_exp)) ? ctx.get_enode(bv_exp)->get_owner() :
-                                                   bu.mk_numeral(bias, ebits);
-
-            TRACE("t_fpa", tout << "bv rep: ["
-                  << mk_ismt2_pp(e_sgn, m) << "\n"
-                  << mk_ismt2_pp(e_sig, m) << "\n"
-                  << mk_ismt2_pp(e_exp, m) << "]\n";);                        
-            
-            if (!ctx.e_internalized(bv_sgn) ||
-                ctx.get_enode(bv_sgn)->get_num_th_vars() == 0 ||
-                !bv_th->get_fixed_value(e_sgn, sgn_r))
-                    sgn_r = rational(0);
-            if (!ctx.e_internalized(bv_sig) ||
-                ctx.get_enode(bv_sig)->get_num_th_vars() == 0 ||
-                !bv_th->get_fixed_value(e_sig, sig_r))
-                    sig_r = rational(0);
-            if (!ctx.e_internalized(bv_exp) || 
-                ctx.get_enode(bv_exp)->get_num_th_vars() == 0 ||
-                !bv_th->get_fixed_value(e_exp, exp_r))
-                    exp_r = bias;
-
-            // un-bias exponent
-            rational exp_unbiased_r;
-            exp_unbiased_r = exp_r - bias;
-
-            TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " "
-                  << sig_r.to_string() << " "
-                  << exp_unbiased_r.to_string() << "(" << exp_r.to_string() << ")]\n"; );
-
-            scoped_mpz sig_z(mpzm);
-            mpf_exp_t exp_z;
-            scoped_mpq sig_q(mpqm), exp_q(mpqm);
-            scoped_mpz sig_num(mpzm), exp_num(mpzm);
-            mpqm.set(sig_q, sig_r.to_mpq());
-            mpzm.set(sig_num, sig_q.get().numerator());
-            mpqm.set(exp_q, exp_unbiased_r.to_mpq());
-            mpzm.set(exp_num, exp_q.get().numerator());
-            mpzm.set(sig_z, sig_num);
-            exp_z = mpzm.get_int64(exp_num);
-
-            scoped_mpf fp_val(mpfm);
-            mpfm.set(fp_val, ebits, sbits, !sgn_r.is_zero(), sig_z, exp_z);            
-
-            TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mpfm.to_string(fp_val) << std::endl;);
-            res = alloc(expr_wrapper_proc, m_factory->mk_value(fp_val));
-        }
-        else
-            UNREACHABLE();
-
-        return res;
-    }
-
-    void theory_fpa::assign_eh(bool_var v, bool is_true) {
-        TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << ")\n";);
-        /* CMW: okay to ignore? */
-        theory::assign_eh(v, is_true);
     }
 
     void theory_fpa::relevant_eh(app * n) {
         TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, get_manager()) << "\n";);
+        
+        NOT_IMPLEMENTED_YET();
+
         ast_manager & m = get_manager();
-        context & ctx = get_context();
+
+        if (m.is_bool(n))
+            return;
+
         float_util & fu = m_converter.fu();
         bv_util & bu = m_converter.bu();
+        mpf_manager & mpfm = fu.fm();
 
-        if (m.is_bool(n)) {
+        if (bu.is_bv(n))
-            bool_var v = ctx.get_bool_var(n);
+            return;
-            atom * a = get_bv2a(v);
-            pred_atom * pa = static_cast<pred_atom*>(a);
-            ctx.mark_as_relevant(pa->m_def);            
-            ctx.mk_th_axiom(get_id(), pa->m_var, ~pa->m_def);
-            ctx.mk_th_axiom(get_id(), ~pa->m_var, pa->m_def);
-        }
-        else if (ctx.e_internalized(n)) {
-            SASSERT(m_trans_map.contains(n));
-            expr * ex;
-            proof * px;
-            m_trans_map.get(n, ex, px);
-            sort * n_srt = m.get_sort(n);
 
-            if (fu.is_rm(n_srt)) {
+        sort * s = m.get_sort(n);
-                ctx.mark_as_relevant(ex);                
+        func_decl *wrap, *unwrap;
-            }
+        get_wrap(s, wrap, unwrap);
-            else if (fu.is_float(n_srt)) {
-                expr * bv_sgn, *bv_sig, *bv_exp;
-                split_triple(ex, bv_sgn, bv_sig, bv_exp);
 
-                ctx.mark_as_relevant(bv_sgn);
+        if (n->get_decl() != unwrap) {
-                ctx.mark_as_relevant(bv_sig);
+            expr * wrapped = m.mk_app(wrap, n);
-                ctx.mark_as_relevant(bv_exp);
+            mpf_rounding_mode rm;
-            }
+            scoped_mpf val(mpfm);
-            else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV ||
+            if (fu.is_rm_value(n, rm))
-                     n->get_decl()->get_decl_kind() == OP_FLOAT_TO_REAL) {
+                assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rm, 3)));
-                expr_ref eq(m);
+            else if (fu.is_value(n, val)) {
-                app * ex_a = to_app(ex);
+                unsigned sz = val.get().get_ebits() + val.get().get_sbits();
-                if (n->get_id() > ex_a->get_id())
+                scoped_mpq q(fu.fm().mpq_manager());
-                    std::swap(n, ex_a);
+                mpfm.to_rational(val, q);
-                eq = m.mk_eq(n, ex_a);
+                assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rational(q), sz)));
-                ctx.internalize(eq, false);
-                literal l = ctx.get_literal(eq);
-                ctx.mk_th_axiom(get_id(), 1, &l);
-                ctx.mark_as_relevant(l);
             }
             else
-                NOT_IMPLEMENTED_YET();
+                assert_cnstr(m.mk_eq(m.mk_app(unwrap, wrapped), n));
         }
-        else
-            UNREACHABLE();
     }
 
     void theory_fpa::reset_eh() {
+        TRACE("t_fpa", tout << "reset_eh for: " << "\n";);
         pop_scope_eh(m_trail_stack.get_num_scopes());
         m_rw.reset();
-        m_trans_map.reset();
         m_bool_var2atom.reset();
         m_temporaries.reset();
         m_tvars.reset();
         theory::reset_eh();
     }
 
-    void theory_fpa::init_model(model_generator & m) {        
+    void theory_fpa::init_model(model_generator & mg) {
+        TRACE("t_fpa", tout << "initializing model" << std::endl;);
         m_factory = alloc(fpa_factory, get_manager(), get_family_id());
-        m.register_factory(m_factory);
+        mg.register_factory(m_factory);
+        TRACE("t_fpa", display(tout););
+    }
+
+    model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
+        TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
+
+        ast_manager & m = get_manager();
+        float_util & fu = m_converter.fu();
+
+        expr * owner = n->get_owner();
+        sort * o_srt = m.get_sort(owner);
+
+        mpf_rounding_mode rm;
+
+        if (fu.is_rm_value(n->get_owner(), rm))
+            return alloc(expr_wrapper_proc, n->get_owner());
+        else if (fu.is_value(n->get_owner()))
+            return alloc(expr_wrapper_proc, n->get_owner());
+        else if (fu.is_rm(owner))
+            return alloc(fpa_rm_value_proc, this, app_ref(to_app(owner), m));
+        else if (fu.is_float(owner))
+            return alloc(fpa_value_proc, this, app_ref(to_app(owner), m));
+        
+        UNREACHABLE();
+        return 0;
+    }
+
+    void theory_fpa::finalize_model(model_generator & mg) {}
+
+    void theory_fpa::display(std::ostream & out) const
+    {
+        ast_manager & m = get_manager();
+        context & ctx = get_context();
+        
+        out << "theory variables:" << std::endl;        
+        ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
+        ptr_vector<enode>::const_iterator end = ctx.end_enodes();
+        for (; it != end; it++)
+            out << (*it)->get_th_var(get_family_id()) << " -> " <<
+            mk_ismt2_pp((*it)->get_owner(), m) << std::endl; 
     }
 };

src/smt/theory_fpa.h

@@ -23,7 +23,9 @@ Revision History:
 #include"trail.h"
 #include"fpa2bv_converter.h"
 #include"fpa2bv_rewriter.h"
+#include"th_rewriter.h"
 #include"value_factory.h"
+#include"smt_model_generator.h"
 
 namespace smt {
 
@@ -54,7 +56,6 @@ namespace smt {
         }
     };    
 
-
     class theory_fpa : public theory {
         class th_trail_stack : public trail_stack<theory_fpa> {
         public: 
@@ -62,6 +63,45 @@ namespace smt {
             virtual ~th_trail_stack() {}
         };
 
+        class fpa2bv_converter_wrapped : public fpa2bv_converter {
+        public:
+            theory_fpa & m_th;
+            fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) :
+                fpa2bv_converter(m),
+                m_th(*th) {}
+            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);
+        };
+        
+        class fpa_value_proc : public model_value_proc {
+        protected:
+            theory_fpa                    & m_th;
+            app_ref                         m_a;
+            svector<model_value_dependency> m_dependencies;
+        public:
+            fpa_value_proc(theory_fpa * th, app_ref & a) : m_th(*th), m_a(a) {}
+            void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
+            virtual ~fpa_value_proc() {}
+            virtual void get_dependencies(buffer<model_value_dependency> & result) {
+                result.append(m_dependencies.size(), m_dependencies.c_ptr());
+            }
+            virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
+        };
+
+        class fpa_rm_value_proc : public fpa_value_proc {
+            float_util & m_fu;
+            bv_util    & m_bu;
+        public:
+            fpa_rm_value_proc(theory_fpa * th, app_ref & a) : 
+                fpa_value_proc(th, a), 
+                m_fu(th->m_converter.fu()), 
+                m_bu(th->m_converter.bu()) {}
+            void add_dependency(enode * n) { fpa_value_proc::add_dependency(n); }
+            virtual ~fpa_rm_value_proc() {}
+            virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
+        };
+    
     public:
         class atom {
         public:
@@ -82,14 +122,17 @@ namespace smt {
         region & get_region() { return m_trail_stack.get_region(); }        
 
     protected:
-        fpa2bv_converter m_converter;
+        fpa2bv_converter_wrapped  m_converter;
-        fpa2bv_rewriter  m_rw;
+        fpa2bv_rewriter           m_rw;
-        expr_map         m_trans_map;
+        th_rewriter               m_th_rw;
-        th_trail_stack   m_trail_stack;
+        th_trail_stack            m_trail_stack;
-        bool_var2atom    m_bool_var2atom;
+        bool_var2atom             m_bool_var2atom;
-        enode_vector     m_temporaries;
+        enode_vector              m_temporaries;
-        int_vector       m_tvars;
+        vector<theory_var>        m_tvars;        
-        fpa_factory *    m_factory;
+        fpa_factory *             m_factory;
+        obj_map<sort, func_decl*> m_wraps;
+        obj_map<sort, func_decl*> m_unwraps;
+        float_decl_plugin         m_flt_plugin;
 
         virtual final_check_status final_check_eh() { return FC_DONE; }
         virtual bool internalize_atom(app * atom, bool gate_ctx);
@@ -108,21 +151,24 @@ namespace smt {
         void assign_eh(bool_var v, bool is_true);
         virtual void relevant_eh(app * n);
         virtual void init_model(model_generator & m);
+        virtual void finalize_model(model_generator & mg);
+
     public:
         theory_fpa(ast_manager& m);
         virtual ~theory_fpa();
 
-    protected:
+        virtual void display(std::ostream & out) const;
-        void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
+
-            SASSERT(is_app_of(e, get_family_id(), OP_FLOAT_TO_FP));
+    protected:
-            SASSERT(to_app(e)->get_num_args() == 3);
+        expr_ref mk_side_conditions();
-            sgn = to_app(e)->get_arg(0);
+        expr_ref convert_atom(expr * e);
-            sig = to_app(e)->get_arg(1);
+        expr_ref convert_term(expr * e);
-            exp = to_app(e)->get_arg(2);
+        void get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap);
-        }
+        void add_trail(ast * a);
 
-        void add_extra_assertions();
         void mk_bv_eq(expr * x, expr * y);
+        void attach_new_th_var(enode * n);
+        void assert_cnstr(expr * e);
     };
 
 };