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: public class DepthTermOrdering implements TermOrdering {
22:
23: /**
24: * Compare the two given terms
25: * @return a number negative, zero or a number positive if
26: * <code>p_a</code> is less than, equal, or greater than
27: * <code>p_b</code> regarding the ordering given by the
28: * implementing class
29: */
30: public int compare(Term p_a, Term p_b) {
31: DepthCollector depthsA = new DepthCollector();
32: DepthCollector depthsB = new DepthCollector();
33:
34: p_a.execPostOrder(depthsA);
35: p_b.execPostOrder(depthsB);
36:
37: if (depthsA.getMaxDepth() < depthsB.getMaxDepth())
38: return compareVars(depthsA, depthsB);
39: else if (depthsB.getMaxDepth() < depthsA.getMaxDepth())
40: return -compareVars(depthsB, depthsA);
41: else
42: return 0;
43: }
44:
45: /**
46: * @return a negative number, if each variable collected by
47: * <code>p_depthsA</code> has also been collected by
48: * <code>p_depthsB</code>, and <code>p_depthsB</code> has also
49: * found a greater maximum depth for that variable; zero otherwise
50: */
51: protected int compareVars(DepthCollector p_depthsA,
52: DepthCollector p_depthsB) {
53: IteratorOfOperator it = p_depthsA.getVariables();
54: Operator var;
55: int depthB;
56:
57: while (it.hasNext()) {
58: var = it.next();
59: depthB = p_depthsB.getMaxDepth(var);
60:
61: if (depthB == -1 || depthB <= p_depthsA.getMaxDepth(var))
62: return 0;
63: }
64:
65: return -1;
66: }
67:
68: }
|