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

Debug traces

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-15 11:48:25 +01:00
parent d82afcc48c
commit ff42c44f37
2 changed files with 17 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -558,22 +558,3 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
return res; return res;
} }
void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
TRACE("bv2fpa", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++)
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
}

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

@ -33,6 +33,23 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
} }
void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++)
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
obj_hashtable<func_decl> seen; obj_hashtable<func_decl> seen;
m_bv2fp->convert_consts(mc, float_mdl, seen); m_bv2fp->convert_consts(mc, float_mdl, seen);
m_bv2fp->convert_rm_consts(mc, float_mdl, seen); m_bv2fp->convert_rm_consts(mc, float_mdl, seen);