mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Adjusted default model display for float literals.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-28 13:31:30 +00:00
parent 65cc5fbe8b
commit 7f8a34d2e1
2 changed files with 26 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/ast/ast_smt2_pp.cpp
View file

@ -222,7 +222,7 @@ format * smt2_pp_environment::pp_bv_literal(app * t, bool use_bv_lits, bool bv_n
return vf; return vf;
} }
format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) { format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits) {
mpf_manager & fm = get_futil().fm(); mpf_manager & fm = get_futil().fm();
scoped_mpf v(fm); scoped_mpf v(fm);
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -231,28 +231,38 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
VERIFY(get_futil().is_value(t, v)); VERIFY(get_futil().is_value(t, v));
if (fm.is_nan(v)) { if (fm.is_nan(v)) {
buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
return mk_string(get_manager(), buf.c_str()); return mk_string(m, buf.c_str());
} }
else if (fm.is_pinf(v)) { else if (fm.is_pinf(v)) {
buf << "(_ +oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; buf << "(_ +oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
return mk_string(get_manager(), buf.c_str()); return mk_string(m, buf.c_str());
} }
else if (fm.is_ninf(v)) { else if (fm.is_ninf(v)) {
buf << "(_ -oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; buf << "(_ -oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
return mk_string(get_manager(), buf.c_str()); return mk_string(m, buf.c_str());
} }
else if (fm.is_pzero(v)) { else if (fm.is_pzero(v)) {
buf << "(_ +zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; buf << "(_ +zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
return mk_string(get_manager(), buf.c_str()); return mk_string(m, buf.c_str());
} }
else if (fm.is_nzero(v)) { else if (fm.is_nzero(v)) {
buf << "(_ -zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; buf << "(_ -zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
return mk_string(get_manager(), buf.c_str()); return mk_string(m, buf.c_str());
}
else if (use_float_real_lits)
{
buf << "((_ to_fp " << v.get().get_ebits() << " " <<
v.get().get_sbits() << ") RTZ " <<
fm.to_string(v).c_str() << ")";
return mk_string(m, buf.c_str());
} }
else { else {
if (use_bv_lits)
buf << "(fp #b" << (fm.sgn(v) ? 1 : 0); buf << "(fp #b" << (fm.sgn(v) ? 1 : 0);
body = mk_string(get_manager(), buf.c_str()); else
body = mk_compose(m, body, mk_string(get_manager(), " ")); buf << "(fp (_ bv" << (fm.sgn(v) ? 1 : 0) << " 1)";
body = mk_string(m, buf.c_str());
body = mk_compose(m, body, mk_string(m, " "));
mpf_exp_t exp = fm.exp(v); mpf_exp_t exp = fm.exp(v);
const mpz & bias = fm.m_powers2.m1(v.get().get_ebits() - 1); const mpz & bias = fm.m_powers2.m1(v.get().get_ebits() - 1);
@ -260,7 +270,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
app_ref e_biased_exp(m); app_ref e_biased_exp(m);
e_biased_exp = get_bvutil().mk_numeral(biased_exp, v.get().get_ebits()); e_biased_exp = get_bvutil().mk_numeral(biased_exp, v.get().get_ebits());
body = mk_compose(m, body, pp_bv_literal(e_biased_exp, use_bv_lits, false)); body = mk_compose(m, body, pp_bv_literal(e_biased_exp, use_bv_lits, false));
body = mk_compose(m, body, mk_string(get_manager(), " ")); body = mk_compose(m, body, mk_string(m, " "));
scoped_mpz sig(fm.mpz_manager()); scoped_mpz sig(fm.mpz_manager());
sig = fm.sig(v); sig = fm.sig(v);
@ -268,7 +278,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits) {
e_sig = get_bvutil().mk_numeral(rational(sig), v.get().get_sbits() - 1); e_sig = get_bvutil().mk_numeral(rational(sig), v.get().get_sbits() - 1);
body = mk_compose(m, body, pp_bv_literal(e_sig, use_bv_lits, false)); body = mk_compose(m, body, pp_bv_literal(e_sig, use_bv_lits, false));
body = mk_compose(m, body, mk_string(get_manager(), ")")); body = mk_compose(m, body, mk_string(m, ")"));
return body; return body;
} }
} }
@ -446,6 +456,7 @@ class smt2_printer {
bool m_pp_decimal; bool m_pp_decimal;
unsigned m_pp_decimal_precision; unsigned m_pp_decimal_precision;
bool m_pp_bv_lits; bool m_pp_bv_lits;
bool m_pp_float_real_lits;
bool m_pp_bv_neg; bool m_pp_bv_neg;
unsigned m_pp_max_depth; unsigned m_pp_max_depth;
unsigned m_pp_min_alias_size; unsigned m_pp_min_alias_size;
@ -565,7 +576,7 @@ class smt2_printer {
f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg); f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
} }
else if (m_env.get_futil().is_value(c)) { else if (m_env.get_futil().is_value(c)) {
f = m_env.pp_float_literal(c, m_pp_bv_lits); f = m_env.pp_float_literal(c, m_pp_bv_lits, m_pp_float_real_lits);
} }
else if (m_env.get_dlutil().is_numeral(c)) { else if (m_env.get_dlutil().is_numeral(c)) {
f = m_env.pp_datalog_literal(c); f = m_env.pp_datalog_literal(c);
@ -1008,6 +1019,7 @@ public:
m_pp_decimal = p.decimal(); m_pp_decimal = p.decimal();
m_pp_decimal_precision = p.decimal_precision(); m_pp_decimal_precision = p.decimal_precision();
m_pp_bv_lits = p.bv_literals(); m_pp_bv_lits = p.bv_literals();
m_pp_float_real_lits = p.fp_real_literals();
m_pp_bv_neg = p.bv_neg(); m_pp_bv_neg = p.bv_neg();
m_pp_max_depth = p.max_depth(); m_pp_max_depth = p.max_depth();
m_pp_min_alias_size = p.min_alias_size(); m_pp_min_alias_size = p.min_alias_size();

2
src/ast/ast_smt2_pp.h
View file

@ -52,7 +52,7 @@ public:
virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len); virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg); virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec); virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits); virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
virtual format_ns::format * pp_datalog_literal(app * t); virtual format_ns::format * pp_datalog_literal(app * t);
virtual format_ns::format * pp_sort(sort * s); virtual format_ns::format * pp_sort(sort * s);
virtual format_ns::format * pp_fdecl_ref(func_decl * f); virtual format_ns::format * pp_fdecl_ref(func_decl * f);