Struct ResolutionRefutation 

pub struct ResolutionRefutation {
    pub clauses: Vec<Clause>,
    pub steps: Vec<ResolutionStep>,
}

A resolution refutation: derives ⊥ from a set of clauses.

Fields

clauses: Vec<Clause>

The initial clause set.

steps: Vec<ResolutionStep>

The sequence of resolution steps.

Implementations

impl ResolutionRefutation

pub fn new(clauses: Vec<Clause>) -> Self

Create a new refutation attempt from a clause set.

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

Add a resolution step.

pub fn is_complete(&self) -> bool

Returns true if the last step produced the empty clause.

pub fn unit_propagate(&self) -> Vec<Literal>

Perform unit propagation: return the set of forced literals.

pub fn dpll_step(&self) -> Option<u32>

A single DPLL-style split on the first unassigned variable.

Trait Implementations

impl Clone for ResolutionRefutation

fn clone(&self) -> ResolutionRefutation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolutionRefutation

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

Formats the value using the given formatter.