A tool for visualising, analysing and understanding quantifier instantiations made via E-matching in a run of an SMT solver (at present, only Z3 has been modified to provide the necessary log files). The tool takes a log file (which can be generated by Z3 by passing additional command-line options; see below) and presents information visually, primarily using a graph representation of the quantifier instantiations made and their causal connections. This graph can be filtered and explored in a variety of ways, and detailed explanations of individual quantifier instantiations are assembled and displayed. A range of customisations are available for aiding the presentation and understanding of this information, including explanations of equalities used to justify a quantifier instantiation.
This tool reimplements Axiom Profiler 1.0 and aims to eventually add new features while still delivering on 3 improvements:
- OS agnostic (runs in the browser)
- Better performance (about 10x faster parsing)
- Does not crash
More details of the tool's features can be found in the README of the old tool.
Note: not all features of the old tool are currently implemented: you may still find it useful to use the old tool.
NOTE: The Axiom Profiler requires at least version 4.8.5 of z3. To build the latest version of z3 from source follow the instructions at https://github.com/Z3Prover/z3.
Run Z3 with two extra command-line options:
z3 trace=true proof=true ./input.smt2
This will produce a log file called ./z3.log.
If you want to specify the target filename, you can pass a third option:
z3 trace=true proof=true trace-file-name=foo.log ./input.smt2
NOTE: if this takes too long, it is possible to run the Axiom Profiler with a prefix of a valid log file - you could potentially kill the z3 process and obtain the corresponding partial log. Some users (especially on Windows) have reported that killing z3 can cause a lot of the file contents to disappear; if you observe this problem, it's recommended to copy the log file before killing the process.
Similarly, if you have a log file which takes too long to load into the Axiom Profiler, hitting Cancel will cause the tool to work with the portion loaded so far.
To obtain a Z3 log with Boogie, use e.g:
boogie /vcsCores:1 /z3opt:trace=true /z3opt:PROOF=true ./file.bpl
Note that you may also want to pass the /vcsCores:1 option to disable concurrency (since otherwise many Z3 instances may write to the same file)
To obtain a Z3 log with the Viper symbolic execution verifier (Silicon), use e.g:
silicon --numberOfParallelVerifiers 1 --z3Args "trace=true proof=true" ./file.vpr
If it complains about an unrecognized argument, try escaping the double-quotes. E.g.:
silicon --numberOfParallelVerifiers 1 --z3Args '"trace=true proof=true"' ./file.vpr
on Unix-like systems or:
silicon --numberOfParallelVerifiers 1 --z3Args """trace=true proof=true""" ./file.vpr
in Windows command prompt.
To obtain a Z3 log with the Viper verification condition generation verifier (Carbon), use e.g:
carbon --print ./file.bpl ./file.vpr
boogie /vcsCores:1 /z3opt:trace=true /z3opt:proof=true ./file.bpl
In all cases, the Z3 log should be stored in ./z3.log (this can also be altered by correspondingly passing z3 the trace-file-name option described above)
See these instructions in Dafny's wiki: Investigating slow verification performance.
See these instructions in FStar's wiki: Profiling Z3 queries.