Struct PartialCoveringMeasure 

pub struct PartialCoveringMeasure {
    pub base: CoveringMeasure,
    pub lo: usize,
    pub hi: usize,
}

A covering measure restricted to the absolute rounds [lo, hi] — it breaks only those covering levels, leaving a residual for a later stage. The tool that makes COMPOSITION non-trivial: a stage that genuinely hands a smaller problem to the next.

Fields

base: CoveringMeasure

lo: usize

hi: usize

Trait Implementations

impl Clone for PartialCoveringMeasure

fn clone(&self) -> PartialCoveringMeasure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl LyapunovMeasure for PartialCoveringMeasure

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, local_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.