Implement is_value for unions of empty/singleton sets

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/finite_set_decl_plugin.cpp

@@ -187,7 +187,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,7 +127,70 @@ static void tst_finite_set_map_select() {
     ENSURE(selected_set->get_sort() == finite_set_int.get());
 }
 
+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
+    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()));
+}
+
 void tst_finite_set() {
     tst_finite_set_basic();
     tst_finite_set_map_select();
+    tst_finite_set_is_value();
 }