diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 247cfcacb..34417b7fc 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -56,7 +56,7 @@ protected: special_t m_min_max_specials; friend class fpa2bv_model_converter; - friend class bv2fpa_converter; + friend class bv2fpa_converter; public: fpa2bv_converter(ast_manager & m); @@ -138,11 +138,11 @@ public: void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } @@ -227,9 +227,9 @@ private: void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); - expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); + expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); }; #endif diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 248d5b84d..3a45e1876 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -84,15 +84,15 @@ namespace smt { } } - theory_fpa::theory_fpa(ast_manager & m) : - theory(m.mk_family_id("fpa")), - m_converter(m, this), - m_rw(m, m_converter, params_ref()), - m_th_rw(m), - m_trail_stack(*this), - m_fpa_util(m_converter.fu()), - m_bv_util(m_converter.bu()), - m_arith_util(m_converter.au()), + theory_fpa::theory_fpa(ast_manager & m) : + theory(m.mk_family_id("fpa")), + m_converter(m, this), + m_rw(m, m_converter, params_ref()), + m_th_rw(m), + m_trail_stack(*this), + m_fpa_util(m_converter.fu()), + m_bv_util(m_converter.bu()), + m_arith_util(m_converter.au()), m_is_initialized(false) { params_ref p; @@ -799,33 +799,35 @@ namespace smt { } void theory_fpa::finalize_model(model_generator & mg) { +#if 0 ast_manager & m = get_manager(); proto_model & mdl = mg.get_model(); - proto_model new_model(m); - - bv2fpa_converter bv2fp(m, m_converter); - - obj_hashtable seen; - bv2fp.convert_min_max_specials(&mdl, &new_model, seen); - bv2fp.convert_uf2bvuf(&mdl, &new_model, seen); - - for (obj_hashtable::iterator it = seen.begin(); - it != seen.end(); - it++) - mdl.unregister_decl(*it); - - for (unsigned i = 0; i < new_model.get_num_constants(); i++) { - func_decl * f = new_model.get_constant(i); - mdl.register_decl(f, new_model.get_const_interp(f)); - } - - for (unsigned i = 0; i < new_model.get_num_functions(); i++) { - func_decl * f = new_model.get_function(i); - func_interp * fi = new_model.get_func_interp(f)->copy(); - mdl.register_decl(f, fi); - } + proto_model new_model(m); + + bv2fpa_converter bv2fp(m, m_converter); + + obj_hashtable seen; + bv2fp.convert_min_max_specials(&mdl, &new_model, seen); + bv2fp.convert_uf2bvuf(&mdl, &new_model, seen); + + for (obj_hashtable::iterator it = seen.begin(); + it != seen.end(); + it++) + mdl.unregister_decl(*it); + + for (unsigned i = 0; i < new_model.get_num_constants(); i++) { + func_decl * f = new_model.get_constant(i); + mdl.register_decl(f, new_model.get_const_interp(f)); + } + + for (unsigned i = 0; i < new_model.get_num_functions(); i++) { + func_decl * f = new_model.get_function(i); + func_interp * fi = new_model.get_func_interp(f)->copy(); + mdl.register_decl(f, fi); + } +#endif } - + void theory_fpa::display(std::ostream & out) const { ast_manager & m = get_manager(); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 9b95cf921..88224d2f2 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -22,52 +22,48 @@ Notes: void fpa2bv_model_converter::display(std::ostream & out) { out << "(fpa2bv-model-converter"; - m_bv2fp->display(out); + m_bv2fp->display(out); out << ")"; } model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { - fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to()); - res->m_bv2fp = m_bv2fp->translate(translator); + fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to()); + res->m_bv2fp = m_bv2fp->translate(translator); return res; } void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { - obj_hashtable seen; - m_bv2fp->convert_consts(mc, float_mdl, seen); - m_bv2fp->convert_rm_consts(mc, float_mdl, seen); - m_bv2fp->convert_min_max_specials(mc, float_mdl, seen); - m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen); - - // Keep all the non-float constants. - unsigned sz = mc->get_num_constants(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * c = mc->get_constant(i); - if (!seen.contains(c)) - float_mdl->register_decl(c, mc->get_const_interp(c)); - } - - // And keep everything else - sz = mc->get_num_functions(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * f = mc->get_function(i); - if (!seen.contains(f)) - { - TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); - func_interp * val = mc->get_func_interp(f)->copy(); - float_mdl->register_decl(f, val); - } - } - - sz = mc->get_num_uninterpreted_sorts(); - for (unsigned i = 0; i < sz; i++) - { - sort * s = mc->get_uninterpreted_sort(i); - ptr_vector u = mc->get_universe(s); - float_mdl->register_usort(s, u.size(), u.c_ptr()); - } + obj_hashtable seen; + m_bv2fp->convert_consts(mc, float_mdl, seen); + m_bv2fp->convert_rm_consts(mc, float_mdl, seen); + m_bv2fp->convert_min_max_specials(mc, float_mdl, seen); + m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen); + + // Keep all the non-float constants. + unsigned sz = mc->get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * c = mc->get_constant(i); + if (!seen.contains(c)) + float_mdl->register_decl(c, mc->get_const_interp(c)); + } + + // And keep everything else + sz = mc->get_num_functions(); + for (unsigned i = 0; i < sz; i++) { + func_decl * f = mc->get_function(i); + if (!seen.contains(f)) { + TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); + func_interp * val = mc->get_func_interp(f)->copy(); + float_mdl->register_decl(f, val); + } + } + + sz = mc->get_num_uninterpreted_sorts(); + for (unsigned i = 0; i < sz; i++) { + sort * s = mc->get_uninterpreted_sort(i); + ptr_vector u = mc->get_universe(s); + float_mdl->register_usort(s, u.size(), u.c_ptr()); + } } model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) { diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 7a39c0fba..1f482478b 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -25,23 +25,22 @@ Notes: class fpa2bv_model_converter : public model_converter { ast_manager & m; - bv2fpa_converter * m_bv2fp; + bv2fpa_converter * m_bv2fp; public: - fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) : - m(m) { - m_bv2fp = alloc(bv2fpa_converter, m, conv); + fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv): + m(m), + m_bv2fp(alloc(bv2fpa_converter, m, conv)) { } virtual ~fpa2bv_model_converter() { - if (m_bv2fp) dealloc(m_bv2fp); - m_bv2fp = 0; + dealloc(m_bv2fp); } virtual void operator()(model_ref & md, unsigned goal_idx) { SASSERT(goal_idx == 0); model * new_model = alloc(model, m); - convert(md.get(), new_model); + convert(md.get(), new_model); md = new_model; } @@ -56,9 +55,9 @@ public: protected: fpa2bv_model_converter(ast_manager & m) : m(m), - m_bv2fp(0) {} - - void convert(model_core * mc, model * float_mdl); + m_bv2fp(0) {} + + void convert(model_core * mc, model * float_mdl); }; diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 9dc0b43f9..f35a12ede 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -8,6 +8,7 @@ Copyright (c) 2016 Microsoft Corporation #include "datatype_decl_plugin.h" #include "reg_decl_plugins.h" #include "ast_pp.h" +#include "dt2bv.h" //include static expr_ref mk_const(ast_manager& m, char const* name, sort* s) { @@ -72,6 +73,18 @@ static void test2() { g->assert_expr(m.mk_not(m.mk_eq(x, r))); g->assert_expr(m.mk_not(m.mk_eq(x, b))); g->display(std::cout); + tactic_ref dt2bv = mk_dt2bv_tactic(m); + goal_ref_buffer result; + model_converter_ref mc; + proof_converter_ref pc; + expr_dependency_ref core; + (*dt2bv)(g, result, mc, pc, core); + model_ref mdl1 = alloc(model, m); + model_ref mdl2 = (*mc)(*mdl1); + expr_ref val(m); + mdl2->eval(x, val); + std::cout << val << "\n"; + } void tst_get_consequences() {