From ed526b808d402e5b66bfcb8962ae58568993d00b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 24 Oct 2017 10:16:22 +0200
Subject: [PATCH] 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;