Add finite_set_value_factory implementation

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

src/model/finite_set_value_factory.cpp

@@ -0,0 +1,62 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    finite_set_value_factory.cpp
+
+Abstract:
+
+    Factory for creating finite set values
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-11-06.
+
+Revision History:
+
+--*/
+#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) {
+}
+
+expr * finite_set_value_factory::get_some_value(sort * s) {
+    // Check if we already have a value for this sort
+    value_set * set = nullptr;
+    if (m_sort2value_set.find(s, set) && !set->empty()) {
+        return *(set->begin());
+    }
+    
+    // For finite sets, we can start with an empty set representation
+    // This is a placeholder - the actual implementation would depend on
+    // how finite sets are represented in the specific theory
+    expr * r = m_model.get_some_value(s);
+    if (r != nullptr) {
+        register_value(r);
+    }
+    return r;
+}
+
+expr * finite_set_value_factory::get_fresh_value(sort * s) {
+    // Get a fresh value for a finite set sort
+    value_set * set = get_value_set(s);
+    
+    // If no values have been generated yet, use get_some_value
+    if (set->empty()) {
+        return get_some_value(s);
+    }
+    
+    // Try to generate a fresh value using the model's get_fresh_value
+    expr * fresh = m_model.get_fresh_value(s);
+    if (fresh != nullptr) {
+        register_value(fresh);
+        return fresh;
+    }
+    
+    // For finite domains, we may not be able to generate fresh values
+    // if all values have been exhausted
+    return nullptr;
+}