Struct ReduceIso 

pub struct ReduceIso {
    pub cap: usize,
}

Apply the full sound reduction (reduce: unit-prop + pure-literal + subsumption to fixpoint), then canonicalize up to CNF-isomorphism — one rung coarser than UnitPropIso. A collapse-measure congruence (the reduction is structural, RUP/reduction-certified, not a relabeling), for quotient_class_count. The ladder: reduce-iso ≤ unitprop-iso ≤ iso ≤ rename ≤ raw = distinct.

Fields

cap: usize

Trait Implementations

impl Congruence for ReduceIso

fn name(&self) -> &str

A short label for reporting ("identity", "Bn", "AGL", "cofactor-iso").

fn canonicalize(&self, clauses: &CanonClauses) -> (CanonClauses, Twist)

The canonical representative of clauses’s class, and the twist mapping clauses onto it (i.e. apply_twist(clauses, twist) == representative).