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

-Znext-solver caching #128828

Merged
merged 8 commits into from
Aug 14, 2024
Merged

-Znext-solver caching #128828

merged 8 commits into from
Aug 14, 2024

Commits on Aug 12, 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 committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    7b86c98 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 committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    51338ca View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    e87157b View commit details
    Browse the repository at this point in the history
  4. tracing: debug to trace

    lcnr committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    9308401 View commit details
    Browse the repository at this point in the history
  5. move behavior out of shared fn

    lcnr committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    e83eacd View commit details
    Browse the repository at this point in the history
  6. merge impl blocks

    lcnr committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    0c75c08 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 committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    f860873 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2024

  1. Configuration menu
    Copy the full SHA
    0aa17a4 View commit details
    Browse the repository at this point in the history