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: package de.uka.ilkd.key.unittest;
009:
010: import de.uka.ilkd.key.logic.*;
011: import de.uka.ilkd.key.logic.op.*;
012: import de.uka.ilkd.key.logic.sort.Sort;
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.expression.literal.*;
015: import de.uka.ilkd.key.java.expression.operator.*;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017:
018: import java.util.*;
019:
020: public class EquivalenceClass {
021:
022: private SetOfTerm members;
023: private HashMap lb2ex, ub2ex;
024: // This flag is used to avoid cycles, when it is checked if a concrete
025: // value for this equivalence class is already determined by a given
026: // partial model.
027: private boolean visited = false;
028: // contains the set of terms whose value is not equal to the value
029: // of the terms in this class.
030: private SetOfTerm disjointRep = SetAsListOfTerm.EMPTY_SET;
031: private Boolean bValue = null;
032: private Integer iValue = null;
033: private Term trueLit, falseLit;
034: private Services serv;
035: private static Boolean boolTrue = Model.boolTrue;
036: private static Boolean boolFalse = Model.boolFalse;
037: private static Term nullTerm = TermFactory.DEFAULT
038: .createFunctionTerm(Op.NULL);
039:
040: public EquivalenceClass(SetOfTerm members, Services serv) {
041: this .members = members;
042: lb2ex = new HashMap();
043: ub2ex = new HashMap();
044: this .serv = serv;
045: trueLit = serv.getTypeConverter().convertToLogicElement(
046: BooleanLiteral.TRUE);
047: falseLit = serv.getTypeConverter().convertToLogicElement(
048: BooleanLiteral.FALSE);
049: }
050:
051: public EquivalenceClass(Term t1, Term t2, Services serv) {
052: this (SetAsListOfTerm.EMPTY_SET.add(t1).add(t2), serv);
053: }
054:
055: public EquivalenceClass(Term t, Services serv) {
056: this (SetAsListOfTerm.EMPTY_SET.add(t), serv);
057: }
058:
059: private boolean isInt(Sort s) {
060: return s.extendsTrans(serv.getTypeConverter().getIntegerLDT()
061: .targetSort());
062: }
063:
064: public boolean isInt() {
065: for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
066: Term t = it.next();
067: return isInt(t.sort());
068: }
069: return false;
070: }
071:
072: public KeYJavaType getKeYJavaType() {
073: IteratorOfTerm it = members.iterator();
074: Sort s = it.next().sort();
075: while (it.hasNext()) {
076: Sort s1 = it.next().sort();
077: if (s1.extendsTrans(s)) {
078: s = s1;
079: }
080: }
081: KeYJavaType result = serv.getJavaInfo().getKeYJavaType(s);
082: if (result == null && isInt(s)) {
083: result = serv.getJavaInfo().getKeYJavaType(
084: serv.getTypeConverter().getIntLDT().targetSort());
085: }
086: return result;
087: }
088:
089: public boolean isBoolean() {
090: for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
091: if (serv.getTypeConverter().getBooleanLDT().targetSort() == it
092: .next().sort()) {
093: return true;
094: }
095: }
096: return false;
097: }
098:
099: /**
100: * Returns the locations that are members of this equivalence class.
101: */
102: public SetOfTerm getLocations() {
103: SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
104: IteratorOfTerm it = members.iterator();
105: while (it.hasNext()) {
106: Term t = it.next();
107: if (ModelGenerator.isLocation(t, serv)) {
108: locations = locations.add(t);
109: }
110: }
111: return locations;
112: }
113:
114: public int hashCode() {
115: int result = 0;
116: IteratorOfTerm it = members.iterator();
117: while (it.hasNext()) {
118: result += it.next().toString().hashCode();
119: }
120: return result;
121: }
122:
123: public boolean equals(Object o) {
124: if (!(o instanceof EquivalenceClass)) {
125: return false;
126: }
127: EquivalenceClass eqc = (EquivalenceClass) o;
128: if (eqc.members.size() != members.size()) {
129: return false;
130: }
131: IteratorOfTerm it = members.iterator();
132: l: while (it.hasNext()) {
133: IteratorOfTerm it2 = eqc.members.iterator();
134: Term t = it.next();
135: while (it2.hasNext()) {
136: if (t.toString().equals(it2.next().toString())) {
137: continue l;
138: }
139: }
140: return false;
141: }
142: return true;
143: }
144:
145: public boolean hasConcreteValue(HashMap term2class) {
146: if (isInt())
147: return getConcreteIntValue(term2class) != null;
148: if (isBoolean())
149: return getConcreteBooleanValue(term2class) != null;
150: return false;
151: }
152:
153: /**
154: * Assigns a concrete integer value to this equivalence class. Used for
155: * model generation.
156: */
157: public boolean setInteger(int i) {
158: if (containsLiteral()) {
159: return false;
160: }
161: iValue = new Integer(i);
162: return true;
163: }
164:
165: /**
166: * Assigns a concrete boolean value to this equivalence class. Used for
167: * model generation.
168: */
169: public boolean setBoolean(boolean b) {
170: if (containsLiteral()) {
171: return false;
172: }
173: bValue = bool(b);
174: return true;
175: }
176:
177: public boolean resetValue() {
178: if (containsLiteral()) {
179: return false;
180: }
181: bValue = null;
182: iValue = null;
183: return true;
184: }
185:
186: /**
187: * returns true iff a term t=null was found in the antecedent of the
188: * underlying sequence for a member t of this class.
189: */
190: public boolean isNull() {
191: return members.contains(nullTerm);
192: }
193:
194: /**
195: * returns true iff a term t=null was found in the succecedent of the
196: * underlying sequence for a member t of this class.
197: */
198: public boolean isNotNull(HashMap term2class) {
199: IteratorOfTerm it = disjointRep.iterator();
200: while (it.hasNext()) {
201: Term d = it.next();
202: if (((EquivalenceClass) term2class.get(d)).isNull()) {
203: return true;
204: }
205: }
206: return false;
207: }
208:
209: public SetOfTerm getMembers() {
210: return members;
211: }
212:
213: public void add(Term t) {
214: members = members.add(t);
215: }
216:
217: public void add(EquivalenceClass ec) {
218: members = members.union(ec.getMembers());
219: }
220:
221: public boolean contains(Term t) {
222: return members.contains(t);
223: }
224:
225: public void addDisjoint(Term t) {
226: disjointRep = disjointRep.add(t);
227: }
228:
229: public SetOfTerm getDisjoints() {
230: return disjointRep;
231: }
232:
233: /**
234: * Only for classes of sort int.
235: * Adds the lower bound <code>bound</code> to the set of lower bounds of
236: * this EquivalenceClass. Iff it can be derived from the known bounds
237: * of this class that <code>bound</code> and <code>this</code> denote
238: * identical equivalence classes the members of <code>bound</code> are
239: * to this class and true is returned.
240: */
241: public boolean addLowerBound(EquivalenceClass bound, boolean ex) {
242: if (bound == this || !isInt())
243: return false;
244: if (ub2ex.containsKey(bound)) {
245: if (ex || ((Boolean) ub2ex.get(bound)).booleanValue()) {
246: throw new ModelGenerationFailureException(
247: "Unsatisfiable bound constraints for "
248: + members);
249: } else {
250: lb2ex.remove(bound);
251: ub2ex.remove(bound);
252: add(bound);
253: return true;
254: }
255: }
256: if (lb2ex.containsKey(bound)
257: && ((Boolean) lb2ex.get(bound)).booleanValue()
258: || !lb2ex.containsKey(bound)) {
259: lb2ex.put(bound, bool(ex));
260: }
261: return false;
262: }
263:
264: private Boolean bool(boolean b) {
265: return b ? boolTrue : boolFalse;
266: }
267:
268: /**
269: * Only for classes of sort int.
270: * Adds the upper bound <code>bound</code> to the set of upper bounds of
271: * this EquivalenceClass. Iff it can be derived from the known bounds
272: * of this class that <code>bound</code> and <code>this</code> denote
273: * identical equivalence classes the members of <code>bound</code> are
274: * to this class and true is returned.
275: */
276: public boolean addUpperBound(EquivalenceClass bound, boolean ex) {
277: if (bound == this )
278: return false;
279: if (lb2ex.containsKey(bound)) {
280: if (ex || ((Boolean) lb2ex.get(bound)).booleanValue()) {
281: throw new ModelGenerationFailureException(
282: "Unsatisfiable bound constraints for "
283: + members);
284: } else {
285: lb2ex.remove(bound);
286: ub2ex.remove(bound);
287: add(bound);
288: return true;
289: }
290: }
291: if (ex || !ub2ex.containsKey(bound)) {
292: ub2ex.put(bound, bool(ex));
293: }
294: return false;
295: }
296:
297: public int getMinimalConcreteUpperBound(HashMap term2class) {
298: Iterator it = ub2ex.keySet().iterator();
299: int min = Integer.MAX_VALUE;
300: while (it.hasNext()) {
301: EquivalenceClass ec = (EquivalenceClass) it.next();
302: int current;
303: Integer v = ec.getConcreteIntValue(term2class);
304: if (v == null) {
305: current = ec.getMinimalConcreteUpperBound(term2class);
306: } else {
307: current = v.intValue();
308: }
309: Boolean ex = (Boolean) ub2ex.get(ec);
310: if (ex != null && ex.booleanValue()) {
311: current--;
312: }
313: if (current < min) {
314: min = current;
315: }
316: }
317: return min;
318: }
319:
320: public int getMaximalConcreteLowerBound(HashMap term2class) {
321: Iterator it = lb2ex.keySet().iterator();
322: int max = Integer.MIN_VALUE;
323: while (it.hasNext()) {
324: EquivalenceClass ec = (EquivalenceClass) it.next();
325: int current;
326: Integer v = ec.getConcreteIntValue(term2class);
327: if (v == null) {
328: current = ec.getMaximalConcreteLowerBound(term2class);
329: } else {
330: current = v.intValue();
331: }
332: Boolean ex = (Boolean) lb2ex.get(ec);
333: if (ex != null && ex.booleanValue()) {
334: current++;
335: }
336: if (current > max) {
337: max = current;
338: }
339: }
340: return max;
341: }
342:
343: public boolean consistencyCheck(HashMap term2class) {
344: if (isInt()) {
345: if (getMaximalConcreteLowerBound(term2class) > getMinimalConcreteUpperBound(term2class)) {
346: return false;
347: }
348: if (getConcreteIntValue(term2class) != null) {
349: if (getConcreteIntValue(term2class).longValue() > getMinimalConcreteUpperBound(term2class)
350: || getConcreteIntValue(term2class).longValue() < getMaximalConcreteLowerBound(term2class)) {
351: return false;
352: }
353: IteratorOfTerm itt = disjointRep.iterator();
354: while (itt.hasNext()) {
355: EquivalenceClass ec = (EquivalenceClass) term2class
356: .get(itt.next());
357: Integer i = ec.getConcreteIntValue(term2class);
358: if (i != null) {
359: if (iValue.longValue() == i.longValue()) {
360: return false;
361: }
362: }
363: }
364: }
365: } else if (isBoolean()
366: && getConcreteBooleanValue(term2class) != null) {
367: IteratorOfTerm itt = disjointRep.iterator();
368: while (itt.hasNext()) {
369: EquivalenceClass ec = (EquivalenceClass) term2class
370: .get(itt.next());
371: Boolean b = ec.getConcreteBooleanValue(term2class);
372: if (bValue == b) {
373: return false;
374: }
375: }
376: }
377: return true;
378: }
379:
380: public Boolean getConcreteBooleanValue(HashMap term2class) {
381: if (!isBoolean()) {
382: return null;
383: }
384: if (containsLiteral() || bValue != null) {
385: return bValue;
386: }
387: if (visited) {
388: return null;
389: } else {
390: visited = true;
391: }
392: IteratorOfTerm it = disjointRep.iterator();
393: while (it.hasNext()) {
394: Term t = it.next();
395: EquivalenceClass ec = (EquivalenceClass) term2class.get(t);
396: Boolean b = ec.getConcreteBooleanValue(term2class);
397: if (b != null) {
398: visited = false;
399: bValue = bool(!b.booleanValue());
400: return bValue;
401: }
402: }
403: visited = false;
404: return null;
405: }
406:
407: public Integer getConcreteIntValue(HashMap term2class) {
408: if (!isInt()) {
409: return null;
410: }
411: if (containsLiteral() || iValue != null) {
412: return iValue;
413: }
414: IteratorOfTerm it = members.iterator();
415: while (it.hasNext()) {
416: Term t = it.next();
417: Operator op = t.op();
418: // Do you really want the addition operators below or should it be
419: // getJavaAddInt, getJavaAddLong? (RB)
420: if (op == serv.getTypeConverter().getIntegerLDT()
421: .getArithAddition()
422: || op == serv.getTypeConverter().getIntLDT()
423: .getArithJavaIntAddition()) {
424: Integer res = null;
425: for (int i = 0; i < 2; i++) {
426: EquivalenceClass ec = (EquivalenceClass) term2class
427: .get(t.sub(i));
428: if (ec != null) {
429: Integer iv = ec.getConcreteIntValue(term2class);
430: if (iv != null && i == 0) {
431: res = ec.getConcreteIntValue(term2class);
432: } else if (iv != null) {
433: return new Integer(iv.intValue()
434: + res.intValue());
435: } else {
436: break;
437: }
438: } else {
439: try {
440: ProgramElement pe = serv.getTypeConverter()
441: .convertToProgramElement(t.sub(i));
442: if (pe instanceof IntLiteral) {
443: if (res == null && i == 0) {
444: res = new Integer(((IntLiteral) pe)
445: .getValue());
446: } else if (res != null) {
447: return new Integer(
448: ((IntLiteral) pe)
449: .getValue()
450: + res.intValue());
451: } else {
452: break;
453: }
454: }
455: } catch (RuntimeException e) {
456: // System.out.println(e);
457: }
458: }
459: }
460: if (res != null) {
461: return res;
462: }
463: }
464: }
465: return null;
466: //...
467: }
468:
469: public boolean containsLiteral() {
470: IteratorOfTerm it = members.iterator();
471: while (it.hasNext()) {
472: Term t = it.next();
473: if (isBoolean()) {
474: if (trueLit.equals(t)) {
475: if (bValue == null)
476: bValue = boolTrue;
477: return true;
478: } else if (falseLit.equals(t)) {
479: if (bValue == null)
480: bValue = boolFalse;
481: return true;
482: }
483: }
484: if (isInt()) {
485: try {
486: ProgramElement pe = serv.getTypeConverter()
487: .convertToProgramElement(t);
488: boolean negative = false;
489: if (pe instanceof Negative) {
490: pe = ((Negative) pe).getChildAt(0);
491: }
492: if (pe instanceof IntLiteral) {
493: if (iValue == null) {
494: iValue = new Integer((negative ? "-" : "")
495: + ((IntLiteral) pe).getValue());
496: }
497: return true;
498: }
499: } catch (RuntimeException e) {
500: // System.out.println(e);
501: }
502: }
503: }
504: return false;
505: }
506:
507: public String toString() {
508: return members.toString();
509: }
510: }
|