Struct RankedRefutation 

pub struct RankedRefutation {
    pub refuted: bool,
    pub steps: Vec<ProofStep>,
    pub ranks: Vec<u64>,
}

A refutation whose every step carries a rank (a progress/termination measure).

Fields

refuted: bool

Whether the underlying refutation independently checked.

steps: Vec<ProofStep>

The proof steps, in order.

ranks: Vec<u64>

ranks[i] is the measure value at step i. Must be non-increasing for a valid certificate.

Implementations

impl RankedRefutation

pub fn certify( &self, num_vars: usize, formula: &[Vec<Lit>], ) -> Option<SizeBound>

Independently check BOTH facets against the original formula: the refutation is correct (the PR checker accepts it) AND its size is bounded by its rank certificate. Returns the certified SizeBound only if both hold.

Trait Implementations

impl Clone for RankedRefutation

fn clone(&self) -> RankedRefutation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RankedRefutation

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

Formats the value using the given formatter.