mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

detect singleton range

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-25 20:49:27 -07:00
parent 98226e1842
commit 5e38eb328d
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/test/regex_range_collapse.cpp
View file

@ -34,6 +34,22 @@ namespace {
static bool extract_range_chars(seq_util& u, expr* e, unsigned& lo, unsigned& hi) { static bool extract_range_chars(seq_util& u, expr* e, unsigned& lo, unsigned& hi) {
expr* lo_e = nullptr; expr* hi_e = nullptr; expr* lo_e = nullptr; expr* hi_e = nullptr;
expr *s = nullptr;
zstring str;
if (u.re.is_to_re(e, s) && u.str.is_string(s, str) && str.length() == 1) {
lo = hi = str[0];
return true;
}
else if (u.re.is_range(e, lo_e, hi_e) && u.str.is_string(lo_e) && u.str.is_string(hi_e)) {
zstring lo_str, hi_str;
u.str.is_string(lo_e, lo_str);
u.str.is_string(hi_e, hi_str);
if (lo_str.length() == 1 && hi_str.length() == 1) {
lo = lo_str[0];
hi = hi_str[0];
return true;
}
}
if (!u.re.is_range(e, lo_e, hi_e)) if (!u.re.is_range(e, lo_e, hi_e))
return false; return false;
// Accept either string-constant or (seq.unit (Char N)) bound form. // Accept either string-constant or (seq.unit (Char N)) bound form.