Struct chalk_engine::solve::SLGSolver

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

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>

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

Formats the value using the given formatter.

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

pub 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).

pub 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.

pub 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).

pub 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.