Enum EmitError 

pub enum EmitError {
    StepNotRup {
        index: usize,
    },
    EmptyClauseNotRup,
    RequiresSubstitutionRedundancy {
        index: usize,
    },
    PrInRupOnlyFormat {
        index: usize,
    },
    SizeCapExceeded,
}

Why a proof could not be emitted in a requested standard format.

Variants

StepNotRup

A step’s added clause is not RUP w.r.t. the database at that point — the refutation does not actually check, so there is nothing sound to emit.

Fields

index: usize

EmptyClauseNotRup

The refutation does not end by deriving the empty clause (it is not a refutation).

RequiresSubstitutionRedundancy

A Pr step carries a substitution witness that is irreducibly SR — it cannot be expressed as a standard PR assignment witness, so no dpr-trim-checkable line exists.

Fields

index: usize

PrInRupOnlyFormat

A Pr step appeared where the chosen format (DRAT/LRAT) admits only RUP additions.

Fields

index: usize

SizeCapExceeded

A streaming emitter’s sink refused a write — it hit the caller’s byte cap (see SizeSink). Surfaced only when measuring a proof’s size against a bound; the String-returning emitters, whose sink never fails, cannot produce it.

Trait Implementations

impl Clone for EmitError

fn clone(&self) -> EmitError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EmitError

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

Formats the value using the given formatter.

impl From<Error> for EmitError

fn from(_: Error) -> Self

The only writer that returns core::fmt::Error here is a capped SizeSink; a String sink is infallible, so this conversion fires exactly when a size bound was crossed.

impl PartialEq for EmitError

fn eq(&self, other: &EmitError) -> 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 EmitError

impl StructuralPartialEq for EmitError