mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

initialize tag class circular linked list

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-28 17:10:23 +01:00
parent a3aee0247a
commit bbb3d5379b
2 changed files with 48 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/util/trace.cpp
View file

@ -57,6 +57,37 @@ void finalize_trace() {
g_enabled_trace_tags = nullptr;
}
const TraceTag* get_tag_classes() {
static bool tag_class_init = false; // ignore thread safety assuming TRACE is already under a lock.
if (!tag_class_init) {
// Arrays to track first and last tag in each class
TraceTag first[static_cast<unsigned>(TraceTag::Count)];
TraceTag last[static_cast<unsigned>(TraceTag::Count)];
for (unsigned i = 0; i < static_cast<unsigned>(TraceTag::Count); ++i)
first[i] = last[i] = TraceTag::Count;
// Link tags in each class
for (unsigned i = 0; i < static_cast<unsigned>(TraceTag::Count); ++i) {
TraceTag tag = static_cast<TraceTag>(i);
TraceTag tag_class = get_trace_tag_class(tag);
unsigned cls = static_cast<unsigned>(tag_class);
if (first[cls] == TraceTag::Count)
first[cls] = tag;
else
tag_classes[static_cast<unsigned>(last[cls])] = tag;
last[cls] = tag;
}
// Close the circular list for each class
for (unsigned cls = 0; cls < static_cast<unsigned>(TraceTag::Count); ++cls)
if (last[cls] != TraceTag::Count && first[cls] != TraceTag::Count)
tag_classes[static_cast<unsigned>(last[cls])] = first[cls];
tag_class_init = true;
}
return tag_classes;
}
void enable_trace(const char * tag) {
get_enabled_trace_tags().insert(tag);

17
src/util/trace_tags.h
View file

@ -29,6 +29,15 @@ inline const char* get_trace_tag_doc(TraceTag tag) {
}
}
inline TraceTag get_trace_tag_class(TraceTag tag) {
switch (tag) {
#define X(tag, tag_class, desc) case TraceTag::tag: return TraceTag::tag_class;
#include "util/trace_tags.def"
#undef X
default: return TraceTag::Count;
}
}
// Return the number of TraceTags
inline constexpr int trace_tag_count() {
return static_cast<int>(TraceTag::Count);
@ -44,6 +53,14 @@ inline constexpr int count_tags_in_class(TraceTag cls) {
return count;
}
static TraceTag tag_classes[] = {
#define X(tag, tc, desc) TraceTag::tag,
#include "util/trace_tags.def"
#undef X
};
// TODO(#7663): Implement tag_class activation of all associated tags
// TODO: Need to consider implementation approach and memory management
// Return all tags that belong to the given class