Struct Subcube 

pub struct Subcube {
    pub n: usize,
    pub care: u64,
    pub value: u64,
}

A subcube of {0,1}ⁿ: the coordinates set in care are fixed to the matching bits of value; the rest are free. As a blocker it is the footprint of one clause — the corners that falsify it. (Pnp.lean’s Blocker, generalized from clean 3-bit faces to any width.)

Fields

n: usize

care: u64

Bitmask of the fixed (“cared-about”) coordinates — the blocker’s support.

value: u64

Required values on the fixed coordinates; bits outside care are held at 0.

Implementations

impl Subcube

pub fn blocker(clause: &[Lit], n: usize) -> Subcube

The blocker of a clause: the subcube of corners that set every literal false. A positive literal xᵥ is false at c[v]=0; a negative literal ¬xᵥ is false at c[v]=1. So care is the clause’s variable set and value’s bit v is set exactly for the negative literals.

pub fn covers(&self, corner: Corner) -> bool

Does this subcube contain corner? (Pnp.lean’s Blocker.Covers — is the clause falsified at this corner?)

pub fn dimension(&self) -> usize

The number of free coordinates — the subcube’s dimension as a face (n - |support|).

pub fn footprint_card(&self) -> u64

How many corners this blocker forbids: 2^dimension (the footprint cardinality).

pub fn clause_literals(&self) -> Vec<(usize, bool)>

Recover the clause this blocker is the footprint of — the inverse of Subcube::blocker. A fixed coordinate v appears positively when value’s bit is 0 (the clause is falsified at v=0) and negatively when it is 1. Round-tripping a clause through blocker and back is the proof that the geometric representation loses nothing.

pub fn clause_lp_value(&self, point: &[f64]) -> f64

The LP value of this blocker’s clause at a fractional point of [0,1]ⁿ: Σ over literals of x (positive) or 1−x (negative). The clause’s relaxation is satisfied iff the value is ≥ 1. At the ½-center every literal contributes ½, so the value is width/2 — satisfied iff width ≥ 2.

pub fn resolve(&self, other: &Subcube) -> Option<(usize, Subcube)>

Resolve two blockers — the geometry of clause resolution, the engine of “rules beget rules.” Two blockers resolve when their fixed coordinates agree everywhere except a single pivot where they take opposite values (one clause carries the pivot literal, the other its negation, with no other clashing literal). The resolvent is the merged blocker with the pivot freed — a new rule derived from the two neighbors, exactly the Quine–McCluskey adjacency of two implicants. Returns (pivot, resolvent), or None when there is no single clean pivot (no opposite literal, or a second clash making the resolvent a tautology).

pub fn footprint(&self) -> Vec<Corner>

Enumerate the blocked corners — the full footprint. Only sensible for small dimension.

Trait Implementations

impl Clone for Subcube

fn clone(&self) -> Subcube

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for Subcube

impl Debug for Subcube

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

Formats the value using the given formatter.

impl Eq for Subcube

impl Hash for Subcube

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Subcube

fn cmp(&self, other: &Subcube) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for Subcube

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

Equality operator ==.

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

Inequality operator !=.

impl PartialOrd for Subcube

fn partial_cmp(&self, other: &Subcube) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralPartialEq for Subcube