Struct NarrowingSystem 

pub struct NarrowingSystem {
    pub trs: Trs,
    pub var_counter: u32,
}

A narrowing system: computes all possible narrowing steps of a term w.r.t. a TRS.

Narrowing generalises rewriting to terms with variables: a term t narrows to t' if there is a substitution σ and a rule l → r such that t[σ]_p = l[σ] for some non-variable position p, and t' = t[r]_p[σ].

Fields

trs: Trs

The underlying TRS used for narrowing steps.

var_counter: u32

Variable counter for generating fresh variable names.

Implementations

impl NarrowingSystem

pub fn new(trs: Trs) -> Self

Create a new narrowing system wrapping the given TRS.

pub fn narrow_step(&mut self, t: &Term) -> Vec<(Substitution, Term)>

Compute one level of narrowing steps from term t.

Returns a list of (substitution, narrowed_term) pairs.

pub fn basic_narrow( &mut self, t: &Term, depth: usize, ) -> Vec<(Substitution, Term)>

Basic narrowing: perform up to depth levels of narrowing from t.

Returns all reachable (substitution, term) pairs.

pub fn narrowing_unify( &mut self, s: &Term, t: &Term, depth: usize, ) -> Option<Substitution>

Unification via narrowing: tries to unify s and t by narrowing s toward t.

Trait Implementations

impl Clone for NarrowingSystem

fn clone(&self) -> NarrowingSystem

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for NarrowingSystem

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.