From 5dacb270f80537b82bf1c5b727330dd09baca394 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Oct 2025 22:53:27 +0200 Subject: [PATCH] add to spec Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/finite_set_rewriter.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index 933e45d11..cc028d3ff 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -6,8 +6,8 @@ Module Name: finite_set_rewriter.h Abstract: - Rewriting Simplification for finite sets + Rewriting Simplification for finite sets Sample rewrite rules: set.union s set.empty -> s @@ -18,6 +18,7 @@ Sample rewrite rules: set.intersect(x, x) -> x set.difference(x, x) -> set.empty + Generally this module implements basic algebraic simplification rules for finite sets where the signature is defined in finite_set_decl_plugin.h. @@ -50,3 +51,4 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); }; +