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.logic;
12:
13: import de.uka.ilkd.key.logic.op.IteratorOfOperator;
14: import de.uka.ilkd.key.logic.op.Operator;
15:
16: /**
17: * Term ordering, comparing the maximum depths of terms and contained
18: * variables; following definition 5.14 in the script "Automatisches
19: * Beweisen", Bernhard Beckert, Reiner Haehnle
20: *
21: * This ordering has the possibility to refer to a secundary ordering
22: * upon terms having the same depths (i.e. both the same maximal depth
23: * and maximal variable depths); this guarantees substitutions to stay
24: * monotonic
25: */
26: public class CascadeDepthTermOrdering extends DepthTermOrdering {
27:
28: /**
29: * secundary ordering
30: */
31: private TermOrdering orderingB;
32:
33: public CascadeDepthTermOrdering(TermOrdering p_orderingB) {
34: orderingB = p_orderingB;
35: }
36:
37: /**
38: * Compare the two given terms
39: * @return a number negative, zero or a number positive if
40: * <code>p_a</code> is less than, equal, or greater than
41: * <code>p_b</code> regarding the ordering given by the
42: * implementing class
43: */
44: public int compare(Term p_a, Term p_b) {
45: DepthCollector depthsA = new DepthCollector();
46: DepthCollector depthsB = new DepthCollector();
47:
48: p_a.execPostOrder(depthsA);
49: p_b.execPostOrder(depthsB);
50:
51: if (depthsA.getMaxDepth() < depthsB.getMaxDepth())
52: return compareVars(depthsA, depthsB);
53: else if (depthsB.getMaxDepth() < depthsA.getMaxDepth())
54: return -compareVars(depthsB, depthsA);
55: else if (equalVars(depthsA, depthsB))
56: return orderingB.compare(p_a, p_b);
57: return 0;
58: }
59:
60: /**
61: * @return true, iff each variable collected by
62: * <code>p_depthsA</code> has also been collected by
63: * <code>p_depthsB</code> with the same maximum depth
64: */
65: private boolean equalVars(DepthCollector p_depthsA,
66: DepthCollector p_depthsB) {
67: return equalVarsHelp(p_depthsA, p_depthsB)
68: && equalVarsHelp(p_depthsB, p_depthsA);
69: }
70:
71: private boolean equalVarsHelp(DepthCollector p_depthsA,
72: DepthCollector p_depthsB) {
73: IteratorOfOperator it = p_depthsA.getVariables();
74: Operator var;
75:
76: while (it.hasNext()) {
77: var = it.next();
78:
79: if (p_depthsA.getMaxDepth(var) != p_depthsB
80: .getMaxDepth(var))
81: return false;
82: }
83:
84: return true;
85: }
86:
87: }
|