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: /**
14: * Combine two term orderings: if two terms are unrelated, regarding
15: * ordering <code>orderingA</code>, then <code>orderingB</code> is
16: * used (nb: this will usually NOT result in an ordering, for which *
17: * substitutions are monotonic)
18: */
19: public class CascadeTermOrdering implements TermOrdering {
20:
21: private TermOrdering orderingA;
22: private TermOrdering orderingB;
23:
24: public CascadeTermOrdering(TermOrdering p_orderingA,
25: TermOrdering p_orderingB) {
26: orderingA = p_orderingA;
27: orderingB = p_orderingB;
28: }
29:
30: /**
31: * Compare the two given terms
32: * @return a number negative, zero or a number positive if
33: * <code>p_a</code> is less than, equal, or greater than
34: * <code>p_b</code> regarding the ordering given by the
35: * implementing class
36: */
37: public int compare(Term p_a, Term p_b) {
38: int w = orderingA.compare(p_a, p_b);
39:
40: if (w == 0)
41: return orderingB.compare(p_a, p_b);
42:
43: return w;
44: }
45:
46: }
|