pub trait Delegate {
    type Cx: Cx;
    type ValidationScope;
    type ProofTreeBuilder;

    const ENABLE_PROVISIONAL_CACHE: bool;
    const FIXPOINT_STEP_LIMIT: usize;
    const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize;

    // Required methods
    fn enter_validation_scope(
        cx: Self::Cx,
        input: <Self::Cx as Cx>::Input,
    ) -> Option<Self::ValidationScope>;
    fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool;
    fn recursion_limit(cx: Self::Cx) -> usize;
    fn initial_provisional_result(
        cx: Self::Cx,
        kind: PathKind,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn is_initial_provisional_result(
        cx: Self::Cx,
        kind: PathKind,
        input: <Self::Cx as Cx>::Input,
        result: <Self::Cx as Cx>::Result,
    ) -> bool;
    fn on_stack_overflow(
        cx: Self::Cx,
        inspect: &mut Self::ProofTreeBuilder,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn on_fixpoint_overflow(
        cx: Self::Cx,
        input: <Self::Cx as Cx>::Input,
    ) -> <Self::Cx as Cx>::Result;
    fn is_ambiguous_result(result: <Self::Cx as Cx>::Result) -> bool;
    fn propagate_ambiguity(
        cx: Self::Cx,
        for_input: <Self::Cx as Cx>::Input,
        from_result: <Self::Cx as Cx>::Result,
    ) -> <Self::Cx as Cx>::Result;
    fn step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool;
}

Required Associated Types§

Required Associated Constants§

source

const ENABLE_PROVISIONAL_CACHE: bool

Whether to use the provisional cache. Set to false by a fuzzer when validating the search graph.

source

const FIXPOINT_STEP_LIMIT: usize

source

const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize

Required Methods§

source

fn enter_validation_scope( cx: Self::Cx, input: <Self::Cx as Cx>::Input, ) -> Option<Self::ValidationScope>

Returning Some disables the global cache for the current goal.

The ValidationScope is used when fuzzing the search graph to track for which goals the global cache has been disabled. This is necessary as we may otherwise ignore the global cache entry for some goal G only to later use it, failing to detect a cycle goal and potentially changing the result.

source

fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool

source

fn recursion_limit(cx: Self::Cx) -> usize

source

fn initial_provisional_result( cx: Self::Cx, kind: PathKind, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

source

fn is_initial_provisional_result( cx: Self::Cx, kind: PathKind, input: <Self::Cx as Cx>::Input, result: <Self::Cx as Cx>::Result, ) -> bool

source

fn on_stack_overflow( cx: Self::Cx, inspect: &mut Self::ProofTreeBuilder, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

source

fn on_fixpoint_overflow( cx: Self::Cx, input: <Self::Cx as Cx>::Input, ) -> <Self::Cx as Cx>::Result

source

fn is_ambiguous_result(result: <Self::Cx as Cx>::Result) -> bool

source

fn propagate_ambiguity( cx: Self::Cx, for_input: <Self::Cx as Cx>::Input, from_result: <Self::Cx as Cx>::Result, ) -> <Self::Cx as Cx>::Result

source

fn step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool

Object Safety§

This trait is not object safe.

Implementors§