Skip to content

Commit

Permalink
Update README with new name
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif authored Feb 13, 2025
1 parent d20a494 commit a1c6f62
Showing 1 changed file with 5 additions and 8 deletions.
13 changes: 5 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,23 +1,20 @@
# Axiom Profiler 2.0
![SmtScope](axiom-profiler-GUI/assets/html/logo_side_small.png?raw=true "SmtScope")

[Runs online](https://viperproject.github.io/axiom-profiler-2/) · [Tutorial](https://github.com/viperproject/axiom-profiler-2/wiki/Tutorial)

A tool for visualising, analysing and understanding quantifier instantiations made via E-matching in a run of an SMT solver (at present, only [Z3](https://github.com/Z3Prover/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](https://github.com/viperproject/axiom-profiler) 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
This tool supersedes the [Axiom Profiler](https://github.com/viperproject/axiom-profiler). S<b><sub><sup>MT</sup></sub></b>S<b><sub><sup>COPE</sup></sub></b> is more stable, ~10x faster and is better a debugging z3 performance issues.

More details of the tool's features can be found in the [README](https://github.com/viperproject/axiom-profiler/blob/master/README.md) 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.
## Obtaining logs from Z3

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.
NOTE: The S<b><sub><sup>MT</sup></sub></b>S<b><sub><sup>COPE</sup></sub></b> 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:

Expand All @@ -28,9 +25,9 @@ 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.
NOTE: if this takes too long, it is possible to run S<b><sub><sup>MT</sup></sub></b>S<b><sub><sup>COPE</sup></sub></b> 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.
Similarly, if you have a log file which takes too long to load into S<b><sub><sup>MT</sup></sub></b>S<b><sub><sup>COPE</sup></sub></b>, hitting Cancel will cause the tool to work with the portion loaded so far.

To correctly parse the log file, we impose a few [restrictions](smt-log-parser/design-docs/restrictions.md) on the smt2 file given to z3.

Expand Down

0 comments on commit a1c6f62

Please sign in to comment.