mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

renamed re to rex and added custom pretty printing for info (#4650)

Browse source
This commit is contained in:
Margus Veanes 2020-08-19 19:20:14 -07:00 • committed by GitHub
parent 79aa3457c1
commit de65c61ebc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 60 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_rewriter.h
View file

@ -288,8 +288,8 @@ class seq_rewriter {
void remove_empty_and_concats(expr_ref_vector& es);
void remove_leading(unsigned n, expr_ref_vector& es);
class seq_util::re& re() { return u().re; }
class seq_util::re const& re() const { return u().re; }
class seq_util::rex& re() { return u().re; }
class seq_util::rex const& re() const { return u().re; }
class seq_util::str& str() { return u().str; }
class seq_util::str const& str() const { return u().str; }

72
src/ast/seq_decl_plugin.cpp
View file

@ -1312,12 +1312,12 @@ unsigned seq_util::str::max_length(expr* s) const {
return result;
}
unsigned seq_util::re::min_length(expr* r) const {
unsigned seq_util::rex::min_length(expr* r) const {
SASSERT(u.is_re(r));
return get_info(r).min_length;
}
unsigned seq_util::re::max_length(expr* r) const {
unsigned seq_util::rex::max_length(expr* r) const {
SASSERT(u.is_re(r));
expr* r1 = nullptr, *r2 = nullptr, *s = nullptr;
unsigned lo = 0, hi = 0;
@ -1341,49 +1341,49 @@ unsigned seq_util::re::max_length(expr* r) const {
return UINT_MAX;
}
sort* seq_util::re::to_seq(sort* re) {
sort* seq_util::rex::to_seq(sort* re) {
(void)u;
SASSERT(u.is_re(re));
return to_sort(re->get_parameter(0).get_ast());
}
app* seq_util::re::mk_loop(expr* r, unsigned lo) {
app* seq_util::rex::mk_loop(expr* r, unsigned lo) {
parameter param(lo);
return m.mk_app(m_fid, OP_RE_LOOP, 1, &param, 1, &r);
}
app* seq_util::re::mk_loop(expr* r, unsigned lo, unsigned hi) {
app* seq_util::rex::mk_loop(expr* r, unsigned lo, unsigned hi) {
parameter params[2] = { parameter(lo), parameter(hi) };
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
}
app* seq_util::re::mk_loop(expr* r, expr* lo) {
app* seq_util::rex::mk_loop(expr* r, expr* lo) {
expr* rs[2] = { r, lo };
return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 2, rs);
}
app* seq_util::re::mk_loop(expr* r, expr* lo, expr* hi) {
app* seq_util::rex::mk_loop(expr* r, expr* lo, expr* hi) {
expr* rs[3] = { r, lo, hi };
return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 3, rs);
}
app* seq_util::re::mk_full_char(sort* s) {
app* seq_util::rex::mk_full_char(sort* s) {
return m.mk_app(m_fid, OP_RE_FULL_CHAR_SET, 0, nullptr, 0, nullptr, s);
}
app* seq_util::re::mk_full_seq(sort* s) {
app* seq_util::rex::mk_full_seq(sort* s) {
return m.mk_app(m_fid, OP_RE_FULL_SEQ_SET, 0, nullptr, 0, nullptr, s);
}
app* seq_util::re::mk_empty(sort* s) {
app* seq_util::rex::mk_empty(sort* s) {
return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, nullptr, 0, nullptr, s);
}
app* seq_util::re::mk_of_pred(expr* p) {
app* seq_util::rex::mk_of_pred(expr* p) {
return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p);
}
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const {
bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const {
if (is_loop(n)) {
app const* a = to_app(n);
if (a->get_num_args() == 1 && a->get_decl()->get_num_parameters() == 2) {
@ -1396,7 +1396,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& h
return false;
}
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) const {
bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo) const {
if (is_loop(n)) {
app const* a = to_app(n);
if (a->get_num_args() == 1 && a->get_decl()->get_num_parameters() == 1) {
@ -1408,7 +1408,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) const {
return false;
}
bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const {
bool seq_util::rex::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const {
if (is_loop(n)) {
app const* a = to_app(n);
if (a->get_num_args() == 3) {
@ -1421,7 +1421,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) con
return false;
}
bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo) const {
bool seq_util::rex::is_loop(expr const* n, expr*& body, expr*& lo) const {
if (is_loop(n)) {
app const* a = to_app(n);
if (a->get_num_args() == 2) {
@ -1436,21 +1436,21 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, expr*& lo) const {
/**
Returns true iff e is the epsilon regex.
*/
bool seq_util::re::is_epsilon(expr* r) const {
bool seq_util::rex::is_epsilon(expr* r) const {
expr* s;
return is_to_re(r, s) && u.str.is_empty(s);
}
/**
Makes the epsilon regex for a given sequence sort.
*/
app* seq_util::re::mk_epsilon(sort* seq_sort) {
app* seq_util::rex::mk_epsilon(sort* seq_sort) {
return mk_to_re(u.str.mk_empty(seq_sort));
}
/*
Produces compact view of concrete concatenations such as (abcd).
*/
std::ostream& seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) const {
std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const {
SASSERT(re.u.is_seq(s));
if (re.u.str.is_concat(s)) {
expr_ref_vector es(re.m);
@ -1472,7 +1472,7 @@ std::ostream& seq_util::re::pp::compact_helper_seq(std::ostream& out, expr* s) c
/*
Produces output such as [a-z] for a range.
*/
std::ostream& seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
std::ostream& seq_util::rex::pp::compact_helper_range(std::ostream& out, expr* s1, expr* s2) const {
out << "[";
seq_unit(out, s1) << "-";
seq_unit(out, s2) << "]";
@ -1482,7 +1482,7 @@ std::ostream& seq_util::re::pp::compact_helper_range(std::ostream& out, expr* s1
/*
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) const {
bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
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));
}
@ -1490,7 +1490,7 @@ bool seq_util::re::pp::can_skip_parenth(expr* r) const {
/*
Specialize output for a unit sequence converting to visible ASCII characters if possible.
*/
std::ostream& seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
expr* e;
unsigned n = 0;
if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
@ -1509,7 +1509,7 @@ std::ostream& seq_util::re::pp::seq_unit(std::ostream& out, expr* s) const {
/*
Pretty prints the regex r into the out stream
*/
std::ostream& seq_util::re::pp::display(std::ostream& out) const {
std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
unsigned lo = 0, hi = 0;
if (re.is_full_char(e))
@ -1580,7 +1580,7 @@ std::ostream& seq_util::re::pp::display(std::ostream& out) const {
/*
Pretty prints the regex r into the output string
*/
std::string seq_util::re::to_str(expr* r) const {
std::string seq_util::rex::to_str(expr* r) const {
std::ostringstream out;
out << pp(u.re, r);
return out.str();
@ -1589,14 +1589,14 @@ std::string seq_util::re::to_str(expr* r) const {
/*
Returns true iff info has been computed for the regex r
*/
bool seq_util::re::has_valid_info(expr* r) const {
bool seq_util::rex::has_valid_info(expr* r) const {
return r->get_id() < m_infos.size() && m_infos[r->get_id()].is_valid();
}
/*
Returns the info in the cache if the info is valid. Returns invalid_info otherwise.
*/
seq_util::re::info seq_util::re::get_cached_info(expr* e) const {
seq_util::rex::info seq_util::rex::get_cached_info(expr* e) const {
if (has_valid_info(e))
return m_infos[e->get_id()];
else
@ -1606,7 +1606,7 @@ seq_util::re::info seq_util::re::get_cached_info(expr* e) const {
/*
Get the information value associated with the regular expression e
*/
seq_util::re::info seq_util::re::get_info(expr* e) const
seq_util::rex::info seq_util::rex::get_info(expr* e) const
{
SASSERT(u.is_re(e));
auto result = get_cached_info(e);
@ -1619,7 +1619,7 @@ seq_util::re::info seq_util::re::get_info(expr* e) const
/*
Gets the info value for the given regex e, possibly making a new info recursively over the structure of e.
*/
seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
seq_util::rex::info seq_util::rex::get_info_rec(expr* e) const {
auto result = get_cached_info(e);
if (result.is_valid())
return result;
@ -1627,7 +1627,7 @@ seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
return invalid_info;
result = mk_info_rec(to_app(e));
m_infos.setx(e->get_id(), result, invalid_info);
STRACE("re_info", tout << "compute_info(" << pp(u.re, e) << "): min_length=" << m_infos[e->get_id()].min_length << std::endl;);
STRACE("re_info", tout << "compute_info(" << pp(u.re, e) << ")=" << result << std::endl;);
return result;
}
@ -1635,7 +1635,7 @@ seq_util::re::info seq_util::re::get_info_rec(expr* e) const {
Computes the info value for the given regex e recursively over the structure of e.
The regex e does not yet have an entry in the cache.
*/
seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
info i1, i2;
if (e->get_family_id() == u.get_family_id()) {
switch (e->get_decl()->get_decl_kind())
@ -1687,3 +1687,17 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
}
return invalid_info;
}
std::ostream& seq_util::rex::info::display(std::ostream& out) const {
if (valid)
out << "info(" << "min_length=" << min_length << ")";
else
out << "invalid_info";
return out;
}
std::string seq_util::rex::info::str() const {
std::ostringstream out;
display(out);
return out.str();
}

22
src/ast/seq_decl_plugin.h
View file

@ -408,16 +408,18 @@ public:
unsigned max_length(expr* s) const;
};
class re {
class rex {
public:
struct info {
bool valid;
unsigned min_length;
info() : valid(false), min_length(0) {}
info(unsigned k) : valid(true), min_length(k) {}
bool is_valid() { return valid; }
std::ostream& display(std::ostream&) const;
std::string str() const;
};
private:
seq_util& u;
ast_manager& m;
family_id m_fid;
@ -431,7 +433,7 @@ public:
info get_cached_info(expr* e) const;
public:
re(seq_util& u): u(u), m(u.m), m_fid(u.m_fid), m_info_pinned(u.m) {}
rex(seq_util& u): u(u), m(u.m), m_fid(u.m_fid), m_info_pinned(u.m) {}
sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, &param); }
sort* to_seq(sort* re);
@ -503,7 +505,7 @@ public:
std::string to_str(expr* r) const;
class pp {
seq_util::re& re;
seq_util::rex& re;
expr* e;
bool can_skip_parenth(expr* r) const;
std::ostream& seq_unit(std::ostream& out, expr* s) const;
@ -511,12 +513,12 @@ public:
std::ostream& compact_helper_range(std::ostream& out, expr* s1, expr* s2) const;
public:
pp(seq_util::re& r, expr* e) : re(r), e(e) {}
pp(seq_util::rex& r, expr* e) : re(r), e(e) {}
std::ostream& display(std::ostream&) const;
};
};
str str;
re re;
rex re;
seq_util(ast_manager& m):
m(m),
@ -531,8 +533,6 @@ public:
family_id get_family_id() const { return m_fid; }
};
inline std::ostream& operator<<(std::ostream& out, seq_util::re::pp const & p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, seq_util::rex::pp const & p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, seq_util::rex::info const& p) { return p.display(out); }

6
src/smt/seq_regex.cpp
View file

@ -29,7 +29,7 @@ namespace smt {
{}
seq_util& seq_regex::u() { return th.m_util; }
class seq_util::re& seq_regex::re() { return th.m_util.re; }
class seq_util::rex& seq_regex::re() { return th.m_util.re; }
class seq_util::str& seq_regex::str() { return th.m_util.str; }
seq_rewriter& seq_regex::seq_rw() { return th.m_seq_rewrite; }
seq_skolem& seq_regex::sk() { return th.m_sk; }
@ -794,7 +794,7 @@ namespace smt {
STRACE("seq_regex", tout << "Updating state graph for regex "
<< mk_pp(r, m) << ") ";);
if (!m_state_graph.is_seen(r_id))
STRACE("state_graph", tout << std::endl << "state(" << r_id << ") = " << seq_util::re::pp(re(), r) << std::endl;);
STRACE("state_graph", tout << std::endl << "state(" << r_id << ") = " << seq_util::rex::pp(re(), r) << std::endl;);
// Add state
m_state_graph.add_state(r_id);
STRACE("state_graph", tout << "regex(" << r_id << ") = " << mk_pp(r, m) << std::endl;);
@ -817,7 +817,7 @@ namespace smt {
STRACE("seq_regex_verbose", tout
<< std::endl << " traversing deriv: " << dr_id << " ";);
if (!m_state_graph.is_seen(dr_id))
STRACE("state_graph", tout << "state(" << dr_id << ") = " << seq_util::re::pp(re(), dr) << std::endl;);
STRACE("state_graph", tout << "state(" << dr_id << ") = " << seq_util::rex::pp(re(), dr) << std::endl;);
// Add state
m_state_graph.add_state(dr_id);
STRACE("state_graph", tout << "regex(" << dr_id << ") = " << mk_pp(dr, m) << std::endl;);

2
src/smt/seq_regex.h
View file

@ -132,7 +132,7 @@ namespace smt {
Solvers and utilities
*/
seq_util& u();
class seq_util::re& re();
class seq_util::rex& re();
class seq_util::str& str();
seq_rewriter& seq_rw();
seq_skolem& sk();