Struct chalk_recursive::recursive::Solver

struct Solver<'me, I: Interner> {
    program: &'me dyn RustIrDatabase<I>,
    context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>,
}

A Solver is the basic context in which you can propose goals for a given program. All questions posed to the solver are in canonical, closed form, so that each question is answered with effectively a “clean slate”. This allows for better caching, and simplifies management of the inference context.

Fields

program: &'me dyn RustIrDatabase<I>

context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>

Implementations

impl<'me, I: Interner> Solver<'me, I>

pub(crate) fn new( context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, program: &'me dyn RustIrDatabase<I>, ) -> Self

Trait Implementations

impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I>

fn solve_goal( &mut self, goal: UCanonicalGoal<I>, minimums: &mut Minimums, should_continue: impl Fn() -> bool + Clone, ) -> Fallible<Solution<I>>

fn interner(&self) -> I

fn db(&self) -> &dyn RustIrDatabase<I>

fn max_size(&self) -> usize