From bd187e098988c57b5dc8e75480c42717ffeb3482 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 9 Jun 2016 17:51:31 +0100 Subject: [PATCH] Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. Fixes #642 --- src/ast/fpa/fpa2bv_converter.cpp | 10 +++--- src/ast/fpa/fpa2bv_converter.h | 22 ++++++++----- src/smt/theory_fpa.cpp | 42 ++++++++++--------------- src/smt/theory_fpa.h | 3 -- src/tactic/fpa/fpa2bv_model_converter.h | 4 +-- 5 files changed, 38 insertions(+), 43 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6e74f60b1..d833e2381 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1273,10 +1273,10 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr // There is no "hardware interpretation" for fp.min/fp.max. std::pair decls(0, 0); - if (!m_specials.find(f, decls)) { + if (!m_min_max_specials.find(f, decls)) { decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_specials.insert(f, decls); + m_min_max_specials.insert(f, decls); m.inc_ref(f); m.inc_ref(decls.first); m.inc_ref(decls.second); @@ -4100,13 +4100,13 @@ void fpa2bv_converter::reset(void) { 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); - for (obj_map >::iterator it = m_specials.begin(); - it != m_specials.end(); + for (obj_map >::iterator it = m_min_max_specials.begin(); + it != m_min_max_specials.end(); it++) { m.dec_ref(it->m_key); m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } - m_specials.reset(); + m_min_max_specials.reset(); m_extra_assertions.reset(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 45030b301..3f5e76c66 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -32,6 +32,11 @@ Notes: #include"basic_simplifier_plugin.h" class fpa2bv_converter { +public: + typedef obj_map > special_t; + typedef obj_map const2bv_t; + typedef obj_map uf2bvuf_t; + protected: ast_manager & m; basic_simplifier_plugin m_simp; @@ -46,11 +51,10 @@ protected: fpa_decl_plugin * m_plugin; bool m_hi_fp_unspecified; - obj_map m_const2bv; - obj_map m_rm_const2bv; - obj_map m_uf2bvuf; - - obj_map > m_specials; + const2bv_t m_const2bv; + const2bv_t m_rm_const2bv; + uf2bvuf_t m_uf2bvuf; + special_t m_min_max_specials; friend class fpa2bv_model_converter; @@ -154,9 +158,11 @@ public: void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector m_extra_assertions; - - bool is_special(func_decl * f) { return m_specials.contains(f); } - bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); } + + special_t const & get_min_max_specials() const { return m_min_max_specials; }; + const2bv_t const & get_const2bv() const { return m_const2bv; }; + const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }; + uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; }; protected: void mk_one(func_decl *f, expr_ref & sign, expr_ref & result); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 6038867aa..8e96c925d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -83,27 +83,6 @@ namespace smt { } } - void theory_fpa::fpa2bv_converter_wrapped::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - // Note: this introduces new UFs that should be filtered afterwards. - return fpa2bv_converter::mk_function(f, num, args, result); - } - - expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) { - expr_ref a(m), wrapped(m), wu(m), wu_eq(m); - a = m.mk_app(f, x, y); - wrapped = m_th.wrap(a); - wu = m_th.unwrap(wrapped, f->get_range()); - wu_eq = m.mk_eq(wu, a); - m_extra_assertions.push_back(wu_eq); - - unsigned bv_sz = m_bv_util.get_bv_size(wrapped); - expr_ref sc(m); - sc = m.mk_eq(m_bv_util.mk_extract(bv_sz-2, 0, wrapped), m_bv_util.mk_numeral(0, bv_sz-1)); - m_extra_assertions.push_back(sc); - - return wu; - } - theory_fpa::theory_fpa(ast_manager & m) : theory(m.mk_family_id("fpa")), m_converter(m, this), @@ -727,8 +706,23 @@ namespace smt { void theory_fpa::init_model(model_generator & mg) { TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout);); - m_factory = alloc(fpa_value_factory, get_manager(), get_family_id()); - mg.register_factory(m_factory); + ast_manager & m = get_manager(); + m_factory = alloc(fpa_value_factory, m, get_family_id()); + mg.register_factory(m_factory); + + fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf(); + for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin(); + it != uf2bvuf.end(); + it++) { + mg.hide(it->m_value); + } + fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials(); + for (fpa2bv_converter::special_t::iterator it = specials.begin(); + it != specials.end(); + it++) { + mg.hide(it->m_value.first->get_decl()); + mg.hide(it->m_value.second->get_decl()); + } } model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { @@ -882,8 +876,6 @@ namespace smt { } return false; } - else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f)) - return false; else return true; } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 32fcfcffc..2b327eb66 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -83,9 +83,6 @@ namespace smt { 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); - virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - - virtual expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y); }; class fpa_value_proc : public model_value_proc { diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 0e92841de..909a7cb78 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -64,8 +64,8 @@ public: m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map >::iterator it = conv.m_specials.begin(); - it != conv.m_specials.end(); + for (obj_map >::iterator it = conv.m_min_max_specials.begin(); + it != conv.m_min_max_specials.end(); it++) { m_specials.insert(it->m_key, it->m_value); m.inc_ref(it->m_key);