Observability - count sat/unsat calls to assume() and stateful @precondition()s
#3869
Conversation
Zac-HD
force-pushed
the
observe-predicate-outcomes
branch
2 times, most recently
from
51c4d21
to
c55e0d2
Compare
There was a problem hiding this comment.
cool stuff!
idle comment: distinguishing by line leads to overlapping reports with multiple assume statements on a single line (contrived: assume(a); assume(b), but perhaps more natural is the unidiomatic if assume(a): assume(b), or assume(a) and assume(b)). This is (1) sort of a feature that we report both here, (2) probably rare, and (3) we're only reporting this metadata and not actioning on it. All of which mean I don't think this is a problem at all.
| self._observability_predicates: defaultdict = defaultdict( | ||
| lambda: {"sat": 0, "unsat": 0} | ||
| ) |
There was a problem hiding this comment.
nit: since we're exposing this in observability reports, the full names of "satisfied" and "unsatisfied" make more sense to me from the perspective of a library parsing our observability spec. Bringing this up because it's easy to change now, as opposed to when the format has stabilized a bit (and potentially has stable consumers).
Zac-HD
force-pushed
the
observe-predicate-outcomes
branch
from
43b7269
to
4911c23
Compare
This is part of #3845, which will enable downstream tools to resolve #213 for good. Also includes some extra metadata to fix #3861, since it looked easy.
@hgoldstein95, let me know what you think - will this be useful for Tyche?