Enum SNode 

pub enum SNode {
    Trivial(CanonClauses),
    Structured {
        clauses: CanonClauses,
        route: Route,
    },
    Internal {
        clauses: CanonClauses,
        var: u32,
        lo: usize,
        hi: usize,
    },
}

A node of the structured-leaf cofactor DAG.

Variants

Trivial(CanonClauses)

The clause set contains ⊥ — UNSAT on the spot.

Structured

A specialist route refutes this cofactor (route fired); certified internally by that route.

Fields

clauses: CanonClauses

route: Route

Internal

Branch on var: children are the two Shannon cofactors.

Fields

clauses: CanonClauses

var: u32

lo: usize

hi: usize

Trait Implementations

impl Clone for SNode

fn clone(&self) -> SNode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SNode

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

Formats the value using the given formatter.