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

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<expr> 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 {

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