Struct Proof 

pub struct Proof { /* private fields */ }

A proof tree with explicit node tracking.

This structure maintains a DAG (Directed Acyclic Graph) of proof steps, allowing for efficient premise tracking and proof compression.

Implementations

impl Proof

pub fn new() -> Self

Create a new empty proof

pub fn add_axiom(&mut self, conclusion: impl Into<String>) -> ProofNodeId

Add an axiom to the proof

pub fn add_inference( &mut self, rule: impl Into<String>, premises: Vec<ProofNodeId>, conclusion: impl Into<String>, ) -> ProofNodeId

Add an inference step to the proof

pub fn add_inference_with_args( &mut self, rule: impl Into<String>, premises: Vec<ProofNodeId>, args: Vec<String>, conclusion: impl Into<String>, ) -> ProofNodeId

Add an inference step with arguments

pub fn get_node(&self, id: ProofNodeId) -> Option<&ProofNode>

Get a proof node by ID

pub fn update_conclusion( &mut self, id: ProofNodeId, new_conclusion: impl Into<String>, ) -> bool

Update the conclusion of a proof node.

Returns true if the node was found and updated, false otherwise. This is useful for proof simplification and transformation.

pub fn nodes(&self) -> &[ProofNode]

Get all proof nodes

pub fn roots(&self) -> &[ProofNodeId]

Get the root nodes

pub fn root(&self) -> Option<ProofNodeId>

Get the primary root (last added root)

pub fn root_node(&self) -> Option<&ProofNode>

Get the primary root node

pub fn len(&self) -> usize

Get the number of nodes

pub fn depth(&self) -> u32

Get the maximum depth of the proof tree

pub fn node_count(&self) -> usize

Get the node count (alias for len())

pub fn leaf_nodes(&self) -> Vec<ProofNodeId>

Get all leaf nodes (axioms - nodes with no premises)

pub fn premises(&self, node_id: ProofNodeId) -> Option<&[ProofNodeId]>

Get the premises of a node (if it’s an inference)

pub fn is_empty(&self) -> bool

Check if the proof is empty

pub fn clear(&mut self)

Clear the proof

pub fn stats(&self) -> ProofStats

Get proof statistics

pub fn write<W: Write>(&self, writer: W) -> Result<()>

Write the proof in a human-readable format

pub fn to_string_repr(&self) -> String

Convert to string

pub fn add_axioms( &mut self, conclusions: impl IntoIterator<Item = impl Into<String>>, ) -> Vec<ProofNodeId>

Add multiple axioms at once and return their IDs

pub fn find_nodes_by_rule(&self, rule: &str) -> Vec<ProofNodeId>

Find all nodes with a specific rule

pub fn find_nodes_by_conclusion(&self, conclusion: &str) -> Vec<ProofNodeId>

Find all nodes with a specific conclusion

pub fn get_children(&self, node_id: ProofNodeId) -> Vec<ProofNodeId>

Get all direct children (premises) of a node

pub fn get_parents(&self, node_id: ProofNodeId) -> Vec<ProofNodeId>

Get all direct parents (dependents) of a node

pub fn is_ancestor( &self, ancestor: ProofNodeId, descendant: ProofNodeId, ) -> bool

Check if one node is an ancestor of another

pub fn get_all_ancestors(&self, node_id: ProofNodeId) -> Vec<ProofNodeId>

Get all ancestors of a node (all nodes it depends on)

pub fn count_rule(&self, rule: &str) -> usize

Count nodes of a specific rule type

pub fn set_metadata(&mut self, node_id: ProofNodeId, metadata: ProofMetadata)

Set metadata for a proof node.

pub fn get_metadata(&self, node_id: ProofNodeId) -> Option<&ProofMetadata>

Get metadata for a proof node.

pub fn get_metadata_mut( &mut self, node_id: ProofNodeId, ) -> Option<&mut ProofMetadata>

Get mutable metadata for a proof node.

pub fn remove_metadata(&mut self, node_id: ProofNodeId) -> Option<ProofMetadata>

Remove metadata for a proof node.

pub fn has_metadata(&self, node_id: ProofNodeId) -> bool

Check if a node has metadata.

pub fn nodes_with_tag(&self, tag: &str) -> Vec<ProofNodeId>

Get all nodes with a specific tag.

pub fn nodes_with_priority(&self, priority: Priority) -> Vec<ProofNodeId>

Get all nodes with a specific priority.

pub fn nodes_with_difficulty(&self, difficulty: Difficulty) -> Vec<ProofNodeId>

Get all nodes with a specific difficulty.

pub fn nodes_with_strategy(&self, strategy: Strategy) -> Vec<ProofNodeId>

Get all nodes with a specific strategy.

pub fn get_or_create_metadata( &mut self, node_id: ProofNodeId, ) -> &mut ProofMetadata

Get or create metadata for a node.

Trait Implementations

impl Clone for Proof

fn clone(&self) -> Proof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Proof

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

Formats the value using the given formatter.

impl Default for Proof

fn default() -> Self

Returns the “default value” for a type.