Enum ProofSystem 

pub enum ProofSystem {
    Resolution,
    Frege,
    ExtendedFrege,
    HalfFrege,
    CuttingPlanes,
    Nullstellensatz,
    SOS,
    IPS,
}

A propositional proof system.

Variants

Resolution

Resolution (Robinson 1965).

Frege

Frege / Hilbert-style propositional calculus.

ExtendedFrege

Extended Frege (with extension axioms).

HalfFrege

Half-Frege (bounded-depth Frege).

CuttingPlanes

Cutting Planes (LP relaxation cuts).

Nullstellensatz

Nullstellensatz proof system (algebraic).

SOS

Sum-of-Squares (Positivstellensatz).

IPS

Ideal Proof System (IPS).

Trait Implementations

impl Clone for ProofSystem

fn clone(&self) -> ProofSystem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofSystem

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

Formats the value using the given formatter.

impl Display for ProofSystem

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

Formats the value using the given formatter.

impl Hash for ProofSystem

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for ProofSystem

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

impl StructuralPartialEq for ProofSystem