Constructor and Description |
---|
Node(Proof proof)
creates an empty node that is root and leaf.
|
Node(Proof proof,
Sequent seq)
creates a node with the given contents
|
Node(Proof proof,
Sequent seq,
Node parent)
creates a node with the given contents, the given collection of children (all
elements must be of class Node) and the given parent node.
|
Modifier and Type | Method and Description |
---|---|
void |
add(Node newChild)
Makes the given node a child of this node.
|
void |
addAll(Node[] newChildren)
Makes the given node children of this node.
|
void |
addLocalFunctions(java.util.Collection<? extends Function> elements) |
void |
addLocalProgVars(java.lang.Iterable<? extends IProgramVariable> elements) |
void |
addNoPosTacletApp(NoPosTacletApp s)
adds a new NoPosTacletApp to the set of available NoPosTacletApps at this
node
|
void |
addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod) |
Node |
child(int i) |
int |
childrenCount() |
java.util.Iterator<Node> |
childrenIterator() |
void |
clearNameCache() |
Node |
commonAncestor(Node other)
Search for the root of the smallest subtree containing
this and other ; we assume that the two nodes are
part of the same proof tree |
int |
countBranches() |
int |
countNodes() |
<T> void |
deregister(T obj,
java.lang.Class<T> service)
Remove a previous registered user-defined data.
|
boolean |
find(Node node)
Searches for a given node in the subtree starting with this node.
|
RuleApp |
getAppliedRuleApp() |
int |
getChildNr(Node child) |
java.lang.Iterable<Function> |
getLocalFunctions()
Returns the set of freshly created function symbols known to this node.
|
java.lang.Iterable<NoPosTacletApp> |
getLocalIntroducedRules()
Returns the set of NoPosTacletApps at this node
|
ImmutableList<IProgramVariable> |
getLocalProgVars()
Returns the set of created program variables known in this node.
|
NameRecorder |
getNameRecorder() |
NodeInfo |
getNodeInfo()
the node information object encapsulates non-logical information of the node,
e.g.
|
ImmutableList<RenamingTable> |
getRenamingTable() |
java.util.List<StrategyInfoUndoMethod> |
getStrategyInfoUndoMethods() |
java.lang.StringBuffer |
getUniqueTacletId() |
Lookup |
getUserData()
Get the assocated lookup of user-defined data.
|
boolean |
isClosed() |
java.util.Iterator<Node> |
iterator()
Returns an iterator over this node's children.
|
boolean |
leaf() |
java.util.Iterator<Node> |
leavesIterator() |
<T> T |
lookup(java.lang.Class<T> service)
Retrieves a user-defined data.
|
java.lang.String |
name() |
Node |
parent() |
Proof |
proof()
returns the proof the Node belongs to
|
<T> void |
register(T obj,
java.lang.Class<T> service)
Register a user-defined data in this node info.
|
boolean |
root() |
boolean |
sanityCheckDoubleLinks()
Checks if the parent has this node as child and continues recursively with
the children of this node.
|
Sequent |
sequent()
returns the sequent of this node
|
int |
serialNr() |
void |
setAppliedRuleApp(RuleApp ruleApp) |
void |
setNameRecorder(NameRecorder rec) |
void |
setRenamings(ImmutableList<RenamingTable> list) |
void |
setSequent(Sequent seq)
sets the sequent at this node
|
int |
siblingNr()
Returns the sibling number of this node or -1 if it is the root node
|
Statistics |
statistics() |
java.util.Iterator<Node> |
subtreeIterator() |
java.lang.String |
toString() |
public Node(Proof proof)
public void setSequent(Sequent seq)
public Sequent sequent()
public NodeInfo getNodeInfo()
public Proof proof()
public void setAppliedRuleApp(RuleApp ruleApp)
public void clearNameCache()
public NameRecorder getNameRecorder()
public void setNameRecorder(NameRecorder rec)
public void setRenamings(ImmutableList<RenamingTable> list)
public ImmutableList<RenamingTable> getRenamingTable()
public RuleApp getAppliedRuleApp()
public java.lang.Iterable<NoPosTacletApp> getLocalIntroducedRules()
public ImmutableList<IProgramVariable> getLocalProgVars()
public void addLocalProgVars(java.lang.Iterable<? extends IProgramVariable> elements)
public java.lang.Iterable<Function> getLocalFunctions()
public void addLocalFunctions(java.util.Collection<? extends Function> elements)
public void addNoPosTacletApp(NoPosTacletApp s)
s
- the app to add.public Node parent()
public boolean leaf()
public boolean find(Node node)
true
iff the node was found.public Node commonAncestor(Node other)
this
and other
; we assume that the two nodes are
part of the same proof treeother
- a node.this
and the specified node.public boolean root()
public Statistics statistics()
public void add(Node newChild)
newChild
- the node to make a child of this node.public void addAll(Node[] newChildren)
newChildren
- the node to make into children of this node.public java.util.Iterator<Node> leavesIterator()
public java.util.Iterator<Node> childrenIterator()
public java.util.Iterator<Node> subtreeIterator()
public int childrenCount()
public Node child(int i)
i
- an index.public int getChildNr(Node child)
child
- a child of this node.child
, if it is a child of this
node (starting with 0
), -1
otherwisepublic java.lang.StringBuffer getUniqueTacletId()
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String name()
public boolean sanityCheckDoubleLinks()
public boolean isClosed()
public int countNodes()
public int countBranches()
public int serialNr()
public int siblingNr()
public java.util.List<StrategyInfoUndoMethod> getStrategyInfoUndoMethods()
public void addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod)
public java.util.Iterator<Node> iterator()
leavesIterator()
if you need to iterate over leaves instead.iterator
in interface java.lang.Iterable<Node>
public <T> T lookup(java.lang.Class<T> service)
T
- any classservice
- the class for which the data were registeredregister(Object, Class)
public <T> void register(T obj, java.lang.Class<T> service)
T
- obj
- an object to be registeredservice
- the key under it should be registeredpublic <T> void deregister(T obj, java.lang.Class<T> service)
T
- arbitray objectobj
- registered objectservice
- the key under which the data was registered@Nonnull public Lookup getUserData()
Copyright © 2003-2019 The KeY-Project.