Struct TermRewriteSystem 

pub struct TermRewriteSystem {
    pub rules: Vec<RewriteRule>,
    pub signature: Signature,
}

A term rewriting system: a collection of rewrite rules.

Fields

rules: Vec<RewriteRule>

signature: Signature

Implementations

impl TermRewriteSystem

pub fn new(sig: Signature) -> Self

Create an empty TRS.

pub fn add_rule(&mut self, rule: RewriteRule)

Add a rewrite rule.

pub fn rewrite_step(&self, t: &Term) -> Option<Term>

Perform one outermost-innermost rewrite step on t. Returns Some(result) if any rule applies; None if already normal.

pub fn normalize(&self, t: &Term, max_steps: usize) -> Term

Reduce t to normal form (up to a step limit to avoid infinite loops).

pub fn find_critical_pairs(&self) -> Vec<(Term, Term)>

Check for local confluence by testing critical pairs (simplified). Returns a list of (t1, t2) pairs where t1 and t2 are the two reducts of a critical overlap between rules i and j.