From ced7952a7b51a8a8079b6469710326549d558dca Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Mar 2026 21:34:45 -0700 Subject: [PATCH] Implement not_contains_axiom in seq_axioms.cpp (#9098) * Implement not_contains_axiom in seq_axioms.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2df315a7-6f41-4d22-9e77-1e778d97fdb8 * Rewrite not_contains_axiom using recfun recursive function instead of skolem predicate Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/28c9f40f-e66f-41b6-bec0-efff6bc9f902 * Use structural decomposition a = unit(nth(a,0)) ++ tail(a) in not_contains_axiom else-branch Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/e35f6eaa-4c4a-4629-bce2-c6a2a96e2ace * Refactor tail_s initialization in seq_axioms.cpp --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 40 ++++++++++++++++++++++++++++++++- src/ast/rewriter/seq_axioms.h | 1 + 2 files changed, 40 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index ffb6a36c4..510282938 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -34,6 +34,7 @@ namespace seq { a(m), seq(m), m_sk(m, r), + m_not_contains(m), m_clause(m), m_trail(m) {} @@ -1346,7 +1347,44 @@ namespace seq { */ void axioms::not_contains_axiom(expr *e) { - throw default_exception("not implemented"); + expr* _a = nullptr, *_b = nullptr; + VERIFY(seq.str.is_contains(e, _a, _b)); + auto ca = purify(_a); + auto cb = purify(_b); + sort* srt = ca->get_sort(); + + if (!m_not_contains || m_not_contains->get_domain(0) != srt) { + recfun::util rec(m); + recfun::decl::plugin& plugin = rec.get_plugin(); + recfun_replace rf(m); + sort* domain[2] = { srt, srt }; + auto d = plugin.ensure_def(symbol("nc"), 2, domain, m.mk_bool_sort(), true); + m_not_contains = d.get_def()->get_decl(); + var_ref vs(m.mk_var(1, srt), m); + 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 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 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(), + m.mk_ite(m.mk_eq(len_p, len_s), + m.mk_not(m.mk_eq(vs, vp)), + else_branch)), + m); + var* vars[2] = { vs, vp }; + plugin.set_definition(rf, d, false, 2, vars, body); + } + + expr* app_args[2] = { ca.get(), cb.get() }; + expr_ref nc_app(m.mk_app(m_not_contains.get(), 2, app_args), m); + expr_ref cnt(e, m); + add_clause(cnt, nc_app); } expr_ref axioms::length_limit(expr* s, unsigned k) { diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 29fffe00f..53d448f7d 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -32,6 +32,7 @@ namespace seq { arith_util a; seq_util seq; skolem m_sk; + func_decl_ref m_not_contains; expr_ref_vector m_clause; expr_ref_vector m_trail; obj_map m_purified;