mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

add diseq axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-18 12:58:17 -07:00
parent 777bda01a5
commit a2352529f8
2 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1307,5 +1307,26 @@ namespace seq {
return bound_tracker;
}
// |u| != |v| OR
// (u = w[a]u' AND v = w[b]v' AND a != b)
void axioms::diseq_axiom(expr *u, expr *v) {
expr_ref u_len(mk_len(u), m);
expr_ref v_len(mk_len(v), m);
expr_ref len_eq(mk_eq(u_len, v_len), m);
expr_ref eq_uv(mk_eq(u, v), m);
sort *char_sort = nullptr;
VERIFY(seq.is_seq(u->get_sort(), char_sort));
expr_ref a = m_sk.mk("diseq.a", u, v, char_sort);
expr_ref b = m_sk.mk("diseq.b", u, v, char_sort);
expr_ref w = m_sk.mk("diseq.w", u, v);
expr_ref up = m_sk.mk("diseq.u'", u, v);
expr_ref vp = m_sk.mk("diseq.v'", u, v);
expr_ref u_eq(mk_eq(u, mk_concat(w, seq.str.mk_unit(a), up)), m);
expr_ref v_eq(mk_eq(v, mk_concat(w, seq.str.mk_unit(b), vp)), m);
add_clause(eq_uv, ~len_eq, u_eq);
add_clause(eq_uv, ~len_eq, v_eq);
add_clause(eq_uv, ~len_eq, ~mk_eq(a, b));
}
}

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

@ -109,6 +109,7 @@ namespace seq {
void replace_re_axiom(expr* e);
void replace_all_axiom(expr* e);
void replace_re_all_axiom(expr* e);
void diseq_axiom(expr *l, expr *r);
expr_ref length_limit(expr* s, unsigned k);
expr_ref is_digit(expr* ch);