Struct Proof 

pub struct Proof { /* private fields */ }

A proof of unsatisfiability

Implementations

impl Proof

pub fn new() -> Self

Create a new empty proof

pub fn add_step(&mut self, step: ProofStep)

Add a proof step

pub fn set_empty_clause(&mut self, index: u32)

Set the index of the empty clause (final step proving unsat)

pub fn is_complete(&self) -> bool

Check if the proof is complete (has an empty clause)

pub fn len(&self) -> usize

Get the number of proof steps

pub fn is_empty(&self) -> bool

Check if the proof is empty

pub fn format(&self) -> String

Format the proof as a string (for debugging or output)

Trait Implementations

impl Clone for Proof

fn clone(&self) -> Proof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Proof

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

Formats the value using the given formatter.

impl Default for Proof

fn default() -> Self

Returns the “default value” for a type.