mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix re.range rewrite for theory_str
This commit is contained in:
parent
4d5c1dcfb6
commit
c198bc5863
|
@ -350,7 +350,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
SASSERT(num_args == 2);
|
||||
return mk_re_union(args[0], args[1], result);
|
||||
case OP_RE_RANGE:
|
||||
return BR_FAILED;
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_range(args[0], args[1], result);
|
||||
case OP_RE_INTERSECT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_inter(args[0], args[1], result);
|
||||
|
@ -1313,6 +1314,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
/*
|
||||
* (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
|
||||
TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
|
||||
zstring str_lo, str_hi;
|
||||
if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
|
||||
if (str_lo.length() == 1 && str_hi.length() == 1) {
|
||||
unsigned int c1 = str_lo[0];
|
||||
unsigned int c2 = str_hi[0];
|
||||
if (c1 > c2) {
|
||||
// exchange c1 and c2
|
||||
unsigned int tmp = c1;
|
||||
c2 = c1;
|
||||
c1 = tmp;
|
||||
}
|
||||
zstring s(c1);
|
||||
expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
|
||||
for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
|
||||
zstring s_ch(ch);
|
||||
expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
|
||||
acc = m_util.re.mk_union(acc, acc2);
|
||||
}
|
||||
result = acc;
|
||||
return BR_REWRITE2;
|
||||
} else {
|
||||
m().raise_exception("string constants in re.range must have length 1");
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
/*
|
||||
emp+ = emp
|
||||
all+ = all
|
||||
|
@ -1342,9 +1376,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
// result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
|
||||
// return BR_REWRITE2;
|
||||
//return BR_FAILED;
|
||||
result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
|
||||
|
|
|
@ -120,6 +120,7 @@ class seq_rewriter {
|
|||
br_status mk_re_plus(expr* a, expr_ref& result);
|
||||
br_status mk_re_opt(expr* a, expr_ref& result);
|
||||
br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
|
||||
br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
|
||||
|
||||
bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
|
||||
bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r,
|
||||
|
|
Loading…
Reference in a new issue