Struct TreeTerm

pub struct TreeTerm<L: Language> {
    pub node: L,
    pub backward_rule: Option<Symbol>,
    pub forward_rule: Option<Symbol>,
    pub child_proofs: Vec<TreeExplanation<L>>,
    /* private fields */
}

An explanation for a term and its equivalent children. Each child is a proof transforming the initial child into the final child term. The initial term is given by taking each first sub-term in each child_proofs recursively. The final term is given by all of the final terms in each child_proofs.

If forward_rule is provided, then this TreeTerm’s initial term can be derived from the previous TreeTerm by applying the rule. Similarly, if backward_rule is provided, then the previous TreeTerm’s final term is given by applying the rule to this TreeTerm’s initial term.

TreeTerms are flattened by first flattening child_proofs, then wrapping the flattened proof with this TreeTerm’s node.

Fields

node: L

A node representing this TreeTerm’s operator. The children of the node should be ignored.

backward_rule: Option<Symbol>

A rule rewriting this TreeTerm’s initial term back to the last TreeTerm’s final term.

forward_rule: Option<Symbol>

A rule rewriting the last TreeTerm’s final term to this TreeTerm’s initial term.

child_proofs: Vec<TreeExplanation<L>>

A list of child proofs, each transforming the initial term to the final term for that child.

Implementations

impl<L: Language> TreeTerm<L>

pub fn new(node: L, child_proofs: Vec<TreeExplanation<L>>) -> TreeTerm<L>

Construct a new TreeTerm given its node and child_proofs.

pub fn get_initial_flat_term(&self) -> FlatTerm<L>

Get a FlatTerm representing the first term in this proof.

pub fn get_last_flat_term(&self) -> FlatTerm<L>

Get a FlatTerm representing the final term in this proof.

pub fn flatten_explanation(&self) -> FlatExplanation<L>

Construct the FlatExplanation for this TreeTerm.

Trait Implementations

impl<L: Clone + Language> Clone for TreeTerm<L>

fn clone(&self) -> TreeTerm<L>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<L: Debug + Language> Debug for TreeTerm<L>

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

Formats the value using the given formatter.

impl<L: Language + Display + FromOp> Display for TreeTerm<L>

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

Formats the value using the given formatter.