From aa1f1f56b6f40437279d35780815774df786c3aa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 17 Oct 2025 16:54:12 +0200
Subject: [PATCH] prepare for incremental axiom propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_finite_set.cpp | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 21ca5153b..947d365c2 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -126,8 +126,14 @@ namespace smt {
 
     void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) {
         TRACE(finite_set, tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";);
-        // When two sets are equal, propagate membership constraints
-        // This is handled by congruence closure, so no additional work needed here
+        //    x = y, y in S
+        // -------------------
+        //  axioms for x in S
+
+        auto n1 = get_enode(v1);
+        auto n2 = get_enode(v2);
+        auto e1 = n1->get_expr();
+        auto e2 = n2->get_expr();
     }
 
     void theory_finite_set::new_diseq_eh(theory_var v1, theory_var v2) {
@@ -191,6 +197,10 @@ namespace smt {
         // Assert all new lemmas as clauses
         for (unsigned i = sz; i < m_theory_axioms.size(); ++i) 
             assert_clause(m_theory_axioms[i]);
+
+
+        // TODO also add axioms for x in S u T, x in S n T, etc to the stack of m_theory_axioms.
+        // The axioms are then instantiated if they are propagating.
     }
 
     /**
@@ -363,6 +373,9 @@ namespace smt {
             if (!ctx.is_relevant(x))
                 continue;
             x = x->get_root();
+            if (x->is_marked())
+                continue;
+            x->set_mark();  // make sure we only do this once per element
             // TODO: use marking of x to avoid duplicate work
             for (auto p : enode::parents(x)) {
                 if (!ctx.is_relevant(p))
@@ -381,6 +394,11 @@ namespace smt {
                 m_set_members.find(set)->insert(x);
             }
         }
+        for (auto x : m_elements) {
+            x = x->get_root();
+            if (x->is_marked())
+                x->unset_mark();
+        }
     }
 
     struct finite_set_value_proc : model_value_proc {