mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-10 16:12:03 +00:00
Code Activity

Remove type variable collection logic from constructors

Browse source 
Removed the logic for collecting type variables from field sorts based on constructors.
This commit is contained in:
Nikolaj Bjorner 2025-10-14 18:11:20 +02:00 • committed by GitHub
parent b7621ae90f
commit c043c325bc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/api_datatype.cpp
View file

@ -323,21 +323,6 @@ extern "C" {
params.push_back(to_sort(parameters[i])); params.push_back(to_sort(parameters[i]));
} }
} }
else {
// Otherwise, collect type variables from field sorts in order of first appearance
obj_hashtable<sort> seen;
for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
for (unsigned j = 0; j < cn->m_sorts.size(); ++j) {
if (cn->m_sorts[j].get() && m.is_type_var(cn->m_sorts[j].get())) {
if (!seen.contains(cn->m_sorts[j].get())) {
params.push_back(cn->m_sorts[j].get());
seen.insert(cn->m_sorts[j].get());
}
}
}
}
}
ptr_vector<constructor_decl> constrs; ptr_vector<constructor_decl> constrs;
for (unsigned i = 0; i < num_constructors; ++i) { for (unsigned i = 0; i < num_constructors; ++i) {