mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

add parameter to specify the file into which dot proofs are to be printed

Browse source
This commit is contained in:
Simon Cruanes 2017-10-24 10:16:22 +02:00
parent 24edb8fb47
commit ed526b808d
3 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/basic_cmds.cpp
View file

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

5
src/cmd_context/context_params.cpp
View file

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

1
src/cmd_context/context_params.h
View file

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