mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

added missing const declarations that caused build failure on some platforms

Browse source
This commit is contained in:
Margus Veanes 2020-08-13 20:04:35 -07:00
parent 0d9dc032d7
commit 1233cb4621
2 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/seq_decl_plugin.cpp
View file

@ -1469,7 +1469,7 @@ app* seq_util::re::mk_epsilon(sort* seq_sort) {
/* /*
Produces compact view of concrete concatenations such as (abcd). Produces compact view of concrete concatenations such as (abcd).
*/ */
void seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) { void seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) const {
SASSERT(re.u.is_seq(s)); SASSERT(re.u.is_seq(s));
if (re.m.is_value(s)) { if (re.m.is_value(s)) {
SASSERT(s->get_kind() == ast_kind::AST_APP); SASSERT(s->get_kind() == ast_kind::AST_APP);
@ -1494,7 +1494,7 @@ void seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) {
/* /*
Produces output such as [a-z] for a range. Produces output such as [a-z] for a range.
*/ */
void seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) { void seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
out << "["; out << "[";
if (re.u.str.is_unit(s1)) if (re.u.str.is_unit(s1))
seq_unit(out, s1); seq_unit(out, s1);
@ -1511,7 +1511,7 @@ void seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s
/* /*
Checks if parenthesis can be omitted in some cases in a loop body or in complement. Checks if parenthesis can be omitted in some cases in a loop body or in complement.
*/ */
bool seq_util::re::pp::can_skip_parenth(expr* r) { bool seq_util::re::pp::can_skip_parenth(expr* r) const {
expr* s; expr* s;
return ((re.is_to_re(r, s) && re.u.str.is_unit(s)) || re.is_range(r) || re.is_empty(r) || re.is_epsilon(r)); return ((re.is_to_re(r, s) && re.u.str.is_unit(s)) || re.is_range(r) || re.is_empty(r) || re.is_epsilon(r));
} }
@ -1519,7 +1519,7 @@ bool seq_util::re::pp::can_skip_parenth(expr* r) {
/* /*
Specialize output for a unit sequence converting to visible ASCII characters if possible. Specialize output for a unit sequence converting to visible ASCII characters if possible.
*/ */
void seq_util::re::pp::seq_unit(std::ostream& out, expr* s) { void seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
expr* e; expr* e;
if (re.u.str.is_unit(s, e)) { if (re.u.str.is_unit(s, e)) {
rational r; rational r;
@ -1543,7 +1543,7 @@ void seq_util::re::pp::seq_unit(std::ostream& out, expr* s) {
/* /*
Pretty prints the regex r into the out stream Pretty prints the regex r into the out stream
*/ */
std::ostream& seq_util::re::pp::display(std::ostream& out) { std::ostream& seq_util::re::pp::display(std::ostream& out) const {
expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr; expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
unsigned lo = 0, hi = 0; unsigned lo = 0, hi = 0;
if (re.is_full_char(e)) if (re.is_full_char(e))

12
src/ast/seq_decl_plugin.h
View file

@ -486,14 +486,14 @@ public:
class pp { class pp {
seq_util::re& re; seq_util::re& re;
expr* e; expr* e;
bool can_skip_parenth(expr* r); bool can_skip_parenth(expr* r) const;
void seq_unit(std::ostream& out, expr* s); void seq_unit(std::ostream& out, expr* s) const;
void compact_helper_seq(std::ostream& out, expr* s); void compact_helper_seq(std::ostream& out, expr* s) const;
void compact_helper_range(std::ostream& out, expr* s1, expr* s2); void compact_helper_range(std::ostream& out, expr* s1, expr* s2) const;
public: public:
pp(seq_util::re& r, expr* e) : re(r), e(e) {} pp(seq_util::re& r, expr* e) : re(r), e(e) {}
std::ostream& display(std::ostream&); std::ostream& display(std::ostream&) const;
}; };
}; };
@ -514,7 +514,7 @@ public:
}; };
inline std::ostream& operator<<(std::ostream& out, seq_util::re::pp& p) { return p.display(out); } inline std::ostream& operator<<(std::ostream& out, seq_util::re::pp const & p) { return p.display(out); }