mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
re.range with non-unit arguments is the empty language (#4360)
This commit is contained in:
parent
152d6338f8
commit
1c760b04cf
|
@ -308,7 +308,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
return a.detach();
|
||||
}
|
||||
else {
|
||||
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
|
||||
// if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
|
||||
return alloc(eautomaton, sm);
|
||||
}
|
||||
}
|
||||
else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
|
||||
|
|
|
@ -812,9 +812,11 @@ namespace smt {
|
|||
zstring str1, str2;
|
||||
u.str.is_string(sub1, str1);
|
||||
u.str.is_string(sub2, str2);
|
||||
SASSERT(str1.length() == 1);
|
||||
SASSERT(str2.length() == 1);
|
||||
return 1 + str2[0] - str1[0];
|
||||
if (str1.length() == 1 && str2.length() == 1) {
|
||||
return 1 + str2[0] - str1[0];
|
||||
} else {
|
||||
return 1;
|
||||
}
|
||||
} else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
|
||||
return 1;
|
||||
} else {
|
||||
|
@ -964,9 +966,13 @@ namespace smt {
|
|||
zstring str1, str2;
|
||||
u.str.is_string(sub1, str1);
|
||||
u.str.is_string(sub2, str2);
|
||||
SASSERT(str1.length() == 1);
|
||||
SASSERT(str2.length() == 1);
|
||||
lens.insert(1);
|
||||
// re.range is a language of singleton strings if both of its arguments are;
|
||||
// otherwise it is the empty language
|
||||
if (str1.length() == 1 && str2.length() == 1) {
|
||||
lens.insert(1);
|
||||
} else {
|
||||
lens.insert(0);
|
||||
}
|
||||
} else if (u.re.is_full_char(re)) {
|
||||
lens.insert(1);
|
||||
} else if (u.re.is_full_seq(re)) {
|
||||
|
|
Loading…
Reference in a new issue