From 522be5d8c2598e69f344f9f359c76eec518230ee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Oct 2025 18:14:43 -0700 Subject: [PATCH] add stub for rewriter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/finite_sets_rewriter.cpp | 1 + src/ast/rewriter/finite_sets_rewriter.h | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 src/ast/rewriter/finite_sets_rewriter.cpp create mode 100644 src/ast/rewriter/finite_sets_rewriter.h 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. + +--*/