Struct ConfluenceChecker 

pub struct ConfluenceChecker { /* private fields */ }

Confluence checker for rewrite systems.

Implementations

impl ConfluenceChecker

pub fn new() -> Self

Create a new confluence checker.

pub fn with_max_depth(self, depth: usize) -> Self

Set maximum depth for joinability testing.

pub fn with_max_expr_size(self, size: usize) -> Self

Set maximum expression size.

pub fn check(&mut self, system: &RewriteSystem) -> ConfluenceReport

Check confluence of a rewrite system.

pub fn test_joinability( &mut self, expr1: &TLExpr, expr2: &TLExpr, system: &RewriteSystem, ) -> bool

Test if two expressions are joinable (can be rewritten to a common form).

Uses breadth-first search to explore possible rewrites.

Trait Implementations

impl Default for ConfluenceChecker

fn default() -> Self

Returns the “default value” for a type.