From 0371bbd1922d571958939ce23558be2d1dfb637f Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 16 Oct 2025 13:36:55 +0200 Subject: [PATCH] Extend finite_set_decl_plugin::is_value to support unions of empty/singleton sets (#7980) * Initial plan * Initial state - all tests passing Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement is_value for unions of empty/singleton sets 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 --- src/ast/finite_set_decl_plugin.cpp | 55 ++++++++++++++++++++++++++- src/test/finite_set.cpp | 61 +++++++++++++++++++++++++++++- 2 files changed, 114 insertions(+), 2 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 4d669e12a..891d5f6b9 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -189,7 +189,60 @@ bool finite_set_decl_plugin::is_fully_interp(sort * s) const { } bool finite_set_decl_plugin::is_value(app * e) const { - return is_unique_value(e); + // Check if e is a union of either empty sets or singleton sets, + // where the singleton member is a value. + // Use ptr_buffer and expr_fast_mark1 to avoid exponential overhead. + + ptr_buffer todo; + expr_fast_mark1 visited; + + todo.push_back(e); + + while (!todo.empty()) { + expr* current = todo.back(); + todo.pop_back(); + + // Skip if already visited + if (visited.is_marked(current)) + continue; + visited.mark(current); + + // Check if current is an app + if (!is_app(current)) + return false; + + app* a = to_app(current); + + // Check if it's an empty set + if (is_app_of(a, m_family_id, OP_FINITE_SET_EMPTY)) + continue; + + // Check if it's a singleton with a value element + if (is_app_of(a, m_family_id, OP_FINITE_SET_SINGLETON)) { + if (a->get_num_args() != 1) + return false; + expr* elem = a->get_arg(0); + if (!is_app(elem)) + return false; + if (!m_manager->is_value(elem)) + return false; + continue; + } + + // Check if it's a union + if (is_app_of(a, m_family_id, OP_FINITE_SET_UNION)) { + // Add arguments to todo list + for (unsigned i = 0; i < a->get_num_args(); ++i) { + todo.push_back(a->get_arg(i)); + } + continue; + } + + // If it's none of the above, it's not a value + return false; + } + + return true; } bool finite_set_decl_plugin::is_unique_value(app* e) const { diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp index 7c62e52c0..d9b9ee515 100644 --- a/src/test/finite_set.cpp +++ b/src/test/finite_set.cpp @@ -127,20 +127,78 @@ static void tst_finite_set_map_select() { ENSURE(selected_set->get_sort() == finite_set_int.get()); } -static void tst_finite_set_is_fully_interp() { +static void tst_finite_set_is_value() { ast_manager m; reg_decl_plugins(m); + + finite_set_util fsets(m); arith_util arith(m); + finite_set_decl_plugin* plugin = static_cast(m.get_plugin(fsets.get_family_id())); + + // Create Int sort and finite set sort // Test with Int sort (should be fully interpreted) sort_ref int_sort(arith.mk_int(), m); parameter int_param(int_sort.get()); sort_ref finite_set_int(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &int_param), m); + + // Test 1: Empty set is a value + app_ref empty_set(fsets.mk_empty(finite_set_int), m); + ENSURE(plugin->is_value(empty_set.get())); + + // Test 2: Singleton with value element is a value + expr_ref five(arith.mk_int(5), m); + app_ref singleton_five(fsets.mk_singleton(five), m); + ENSURE(plugin->is_value(singleton_five.get())); + + // Test 3: Union of empty and singleton is a value + app_ref union_empty_singleton(fsets.mk_union(empty_set, singleton_five), m); + ENSURE(plugin->is_value(union_empty_singleton.get())); + + // Test 4: Union of two singletons with value elements is a value + expr_ref seven(arith.mk_int(7), m); + app_ref singleton_seven(fsets.mk_singleton(seven), m); + app_ref union_two_singletons(fsets.mk_union(singleton_five, singleton_seven), m); + ENSURE(plugin->is_value(union_two_singletons.get())); + + // Test 5: Nested union of singletons and empty sets is a value + app_ref union_nested(fsets.mk_union(union_empty_singleton, singleton_seven), m); + ENSURE(plugin->is_value(union_nested.get())); + + // Test 6: Union with empty set is a value + app_ref union_empty_empty(fsets.mk_union(empty_set, empty_set), m); + ENSURE(plugin->is_value(union_empty_empty.get())); + + // Test 7: Triple union is a value + expr_ref nine(arith.mk_int(9), m); + app_ref singleton_nine(fsets.mk_singleton(nine), m); + app_ref union_temp(fsets.mk_union(singleton_five, singleton_seven), m); + app_ref union_triple(fsets.mk_union(union_temp, singleton_nine), m); + ENSURE(plugin->is_value(union_triple.get())); + + // Test 8: Range is NOT a value (it's not a union of empty/singletons) + expr_ref zero(arith.mk_int(0), m); + expr_ref ten(arith.mk_int(10), m); + app_ref range_set(fsets.mk_range(zero, ten), m); + ENSURE(!plugin->is_value(range_set.get())); + + // Test 9: Union with range is NOT a value + app_ref union_with_range(fsets.mk_union(singleton_five, range_set), m); + ENSURE(!plugin->is_value(union_with_range.get())); + + // Test 10: Intersect is NOT a value + app_ref intersect_set(fsets.mk_intersect(singleton_five, singleton_seven), m); + ENSURE(!plugin->is_value(intersect_set.get())); ENSURE(m.is_fully_interp(int_sort)); ENSURE(m.is_fully_interp(finite_set_int)); +} + +static void tst_finite_set_is_fully_interp() { + ast_manager m; + reg_decl_plugins(m); // Test with Bool sort (should be fully interpreted) sort_ref bool_sort(m.mk_bool_sort(), m); @@ -162,5 +220,6 @@ static void tst_finite_set_is_fully_interp() { void tst_finite_set() { tst_finite_set_basic(); tst_finite_set_map_select(); + tst_finite_set_is_value(); tst_finite_set_is_fully_interp(); }