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;
12:
13: import java.util.Stack;
14:
15: /** Proof-specific counter object: taclet names, var names, node numbers, &c */
16: public class Counter {
17:
18: private String name;
19: private int count;
20:
21: private Stack undoAnchors = new Stack();
22:
23: public Counter(String name) {
24: this .name = name;
25: }
26:
27: public int getCount() {
28: return count;
29: }
30:
31: public int getCountPlusPlus(Node undoAnchor) {
32: undoAnchors.push(new NodeAnchor(undoAnchor));
33: return count++;
34: }
35:
36: public int getCountPlusPlusWithParent(Node undoAnchor) {
37: undoAnchors.push(new NodeAnchor(undoAnchor, true));
38: return count++;
39: }
40:
41: public void undo(Node node) {
42: if (undoAnchors.size() == 0) {
43: de.uka.ilkd.key.util.Debug.assertTrue(count == 0,
44: "No undoAnchor, count should be 0");
45: return;
46: }
47: NodeAnchor anchor = (NodeAnchor) undoAnchors.peek();
48: if ((!anchor.anchorIsParent() && anchor.node() == node)
49: || (anchor.anchorIsParent() && anchor.node() == node
50: .parent())) {
51: undoAnchors.pop();
52: count--;
53: }
54: }
55:
56: public String toString() {
57: return "Counter " + name + ": " + count;
58: }
59:
60: private static class NodeAnchor {
61: Node node;
62: boolean anchorIsParent = false;
63:
64: NodeAnchor(Node n) {
65: node = n;
66: }
67:
68: NodeAnchor(Node n, boolean anchorIsChild) {
69: node = n;
70: this .anchorIsParent = anchorIsChild;
71: }
72:
73: Node node() {
74: return node;
75: }
76:
77: boolean anchorIsParent() {
78: return anchorIsParent;
79: }
80: }
81:
82: }
|