Struct AffineCanonical 

pub struct AffineCanonical {
    pub num_vars: usize,
    pub clauses: Vec<Vec<Lit>>,
    /* private fields */
}

The result of the canonical affine reduction: an equisatisfiable formula over the free generators (the linearly-determined variables eliminated), plus the map to lift a reduced model back to the full space. This is the affine analogue of breaking a permutation orbit down to one representative — here the RREF canonicalizes the affine structure and the determined coordinates fall away.

Fields

num_vars: usize

clauses: Vec<Vec<Lit>>

Implementations

impl AffineCanonical

pub fn lift(&self, reduced_model: &[bool]) -> Vec<bool>

Lift a model of the reduced formula back to a model over the original variables, reconstructing each eliminated coordinate from its canonical definition (constant, or alias of a survivor).

Trait Implementations

impl Clone for AffineCanonical

fn clone(&self) -> AffineCanonical

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AffineCanonical

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

Formats the value using the given formatter.