Struct ProofComplexityMeasure 

pub struct ProofComplexityMeasure {
    pub size: usize,
    pub depth: usize,
    pub width: usize,
    pub degree: usize,
}

Proof complexity measure: size, depth, width, degree.

Fields

size: usize

Total number of lines / nodes in the proof.

depth: usize

Maximum nesting depth.

width: usize

Maximum clause width (number of literals per clause).

degree: usize

Algebraic degree (for algebraic systems).

Implementations

impl ProofComplexityMeasure

pub fn zero() -> Self

Construct a measure with all fields set to zero.

pub fn is_within_bound(&self, bound: usize) -> bool

Returns true if all measures are within the given bound.

Trait Implementations

impl Clone for ProofComplexityMeasure

fn clone(&self) -> ProofComplexityMeasure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofComplexityMeasure

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

Formats the value using the given formatter.

impl PartialEq for ProofComplexityMeasure

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

impl StructuralPartialEq for ProofComplexityMeasure