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 java.math.BigInteger;
014: import java.util.HashMap;
015: import java.util.HashSet;
016: import java.util.Set;
017: import java.util.WeakHashMap;
018:
019: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
020: import de.uka.ilkd.key.logic.op.*;
021: import de.uka.ilkd.key.logic.sort.IteratorOfSort;
022: import de.uka.ilkd.key.logic.sort.ObjectSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024:
025: /**
026: *
027: */
028: public class LexPathOrdering implements TermOrdering {
029:
030: public int compare(Term p_a, Term p_b) {
031: final CompRes res = compareHelp(p_a, p_b);
032: if (res.lt())
033: return -1;
034: else if (res.gt())
035: return 1;
036: else
037: return 0;
038: }
039:
040: private abstract static class CompRes {
041: public boolean uncomparable() {
042: return false;
043: }
044:
045: public boolean eq() {
046: return false;
047: }
048:
049: public boolean gt() {
050: return false;
051: }
052:
053: public boolean lt() {
054: return false;
055: }
056:
057: public boolean geq() {
058: return gt() || eq();
059: }
060:
061: public boolean leq() {
062: return lt() || eq();
063: }
064: }
065:
066: private final static CompRes UNCOMPARABLE = new CompRes() {
067: public boolean uncomparable() {
068: return true;
069: }
070: };
071: private final static CompRes EQUALS = new CompRes() {
072: public boolean eq() {
073: return true;
074: }
075: };
076: private final static CompRes GREATER = new CompRes() {
077: public boolean gt() {
078: return true;
079: }
080: };
081: private final static CompRes LESS = new CompRes() {
082: public boolean lt() {
083: return true;
084: }
085: };
086:
087: private final static class CacheKey {
088: public final Term left;
089: public final Term right;
090:
091: public CacheKey(final Term left, final Term right) {
092: this .left = left;
093: this .right = right;
094: }
095:
096: public boolean equals(Object arg0) {
097: if (!(arg0 instanceof CacheKey))
098: return false;
099: final CacheKey key0 = (CacheKey) arg0;
100: return left.equals(key0.left) && right.equals(key0.right);
101: }
102:
103: public int hashCode() {
104: return left.hashCode() + 2 * right.hashCode();
105: }
106: }
107:
108: private final HashMap cache = new HashMap();
109:
110: private CompRes compareHelp(Term p_a, Term p_b) {
111: final CacheKey key = new CacheKey(p_a, p_b);
112: CompRes res = (CompRes) cache.get(key);
113: if (res == null) {
114: res = compareHelp2(p_a, p_b);
115: if (cache.size() > 100000)
116: cache.clear();
117: cache.put(key, res);
118: }
119: return res;
120: }
121:
122: private CompRes compareHelp2(Term p_a, Term p_b) {
123:
124: if (oneSubGeq(p_a, p_b))
125: return GREATER;
126: if (oneSubGeq(p_b, p_a))
127: return LESS;
128:
129: final int opComp = compare(p_a.op(), p_a.sort(), p_b.op(), p_b
130: .sort());
131: if (opComp == 0) {
132: final CompRes lexComp = compareSubsLex(p_a, p_b);
133: if (lexComp.eq()) {
134: return EQUALS;
135: } else if (lexComp.gt()) {
136: if (greaterThanSubs(p_a, p_b, 1))
137: return GREATER;
138: } else if (lexComp.lt()) {
139: if (greaterThanSubs(p_b, p_a, 1))
140: return LESS;
141: }
142: }
143:
144: if (opComp > 0) {
145: if (greaterThanSubs(p_a, p_b, 0))
146: return GREATER;
147: } else {
148: if (greaterThanSubs(p_b, p_a, 0))
149: return LESS;
150: }
151:
152: return UNCOMPARABLE;
153: }
154:
155: private CompRes compareSubsLex(Term p_a, Term p_b) {
156: int i = 0;
157:
158: while (true) {
159: if (i >= p_a.arity()) {
160: if (i >= p_b.arity())
161: return EQUALS;
162: else
163: return LESS;
164: }
165:
166: if (i >= p_b.arity())
167: return GREATER;
168:
169: final CompRes subRes = compareHelp(p_a.sub(i), p_b.sub(i));
170: if (!subRes.eq())
171: return subRes;
172:
173: ++i;
174: }
175: }
176:
177: private boolean greaterThanSubs(Term p_a, Term p_b, int firstSub) {
178: for (int i = firstSub; i < p_b.arity(); ++i) {
179: if (!compareHelp(p_a, p_b.sub(i)).gt())
180: return false;
181: }
182: return true;
183: }
184:
185: private boolean oneSubGeq(Term p_a, Term p_b) {
186: for (int i = 0; i != p_a.arity(); ++i) {
187: if (compareHelp(p_a.sub(i), p_b).geq())
188: return true;
189: }
190: return false;
191: }
192:
193: /**
194: * Compare the two given symbols
195: *
196: * @return a number negative, zero or a number positive if <code>p_a</code>
197: * is less than, equal, or greater than <code>p_b</code>
198: */
199: private int compare(Operator aOp, Sort aSort, Operator bOp,
200: Sort bSort) {
201: if (aOp == bOp)
202: return 0;
203:
204: // Search for literals
205: int v = literalWeighter.compareWeights(aOp, bOp);
206: if (v != 0)
207: return v;
208:
209: if (isVar(aOp)) {
210: if (!isVar(bOp))
211: return 1;
212: } else {
213: if (isVar(bOp))
214: return -1;
215: }
216:
217: // compare the sorts of the symbols: more specific sorts are smaller
218: v = getSortDepth(bSort) - getSortDepth(aSort);
219: if (v != 0)
220: return v;
221:
222: // Search for special function symbols
223: v = functionWeighter.compareWeights(aOp, bOp);
224: if (v != 0)
225: return v;
226:
227: // smaller arity is smaller
228: v = aOp.arity() - bOp.arity();
229: if (v != 0)
230: return v;
231:
232: // use the names of the symbols
233: v = aOp.name().compareTo(bOp.name());
234: if (v != 0)
235: return v;
236:
237: // HACK: compare the hash values of the two symbols
238: return sign(bOp.hashCode() - aOp.hashCode());
239: }
240:
241: /**
242: * Hashmap from <code>Sort</code> to <code>Integer</code>, storing the
243: * lengths of maximal paths from a sort to the top element of the sort
244: * lattice.
245: */
246: private final WeakHashMap sortDepthCache = new WeakHashMap();
247:
248: /**
249: * @return the length of the longest path from <code>s</code> to the top
250: * element of the sort lattice. Probably this length is not computed
251: * correctly here, because the representation of sorts in key is
252: * completely messed up, but you get the idea
253: */
254: private int getSortDepth(Sort s) {
255: Integer res = (Integer) sortDepthCache.get(s);
256: if (res == null) {
257: res = new Integer(getSortDepthHelp(s));
258: sortDepthCache.put(s, res);
259: }
260: return res.intValue();
261: }
262:
263: private int getSortDepthHelp(Sort s) {
264: int res = -1;
265:
266: // HACKish: ensure that object sorts are bigger than primitive sorts
267: final String sName = s.name().toString();
268: if ("int".equals(sName))
269: res = 10000;
270: if ("boolean".equals(sName))
271: res = 20000;
272:
273: final IteratorOfSort it = s.extendsSorts().iterator();
274: while (it.hasNext())
275: res = Math.max(res, getSortDepth(it.next()));
276:
277: return res + 1;
278: }
279:
280: ////////////////////////////////////////////////////////////////////////////
281:
282: /**
283: * Base class for metrics on symbols that are used to construct an ordering
284: */
285: private static abstract class Weighter {
286:
287: /**
288: * Compare the weights of two symbols using the function
289: * <code>getWeight</code>.
290: *
291: * @return a number negative, zero or a number positive if the weight of
292: * <code>p_a</code> is less than, equal, or greater than the
293: * weight of <code>p_b</code>
294: */
295: public int compareWeights(Operator p_a, Operator p_b) {
296: final Integer aWeight = getWeight(p_a);
297: final Integer bWeight = getWeight(p_b);
298:
299: if (aWeight == null) {
300: if (bWeight == null)
301: return 0;
302: else
303: return 1;
304: } else {
305: if (bWeight == null)
306: return -1;
307: else
308: return aWeight.intValue() - bWeight.intValue();
309: }
310: }
311:
312: protected abstract Integer getWeight(Operator p_op);
313: }
314:
315: /**
316: * Explicit ordering of literals (symbols assigned a weight by this
317: * class are regarded as smaller than all other symbols)
318: */
319: private static class LiteralWeighter extends Weighter {
320:
321: private final Set intFunctionNames = new HashSet();
322: {
323: intFunctionNames.add("#");
324: intFunctionNames.add("0");
325: intFunctionNames.add("1");
326: intFunctionNames.add("2");
327: intFunctionNames.add("3");
328: intFunctionNames.add("4");
329: intFunctionNames.add("5");
330: intFunctionNames.add("6");
331: intFunctionNames.add("7");
332: intFunctionNames.add("8");
333: intFunctionNames.add("9");
334: intFunctionNames.add("Z");
335: intFunctionNames.add("neglit");
336: }
337:
338: protected Integer getWeight(Operator p_op) {
339: final String opStr = p_op.name().toString();
340:
341: if (intFunctionNames.contains(opStr))
342: return new Integer(0);
343:
344: if (opStr.equals("neg"))
345: return new Integer(1);
346: if (p_op.name().equals(AbstractIntegerLDT.CHAR_ID_NAME))
347: return new Integer(1);
348: if (p_op instanceof Function
349: && ((Function) p_op).sort() == Sort.NULL)
350: return new Integer(2);
351: if (p_op instanceof Function
352: && (opStr.equals("TRUE") | opStr.equals("FALSE")))
353: return new Integer(3);
354:
355: if (opStr.equals("add"))
356: return new Integer(6);
357: if (opStr.equals("mul"))
358: return new Integer(7);
359: if (opStr.equals("div"))
360: return new Integer(8);
361: if (opStr.equals("jdiv"))
362: return new Integer(9);
363:
364: return null;
365: }
366: }
367:
368: /**
369: * Explicit ordering for different kinds of function symbols; symbols like
370: * C::<get> or C.<nextToCreate> should be smaller than other symbols
371: */
372: private static class FunctionWeighter extends Weighter {
373: protected Integer getWeight(Operator p_op) {
374: final String opStr = p_op.name().toString();
375:
376: if (opStr.endsWith("::<get>"))
377: return new Integer(10);
378: if (opStr.endsWith("<nextToCreate>"))
379: return new Integer(20);
380:
381: /* if ( p_op instanceof SortDependingSymbol ) return new Integer ( 10 );
382:
383: if ( p_op instanceof AttributeOp ) return new Integer ( 20 );
384:
385: if ( p_op instanceof ProgramVariable ) {
386: final ProgramVariable var = (ProgramVariable)p_op;
387: if ( var.isStatic () ) return new Integer ( 30 );
388: if ( var.isMember () ) return new Integer ( 31 );
389: return new Integer ( 32 );
390: } */
391:
392: return null;
393: }
394: }
395:
396: private final Weighter literalWeighter = new LiteralWeighter();
397: private final Weighter functionWeighter = new FunctionWeighter();
398:
399: ////////////////////////////////////////////////////////////////////////////
400:
401: /**
402: * @return true iff <code>op</code> is a logic variable
403: */
404: private boolean isVar(Operator op) {
405: return op instanceof Metavariable
406: || op instanceof QuantifiableVariable;
407: }
408:
409: private int sign(int p) {
410: if (p > 0)
411: return 1;
412: else if (p < 0)
413: return -1;
414: return 0;
415: }
416:
417: /**
418: * TODO: this should also be used when comparing terms
419: *
420: * The reduction ordering on integers that is described in "A
421: * critical-pair/completion algorithm for finitely generated ideals in
422: * rings", with the difference that positive numbers are here considered as
423: * smaller than negative numbers (with the same absolute value)
424: *
425: * @return a negative number, zero, or a positive number, if <code>a</code>
426: * is smaller, equal to or greater than <code>b</code>
427: */
428: public static int compare(BigInteger a, BigInteger b) {
429: final int c = a.abs().compareTo(b.abs());
430: if (c != 0)
431: return c;
432: return b.signum() - a.signum();
433: }
434:
435: /**
436: * @return the result of dividing <code>a</code> by <code>c</code>,
437: * such that the remainder becomes minimal in the reduction ordering
438: * <code>LexPathOrdering.compare</code> on integers
439: */
440: public static BigInteger divide(BigInteger a, BigInteger c) {
441: final BigInteger[] divRem = a.divideAndRemainder(c);
442: while (true) {
443: // could be done more efficiently. but apparently the rounding
444: // behaviour of BigInteger.divide for negative numbers is not
445: // properly specified. or everything becomes very tedious ...
446:
447: final BigInteger newRem1 = divRem[1].subtract(c);
448: if (compare(newRem1, divRem[1]) < 0) {
449: divRem[0] = divRem[0].add(BigInteger.ONE);
450: divRem[1] = newRem1;
451: continue;
452: }
453: final BigInteger newRem2 = divRem[1].add(c);
454: if (compare(newRem2, divRem[1]) < 0) {
455: divRem[0] = divRem[0].subtract(BigInteger.ONE);
456: divRem[1] = newRem2;
457: continue;
458: }
459:
460: return divRem[0];
461: }
462: }
463: }
|