Struct ResolutionStep 

pub struct ResolutionStep {
    pub parent1: Clause,
    pub parent2: Clause,
    pub pivot: u32,
    pub resolvent: Clause,
}

A single resolution step: C_1 ∨ x, C_2 ∨ ¬x ⊢ C_1 ∨ C_2.

Fields

parent1: Clause

First parent clause (contains pivot positively).

parent2: Clause

Second parent clause (contains pivot negatively).

pivot: u32

The pivot variable.

resolvent: Clause

The resolvent clause.

Implementations

impl ResolutionStep

pub fn resolve(c1: &Clause, c2: &Clause, pivot: u32) -> Option<Self>

Attempt to resolve c1 and c2 on variable pivot. Returns None if the pivot does not appear with opposite signs.

Trait Implementations

impl Clone for ResolutionStep

fn clone(&self) -> ResolutionStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolutionStep

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

Formats the value using the given formatter.