From ad7b2489565df3f3d7569b7db68f4421bfb6c8f7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Oct 2025 14:04:51 -0700
Subject: [PATCH] add outline of axiomatization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/finite_set_axioms.h          | 85 +++++++++++++++++++
 ...s_rewriter.cpp => finite_set_rewriter.cpp} |  0
 ..._sets_rewriter.h => finite_set_rewriter.h} |  2 +-
 3 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 src/ast/rewriter/finite_set_axioms.h
 rename src/ast/rewriter/{finite_sets_rewriter.cpp => finite_set_rewriter.cpp} (100%)
 rename src/ast/rewriter/{finite_sets_rewriter.h => finite_set_rewriter.h} (93%)

diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h
new file mode 100644
index 000000000..4bc853fbd
--- /dev/null
+++ b/src/ast/rewriter/finite_set_axioms.h
@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_set_axioms.h
+
+Abstract:
+    Axiom schemas for finite sets.
+
+    Axiom schemars for finite sets are instantiated based on the state of the
+    congruence closure and existing assertions in for finite sets.
+    This module implements axiom schemas that are invoked by saturating constraints
+    with respect to the semantics of set operations. 
+
+    Let v1 ~ v2 mean that v1 and v2 are congruent
+
+    The set-based decision procedure relies on saturating with respect
+    to rules of the form:
+    
+      x in v1 == v2, v1 ~ set.empty
+    --------------------------------
+       not (x in set.empty)
+
+
+     x in v1 == v2, v1 ~ v3, v3 == (set.union v4 v5)
+     -----------------------------------------------
+           x in v1 <=> x in v4 or x in v5    
+ 
+
+    set.in : S (FiniteSet S) -> Bool
+    set.size : (FiniteSet S) -> Int
+    set.subset : (FiniteSet S) (FiniteSet S) -> Bool
+    set.map : (S -> T) (FiniteSet S) -> (FiniteSet T)
+    set.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S)
+    set.range : Int Int -> (FiniteSet Int)
+       
+--*/
+
+class finite_set_axioms {
+    ast_manager&    m;
+    finite_set_util u;
+
+    std::function<void(expr_ref_vector const &)> m_add_clause;
+
+public:
+
+    finite_set_axioms(ast_manager &m) : m(m), u(m) {}
+
+    void set_add_clause(std::function<void(expr_ref_vector const &)> &ac) {
+        m_add_clause = ac;
+    }
+
+    // a ~ set.empty => not (x in a)
+    void in_empty_axiom(expr *x);
+
+    // a := set.union(b, c) 
+    // (x in a) <=> (x in b) or (x in c)
+    void in_union_axiom(expr *x, expr *a);
+
+    // a := set.intersect(b, c)
+    // (x in a) <=> (x in b) and (x in c)
+    void in_intersect_axiom(expr *x, expr *a);
+    
+    // a := set.difference(b, c)
+    // (x in a) <=> (x in b) and not (x in c)
+    void in_difference_axiom(expr *x, expr *a);
+
+    // a := set.singleton(b)
+    // (x in a) <=> (x == b)
+    void in_singleton_axiom(expr *x, expr *a);
+
+    // a := set.range(lo, hi)
+    // (x in a) <=> (lo <= x <= hi)
+    void in_range_axiom(expr *x, expr *a);
+
+    // a := set.map(f, b)
+    // (x in a) <=> set.map_inverse(f, x, b)
+    void in_map_axiom(expr *x, expr *a);
+
+    // a := set.select(p, b)
+    // (x in a) <=> (x in b) and p(x)
+    void in_select_axiom(expr *x, expr *a);
+
+};
\ No newline at end of file
diff --git a/src/ast/rewriter/finite_sets_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp
similarity index 100%
rename from src/ast/rewriter/finite_sets_rewriter.cpp
rename to src/ast/rewriter/finite_set_rewriter.cpp
diff --git a/src/ast/rewriter/finite_sets_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h
similarity index 93%
rename from src/ast/rewriter/finite_sets_rewriter.h
rename to src/ast/rewriter/finite_set_rewriter.h
index f99d9b5a5..bd3334cc9 100644
--- a/src/ast/rewriter/finite_sets_rewriter.h
+++ b/src/ast/rewriter/finite_set_rewriter.h
@@ -3,7 +3,7 @@ Copyright (c) 2025 Microsoft Corporation
 
 Module Name:
 
-    finite_sets_rewriter.h
+    finite_set_rewriter.h
 
 Abstract:
     Rewriting Simplification for finite sets