Struct ProofTree 

pub struct ProofTree {
    pub root: ProofNode,
    pub query: Term,
    pub bindings: HashMap<String, Term>,
    pub is_complete: bool,
}

A complete distributed proof tree for a top-level query.

After DistributedBackwardChainer::prove_with_tree returns, callers inspect is_complete to know whether the goal was fully proved and bindings to extract the final variable bindings.

Fields

root: ProofNode

Root node of the tree.

query: Term

The top-level query term.

bindings: HashMap<String, Term>

Final variable bindings produced by the proof search.

is_complete: bool

true when every node in the tree is resolved.

Implementations

impl ProofTree

pub fn new( root: ProofNode, query: Term, bindings: HashMap<String, Term>, ) -> Self

Construct a new proof tree.

pub fn failed(query: Term) -> Self

Build an “empty” (failed) proof tree for a query that could not be proved.

pub fn size(&self) -> usize

Total number of nodes in the tree.

pub fn max_depth(&self) -> usize

Maximum depth reached by the proof search.

pub fn contributing_peers(&self) -> Vec<String>

All unique peer IDs that contributed to the proof.

pub fn prune_unresolved(&mut self)

Remove branches that did not contribute to a resolved proof.

Traverses the tree and prunes any subtree whose root node is not resolved. After pruning, is_complete is re-derived from the root.

Only the shortest resolution path is kept for each unique set of bindings: when multiple resolved branches exist at the same level, the shallowest one (fewest total nodes) is retained.

pub fn collapse_chains(&mut self)

Collapse relay chains where an intermediate node has exactly one child.

A chain A → B → C becomes A → C when B has a single child and carries no rule CID or peer attribution of its own. Depths are recomputed after collapsing to keep the tree consistent.

pub fn remote_contributions(&self) -> Vec<(&ProofNode, SocketAddr)>

Return all proof nodes that were resolved by remote peers together with a parsed std::net::SocketAddr.

The peer field is expected to contain an address in the form "ip:port". Nodes whose peer string cannot be parsed as a SocketAddr are silently omitted.

pub fn merge(&mut self, other: ProofTree)

Merge other into self, keeping the deeper/more-complete subtree for each branch.

When both trees have a resolved root the tree with more nodes (richer derivation) wins. When only one is resolved that one wins. Bindings from other are folded in for keys not already present in self.

pub fn to_stream( &self, session_id: impl Into<String>, ) -> (ProofTreeStreamer, UnboundedReceiver<ProofTreeUpdate>)

Stream this tree as crate::proof_tree_streaming::ProofTreeUpdate events.

The method walks the tree in BFS order, emitting one update per node, then emits a final update. Returns the crate::proof_tree_streaming::ProofTreeStreamer that was used together with the receiving end of the channel so the caller can consume updates asynchronously.

Trait Implementations

impl Clone for ProofTree

fn clone(&self) -> ProofTree

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTree

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ProofTree

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for ProofTree

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

Formats the value using the given formatter.

impl Serialize for ProofTree

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.