1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     ast_printer.h
7 
8 Abstract:
9 
10     Abstract AST printer
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2012-10-21
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "ast/ast_smt2_pp.h"
23 
24 class ast_printer {
25 public:
~ast_printer()26     virtual ~ast_printer() {}
pp(sort * s,format_ns::format_ref & r)27     virtual void pp(sort * s, format_ns::format_ref & r) const { UNREACHABLE(); }
pp(func_decl * f,format_ns::format_ref & r)28     virtual void pp(func_decl * f, format_ns::format_ref & r) const { UNREACHABLE(); }
pp(expr * n,unsigned num_vars,char const * var_prefix,format_ns::format_ref & r,sbuffer<symbol> & var_names)29     virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const { UNREACHABLE(); }
pp(expr * n,format_ns::format_ref & r)30     virtual void pp(expr * n, format_ns::format_ref & r) const { UNREACHABLE(); }
31     virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const {
32         out << "#" << s->get_id() << "\n";
33     }
display(std::ostream & out,expr * n,unsigned indent,unsigned num_vars,char const * var_prefix,sbuffer<symbol> & var_names)34     virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
35         out << "#" << n->get_id() << "\n";
36     }
37     virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const {
38         out << "#" << n->get_id() << "\n";
39     }
40     virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const {
41         out << "#" << f->get_id() << "\n";
42     }
43 };
44 
45 class ast_printer_context : public ast_printer {
46 public:
~ast_printer_context()47     ~ast_printer_context() override {}
48     virtual ast_manager & get_ast_manager() = 0;
regular_stream()49     virtual std::ostream & regular_stream() { return std::cout; }
diagnostic_stream()50     virtual std::ostream & diagnostic_stream() { return std::cerr; }
51 };
52 
53 
54 ast_printer_context * mk_simple_ast_printer_context(ast_manager & m);
55 
56