Struct CoveringMeasure 

pub struct CoveringMeasure {
    pub num_vars: usize,
    pub formula: Vec<Vec<Lit>>,
    pub items: usize,
    pub bins: usize,
}

A covering Lyapunov measure: items into bins (var(i,b) = i*bins + b) with item-swap witnesses. ONE measure type that instantiates the theorem for every covering family — PHP (items = n, bins = n-1), clique-coloring (items = n, bins = k), and any other generalized pigeonhole. The “lift”: the family is data, the measure is uniform.

Fields

num_vars: usize

formula: Vec<Vec<Lit>>

items: usize

bins: usize

Trait Implementations

impl Clone for CoveringMeasure

fn clone(&self) -> CoveringMeasure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl LyapunovMeasure for CoveringMeasure

fn num_vars(&self) -> usize

The number of variables of the formula.

fn formula(&self) -> &[Vec<Lit_>]

The formula F the measure refutes.

fn initial_potential(&self) -> u64

The initial potential L (the number of descent levels).

fn width(&self) -> u64

The per-level width bound w (max certified additions per level).

fn descent_step( &self, level: u64, _db: &[Vec<Lit_>], ) -> Vec<(Vec<Lit_>, Witness)>

The certified-redundant clause additions descending from level to level-1, given the current database. Each MUST be RUP/PR/SR against db (the constructor re-checks, fail-closed), and there must be at most width() of them.