computing and memoizing info for regexes #4647
Conversation
src/ast/seq_decl_plugin.h
Outdated
| @@ -478,10 +493,11 @@ class seq_util { | |||
| bool is_loop(expr const* n, expr*& body, unsigned& lo) const; | |||
| bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const; | |||
| bool is_loop(expr const* n, expr*& body, expr*& lo) const; | |||
| unsigned min_length(expr* r) const; | |||
| unsigned min_length(expr* r); | |||
There was a problem hiding this comment.
declare m_info and m_pinned with "mutable", then we can keep the const qualifier, which is probably reasonable.
src/ast/seq_decl_plugin.cpp
Outdated
| e_info = info(1); | ||
| break; | ||
| case OP_RE_CONCAT: | ||
| compute_info_rec(ea->get_arg(0)); |
There was a problem hiding this comment.
if you have this return an info, then you can combine many of the lines that first compute info, then access it.
src/ast/seq_decl_plugin.cpp
Outdated
| /* | ||
| Computes the info value for the given regex e recursively over the structure of e | ||
| */ | ||
| void seq_util::re::compute_info_rec(expr* e) { |
There was a problem hiding this comment.
thus with return value a seq_util::re::info you can use the result in the combiner.
src/ast/seq_decl_plugin.cpp
Outdated
|
|
||
| SASSERT(is_app(e)); | ||
| app* ea = to_app(e); | ||
| SASSERT(!m.is_ite(e)); |
There was a problem hiding this comment.
this is going to be too fragile to assume the expressions have some restricted form.
src/ast/seq_decl_plugin.cpp
Outdated
|
|
||
| info e_info(invalid_info); | ||
| unsigned k1, k2; | ||
| switch (ea->get_decl()->get_decl_kind()) |
There was a problem hiding this comment.
the get_decl_kind() can only be accessed after you have ensured the family_id() of the decl belongs to seq. So there has to be a test whether the ea->get_family_id() is right.
src/ast/seq_decl_plugin.cpp
Outdated
| /* | ||
| Get the information value associated with the regular expression e | ||
| */ | ||
| seq_util::re::info seq_util::re::get_info(expr* e) |
There was a problem hiding this comment.
Seems cleaner to separate the memoization from the recursive calls.
info get_info(expr * e) {
auto result = get_cached_info(e);
if (result.is_valid())
return result;
m_info_pinned.push_back(e);
return get_info_rec(e);
}
info get_info_rec(expr* e) {
auto result = get_cached_info(e);
if (result.is_valid())
return result;
if (!is_app(e))
return unknown_info;
result = mk_info(to_app(e));
add_cache(e, result);
return result;
}
info mk_info(app* r) {
if (r->get_family_id() == u.get_family_id()) {
switch (r->get_decl_kind()) {
case ...
}
return unknown_info;
}
if (m.is_ite(r, c, t, e)) {
}
}
Started computing info for regex expressions, initially just computing min_length.
Replaced also original implementation of min_length by using the info value.
Will use it to maintain misc information, such as being standard, being monadic, star-depth, etc.