Analyzing the trace file generated by z3 #6874
-
|
Hi, I am trying to analyze performance of quantifier instantiation by parsing the trace file generated by z3. However, the z3tracer tool only supports z3 4.8.9. I am wondering whether there is a reference doc for parsing the generated trace file. Thanks! |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
The legacy tools is AxiomProfiler, https://github.com/viperproject/axiom-profiler. You could also try custom scripts around the proof logs: You could also log quantifier instantiations by setting a configuration: |
Beta Was this translation helpful? Give feedback.
The legacy tools is AxiomProfiler, https://github.com/viperproject/axiom-profiler.
Maybe @alexanderjsummers has updates.
You could also try custom scripts around the proof logs:
https://microsoft.github.io/z3guide/programming/Proof%20Logs
You could also log quantifier instantiations by setting a configuration:
z3 solver.instantiations2console=true file.smt2