Struct Lrat 

pub struct Lrat {
    pub steps: Vec<LratStep>,
}

An LRAT refutation of a formula whose clauses carry the ids 1..=n: additions in increasing id order, ending in the empty clause.

Fields

steps: Vec<LratStep>

Implementations

impl Lrat

pub fn to_text(&self) -> String

The proof as LRAT text: <id> <clause> 0 <hints> 0 a line, literals in DIMACS numbering.

Trait Implementations

impl Clone for Lrat

fn clone(&self) -> Lrat

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lrat

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

Formats the value using the given formatter.

impl PartialEq for Lrat

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Lrat

impl StructuralPartialEq for Lrat