Struct rustc_type_ir::search_graph::SearchGraph

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

Fields

mode: SolverMode

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, ProvisionalCacheEntry<X>>

_marker: PhantomData<D>

Implementations

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

pub(super) fn check_invariants(&self)

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

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

pub fn solver_mode(&self) -> SolverMode

fn update_parent_goal( &mut self, reached_depth: StackDepth, encountered_overflow: bool, )

pub fn is_empty(&self) -> bool

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

fn tag_cycle_participants( stack: &mut IndexVec<StackDepth, StackEntry<X>>, usage_kind: Option<UsageKind>, head: StackDepth, )

fn clear_dependent_provisional_results( provisional_cache: &mut HashMap<X::Input, ProvisionalCacheEntry<X>>, head: StackDepth, )

pub fn with_new_goal( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, prove_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 lookup_global_cache( &mut self, cx: X, input: X::Input, available_depth: AvailableDepth, inspect: &mut D::ProofTreeBuilder, ) -> 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.

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

fn fixpoint_step_in_task<F>( &mut self, cx: X, input: X::Input, inspect: &mut D::ProofTreeBuilder, prove_goal: &mut F, ) -> StepResult<X>

where F: FnMut(&mut Self, &mut D::ProofTreeBuilder) -> 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.

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