Merge pull request #1323 from c-cube/pp-proof-graphviz

print proofs in graphviz

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

src/ast/ast_pp_dot.cpp

@@ -0,0 +1,134 @@
+/*++
+
+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;
+    res.reserve(s.size()); // preallocate
+    for (auto c : s) {
+        if (c == '\n')
+            res.append("\\l");
+        else
+            res.push_back(c);
+    }
+    return res;
+}
+
+// map from proofs to unique IDs
+typedef obj_map<const expr, unsigned> expr2id;
+typedef obj_map<const expr, bool> 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<const expr *>   m_to_print;
+    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),
+        m_out(out),
+        m_next_id(0),
+        m_id_map(),
+        m_to_print(),
+        m_printed(),
+        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
+        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:
+
+    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, m());
+        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,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << std::endl;
+    }
+    
+    void pp_step(const proof * p) {
+        TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << num_args);
+        if (m().has_fact(p)) {
+            // print 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_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 < 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)
+                    << "[label=\"" << label << "\"];" << std::endl;;
+            }
+        } else {
+            pp_atomic_step(p);
+        }
+    }
+
+    // find a unique ID for this proof
+    unsigned get_id(const expr * e) {
+        unsigned id = 0;
+        if (!m_id_map.find(e, id)) {
+             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); }
+

src/ast/ast_pp_dot.h

@@ -0,0 +1,24 @@
+/*++
+
+Abstract: Pretty-printer for proofs in Graphviz format
+
+--*/
+
+#pragma once
+
+#include <iostream>
+#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);

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,26 @@ 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");
+    }
+
+    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;
+});
+
 static void print_core(cmd_context& ctx) {
     ptr_vector<expr> core;
     ctx.get_check_sat_result()->get_unsat_core(core);
@@ -840,6 +861,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));

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);

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;