mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add some colors to the proof output

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

12
src/ast/ast_pp_dot.cpp
View file

@ -32,6 +32,7 @@ struct ast_pp_dot_st {
svector<const expr *> 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) {