Struct ProofStep

pub struct ProofStep {
    pub id: TermId,
    pub kind: ProofStepKind,
    pub result: TermIdx,
    pub prerequisites: BoxSlice<ProofIdx>,
    pub frame: StackIdx,
}

A Z3 proof step and associated data. Represents a single step where z3 proved a boolean expression. These steps have dependencies which combine to build up a proof tree. Parts of this tree may be under hypotheses in which case the solver tries to do a proof by contradiction (and the proved terms are only valid under these hypotheses).

Fields

id: TermId

The parsed term id of the proof step itself (corresponds to ProofIdx). Only useful for debugging.

kind: ProofStepKind

The kind of proof step. Which logical rule was used to derive the result.

result: TermIdx

The (boolean) term which this step proves. This might not necessarily be a “full” proof if this step (transitively) depends on any hypotheses!

prerequisites: BoxSlice<ProofIdx>

The antecedents of this proof step.

frame: StackIdx

The frame in which this proof step was created. The proof is forgotten (and may be repeated later) when the frame is popped.

Trait Implementations

impl Debug for ProofStep

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

Formats the value using the given formatter.

impl HasTermId for ProofStep

fn term_id(&self) -> TermId