Struct InductionCertificate 

pub struct InductionCertificate {
    pub invariant: Vec<(AigLit, AigLit)>,
    pub steps: Vec<Lrat>,
    pub outputs: Vec<Option<Lrat>>,
}

The proof that two circuits agree at every clock from reset: an invariant of register literal pairs true at reset, each pair’s next values proven equal assuming the invariant (one proof a pair, in order), and each output pair proven equal assuming it (one proof an output, in the product’s order, absent for an output pair that is one literal).

Fields

invariant: Vec<(AigLit, AigLit)>

steps: Vec<Lrat>

outputs: Vec<Option<Lrat>>

Trait Implementations

impl Clone for InductionCertificate

fn clone(&self) -> InductionCertificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductionCertificate

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

Formats the value using the given formatter.