Struct ArrayProofRecorder 

pub struct ArrayProofRecorder { /* private fields */ }

Array-specific proof recorder

Implementations

impl ArrayProofRecorder

pub fn new() -> Self

Create a new array proof recorder

pub fn record_select_store_same( &mut self, array: impl Into<ProofTerm>, index: impl Into<ProofTerm>, value: impl Into<ProofTerm>, ) -> TheoryStepId

Record a select-store axiom (same index)

pub fn record_select_store_diff( &mut self, neq_proof: TheoryStepId, array: impl Into<ProofTerm>, i: impl Into<ProofTerm>, j: impl Into<ProofTerm>, v: impl Into<ProofTerm>, ) -> TheoryStepId

Record a select-store axiom (different index)

pub fn proof(&self) -> &TheoryProof

Get the recorded proof

pub fn take_proof(&mut self) -> TheoryProof

Take the proof

Trait Implementations

impl Debug for ArrayProofRecorder

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

Formats the value using the given formatter.

impl Default for ArrayProofRecorder

fn default() -> ArrayProofRecorder

Returns the “default value” for a type.