mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 00:26:38 +00:00
remove unneeded reverse case in derivative; placeholder for generalized lifted derivative
This commit is contained in:
calebstanford-msr
parent
c967b4aead
commit
9987adbe20
1 changed files with 164 additions and 23 deletions
|
|
@ -2207,7 +2207,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
|
|||
}
|
||||
|
||||
/*
|
||||
Push reverse inwards (gets stuck at variables and strings).
|
||||
Push reverse inwards (whenever possible).
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
|
||||
sort* seq_sort = nullptr;
|
||||
|
|
@ -2286,7 +2286,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
|
|||
return BR_REWRITE3;
|
||||
}
|
||||
else {
|
||||
// stuck cases: variable, re().is_to_re, re().is_derivative, ...
|
||||
// stuck cases: variable, re().is_derivative, ...
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
|
|
@ -2410,26 +2410,6 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
|
|||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {
|
||||
// Reverses are rewritten so that the only derivative case is
|
||||
// derivative of a reverse of a string. (All other cases stuck)
|
||||
// This is analagous to the previous is_to_re case.
|
||||
expr_ref hd(m()), tl(m());
|
||||
if (get_head_tail_reversed(r2, hd, tl)) {
|
||||
result = re_and(
|
||||
m().mk_eq(ele, tl),
|
||||
re().mk_reverse(re().mk_to_re(hd))
|
||||
);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
else if (str().is_empty(r2)) {
|
||||
result = re().mk_empty(m().get_sort(r));
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
else if (re().is_range(r, r1, r2)) {
|
||||
// r1, r2 are sequences.
|
||||
zstring s1, s2;
|
||||
|
|
@ -2465,10 +2445,171 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
|
|||
return BR_REWRITE2;
|
||||
}
|
||||
// stuck cases: re().is_derivative, variable, ...
|
||||
// and re().is_reverse if the reverse is not applied to a string
|
||||
// and re().is_reverse
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
/*
|
||||
Generalized "lifted" symbolic derivative
|
||||
lifted in the sense of having the following type:
|
||||
regex -> (List (pred * regex))
|
||||
The list [(p1, r1), (p2, r2), ...] represents
|
||||
a regex disjunction: if(p1, r1, none) or if(p2, r2, none) or ...
|
||||
*/
|
||||
// br_status seq_rewriter::gen_derivative(expr* r, expr_ref& result) {
|
||||
// sort* seq_sort = nullptr, *ele_sort = nullptr;
|
||||
// VERIFY(m_util.is_re(r, seq_sort));
|
||||
// VERIFY(m_util.is_seq(seq_sort, ele_sort));
|
||||
// SASSERT(ele_sort == m().get_sort(ele));
|
||||
// expr* r1 = nullptr, *r2 = nullptr, *p = nullptr;
|
||||
// unsigned lo = 0, hi = 0;
|
||||
// if (re().is_concat(r, r1, r2)) {
|
||||
// expr_ref is_n = is_nullable(r1);
|
||||
// expr_ref dr1(re().mk_derivative(ele, r1), m());
|
||||
// expr_ref dr2(re().mk_derivative(ele, r2), m());
|
||||
// result = re().mk_concat(dr1, r2);
|
||||
// if (m().is_false(is_n)) {
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (m().is_true(is_n)) {
|
||||
// result = re().mk_union(result, dr2);
|
||||
// return BR_REWRITE3;
|
||||
// }
|
||||
// else {
|
||||
// result = re().mk_union(result, re_and(is_n, dr2));
|
||||
// return BR_REWRITE3;
|
||||
// }
|
||||
// }
|
||||
// else if (re().is_star(r, r1)) {
|
||||
// result = re().mk_concat(re().mk_derivative(ele, r1), r);
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_plus(r, r1)) {
|
||||
// result = re().mk_derivative(ele, re().mk_star(r1));
|
||||
// return BR_REWRITE1;
|
||||
// }
|
||||
// else if (re().is_union(r, r1, r2)) {
|
||||
// result = re().mk_union(
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_derivative(ele, r2)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_intersection(r, r1, r2)) {
|
||||
// result = re().mk_inter(
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_derivative(ele, r2)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_diff(r, r1, r2)) {
|
||||
// result = re().mk_diff(
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_derivative(ele, r2)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (m().is_ite(r, p, r1, r2)) {
|
||||
// result = m().mk_ite(
|
||||
// p,
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_derivative(ele, r2)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_opt(r, r1)) {
|
||||
// result = re().mk_derivative(ele, r1);
|
||||
// return BR_REWRITE1;
|
||||
// }
|
||||
// else if (re().is_complement(r, r1)) {
|
||||
// result = re().mk_complement(re().mk_derivative(ele, r1));
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_loop(r, r1, lo)) {
|
||||
// if (lo > 0) {
|
||||
// lo--;
|
||||
// }
|
||||
// result = re().mk_concat(
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_loop(r1, lo)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_loop(r, r1, lo, hi)) {
|
||||
// if (hi == 0) {
|
||||
// result = re().mk_empty(m().get_sort(r));
|
||||
// return BR_DONE;
|
||||
// }
|
||||
// hi--;
|
||||
// if (lo > 0) {
|
||||
// lo--;
|
||||
// }
|
||||
// result = re().mk_concat(
|
||||
// re().mk_derivative(ele, r1),
|
||||
// re().mk_loop(r1, lo, hi)
|
||||
// );
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (re().is_full_seq(r) ||
|
||||
// re().is_empty(r)) {
|
||||
// result = r;
|
||||
// return BR_DONE;
|
||||
// }
|
||||
// else if (re().is_to_re(r, r1)) {
|
||||
// // r1 is a string here (not a regexp)
|
||||
// expr_ref hd(m()), tl(m());
|
||||
// if (get_head_tail(r1, hd, tl)) {
|
||||
// // head must be equal; if so, derivative is tail
|
||||
// result = re_and(m().mk_eq(ele, hd),re().mk_to_re(tl));
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// else if (str().is_empty(r1)) {
|
||||
// result = re().mk_empty(m().get_sort(r));
|
||||
// return BR_DONE;
|
||||
// }
|
||||
// else {
|
||||
// return BR_FAILED;
|
||||
// }
|
||||
// }
|
||||
// else if (re().is_range(r, r1, r2)) {
|
||||
// // r1, r2 are sequences.
|
||||
// zstring s1, s2;
|
||||
// if (str().is_string(r1, s1) && str().is_string(r2, s2)) {
|
||||
// if (s1.length() == 1 && s2.length() == 1) {
|
||||
// r1 = m_util.mk_char(s1[0]);
|
||||
// r2 = m_util.mk_char(s2[0]);
|
||||
// result = m().mk_and(m_util.mk_le(r1, ele), m_util.mk_le(ele, r2));
|
||||
// result = re_predicate(result, seq_sort);
|
||||
// return BR_REWRITE3;
|
||||
// }
|
||||
// else {
|
||||
// result = re().mk_empty(m().get_sort(r));
|
||||
// return BR_DONE;
|
||||
// }
|
||||
// }
|
||||
// expr* e1 = nullptr, *e2 = nullptr;
|
||||
// if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
|
||||
// result = m().mk_and(m_util.mk_le(e1, ele), m_util.mk_le(ele, e2));
|
||||
// result = re_predicate(result, seq_sort);
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// }
|
||||
// else if (re().is_full_char(r)) {
|
||||
// result = re().mk_to_re(str().mk_empty(seq_sort));
|
||||
// return BR_DONE;
|
||||
// }
|
||||
// else if (re().is_of_pred(r, p)) {
|
||||
// array_util array(m());
|
||||
// expr* args[2] = { p, ele };
|
||||
// result = array.mk_select(2, args);
|
||||
// result = re_predicate(result, seq_sort);
|
||||
// return BR_REWRITE2;
|
||||
// }
|
||||
// // stuck cases: re().is_derivative, variable, ...
|
||||
// // and re().is_reverse
|
||||
// return BR_FAILED;
|
||||
// }
|
||||
|
||||
/*
|
||||
* pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes.
|
||||
*/
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue