Enum AffineOutcome 

pub enum AffineOutcome {
    Refuted(Option<Vec<Vec<Lit>>>),
    Forced(Vec<Vec<Lit>>),
    Unchanged,
}

The outcome of the affine break.

Variants

Refuted(Option<Vec<Vec<Lit>>>)

The recovered linear system is inconsistent (0 = 1) ⇒ the formula is UNSAT, by an obstruction no clause permutation can express. The payload is the certificate: the GF(2) linear-dependency refutation compiled to clausal DRAT resolvents through the crate::xor_drat bridge (a sequence of RUP lemmas that drat-trim / crate::rup::check_refutation verifies against the original CNF), or None when the resolution expansion exceeds its budget — the verdict still stands on the native algebraic certificate, exactly as the Route::Parity cut does.

Forced(Vec<Vec<Lit>>)

Consistent, but Gauss elimination forced linear consequences — units and/or equivalences not stated by any single clause. The carried clauses are sound to conjoin (implied by the formula) and are genuinely new (none already present), so adding them strictly strengthens it for search.

Unchanged

No linear structure, or nothing new derivable.

Trait Implementations

impl Clone for AffineOutcome

fn clone(&self) -> AffineOutcome

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AffineOutcome

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

Formats the value using the given formatter.

impl PartialEq for AffineOutcome

fn eq(&self, other: &AffineOutcome) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for AffineOutcome

impl StructuralPartialEq for AffineOutcome