diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 1ff500359..517829026 100644 --- a/scripts/mk_project.py +++ b/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', diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp similarity index 92% rename from src/tactic/fpa/fpa2bv_converter.cpp rename to src/ast/fpa/fpa2bv_converter.cpp index 533988689..20925a0f9 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/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::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::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::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::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::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::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 seen; - - for (obj_map::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::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::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.end(); - it++) - seen.insert(it->m_value); - - for (obj_map::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 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 const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf); -} diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h similarity index 72% rename from src/tactic/fpa/fpa2bv_converter.h rename to src/ast/fpa/fpa2bv_converter.h index 79c8039ef..2ccdac6a9 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/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 m_const2bv; - obj_map m_rm_const2bv; - obj_map m_uf2bvuf; - obj_map m_uf23bvuf; - -public: - fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf) : - m(m) { - // Just create a copy? - for (obj_map::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::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::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::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 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 const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf); - #endif diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h similarity index 100% rename from src/tactic/fpa/fpa2bv_rewriter.h rename to src/ast/fpa/fpa2bv_rewriter.h diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp new file mode 100644 index 000000000..147d87496 --- /dev/null +++ b/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(); + } +}; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h new file mode 100644 index 000000000..3716247d3 --- /dev/null +++ b/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_ */ + diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp new file mode 100644 index 000000000..9b4b5a70f --- /dev/null +++ b/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::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::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::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::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::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::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 seen; + + for (obj_map::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::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::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) + seen.insert(it->m_value); + + for (obj_map::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 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 const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf); +} diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h new file mode 100644 index 000000000..7b9598740 --- /dev/null +++ b/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 m_const2bv; + obj_map m_rm_const2bv; + obj_map m_uf2bvuf; + obj_map m_uf23bvuf; + +public: + fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf) : + m(m) { + // Just create a copy? + for (obj_map::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::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::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::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 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 const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf); + +#endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 9bb35eea6..3a6b7ea45 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/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 {