Struct SearchGraph

pub struct SearchGraph<D: Delegate<Cx = X>, X: Cx = X> {
    mode: SolverMode,
    root_depth: AvailableDepth,
    stack: IndexVec<StackDepth, StackEntry<X>>,
    provisional_cache: HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>,
    _marker: PhantomData<D>,
}

Fields

mode: SolverMode

root_depth: AvailableDepth

stack: IndexVec<StackDepth, StackEntry<X>>

The stack of goals currently being computed.

An element is deeper in the stack if its index is lower.

provisional_cache: HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>

The provisional cache contains entries for already computed goals which still depend on goals higher-up in the stack. We don’t move them to the global cache and track them locally instead. A provisional cache entry is only valid until the result of one of its cycle heads changes.

_marker: PhantomData<D>

Implementations

impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D>

pub fn new(mode: SolverMode, root_depth: usize) -> SearchGraph<D>

pub fn solver_mode(&self) -> SolverMode

fn update_parent_goal( cx: X, stack: &mut IndexVec<StackDepth, StackEntry<X>>, reached_depth: StackDepth, heads: &CycleHeads, encountered_overflow: bool, nested_goals: &NestedGoals<X>, )

Lazily update the stack entry for the parent goal. This behavior is shared between actually evaluating goals and using existing global cache entries to make sure they have the same impact on the remaining evaluation.

pub fn is_empty(&self) -> bool

pub fn debug_current_depth(&self) -> usize

The number of goals currently in the search graph. This should only be used for debugging purposes.

fn step_kind(cx: X, input: X::Input) -> PathKind

fn stack_path_kind( cx: X, stack: &IndexVec<StackDepth, StackEntry<X>>, head: StackDepth, ) -> PathKind

Whether the path from head to the current stack entry is inductive or coinductive.

pub fn with_new_goal( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, evaluate_goal: impl FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result, ) -> X::Result

Probably the most involved method of the whole solver.

Given some goal which is proven via the prove_goal closure, this handles caching, overflow, and coinductive cycles.

fn handle_overflow( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, ) -> X::Result

fn clear_dependent_provisional_results(&mut self)

When reevaluating a goal with a changed provisional result, all provisional cache entry which depend on this goal get invalidated.

fn rebase_provisional_cache_entries( &mut self, cx: X, stack_entry: &StackEntry<X>, mutate_result: impl FnMut(X::Input, X::Result) -> X::Result, )

A necessary optimization to handle complex solver cycles. A provisional cache entry relies on a set of cycle heads and the path towards these heads. When popping a cycle head from the stack after we’ve finished computing it, we can’t be sure that the provisional cache entry is still applicable. We need to keep the cache entries to prevent hangs.

What we therefore do is check whether the cycle kind of all cycles the goal of a provisional cache entry is involved in would stay the same when computing the goal without its cycle head on the stack. For more details, see the relevant rustc-dev-guide chapter.

This can be thought of rotating the sub-tree of this provisional result and changing its entry point while making sure that all paths through this sub-tree stay the same.

In case the popped cycle head failed to reach a fixpoint anything which depends on its provisional result is invalid. Actually discarding provisional cache entries in this case would cause hangs, so we instead change the result of dependant provisional cache entries to also be ambiguous. This causes some undesirable ambiguity for nested goals whose result doesn’t actually depend on this cycle head, but that’s acceptable to me.

fn lookup_provisional_cache( &mut self, cx: X, input: X::Input, ) -> Option<X::Result>

fn candidate_is_applicable( cx: X, stack: &IndexVec<StackDepth, StackEntry<X>>, provisional_cache: &HashMap<X::Input, Vec<ProvisionalCacheEntry<X>>>, nested_goals: &NestedGoals<X>, ) -> bool

Even if there is a global cache entry for a given goal, we need to make sure evaluating this entry would not have ended up depending on either a goal already on the stack or a provisional cache entry.

fn lookup_global_cache_untracked( &self, cx: X, input: X::Input, available_depth: AvailableDepth, ) -> Option<X::Result>

Used when fuzzing the global cache. Accesses the global cache without updating the state of the search graph.

fn lookup_global_cache( &mut self, cx: X, input: X::Input, available_depth: AvailableDepth, ) -> Option<X::Result>

Try to fetch a previously computed result from the global cache, making sure to only do so if it would match the result of reevaluating this goal.

fn check_cycle_on_stack(&mut self, cx: X, input: X::Input) -> Option<X::Result>

fn reached_fixpoint( &mut self, cx: X, stack_entry: &StackEntry<X>, usage_kind: UsageKind, result: X::Result, ) -> bool

Whether we’ve reached a fixpoint when evaluating a cycle head.

fn evaluate_goal_in_task( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, evaluate_goal: impl FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result, ) -> (StackEntry<X>, X::Result)

When we encounter a coinductive cycle, we have to fetch the result of that cycle while we are still computing it. Because of this we continuously recompute the cycle until the result of the previous iteration is equal to the final result, at which point we are done.

fn insert_global_cache( &mut self, cx: X, input: X::Input, final_entry: StackEntry<X>, result: X::Result, dep_node: X::DepNodeIndex, )

When encountering a cycle, both inductive and coinductive, we only move the root into the global cache. We also store all other cycle participants involved.

We must not use the global cache entry of a root goal if a cycle participant is on the stack. This is necessary to prevent unstable results. See the comment of StackEntry::nested_goals for more details.

Layout

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 72 bytes