add fintie_set_value_factory outline

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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); }

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,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;
+}

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;
+};