mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

add way to access range bounds directly #6186

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-22 09:35:25 -07:00
parent 87dd837b55
commit 1e0f71c971
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/ast/seq_decl_plugin.cpp
View file

@ -1107,6 +1107,31 @@ unsigned seq_util::rex::max_length(expr* r) const {
return UINT_MAX;
}
/**
\brief determine if \c n is a range regular expression where the lower and upper bounds
are given by single characters.
Range expressions where lower and upper bounds are not single characters are either
the empty language (when a bound is a string but not a single character) or symbolic
(when both bounds are not ground strings). The general is_range can be used to process
range expressions for these cases, but they don't correspond to mainstream regex usage.
*/
bool seq_util::rex::is_range(expr const* n, unsigned& lo, unsigned& hi) const {
expr* _lo, *_hi;
zstring los, his;
if (!is_range(n, _lo, _hi))
return false;
if (!u.str.is_string(_lo, los))
return false;
if (!u.str.is_string(_hi, his))
return false;
if (los.length() != 1 || his.length() != 1)
return false;
lo = los[0];
hi = his[0];
return true;
}
sort* seq_util::rex::to_seq(sort* re) {
(void)u;
SASSERT(u.is_re(re));

1
src/ast/seq_decl_plugin.h
View file

@ -545,6 +545,7 @@ public:
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); }
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); }
bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); }
bool is_range(expr const* n, unsigned& lo, unsigned& hi) const;
bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); }
bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); }
bool is_full_char(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_CHAR_SET); }