Skip to content

Commit

Permalink
make the rule a in (str.to_re a') -> (a == a') working always again
Browse files Browse the repository at this point in the history
jurajsic committed Apr 27, 2024
1 parent 0fa55a5 commit 5e0e87f
Showing 1 changed file with 2 additions and 13 deletions.
15 changes: 2 additions & 13 deletions src/ast/rewriter/seq_rewriter.cpp
Original file line number Diff line number Diff line change
@@ -4544,19 +4544,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
}
expr_ref b_s(m());
if (lift_str_from_to_re(b, b_s)) {
// NOODLER we do not apply
// a in (str.to_re a') -> (a == a')
// always, because replacing regexes to equalities
// can then lead to disequalities (if there is negation before),
// however, that is not beneficial for noodler.
// Instead, we replace only if there is a variable (noodler cannot handle var in regex)
m_lhs.reset();
str().get_concat(b_s, m_lhs);
remove_empty_and_concats(m_lhs);
if (has_var(m_lhs)) {
result = m_br.mk_eq_rw(a, b_s);
return BR_REWRITE_FULL;
}
result = m_br.mk_eq_rw(a, b_s);
return BR_REWRITE_FULL;
}
expr* b1 = nullptr;
expr* eps = nullptr;

0 comments on commit 5e0e87f

Please sign in to comment.