Struct chalk_engine::solve::SLGSolver
source · pub struct SLGSolver<I: Interner> {
pub(crate) forest: Forest<I>,
pub(crate) max_size: usize,
pub(crate) expected_answers: Option<usize>,
}
Fields§
§forest: Forest<I>
§max_size: usize
§expected_answers: Option<usize>
Implementations§
Trait Implementations§
source§impl<I: Interner> Solver<I> for SLGSolver<I>
impl<I: Interner> Solver<I> for SLGSolver<I>
source§fn solve(
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
) -> Option<Solution<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). Read moresource§fn solve_limited(
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
should_continue: &dyn Fn() -> bool,
) -> 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>>
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
. Read moresource§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
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). Read more§fn has_unique_solution(
&mut self,
program: &dyn RustIrDatabase<I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
) -> bool
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.
Auto Trait Implementations§
impl<I> Freeze for SLGSolver<I>
impl<I> RefUnwindSafe for SLGSolver<I>where
<I as Interner>::InternedCanonicalVarKinds: RefUnwindSafe,
<I as Interner>::InternedGoal: RefUnwindSafe,
<I as Interner>::InternedProgramClauses: RefUnwindSafe,
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedConstraints: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
impl<I> Send for SLGSolver<I>where
<I as Interner>::InternedCanonicalVarKinds: Send,
<I as Interner>::InternedGoal: Send,
<I as Interner>::InternedProgramClauses: Send,
<I as Interner>::InternedSubstitution: Send,
<I as Interner>::InternedConstraints: Send,
<I as Interner>::InternedLifetime: Send,
<I as Interner>::InternedType: Send,
impl<I> Sync for SLGSolver<I>where
<I as Interner>::InternedCanonicalVarKinds: Sync,
<I as Interner>::InternedGoal: Sync,
<I as Interner>::InternedProgramClauses: Sync,
<I as Interner>::InternedSubstitution: Sync,
<I as Interner>::InternedConstraints: Sync,
<I as Interner>::InternedLifetime: Sync,
<I as Interner>::InternedType: Sync,
impl<I> Unpin for SLGSolver<I>where
<I as Interner>::InternedCanonicalVarKinds: Unpin,
<I as Interner>::InternedGoal: Unpin,
<I as Interner>::InternedProgramClauses: Unpin,
<I as Interner>::InternedSubstitution: Unpin,
<I as Interner>::InternedConstraints: Unpin,
<I as Interner>::InternedLifetime: Unpin,
<I as Interner>::InternedType: Unpin,
impl<I> UnwindSafe for SLGSolver<I>where
<I as Interner>::InternedCanonicalVarKinds: UnwindSafe,
<I as Interner>::InternedGoal: UnwindSafe,
<I as Interner>::InternedProgramClauses: UnwindSafe,
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedConstraints: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedType: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more