diff --git a/src/ast/rewriter/finite_sets_rewriter.cpp b/src/ast/rewriter/finite_sets_rewriter.cpp
new file mode 100644
index 000000000..8b1378917
--- /dev/null
+++ b/src/ast/rewriter/finite_sets_rewriter.cpp
@@ -0,0 +1 @@
+
diff --git a/src/ast/rewriter/finite_sets_rewriter.h b/src/ast/rewriter/finite_sets_rewriter.h
new file mode 100644
index 000000000..f99d9b5a5
--- /dev/null
+++ b/src/ast/rewriter/finite_sets_rewriter.h
@@ -0,0 +1,20 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_sets_rewriter.h
+
+Abstract:
+    Rewriting Simplification for finite sets
+
+
+Sampe rewrite rules:
+    set.union s set.empty -> s
+    set.intersect s set.empty -> set.empty
+    set.in x (set.singleton y) -> x = y
+
+Generally this module implements basic algebraic simplificaiton rules for finite sets
+where the signature is defined in finite_sets_decl_plugin.h.
+   
+--*/