mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Bugfixes for model verification of unspecified values of fp.min/fp.max

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-02 19:25:44 +00:00
parent 14d2356a32
commit 92152b16ca
6 changed files with 131 additions and 113 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,10 +36,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_mpf_manager(m_util.fm()),
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_hi_fp_unspecified(true),
m_min_pn_zeros(0, m),
m_min_np_zeros(0, m),
m_max_pn_zeros(0, m),
m_max_np_zeros(0, m),
m_extra_assertions(m) {
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m.mk_family_id("fpa")));
}
@ -1154,22 +1150,22 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
// The hardware interpretation is -0.0.
mk_nzero(f, res);
else {
if (m_min_pn_zeros == 0) {
m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl());
}
if (m_min_np_zeros == 0) {
m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl());
std::pair<app*, app*> decls(0, 0);
if (!m_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.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(m_min_pn_zeros,
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(m_min_np_zeros,
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
@ -1243,22 +1239,22 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
// The hardware interpretation is +0.0.
mk_pzero(f, res);
else {
if (m_max_pn_zeros == 0) {
m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl());
}
if (m_max_np_zeros == 0) {
m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl());
std::pair<app*, app*> decls(0, 0);
if (!m_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.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(m_max_pn_zeros,
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(m_max_np_zeros,
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
@ -3839,14 +3835,16 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}
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);
m_min_np_zeros = 0;
m_min_pn_zeros = 0;
m_max_np_zeros = 0;
m_max_pn_zeros = 0;
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
}
m_extra_assertions.reset();
}

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

@ -54,12 +54,10 @@ protected:
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
app_ref m_min_pn_zeros;
app_ref m_min_np_zeros;
app_ref m_max_pn_zeros;
app_ref m_max_np_zeros;
obj_map<func_decl, std::pair<app *, app *> > m_specials;
friend class fpa2bv_model_converter;
public:
fpa2bv_converter(ast_manager & m);
@ -153,11 +151,6 @@ public:
expr_ref mk_to_sbv_unspecified(unsigned width);
expr_ref mk_to_real_unspecified();
obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
obj_hashtable<func_decl> const & decls_to_hide() const { return m_decls_to_hide; }
void reset(void);
void dbg_decouple(const char * prefix, expr_ref & e);

4
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -439,7 +439,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
return BR_DONE;
return BR_REWRITE1;
}
else {
scoped_mpf r(m_fm);
@ -474,7 +474,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
return BR_DONE;
return BR_REWRITE1;
}
else {
scoped_mpf r(m_fm);

56
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -45,6 +45,15 @@ 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<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.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.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
}
out << ")" << std::endl;
}
@ -79,12 +88,16 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * k = translator(*it);
res->m_decls_to_hide.insert(k);
func_decl * k = translator(it->m_key);
app * v1 = translator(it->m_value.first);
app * v2 = translator(it->m_value.second);
res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
translator.to().inc_ref(k);
translator.to().inc_ref(v1);
translator.to().inc_ref(v2);
}
return res;
}
@ -217,10 +230,29 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
obj_hashtable<func_decl> seen;
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++)
seen.insert(*it);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * f = it->m_key;
expr_ref pzero(m), nzero(m);
pzero = fu.mk_pzero(f->get_range());
nzero = fu.mk_nzero(f->get_range());
expr_ref pn(m), np(m);
bv_mdl->eval(it->m_value.first, pn, true);
bv_mdl->eval(it->m_value.second, np, true);
seen.insert(it->m_value.first->get_decl());
seen.insert(it->m_value.second->get_decl());
func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
expr * pn_args[2] = { pzero, nzero };
if (pn != np) flt_fi->insert_new_entry(pn_args, (m.is_true(pn) ? nzero : pzero));
flt_fi->set_else(m.is_true(np) ? nzero : pzero);
float_mdl->register_decl(f, flt_fi);
TRACE("fpa2bv_mc", tout << "fp.min/fp.max special: " << std::endl <<
mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;);
}
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
@ -362,10 +394,6 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
}
}
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide);
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) {
return alloc(fpa2bv_model_converter, m, conv);
}

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

@ -27,44 +27,41 @@ class fpa2bv_model_converter : public model_converter {
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_hashtable<func_decl> m_decls_to_hide;
obj_map<func_decl, std::pair<app*, app*> > m_specials;
public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide) :
m(m) {
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
it != const2bv.end();
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) {
for (obj_map<func_decl, expr*>::iterator it = conv.m_const2bv.begin();
it != conv.m_const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, expr*>::iterator it = rm_const2bv.begin();
it != rm_const2bv.end();
for (obj_map<func_decl, expr*>::iterator it = conv.m_rm_const2bv.begin();
it != conv.m_rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
it != uf2bvuf.end();
for (obj_map<func_decl, func_decl*>::iterator it = conv.m_uf2bvuf.begin();
it != conv.m_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_hashtable<func_decl>::iterator it = decls_to_hide.begin();
it != decls_to_hide.end();
it++)
{
m_decls_to_hide.insert(*it);
m.inc_ref(*it);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_specials.begin();
it != conv.m_specials.end();
it++) {
m_specials.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value.first);
m.inc_ref(it->m_value.second);
}
}
@ -72,7 +69,13 @@ public:
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);
dec_ref_collection_values(m, m_decls_to_hide);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
}
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
@ -92,7 +95,7 @@ public:
virtual model_converter * translate(ast_translation & translator);
protected:
fpa2bv_model_converter(ast_manager & m) : m(m) { }
fpa2bv_model_converter(ast_manager & m) : m(m){ }
void convert(model * bv_mdl, model * float_mdl);
expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const;
@ -102,10 +105,6 @@ protected:
};
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_hashtable<func_decl> const & decls_to_hide);
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv);
#endif

2
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -105,7 +105,7 @@ class fpa2bv_tactic : public tactic {
}
if (g->models_enabled())
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide());
mc = mk_fpa2bv_model_converter(m, m_conv);
g->inc_depth();
result.push_back(g.get());