Enum ProofResult 

pub enum ProofResult {
    Unsatisfiable {
        steps: usize,
        derivation: Vec<ResolutionStep>,
    },
    Satisfiable,
    Saturated {
        clauses_generated: usize,
    },
    ResourceLimitReached {
        steps_attempted: usize,
    },
}

Result of a resolution proof attempt.

Variants

Unsatisfiable

The clause set is unsatisfiable (empty clause derived)

Fields

steps: usize

Steps taken to derive empty clause

derivation: Vec<ResolutionStep>

Derivation path (sequence of resolution steps)

Satisfiable

The clause set is satisfiable (no contradiction found)

Saturated

Proof attempt reached saturation without finding empty clause

Fields

clauses_generated: usize

Number of clauses generated

ResourceLimitReached

Proof search reached resource limit

Fields

steps_attempted: usize

Number of steps attempted

Implementations

impl ProofResult

pub fn is_unsatisfiable(&self) -> bool

Check if the result proves unsatisfiability.

pub fn is_satisfiable(&self) -> bool

Check if the result proves satisfiability.

pub fn steps(&self) -> usize

Get the number of steps taken.

Trait Implementations

impl Clone for ProofResult

fn clone(&self) -> ProofResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofResult

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ProofResult

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for ProofResult

fn eq(&self, other: &ProofResult) -> 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 Serialize for ProofResult

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for ProofResult