Trait chalk_solve::solve::Solver

source · 
pub trait Solver<I: Interner>
where
    Self: Debug,
{
    // Required methods
    fn solve(
        &mut self,
        program: &dyn RustIrDatabase<I>,
        goal: &UCanonical<InEnvironment<Goal<I>>>,
    ) -> Option<Solution<I>>;
    fn solve_limited(
        &mut self,
        program: &dyn RustIrDatabase<I>,
        goal: &UCanonical<InEnvironment<Goal<I>>>,
        should_continue: &dyn Fn() -> bool,
    ) -> Option<Solution<I>>;
    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;

    // Provided method
    fn has_unique_solution(
        &mut self,
        program: &dyn RustIrDatabase<I>,
        goal: &UCanonical<InEnvironment<Goal<I>>>,
    ) -> bool { ... }
}
Expand description

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.

Required Methods§

source

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

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.

§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.
source

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

§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 the 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.

Provided Methods§

source

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.

Implementors§