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!
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!