| java.lang.Object
 de.uka.ilkd.key.proof.Node
| Constructor Summary | |
| public | Node(Proof proof)
creates an empty node that is root and leaf. | | public | Node(Proof proof, Sequent seq)
| | public | Node(Proof proof, Sequent seq, List children, Node parent, Sink branchSink)
creates a node with the given contents, the given collection
of children (all elements must be of class Node) and the given
parent node. |
| reuseCandidate | | int reuseCandidate(Code) | | |
| Node | | public Node(Proof proof)(Code) | | creates an empty node that is root and leaf.
|
| Node | | public Node(Proof proof, Sequent seq, List children, Node parent, Sink branchSink)(Code) | | creates a node with the given contents, the given collection
of children (all elements must be of class Node) and the given
parent node.
|
| add | | public void add(Node child)(Code) | | makes the given node a child of this node.
|
| addNoPosTacletApp | | public void addNoPosTacletApp(NoPosTacletApp s)(Code) | | adds a new NoPosTacletApp to the set of available NoPosTacletApps
at this node
|
| child | | public Node child(int i)(Code) | | returns i-th child
|
| childrenCount | | public int childrenCount()(Code) | | returns number of children
|
| childrenIterator | | public IteratorOfNode childrenIterator()(Code) | | returns an iterator for the direct children of this node.
|
| clearReuseCandidates | | public static void clearReuseCandidates()(Code) | | |
| clearReuseCandidates | | public static void clearReuseCandidates(Proof p)(Code) | | |
| commonAncestor | | public Node commonAncestor(Node p_node)(Code) | | Search for the node being the root of the smallest subtree
containing this and p_node; we assume
that the two nodes are part of the same proof tree
|
| countBranches | | public int countBranches()(Code) | | retrieves number of branches
|
| countNodes | | public int countNodes()(Code) | | retrieves number of nodes
|
| cutChildrenSinks | | public void cutChildrenSinks()(Code) | | Remove a possibly existing merger, restore the old state by
calling "localSink.reset()". Currently this doesn't really
remove the connection between the children sinks and the branch
sink.
|
| find | | public boolean find(Node node)(Code) | | searches for a given node in the subtree starting with this node
|
| getChildNr | | public int getChildNr(Node p_node)(Code) | | the number of the node p_node, if it is achild of this node (starting with 0),-1 otherwise |
| getGlobalProgVars | | public SetOfProgramVariable getGlobalProgVars()(Code) | | |
| getNoPosTacletApps | | public SetOfNoPosTacletApp getNoPosTacletApps()(Code) | | Returns the set of NoPosTacletApps at this node
|
| getNodeInfo | | public NodeInfo getNodeInfo()(Code) | | the node information object encapsulates non-logical information
of the node, e.g.
|
| getRenamingTable | | public ListOfRenamingTable getRenamingTable()(Code) | | |
| getRestrictedMetavariables | | public SetOfMetavariable getRestrictedMetavariables()(Code) | | |
| getUniqueTacletNr | | public int getUniqueTacletNr()(Code) | | |
| isClosed | | public boolean isClosed()(Code) | | |
| isReuseCandidate | | public boolean isReuseCandidate()(Code) | | |
| leaf | | public boolean leaf()(Code) | | returns true, iff this node is a leaf, i.e. has no children.
|
| leavesIterator | | public IteratorOfNode leavesIterator()(Code) | | returns an iterator for the leaves of the subtree below this
node. The computation is called at every call!
|
| markPersistentCandidate | | public void markPersistentCandidate()(Code) | | |
| markReuseCandidate | | public void markReuseCandidate()(Code) | | |
| parent | | public Node parent()(Code) | | returns the parent node of this node.
|
| proof | | public Proof proof()(Code) | | returns the proof the Node belongs to
|
| remove | | public void remove()(Code) | | removes child/parent relationship between this node and its
parent; if this node is root nothing happens.
|
| remove | | public boolean remove(Node child)(Code) | | removes child/parent relationship between the given node and
this node; if the given node is not child of this node,
nothing happens and then and only then false is returned.
false iff the given node was not child of this node andnothing has been done. |
| removeLocalRootSink | | public void removeLocalRootSink()(Code) | | |
| reserveSinks | | public IteratorOfSink reserveSinks(int p_count)(Code) | | Reserve p_count sinks meant for children and return them. If
ultimately more than one sink is needed, the first call to this
method MUST have p_count>1.
|
| resetBranchSink | | public void resetBranchSink()(Code) | | |
| reuseCandidatesIterator | | public static Iterator reuseCandidatesIterator()(Code) | | |
| reuseCandidatesNumber | | public static int reuseCandidatesNumber()(Code) | | |
| root | | public boolean root()(Code) | | returns true, iff this node is root, i.e. has no parents.
|
| sanityCheckDoubleLinks | | public boolean sanityCheckDoubleLinks()(Code) | | checks if the parent has this node as child and continues recursively
with the children of this node.
true iff the parent of this node has this node as child andthis condition holds also for the own children. |
| sequent | | public Sequent sequent()(Code) | | returns the sequent of this node
|
| serialNr | | public int serialNr()(Code) | | |
| setAppliedRuleApp | | public void setAppliedRuleApp(RuleApp ruleApp)(Code) | | |
| setClosed | | public void setClosed()(Code) | | |
| setGlobalProgVars | | public void setGlobalProgVars(SetOfProgramVariable progVars)(Code) | | |
| setRenamings | | public void setRenamings(ListOfRenamingTable list)(Code) | | |
| setSequent | | public void setSequent(Sequent seq)(Code) | | sets the sequent at this node
|
| siblingNr | | public int siblingNr()(Code) | | returns the sibling number of this node or -1 if
it is the root node
the sibling number of this node or -1 ifit is the root node |
| subtreeCompletelyClosed | | public void subtreeCompletelyClosed()(Code) | | This is called by "BranchRestricter" to indicate that the
subtree below this Node is closed
|
| unmarkReuseCandidate | | public void unmarkReuseCandidate()(Code) | | |
|
|