From a2352529f82a8a0992a7e75bef1303b5c693253f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Mar 2026 12:58:17 -0700 Subject: [PATCH] add diseq axiom Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 21 +++++++++++++++++++++ src/ast/rewriter/seq_axioms.h | 1 + 2 files changed, 22 insertions(+) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index af6204de5..5528b7eb7 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -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)); + } + } diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 583898562..48828a4e6 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -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);