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.strategy;
12:
13: import de.uka.ilkd.key.util.Debug;
14:
15: /**
16: * Implementation of the <code>RuleAppCost</code> interface that uses
17: * a <code>long</code> value for the representation of costs, ordered by the
18: * usual ordering of natural numbers. Objects of this class are immutable
19: */
20: public class LongRuleAppCost implements RuleAppCost {
21:
22: public static final LongRuleAppCost ZERO_COST = new LongRuleAppCost(
23: 0);
24:
25: private final long cost;
26:
27: public static RuleAppCost create(long p_cost) {
28: if (p_cost == 0)
29: return ZERO_COST;
30: return new LongRuleAppCost(p_cost);
31: }
32:
33: private LongRuleAppCost(long p_cost) {
34: cost = p_cost;
35: }
36:
37: public int compareTo(Object o) {
38: if (o instanceof TopRuleAppCost)
39: return -1;
40: return compareTo((LongRuleAppCost) o);
41: }
42:
43: public int compareTo(LongRuleAppCost c) {
44: return (cost < c.cost ? -1 : (cost == c.cost ? 0 : 1));
45: }
46:
47: public boolean equals(Object o) {
48: return compareTo(o) == 0;
49: }
50:
51: public int hashCode() {
52: return (int) cost;
53: }
54:
55: public RuleAppCost add(RuleAppCost cost2) {
56: if (cost2 instanceof LongRuleAppCost) {
57: return add((LongRuleAppCost) cost2);
58: } else if (cost2 instanceof TopRuleAppCost) {
59: return TopRuleAppCost.INSTANCE;
60: } else {
61: Debug.fail("Can't add costs of class " + cost2.getClass());
62: // Should not be reached
63: return null;
64: }
65: }
66:
67: public RuleAppCost add(LongRuleAppCost cost2) {
68: if (cost == 0) {
69: return cost2;
70: } else if (cost2.cost == 0) {
71: return this ;
72: } else {
73: return LongRuleAppCost.create(cost + cost2.cost);
74: }
75: }
76:
77: public long getValue() {
78: return cost;
79: }
80:
81: public String toString() {
82: return "Costs " + cost;
83: }
84: }
|