Struct KnuthBendixCompletion 

pub struct KnuthBendixCompletion {
    pub trs: TermRewriteSystem,
    pub pending: Vec<(Term, Term)>,
    pub max_steps: usize,
}

A simple Knuth-Bendix completion procedure.

Given a set of equations, attempts to produce a confluent and terminating TRS.

Fields

trs: TermRewriteSystem

pending: Vec<(Term, Term)>

Pending equations (lhs, rhs) to orient.

max_steps: usize

Maximum completion steps.

Implementations

impl KnuthBendixCompletion

pub fn new( sig: Signature, equations: Vec<(Term, Term)>, max_steps: usize, ) -> Self

Create a new KB completion instance from initial equations.

pub fn run(&mut self) -> bool

Run the completion procedure. Returns true if completion succeeded (no unorientable equations remain).

pub fn result_rules(&self) -> &[RewriteRule]

Return the resulting confluent TRS rules.