mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

move seq_derive and fix include paths, remove antimirov code

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-03 11:04:19 -07:00
parent 1f28fd0e6b
commit cb2cf913e3
6 changed files with 3 additions and 421 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2921,390 +2921,6 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
return m_derive(ele, r);
}
expr_ref seq_rewriter::mk_antimirov_deriv(expr* e, expr* r, expr* path) {
// Ensure references are owned
expr_ref _e(e, m()), _path(path, m()), _r(r, m());
expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, e, r, path), m());
if (!result) {
mk_antimirov_deriv_rec(e, r, path, result);
m_op_cache.insert(OP_RE_DERIVATIVE, e, r, path, result);
STRACE(seq_regex, tout << "D(" << mk_pp(e, m()) << "," << mk_pp(r, m()) << "," << mk_pp(path, m()) << ")" << std::endl;);
STRACE(seq_regex, tout << "= " << mk_pp(result, m()) << std::endl;);
}
return result;
}
void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result) {
sort* seq_sort = nullptr, * ele_sort = nullptr;
expr_ref _r(r, m()), _path(path, m());
VERIFY(m_util.is_re(r, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort));
SASSERT(ele_sort == e->get_sort());
expr* r1 = nullptr, * r2 = nullptr, * c = nullptr;
expr_ref c1(m());
expr_ref c2(m());
auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); };
auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); };
unsigned lo = 0, hi = 0;
if (re().is_empty(r) || re().is_epsilon(r))
// D(e,[]) = D(e,()) = []
result = nothing();
else if (re().is_full_seq(r) || re().is_dot_plus(r))
// D(e,.*) = D(e,.+) = .*
result = dotstar();
else if (re().is_full_char(r))
// D(e,.) = ()
result = epsilon();
else if (re().is_to_re(r, r1)) {
expr_ref h(m());
expr_ref t(m());
// here r1 is a sequence
if (get_head_tail(r1, h, t)) {
if (eq_char(e, h))
result = re().mk_to_re(t);
else if (neq_char(e, h))
result = nothing();
else
result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing());
}
else {
// observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
{
auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto eq_first = m().mk_eq(mk_seq_first(r1), e);
m_br.mk_and(is_non_empty, eq_first, c1);
}
m_br.mk_and(path, c1, c2);
if (m().is_false(c2))
result = nothing();
else
// observe that the precondition |r1|>0 is implied by c1 for use of mk_seq_rest
result = m().mk_ite(c1, re().mk_to_re(mk_seq_rest(r1)), nothing());
}
}
else if (re().is_reverse(r, r2))
if (re().is_to_re(r2, r1)) {
// here r1 is a sequence
// observe that the precondition |r1|>0 of mk_seq_last is implied by c1
{
auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto eq_last = m().mk_eq(mk_seq_last(r1), e);
m_br.mk_and(is_non_empty, eq_last, c1);
}
m_br.mk_and(path, c1, c2);
if (m().is_false(c2))
result = nothing();
else
// observe that the precondition |r1|>0 of mk_seq_rest is implied by c1
result = re().mk_ite_simplify(c1, re().mk_reverse(re().mk_to_re(mk_seq_butlast(r1))), nothing());
}
else {
result = mk_regex_reverse(r2);
if (result.get() == r)
//r2 is an uninterpreted regex that is stuck
//for example if r = (re.reverse R) where R is a regex variable then
//here result.get() == r
result = re().mk_derivative(e, result);
else
result = mk_antimirov_deriv(e, result, path);
}
else if (re().is_concat(r, r1, r2)) {
expr_ref r1nullable(is_nullable(r1), m());
c1 = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), r2);
expr_ref r1nullable_and_path(m());
m_br.mk_and(r1nullable, path, r1nullable_and_path);
if (m().is_false(r1nullable_and_path))
// D(e,r1)r2
result = c1;
else
// D(e,r1)r2|(ite (r1nullable) (D(e,r2)) [])
// observe that (mk_ite_simplify(true, D(e,r2), []) = D(e,r2)
result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
}
else if (m().is_ite(r, c, r1, r2)) {
{
auto cp = m().mk_and(c, path);
c1 = simplify_path(e, cp);
}
{
auto notc = m().mk_not(c);
auto np = m().mk_and(notc, path);
c2 = simplify_path(e, np);
}
if (m().is_false(c1))
result = mk_antimirov_deriv(e, r2, c2);
else if (m().is_false(c2))
result = mk_antimirov_deriv(e, r1, c1);
else
result = re().mk_ite_simplify(c, mk_antimirov_deriv(e, r1, c1), mk_antimirov_deriv(e, r2, c2));
}
else if (re().is_range(r, r1, r2)) {
expr_ref range(m());
expr_ref psi(m().mk_false(), m());
if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
// SASSERT(u().is_char(c1));
// SASSERT(u().is_char(c2));
// case: c1 <= e <= c2
// deterministic evaluation for range bounds
auto a_le = u().mk_le(c1, e);
auto b_le = u().mk_le(e, c2);
auto rng_cond = m().mk_and(a_le, b_le);
range = simplify_path(e, rng_cond);
psi = simplify_path(e, m().mk_and(path, range));
}
else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
SASSERT(u().is_char(c2));
// r1 nonground: |r1|=1 & r1[0] <= e <= c2
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
expr_ref r1_0(str().mk_nth_i(r1, zero), m());
range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2))));
psi = simplify_path(e, m().mk_and(path, range));
}
else if (!str().is_string(r2) && str().is_unit_string(r1, c1)) {
SASSERT(u().is_char(c1));
// r2 nonground: |r2|=1 & c1 <= e <= r2_0
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
expr_ref r2_0(str().mk_nth_i(r2, zero), m());
range = simplify_path(e, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0))));
psi = simplify_path(e, m().mk_and(path, range));
}
else if (!str().is_string(r1) && !str().is_string(r2)) {
// both r1 and r2 nonground: |r1|=1 & |r2|=1 & r1[0] <= e <= r2[0]
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
expr_ref r1_0(str().mk_nth_i(r1, zero), m());
expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
expr_ref r2_0(str().mk_nth_i(r2, zero), m());
range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0)))));
psi = simplify_path(e, m().mk_and(path, range));
}
if (m().is_false(psi))
result = nothing();
else
result = re().mk_ite_simplify(range, epsilon(), nothing());
}
else if (re().is_union(r, r1, r2))
result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));
else if (re().is_intersection(r, r1, r2))
result = mk_antimirov_deriv_intersection(e,
mk_antimirov_deriv(e, r1, path),
mk_antimirov_deriv(e, r2, path), m().mk_true());
else if (re().is_star(r, r1) || re().is_plus(r, r1) || (re().is_loop(r, r1, lo) && 0 <= lo && lo <= 1))
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_star(r1));
else if (re().is_loop(r, r1, lo))
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, lo - 1));
else if (re().is_loop(r, r1, lo, hi)) {
if ((lo == 0 && hi == 0) || hi < lo)
result = nothing();
else {
expr_ref t(re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1), m());
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), t);
}
}
else if (re().is_opt(r, r1))
result = mk_antimirov_deriv(e, r1, path);
else if (re().is_complement(r, r1))
// D(e,~r1) = ~D(e,r1)
result = mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r1, path));
else if (re().is_diff(r, r1, r2))
result = mk_antimirov_deriv_intersection(e,
mk_antimirov_deriv(e, r1, path),
mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r2, path)), m().mk_true());
else if (re().is_of_pred(r, r1)) {
array_util array(m());
expr* args[2] = { r1, e };
result = array.mk_select(2, args);
// Use mk_der_cond to normalize
result = mk_der_cond(result, e, seq_sort);
}
else
// stuck cases
result = re().mk_derivative(e, r);
}
expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* d2, expr* path) {
sort* seq_sort = nullptr, * ele_sort = nullptr;
VERIFY(m_util.is_re(d1, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort));
expr_ref result(m());
expr* c, * a, * b;
if (m_re_deriv_depth >= m_max_re_deriv_depth) {
// Depth limit reached: construct intersection without further decomposition
result = mk_regex_inter_normalize(d1, d2);
}
else if (re().is_empty(d1))
result = d1;
else if (re().is_empty(d2))
result = d2;
else if (m().is_ite(d1, c, a, b)) {
expr_ref path_and_c(simplify_path(e, m().mk_and(path, c)), m());
expr_ref path_and_notc(simplify_path(e, m().mk_and(path, m().mk_not(c))), m());
++m_re_deriv_depth;
if (m().is_false(path_and_c))
result = mk_antimirov_deriv_intersection(e, b, d2, path);
else if (m().is_false(path_and_notc))
result = mk_antimirov_deriv_intersection(e, a, d2, path);
else
result = m().mk_ite(c, mk_antimirov_deriv_intersection(e, a, d2, path_and_c),
mk_antimirov_deriv_intersection(e, b, d2, path_and_notc));
--m_re_deriv_depth;
}
else if (m().is_ite(d2)) {
// swap d1 and d2
++m_re_deriv_depth;
result = mk_antimirov_deriv_intersection(e, d2, d1, path);
--m_re_deriv_depth;
}
else if (d1 == d2 || re().is_full_seq(d2))
result = mk_antimirov_deriv_restrict(e, d1, path);
else if (re().is_full_seq(d1))
result = mk_antimirov_deriv_restrict(e, d2, path);
else if (re().is_union(d1, a, b)) {
// distribute intersection over the union in d1
++m_re_deriv_depth;
result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path),
mk_antimirov_deriv_intersection(e, b, d2, path));
--m_re_deriv_depth;
}
else if (re().is_union(d2, a, b)) {
// distribute intersection over the union in d2
++m_re_deriv_depth;
result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path),
mk_antimirov_deriv_intersection(e, d1, b, path));
--m_re_deriv_depth;
}
else
result = mk_regex_inter_normalize(d1, d2);
return result;
}
expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
expr_ref result(m());
expr_ref _r(r, m()), _d(d, m());
expr* c, * t, * e;
if (m_re_deriv_depth >= m_max_re_deriv_depth) {
// Depth limit reached: construct concat without further decomposition
result = mk_re_append(d, r);
}
else if (m().is_ite(d, c, t, e)) {
++m_re_deriv_depth;
auto r2 = mk_antimirov_deriv_concat(e, r);
auto r1 = mk_antimirov_deriv_concat(t, r);
--m_re_deriv_depth;
result = m().mk_ite(c, r1, r2);
}
else if (re().is_union(d, t, e)) {
++m_re_deriv_depth;
result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
--m_re_deriv_depth;
}
else
result = mk_re_append(d, r);
SASSERT(result.get());
return result;
}
expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) {
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(d, seq_sort));
auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); };
auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
auto dotstar = [&]() { return expr_ref(re().mk_full_seq(d->get_sort()), m()); };
auto dotplus = [&]() { return expr_ref(re().mk_plus(re().mk_full_char(d->get_sort())), m()); };
expr_ref result(m());
expr* c, * t, * e;
if (m_re_deriv_depth >= m_max_re_deriv_depth) {
// Depth limit reached: construct complement without further decomposition
result = re().mk_complement(d);
}
else if (re().is_empty(d))
result = dotstar();
else if (re().is_epsilon(d))
result = dotplus();
else if (re().is_full_seq(d))
result = nothing();
else if (re().is_dot_plus(d))
result = epsilon();
else if (m().is_ite(d, c, t, e)) {
++m_re_deriv_depth;
result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
--m_re_deriv_depth;
}
else if (re().is_union(d, t, e)) {
++m_re_deriv_depth;
result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true());
--m_re_deriv_depth;
}
else if (re().is_intersection(d, t, e)) {
++m_re_deriv_depth;
result = mk_antimirov_deriv_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
--m_re_deriv_depth;
}
else if (re().is_complement(d, t))
result = t;
else
result = re().mk_complement(d);
return result;
}
expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) {
sort* seq_sort = nullptr, * ele_sort = nullptr;
VERIFY(m_util.is_re(d1, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort));
expr_ref result(m());
expr* c1, * t1, * e1, * c2, * t2, * e2;
if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2) && c1 == c2)
// eliminate duplicate branching on exactly the same condition
result = m().mk_ite(c1, mk_antimirov_deriv_union(t1, t2), mk_antimirov_deriv_union(e1, e2));
else
result = mk_regex_union_normalize(d1, d2);
return result;
}
// restrict the guards of all conditionals id d and simplify the resulting derivative
// restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c))
// restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond)
// where {} U X = X, X U X = X
// restrict(R, cond) = R
//
// restrict(d, false) = []
//
// it is already assumed that the restriction takes place within a branch
// so the condition is not added explicitly but propagated down in order to eliminate
// infeasible cases
expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) {
expr_ref result(d, m());
expr_ref _cond(cond, m());
expr* c, * a, * b;
if (m().is_false(cond))
result = re().mk_empty(d->get_sort());
else if (re().is_empty(d) || m().is_true(cond))
result = d;
else if (m_re_deriv_depth >= m_max_re_deriv_depth)
result = d;
else if (m().is_ite(d, c, a, b)) {
expr_ref path_and_c(simplify_path(e, m().mk_and(cond, c)), m());
expr_ref path_and_notc(simplify_path(e, m().mk_and(cond, m().mk_not(c))), m());
++m_re_deriv_depth;
result = re().mk_ite_simplify(c, mk_antimirov_deriv_restrict(e, a, path_and_c),
mk_antimirov_deriv_restrict(e, b, path_and_notc));
--m_re_deriv_depth;
}
else if (re().is_union(d, a, b)) {
++m_re_deriv_depth;
expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m());
expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m());
--m_re_deriv_depth;
result = mk_antimirov_deriv_union(a1, b1);
}
return result;
}
expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
expr_ref _r1(r1, m()), _r2(r2, m());
@ -3551,29 +3167,6 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
return result;
}
expr_ref seq_rewriter::mk_in_antimirov(expr* s, expr* d){
expr_ref result(mk_in_antimirov_rec(s, d), m());
return result;
}
expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) {
expr* c, * d1, * d2;
expr_ref result(m());
if (re().is_full_seq(d) || (str().min_length(s) > 0 && re().is_dot_plus(d)))
// s in .* <==> true, also: s in .+ <==> true when |s|>0
result = m().mk_true();
else if (re().is_empty(d) || (str().min_length(s) > 0 && re().is_epsilon(d)))
// s in [] <==> false, also: s in () <==> false when |s|>0
result = m().mk_false();
else if (m().is_ite(d, c, d1, d2))
result = re().mk_ite_simplify(c, mk_in_antimirov_rec(s, d1), mk_in_antimirov_rec(s, d2));
else if (re().is_union(d, d1, d2))
m_br.mk_or(mk_in_antimirov_rec(s, d1), mk_in_antimirov_rec(s, d2), result);
else
result = re().mk_in_re(s, d);
return result;
}
/*
* calls elim_condition
*/