Trait chalk_engine::slg::ResolventOps
source · pub trait ResolventOps<I: Interner> {
fn resolvent_clause(
&mut self,
ops: &dyn UnificationDatabase<I>,
interner: I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>;
fn apply_answer_subst(
&mut self,
interner: I,
unification_database: &dyn UnificationDatabase<I>,
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: Canonical<AnswerSubst<I>>
) -> Fallible<()>;
}
Required Methods
sourcefn resolvent_clause(
&mut self,
ops: &dyn UnificationDatabase<I>,
interner: I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
fn resolvent_clause(
&mut self,
ops: &dyn UnificationDatabase<I>,
interner: I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
Combines the goal
(instantiated within infer
) with the
given program clause to yield the start of a new strand (a
canonical ex-clause).
The bindings in infer
are unaffected by this operation.
fn apply_answer_subst(
&mut self,
interner: I,
unification_database: &dyn UnificationDatabase<I>,
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: Canonical<AnswerSubst<I>>
) -> Fallible<()>
Implementations on Foreign Types
sourceimpl<I: Interner> ResolventOps<I> for InferenceTable<I>
impl<I: Interner> ResolventOps<I> for InferenceTable<I>
sourcefn resolvent_clause(
&mut self,
db: &dyn UnificationDatabase<I>,
interner: I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
fn resolvent_clause(
&mut self,
db: &dyn UnificationDatabase<I>,
interner: I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
Applies the SLG resolvent algorithm to incorporate a program clause into the main X-clause, producing a new X-clause that must be solved.
Parameters
goal
is the goal G that we are trying to solveclause
is the program clause that may be useful to that end