mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Improved FPA models of partial theory functions

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-13 19:50:51 +01:00
parent de15932f4c
commit 2165c09def
1 changed files with 27 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -120,9 +120,9 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
res = m_fpa_util.mk_value(fp_val); res = m_fpa_util.mk_value(fp_val);
TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) << TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
" " << mk_ismt2_pp(exp, m) << " " << mk_ismt2_pp(exp, m) <<
" " << mk_ismt2_pp(sig, m) << "] == " << " " << mk_ismt2_pp(sig, m) << "] == " <<
mk_ismt2_pp(res, m) << std::endl;); mk_ismt2_pp(res, m) << std::endl;);
m_fpa_util.fm().del(fp_val); m_fpa_util.fm().del(fp_val);
return res; return res;
@ -263,7 +263,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
unsigned arity = bv_f->get_arity(); unsigned arity = bv_f->get_arity();
func_interp * bv_fi = mc->get_func_interp(bv_f); func_interp * bv_fi = mc->get_func_interp(bv_f);
if (bv_fi != 0) { if (bv_fi) {
fpa_rewriter rw(m); fpa_rewriter rw(m);
expr_ref ai(m); expr_ref ai(m);
result = alloc(func_interp, m, arity); result = alloc(func_interp, m, arity);
@ -384,7 +384,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
expr * bvval = to_app(val)->get_arg(0); expr * bvval = to_app(val)->get_arg(0);
expr_ref fv(m); expr_ref fv(m);
fv = convert_bv2rm(mc, to_app(bvval)); fv = convert_bv2rm(mc, to_app(bvval));
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;); TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
target_model->register_decl(var, fv); target_model->register_decl(var, fv);
seen.insert(to_app(bvval)->get_decl()); seen.insert(to_app(bvval)->get_decl());
} }
@ -455,11 +455,14 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
// Upon request, add this 'recursive' definition? // Upon request, add this 'recursive' definition?
func_interp * fmv = convert_func_interp(mc, f, it->m_value); func_interp * fmv = convert_func_interp(mc, f, it->m_value);
unsigned n = fmv->get_arity(); if (fmv) {
expr_ref_vector args(m); unsigned n = fmv->get_arity();
for (unsigned i = 0; i < n; i++) expr_ref_vector args(m);
args.push_back(m.mk_var(i, f->get_domain()[i])); for (unsigned i = 0; i < n; i++)
fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); args.push_back(m.mk_var(i, f->get_domain()[i]));
fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
target_model->register_decl(f, fmv);
}
} }
else { else {
func_interp * fmv = convert_func_interp(mc, f, it->m_value); func_interp * fmv = convert_func_interp(mc, f, it->m_value);
@ -554,21 +557,20 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) { void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
TRACE("bv2fpa", tout << "BV Model: " << std::endl; TRACE("bv2fpa", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++) for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " << tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) { for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i); func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl; tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f); func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) { for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j); func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++) { for (unsigned k = 0; k < f->get_arity(); k++)
tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
} }
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
} });
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
} }