Struct varisat_checker::clauses::ClauseLits

pub struct ClauseLits {
    length: LitIdx,
    inline: [LitIdx; 3],
}

Literals of a clause, either inline or an index into a buffer

Fields

length: LitIdx

inline: [LitIdx; 3]

Methods

impl ClauseLits

fn new(lits: &[Lit], buffer: &mut Vec<Lit>) -> ClauseLits

Create a new ClauseLits, storing them in the given buffer if necessary

pub fn slice<'a, 'b, 'c>(&'a self, buffer: &'b [Lit]) -> &'c [Lit] where
    'a: 'c,
    'b: 'c, 

Returns the literals as a slice given a storage buffer

fn buffer_used(&self) -> usize

Literals stored in the literal buffer