Mentions légales du service

Skip to content

Add faster implementation of LRijkstraCore

BOUR Frederic requested to merge fbour/menhir:faster-reachability into master

This MR tracks the progress integrating the new implementation of LRijkstra into Menhir. The implementation is ready, but the code is still lacking some comments and cleanups.

In this branch, menhir --list-errors defaults to the new algorithm, though the behavior is configurable with the added --list-errors-algorithm flag. It can be set to:

  • fast: use the new algorithm
  • classic: use the previous algorithm
  • validate: run both, check that shortest lengths match, then use fast for producing actual erroneous sentences

The Fix library has a few additions:

  • DataFlow.RunCustomMaps which exposes a lower-level interface than the existing DataFlow solver, crucial for efficiently solving the large problems generated by LRijkstraFast
  • CompactQueue, an alternative to the standard Queue which is a more compact and improved the time and space consumption of DataFlow.RunCustomMaps on large problems
  • Numbering.Typed which implements various type-level tricks to manipulate finite set and vectors indexed by elements from finite sets Once we are done with this MR, I will open a new one to update the Fix library upstream.

Inside Menhir, besides the addition of new algorithms, the main change is that LRijsktra is now parameterized by the reachability algorithm. The logic to chose which algorithm to instantiate LRijkstra with is added to Back

Edited by BOUR Frederic

Merge request reports