trace : Classify tag_names unique to smt_internalize.cpp#7713
Conversation
|
@microsoft-github-policy-service agree company="NSHC" |
| X(berlekamp_matrix, berlekamp_matrix, "berlekamp matrix") | ||
| X(pob, pob, "pob") | ||
| X(theory_str, theory_str, "theory str") | ||
| X(smt_internalize, smt_internalize, "smt internalize") |
There was a problem hiding this comment.
we should keep these alphabetical.
Otherwise, small updates become chaotic.
The python script that generates trace_tags_def can sort.
There was a problem hiding this comment.
maybe change the convention for X to use the group first, then the tag.
Then alphabetical order is stable relative to group.
There was a problem hiding this comment.
what do you think about sorting them like this:
X(A_tag_class, A_tag_class ...)
X(A_tag_name, A_tag_class ...)
X(B_tag_name, A_tag_class ...)
X(B_tag_class, B_tag_class ...)
X(A_tag_name, B_tag_class ...)
X(B_tag_name, B_tag_class ...)
There was a problem hiding this comment.
Here is what i described:
X(A_tag_class, A_tag_class ...)
X(A_tag_class, A1_tag_name ...)
X(A_tag_class, A2_tag_name ...)
X(B_tag_class, B_tag_class ...)
X(B_tag_class, B1_tag_name ...)
X(B_tag_cass, B2_tag_name ...)
It could be a group but then having too many specialized trace tags doesnt produce really clear value to me. That said, sometimes when debugging conflict resolution I end up shuffling tag names. |
2 participants
I’ve grouped the
tag_namesused only insmt_internalize.cppunder thesmt_internalizetag_class.For
tag_namesthat appear across multiple files such assmt_context.cpp,smt_clause_proof.cpp, andsmt_internalize.cpp, further classification is needed.I’d appreciate your advice on whether we should consider renaming
tag_namesthat are used in multiple places.For example,
z3/src/smt/smt_internalizer.cpp
Line 620 in 8de80e6
z3/src/smt/smt_clause_proof.cpp
Line 240 in 8de80e6
z3/src/smt/smt_consequences.cpp
Line 55 in 8de80e6
z3/src/smt/smt_context.cpp
Line 2433 in 8de80e6