Struct DerivationNode 

pub struct DerivationNode {
    pub goal: (String, String),
    pub rule: Option<DeductiveRule>,
    pub children: Vec<DerivationNode>,
    pub program: Option<String>,
}

A deductive synthesis derivation tree node.

Fields

goal: (String, String)

The synthesis goal at this node: (precondition, postcondition).

rule: Option<DeductiveRule>

The rule applied to discharge this goal.

children: Vec<DerivationNode>

Child derivations.

program: Option<String>

The synthesised program fragment (leaf nodes only).

Implementations

impl DerivationNode

pub fn leaf( pre: impl Into<String>, post: impl Into<String>, program: impl Into<String>, ) -> Self

Create a leaf node with a concrete program.

pub fn internal( pre: impl Into<String>, post: impl Into<String>, rule: DeductiveRule, children: Vec<DerivationNode>, ) -> Self

Create an internal node with a rule and sub-goals.

pub fn extract_program(&self) -> String

Extract the full synthesised program by recursively assembling sub-trees.

pub fn depth(&self) -> usize

Depth of the derivation tree.

Trait Implementations

impl Clone for DerivationNode

fn clone(&self) -> DerivationNode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DerivationNode

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

Formats the value using the given formatter.