Struct SearchGraph 

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

Fields

root_depth: AvailableDepth

stack: Stack<X>

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(root_depth: usize) -> SearchGraph<D>

fn update_parent_goal( stack: &mut Stack<X>, step_kind_from_parent: PathKind, required_depth_for_nested: usize, heads: impl Iterator<Item = (StackDepth, CycleHead)>, encountered_overflow: bool, context: UpdateParentGoalCtxt<'_, 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 cycle_path_kind( stack: &Stack<X>, step_kind_to_head: PathKind, head: StackDepth, ) -> PathKind

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

The step_kind_to_head is used to add a single additional path segment to the path on the stack which completes the cycle. This given an inductive step AB which then cycles coinductively with A, we need to treat this cycle as coinductive.

pub fn enter_single_candidate(&mut self)

pub fn finish_single_candidate(&mut self) -> CandidateHeadUsages

pub fn ignore_candidate_head_usages(&mut self, usages: CandidateHeadUsages)

pub fn evaluate_root_goal_for_proof_tree( cx: X, root_depth: usize, input: X::Input, inspect: &mut D::ProofTreeBuilder, ) -> X::Result

pub fn evaluate_goal( &mut self, cx: X, input: X::Input, step_kind_from_parent: PathKind, inspect: &mut D::ProofTreeBuilder, ) -> X::Result

Probably the most involved method of the whole solver.

While goals get computed via D::compute_goal, this function handles caching, overflow, and cycles.

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

fn clear_dependent_provisional_results_for_rerun(&mut self)

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

Note that we keep provisional cache entries which accessed this goal as a cycle head, but don’t depend on its value.

fn rebase_provisional_cache_entries( &mut self, 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.

This can be thought of as pretending to reevaluate the popped head as nested goals of this provisional result. For this to be correct, all cycles encountered while we’d reevaluate the cycle head as a nested goal must keep the same cycle kind. rustc-dev-guide chapter.

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, input: X::Input, step_kind_from_parent: PathKind, ) -> Option<X::Result>

fn candidate_is_applicable( &self, step_kind_from_parent: PathKind, 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, step_kind_from_parent: PathKind, 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, step_kind_from_parent: PathKind, 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, step_kind_from_parent: PathKind, ) -> Option<X::Result>

fn reached_fixpoint( &mut self, cx: X, stack_entry: &StackEntry<X>, usages: HeadUsages, 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, ) -> EvaluationResult<X>

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, evaluation_result: EvaluationResult<X>, 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: 64 bytes