Struct Earlier 

pub struct Earlier { /* private fields */ }

Lemmas in proof order, each node of one indexed by the lemmas that relate it: the lemmas touching a cone found in time proportional to the cone, not to every lemma, in lemma order.

Implementations

impl Earlier

pub fn new() -> Earlier

pub fn push(&mut self, a: AigLit, b: AigLit)

Add the lemma a ≡ b after every one before it.

pub fn pairs(&self) -> &[(AigLit, AigLit)]

Trait Implementations

impl Clone for Earlier

fn clone(&self) -> Earlier

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Earlier

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

Formats the value using the given formatter.

impl Default for Earlier

fn default() -> Earlier

Returns the “default value” for a type.

impl From<&[(AigLit, AigLit)]> for Earlier

fn from(pairs: &[(AigLit, AigLit)]) -> Earlier

Converts to this type from the input type.