Struct ProofTreeArray

pub struct ProofTreeArray {
    pub trees: Vec<ProofTree>,
    pub qed: usize,
    /* private fields */
}

An array of proof trees, used to collect steps of a proof in proof order

Fields

trees: Vec<ProofTree>

The list of proof trees

qed: usize

The QED step

Implementations

impl ProofTreeArray

pub fn with_logical_steps<T>( &self, db: &Database, f: impl Fn(usize, usize, StatementRef<'_>, Vec<usize>) -> T, ) -> Vec<T>

Applies the provided function to each of the logical steps. It takes 4 parameters:

• cur - the index of the step among all proof steps (incuding non-logical ones). This can be used as an index in ProofTreeArray’s expressions exprs and indents.
• ix - the index of the step, when only logical steps are counted,
• stmt - the statement applied at this step,
• hyps - the indices of the hypotheses for this step (only counting logical hypotheses)

pub fn with_steps<T>( &self, db: &Database, f: impl Fn(usize, StatementRef<'_>, &Vec<usize>) -> T, ) -> Vec<T>

Applies the provided function to each of the steps. It takes 3 parameters:

• cur - the current index of the step,
• stmt - the statement applied at this step,
• hyps - the indices of the hypotheses for this step,

impl ProofTreeArray

pub fn new(enable_exprs: bool) -> Self

Constructs a new empty ProofTreeArray. If enable_exprs is true, it will construct expressions for each step, used by Database::export_mmp_proof_tree.

pub fn index(&self, tree: &ProofTree) -> Option<usize>

Get the index of a proof tree in the array

pub fn indent(&self) -> &[u16]

Get the minimum distance from each step to the QED step

pub fn calc_indent(&mut self)

Finds the shortest path from each node in the proof tree to the qed step, using Dijkstra’s algorithm. Based on the example in https://doc.rust-lang.org/std/collections/binary_heap/.

pub fn count_parents(&self) -> Vec<usize>

Get the number of parents of each step in the proof

pub fn to_rpn(&self, parents: &[usize], explicit: bool) -> Vec<RPNStep>

Write the proof as an RPN sequence with backrefs

pub fn normal_iter(&self, explicit: bool) -> NormalIter<'_>

Produce an iterator over the steps in the proof in normal/uncompressed mode. (Because this can potentially be very long, we do not store the list and just stream it.)

pub fn exprs(&self) -> Option<&[Vec<u8>]>

Returns the list of expressions corresponding to each proof tree.

Trait Implementations

impl Clone for ProofTreeArray

fn clone(&self) -> ProofTreeArray

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTreeArray

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

Formats the value using the given formatter.

impl Default for ProofTreeArray

fn default() -> Self

Returns the “default value” for a type.

impl ProofBuilder for ProofTreeArray

type Item = usize

The data type being generated

type Accum = Vec<usize>

The hyp gathering type

fn push(&mut self, hyps: &mut Vec<usize>, hyp: usize)

Add a new hyp to the accumulation type

fn build( &mut self, addr: StatementAddress, trees: Vec<usize>, pool: &[u8], expr: Range<usize>, ) -> usize

Create a proof data node from a statement, the data for the hypotheses, and the compressed constant string