From cc8bfd789015d2696072e4306db88de392fd3834 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Oct 2025 13:27:26 +0200
Subject: [PATCH] add fintie_set_value_factory outline

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/finite_set_decl_plugin.h       |  7 +++
 src/model/CMakeLists.txt               |  1 +
 src/model/finite_set_value_factory.cpp | 60 ++++++++++++++++++++++++++
 src/model/finite_set_value_factory.h   | 29 +++++++++++++
 4 files changed, 97 insertions(+)
 create mode 100644 src/model/finite_set_value_factory.cpp
 create mode 100644 src/model/finite_set_value_factory.h

diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h
index 555781261..c17b3f517 100644
--- a/src/ast/finite_set_decl_plugin.h
+++ b/src/ast/finite_set_decl_plugin.h
@@ -111,6 +111,13 @@ public:
     finite_set_recognizers(family_id fid):m_fid(fid) {}
     family_id get_family_id() const { return m_fid; }
     bool is_finite_set(sort* s) const { return is_sort_of(s, m_fid, FINITE_SET_SORT); }
+    bool is_finite_set(sort* s, sort*& elem_sort) const {
+        if (is_finite_set(s)) {
+            elem_sort = to_sort(s->get_parameter(0).get_ast());
+            return true;
+        }
+        return false;
+    }
     bool is_finite_set(expr const* n) const { return is_finite_set(n->get_sort()); }
     bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_EMPTY); }
     bool is_singleton(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SINGLETON); }
diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt
index 9ba93b8e1..436a3c69f 100644
--- a/src/model/CMakeLists.txt
+++ b/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
diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
new file mode 100644
index 000000000..135ad60df
--- /dev/null
+++ b/src/model/finite_set_value_factory.cpp
@@ -0,0 +1,60 @@
+/*++
+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 (m_sort2value_set.find(s, set) && !set->set.empty()) 
+        return *(set->set.begin());
+    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
+
+    auto& [set, values] = 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;
+    }
+    auto& [set_e, values_e] = get_value_set(elem_sort);
+    unsigned next_index = values.size();
+
+    // For finite domains, we may not be able to generate fresh values
+    // if all values have been exhausted
+    // create sets based on next_index
+    // assume that values_e contains all the values of the element sort
+    // and they have already been generated.
+    // Figure out if we are creating two, three, or more element sets
+    // and map next_index into the elements in a uniqe way.
+    return nullptr;
+}
\ No newline at end of file
diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h
new file mode 100644
index 000000000..9ae5f462f
--- /dev/null
+++ b/src/model/finite_set_value_factory.h
@@ -0,0 +1,29 @@
+/*++
+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;
+};
\ No newline at end of file