mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

further PR comment fixes

Browse source
This commit is contained in:
Margus Veanes 2020-08-13 16:44:13 -07:00
parent 5f9a326910
commit ae413365e9
3 changed files with 132 additions and 167 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/ast/seq_decl_plugin.h
View file

@ -412,10 +412,6 @@ public:
seq_util& u;
ast_manager& m;
family_id m_fid;
void seq_util::re::pp_compact_helper_seq(std::ostream& out, expr* s);
void seq_util::re::pp_compact_helper_range(std::ostream& out, expr* s1, expr* s2);
bool seq_util::re::pp_can_skip_parenth(expr* r);
void seq_util::re::pp_seq_unit(std::ostream& out, expr* s);
public:
re(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
@ -486,8 +482,20 @@ public:
unsigned max_length(expr* r) const;
bool is_epsilon(expr* r) const;
app* mk_epsilon(sort* seq_sort);
std::string pp(expr* r);
void pp(std::ostream& out, expr* r);
class pp {
seq_util::re& re;
expr* e;
bool can_skip_parenth(expr* r);
void seq_unit(std::ostream& out, expr* s);
void compact_helper_seq(std::ostream& out, expr* s);
void compact_helper_range(std::ostream& out, expr* s1, expr* s2);
public:
pp(seq_util::re& r, expr* e) : re(r), e(e) {}
std::ostream& display(std::ostream&);
};
};
str str;
re re;
@ -506,4 +514,8 @@ public:
};
inline std::ostream& operator<<(std::ostream& out, seq_util::re::pp& p) { return p.display(out); }