From 121e83b6b7960263b5fec710202a070ad2477ed4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 May 2013 17:54:30 +0100 Subject: [PATCH] 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());