1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     ast_pp.h
7 
8 Abstract:
9 
10     Pretty printer
11 
12 Author:
13 
14     Leonardo de Moura 2008-01-20.
15 
16 Revision History:
17 
18     2012-11-17 - ast_smt2_pp is the official pretty printer in Z3
19 
20 --*/
21 #pragma once
22 
23 #include "ast/ast_smt2_pp.h"
24 
25 struct mk_pp : public mk_ismt2_pp {
26     mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr):
mk_ismt2_ppmk_pp27         mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
28     }
29     mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr):
mk_ismt2_ppmk_pp30         mk_ismt2_pp(t, m, indent, num_vars, var_prefix) {
31     }
32 };
33 
34 
35 //<! print vector of ASTs
36 class mk_pp_vec {
37     ast_manager &   m;
38     ast_ref_vector  vec;
39 public:
mk_pp_vec(unsigned len,ast ** vec0,ast_manager & m)40     mk_pp_vec(unsigned len, ast ** vec0, ast_manager & m) : m(m), vec(m) {
41         for (unsigned i=0; i<len; ++i) vec.push_back(vec0[i]);
42     }
display(std::ostream & out)43     void display(std::ostream & out) const {
44         bool first = true;
45         for (ast* e : vec) {
46             if (first) { first = false; } else { out << " "; }
47             out << mk_pp(e, m);
48         }
49     }
50 };
51 
52 inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
53     pp.display(out);
54     return out;
55 }
56 
57 
58 inline std::string operator+(char const* s, mk_pp const& pp) {
59     std::ostringstream strm;
60     strm << s << pp;
61     return strm.str();
62 }
63 
64 inline std::string operator+(std::string const& s, mk_pp const& pp) {
65     std::ostringstream strm;
66     strm << s << pp;
67     return strm.str();
68 }
69 
70 inline std::string& operator+=(std::string& s, mk_pp const& pp) {
71     return s = s + pp;
72 }
73 
74