Struct KnuthBendixData 

pub struct KnuthBendixData {
    pub rules: Vec<(String, String)>,
    pub critical_pairs: Vec<(String, String)>,
    pub is_confluent: bool,
    pub order: String,
}

Knuth-Bendix completion data.

Fields

rules: Vec<(String, String)>

Current set of rules.

critical_pairs: Vec<(String, String)>

Critical pairs found.

is_confluent: bool

Whether the system is confluent.

order: String

Termination order description.

Implementations

impl KnuthBendixData

pub fn new(order: &str) -> Self

Creates Knuth-Bendix data.

pub fn add_oriented_rule(&mut self, lhs: &str, rhs: &str)

Adds a rule (already oriented).

pub fn add_critical_pair(&mut self, left: &str, right: &str)

Registers a critical pair.

pub fn mark_confluent(&mut self)

Marks as confluent (after resolving all critical pairs).

pub fn description(&self) -> String

Returns the convergent TRS description.

pub fn num_rules(&self) -> usize

Counts joinable critical pairs.

Trait Implementations

impl Clone for KnuthBendixData

fn clone(&self) -> KnuthBendixData

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for KnuthBendixData

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

Formats the value using the given formatter.