From 78db1d0f86c35b424522ea600b52f9604c2e1eae Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 1 May 2013 16:13:24 -0700 Subject: [PATCH 1/4] fix build of unit tests Signed-off-by: Nuno Lopes --- src/smt/diff_logic.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index f6576a41f..7216bba7e 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -21,6 +21,7 @@ Revision History: #include"vector.h" #include"heap.h" +#include"statistics.h" #include"trace.h" #include"warning.h" From 00d5dea9a5694aae8df2d9a78ae7fce04effd4af Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 2 May 2013 15:24:07 +0100 Subject: [PATCH 2/4] FPA: added support for rewriting quantified floats to quantified bit-vectors. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 14 +++++ src/tactic/fpa/fpa2bv_converter.h | 4 +- src/tactic/fpa/fpa2bv_rewriter.h | 84 +++++++++++++++++++++++++++-- 3 files changed, 98 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 84a1efaff..2e2a270ee 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -150,6 +150,20 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { } } +void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) { + SASSERT(is_float(srt)); + unsigned ebits = m_util.get_ebits(srt); + unsigned sbits = m_util.get_sbits(srt); + + expr_ref sgn(m), s(m), e(m); + + sgn = m.mk_var(base_inx, m_bv_util.mk_sort(1)); + s = m.mk_var(base_inx + 1, m_bv_util.mk_sort(sbits-1)); + e = m.mk_var(base_inx + 2, m_bv_util.mk_sort(ebits)); + + mk_triple(sgn, s, e, result); +} + void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { SASSERT(f->get_family_id() == null_family_id); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index e5d546763..4ed794a7c 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -35,7 +35,7 @@ class fpa2bv_converter { ast_manager & m; basic_simplifier_plugin m_simp; float_util m_util; - mpf_manager & m_mpf_manager; + mpf_manager & m_mpf_manager; unsynch_mpz_manager & m_mpz_manager; bv_util m_bv_util; float_decl_plugin * m_plugin; @@ -48,6 +48,7 @@ public: ~fpa2bv_converter(); float_util & fu() { return m_util; } + bv_util & bu() { return m_bv_util; } bool is_float(sort * s) { return m_util.is_float(s); } bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); } @@ -68,6 +69,7 @@ public: void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_const(func_decl * f, expr_ref & result); void mk_rm_const(func_decl * f, expr_ref & result); + void mk_var(unsigned base_inx, sort * srt, expr_ref & result); void mk_plus_inf(func_decl * f, expr_ref & result); void mk_minus_inf(func_decl * f, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 4b3525a32..02b40840a 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -29,6 +29,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { ast_manager & m_manager; expr_ref_vector m_out; fpa2bv_converter & m_conv; + sort_ref_vector m_bindings; + expr_ref_vector m_mappings; unsigned long long m_max_memory; unsigned m_max_steps; @@ -38,7 +40,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p): m_manager(m), m_out(m), - m_conv(c) { + m_conv(c), + m_bindings(m), + m_mappings(m) { updt_params(p); // We need to make sure that the mananger has the BV plugin loaded. symbol s_bv("bv"); @@ -53,6 +57,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { m_out.finalize(); } + void reset() { + } + void updt_params(params_ref const & p) { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_steps = p.get_uint("max_steps", UINT_MAX); @@ -140,17 +147,88 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { return BR_FAILED; } + bool pre_visit(expr * t) + { + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("fpa2bv", tout << "pre_visit [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + sort_ref_vector new_bindings(m_manager); + for (unsigned i = 0 ; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + m_mappings.resize(m_bindings.size(), 0); + } + return true; + } + bool reduce_quantifier(quantifier * old_q, expr * new_body, expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { - return false; + unsigned curr_sz = m_bindings.size(); + SASSERT(old_q->get_num_decls() <= curr_sz); + unsigned num_decls = old_q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + string_buffer<> name_buffer; + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + for (unsigned i = 0; i < num_decls; i++) { + symbol const & n = old_q->get_decl_name(i); + sort * s = old_q->get_decl_sort(i); + if (m_conv.is_float(s)) { + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + name_buffer.reset(); + name_buffer << n << ".exp"; + new_decl_names.push_back(symbol(name_buffer.c_str())); + new_decl_sorts.push_back(m_conv.bu().mk_sort(ebits)); + name_buffer.reset(); + name_buffer << n << ".sig"; + new_decl_names.push_back(symbol(name_buffer.c_str())); + new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits-1)); + name_buffer.reset(); + name_buffer << n << ".sgn"; + new_decl_names.push_back(symbol(name_buffer.c_str())); + new_decl_sorts.push_back(m_conv.bu().mk_sort(1)); + } + else { + new_decl_sorts.push_back(s); + new_decl_names.push_back(n); + } + } + result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), + new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), + old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + m_bindings.shrink(old_sz); + m_mappings.shrink(old_sz); + TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << + " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + return true; } bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { - return false; + if (t->get_idx() >= m_bindings.size()) + return false; + unsigned inx = m_bindings.size() - t->get_idx() - 1; + if (m_mappings[inx] == 0) + { + unsigned shift = 0; + for (unsigned i = m_bindings.size() - 1; i > inx; i--) + if (m_conv.is_float(m_bindings[i].get())) shift += 2; + expr_ref new_var(m()); + m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var); + m_mappings[inx] = new_var; + } + result = m_mappings[inx].get(); + result_pr = 0; + TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); + return true; } }; From 8f60a936d2b0f0f0a9f71f3c8339cd364e3d2750 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 May 2013 15:57:42 +0100 Subject: [PATCH 3/4] FPA: Added support for float-UF to BV-UF translation. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 98 ++++++++++++++++++++++++++++- src/tactic/fpa/fpa2bv_converter.h | 20 +++++- src/tactic/fpa/fpa2bv_rewriter.h | 22 ++++++- 3 files changed, 136 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 2e2a270ee..acb41a2b1 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -38,6 +38,17 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : fpa2bv_converter::~fpa2bv_converter() { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); + dec_ref_map_key_values(m, m_uf2bvuf); + + obj_map::iterator it = m_uf23bvuf.begin(); + obj_map::iterator end = m_uf23bvuf.end(); + for (; it != end; ++it) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.f_sgn); + m.dec_ref(it->m_value.f_sig); + m.dec_ref(it->m_value.f_exp); + } + m_uf23bvuf.reset(); } void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { @@ -164,6 +175,90 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) mk_triple(sgn, s, e, result); } +void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) +{ + TRACE("fpa2bv_dbg", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; ); + SASSERT(f->get_arity() == num); + + expr_ref_buffer new_args(m); + + for (unsigned i = 0; i < num ; i ++) + if (is_float(args[i])) + { + expr * sgn, * sig, * exp; + split(args[i], sgn, sig, exp); + new_args.push_back(sgn); + new_args.push_back(sig); + new_args.push_back(exp); + } + else + new_args.push_back(args[i]); + + func_decl * fd; + func_decl_triple fd3; + if (m_uf2bvuf.find(f, fd)) { + result = m.mk_app(fd, new_args.size(), new_args.c_ptr()); + } + else if (m_uf23bvuf.find(f, fd3)) + { + expr_ref a_sgn(m), a_sig(m), a_exp(m); + a_sgn = m.mk_app(fd3.f_sgn, new_args.size(), new_args.c_ptr()); + a_sig = m.mk_app(fd3.f_sig, new_args.size(), new_args.c_ptr()); + a_exp = m.mk_app(fd3.f_exp, new_args.size(), new_args.c_ptr()); + mk_triple(a_sgn, a_sig, a_exp, result); + } + else { + sort_ref_buffer new_domain(m); + + for (unsigned i = 0; i < f->get_arity() ; i ++) + if (is_float(f->get_domain()[i])) + { + new_domain.push_back(m_bv_util.mk_sort(1)); + new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(f->get_domain()[i])-1)); + new_domain.push_back(m_bv_util.mk_sort(m_util.get_ebits(f->get_domain()[i]))); + } + else + new_domain.push_back(f->get_domain()[i]); + + if (!is_float(f->get_range())) + { + func_decl * fbv = m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range(), *f->get_info()); + TRACE("fpa2bv_dbg", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl; ); + m_uf2bvuf.insert(f, fbv); + m.inc_ref(f); + m.inc_ref(fbv); + result = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); + } + else + { + string_buffer<> name_buffer; + name_buffer.reset(); name_buffer << f->get_name() << ".sgn"; + func_decl * f_sgn = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(1)); + name_buffer.reset(); name_buffer << f->get_name() << ".sig"; + func_decl * f_sig = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_sbits(f->get_range())-1)); + name_buffer.reset(); name_buffer << f->get_name() << ".exp"; + func_decl * f_exp = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_ebits(f->get_range()))); + expr_ref a_sgn(m), a_sig(m), a_exp(m); + a_sgn = m.mk_app(f_sgn, new_args.size(), new_args.c_ptr()); + a_sig = m.mk_app(f_sig, new_args.size(), new_args.c_ptr()); + a_exp = m.mk_app(f_exp, new_args.size(), new_args.c_ptr()); + TRACE("fpa2bv_dbg", tout << "New UF func_decls : " << std::endl; + tout << mk_ismt2_pp(f_sgn, m) << std::endl; + tout << mk_ismt2_pp(f_sig, m) << std::endl; + tout << mk_ismt2_pp(f_exp, m) << std::endl; ); + m_uf23bvuf.insert(f, func_decl_triple(f_sgn, f_sig, f_exp)); + m.inc_ref(f); + m.inc_ref(f_sgn); + m.inc_ref(f_sig); + m.inc_ref(f_exp); + mk_triple(a_sgn, a_sig, a_exp, result); + } + } + + TRACE("fpa2bv_dbg", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; ); + + SASSERT(is_well_sorted(m, result)); +} void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { SASSERT(f->get_family_id() == null_family_id); @@ -1953,7 +2048,8 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef _DEBUG - // return; + return; + // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); extra_assertions.push_back(m.mk_eq(new_e, e)); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 4ed794a7c..f090e3e8d 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -42,6 +42,21 @@ class fpa2bv_converter { obj_map m_const2bv; obj_map m_rm_const2bv; + obj_map m_uf2bvuf; + + 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) + { + f_sgn = sgn; + f_sig = sig; + f_exp = exp; + } + func_decl * f_sgn; + func_decl * f_sig; + func_decl * f_exp; + }; + obj_map m_uf23bvuf; public: fpa2bv_converter(ast_manager & m); @@ -67,8 +82,9 @@ public: void mk_rounding_mode(func_decl * f, expr_ref & result); void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_const(func_decl * f, expr_ref & result); + void mk_const(func_decl * f, expr_ref & result); void mk_rm_const(func_decl * f, expr_ref & result); + void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_var(unsigned base_inx, sort * srt, expr_ref & result); void mk_plus_inf(func_decl * f, expr_ref & result); @@ -102,7 +118,7 @@ public: void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 02b40840a..aec00d30c 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -143,6 +143,23 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { throw tactic_exception("NYI"); } } + + if (f->get_family_id() == null_family_id) + { + bool is_float_uf = m_conv.is_float(f->get_range()); + unsigned i = 0; + while (!is_float_uf && i < num) + { + is_float_uf = m_conv.is_float(f->get_domain()[i]); + i++; + } + + if (is_float_uf) + { + m_conv.mk_uninterpreted_function(f, num, args, result); + return BR_DONE; + } + } return BR_FAILED; } @@ -222,7 +239,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { for (unsigned i = m_bindings.size() - 1; i > inx; i--) if (m_conv.is_float(m_bindings[i].get())) shift += 2; expr_ref new_var(m()); - m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var); + if (m_conv.is_float(t->get_sort())) + m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var); + else + new_var = m().mk_var(t->get_idx() + shift, t->get_sort()); m_mappings[inx] = new_var; } result = m_mappings[inx].get(); From 121e83b6b7960263b5fec710202a070ad2477ed4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 May 2013 17:54:30 +0100 Subject: [PATCH 4/4] FPA: bugfixes for UF in model converter for fpa2bv. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 44 ++++++++++++++++++++--- src/tactic/fpa/fpa2bv_converter.h | 55 ++++++++++++++++++++--------- src/tactic/fpa/fpa2bv_tactic.cpp | 2 +- 3 files changed, 80 insertions(+), 21 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index acb41a2b1..363cf1df8 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -2403,6 +2403,25 @@ void fpa2bv_model_converter::display(std::ostream & out) { 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; } @@ -2523,6 +2542,20 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { } } + 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. @@ -2530,7 +2563,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { for (unsigned i = 0; i < sz; i++) { func_decl * c = bv_mdl->get_constant(i); - if (!seen.contains(c)) + if (!seen.contains(c)) float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); } @@ -2539,7 +2572,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { for (unsigned i = 0; i < sz; i++) { func_decl * c = bv_mdl->get_function(i); - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + if (!seen.contains(c)) + float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); } sz = bv_mdl->get_num_uninterpreted_sorts(); @@ -2553,6 +2587,8 @@ void fpa2bv_model_converter::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) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_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/tactic/fpa/fpa2bv_converter.h index f090e3e8d..2a68342f8 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -31,20 +31,7 @@ typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2, class fpa2bv_model_converter; -class fpa2bv_converter { - ast_manager & m; - basic_simplifier_plugin m_simp; - float_util m_util; - mpf_manager & m_mpf_manager; - unsynch_mpz_manager & m_mpz_manager; - bv_util m_bv_util; - float_decl_plugin * m_plugin; - - obj_map m_const2bv; - obj_map m_rm_const2bv; - obj_map m_uf2bvuf; - - struct func_decl_triple { +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) { @@ -56,6 +43,19 @@ class fpa2bv_converter { func_decl * f_sig; func_decl * f_exp; }; + +class fpa2bv_converter { + ast_manager & m; + basic_simplifier_plugin m_simp; + float_util m_util; + mpf_manager & m_mpf_manager; + unsynch_mpz_manager & m_mpz_manager; + bv_util m_bv_util; + float_decl_plugin * m_plugin; + + obj_map m_const2bv; + obj_map m_rm_const2bv; + obj_map m_uf2bvuf; obj_map m_uf23bvuf; public: @@ -122,6 +122,8 @@ public: obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } + obj_map const & uf2bvuf() const { return m_uf2bvuf; } + obj_map const & uf23bvuf() const { return m_uf23bvuf; } void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector extra_assertions; @@ -166,10 +168,14 @@ 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 & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf) : m(m) { // Just create a copy? for (obj_map::iterator it = const2bv.begin(); @@ -188,6 +194,21 @@ public: 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() { @@ -220,6 +241,8 @@ protected: model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv); + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf); #endif diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index a90ff9317..9bb35eea6 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic { } if (g->models_enabled()) - mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv()); + mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.uf23bvuf()); g->inc_depth(); result.push_back(g.get());