mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
Add comprehensive algebraic rewrite rules to finite_set_rewriter (#7975)
* Initial plan * Add comprehensive rewrite rules for finite set operations Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add comprehensive unit tests for finite set rewrite rules Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix order of checks in mk_in to handle singleton same element case first Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- 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>
This commit is contained in:
Copilot
GitHub
parent
4225f1a0f1
commit
2e7f80f597
2 changed files with 309 additions and 16 deletions
|
|
@ -31,55 +31,169 @@ br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, exp
|
|||
case OP_FINITE_SET_SUBSET:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_subset(args[0], args[1], result);
|
||||
case OP_FINITE_SET_SINGLETON:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_singleton(args[0], result);
|
||||
case OP_FINITE_SET_IN:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_in(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
|
||||
// Idempotency: 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
|
||||
// Identity: set.union(x, empty) -> x or set.union(empty, x) -> x
|
||||
if (num_args == 2) {
|
||||
if (m_util.is_empty(args[0])) {
|
||||
result = args[1];
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_empty(args[1])) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// Absorption: set.union(x, set.intersect(x, y)) -> x
|
||||
expr* a1, *a2;
|
||||
if (m_util.is_intersect(args[1], a1, a2)) {
|
||||
if (args[0] == a1 || args[0] == a2) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
// Absorption: set.union(set.intersect(x, y), x) -> x
|
||||
if (m_util.is_intersect(args[0], a1, a2)) {
|
||||
if (args[1] == a1 || args[1] == a2) {
|
||||
result = args[1];
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
// set.intersect(x, x) -> x
|
||||
// Idempotency: set.intersect(x, x) -> x
|
||||
if (num_args == 2 && args[0] == args[1]) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// Annihilation: set.intersect(x, empty) -> empty or set.intersect(empty, x) -> empty
|
||||
if (num_args == 2) {
|
||||
if (m_util.is_empty(args[0])) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_empty(args[1])) {
|
||||
result = args[1];
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// Absorption: set.intersect(x, set.union(x, y)) -> x
|
||||
expr* a1, *a2;
|
||||
if (m_util.is_union(args[1], a1, a2)) {
|
||||
if (args[0] == a1 || args[0] == a2) {
|
||||
result = args[0];
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
// Absorption: set.intersect(set.union(x, y), x) -> x
|
||||
if (m_util.is_union(args[0], a1, a2)) {
|
||||
if (args[1] == a1 || args[1] == a2) {
|
||||
result = args[1];
|
||||
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;
|
||||
}
|
||||
|
||||
// Identity: set.difference(x, empty) -> x
|
||||
if (m_util.is_empty(arg2)) {
|
||||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// Annihilation: set.difference(empty, x) -> empty
|
||||
if (m_util.is_empty(arg1)) {
|
||||
result = arg1;
|
||||
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
|
||||
// set.subset(x, x) -> true
|
||||
if (arg1 == arg2) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// set.subset(empty, x) -> true
|
||||
if (m_util.is_empty(arg1)) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// set.subset(x, empty) -> x = empty
|
||||
if (m_util.is_empty(arg2)) {
|
||||
result = m().mk_eq(arg1, arg2);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
// General case: 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;
|
||||
}
|
||||
|
||||
br_status finite_set_rewriter::mk_singleton(expr * arg, expr_ref & result) {
|
||||
// Singleton is already in normal form, no simplifications
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) {
|
||||
// set.in(x, empty) -> false
|
||||
if (m_util.is_empty(set)) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// set.in(x, singleton(y)) checks
|
||||
expr* singleton_elem;
|
||||
if (m_util.is_singleton(set, singleton_elem)) {
|
||||
// set.in(x, singleton(x)) -> true (when x is the same)
|
||||
if (elem == singleton_elem) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
// set.in(x, singleton(y)) -> x = y (when x != y)
|
||||
result = m().mk_eq(elem, singleton_elem);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -36,9 +36,9 @@ static void test_union_idempotent() {
|
|||
app_ref s1(fsets.mk_range(zero, ten), m);
|
||||
|
||||
// Test set.union(s1, s1) -> s1
|
||||
expr* args[2] = { s1, s1 };
|
||||
app_ref union_app(fsets.mk_union(s1, s1), m);
|
||||
expr_ref result(m);
|
||||
br_status st = rw.mk_union(2, args, result);
|
||||
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);
|
||||
|
|
@ -59,9 +59,9 @@ static void test_intersect_idempotent() {
|
|||
app_ref s1(fsets.mk_range(zero, ten), m);
|
||||
|
||||
// Test set.intersect(s1, s1) -> s1
|
||||
expr* args[2] = { s1, s1 };
|
||||
app_ref intersect_app(fsets.mk_intersect(s1, s1), m);
|
||||
expr_ref result(m);
|
||||
br_status st = rw.mk_intersect(2, args, result);
|
||||
br_status st = rw.mk_app_core(intersect_app->get_decl(), intersect_app->get_num_args(), intersect_app->get_args(), result);
|
||||
|
||||
ENSURE(st == BR_DONE);
|
||||
ENSURE(result == s1);
|
||||
|
|
@ -82,8 +82,9 @@ static void test_difference_same() {
|
|||
app_ref s1(fsets.mk_range(zero, ten), m);
|
||||
|
||||
// Test set.difference(s1, s1) -> empty
|
||||
app_ref diff_app(fsets.mk_difference(s1, s1), m);
|
||||
expr_ref result(m);
|
||||
br_status st = rw.mk_difference(s1, s1, result);
|
||||
br_status st = rw.mk_app_core(diff_app->get_decl(), diff_app->get_num_args(), diff_app->get_args(), result);
|
||||
|
||||
ENSURE(st == BR_DONE);
|
||||
ENSURE(fsets.is_empty(result));
|
||||
|
|
@ -106,8 +107,9 @@ static void test_subset_rewrite() {
|
|||
app_ref s2(fsets.mk_range(zero, twenty), m);
|
||||
|
||||
// Test set.subset(s1, s2) -> set.intersect(s1, s2) = s1
|
||||
app_ref subset_app(fsets.mk_subset(s1, s2), m);
|
||||
expr_ref result(m);
|
||||
br_status st = rw.mk_subset(s1, s2, result);
|
||||
br_status st = rw.mk_app_core(subset_app->get_decl(), subset_app->get_num_args(), subset_app->get_args(), result);
|
||||
|
||||
ENSURE(st == BR_REWRITE3);
|
||||
ENSURE(m.is_eq(result));
|
||||
|
|
@ -148,10 +150,187 @@ static void test_mk_app_core() {
|
|||
ENSURE(result == s1);
|
||||
}
|
||||
|
||||
static void test_union_with_empty() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create a set and empty 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);
|
||||
app_ref empty_set(fsets.mk_empty(s1->get_sort()), m);
|
||||
|
||||
// Test set.union(s1, empty) -> s1
|
||||
app_ref union_app1(fsets.mk_union(s1, empty_set), m);
|
||||
expr_ref result1(m);
|
||||
br_status st1 = rw.mk_app_core(union_app1->get_decl(), union_app1->get_num_args(), union_app1->get_args(), result1);
|
||||
ENSURE(st1 == BR_DONE);
|
||||
ENSURE(result1 == s1);
|
||||
|
||||
// Test set.union(empty, s1) -> s1
|
||||
app_ref union_app2(fsets.mk_union(empty_set, s1), m);
|
||||
expr_ref result2(m);
|
||||
br_status st2 = rw.mk_app_core(union_app2->get_decl(), union_app2->get_num_args(), union_app2->get_args(), result2);
|
||||
ENSURE(st2 == BR_DONE);
|
||||
ENSURE(result2 == s1);
|
||||
}
|
||||
|
||||
static void test_intersect_with_empty() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create a set and empty 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);
|
||||
app_ref empty_set(fsets.mk_empty(s1->get_sort()), m);
|
||||
|
||||
// Test set.intersect(s1, empty) -> empty
|
||||
app_ref intersect_app1(fsets.mk_intersect(s1, empty_set), m);
|
||||
expr_ref result1(m);
|
||||
br_status st1 = rw.mk_app_core(intersect_app1->get_decl(), intersect_app1->get_num_args(), intersect_app1->get_args(), result1);
|
||||
ENSURE(st1 == BR_DONE);
|
||||
ENSURE(result1 == empty_set);
|
||||
|
||||
// Test set.intersect(empty, s1) -> empty
|
||||
app_ref intersect_app2(fsets.mk_intersect(empty_set, s1), m);
|
||||
expr_ref result2(m);
|
||||
br_status st2 = rw.mk_app_core(intersect_app2->get_decl(), intersect_app2->get_num_args(), intersect_app2->get_args(), result2);
|
||||
ENSURE(st2 == BR_DONE);
|
||||
ENSURE(result2 == empty_set);
|
||||
}
|
||||
|
||||
static void test_difference_with_empty() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create a set and empty 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);
|
||||
app_ref empty_set(fsets.mk_empty(s1->get_sort()), m);
|
||||
|
||||
// Test set.difference(s1, empty) -> s1
|
||||
app_ref diff_app1(fsets.mk_difference(s1, empty_set), m);
|
||||
expr_ref result1(m);
|
||||
br_status st1 = rw.mk_app_core(diff_app1->get_decl(), diff_app1->get_num_args(), diff_app1->get_args(), result1);
|
||||
ENSURE(st1 == BR_DONE);
|
||||
ENSURE(result1 == s1);
|
||||
|
||||
// Test set.difference(empty, s1) -> empty
|
||||
app_ref diff_app2(fsets.mk_difference(empty_set, s1), m);
|
||||
expr_ref result2(m);
|
||||
br_status st2 = rw.mk_app_core(diff_app2->get_decl(), diff_app2->get_num_args(), diff_app2->get_args(), result2);
|
||||
ENSURE(st2 == BR_DONE);
|
||||
ENSURE(result2 == empty_set);
|
||||
}
|
||||
|
||||
static void test_subset_with_empty() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create a set and empty 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);
|
||||
app_ref empty_set(fsets.mk_empty(s1->get_sort()), m);
|
||||
|
||||
// Test set.subset(empty, s1) -> true
|
||||
app_ref subset_app1(fsets.mk_subset(empty_set, s1), m);
|
||||
expr_ref result1(m);
|
||||
br_status st1 = rw.mk_app_core(subset_app1->get_decl(), subset_app1->get_num_args(), subset_app1->get_args(), result1);
|
||||
ENSURE(st1 == BR_DONE);
|
||||
ENSURE(m.is_true(result1));
|
||||
|
||||
// Test set.subset(s1, s1) -> true
|
||||
app_ref subset_app2(fsets.mk_subset(s1, s1), m);
|
||||
expr_ref result2(m);
|
||||
br_status st2 = rw.mk_app_core(subset_app2->get_decl(), subset_app2->get_num_args(), subset_app2->get_args(), result2);
|
||||
ENSURE(st2 == BR_DONE);
|
||||
ENSURE(m.is_true(result2));
|
||||
}
|
||||
|
||||
static void test_in_singleton() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create elements and singleton
|
||||
expr_ref five(arith.mk_int(5), m);
|
||||
expr_ref ten(arith.mk_int(10), m);
|
||||
app_ref singleton_five(fsets.mk_singleton(five), m);
|
||||
|
||||
// Test set.in(five, singleton(five)) -> true
|
||||
app_ref in_app1(fsets.mk_in(five, singleton_five), m);
|
||||
expr_ref result1(m);
|
||||
br_status st1 = rw.mk_app_core(in_app1->get_decl(), in_app1->get_num_args(), in_app1->get_args(), result1);
|
||||
ENSURE(st1 == BR_DONE);
|
||||
ENSURE(m.is_true(result1));
|
||||
|
||||
// Test set.in(ten, singleton(five)) -> ten = five
|
||||
app_ref in_app2(fsets.mk_in(ten, singleton_five), m);
|
||||
expr_ref result2(m);
|
||||
br_status st2 = rw.mk_app_core(in_app2->get_decl(), in_app2->get_num_args(), in_app2->get_args(), result2);
|
||||
ENSURE(st2 == BR_REWRITE1);
|
||||
ENSURE(m.is_eq(result2));
|
||||
}
|
||||
|
||||
static void test_in_empty() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
||||
finite_set_util fsets(m);
|
||||
finite_set_rewriter rw(m);
|
||||
arith_util arith(m);
|
||||
|
||||
// Create element and empty set
|
||||
sort_ref int_sort(arith.mk_int(), m);
|
||||
expr_ref five(arith.mk_int(5), m);
|
||||
parameter param(int_sort.get());
|
||||
sort_ref set_sort(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, ¶m), m);
|
||||
app_ref empty_set(fsets.mk_empty(set_sort), m);
|
||||
|
||||
// Test set.in(five, empty) -> false
|
||||
app_ref in_app(fsets.mk_in(five, empty_set), m);
|
||||
expr_ref result(m);
|
||||
br_status st = rw.mk_app_core(in_app->get_decl(), in_app->get_num_args(), in_app->get_args(), result);
|
||||
ENSURE(st == BR_DONE);
|
||||
ENSURE(m.is_false(result));
|
||||
}
|
||||
|
||||
void tst_finite_set_rewriter() {
|
||||
test_union_idempotent();
|
||||
test_intersect_idempotent();
|
||||
test_difference_same();
|
||||
test_subset_rewrite();
|
||||
test_mk_app_core();
|
||||
test_union_with_empty();
|
||||
test_intersect_with_empty();
|
||||
test_difference_with_empty();
|
||||
test_subset_with_empty();
|
||||
test_in_singleton();
|
||||
test_in_empty();
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue