epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Improve performance of DiGraph #204

Closed mario-bucev closed 1 year ago

mario-bucev commented 1 year ago

Copied/pasted comment from Graphs.scala: Implementation note: inEdgesMap and outEdgesMap can be derived from N and E. However, since inEdges and outEdges are often used with updated copies of the graph, it is interesting performance-wise to have these maps as fields and "update" them alongside "update" operation such as +, ++ etc.

samarion commented 1 year ago

Are you sure this improves performance in the Inox/Stainless end-to-end flows?

Usually we construct the entire graph before we start looking into transitive edges, so computing the fields for intermediate graphs might actually be slower.

mario-bucev commented 1 year ago

It does for large programs. For instance loading verification/valid is significantly faster in the preprocessing step. Of course this may have a negative impact for smaller programs but it should be negligible.