diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 0a14d9473..4dcdd2a35 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -10,6 +10,7 @@ z3_add_component(ast ast_printer.cpp ast_smt2_pp.cpp ast_smt_pp.cpp + ast_pp_dot.cpp ast_translation.cpp ast_util.cpp bv_decl_plugin.cpp diff --git a/src/ast/ast_pp_dot.cpp b/src/ast/ast_pp_dot.cpp new file mode 100644 index 000000000..8e3406ccb --- /dev/null +++ b/src/ast/ast_pp_dot.cpp @@ -0,0 +1,126 @@ +/*++ + +Abstract: Pretty-printer for proofs in Graphviz format + +--*/ + +#include "util/util.h" +#include "util/map.h" +#include "ast_pp_dot.h" + +// string escaping for DOT +std::string escape_dot(std::string const & s) { + std::string res; + for (auto c : s) { + if (c == '\n') + res.append("\\l"); + else + res.push_back(c); + } + return res; +} + +// map from proofs to unique IDs +typedef map, default_eq > expr2id; +typedef map, default_eq > set_expr; + +// temporary structure for traversing the proof and printing it +struct ast_pp_dot_st { + const ast_pp_dot * m_pp; + set_expr m_printed; + expr2id m_id_map; + svector m_to_print; + std::ostream & m_out; + unsigned m_next_id; + + ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) : + m_pp(pp), + m_out(out), + m_next_id(0), + m_id_map(), + m_to_print(), + m_printed() {} + + void push_term(const expr * a) { m_to_print.push_back(a); } + + void pp_loop() { + // DFS traversal + auto& m = get_manager(); + while (!m_to_print.empty()) { + const expr * a = m_to_print.back(); + m_to_print.pop_back(); + if (!m_printed.contains(a)) { + m_printed.insert(a, true); + if (m.is_proof(a)) + pp_step(to_app(a)); + else + pp_atomic_step(a); + } + } + } + +private: + + ast_manager & get_manager() const { return m_pp->get_manager(); } + + // label for an expression + std::string label_of_expr(const expr * e) const { + expr_ref er((expr*)e, get_manager()); + std::ostringstream out; + out << er << std::flush; + return escape_dot(out.str()); + } + + void pp_atomic_step(const expr * e) { + unsigned id = get_id(e); + m_out << "node_" << id << " [shape=box,label=\"" << label_of_expr(e) << "\"] ;" << std::endl; + } + + void pp_step(const proof * p) { + auto m = get_manager(); + unsigned num_args = p->get_num_args(); + TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << num_args); + if (num_args > 0) { + // print result + expr* p_res = p->get_args()[num_args-1]; // result + unsigned id = get_id(p); + m_out << "node_" << id << " [shape=box,label=\"" << label_of_expr(p_res) << "\"]" << std::endl; + // now print edges to parents (except last one, which is the result) + std::string label = p->get_decl()->get_name().str(); + for (unsigned i = 0 ; i+1 < num_args; ++i) { + expr* parent = p->get_args()[i]; + // explore parent, also print a link to it + push_term(to_app(parent)); + m_out << "node_" << id << " -> " << "node_" << get_id((expr*)parent) + << "[label=\"" << label << "\"];" << std::endl;; + } + } else { + pp_atomic_step(p); + } + } + + // find a unique ID for this proof + unsigned get_id(const expr * e) { + if (m_id_map.contains(e)) { + return m_id_map[e]; + } else { + auto id = m_next_id ++; + m_id_map.insert(e, id); + return id; + } + } + +}; + +// main printer +std::ostream & ast_pp_dot::pp(std::ostream & out) const { + out << "digraph proof { " << std::endl; + ast_pp_dot_st pp_st(this, out); + pp_st.push_term(m_pr); + pp_st.pp_loop(); + out << std::endl << " } " << std::endl << std::flush; + return out; +} + +std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p) { return p.pp(out); } + diff --git a/src/ast/ast_pp_dot.h b/src/ast/ast_pp_dot.h new file mode 100644 index 000000000..38c45e00b --- /dev/null +++ b/src/ast/ast_pp_dot.h @@ -0,0 +1,24 @@ +/*++ + +Abstract: Pretty-printer for proofs in Graphviz format + +--*/ + +#pragma once + +#include +#include "ast_pp.h" + +class ast_pp_dot { + ast_manager & m_manager; + proof * const m_pr; + + public: + ast_pp_dot(proof *pr, ast_manager &m) : m_manager(m), m_pr(pr) {} + ast_pp_dot(proof_ref &e) : m_manager(e.m()), m_pr(e.get()) {} + + std::ostream & pp(std::ostream & out) const; + ast_manager & get_manager() const { return m_manager; } +}; + +std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p); \ No newline at end of file diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 21b66febd..60dd09f59 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -20,6 +20,7 @@ Notes: #include "util/version.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_pp_dot.h" #include "ast/ast_pp.h" #include "ast/array_decl_plugin.h" #include "ast/pp.h" @@ -202,6 +203,25 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { } }); +ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it in graphviz", { + if (!ctx.produce_proofs()) + throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)"); + if (!ctx.has_manager() || + ctx.cs_state() != cmd_context::css_unsat) + throw cmd_exception("proof is not available"); + proof_ref pr(ctx.m()); + pr = ctx.get_check_sat_result()->get_proof(); + if (pr == 0) + throw cmd_exception("proof is not available"); + if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) { + throw cmd_exception("proof is not well sorted"); + } + + // TODO: specify file into which the proof should be printed + std::ofstream out("proof.dot"); + out << ast_pp_dot(pr) << std::endl; +}); + static void print_core(cmd_context& ctx) { ptr_vector core; ctx.get_check_sat_result()->get_unsat_core(core); @@ -840,6 +860,7 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(get_assignment_cmd)); ctx.insert(alloc(get_assertions_cmd)); ctx.insert(alloc(get_proof_cmd)); + ctx.insert(alloc(get_proof_graph_cmd)); ctx.insert(alloc(get_unsat_core_cmd)); ctx.insert(alloc(set_option_cmd)); ctx.insert(alloc(get_option_cmd));