From f7a8260356d6e1275fbe4348250632b17d6768b5 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 15 Oct 2025 19:38:59 +0000
Subject: [PATCH] Implement finite_set is_fully_interp to check element sort

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/finite_set_decl_plugin.cpp |  7 ++++++-
 src/test/finite_set.cpp            | 33 ++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 002887905..5cd1fd035 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -183,7 +183,12 @@ expr * finite_set_decl_plugin::get_some_value(sort * s) {
 }
 
 bool finite_set_decl_plugin::is_fully_interp(sort * s) const {
-    return false;
+    if (!is_finite_set(s))
+        return false;
+    sort* element_sort = get_element_sort(s);
+    if (!element_sort)
+        return false;
+    return m_manager->is_fully_interp(element_sort);
 }
 
 bool finite_set_decl_plugin::is_value(app * e) const {
diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp
index ca6ae35bb..7c62e52c0 100644
--- a/src/test/finite_set.cpp
+++ b/src/test/finite_set.cpp
@@ -127,7 +127,40 @@ static void tst_finite_set_map_select() {
     ENSURE(selected_set->get_sort() == finite_set_int.get());
 }
 
+static void tst_finite_set_is_fully_interp() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    
+    finite_set_util fsets(m);
+    arith_util arith(m);
+    
+    // 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);
+    
+    ENSURE(m.is_fully_interp(int_sort));
+    ENSURE(m.is_fully_interp(finite_set_int));
+    
+    // Test with Bool sort (should be fully interpreted)
+    sort_ref bool_sort(m.mk_bool_sort(), m);
+    parameter bool_param(bool_sort.get());
+    sort_ref finite_set_bool(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &bool_param), m);
+    
+    ENSURE(m.is_fully_interp(bool_sort));
+    ENSURE(m.is_fully_interp(finite_set_bool));
+    
+    // Test with uninterpreted sort (should not be fully interpreted)
+    sort_ref uninterp_sort(m.mk_uninterpreted_sort(symbol("U")), m);
+    parameter uninterp_param(uninterp_sort.get());
+    sort_ref finite_set_uninterp(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &uninterp_param), m);
+    
+    ENSURE(!m.is_fully_interp(uninterp_sort));
+    ENSURE(!m.is_fully_interp(finite_set_uninterp));
+}
+
 void tst_finite_set() {
     tst_finite_set_basic();
     tst_finite_set_map_select();
+    tst_finite_set_is_fully_interp();
 }