mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

add a comment, remove }

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-17 14:52:53 +02:00
parent d6908a3d4b
commit af2082a1aa
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/model/finite_set_value_factory.cpp
View file

@ -27,6 +27,9 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
return u.mk_empty(s); return u.mk_empty(s);
} }
/**
* create sets {}, {a}, {b}, {a,b}, {c}, {a,c}, {b,c}, {a,b,c}, {d}, ...
*/
expr * finite_set_value_factory::get_fresh_value(sort * s) { expr * finite_set_value_factory::get_fresh_value(sort * s) {
sort* elem_sort = nullptr; sort* elem_sort = nullptr;
VERIFY(u.is_finite_set(s, elem_sort)); VERIFY(u.is_finite_set(s, elem_sort));
@ -50,7 +53,6 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
auto e = m_model.get_fresh_value(elem_sort); auto e = m_model.get_fresh_value(elem_sort);
if (!e) if (!e)
return nullptr; return nullptr;
register_value(e);
auto r = u.mk_singleton(e); auto r = u.mk_singleton(e);
register_value(r); register_value(r);
return r; return r;
@ -59,9 +61,8 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
// Case 3: Find greatest power of 2 N < values.size() and create union // Case 3: Find greatest power of 2 N < values.size() and create union
// Find the greatest N that is a power of 2 and N < values.size() // Find the greatest N that is a power of 2 and N < values.size()
unsigned N = 1; unsigned N = 1;
while (N * 2 < values.size()) { while (N * 2 < values.size())
N *= 2; N *= 2;
}
auto r = u.mk_union(values.get(values.size() - N), values.get(N)); auto r = u.mk_union(values.get(values.size() - N), values.get(N));
register_value(r); register_value(r);