mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 13:56:03 +00:00
Code Activity

Update copyright and add TODOs in finite_set_value_factory

Browse source 
Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.
This commit is contained in:
Nikolaj Bjorner 2025-10-15 21:33:02 +02:00 • committed by GitHub
parent 605ee863e1
commit 698e71283c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/model/finite_set_value_factory.cpp
View file

@ -1,5 +1,5 @@
/*++ /*++
Copyright (c) 2006 Microsoft Corporation Copyright (c) 2025 Microsoft Corporation
Module Name: Module Name:
@ -9,12 +9,6 @@ Abstract:
Factory for creating finite set values 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/finite_set_value_factory.h"
#include "model/model_core.h" #include "model/model_core.h"
@ -26,18 +20,12 @@ finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fi
expr * finite_set_value_factory::get_some_value(sort * s) { expr * finite_set_value_factory::get_some_value(sort * s) {
// Check if we already have a value for this sort // Check if we already have a value for this sort
value_set * set = nullptr; value_set * set = nullptr;
if (m_sort2value_set.find(s, set) && !set->empty()) { if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin()); return *(set->begin());
}
// TODO add handling here
// For finite sets, we can start with an empty set representation
// This is a placeholder - the actual implementation would depend on return nullptr;
// 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) { expr * finite_set_value_factory::get_fresh_value(sort * s) {
@ -45,17 +33,13 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
value_set * set = get_value_set(s); value_set * set = get_value_set(s);
// If no values have been generated yet, use get_some_value // If no values have been generated yet, use get_some_value
if (set->empty()) { if (set->empty())
return get_some_value(s); return get_some_value(s);
}
// TODO add handling here: create a fresh value for the element sort.
// Try to generate a fresh value using the model's get_fresh_value // if it fails, then traverse set to add a new value to a set such that
expr * fresh = m_model.get_fresh_value(s); // the new set hasn't been created before.
if (fresh != nullptr) {
register_value(fresh);
return fresh;
}
// For finite domains, we may not be able to generate fresh values // For finite domains, we may not be able to generate fresh values
// if all values have been exhausted // if all values have been exhausted
return nullptr; return nullptr;