Centralize and document TRACE tags using X-macros #7657

IamYJLee · 2025-05-21T02:24:02Z

Summary

This PR refactors the tracing infrastructure to introduce a structured, hierarchical tagging system using enum class TraceTag. All TRACE, STRACE, SCTRACE, and CTRACE macros have been updated to use enum-based tags instead of string literals, enabling type-safe, consistent trace logging throughout the codebase.

Key Changes

Introduced TraceTag enum and corresponding trace_tag.def file using X-macro format.
Replaced all raw string-based trace tags with TraceTag enum values across the codebase.
Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

Testing

I enabled g_enable_all_trace_tags and compared the .z3-trace output for my existing SMT-LIB expressions before and after the changes. The outputs were identical, indicating functional equivalence.

TODO

Tags are now organized hierarchically: enabling a trace class also enables all associated tags. (Support tag_class-based trace activation #7663)

However, since this change touches a large portion of the codebase, broader testing with more SMT-LIB expressions would be helpful to ensure full coverage and correctness.

- Created trace_tags.def to centralize TRACE tag definitions - Each tag includes a symbolic name and description - Set up enum class TraceTag for type-safe usage in TRACE macros

- Python script parses trace_tags.def and outputs trace_tags.md

NikolajBjorner · 2025-05-21T02:32:38Z

scripts/generate_trace_tag_docs.py

@@ -0,0 +1,35 @@
+# generate_trace_tag_docs.py


something calls this script, e.g., called from doc/mk_api_doc.py to include in api doc package?

Currently, the script is intended to be run manually and is not yet hooked into doc/mk_api_doc.py.
Integration into the API doc pipeline can be considered in the future if that makes sense.

right, first this script has to be pushed :-)

NikolajBjorner · 2025-05-21T02:34:32Z

src/smt/smt_context.cpp

@@ -1702,6 +1702,7 @@ namespace smt {
     */
    bool context::propagate() {
        TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);
+        TRACE_NEW(TraceTag::propagate, tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);


Replacing TRACE by TRACE_NEW and populating trace_tags.def is definitely scriptable.
Based on the original github issue is there any "module" information you wanted to add?

Yes — I’d like to categorize all TRACE tags, starting with:

SMT Internalization: tracking e-graph construction

Congruence Closure Core: focusing on quantifier instantiation

The goal is to build a structured view of all trace points across the solver.

So what is then the plan to achieve this based on C macros?
Have a third column with a class (which is also defined in the enum column) and create a map from class to members such that when the class is traced and TRACE is hit for a member, the trace is invoked?

I’d like to propose the following structure:

Add a class column to trace_tags.def

Keep the current -tr:tag_name option for enabling individual trace tags

Introduce a new -tr_class:tag_class_name option that enables all tags associated with the specified class

If -tr_class:tag_class_name is used, all tags under that class would be activated for tracing.
Let me know if this direction makes sense or if you'd suggest a different approach!

If we proceed with this structure, I’d really appreciate your input on how to conceptually group the existing trace tags into classes.

I believe the simpler and also usable approach would be if you use a single name-space for tag_name and tag-class-name and introduce a hierarchy by making X be of the form
X(tag_name, tag_class_name, "description")
X(tag_class_name, tag_class_name, "description")
So all classes are also tags and we can either take the 1step closure or transitive closure if that turns out to be more useful.
There would be no extra -tr_class option either.

I would merge this PR first and implement tags everywhere so rename TRACE_NEW to TRACE.
Porting all other tags is scriptable by assigning every tag to its own class by default.
It may be an AI query hack to refactor into classes, except the code base is not a friend of small context windows.

NikolajBjorner · 2025-05-21T02:37:38Z

src/util/trace.h

@@ -81,6 +82,7 @@ static inline void finalize_trace() {}
 #define STRACEBODY(CODE) CODE; tout.flush()

 #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })
+#define TRACE_NEW(TAG, CODE) TRACE_CODE(if (is_trace_enabled(to_string(TAG))) { THREAD_LOCK(TRACEBODY(to_string(TAG), CODE)); })


in a separate round, maybe is_trace_enabled uses the enum directly?
Using strings in first round is the way to go.

I've updated the code as suggested — is_trace_enabled accepts the enum directly.

The changes are included in commit cac9782.
Please take a look and let me know if anything else needs refinement!

NikolajBjorner · 2025-05-21T02:39:52Z

src/util/trace.h

@@ -81,6 +82,7 @@ static inline void finalize_trace() {}
 #define STRACEBODY(CODE) CODE; tout.flush()

 #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })
+#define TRACE_NEW(TAG, CODE) TRACE_CODE(if (is_trace_enabled(to_string(TAG))) { THREAD_LOCK(TRACEBODY(to_string(TAG), CODE)); })


Can't the TRACE macro itself pre-pend the class name TraceTag to eliminate common clutter from uses?

I've updated the code as suggested — TRACE_NEW now prepends TraceTag.

The changes are included in commit cac9782.
Please take a look and let me know if anything else needs refinement!

nunoplopes · 2025-05-21T15:47:42Z

Stepping back a little, who needs to know about the tracing mechanism besides the Z3 developers? Probably no one.

Also, a simple grep (e.g.grep -RoP --no-filename 'TRACE\s*\("\K[^"]+' src) is sufficient to gather all trace tags from the code automatically.

NikolajBjorner · 2025-05-21T16:44:04Z

Stepping back a little, who needs to know about the tracing mechanism besides the Z3 developers? Probably no one.

Also, a simple grep (e.g.grep -RoP --no-filename 'TRACE\s*\("\K[^"]+' src) is sufficient to gather all trace tags from the code automatically.

this would benefit also from trace classes which is then more systematic, and also some discipline implied by a def manifest which avoids dealing with silly typos creating two tags instead of one.

IamYJLee · 2025-05-21T23:27:42Z

Stepping back a little, who needs to know about the tracing mechanism besides the Z3 developers? Probably no one.

Also, a simple grep (e.g.grep -RoP --no-filename 'TRACE\s*\("\K[^"]+' src) is sufficient to gather all trace tags from the code automatically.

While it's true that we can extract trace tags using grep, I believe having a structured and documented list — especially with class-based organization — can be meaningful not just for Z3 developers, but also for users or researchers like myself who aim to deeply understand how input conditions are processed internally.

Even though TRACE is primarily a debugging mechanism, exposing it in a more systematic and categorized way could help advanced users trace how specific components like E-matching, internalization, or congruence closure are triggered, which is valuable for learning, debugging, and contributing effectively.

NikolajBjorner · 2025-05-21T23:47:35Z

FWIW, a simple AI prompt created basically this.
Modify/reuse for creating file with X.
Extra credit: sort entries.

Reverted push: Not all cpp versions like musing ##TAG to stringify the identifier in some settings.
Probably fixable.

import os
import re

# Initialize an empty set to store unique tags
unique_tags = set()

# Define the directory to be walked
directory = 'src'

# Walk through all files in the directory recursively
for root, dirs, files in os.walk(directory):
    files = [f for f in files if f.endswith(".cpp") or f.endswith(".h")]
    for file in files:
        file_path = os.path.join(root, file)
        print(file_path)
        
        # Read the content of the file
        with open(file_path, 'r') as f:
            content = f.read()
        
        # Find all occurrences of TRACE("sometag"
        matches = re.findall(r'TRACE\("([^"]+)"', content)
        
        # Replace occurrences of TRACE("sometag" with TRACE(sometag)
        new_content = re.sub(r'TRACE\("([^"]+)"', r'TRACE(\1', content)
        
        # Write the modified content back to the file
        with open(file_path, 'w') as f:
            f.write(new_content)
        
        # Add found tags to the set
        unique_tags.update(matches)

# Print out the accumulated tags in the specified format
for i, tag in enumerate(unique_tags):
    print(f'X({tag}, "{tag}")')

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags - Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag - Implement initial version of trace_tag.def using X(tag, tag_class, description) (class names and descriptions to be refined in a future update)

- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

… mk_api_doc.py

IamYJLee · 2025-05-26T04:45:47Z

@NikolajBjorner
Please review the overall changes in this PR.
trace_tags.def includes all current tags using the X(tag, tag_class, description) format, but class names and descriptions are still placeholders and will be refined later.

NikolajBjorner · 2025-05-26T10:00:14Z

src/util/trace_tags.h

+    #define X(tag, class, desc) if (strncmp(#tag, tag_str, strlen(#tag)) == 0) return TraceTag::tag;
+    #include "trace_tags.def"
+    #undef X
+    return TraceTag::Count;  // 매칭되는 태그가 없는 경우


remove unicode comment

Fixed. PTAL.

NikolajBjorner · 2025-05-26T10:18:44Z

src/util/trace_tags.h

+#include <cstring>
+
+enum class TraceTag {
+#define X(tag, class, desc) tag,


to be safer, avoid identifier "class". I run into compiler incompatibilities a lot.

Fixed. PTAL.

NikolajBjorner · 2025-05-26T10:23:26Z

src/util/trace_tags.h

+inline const TraceTag* get_tags_by_class(TraceTag cls, int& count) {
+    count = count_tags_in_class(cls);
+    static TraceTag* class_tags = nullptr;
+    if (class_tags) delete[] class_tags;


this will cause bug reports with leaks and all memory should go over memory_manager.
We use init/finalize for global memory.
Also, wouldn't an approach where members are added to a single linked list within an array of all tags that gets allocated once do the job?

Or maybe just get rid of this class altogether?

If this is to keep, you can just define an iterator that generates the result on-the-fly.

@NikolajBjorner @nunoplopes
Thanks for the review!
I've created a follow-up issue to track the implementation. (#7663)
I'd appreciate any feedback or suggestions on the proposed implementation direction in that issue!

could you disable or remove this for the current PR?
Then I can merge what there is. With the code below exposed, someone will just start filing a gotcha fuzz bug that there is a memory leak.

Disabled the code per your comment. PTAL.

NikolajBjorner · 2025-05-26T11:32:17Z

Suggestuin is to defer implementing this feature in first pr. Then merging will be quicker. Milestone 1 is using enums.

…ode comment in trace_tags.h.

…ation

IamYJLee · 2025-05-27T01:11:12Z

Suggestuin is to defer implementing this feature in first pr. Then merging will be quicker. Milestone 1 is using enums.

Thanks for the suggestion — I've added a TODO to defer this feature.
I've also created a follow-up issue to track the implementation. (#7663)

…dy (Z3Prover#7663).

NikolajBjorner · 2025-05-28T13:49:33Z

For enabling tag classes, let us use a separate PR after this has gone through all builds.
You already have a method for extracting a static array of trace tags.

// Return all TraceTags as an array
inline const TraceTag* all_trace_tags() {
    static TraceTag tags[] = {
#define X(tag, tag_class, desc) TraceTag::tag,
#include "trace_tags.def"
#undef X
    };
    return tags;
}

Though, these are elements of a consecutive enum type, so I don't think this method does anything that can't be done by playing with values of the enum type itself.

what you could expose is a method that returns a static array where elements of each tag class are linked in a cyclic (or TraceTag::Count terminated) list.

struct tag_class {
      TraceTag next;
};

static tag_class tag_class[] = {
#define X(tag, tc, desc) tag,
#include "trace_tags.def"
#undef  X
};

const tag_class* get_tag_class() {
   static tag_class_init = false; // ignore thread safety assuming TRACE is already under a lock.
   if (!tag_class_init) {
      // code that initializes "next" -            
       tag_class_init = true;
   }
   return tag_class;
}

IamYJLee added 2 commits May 21, 2025 11:18

Introduce X-macro-based trace tag definition

e2f22f1

- Created trace_tags.def to centralize TRACE tag definitions - Each tag includes a symbolic name and description - Set up enum class TraceTag for type-safe usage in TRACE macros

Add script to generate Markdown documentation from trace_tags.def

8917ade

- Python script parses trace_tags.def and outputs trace_tags.md

IamYJLee mentioned this pull request May 21, 2025

Is There a List of Available TRACE Tags by Major Logic (e.g., E-matching)? #7655

Closed

NikolajBjorner reviewed May 21, 2025

View reviewed changes

Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

cac9782

IamYJLee added 4 commits May 26, 2025 10:22

trace: replace all string-based TRACE tags with enum TraceTag

3718996

- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

trace : add cstring header

955111c

trace : Add Markdown documentation generation from trace_tags.def via…

9e4a58c

… mk_api_doc.py

IamYJLee marked this pull request as ready for review May 26, 2025 04:40

NikolajBjorner reviewed May 26, 2025

View reviewed changes

trace : rename macro parameter 'class' to 'tag_class' and remove Unic…

f09dd49

…ode comment in trace_tags.h.

IamYJLee mentioned this pull request May 27, 2025

Support tag_class-based trace activation #7663

Closed

2 tasks

trace : Add TODO comment for future implementation of tag_class activ…

b003937

…ation

IamYJLee force-pushed the enhancement/trace-tag-enum-doc branch from 618b120 to b003937 Compare May 27, 2025 01:09

trace : Disable code related to tag_class until implementation is rea…

0c11a8c

…dy (Z3Prover#7663).

NikolajBjorner merged commit 0a93ff5 into Z3Prover:master May 28, 2025
1 check was pending

Centralize and document TRACE tags using X-macros #7657

Centralize and document TRACE tags using X-macros #7657

Uh oh!

Conversation

IamYJLee commented May 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Key Changes

Testing

TODO

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nunoplopes commented May 21, 2025

Uh oh!

NikolajBjorner commented May 21, 2025

Uh oh!

IamYJLee commented May 21, 2025

Uh oh!

NikolajBjorner commented May 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

IamYJLee commented May 26, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

IamYJLee May 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NikolajBjorner commented May 26, 2025

Uh oh!

IamYJLee commented May 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

NikolajBjorner commented May 28, 2025

Uh oh!

Uh oh!

IamYJLee commented May 21, 2025 •

edited

Loading

NikolajBjorner commented May 21, 2025 •

edited

Loading

IamYJLee May 27, 2025 •

edited

Loading

IamYJLee commented May 27, 2025 •

edited

Loading