Struct WqoInstance 

pub struct WqoInstance {
    pub carrier: Vec<u64>,
    pub le_matrix: Vec<Vec<bool>>,
}

Represents a well-quasi-order (WQO) over a finite carrier.

An encoding of the WQO property: every infinite sequence has a good pair (indices i < j with carrier[i] ≤ carrier[j]).

Fields

carrier: Vec<u64>

The elements of the carrier set (finite approximation).

le_matrix: Vec<Vec<bool>>

The quasi-order as a boolean matrix (le_matrix[i][j] = carrier[i] ≤ carrier[j]).

Implementations

impl WqoInstance

pub fn new(carrier: Vec<u64>, le: impl Fn(u64, u64) -> bool) -> Self

Create a WQO instance from a carrier and a comparator.

pub fn has_good_pair(&self, seq: &[usize]) -> bool

Check if a sequence (given as indices into carrier) has a good pair.

pub fn find_good_pair(&self, seq: &[usize]) -> Option<(usize, usize)>

Return the first good pair in a sequence, if one exists.

pub fn size(&self) -> usize

Number of elements in the carrier.

pub fn is_reflexive(&self) -> bool

Check if the relation is reflexive.

pub fn is_transitive(&self) -> bool

Check if the relation is transitive.