mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

use recursive function for not-contains

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-23 13:18:34 -07:00
parent ced7952a7b
commit dbdccbff97
4 changed files with 40 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/seq_axioms.cpp
View file

@ -268,14 +268,20 @@ namespace seq {
m_sk.decompose(s, head, tail);
TRACE(seq, tout << "tail " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
expr_ref emp = mk_eq_empty(s);
add_clause(emp, mk_seq_eq(s, mk_concat(head, e)));
expr_ref con = mk_concat(head, e);
if (m_mark_no_diseq)
m_mark_no_diseq(con);
add_clause(emp, mk_seq_eq(s, con));
add_clause(~emp, mk_eq_empty(e));
}
void axioms::drop_last_axiom(expr* e, expr* s) {
TRACE(seq, tout << "drop last " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
expr_ref emp = mk_eq_empty(s);
add_clause(emp, mk_seq_eq(s, mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s)))));
expr_ref con = mk_concat(e, seq.str.mk_unit(m_sk.mk_last(s)));
if (m_mark_no_diseq)
m_mark_no_diseq(con);
add_clause(emp, mk_seq_eq(s, con));
add_clause(~emp, mk_eq_empty(e));
}
@ -1364,12 +1370,12 @@ namespace seq {
var_ref vp(m.mk_var(0, srt), m);
expr_ref len_s(seq.str.mk_length(vs), m);
expr_ref len_p(seq.str.mk_length(vp), m);
// expr_ref tail_s(seq.str.mk_substr(vs, a.mk_int(1), a.mk_sub(len_s, a.mk_int(1))), m);
expr_ref tail_s(m_sk.mk("tail.s", vs), m);
expr* nc_args[2] = { tail_s.get(), vp.get() };
expr_ref head(m), tail(m);
m_sk.decompose(vs, head, tail);
expr* nc_args[2] = { tail.get(), vp.get() };
expr_ref pref(seq.str.mk_prefix(vp, vs), m);
expr_ref hd(seq.str.mk_unit(seq.str.mk_nth_i(vs, a.mk_int(0))), m);
expr_ref decomp(m.mk_eq(vs, seq.str.mk_concat(hd, tail_s)), m);
expr_ref decomp(m.mk_eq(vs, seq.str.mk_concat(hd, tail)), m);
expr_ref else_branch(m.mk_and(m.mk_not(pref), m.mk_and(decomp, m.mk_app(m_not_contains.get(), 2, nc_args))), m);
expr_ref body(m.mk_ite(a.mk_gt(len_p, len_s),
m.mk_true(),

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

@ -3149,9 +3149,14 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr*
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));
else {
expr_ref th(mk_antimirov_deriv_intersection(e, a, d2, path_and_c), m());
expr_ref el(mk_antimirov_deriv_intersection(e, b, d2, path_and_notc), m());
if (th == el)
result = th;
else
result = m().mk_ite(c, th, el);
}
}
else if (m().is_ite(d2))
// swap d1 and d2
@ -3207,8 +3212,14 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) {
result = nothing();
else if (re().is_dot_plus(d))
result = epsilon();
else if (m().is_ite(d, c, t, e))
result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
else if (m().is_ite(d, c, t, e)) {
expr_ref th(mk_antimirov_deriv_negate(elem, t), m());
expr_ref el(mk_antimirov_deriv_negate(elem, e), m());
if (th == el)
result = th;
else
result = m().mk_ite(c, th, el);
}
else if (re().is_union(d, t, e))
result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true());
else if (re().is_intersection(d, t, e))
@ -3226,9 +3237,15 @@ expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) {
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));
if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2) && c1 == c2) {
expr_ref th(mk_antimirov_deriv_union(t1, t2), m());
expr_ref el(mk_antimirov_deriv_union(e1, e2), m());
if (th == el)
result = th;
else
// eliminate duplicate branching on exactly the same condition
result = m().mk_ite(c1, th, el);
}
else
result = mk_regex_union_normalize(d1, d2);
return result;
@ -6066,6 +6083,7 @@ lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vect
re_eval_pos current = todo.back();
todo.pop_back();
r = current.e;
// IF_VERBOSE(1, verbose_stream() << "derive " << mk_pp(r, m()) << "\n");
str.resize(current.str_len);
if (current.needs_derivation) {
SASSERT(current.exclude.empty());

3
src/smt/seq_model.cpp
View file

@ -308,12 +308,11 @@ namespace smt {
// We checked non-emptiness during Nielsen already
lbool wr = m_rewriter.some_seq_in_re(re_expr, witness);
if (wr == l_true && witness) {
// std::cout << "Witness for " << mk_pp(var->get_expr(), m) << " in " <<
// mk_pp(re_expr, m) << ": " << mk_pp(witness, m) << std::endl;
m_trail.push_back(witness);
m_factory->register_value(witness);
return witness;
}
IF_VERBOSE(1, verbose_stream() << "witness extraction failed: " << wr << "\n" << mk_pp(re_expr, m) << "\n");
UNREACHABLE();
}

2
src/smt/theory_nseq.cpp
View file

@ -246,7 +246,7 @@ namespace smt {
if (is_true)
m_axioms.contains_true_axiom(e);
else
m_axioms.unroll_not_contains(e);
m_axioms.not_contains_axiom(e);
}
else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) {
// axioms added via relevant_eh → dequeue_axiom