mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models.

Browse source 
Fixes
This commit is contained in:
Christoph M. Wintersteiger 2016-06-09 17:51:31 +01:00
parent bfeab9cc15
commit bd187e0989
5 changed files with 38 additions and 43 deletions

10
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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<app*, app*> 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<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
for (obj_map<func_decl, std::pair<app*, app*> >::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();
}

22
src/ast/fpa/fpa2bv_converter.h
View file

@ -32,6 +32,11 @@ Notes:
#include"basic_simplifier_plugin.h"
class fpa2bv_converter {
public:
typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
typedef obj_map<func_decl, expr*> const2bv_t;
typedef obj_map<func_decl, func_decl*> 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<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, std::pair<app *, app *> > 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);

42
src/smt/theory_fpa.cpp
View file

@ -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;
}

3
src/smt/theory_fpa.h
View file

@ -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 {

4
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -64,8 +64,8 @@ public:
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_specials.begin();
it != conv.m_specials.end();
for (obj_map<func_decl, std::pair<app*, app*> >::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);