1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 ast_printer.cpp
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 #include "ast/ast_printer.h"
20 #include "ast/pp.h"
21
22 class simple_ast_printer_context : public ast_printer_context {
23 ast_manager & m_manager;
24 scoped_ptr<smt2_pp_environment_dbg> m_env;
env() const25 smt2_pp_environment_dbg & env() const { return *(m_env.get()); }
26 public:
simple_ast_printer_context(ast_manager & m)27 simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); }
~simple_ast_printer_context()28 ~simple_ast_printer_context() override {}
m() const29 ast_manager & m() const { return m_manager; }
get_ast_manager()30 ast_manager & get_ast_manager() override { return m_manager; }
display(std::ostream & out,sort * s,unsigned indent=0) const31 void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); }
display(std::ostream & out,expr * n,unsigned indent=0) const32 void display(std::ostream & out, expr * n, unsigned indent = 0) const override { out << mk_ismt2_pp(n, m(), indent); }
display(std::ostream & out,func_decl * f,unsigned indent=0) const33 void display(std::ostream & out, func_decl * f, unsigned indent = 0) const override {
34 out << f->get_name();
35 }
pp(sort * s,format_ns::format_ref & r) const36 void pp(sort * s, format_ns::format_ref & r) const override { mk_smt2_format(s, env(), params_ref(), r); }
pp(func_decl * f,format_ns::format_ref & r) const37 void pp(func_decl * f, format_ns::format_ref & r) const override { mk_smt2_format(f, env(), params_ref(), r, "declare-fun"); }
pp(expr * n,format_ns::format_ref & r) const38 void pp(expr * n, format_ns::format_ref & r) const override {
39 sbuffer<symbol> buf;
40 mk_smt2_format(n, env(), params_ref(), 0, nullptr, r, buf);
41 }
pp(expr * n,unsigned num_vars,char const * var_prefix,format_ns::format_ref & r,sbuffer<symbol> & var_names) const42 void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const override {
43 mk_smt2_format(n, env(), params_ref(), num_vars, var_prefix, r, var_names);
44 }
display(std::ostream & out,expr * n,unsigned indent,unsigned num_vars,char const * var_prefix,sbuffer<symbol> & var_names) const45 void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const override {
46 NOT_IMPLEMENTED_YET();
47 }
48
49 };
50
mk_simple_ast_printer_context(ast_manager & m)51 ast_printer_context * mk_simple_ast_printer_context(ast_manager & m) {
52 return alloc(simple_ast_printer_context, m);
53 }
54