From 0f4126f665ed902d9c8dfbe92f329ff150a25b74 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2026 23:15:23 -0700 Subject: [PATCH] add filter for avoiding creating redundant disequality axioms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 10 ++++++++-- src/ast/rewriter/seq_axioms.h | 4 ++++ src/smt/theory_nseq.cpp | 8 +++++++- src/smt/theory_nseq.h | 1 + 4 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index b47b946a2..2c32fc476 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1357,8 +1357,14 @@ namespace seq { expr_ref vp = m_sk.mk("diseq.v'", u, v); expr_ref up_len(mk_len(up), m); expr_ref vp_len(mk_len(vp), m); - 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); + expr_ref wau(mk_concat(w, seq.str.mk_unit(a), up), m); + expr_ref wbv(mk_concat(w, seq.str.mk_unit(b), vp), m); + expr_ref u_eq(mk_eq(u, wau), m); + expr_ref v_eq(mk_eq(v, wbv), m); + if (m_mark_no_diseq) { + m_mark_no_diseq(wau); + m_mark_no_diseq(wbv); + } 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 4a1b8b96e..0c29ad5d8 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -38,6 +38,7 @@ namespace seq { std::function m_add_clause; std::function m_set_phase; std::function m_ensure_digits; + std::function m_mark_no_diseq; expr_ref mk_len(expr* s); expr_ref mk_sub(expr* x, expr* y); @@ -81,6 +82,9 @@ namespace seq { void set_add_clause(std::function& ac) { m_add_clause = ac; } void set_phase(std::function& sp) { m_set_phase = sp; } void set_ensure_digits(std::function& ed) { m_ensure_digits = ed; } + void set_mark_no_diseq(std::function &f) { + m_mark_no_diseq = f; + } void suffix_axiom(expr* n); void prefix_axiom(expr* n); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 8e59e847c..9e1149984 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -63,9 +63,14 @@ namespace smt { std::function < void(void)> ensure_digit_axiom = [&]() { throw default_exception("digit axioms should be added lazily via seq_axioms::ensure_digit_axiom"); }; + std::function mark_no_diseq = [&](expr *e) { + m_no_diseq_set.insert(e); + ctx.push_trail(insert_obj_trail(m_no_diseq_set, e)); + }; m_axioms.set_add_clause(add_clause); m_axioms.set_phase(set_phase); m_axioms.set_ensure_digits(ensure_digit_axiom); + m_axioms.set_mark_no_diseq(mark_no_diseq); } // ----------------------------------------------------------------------- @@ -177,10 +182,11 @@ namespace smt { void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) { expr* e1 = get_enode(v1)->get_expr(); expr* e2 = get_enode(v2)->get_expr(); + TRACE(seq, tout << mk_pp(e1, m) << " != " << mk_pp(e2, m) << "\n"); if (m_seq.is_re(e1)) // regex disequality: nseq cannot verify language non-equivalence push_unhandled_pred(); - else if (m_seq.is_seq(e1)) + else if (m_seq.is_seq(e1) && !m_no_diseq_set.contains(e1) && !m_no_diseq_set.contains(e2)) m_axioms.diseq_axiom(e1, e2); else ; diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 959853acd..efcd1f672 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -62,6 +62,7 @@ namespace smt { unsigned m_prop_qhead = 0; unsigned m_next_mem_id = 0; // monotone counter for tracked_str_mem ids obj_hashtable m_axiom_set; // dedup guard for axiom_item enqueues + obj_hashtable m_no_diseq_set; // track expressions that should not trigger new disequality axioms // statistics unsigned m_num_conflicts = 0;