Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(verifier): support error recovery with the fast solver #5915

Merged
merged 1 commit into from
Nov 2, 2023

Commits on Nov 2, 2023

  1. feat(verifier): support error recovery with the fast solver

    This PR adds error recovery to the fast solver. It behaves like recovery
    in the old solver (where the first goal/goal group to fail in linear order
    are reported). Unfortunately, we have to do this by re-running the solver
    while we walk back each individual goal.
    
    Note that UseFileNodes should be called *before* any parsing function.
    This already happens in verifier_main, but some tests were calling it
    afterward. The old solver does a bunch of work in PrepareDatabase
    (including handling assertions in file nodes), while the fast solver
    handles everything during parsing. (This avoids an expensive sort.)
    zrlk committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    22964d3 View commit details
    Browse the repository at this point in the history