01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof.proofevent;
12:
13: import de.uka.ilkd.key.proof.Node;
14: import de.uka.ilkd.key.rule.RuleApp;
15:
16: /**
17: * More specific information about a rule application (currently
18: * information about added and removed formulas)
19: */
20: public class RuleAppInfo {
21:
22: RuleAppInfo(RuleApp p_appliedRule, Node p_originalNode,
23: ListOfNodeReplacement p_newNodes) {
24: app = p_appliedRule;
25: originalNode = p_originalNode;
26: newNodes = p_newNodes;
27: }
28:
29: /**
30: * RuleApp this event reports
31: */
32: RuleApp app = null;
33:
34: /**
35: * Node the rule has been applied on
36: */
37: Node originalNode = null;
38:
39: /**
40: * New nodes that have been introduced by this rule application
41: */
42: ListOfNodeReplacement newNodes = null;
43:
44: public RuleApp getRuleApp() {
45: return app;
46: }
47:
48: /**
49: * @return Node the rule has been applied on
50: */
51: public Node getOriginalNode() {
52: return originalNode;
53: }
54:
55: /**
56: * @return Nodes by which the original one has been replaced (the
57: * original node, if only the closure constraint of this node has
58: * been changed)
59: */
60: public IteratorOfNodeReplacement getReplacementNodes() {
61: return newNodes.iterator();
62: }
63:
64: public String toString() {
65: return "RuleApp: " + getRuleApp() + "\nNode: "
66: + getOriginalNode() + "\nResulting nodes: " + newNodes;
67: }
68: }
|