From 4b40969da6a825717a9776f6ce798f69b4c7ae63 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Mar 2026 13:32:18 -0700
Subject: [PATCH] added diseq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_nseq.cpp | 56 +++++++++++++++++++++++++----------------
 src/smt/theory_nseq.h   |  6 +++--
 2 files changed, 39 insertions(+), 23 deletions(-)

diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index da3e20ac7..ad2fc99ca 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -27,17 +27,47 @@ namespace smt {
     theory_nseq::theory_nseq(context& ctx) :
         theory(ctx, ctx.get_manager().mk_family_id("seq")),
         m_seq(m),
-        m_autil(m),
+        m_autil(m), 
+        m_th_rewriter(m),
         m_rewriter(m),
         m_arith_value(m),
         m_egraph(m),
         m_sgraph(m, m_egraph),
         m_context_solver(m),
         m_nielsen(m_sgraph, m_context_solver),
+        m_axioms(m_th_rewriter),
         m_state(),
         m_regex(m_sgraph),
         m_model(m, m_seq, m_rewriter, m_sgraph)
-    {}
+    {
+        std::function<void(expr_ref_vector const&)> add_clause =
+            [&](expr_ref_vector const &clause) {
+            literal_vector lits;
+            for (auto const &e : clause) {
+                auto lit = mk_literal(e);
+                if (lit == false_literal)
+                    continue;
+                if (lit == true_literal)
+                    return;
+                if (ctx.get_assignment(lit) == l_true)
+                    return;
+                ctx.mark_as_relevant(lit);
+                lits.push_back(lit);
+            }
+            // TODO - add validation, trace axioms
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
+        };
+        std::function < void(expr* e)> set_phase = [&](expr* e) {
+            literal lit = mk_literal(e);
+            ctx.force_phase(lit);
+        };
+        std::function < void(void)> ensure_digit_axiom = [&]() {
+            throw default_exception("digit axioms should be added lazily via seq_axioms::ensure_digit_axiom");
+        };
+        m_axioms.set_add_clause(add_clause);
+        m_axioms.set_phase(set_phase);
+        m_axioms.set_ensure_digits(ensure_digit_axiom);
+    }
 
     // -----------------------------------------------------------------------
     // Initialization
@@ -154,12 +184,10 @@ namespace smt {
             push_unhandled_pred();
             return;
         }
-        if (!m_seq.is_seq(e1) || !m_seq.is_seq(e2))
+        if (!m_seq.is_seq(e1))
             return;
-        unsigned idx = m_state.diseqs().size();
-        m_state.add_diseq(get_enode(v1), get_enode(v2));
-        ctx.push_trail(restore_vector(m_prop_queue));
-        m_prop_queue.push_back({prop_item::diseq_prop, idx});
+
+        m_axioms.diseq_axiom(e1, e2);
     }
 
     // -----------------------------------------------------------------------
@@ -243,9 +271,6 @@ namespace smt {
             case prop_item::eq_prop:
                 propagate_eq(idx);
                 break;
-            case prop_item::diseq_prop:
-                propagate_diseq(idx);
-                break;
             case prop_item::pos_mem_prop:
                 propagate_pos_mem(idx);
                 break;
@@ -261,17 +286,6 @@ namespace smt {
         ensure_length_var(src.m_r->get_expr());
     }
 
-    void theory_nseq::propagate_diseq(unsigned idx) {
-        // Disequalities are recorded for use during final_check.
-        // No eager propagation beyond recording.
-        TRACE(seq,
-            auto const& d = m_state.get_diseq(idx);
-            tout << "nseq diseq: "
-                 << mk_bounded_pp(d.m_n1->get_expr(), m, 3)
-                 << " != "
-                 << mk_bounded_pp(d.m_n2->get_expr(), m, 3) << "\n";);
-    }
-
     void theory_nseq::propagate_pos_mem(unsigned idx) {
         auto const& mem = m_state.str_mems()[idx];
 
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index 2a9fd1d53..7c107de57 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -21,6 +21,7 @@ Author:
 
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
+#include "ast/rewriter/seq_axioms.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/euf/euf_sgraph.h"
 #include "smt/smt_theory.h"
@@ -36,6 +37,7 @@ namespace smt {
     class theory_nseq : public theory {
         seq_util       m_seq;
         arith_util     m_autil;
+        th_rewriter    m_th_rewriter;
         seq_rewriter   m_rewriter;
         arith_value    m_arith_value;
         euf::egraph    m_egraph;  // private egraph (not shared with smt context)
@@ -44,13 +46,14 @@ namespace smt {
         // to the m_nielsen constructor and must remain stable for the object's lifetime.
         context_solver m_context_solver;
         seq::nielsen_graph m_nielsen;
+        seq::axioms m_axioms;
         seq_state     m_state;
         seq::seq_regex     m_regex;   // regex membership pre-processing
         seq_model     m_model;   // model construction helper
 
         // propagation queue
         struct prop_item {
-            enum kind_t { eq_prop, diseq_prop, pos_mem_prop } m_kind;
+            enum kind_t { eq_prop, pos_mem_prop } m_kind;
             unsigned m_idx;
         };
         svector<prop_item>  m_prop_queue;
@@ -110,7 +113,6 @@ namespace smt {
 
         // propagation dispatch helpers
         void propagate_eq(unsigned idx);
-        void propagate_diseq(unsigned idx);
         void propagate_pos_mem(unsigned idx);
         void ensure_length_var(expr* e);