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.

Sign up for GitHub

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

Jump to bottom

refactor search graph even more! #128115

Closed
wants to merge 7 commits into from
Closed

refactor search graph even more! #128115

wants to merge 7 commits into from

Commits on Jul 23, 2024

  1. do not use the global solver cache for proof trees 

    doing so requires overwriting global cache entries and
generally adds significant complexity to the solver. This is
also only ever done for root goals, so it feels easier to wrap
the `evaluate_canonical_goal` in an ordinary query if
necessary.
    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    e8cb28b View commit details
    Browse the repository at this point in the history

  2. expand fuzzing support 

    this allows us to only sometimes disable the global cache.
    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    49922f7 View commit details
    Browse the repository at this point in the history

  3. simplify match + move debug! call

    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    4955a35 View commit details
    Browse the repository at this point in the history

  4. tracing: debug to trace

    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    61851f9 View commit details
    Browse the repository at this point in the history

  5. move behavior out of shared fn

    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    a7ce1e1 View commit details
    Browse the repository at this point in the history

  6. merge impl blocks

    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    9fbcf25 View commit details
    Browse the repository at this point in the history

  7. split provisional cache and stack lookup 

    this makes it easier to maintain and modify going forward.
There may be a small performance cost as we now need to
access the provisional cache *and* walk through the stack
to detect cycles. However, the provisional cache should be
mostly empty and the stack should only have a few elements
so the performance impact is likely minimal.

Given the complexity of the search graph maintainability
trumps linear performance improvements.
    @lcnr
    lcnr committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    4d64109 View commit details
    Browse the repository at this point in the history