public class Node
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private RuleApp |
appliedRuleApp |
private java.lang.String |
cachedName |
private java.util.ArrayList<Node> |
children |
private boolean |
closed |
private static java.lang.String |
CLOSED_GOAL |
private static java.lang.String |
INTERACTIVE_GOAL |
private static java.lang.String |
LINKED_GOAL |
private ImmutableList<Function> |
localFunctions
a linked list of the locally generated function symbols.
|
private ImmutableSet<NoPosTacletApp> |
localIntroducedRules
If the rule base has been extended e.g. by loading a new taclet as
lemma or by applying a taclet with an addrule section on this node,
then these taclets are stored in this list
|
private ImmutableList<IProgramVariable> |
localProgVars
a linked list of the locally generated program variables.
|
private NameRecorder |
nameRecorder |
private NodeInfo |
nodeInfo
contains non-logical content, used for user feedback
|
private static java.lang.String |
NODES |
private static java.lang.String |
OPEN_GOAL |
(package private) Node |
parent |
private Proof |
proof
the proof the node belongs to
|
private ImmutableList<RenamingTable> |
renamings |
private static java.lang.String |
RULE_APPLICATION_WITHOUT_RULE |
private static java.lang.String |
RULE_WITHOUT_NAME |
private Sequent |
seq |
private int |
serialNr |
private int |
siblingNr |
private java.util.List<StrategyInfoUndoMethod> |
undoInfoForStrategyInfo
Holds the undo methods for the information added by rules to the
Goal.strategyInfos . |
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 child)
makes the given node a child of this node.
|
void |
addAll(Node[] newChildren)
makes the given node a child 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)
returns i-th child
|
int |
childrenCount()
returns number of children
|
java.util.Iterator<Node> |
childrenIterator()
returns an iterator for the direct children of this node.
|
void |
clearNameCache() |
(package private) void |
clearNodeInfo()
When pruning, data referring to future nodes has to be cleared;
however, the sequent change info is related to the parent node,
it has to be preserved.
|
(package private) Node |
close()
marks a node as closed
|
Node |
commonAncestor(Node p_node)
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 |
int |
countBranches()
retrieves number of branches
|
int |
countNodes()
retrieves number of nodes
|
boolean |
find(Node node)
searches for a given node in the subtree starting with this node
|
RuleApp |
getAppliedRuleApp() |
int |
getChildNr(Node p_node) |
(package private) java.util.List<Node> |
getLeaves()
computes the leaves of the current subtree and returns them
|
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() |
private boolean |
isCloseable()
checks if an inner node is closeable
|
boolean |
isClosed() |
java.util.Iterator<Node> |
iterator()
Iterator over children.
|
boolean |
leaf()
returns true, iff this node is a leaf, i.e. has no children.
|
java.util.Iterator<Node> |
leavesIterator()
returns an iterator for the leaves of the subtree below this
node.
|
java.lang.String |
name() |
Node |
parent()
returns the parent node of this node.
|
Proof |
proof()
returns the proof the Node belongs to
|
(package private) void |
remove()
removes child/parent relationship between this node and its
parent; if this node is root nothing happens.
|
(package private) boolean |
remove(Node child)
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.
|
(package private) void |
reopen()
Opens a previously closed node and all its closed
parents.
|
boolean |
root()
returns true, iff this node is root, i.e. has no parents.
|
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()
returns an iterator for all nodes in the subtree.
|
java.lang.String |
toString() |
private java.lang.StringBuffer |
toString(java.lang.String prefix,
java.lang.StringBuffer tree,
java.lang.String preEnumeration,
int postNr,
int maxNr,
int ownNr)
helps toString method
|
private static final java.lang.String RULE_WITHOUT_NAME
private static final java.lang.String RULE_APPLICATION_WITHOUT_RULE
private static final java.lang.String INTERACTIVE_GOAL
private static final java.lang.String LINKED_GOAL
private static final java.lang.String OPEN_GOAL
private static final java.lang.String CLOSED_GOAL
private static final java.lang.String NODES
private final Proof proof
private Sequent seq
private final java.util.ArrayList<Node> children
Node parent
private RuleApp appliedRuleApp
private NameRecorder nameRecorder
private ImmutableList<IProgramVariable> localProgVars
private ImmutableList<Function> localFunctions
private boolean closed
private NodeInfo nodeInfo
private final int serialNr
private int siblingNr
private ImmutableList<RenamingTable> renamings
private java.lang.String cachedName
private ImmutableSet<NoPosTacletApp> localIntroducedRules
private final java.util.List<StrategyInfoUndoMethod> undoInfoForStrategyInfo
Goal.strategyInfos
.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()
void clearNodeInfo()
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)
public Node parent()
public boolean leaf()
public boolean find(Node node)
public Node commonAncestor(Node p_node)
this
and p_node
; we assume
that the two nodes are part of the same proof treepublic boolean root()
public Statistics statistics()
public void add(Node child)
public void addAll(Node[] newChildren)
void remove()
boolean remove(Node child)
java.util.List<Node> getLeaves()
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)
public int getChildNr(Node p_node)
p_node
, if it is a
child of this node (starting with 0
),
-1
otherwisepublic java.lang.StringBuffer getUniqueTacletId()
private java.lang.StringBuffer toString(java.lang.String prefix, java.lang.StringBuffer tree, java.lang.String preEnumeration, int postNr, int maxNr, int ownNr)
prefix
- needed to keep track if a line has to be printedtree
- the tree representation we want to add this subtree
" @param preEnumeration the enumeration of the parent without the
last numberpostNr
- the last number of the parents enumerationmaxNr
- the number of nodes at this levelownNr
- the place of this node at this levelpublic java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String name()
public boolean sanityCheckDoubleLinks()
Node close()
void reopen()
This is, for instance, needed for the MergeRule
: In
a situation where a merge node and its associated partners
have been closed and the merge node is then pruned away,
the partners have to be reopened again. Otherwise, we
have a soundness issue.
private boolean isCloseable()
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.