Struct chalk_solve::Solver

pub struct Solver<I: Interner>(_);

Finds the solution to "goals", or trait queries -- i.e., figures out what sets of types implement which traits. Also, between queries, this struct stores the cached state from previous solver attempts, which can then be re-used later.

Implementations

impl<I: Interner> Solver<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).

Parameters

• program -- defines the program clauses in scope.
  • Important: You must supply the same set of program clauses each time you invoke solve, as otherwise the cached data may be invalid.
• goal the goal to solve

Returns

• None is the goal cannot be proven.
• Some(solution) if we succeeded in finding some answers, although solution may reflect ambiguity and unknowns.

pub fn solve_limited(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>,
    should_continue: impl 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.

Parameters

• program -- defines the program clauses in scope.
  • Important: You must supply the same set of program clauses each time you invoke solve, as otherwise the cached data may be invalid.
• goal the goal to solve
• should_continue if false is returned, the no further solving will be done. A Guidance(Suggested(...)) will be returned a Solution, using any answers that were generated up to that point.

Returns

• None is the goal cannot be proven.
• Some(solution) if we succeeded in finding some answers, although solution may reflect ambiguity and unknowns.

pub fn solve_multiple(
    &mut self,
    program: &dyn RustIrDatabase<I>,
    goal: &UCanonical<InEnvironment<Goal<I>>>,
    f: impl 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).

Parameters

• program -- defines the program clauses in scope.
  • Important: You must supply the same set of program clauses each time you invoke solve, as otherwise the cached data may be invalid.
• goal the goal to solve
• f -- function to proceed solution. New solutions will be generated while function returns true.
  • first argument is solution found
  • second argument is ther next solution present
  • returns true if next solution should be handled

Returns

• true all solutions were processed with the function.
• false the function returned false and solutions were interrupted.

Trait Implementations

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

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

Formats the value using the given formatter.