Add finite_set_value_factory for creating finite set values in model generation (#7981)

* Initial plan

* Add finite_set_value_factory implementation

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

* Remove unused dl_decl_plugin variable and include

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

* Update copyright and add TODOs in finite_set_value_factory

Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.

* Update copyright information in finite_set_value_factory.h

Updated copyright year from 2006 to 2025.

* Implement finite_set_value_factory using array_util to create singleton sets

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

* Simplify empty set creation in finite_set_value_factory

Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.

* Change family ID for finite_set_value_factory

* Fix build error by restoring array_decl_plugin include and implementation

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

* Update finite_set_value_factory.h

* Add SASSERT for finite set check in factory

Added assertion to check if the sort is a finite set.

* Rename member variable from m_util to u

* Refactor finite_set_value_factory for value handling

* Use register_value instead of direct set insertion

Replaced direct insertion into set with register_value calls.

* Update finite_set_value_factory.cpp

---------

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/model/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(model
   SOURCES
     array_factory.cpp
     datatype_factory.cpp
+    finite_set_value_factory.cpp
     func_interp.cpp
     model2expr.cpp
     model_core.cpp

src/model/finite_set_value_factory.cpp

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_set_value_factory.cpp
+
+Abstract:
+
+    Factory for creating finite set values
+
+--*/
+#include "model/finite_set_value_factory.h"
+#include "model/model_core.h"
+
+finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
+    struct_factory(m, fid, md),
+    u(m) {
+}
+
+expr * finite_set_value_factory::get_some_value(sort * s) {
+    // Check if we already have a value for this sort
+    value_set * set = nullptr;
+    SASSERT(u.is_finite_set(s));
+    #if 0
+    if (m_sort2value_set.find(s, set) && !set->empty()) 
+        return *(set->begin());
+    #endif
+    return u.mk_empty(s);
+}
+
+expr * finite_set_value_factory::get_fresh_value(sort * s) {
+    sort* elem_sort = nullptr;
+    VERIFY(u.is_finite_set(s, elem_sort));
+    // Get a fresh value for a finite set sort
+
+    return nullptr;
+    #if 0
+    value_set * set = get_value_set(s);
+    
+    // If no values have been generated yet, use get_some_value
+    if (set->empty()) {
+        auto r = u.mk_empty(s);
+        register_value(r);
+        return r;
+    }
+    auto e = md.get_fresh_value(elem_sort);
+    if (e) {
+        auto r = u.mk_singleton(e);
+        register_value(r);
+        return r;
+    }
+
+    // For finite domains, we may not be able to generate fresh values
+    // if all values have been exhausted
+    return nullptr;
+    #endif
+}

src/model/finite_set_value_factory.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_set_value_factory.h
+
+Abstract:
+
+    Factory for creating finite set values
+
+--*/
+#pragma once
+
+#include "model/struct_factory.h"
+#include "ast/finite_set_decl_plugin.h"
+
+/**
+   \brief Factory for finite set values.
+*/
+class finite_set_value_factory : public struct_factory {
+    finite_set_util u;
+public:
+    finite_set_value_factory(ast_manager & m, family_id fid, model_core & md);
+    
+    expr * get_some_value(sort * s) override;
+    
+    expr * get_fresh_value(sort * s) override;
+};
+

src/model/model.cpp

@@ -40,6 +40,7 @@ Revision History:
 #include "model/numeral_factory.h"
 #include "model/fpa_factory.h"
 #include "model/char_factory.h"
+#include "model/finite_set_value_factory.h"
 
 
 model::model(ast_manager & m):
@@ -111,6 +112,7 @@ value_factory* model::get_factory(sort* s) {
         m_factories.register_plugin(alloc(arith_factory, m));
         m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
         m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id()));
+        m_factories.register_plugin(alloc(finite_set_value_factory, m, m.mk_family_id("finite_set"), *this));
         //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id());
     }
     family_id fid = s->get_family_id();