mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

add to spec

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-13 22:53:27 +02:00
parent 75bac9c0ce
commit 5dacb270f8
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/finite_set_rewriter.h
View file

@ -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);
};