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

Reconnect stuck in sequences-18.log #33

Open oskari1 opened 2 months ago

oskari1 commented 2 months ago

If I open the sequences-18.log and then apply the filter "Show quant k!354" then the tool gets stuck in the VisibleInstGraph::reconnect function, see here.

I've tried to limit the maximum number of edges to 1000 or so to inspect the intermediate graph of quant k!354 and saw that it adds a lot of edges, see screenshot below.

image

I'll also link two SVG files to inspect the subgraph of k!354 (dark purple nodes), once without and once with other quants: sequences-18-k!354_2 sequences-18-k!354

My suspicion is that it's not a correctness issue but a performance issue, due to how the equality nodes are represented in the edges of the reconnected graph.

JonasAlaif commented 2 months ago

@oskari1 I agree with your analysis. I expect it's probably an issue with a pattern like so:

   [V]
  /   \
[ ]   [ ]
  \   /
   [ ]
  /   \
[ ]   [ ]
  \   /
   [ ]
  /   \
[ ]   [ ]
  \   /
   [ ]
    |
   [V]

where if only the V nodes are visible, then one gets 2^3 indirect edges (grows exponentially with the hidden length). I think that we should change the reconnect to only consider immediate hidden children/parents, without enumerating all the paths between (such that there would only be 2 indirect edges in the above graph, for the 2 hidden children * 1 hidden parent)