Struct DependencyPairGraph 

pub struct DependencyPairGraph {
    pub pairs: Vec<DependencyPairNode>,
    pub edges: Vec<HashSet<usize>>,
}

A dependency pair graph for a TRS — used to prove termination.

In the dependency pair method a “dependency pair” is derived from each rule f(l) → C[g(r)] where g is a defined symbol. Termination is equivalent to the non-existence of infinite chains in the dependency pair graph.

Fields

pairs: Vec<DependencyPairNode>

The dependency pairs (nodes of the graph).

edges: Vec<HashSet<usize>>

Edges: edges[i] is the set of indices j such that pair i may precede pair j.

Implementations

impl DependencyPairGraph

pub fn new() -> Self

Create an empty dependency pair graph.

pub fn add_pair( &mut self, lhs_root: impl Into<String>, rhs_root: impl Into<String>, ) -> usize

Add a dependency pair (lhs_root, rhs_root) and return its index.

pub fn add_edge(&mut self, from: usize, to: usize)

Add an edge from pair from to pair to.

pub fn sccs(&self) -> Vec<Vec<usize>>

Find all strongly connected components (SCCs) via a simple iterative DFS.

Returns a list of SCCs, each represented as a list of pair indices.

pub fn all_sccs_trivial(&self) -> bool

Returns true if all SCCs are trivial (size ≤ 1 and no self-loops).

A TRS is terminating iff its dependency pair graph has no infinite chains, which holds when all non-trivial SCCs can be removed by a reduction pair.

pub fn from_trs(trs: &Trs) -> Self

Derive dependency pairs from a Trs by inspecting rule root symbols.

Trait Implementations

impl Clone for DependencyPairGraph

fn clone(&self) -> DependencyPairGraph

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DependencyPairGraph

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

Formats the value using the given formatter.

impl Default for DependencyPairGraph

fn default() -> DependencyPairGraph

Returns the “default value” for a type.