Trait chalk_engine::context::TruncateOps

pub trait TruncateOps<C: Context> {
    fn goal_needs_truncation(
        &mut self, 
        interner: &C::Interner, 
        subgoal: &C::GoalInEnvironment
    ) -> bool;
    fn answer_needs_truncation(
        &mut self, 
        interner: &C::Interner, 
        subst: &C::Substitution
    ) -> bool;
}

"Truncation" (called "abstraction" in the papers referenced below) refers to the act of modifying a goal or answer that has become too large in order to guarantee termination.

Currently we don't perform truncation (but it might me readded later).

Citations:

• Terminating Evaluation of Logic Programs with Finite Three-Valued Models
  • Riguzzi and Swift; ACM Transactions on Computational Logic 2013
• Radial Restraint
  • Grosof and Swift; 2013

Required methods

fn goal_needs_truncation(
    &mut self,
    interner: &C::Interner,
    subgoal: &C::GoalInEnvironment
) -> bool

Check if subgoal is too large

fn answer_needs_truncation(
    &mut self,
    interner: &C::Interner,
    subst: &C::Substitution
) -> bool

Check if subst is too large

Loading content...

Implementors

Loading content...