From d630838b38f6956aa418c81036c7b60d7d0e4163 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 24 Oct 2017 09:39:16 +0200 Subject: [PATCH 1/4] add a basic printer into graphviz (http://graphviz.org/) for proofs - proofs are output into file `proof.dot` if `(get-proof-graph)` is in the input - use `dot -Txlib proof.dot` to see the proof - use `dot -Tsvg proof.dot` to get a svg file --- src/ast/CMakeLists.txt | 1 + src/ast/ast_pp_dot.cpp | 126 +++++++++++++++++++++++++++++++++ src/ast/ast_pp_dot.h | 24 +++++++ src/cmd_context/basic_cmds.cpp | 21 ++++++ 4 files changed, 172 insertions(+) create mode 100644 src/ast/ast_pp_dot.cpp create mode 100644 src/ast/ast_pp_dot.h 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)); From 24edb8fb47db0c680438c9473212160c93aac2db Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 24 Oct 2017 09:51:47 +0200 Subject: [PATCH 2/4] add some colors to the proof output --- src/ast/ast_pp_dot.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/ast/ast_pp_dot.cpp b/src/ast/ast_pp_dot.cpp index 8e3406ccb..feffa71f1 100644 --- a/src/ast/ast_pp_dot.cpp +++ b/src/ast/ast_pp_dot.cpp @@ -32,6 +32,7 @@ struct ast_pp_dot_st { svector m_to_print; std::ostream & m_out; unsigned m_next_id; + bool m_first; ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) : m_pp(pp), @@ -39,7 +40,8 @@ struct ast_pp_dot_st { m_next_id(0), m_id_map(), m_to_print(), - m_printed() {} + m_printed(), + m_first(true) {} void push_term(const expr * a) { m_to_print.push_back(a); } @@ -73,7 +75,7 @@ private: 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; + m_out << "node_" << id << " [shape=box,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << std::endl; } void pp_step(const proof * p) { @@ -84,7 +86,11 @@ private: // 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; + const char* color = + m_first ? (m_first=false,"color=\"red\"") : num_args==1 ? "color=\"yellow\"": ""; + m_out << "node_" << id << + " [shape=box,style=\"filled\",label=\"" << label_of_expr(p_res) << "\"" + << color << "]" << 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) { From ed526b808d402e5b66bfcb8962ae58568993d00b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 24 Oct 2017 10:16:22 +0200 Subject: [PATCH 3/4] add parameter to specify the file into which dot proofs are to be printed --- src/cmd_context/basic_cmds.cpp | 5 +++-- src/cmd_context/context_params.cpp | 5 +++++ src/cmd_context/context_params.h | 1 + 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 60dd09f59..65c8860b1 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -217,8 +217,9 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it throw cmd_exception("proof is not well sorted"); } - // TODO: specify file into which the proof should be printed - std::ofstream out("proof.dot"); + context_params& params = ctx.params(); + const std::string& file = params.m_dot_proof_file; + std::ofstream out(file); out << ast_pp_dot(pr) << std::endl; }); diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index f8646d41c..78f4223fc 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -111,6 +111,9 @@ void context_params::set(char const * param, char const * value) { else if (p == "trace_file_name") { m_trace_file_name = value; } + else if (p == "dot_proof_file") { + m_dot_proof_file = value; + } else if (p == "unsat_core") { set_bool(m_unsat_core, param, value); } @@ -146,6 +149,7 @@ void context_params::updt_params(params_ref const & p) { m_dump_models = p.get_bool("dump_models", m_dump_models); m_trace = p.get_bool("trace", m_trace); m_trace_file_name = p.get_str("trace_file_name", "z3.log"); + m_dot_proof_file = p.get_str("dot_proof_file", "proof.dot"); m_unsat_core = p.get_bool("unsat_core", m_unsat_core); m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count); m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant); @@ -161,6 +165,7 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); + d.insert("dot_proof_file", CPK_STRING, "file in which to output graphical proofs", "proof.dot"); d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false"); collect_solver_param_descrs(d); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index c238af556..df62057fe 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -30,6 +30,7 @@ class context_params { public: bool m_auto_config; bool m_proof; + std::string m_dot_proof_file; bool m_interpolants; bool m_debug_ref_count; bool m_trace; From 607eba1720da71154f3bccf9bea20e677939327c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 24 Oct 2017 11:44:28 +0200 Subject: [PATCH 4/4] account for review --- src/ast/ast_pp_dot.cpp | 42 ++++++++++++++++++++++-------------------- src/ast/ast_pp_dot.h | 2 +- 2 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/ast/ast_pp_dot.cpp b/src/ast/ast_pp_dot.cpp index feffa71f1..eb4ec80fe 100644 --- a/src/ast/ast_pp_dot.cpp +++ b/src/ast/ast_pp_dot.cpp @@ -11,6 +11,7 @@ Abstract: Pretty-printer for proofs in Graphviz format // string escaping for DOT std::string escape_dot(std::string const & s) { std::string res; + res.reserve(s.size()); // preallocate for (auto c : s) { if (c == '\n') res.append("\\l"); @@ -21,8 +22,8 @@ std::string escape_dot(std::string const & s) { } // map from proofs to unique IDs -typedef map, default_eq > expr2id; -typedef map, default_eq > set_expr; +typedef obj_map expr2id; +typedef obj_map set_expr; // temporary structure for traversing the proof and printing it struct ast_pp_dot_st { @@ -33,6 +34,7 @@ struct ast_pp_dot_st { std::ostream & m_out; unsigned m_next_id; bool m_first; + ast_manager & m_manager; ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) : m_pp(pp), @@ -41,19 +43,21 @@ struct ast_pp_dot_st { m_id_map(), m_to_print(), m_printed(), - m_first(true) {} + m_first(true), + m_manager(pp->get_manager()) {} + + ~ast_pp_dot_st() = default; 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)) + if (m().is_proof(a)) pp_step(to_app(a)); else pp_atomic_step(a); @@ -63,11 +67,11 @@ struct ast_pp_dot_st { private: - ast_manager & get_manager() const { return m_pp->get_manager(); } + inline ast_manager & m() const { return m_manager; } // label for an expression std::string label_of_expr(const expr * e) const { - expr_ref er((expr*)e, get_manager()); + expr_ref er((expr*)e, m()); std::ostringstream out; out << er << std::flush; return escape_dot(out.str()); @@ -79,22 +83,21 @@ private: } 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) { + if (m().has_fact(p)) { // print result - expr* p_res = p->get_args()[num_args-1]; // result + expr* p_res = m().get_fact(p); // result of proof step unsigned id = get_id(p); + unsigned num_parents = m().get_num_parents(p); const char* color = - m_first ? (m_first=false,"color=\"red\"") : num_args==1 ? "color=\"yellow\"": ""; + m_first ? (m_first=false,"color=\"red\"") : num_parents==0 ? "color=\"yellow\"": ""; m_out << "node_" << id << " [shape=box,style=\"filled\",label=\"" << label_of_expr(p_res) << "\"" << color << "]" << 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]; + for (unsigned i = 0 ; i < num_parents; ++i) { + expr* parent = m().get_parent(p, i); // explore parent, also print a link to it push_term(to_app(parent)); m_out << "node_" << id << " -> " << "node_" << get_id((expr*)parent) @@ -107,13 +110,12 @@ private: // 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; + unsigned id = 0; + if (!m_id_map.find(e, id)) { + id = m_next_id++; + m_id_map.insert(e, id); } + return id; } }; diff --git a/src/ast/ast_pp_dot.h b/src/ast/ast_pp_dot.h index 38c45e00b..537754e83 100644 --- a/src/ast/ast_pp_dot.h +++ b/src/ast/ast_pp_dot.h @@ -16,7 +16,7 @@ class ast_pp_dot { 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; } };