search

viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
8 stars 3 forks source link

Helper binary for extracting axiom dependencies #45

Closed Gopiandcode closed 1 month ago

Gopiandcode commented 1 month ago

Hiya!!! I've been implementing a little binary that uses the SMT parser to determine the dependencies between axioms, in such a way that the results of the axiom profiler can then be imported into other tools, such as boogie.

When run on a boogie file, it produces output such as:

axiom |vipertestsallissuessilicon0335bpl.106:22| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.714:29|
axiom |vipertestsallissuessilicon0335bpl.784:20| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.756:22|
axiom |vipertestsallissuessilicon0335bpl.740:17| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.756:22|
axiom |vipertestsallissuessilicon0335bpl.128:22| depends on 7 axioms:
 - |vipertestsallissuessilicon0335bpl.714:29|
 - |vipertestsallissuessilicon0335bpl.133:22|
 - |vipertestsallissuessilicon0335bpl.106:22|
 - |vipertestsallissuessilicon0335bpl.710:22|
 - |vipertestsallissuessilicon0335bpl.762:29|
 - |vipertestsallissuessilicon0335bpl.124:15|
 - |vipertestsallissuessilicon0335bpl.756:22|
axiom |vipertestsallissuessilicon0335bpl.331:15| depends on 2 axioms:
 - |vipertestsallissuessilicon0335bpl.54:134|
 - |vipertestsallissuessilicon0335bpl.42:22|
axiom |vipertestsallissuessilicon0335bpl.349:15| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.331:15|
axiom |vipertestsallissuessilicon0335bpl.83:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.259:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.269:15| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.88:15|
axiom |vipertestsallissuessilicon0335bpl.335:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.54:134| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.31:15|
axiom |vipertestsallissuessilicon0335bpl.93:15| depends on 4 axioms:
 - |vipertestsallissuessilicon0335bpl.93:15|
 - |vipertestsallissuessilicon0335bpl.83:15|
 - |vipertestsallissuessilicon0335bpl.88:15|
 - |vipertestsallissuessilicon0335bpl.78:22|
axiom |vipertestsallissuessilicon0335bpl.191:19| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.345:15|
axiom |vipertestsallissuessilicon0335bpl.762:29| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.133:22|
axiom |vipertestsallissuessilicon0335bpl.354:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.694:22| depends on 1 axioms:
 - |vipertestsallissuessilicon0335bpl.756:22|
axiom |vipertestsallissuessilicon0335bpl.240:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.756:22| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.133:22| depends on 2 axioms:
 - |vipertestsallissuessilicon0335bpl.52:19|
 - |vipertestsallissuessilicon0335bpl.42:22|
axiom |vipertestsallissuessilicon0335bpl.210:15| depends on 0 axioms:
axiom |vipertestsallissuessilicon0335bpl.244:15| depends on 0 axioms:

I'm just creating a PR here, so that maybe we can discuss implementation of this, and whether it could be implemented more efficiently or using functionalities that are already provided by the codebase.

Happy to chat!!!!

Gopiandcode commented 1 month ago

Closing see #50, thanks @JonasAlaif !!!