Struct chalk_engine::solve::SLGSolver

pub struct SLGSolver<I: Interner> { /* private fields */ }

Implementations

impl<I: Interner> SLGSolver<I>

pub fn new(max_size: usize, expected_answers: Option<usize>) -> Self

Trait Implementations

impl<I: Interner> Debug for SLGSolver<I>

fn fmt(&self, fmt: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<I: Interner> Solver<I> for SLGSolver<I>

fn solve(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>
) -> Option<Solution<I>>

Attempts to solve the given goal, which must be in canonical form. Returns a unique solution (if one exists). This will do only as much work towards goal as it has to (and that work is cached for future attempts).

fn solve_limited(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>,
    should_continue: &dyn Fn() -> bool
) -> Option<Solution<I>>

Attempts to solve the given goal, which must be in canonical form. Returns a unique solution (if one exists). This will do only as much work towards goal as it has to (and that work is cached for future attempts). In addition, the solving of the goal can be limited by returning false from should_continue.

fn solve_multiple(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>,
    f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool
) -> bool

Attempts to solve the given goal, which must be in canonical form. Provides multiple solutions to function f. This will do only as much work towards goal as it has to (and that work is cached for future attempts).

fn has_unique_solution(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>
) -> bool

A convenience method for when one doesn’t need the actual solution, only whether or not one exists.