Struct UnitPropIso 

pub struct UnitPropIso {
    pub cap: usize,
}

Unit-propagate to fixpoint, then canonicalize up to CNF-isomorphism — strictly coarser than CofactorIso (cofactors that reduce to isomorphic residuals after propagation merge, and all unit-refutable cofactors collapse into one). A collapse-measure congruence only: unit propagation is a structural reduction, not a relabeling, so the returned twist is the iso-twist of the reduced form — valid for quotient_class_count (which uses only the canonical key), not for the twist-certificate quotient_dag (a propagation merge is certified by RUP instead).

Fields

cap: usize

Trait Implementations

impl Congruence for UnitPropIso

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).