The wiki page at https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries suggests using the Z3 Axiom Profiler; however, the Z3 Axiom Profiler seems to work reliably on Windows only.
How can I easily get the quantifiers that fire the most without the Z3 Axiom Profiler?
Related to Jonathan's reply:
Since this commit: https://github.com/FStarLang/FStar/commit/c4ce03c3709b44600d66b8c2ee55a0e1aa9f75a3
It is sufficient to just run:
z3 smt.qi.profile=true queries-Foo.smt2
since the other F*-specific options are now embedded within the .smt2 file.
This command-line invocation works fine enough for me, relies only on z3's qi.profile feature, and leaves the top offenders at the bottom.
z3 smt.qi.profile=true queries-EverCrypt.Hash.Incremental-33.smt2 |& grep quantifier_instances | sort -t : -k 2 -n
(edited following Nik's answer to remove z3 options now embedded in the smt2 file)
I've been able to use the axiom profiler on Linux via mono but it does indeed take many hours (it appears to hang for a long time during this process, but it does indeed work). Once it has finished its analysis, the interface is quite responsive (although I would recommend staying away from a few of the options under the "File" menu which cause it to crash).
Since I would need to basically leave it overnight for non-trivial traces, I spin it up on a server and use X forwarding via xpra (which allows me to disconnect and reconnect to the server).
If the issue is purely to find queries that are triggering badly, and if fstar works faster with hints, then I also have a useful script fstar-profile-queries that I'd written a few months ago that might be useful. It uses qprofdiff to find offending queries, but does it in a way that is much nicer to work with.
