Struct ResolutionProof 

pub struct ResolutionProof {
    pub input_clauses: Vec<Vec<i32>>,
    pub steps: Vec<(usize, usize, i32, Vec<i32>)>,
}

A resolution proof: a DAG of resolution steps.

Fields

input_clauses: Vec<Vec<i32>>

The input clause set.

steps: Vec<(usize, usize, i32, Vec<i32>)>

Resolution steps: (parent1_idx, parent2_idx, pivot_var, resolvent).

Implementations

impl ResolutionProof

pub fn new(input_clauses: Vec<Vec<i32>>) -> Self

Create a new resolution proof from the given input clauses.

pub fn add_step( &mut self, p1: usize, p2: usize, pivot: i32, resolvent: Vec<i32>, )

Add a resolution step.

pub fn is_refutation(&self) -> bool

Returns true if the proof ends with the empty clause.

Trait Implementations

impl Clone for ResolutionProof

fn clone(&self) -> ResolutionProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolutionProof

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

Formats the value using the given formatter.