[experiment] Special handling of root node in AcyclicGraph algorithm#22014
Draft
ppedrot wants to merge 4 commits intorocq-prover:masterfrom
Draft
[experiment] Special handling of root node in AcyclicGraph algorithm#22014ppedrot wants to merge 4 commits intorocq-prover:masterfrom
ppedrot wants to merge 4 commits intorocq-prover:masterfrom
Conversation
We do not have to explicitly register it when building the empty graph.
We handle it specially.
Member
Author
|
@coqbot bench |
Member
Author
|
@SkySkimmer the bench died with a weird error in an unrelated script... Any idea what went wrong? |
Member
Author
|
Let's retry: @coqbot bench |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The most expensive kind of level constraint in the current algorithm is of the form "enforce u ≤ Set". Indeed the forward pass has to crawl basically the whole graph starting from Set, as all levels are above Set. This is the worst case for the complexity of our variant of of the Tarjan algorithm, which expects the graph to be sparse. Unfortunately, in practice such constraints seem to be commonplace in universe-polymorphic code.
To work around this issue, in this PR we try to handle Set in a special way by not storing it in the graph as a normal node. Instead we assume "Set ≤ u" implicitly everywhere, and we only keep a set of constraints "Set < u". We still have to perform a kind of forward pass to merge a level with Set, but we do so hopefully efficiently by leveraging the topological order maintained by the algorithm. We add in particular a map to quickly access nodes by their topological index.