Trait SolverDelegateEvalExt

pub trait SolverDelegateEvalExt: SolverDelegate {
    // Required methods
    fn evaluate_root_goal(
        &self,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
        generate_proof_tree: GenerateProofTree,
    ) -> (Result<(HasChanged, Certainty), NoSolution>, Option<GoalEvaluation<Self::Interner>>);
    fn root_goal_may_hold_with_depth(
        &self,
        root_depth: usize,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
    ) -> bool;
    fn evaluate_root_goal_raw(
        &self,
        goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>,
        generate_proof_tree: GenerateProofTree,
    ) -> (Result<(NestedNormalizationGoals<Self::Interner>, HasChanged, Certainty), NoSolution>, Option<GoalEvaluation<Self::Interner>>);
}

Required Methods

fn evaluate_root_goal( &self, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, generate_proof_tree: GenerateProofTree, ) -> (Result<(HasChanged, Certainty), NoSolution>, Option<GoalEvaluation<Self::Interner>>)

Evaluates a goal from outside of the trait solver.

Using this while inside of the solver is wrong as it uses a new search graph which would break cycle detection.

fn root_goal_may_hold_with_depth( &self, root_depth: usize, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, ) -> bool

Check whether evaluating goal with a depth of root_depth may succeed. This only returns false if the goal is guaranteed to not hold. In case evaluation overflows and fails with ambiguity this returns true.

This is only intended to be used as a performance optimization in coherence checking.

fn evaluate_root_goal_raw( &self, goal: Goal<Self::Interner, <Self::Interner as Interner>::Predicate>, generate_proof_tree: GenerateProofTree, ) -> (Result<(NestedNormalizationGoals<Self::Interner>, HasChanged, Certainty), NoSolution>, Option<GoalEvaluation<Self::Interner>>)

Object Safety

This trait is not object safe.

Implementors

impl<D, I> SolverDelegateEvalExt for D

where D: SolverDelegate<Interner = I>, I: Interner,