public class Trace extends java.lang.Object implements java.lang.Iterable<TraceNode>
TraceNode
; the head of the tree is
returned by the getProofSearchTree()
method. Performing a
depth-first order traversal of the proof-search tree one gets the sequence of
rules applications performed by the prover during the proof-search. Modifier and Type | Method and Description |
---|---|
_AbstractGoal |
getInitialNodeSet()
Returns the initial node set (the node set at the root of the
proof-search).
|
TraceNode |
getProofSearchTree()
Returns the root of the proof-search tree.
|
_Prover |
getProver()
Returns the prover used to generate this trace.
|
ProofSearchResult |
getStatus()
Returns the status of the proof-search described by this trace.
|
boolean |
isPruned()
Returns
true iff this trace has already been pruned. |
java.util.Iterator<TraceNode> |
iterator()
Returns the iterator containing the nodes of the proof-search tree as
visited by a depth-first order traversal.
|
void |
print(java.io.PrintStream out)
Print a description of the trace on the specified stream.
|
void |
pruneSuccessful()
Prunes the trace-tree removing the inessential branches from the successful
trace.
|
java.lang.String |
toString() |
public TraceNode getProofSearchTree()
public _AbstractGoal getInitialNodeSet()
public _Prover getProver()
public ProofSearchResult getStatus()
public boolean isPruned()
true
iff this trace has already been pruned.true
iff this trace is pruned.public java.util.Iterator<TraceNode> iterator()
iterator
in interface java.lang.Iterable<TraceNode>
public void pruneSuccessful() throws TraceException
isPruned()
will return true
. For a trace describing a
successful proof-search this methods removes all paths corresponding to
failed branches in the proof search.TraceException
- if this trace is not a successful trace and hence
pruning cannot be performed.public java.lang.String toString()
toString
in class java.lang.Object
public void print(java.io.PrintStream out)
out
- the stream where to write the trace.