mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-14 04:26:59 -07:00
parent c4a03dcf7c
commit c0a07f9229
3 changed files with 46 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

98
src/ast/seq_decl_plugin.cpp
View file

@ -1469,43 +1469,33 @@ 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) const { std::ostream& 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.u.str.is_concat(s)) {
SASSERT(s->get_kind() == ast_kind::AST_APP); expr_ref_vector es(re.m);
if (re.u.str.is_concat(s)) { re.u.str.get_concat(s, es);
expr_ref_vector es(re.m); for (expr* e : es) {
re.u.str.get_concat(s, es); if (re.u.str.is_unit(e))
for (unsigned i = 0; i < es.size(); i++) seq_unit(out, e);
if (re.u.str.is_unit(es.get(i))) else
seq_unit(out, es.get(i)); out << mk_pp(e, re.m);
else
out << mk_pp(es.get(i), re.m);
} }
else if (re.u.str.is_empty(s))
out << "()";
else
seq_unit(out, s);
} }
else if (re.u.str.is_empty(s))
out << "()";
else else
out << mk_pp(s, re.m); seq_unit(out, s);
return out;
} }
/* /*
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) const { std::ostream& seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
out << "["; out << "[";
if (re.u.str.is_unit(s1)) seq_unit(out, s1) << "-";
seq_unit(out, s1); seq_unit(out, s2) << "]";
else return out;
out << mk_pp(s1, re.m);
out << "-";
if (re.u.str.is_unit(s2))
seq_unit(out, s2);
else
out << mk_pp(s1, re.m);
out << "]";
} }
/* /*
@ -1519,25 +1509,20 @@ bool seq_util::re::pp::can_skip_parenth(expr* r) const {
/* /*
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) const { std::ostream& seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
expr* e; expr* e;
if (re.u.str.is_unit(s, e)) { unsigned n = 0;
rational r; if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
unsigned sz; if (32 < n && n < 127)
if (re.u.bv().is_numeral(e, r, sz) && sz == 8 && r.is_unsigned()) { out << (char)n;
unsigned n = r.get_unsigned(); else if (n < 16)
if (32 < n && n < 127) out << "\\x0" << std::hex << n;
out << (char)n;
else if (n < 16)
out << "\\x0" << std::hex << n;
else
out << "\\x" << std::hex << n;
}
else else
out << mk_pp(s, re.m); out << "\\x" << std::hex << n;
} }
else else
out << mk_pp(s, re.m); out << mk_pp(s, re.m);
return out;
} }
/* /*
@ -1551,14 +1536,9 @@ std::ostream& seq_util::re::pp::display(std::ostream& out) const {
else if (re.is_full_seq(e)) else if (re.is_full_seq(e))
return out << ".*"; return out << ".*";
else if (re.is_to_re(e, s)) else if (re.is_to_re(e, s))
{ return compact_helper_seq(out, s);
compact_helper_seq(out, s); else if (re.is_range(e, s, s2))
return out; return compact_helper_range(out, s, s2);
}
else if (re.is_range(e, s, s2)) {
compact_helper_range(out, s, s2);
return out;
}
else if (re.is_epsilon(e)) else if (re.is_epsilon(e))
return out << "()"; return out << "()";
else if (re.is_empty(e)) else if (re.is_empty(e))
@ -1569,40 +1549,46 @@ std::ostream& seq_util::re::pp::display(std::ostream& out) const {
return out << pp(re, r1) << "|" << pp(re, r2); return out << pp(re, r1) << "|" << pp(re, r2);
else if (re.is_intersection(e, r1, r2)) else if (re.is_intersection(e, r1, r2))
return out << "(" << pp(re, r1) << ")&(" << pp(re, r2) << ")"; return out << "(" << pp(re, r1) << ")&(" << pp(re, r2) << ")";
else if (re.is_complement(e, r1)) else if (re.is_complement(e, r1)) {
if (can_skip_parenth(r1)) if (can_skip_parenth(r1))
return out << "~" << pp(re, r1); return out << "~" << pp(re, r1);
else else
return out << "~(" << pp(re, r1) << ")"; return out << "~(" << pp(re, r1) << ")";
else if (re.is_plus(e, r1)) }
if (can_skip_parenth(r1)) else if (re.is_plus(e, r1)) {
if (can_skip_parenth(r1))
return out << pp(re, r1) << "+"; return out << pp(re, r1) << "+";
else else
return out << "(" << pp(re, r1) << ")+"; return out << "(" << pp(re, r1) << ")+";
else if (re.is_star(e, r1)) }
else if (re.is_star(e, r1)) {
if (can_skip_parenth(r1)) if (can_skip_parenth(r1))
return out << pp(re, r1) << "*"; return out << pp(re, r1) << "*";
else else
return out << "(" << pp(re, r1) << ")*"; return out << "(" << pp(re, r1) << ")*";
else if (re.is_loop(e, r1, lo)) }
else if (re.is_loop(e, r1, lo)) {
if (can_skip_parenth(r1)) if (can_skip_parenth(r1))
return out << pp(re, r1) << "{" << lo << ",}"; return out << pp(re, r1) << "{" << lo << ",}";
else else
return out << "(" << pp(re, r1) << "){" << lo << ",}"; return out << "(" << pp(re, r1) << "){" << lo << ",}";
else if (re.is_loop(e, r1, lo, hi)) }
else if (re.is_loop(e, r1, lo, hi)) {
if (can_skip_parenth(r1)) if (can_skip_parenth(r1))
return out << pp(re, r1) << "{" << lo << "," << hi << "}"; return out << pp(re, r1) << "{" << lo << "," << hi << "}";
else else
return out << "(" << pp(re, r1) << "){" << lo << "," << hi << "}"; return out << "(" << pp(re, r1) << "){" << lo << "," << hi << "}";
}
else if (re.is_diff(e, r1, r2)) else if (re.is_diff(e, r1, r2))
return out << "(" << pp(re, r1) << ")\\(" << pp(re, r2) << ")"; return out << "(" << pp(re, r1) << ")\\(" << pp(re, r2) << ")";
else if (re.m.is_ite(e, s, r1, r2)) else if (re.m.is_ite(e, s, r1, r2))
return out << "if(" << mk_pp(s, re.m) << "," << pp(re, r1) << "," << pp(re, r2) << ")"; return out << "if(" << mk_pp(s, re.m) << "," << pp(re, r1) << "," << pp(re, r2) << ")";
else if (re.is_opt(e, r1)) else if (re.is_opt(e, r1)) {
if (can_skip_parenth(r1)) if (can_skip_parenth(r1))
return out << pp(re, r1) << "?"; return out << pp(re, r1) << "?";
else else
return out << "(" << pp(re, r1) << ")?"; return out << "(" << pp(re, r1) << ")?";
}
else if (re.is_reverse(e, r1)) else if (re.is_reverse(e, r1))
return out << "reverse(" << pp(re, r1) << ")"; return out << "reverse(" << pp(re, r1) << ")";
else else

6
src/ast/seq_decl_plugin.h
View file

@ -487,9 +487,9 @@ public:
seq_util::re& re; seq_util::re& re;
expr* e; expr* e;
bool can_skip_parenth(expr* r) const; bool can_skip_parenth(expr* r) const;
void seq_unit(std::ostream& out, expr* s) const; std::ostream& seq_unit(std::ostream& out, expr* s) const;
void compact_helper_seq(std::ostream& out, expr* s) const; std::ostream& compact_helper_seq(std::ostream& out, expr* s) const;
void compact_helper_range(std::ostream& out, expr* s1, expr* s2) const; std::ostream& 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) {}

2
src/model/model_evaluator.cpp
View file

@ -160,7 +160,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
family_id fid = f->get_family_id(); family_id fid = f->get_family_id();
bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
br_status st = BR_FAILED; br_status st = BR_FAILED;
#if 1 #if 0
struct pp { struct pp {
func_decl* f; func_decl* f;
expr_ref& r; expr_ref& r;