mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

fix build issues

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-24 03:39:00 -07:00
parent bce143b2b2
commit e6e1d94cf9
1 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/ast/ast_pp_dot.cpp
View file

@ -6,7 +6,7 @@ Abstract: Pretty-printer for proofs in Graphviz format
#include "util/util.h"
#include "util/map.h"
#include "ast_pp_dot.h"
#include "ast/ast_pp_dot.h"
// string escaping for DOT
std::string escape_dot(std::string const & s) {
@ -23,28 +23,27 @@ std::string escape_dot(std::string const & s) {
// 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;
std::ostream & m_out;
const ast_pp_dot * m_pp;
unsigned m_next_id;
expr2id m_id_map;
obj_hashtable<const expr> m_printed;
svector<const expr *> m_to_print;
bool m_first;
ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) :
m_pp(pp),
m_manager(pp->get_manager()),
m_out(out),
m_pp(pp),
m_next_id(0),
m_id_map(),
m_to_print(),
m_printed(),
m_first(true),
m_manager(pp->get_manager()) {}
m_first(true) {}
~ast_pp_dot_st() = default;
@ -56,7 +55,7 @@ struct ast_pp_dot_st {
const expr * a = m_to_print.back();
m_to_print.pop_back();
if (!m_printed.contains(a)) {
m_printed.insert(a, true);
m_printed.insert(a);
if (m().is_proof(a))
pp_step(to_app(a));
else
@ -83,7 +82,7 @@ private:
}
void pp_step(const proof * p) {
TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << num_args);
TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << p->get_num_args() << "\n";);
if (m().has_fact(p)) {
// print result
expr* p_res = m().get_fact(p); // result of proof step