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

Efficient `RawInstGraph::neighbors_directed` #52

Open oskari1 opened 1 month ago

oskari1 commented 1 month ago

When I implemented a disabler to disable all the Instantiation-nodes, I noticed that the code got stuck trying to find all outgoing enabled successors of a node (this was with heaps-simpler3.log). After a detailed analysis, I noticed that the code got stuck in InstGraph::analyse, more specifically, when calling self.raw.neighbors_directed on the node =2.

I found out that the issue was that in a graph like the one in the screenshot, if all successors of the top-most (white) node =2 are disabled, it will essentially iterate through all paths in RawInstGraph::neighbors_directed. In cases like the one shown in the screenshot, this will result in an exponential number of paths searched through and hence it gets stuck.

image

To fix this, I added an efficient pre-computation to find the next enabled nodes (in either direction) right before the analysis in InstGraph::initialise_default such that subsequently in the analysis, we only have to access this field. To this end, I re-used the TransferInitialiser that iterates through the graph in a DP-manner (in topological order for parents and reverse topological order for children) to compute the next enabled children and parents of a node. The code should be rather self-explanatory.

I have tested the code with assertions to see whether the computed neighbours match with the previous version and it did. One thing I'm not sure of is if InstGraph::initialise_default is the right place to call this function.