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

fix (get-proof) command to respect option pp.simplify_implies (#7157)

Browse source
This commit is contained in:
someplaceguy 2024-03-09 23:13:42 +00:00 committed by GitHub
parent 361e04a18e
commit 7bbe3fb2b6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast_smt_pp.cpp
View file

@ -986,7 +986,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
ast_mark sort_mark; ast_mark sort_mark;
for (sort* s : decls.get_sorts()) { for (sort* s : decls.get_sorts()) {
if (!(*m_is_declared)(s)) { if (!(*m_is_declared)(s)) {
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); smt_printer p(strm, m, ql, rn, m_logic, true, m_simplify_implies, 0);
p.pp_sort_decl(sort_mark, s); p.pp_sort_decl(sort_mark, s);
} }
} }
@ -994,7 +994,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
for (unsigned i = 0; i < decls.get_num_decls(); ++i) { for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
func_decl* d = decls.get_func_decls()[i]; func_decl* d = decls.get_func_decls()[i];
if (!(*m_is_declared)(d)) { if (!(*m_is_declared)(d)) {
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); smt_printer p(strm, m, ql, rn, m_logic, true, m_simplify_implies, 0);
p(d); p(d);
strm << "\n"; strm << "\n";
} }
@ -1003,20 +1003,20 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
#endif #endif
for (expr* a : m_assumptions) { for (expr* a : m_assumptions) {
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 1);
strm << "(assert\n "; strm << "(assert\n ";
p(a); p(a);
strm << ")\n"; strm << ")\n";
} }
for (expr* a : m_assumptions_star) { for (expr* a : m_assumptions_star) {
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 1);
strm << "(assert\n "; strm << "(assert\n ";
p(a); p(a);
strm << ")\n"; strm << ")\n";
} }
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0); smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 0);
if (m.is_bool(n)) { if (m.is_bool(n)) {
if (!m.is_true(n)) { if (!m.is_true(n)) {
strm << "(assert\n "; strm << "(assert\n ";

1
src/cmd_context/basic_cmds.cpp
View file

@ -202,6 +202,7 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
cmd_is_declared isd(ctx); cmd_is_declared isd(ctx);
pp.set_is_declared(&isd); pp.set_is_declared(&isd);
pp.set_logic(ctx.get_logic()); pp.set_logic(ctx.get_logic());
pp.set_simplify_implies(params.simplify_implies());
pp.display_smt2(ctx.regular_stream(), pr); pp.display_smt2(ctx.regular_stream(), pr);
ctx.regular_stream() << std::endl; ctx.regular_stream() << std::endl;
} }