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

Request: tabular data for quantifier instantiations #56

Open jwkai opened 1 week ago

jwkai commented 1 week ago

Hi,

I have been using the Axiom Profiler 2 to troubleshoot performance & completeness issues for a Viper-related project, and could benefit from a feature that would allow viewing tabular data about the instantiations of a quantifier made during a run of Z3.

For example, I may be comparing two axiomatizations and notice that one run produces 500 instances of a particular quantifier, while the other run produces 1500 instances of the same quantifier. This is too much data to explore graphically, so it would be helpful if I could generate tables (either within the tool's UI, or as output files) for these instantiations that contains the costs, number of parents/children, trigger matches, bound and yield terms, etc.

In particular, grouping the instances of a quantifier with "identical" trigger or yield terms could help build some understanding of Z3 runs that involve a lot of potential branching/case-splitting.

Thanks!

JonasAlaif commented 1 week ago

Hey. That's a great suggestion! Unfortunately, I'm away for the next few months and don't have time to work on this, but I would be happy to merge a PR if you want to take a shot at it yourself :)

I don't think it should be too difficult to implement a basic version (no need to change the GUI for now). I would have a look at making a similar file to this file and add an extra command here to run it.