001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
014: import de.uka.ilkd.key.logic.op.*;
015: import de.uka.ilkd.key.logic.sort.Sort;
016:
017: /**
018: * Term ordering, using the names of symbols; following the script
019: * "Automatisches Beweisen", Bernhard Beckert, Reiner Haehnle
020: */
021: public class NameTermOrdering implements TermOrdering {
022:
023: /**
024: * Compare the two given terms
025: * @return a number negative, zero or a number positive if
026: * <code>p_a</code> is less than, equal, or greater than
027: * <code>p_b</code> regarding the ordering given by the
028: * implementing class
029: */
030: public int compare(Term p_a, Term p_b) {
031: int w = 0;
032:
033: if (p_a.op() == p_b.op()) {
034: // Compare the subterms
035: if (p_a.arity() != 0) {
036: w = compare(p_a.sub(0), p_b.sub(0));
037:
038: if (w == 0)
039: return 0;
040:
041: int i;
042: for (i = 1; i < p_a.arity(); ++i) {
043: if (w * compare(p_a.sub(i), p_b.sub(i)) <= 0)
044: return 0;
045: }
046: }
047: } else {
048: // Test whether any of the operators is a variable
049: if (isVar(p_a) || isVar(p_b))
050: return 0;
051:
052: w = compare(p_a.op(), p_b.op());
053:
054: if (w == 0)
055: return 0;
056:
057: // Compare the free variables of both terms (we are
058: // currently using the existing collector class for
059: // variable depths; this could be implemented more
060: // efficiently)
061: DepthCollector depthsA = new DepthCollector();
062: DepthCollector depthsB = new DepthCollector();
063:
064: p_a.execPostOrder(depthsA);
065: p_b.execPostOrder(depthsB);
066:
067: if (w < 0) {
068: if (compareVars(depthsA, depthsB) >= 0)
069: return 0;
070: } else if (w > 0) {
071: if (compareVars(depthsB, depthsA) >= 0)
072: return 0;
073: }
074: }
075:
076: return w;
077: }
078:
079: /**
080: * Compare the two given symbols
081: * @return a number negative, zero or a number positive if
082: * <code>p_a</code> is less than, equal, or greater than
083: * <code>p_b</code>
084: */
085: private int compare(Operator p_a, Operator p_b) {
086: if (p_a != p_b) {
087: int v = 0;
088: // Search for special symbols
089: {
090: Integer w = getWeight(p_a);
091: if (w == null) {
092: if (getWeight(p_b) != null)
093: return 1;
094: } else {
095: v = w.intValue();
096: w = getWeight(p_b);
097: if (w == null)
098: return -1;
099: else
100: v -= w.intValue();
101: }
102: }
103:
104: if (v != 0)
105: return v;
106:
107: // program variables are greater than other symbols
108: if (p_a instanceof IProgramVariable) {
109: if (!(p_b instanceof IProgramVariable))
110: return 1;
111: } else {
112: if (p_b instanceof IProgramVariable)
113: return -1;
114: }
115:
116: // use the names of the symbols
117: v = p_a.name().toString().compareTo(p_b.name().toString());
118:
119: if (v != 0)
120: return v;
121:
122: // HACK: compare the hash values of the two symbols
123: return sign(p_b.hashCode() - p_a.hashCode());
124: }
125:
126: return 0;
127: }
128:
129: /**
130: * Explicit ordering of some symbols (symbols assigned a weight by
131: * this method are regarded as smaller than other symbols);
132: * symbols are ordered according to their weight
133: */
134: private Integer getWeight(Operator p_op) {
135: if (p_op.name().equals(AbstractIntegerLDT.NUMBERS_NAME))
136: return new Integer(0);
137: if (p_op.name().equals(AbstractIntegerLDT.CHAR_ID_NAME))
138: return new Integer(1);
139: if (p_op instanceof Function
140: && ((Function) p_op).sort() == Sort.NULL)
141: return new Integer(2);
142: if ("TRUE".equals(p_op.name().toString())
143: || "FALSE".equals(p_op.name().toString()))
144: return new Integer(3);
145: if (p_op instanceof SortDependingSymbol)
146: return new Integer(10);
147:
148: return null;
149: }
150:
151: /**
152: * @return true iff <code>p</code> is a variable
153: */
154: private boolean isVar(Term p) {
155: return p.op() instanceof Metavariable
156: || p.op() instanceof QuantifiableVariable;
157: }
158:
159: private int sign(int p) {
160: if (p > 0)
161: return 1;
162: else if (p < 0)
163: return -1;
164: return 0;
165: }
166:
167: /**
168: * @return a negative number, if each variable collected by
169: * <code>p_depthsA</code> has also been collected by
170: * <code>p_depthsB</code>, zero otherwise
171: */
172: private int compareVars(DepthCollector p_depthsA,
173: DepthCollector p_depthsB) {
174: IteratorOfOperator it = p_depthsA.getVariables();
175:
176: while (it.hasNext()) {
177: if (p_depthsB.getMaxDepth(it.next()) == -1)
178: return 0;
179: }
180:
181: return -1;
182: }
183:
184: }
|