mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

have solver pretty print declarations, include also datatype declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-07 08:52:27 +02:00
parent 7f517c625f
commit 052ac51ed7
1 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast_pp_util.cpp
View file

@ -48,24 +48,20 @@ void ast_pp_util::display_decls(std::ostream& out) {
}
void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
func_decl_ref asrt(m);
expr_ref e(m);
sort* b = m.mk_bool_sort();
asrt = m.mk_func_decl(symbol("assert"), 1, &b, b);
if (neat) {
smt2_pp_environment_dbg env(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
e = m.mk_app(asrt, fmls[i]);
ast_smt2_pp(out, e, env);
out << "\n";
out << "(assert ";
ast_smt2_pp(out, fmls[i], env);
out << ")\n";
}
}
else {
ast_smt_pp ll_smt2_pp(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
e = m.mk_app(asrt, fmls[i]);
ll_smt2_pp.display_expr_smt2(out, e);
out << "\n";
out << "(assert ";
ll_smt2_pp.display_expr_smt2(out, fmls[i]);
out << ")\n";
}
}
}