mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 14:23:35 +00:00
Code Activity

Implement not_contains_axiom in seq_axioms.cpp (#9098)

Browse source 
* 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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-03-22 21:34:45 -07:00 • committed by GitHub
parent 8db175447b
commit ced7952a7b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 40 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,6 +34,7 @@ namespace seq {
a(m), a(m),
seq(m), seq(m),
m_sk(m, r), m_sk(m, r),
m_not_contains(m),
m_clause(m), m_clause(m),
m_trail(m) m_trail(m)
{} {}
@ -1346,7 +1347,44 @@ namespace seq {
*/ */
void axioms::not_contains_axiom(expr *e) { 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) { expr_ref axioms::length_limit(expr* s, unsigned k) {

1
src/ast/rewriter/seq_axioms.h
View file

@ -32,6 +32,7 @@ namespace seq {
arith_util a; arith_util a;
seq_util seq; seq_util seq;
skolem m_sk; skolem m_sk;
func_decl_ref m_not_contains;
expr_ref_vector m_clause; expr_ref_vector m_clause;
expr_ref_vector m_trail; expr_ref_vector m_trail;
obj_map<expr, expr*> m_purified; obj_map<expr, expr*> m_purified;