Enum ProofKind 

pub enum ProofKind {
    Algebra(Vec<(Identity, KernelVerdict)>),
    Circuit,
}

How a lowering is proved.

Variants

Algebra(Vec<(Identity, KernelVerdict)>)

Identities over the integers, each with what the kernels said of it, and the intervals (checked here) that make every lane operation exact and turn the identities’ congruences into equalities.

Circuit

A certified equivalence check of the bit-blasted program against the bit-blasted definition.

Trait Implementations

impl Clone for ProofKind

fn clone(&self) -> ProofKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofKind

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

Formats the value using the given formatter.

impl PartialEq for ProofKind

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

impl StructuralPartialEq for ProofKind