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 <nbjorner@microsoft.com>

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

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;
+}

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

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

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();
+}

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