mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix #6729

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-22 14:07:12 +01:00
parent 06ea765b82
commit a68f91f0a6
1 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/rewriter/seq_rewriter.cpp
View file

@ -5024,12 +5024,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
* (re.range c_1 c_n) * (re.range c_1 c_n)
*/ */
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
zstring s; zstring slo, shi;
unsigned len = 0; unsigned len = 0;
bool is_empty = false; bool is_empty = false;
if (str().is_string(lo, s) && s.length() != 1) if (str().is_string(lo, slo) && slo.length() != 1)
is_empty = true; is_empty = true;
if (str().is_string(hi, s) && s.length() != 1) if (str().is_string(hi, shi) && shi.length() != 1)
is_empty = true;
if (slo.length() == 1 && shi.length() == 1 && slo[0] > shi[0])
is_empty = true; is_empty = true;
len = min_length(lo).second; len = min_length(lo).second;
if (len > 1) if (len > 1)
@ -5246,7 +5248,17 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
else if (re().is_range(r, r1, r2) && else if (re().is_range(r, r1, r2) &&
str().is_string(r1, s1) && str().is_string(r2, s2) && str().is_string(r1, s1) && str().is_string(r2, s2) &&
s1.length() == 1 && s2.length() == 1) { s1.length() == 1 && s2.length() == 1) {
result = m().mk_bool_val(s1[0] <= s2[0]); result = m().mk_bool_val(s1[0] > s2[0]);
return BR_DONE;
}
else if (re().is_range(r, r1, r2) &&
str().is_string(r1, s1) && s1.length() != 1) {
result = m().mk_true();
return BR_DONE;
}
else if (re().is_range(r, r1, r2) &&
str().is_string(r2, s2) && s2.length() != 1) {
result = m().mk_true();
return BR_DONE; return BR_DONE;
} }
else if ((re().is_loop(r, r1, lo) || else if ((re().is_loop(r, r1, lo) ||
@ -5307,6 +5319,7 @@ br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) {
} }
br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
TRACE("seq", tout << mk_pp(l, m()) << " == " << mk_pp(r, m()) << "\n");
expr_ref_vector res(m()); expr_ref_vector res(m());
expr_ref_pair_vector new_eqs(m()); expr_ref_pair_vector new_eqs(m());
if (m_util.is_re(l)) { if (m_util.is_re(l)) {