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

ast_printer fix

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-26 13:56:40 -07:00
parent cba78d220f
commit c15275b53b
1 changed files with 11 additions and 10 deletions

21
src/ast/ast_printer.cpp
View file

@ -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<smt2_pp_environment_dbg> 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<symbol> 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<symbol> & 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<symbol> & 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<symbol> & var_names) const {
NOT_IMPLEMENTED_YET();