de.uka.ilkd.key.proof.proofevent

Class RuleAppInfo

java.lang.Object

de.uka.ilkd.key.proof.proofevent.RuleAppInfo

public class RuleAppInfo
extends java.lang.Object

More specific information about a rule application (currently information about added and removed formulas)

Field Summary

Fields

Modifier and Type	Field and Description
(package private) RuleApp	app RuleApp this event reports
(package private) ImmutableList<NodeReplacement>	newNodes New nodes that have been introduced by this rule application
(package private) Node	originalNode Node the rule has been applied on

Constructor Summary

Constructors

Constructor and Description
RuleAppInfo(RuleApp p_appliedRule, Node p_originalNode, ImmutableList<NodeReplacement> p_newNodes)

Method Summary

Modifier and Type	Method and Description
Node	getOriginalNode()
java.util.Iterator<NodeReplacement>	getReplacementNodes()
RuleApp	getRuleApp()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

app

RuleApp app

RuleApp this event reports

originalNode

Node originalNode

Node the rule has been applied on

newNodes

ImmutableList<NodeReplacement> newNodes

New nodes that have been introduced by this rule application

Constructor Detail

RuleAppInfo

RuleAppInfo(RuleApp p_appliedRule,
            Node p_originalNode,
            ImmutableList<NodeReplacement> p_newNodes)

Method Detail

getRuleApp

public RuleApp getRuleApp()

getOriginalNode

public Node getOriginalNode()

Returns:

Node the rule has been applied on

getReplacementNodes

public java.util.Iterator<NodeReplacement> getReplacementNodes()

Returns:

Nodes by which the original one has been replaced (the original node, if only the closure constraint of this node has been changed)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object