From c526c20cfc0f1978a614b4aa101980a4db49b5b1 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 14 Oct 2025 17:13:18 +0200 Subject: [PATCH] Implement finite_set_rewriter with basic algebraic simplification rules (#7972) * Initial plan * Add finite_set_rewriter implementation with basic rewrite rules Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix finite_set_decl_plugin bug and complete implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert finite_set_decl_plugin changes and disable difference rule Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Re-enable difference rule using set_sort directly Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update finite_set_rewriter.h --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/finite_set_rewriter.cpp | 84 ++++++++++++ src/ast/rewriter/finite_set_rewriter.h | 38 +++++- src/test/CMakeLists.txt | 1 + src/test/finite_set_rewriter.cpp | 157 +++++++++++++++++++++++ src/test/main.cpp | 1 + 6 files changed, 279 insertions(+), 3 deletions(-) create mode 100644 src/test/finite_set_rewriter.cpp diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 8e6306c7e..ade2dabee 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -22,6 +22,7 @@ z3_add_component(rewriter expr_safe_replace.cpp factor_equivs.cpp factor_rewriter.cpp + finite_set_rewriter.cpp fpa_rewriter.cpp func_decl_replace.cpp inj_axiom.cpp diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp index 8b1378917..03edbfb68 100644 --- a/src/ast/rewriter/finite_set_rewriter.cpp +++ b/src/ast/rewriter/finite_set_rewriter.cpp @@ -1 +1,85 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation +Module Name: + + finite_set_rewriter.cpp + +Abstract: + + Rewriting Simplification for finite sets + +Author: + + GitHub Copilot Agent 2025 + +--*/ + +#include "ast/rewriter/finite_set_rewriter.h" + +br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(f->get_family_id() == get_fid()); + + switch (f->get_decl_kind()) { + case OP_FINITE_SET_UNION: + return mk_union(num_args, args, result); + case OP_FINITE_SET_INTERSECT: + return mk_intersect(num_args, args, result); + case OP_FINITE_SET_DIFFERENCE: + SASSERT(num_args == 2); + return mk_difference(args[0], args[1], result); + case OP_FINITE_SET_SUBSET: + SASSERT(num_args == 2); + return mk_subset(args[0], args[1], result); + default: + return BR_FAILED; + } +} + +br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args, expr_ref & result) { + // Handle binary case - check if both arguments are the same + // set.union(x, x) -> x + if (num_args == 2 && args[0] == args[1]) { + result = args[0]; + return BR_DONE; + } + + // Additional simplifications can be added here + // For example: set.union(x, empty) -> x + // But for now, we keep it minimal as per requirements + + return BR_FAILED; +} + +br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * args, expr_ref & result) { + // set.intersect(x, x) -> x + if (num_args == 2 && args[0] == args[1]) { + result = args[0]; + return BR_DONE; + } + + return BR_FAILED; +} + +br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref & result) { + // set.difference(x, x) -> set.empty + if (arg1 == arg2) { + // Get the set sort directly from the argument + sort* set_sort = arg1->get_sort(); + SASSERT(m_util.is_finite_set(set_sort)); + + // Call mk_empty with set_sort directly as suggested + result = m_util.mk_empty(set_sort); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status finite_set_rewriter::mk_subset(expr * arg1, expr * arg2, expr_ref & result) { + // set.subset(x, y) -> set.intersect(x, y) = x + expr_ref intersect(m()); + intersect = m_util.mk_intersect(arg1, arg2); + result = m().mk_eq(intersect, arg1); + return BR_REWRITE3; +} diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index bd3334cc9..933e45d11 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -9,12 +9,44 @@ Abstract: Rewriting Simplification for finite sets -Sampe rewrite rules: +Sample rewrite rules: set.union s set.empty -> s set.intersect s set.empty -> set.empty set.in x (set.singleton y) -> x = y + set.subset(x,y) -> set.intersect(x,y) = x + set.union(x, x) -> x + set.intersect(x, x) -> x + set.difference(x, x) -> set.empty -Generally this module implements basic algebraic simplificaiton rules for finite sets -where the signature is defined in finite_sets_decl_plugin.h. +Generally this module implements basic algebraic simplification rules for finite sets +where the signature is defined in finite_set_decl_plugin.h. --*/ +#pragma once + +#include "ast/finite_set_decl_plugin.h" +#include "ast/rewriter/rewriter_types.h" +#include "util/params.h" + +/** + \brief Cheap rewrite rules for finite sets +*/ +class finite_set_rewriter { + finite_set_util m_util; + // Rewrite rules for set operations + br_status mk_union(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_intersect(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_difference(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_subset(expr * arg1, expr * arg2, expr_ref & result); +public: + finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()): + m_util(m) { + } + + ast_manager & m() const { return m_util.get_manager(); } + family_id get_fid() const { return m_util.get_family_id(); } + finite_set_util& util() { return m_util; } + + br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + +}; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index ac9585b1a..647351060 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -55,6 +55,7 @@ add_executable(test-z3 ext_numeral.cpp f2n.cpp finite_set.cpp + finite_set_rewriter.cpp factor_rewriter.cpp finder.cpp fixed_bit_vector.cpp diff --git a/src/test/finite_set_rewriter.cpp b/src/test/finite_set_rewriter.cpp new file mode 100644 index 000000000..3aaf9ec83 --- /dev/null +++ b/src/test/finite_set_rewriter.cpp @@ -0,0 +1,157 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_rewriter.cpp + +Abstract: + + Test finite set rewriter + +Author: + + GitHub Copilot Agent 2025 + +--*/ + +#include "ast/ast.h" +#include "ast/finite_set_decl_plugin.h" +#include "ast/reg_decl_plugins.h" +#include "ast/arith_decl_plugin.h" +#include "ast/rewriter/finite_set_rewriter.h" + +static void test_union_idempotent() { + ast_manager m; + reg_decl_plugins(m); + + finite_set_util fsets(m); + finite_set_rewriter rw(m); + arith_util arith(m); + + // Create a set + sort_ref int_sort(arith.mk_int(), m); + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + app_ref s1(fsets.mk_range(zero, ten), m); + + // Test set.union(s1, s1) -> s1 + expr* args[2] = { s1, s1 }; + expr_ref result(m); + br_status st = rw.mk_union(2, args, result); + + ENSURE(st == BR_DONE); + ENSURE(result == s1); +} + +static void test_intersect_idempotent() { + ast_manager m; + reg_decl_plugins(m); + + finite_set_util fsets(m); + finite_set_rewriter rw(m); + arith_util arith(m); + + // Create a set + sort_ref int_sort(arith.mk_int(), m); + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + app_ref s1(fsets.mk_range(zero, ten), m); + + // Test set.intersect(s1, s1) -> s1 + expr* args[2] = { s1, s1 }; + expr_ref result(m); + br_status st = rw.mk_intersect(2, args, result); + + ENSURE(st == BR_DONE); + ENSURE(result == s1); +} + +static void test_difference_same() { + ast_manager m; + reg_decl_plugins(m); + + finite_set_util fsets(m); + finite_set_rewriter rw(m); + arith_util arith(m); + + // Create a set + sort_ref int_sort(arith.mk_int(), m); + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + app_ref s1(fsets.mk_range(zero, ten), m); + + // Test set.difference(s1, s1) -> empty + expr_ref result(m); + br_status st = rw.mk_difference(s1, s1, result); + + ENSURE(st == BR_DONE); + ENSURE(fsets.is_empty(result)); +} + +static void test_subset_rewrite() { + ast_manager m; + reg_decl_plugins(m); + + finite_set_util fsets(m); + finite_set_rewriter rw(m); + arith_util arith(m); + + // Create two sets + sort_ref int_sort(arith.mk_int(), m); + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + expr_ref twenty(arith.mk_int(20), m); + app_ref s1(fsets.mk_range(zero, ten), m); + app_ref s2(fsets.mk_range(zero, twenty), m); + + // Test set.subset(s1, s2) -> set.intersect(s1, s2) = s1 + expr_ref result(m); + br_status st = rw.mk_subset(s1, s2, result); + + ENSURE(st == BR_REWRITE3); + ENSURE(m.is_eq(result)); + + // Check that result is an equality + app* eq = to_app(result); + ENSURE(eq->get_num_args() == 2); + + // The left side should be set.intersect(s1, s2) + expr* lhs = eq->get_arg(0); + ENSURE(fsets.is_intersect(lhs)); + + // The right side should be s1 + expr* rhs = eq->get_arg(1); + ENSURE(rhs == s1); +} + +static void test_mk_app_core() { + ast_manager m; + reg_decl_plugins(m); + + finite_set_util fsets(m); + finite_set_rewriter rw(m); + arith_util arith(m); + + // Create sets + sort_ref int_sort(arith.mk_int(), m); + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + app_ref s1(fsets.mk_range(zero, ten), m); + + // Test union through mk_app_core + app_ref union_app(fsets.mk_union(s1, s1), m); + expr_ref result(m); + br_status st = rw.mk_app_core(union_app->get_decl(), union_app->get_num_args(), union_app->get_args(), result); + + ENSURE(st == BR_DONE); + ENSURE(result == s1); +} + +void tst_finite_set_rewriter() { + test_union_idempotent(); + test_intersect_idempotent(); + test_difference_same(); + test_subset_rewrite(); + test_mk_app_core(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index d7ff6cf71..1c1f6862a 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -283,4 +283,5 @@ int main(int argc, char ** argv) { TST(sls_seq_plugin); TST(ho_matcher); TST(finite_set); + TST(finite_set_rewriter); }