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.visualdebugger.statevisualisation;
009:
010: import java.util.*;
011:
012: import de.uka.ilkd.key.java.Services;
013: import de.uka.ilkd.key.java.abstraction.ClassType;
014: import de.uka.ilkd.key.java.declaration.ArrayDeclaration;
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.Equality;
017:
018: public class SymbolicArrayObject extends SymbolicObject {
019:
020: private HashMap equClass2Repr;
021:
022: private final HashMap index2post = new HashMap();
023:
024: private final HashMap index2SO = new HashMap();
025:
026: private final HashMap index2term = new HashMap();
027:
028: private SetOfTerm indexConfiguration;
029:
030: private HashMap indexTerm2EquClass;
031:
032: private LinkedList possibleIndexTermConfigurations;
033:
034: public SymbolicArrayObject(SetOfTerm cl, ClassType t, Services s) {
035: super (cl, t, s);
036: assert (t instanceof ArrayDeclaration);
037: }
038:
039: public SymbolicArrayObject(Term cl, ClassType t, Services s,
040: SetOfTerm possibleIndexTerms) {
041: super (SetAsListOfTerm.EMPTY_SET.add(cl), t, s);
042: // this.possibleIndexTerms=possibleIndexTerms;
043: }
044:
045: public void addAssociationFromIndex(Term index, SymbolicObject so) {
046: index2SO.put(index, so);
047: }
048:
049: public void addIndexConstraint(Term g, Term o) {
050: Term f = g;
051: if (indexTerm2EquClass.containsKey(g)
052: && this .equClass2Repr.containsKey(indexTerm2EquClass
053: .get(g)))
054: f = (Term) equClass2Repr.get(indexTerm2EquClass.get(g));
055:
056: if (index2term.containsKey(f)) {
057: ListOfTerm t = (ListOfTerm) index2term.get(f);
058: t = t.append(o);
059: index2term.remove(f);
060: index2term.put(f, t);
061:
062: } else {
063: ListOfTerm t = SLListOfTerm.EMPTY_LIST.append(o);
064: index2term.put(f, t);
065: }
066:
067: }
068:
069: /**
070: * return all index terms used in this array object figures
071: */
072:
073: public SetOfTerm getAllIndexTerms() {
074: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
075: // System.out.println("PRIM "+this.isPrimitiveType());
076: // System.out.println(index2term);
077: // System.out.println(this.index2S0);
078: HashSet s = new HashSet((this .isPrimitiveType()) ? index2term
079: .keySet() : this .index2SO.keySet());
080: HashSet val = new HashSet(this .equClass2Repr.values());
081: s.addAll(val);
082:
083: for (Iterator it = s.iterator(); it.hasNext();) {
084: result = result.add((Term) it.next());
085: }
086: return result;
087: }
088:
089: public SetOfTerm getAllPostIndex() {
090: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
091: Set s = index2post.keySet();
092: for (Iterator it = s.iterator(); it.hasNext();) {
093: result = result.add((Term) it.next());
094: }
095: return result;
096: }
097:
098: public SymbolicObject getAssociationEndForIndex(Term index) {
099: // System.out.println("getIndex "+index2SO);
100: return (SymbolicObject) index2SO.get(index);
101: }
102:
103: public ListOfTerm getConstraintsForIndex(Term index) {
104: return (ListOfTerm) index2term.get(index);
105: }
106:
107: /**
108: * return the index configuration
109: *
110: * @return
111: */
112: public SetOfTerm getIndexConfiguration() {
113: return this .indexConfiguration;
114:
115: }
116:
117: public String getInstanceName() {
118: // TODO
119: return "Array_" + getId();
120: }
121:
122: public LinkedList getPossibleIndexTermConfigurations() {
123: return possibleIndexTermConfigurations;
124: }
125:
126: // public getal
127:
128: /**
129: * Finds a proper representantive for equivalence class cl.
130: *
131: * @param cl
132: * @return
133: */
134: private Term getRepres(EquClass cl) {
135: Term result = cl.getMembers().iterator().next();
136: for (IteratorOfTerm it = cl.getMembers().iterator(); it
137: .hasNext();) {
138: Term next = it.next();
139: if (isNumberLiteral(next)) {
140: result = next;
141: }
142: }
143:
144: return result;
145: }
146:
147: public Term getValueTermForIndex(Term index) {
148: return (Term) this .index2post.get(index);
149: }
150:
151: private boolean isNumberLiteral(Term t) {
152: char c = t.toString().charAt(0);
153: return c == 'Z';
154: }
155:
156: public boolean isPrimitiveType() {
157: return !(((ArrayDeclaration) getType()).getBaseType()
158: .getKeYJavaType().getJavaType() instanceof ClassType);
159: }
160:
161: /**
162: * sets the index configuration
163: *
164: * @param constraints
165: */
166: public void setIndexConfiguration(SetOfTerm constraints) {
167: indexTerm2EquClass = new HashMap();
168: // s.i
169: IteratorOfTerm it = constraints.iterator();
170: while (it.hasNext()) {
171: EquClass ec = null;
172: Term t = it.next();
173: if (t.op() instanceof Equality /* && !containsImplicitAttr(t) */) {
174: if (indexTerm2EquClass.containsKey(t.sub(0))) {
175: ec = (EquClass) indexTerm2EquClass.get(t.sub(0));
176: if (indexTerm2EquClass.containsKey(t.sub(1))) {
177: ec.add((EquClass) indexTerm2EquClass.get(t
178: .sub(1)));
179: } else {
180: ec.add(t.sub(1));
181: }
182: } else if (indexTerm2EquClass.containsKey(t.sub(1))) {
183: ec = (EquClass) indexTerm2EquClass.get(t.sub(1));
184: ec.add(t.sub(0));
185: } else {
186: ec = new EquClass(t.sub(0), t.sub(1));
187: }
188: IteratorOfTerm ecIt = ec.getMembers().iterator();
189: while (ecIt.hasNext()) {
190: indexTerm2EquClass.put(ecIt.next(), ec);
191: }
192: } else {
193: if (!indexTerm2EquClass.containsKey(t.sub(0).sub(1))) {
194: ec = new EquClass(t.sub(0).sub(1));
195: indexTerm2EquClass.put(t.sub(0).sub(1), ec);
196: }
197: if (!indexTerm2EquClass.containsKey(t.sub(0).sub(0))) {
198: ec = new EquClass(t.sub(0).sub(0));
199: indexTerm2EquClass.put(t.sub(0).sub(0), ec);
200: }
201:
202: }
203:
204: }
205:
206: this .equClass2Repr = new HashMap();
207: for (Iterator it2 = this .indexTerm2EquClass.values().iterator(); it2
208: .hasNext();) {
209:
210: EquClass cl = (EquClass) it2.next();
211: this .equClass2Repr.put(cl, getRepres(cl));
212: /*
213: * System.out.println("AAAAAAAAAAA"); System.out.println("Class
214: * "+cl.members ); System.out.println("Repr "+this.getRepres(cl));
215: */}
216:
217: this .indexConfiguration = constraints;
218:
219: }
220:
221: /**
222: * sets all possible index configurations
223: *
224: * @param possibleIndexTerms
225: */
226: public void setPossibleIndexTermConfigurations(
227: LinkedList possibleIndexTerms) {
228: this .possibleIndexTermConfigurations = possibleIndexTerms;
229: }
230:
231: public void setValueTermForIndex(Term index, Term value) {
232: Term f = index;
233: if (indexTerm2EquClass.containsKey(index)
234: && this .equClass2Repr.containsKey(indexTerm2EquClass
235: .get(index)))
236: f = (Term) equClass2Repr.get(indexTerm2EquClass.get(index));
237:
238: this .index2post.put(f, value);
239: }
240:
241: private class EquClass {
242: private SetOfTerm disjointRep = SetAsListOfTerm.EMPTY_SET;
243:
244: private SetOfTerm members;
245:
246: public EquClass(SetOfTerm members) {
247: this .members = members;
248:
249: }
250:
251: public EquClass(Term t) {
252: this (SetAsListOfTerm.EMPTY_SET.add(t));
253: }
254:
255: public EquClass(Term t1, Term t2) {
256: this (SetAsListOfTerm.EMPTY_SET.add(t1).add(t2));
257: }
258:
259: public void add(EquClass ec) {
260: members = members.union(ec.getMembers());
261: }
262:
263: public void add(Term t) {
264: members = members.add(t);
265: }
266:
267: public void addDisjoint(Term t) {
268: disjointRep = disjointRep.add(t);
269: }
270:
271: public SetOfTerm getDisjoints() {
272: return disjointRep;
273: }
274:
275: public SetOfTerm getMembers() {
276: return members;
277: }
278:
279: public String toString() {
280: return "EquClass: (" + members + ") Disjoint + "
281: + this .disjointRep + " /";
282: }
283:
284: }
285:
286: }
|