From c15275b53b6f294f29c2ffe0a59e17755fde5542 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Oct 2012 13:56:40 -0700 Subject: [PATCH] ast_printer fix Signed-off-by: Leonardo de Moura --- src/ast/ast_printer.cpp | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp index 015075d9b..33ddcb709 100644 --- a/src/ast/ast_printer.cpp +++ b/src/ast/ast_printer.cpp @@ -21,25 +21,26 @@ Revision History: class simple_ast_printer_context : public ast_printer_context { ast_manager & m_manager; - smt2_pp_environment_dbg m_env; + scoped_ptr m_env; + smt2_pp_environment_dbg & env() const { return *(m_env.get()); } public: - simple_ast_printer_context(ast_manager & m):m_manager(m), m_env(m) {} + simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); } virtual ~simple_ast_printer_context() {} ast_manager & m() const { return m_manager; } virtual ast_manager & get_ast_manager() { return m_manager; } - virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { out << mk_ismt2_pp(s, m(), indent); } - virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { out << mk_ismt2_pp(n, m(), indent); } + virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const { out << mk_ismt2_pp(s, m(), indent); } + virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const { out << mk_ismt2_pp(n, m(), indent); } virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const { out << f->get_name(); } - virtual void pp(sort * s, format_ns::format_ref & r) { mk_smt2_format(s, m_env, get_pp_default_params(), r); } - virtual void pp(func_decl * f, format_ns::format_ref & r) { mk_smt2_format(f, m_env, get_pp_default_params(), r); } - virtual void pp(expr * n, format_ns::format_ref & r) { + virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), get_pp_default_params(), r); } + virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), get_pp_default_params(), r); } + virtual void pp(expr * n, format_ns::format_ref & r) const { sbuffer buf; - mk_smt2_format(n, m_env, get_pp_default_params(), 0, 0, r, buf); + mk_smt2_format(n, env(), get_pp_default_params(), 0, 0, r, buf); } - virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) { - mk_smt2_format(n, m_env, get_pp_default_params(), num_vars, var_prefix, r, var_names); + virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const { + mk_smt2_format(n, env(), get_pp_default_params(), num_vars, var_prefix, r, var_names); } virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const { NOT_IMPLEMENTED_YET();