Skip to content

Commit

Permalink
updated printer
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Oct 16, 2021
1 parent cb120c9 commit fb9fa1b
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 48 deletions.
94 changes: 48 additions & 46 deletions src/ast/seq_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1111,24 +1111,23 @@ app* seq_util::rex::mk_epsilon(sort* seq_sort) {
/*
Produces compact view of concrete concatenations such as (abcd).
*/
std::ostream& seq_util::rex::pp::print_seq(std::ostream& out, expr* s) const {
SASSERT(re.u.is_seq(s));
bool seq_util::rex::pp::print_seq(std::ostream& out, expr* s) const {
zstring z;
expr* x, * j, * k, * l, * i, * x_;
if (re.u.str.is_empty(s))
out << "()";
else if (re.u.str.is_unit(s))
print_unit(out, s);
else if (re.u.str.is_concat(s)) {
expr_ref_vector es(re.m);
re.u.str.get_concat(s, es);
for (expr* e : es)
print_seq(out, e);
print(out, e);
}
else if (re.u.str.is_string(s, z)) {
for (unsigned i = 0; i < z.length(); i++)
out << (char)z[i];
}
else if (re.u.str.is_at(s, x, i))
print(out, x) << "@", print(out, i);
else if (re.u.str.is_extract(s, x, j, k)) {
rational jv, iv;
print(out, x);
Expand All @@ -1152,7 +1151,7 @@ std::ostream& seq_util::rex::pp::print_seq(std::ostream& out, expr* s) const {
out << "[" << jv.get_int32() << ",";
print(out, k);
out << "]";
}
}
}
else {
out << "[";
Expand All @@ -1162,19 +1161,19 @@ std::ostream& seq_util::rex::pp::print_seq(std::ostream& out, expr* s) const {
out << "]";
}
}
else
out << mk_pp(s, re.m);
return out;
else
return false;
return true;
}

/*
Produces output such as [a-z] for a range.
*/
std::ostream& seq_util::rex::pp::print_range(std::ostream& out, expr* s1, expr* s2) const {
out << "[";
print_unit(out, s1);
print(out, s1);
out << "-";
print_unit(out, s2);
print(out, s2);
out << "]";
return out;
}
Expand All @@ -1190,9 +1189,10 @@ bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
/*
Specialize output for a unit sequence converting to visible ASCII characters if possible.
*/
std::ostream& seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
bool seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
expr* e, * i;
unsigned n = 0;

if ((re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) || re.u.is_const_char(s, n)) {
char c = (char)n;
if (c == '\n')
Expand Down Expand Up @@ -1226,24 +1226,18 @@ std::ostream& seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
out << "\\x" << std::hex << n;
else if (n <= 0xFFF)
out << "\\u0" << std::hex << n;
else
else
out << "\\u" << std::hex << n;
}
else if (re.u.str.is_nth_i(s, e, i)) {
print(out, e);
out << "[" << mk_pp(i, re.m) << "]";
}
else if (re.m.is_value(s))
out << mk_pp(s, re.m);
else if (is_app(s)) {
out << "(" << to_app(s)->get_decl()->get_name().str();
for (expr * arg : *to_app(s))
print(out << " ", arg);
out << ")";
print(out, e) << "[";
print(out, i) << "]";
}
else if (re.u.str.is_length(s, e))
print(out << "|", e) << "|";
else
out << mk_pp(s, re.m);
return out;
return false;
return true;
}

/*
Expand All @@ -1252,17 +1246,20 @@ std::ostream& seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
unsigned lo = 0, hi = 0;
arith_util a(re.m);
rational v;
if (re.u.is_char(e))
print_unit(out, e);
else if (re.u.is_seq(e))
print_seq(out, e);
if (!e)
out << "null";
else if (print_unit(out, e))
;
else if (print_seq(out, e))
;
else if (re.is_full_char(e))
out << ".";
else if (re.is_full_seq(e))
out << ".*";
else if (re.is_to_re(e, s))
print_seq(out, s);
print(out, s);
else if (re.is_range(e, s, s2))
print_range(out, s, s2);
else if (re.is_epsilon(e))
Expand All @@ -1282,8 +1279,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
print(out, r2);
out << ")";
}
else if (re.is_intersection(e, r1, r2))
{
else if (re.is_intersection(e, r1, r2)) {
out << "(";
print(out, r1);
out << (html_encode ? "&#x22C2;" : "&");
Expand Down Expand Up @@ -1323,12 +1319,9 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
}
}
else if (re.is_loop(e, r1, lo)) {
if (can_skip_parenth(r1)) {
print(out, r1);
out << "{" << lo << ",}";
}
else
{
if (can_skip_parenth(r1))
print(out, r1) << "{" << lo << ",}";
else {
out << "(";
print(out, r1);
out << "){" << lo << ",}";
Expand Down Expand Up @@ -1368,10 +1361,8 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
out << ")";
}
else if (re.is_opt(e, r1)) {
if (can_skip_parenth(r1)) {
print(out, r1);
out << "?";
}
if (can_skip_parenth(r1))
print(out, r1) << "?";
else {
out << "(";
print(out, r1);
Expand All @@ -1386,18 +1377,30 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
else if (re.m.is_eq(e, r1, r2)) {
out << "(";
print(out, r1);
out << "=";
out << " = ";
print(out, r2);
out << ")";
}
else if (re.m.is_not(e, r1)) {
out << "!";
print(out, r1);
}
else if (a.is_add(e, s, s2) && a.is_numeral(s, v) && v < 0)
print(out, s2) << " - " << -v;
else if (a.is_add(e, s, s2) && a.is_numeral(s2, v) && v < 0)
print(out, s) << " - " << -v;
else if (a.is_add(e, s, s2))
print(out, s) << " + ", print(out, s2);
else if (a.is_sub(e, s, s2) && a.is_numeral(s2, v) && v > 0)
print(out, s) << " - " << v;
else if (a.is_le(e, s, s2))
print(out << "(", s) << " <= ", print(out, s2) << ")";
else if (re.m.is_value(e))
out << mk_pp(e, re.m);
else if (is_app(e) && to_app(e)->get_num_args() == 0)
out << mk_pp(e, re.m);
else if (is_app(e)) {
out << "(" << to_app(e)->get_decl()->get_name().str();
out << "(" << to_app(e)->get_decl()->get_name();
for (expr* arg : *to_app(e))
print(out << " ", arg);
out << ")";
Expand All @@ -1409,8 +1412,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
}

std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
print(out, ex);
return out;
return print(out, ex);
}

/*
Expand Down
4 changes: 2 additions & 2 deletions src/ast/seq_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -599,8 +599,8 @@ class seq_util {
expr* ex;
bool html_encode;
bool can_skip_parenth(expr* r) const;
std::ostream& print_unit(std::ostream& out, expr* s) const;
std::ostream& print_seq(std::ostream& out, expr* s) const;
bool print_unit(std::ostream& out, expr* s) const;
bool print_seq(std::ostream& out, expr* s) const;
std::ostream& print_range(std::ostream& out, expr* s1, expr* s2) const;
std::ostream& print(std::ostream& out, expr* e) const;

Expand Down

0 comments on commit fb9fa1b

Please sign in to comment.