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:
012: package de.uka.ilkd.key.counterexample;
013:
014: import java.util.Vector;
015:
016: import de.uka.ilkd.key.logic.op.ConstructorFunction;
017: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
018: import de.uka.ilkd.key.logic.sort.GenSort;
019: import de.uka.ilkd.key.logic.sort.Sort;
020:
021: /**
022: * This class generates the clauses which depend on the generated sorts,
023: * it includes the static clauses generated by <code>Calculus</code>
024: * which this class extends.
025: *
026: * These clauses are different for each adt, depending on the generated
027: * sorts that are used. To these belong the domain generation and search,
028: * the rewriting of constructor arguments and the 'freely generated'
029: * property clauses.
030: *
031: * In the 'all' attribute inherited from Calculus are all Clauses
032: * generated by the Calculus class, which means, that if you use an
033: * instance of this class, you have both the static clauses of Calculus
034: * and the Sort-dependent clauses of this class.
035: *
036: * @author Sonja Pieper
037: * @version 0.1
038: */
039: public class SortCalculus extends Calculus {
040:
041: Vector sortdata;
042: Clauses sorts;
043:
044: /**
045: * Creates a new instance of SortCalculus. First calls the
046: * constructor of the super-class, the effect is that you
047: * already have the static clauses in the all-List after that
048: * is done. Afterwards all clauses SortCalculus generates
049: * are added to the list.
050: *
051: * @param s The generated sorts of the adt are needed to generate
052: * the clauses of this class
053: */
054: SortCalculus(Vector s) {
055: super ();
056: sortdata = s;
057: sorts = new Clauses();
058: sorts.add(this .domains());
059: sorts.add(this .domainsearch());
060: sorts.add(this .constrRewriting());
061: sorts.add(this .freelyGenerated());
062: this .all.add(sorts);
063: }
064:
065: /**
066: * This method returns a subset of the clauses of the complete
067: * calculus, the clauses that generate the domain and search the domain,
068: * constructor rewriting and the clauses that ensure the
069: * adt's 'freely generated' generated property.
070: *
071: * @return The clauses that are dependent on knowing the adt's sorts.
072: */
073: public Clauses getSortClauses() {
074: return sorts;
075: }
076:
077: /**
078: * This method returns a list of clauses which contains one clause
079: * for each constructor in each sort. These clauses generate the domain.
080: *
081: * @return The list of domain generating clauses.
082: */
083: private Clauses domains() {
084:
085: Clauses cs = new Clauses();
086:
087: // for each sort generate domain clauses:
088: for (int sortidx = 0; sortidx < sortdata.size(); sortidx++) {
089:
090: GenSort currentsort = (GenSort) sortdata.elementAt(sortidx);
091: String sortname = currentsort.name().toString();
092: String gen = "gen" + sortname;
093: Vector constructors = currentsort.getConstructors();
094:
095: cs.addComment("Generating domain for " + sortname);
096:
097: // for each constructor generate one clause:
098: for (int constridx = 0; constridx < constructors.size(); constridx++) {
099:
100: ConstructorFunction konstr = (ConstructorFunction) constructors
101: .elementAt(constridx);
102: ArrayOfSort params = konstr.argSort();
103:
104: if (konstr.arity() == 0) {
105: // f.e. "-> gensort(constr,1) ."
106: cs.add(new Clause("", gen + "("
107: + konstr.name().toString() + ",1)"));
108: } else {
109: // "max(M),gensort_0(X_0,Y_0),...,gensort_n(X_n,Y_n),
110: // {Y_(n+1)=1+Y_0+...+Y_n},{1+Y0+...+Y_n<=M}
111: // -> gensort(push(X_0,...,X_n),Y_(n+1)) ."
112:
113: String aconj = new String();
114:
115: { /* begin antecedent generation */
116:
117: aconj = "max(M)";
118:
119: // "gensort(X_i,Y_i)"
120: for (int paramidx = 0; paramidx < params.size(); paramidx++) {
121: aconj = aconj
122: + ",gen"
123: + (params.getSort(paramidx)).name()
124: .toString() + "(X"
125: + paramidx + ",Y" + paramidx + ")";
126: }
127:
128: //{Y_(n+1)=1+Y_0+...+Y_n},{1+Y0+...+Y_n<=M}
129:
130: String Y0toYn = new String();
131: for (int i = 0; i < konstr.arity(); i++) {
132: Y0toYn = Y0toYn + "+Y" + i;
133: }
134:
135: aconj = aconj + "{Y" + konstr.arity() + "=1"
136: + Y0toYn + "},{1" + Y0toYn + "<=M}";
137:
138: }/* end antecedent generation */
139:
140: String cnsq = new String();
141:
142: {/* begin consequent generation */
143:
144: //gensort(constr(X_0 ... X_n),Y_(n+1))
145:
146: String X0toXn = new String("X0");
147: for (int i = 1; i < konstr.arity(); i++) {
148: X0toXn = X0toXn + ",X" + i;
149: }
150:
151: cnsq = "gen" + sortname + "("
152: + konstr.name().toString() + "("
153: + X0toXn + ")" + ",Y" + konstr.arity()
154: + ")";
155:
156: }/* end consequent generation */
157:
158: //add clause to list:
159: cs.add(new Clause(aconj, cnsq));
160:
161: }/* else constr.arity()>0 */
162:
163: }/* for constridx */
164:
165: //redirecting from gennat predicate to nat predicate:
166: cs.add(new Clause("gen" + sortname + "(X,_)", sortname
167: + "(X)", "Redirecting domain for " + sortname));
168:
169: }/* for sortidx */
170:
171: return cs;
172:
173: }/* domains() */
174:
175: /**
176: * For each sort there is on clause that searches the domain of that sort for
177: * elements of that sort to match with other clauses. This method generates these
178: * search clauses.
179: *
180: * @return the list of domainsearch clauses
181: */
182: private Clauses domainsearch() {
183:
184: Clauses cs = new Clauses();
185:
186: for (int sortidx = 0; sortidx < sortdata.size(); sortidx++) {
187: GenSort currentsort = (GenSort) sortdata.elementAt(sortidx);
188: String sortname = currentsort.name().toString();
189: Vector constructors = currentsort.getConstructors();
190:
191: cs.addComment("Search domain of sort " + sortname);
192:
193: //--------- begin consequent generation ------------------
194:
195: String cnsq = new String();
196:
197: for (int constridx = 0; constridx < constructors.size(); constridx++) {
198: ConstructorFunction konstr = (ConstructorFunction) constructors
199: .elementAt(constridx);
200: ArrayOfSort params = konstr.argSort();
201:
202: String or = (constridx > 0 ? ";" : "");
203:
204: String search = new String();
205: String is = "is(X," + konstr.name().toString() + "(";
206:
207: for (int paramidx = 0; paramidx < konstr.arity(); paramidx++) {
208: is = is + "arg" + paramidx + "(X)";
209: Sort paramsort = params.getSort(paramidx);
210: search = search + ",search_"
211: + paramsort.name().toString() + "(arg"
212: + paramidx + "(X))";
213: }/* paramidx */
214:
215: is = ")";
216: cnsq = cnsq + or + is + search;
217:
218: }/* constridx */
219:
220: // ------------- end consequent generation --------------
221:
222: cs.add(new Clause("search_" + sortname + "(X)", cnsq));
223:
224: } /* for sortidx */
225:
226: return cs;
227:
228: }/* domainsearch() */
229:
230: /**
231: * The following rules implement the sort dependent rewrite rules
232: * @return the list of clauses for the rewriting of arguments
233: * of the constructors. These clauses differ from the normal
234: * argument rewriting clauses because constructors do not
235: * have an interpretation.
236: */
237: private Clauses constrRewriting() {
238: Clauses cs = new Clauses();
239:
240: cs.addComment("Constructor Rewriting clauses for each sort:");
241:
242: for (int sortidx = 0; sortidx < sortdata.size(); sortidx++) {
243: GenSort currentsort = (GenSort) sortdata.elementAt(sortidx);
244: String sortname = currentsort.name().toString();
245: Vector constructors = currentsort.getConstructors();
246:
247: for (int constridx = 0; constridx < constructors.size(); constridx++) {
248: ConstructorFunction konstr = (ConstructorFunction) constructors
249: .elementAt(constridx);
250: String pre = "is(X," + konstr.name().toString();
251:
252: for (int rewriteidx = 0; rewriteidx < konstr.arity(); rewriteidx++) {/* the currently rewritten param */
253:
254: String aconjparams = new String();
255: String cnsqparams = new String();
256:
257: for (int paramidx = 0; paramidx < konstr.arity(); paramidx++) {
258: String comma = (paramidx > 0 ? "," : "");
259: aconjparams = aconjparams + comma + "Y"
260: + paramidx;
261: cnsqparams = cnsqparams
262: + comma
263: + (paramidx == rewriteidx ? "Z" : "Y"
264: + paramidx);
265: }/* paramidx */
266:
267: String aconj = "is(X," + konstr.name().toString()
268: + "(" + aconjparams + ")),is(Y"
269: + rewriteidx + ",Z)";
270: String cnsq = "is(X," + konstr.name().toString()
271: + "(" + cnsqparams + "))";
272:
273: cs.add(new Clause(aconj, cnsq));
274: }/* rewriteidx */
275:
276: }/* constridx */
277:
278: }/* sortidx */
279:
280: return cs;
281:
282: }/* sort dependent constructor rewriting */
283:
284: /**
285: * the following rules implement equality under the
286: * assumption that the data types are 'freely generated'
287: * for each Konstruktor there is one rule that says when the
288: * atom is the same so must be the parameters. 'freely generated' backwards.
289: * f.e. 'same(push(N,ST),push(N1,ST1)) -> same(N,N1),same(ST,ST1) .'
290: * or 'same(succ(N),succ(N1)) -> same(N,N1) .'
291: * %%% what about konstruktors with zero parameters?
292: */
293:
294: private Clauses freelyGenerated() { //@@@
295:
296: Clauses cs = new Clauses();
297:
298: cs
299: .addComment("For each Konstruktor 'freely generated' backwards rules:");
300:
301: //---for each sort
302: for (int sortidx = 0; sortidx < sortdata.size(); sortidx++) {
303:
304: GenSort currentsort = (GenSort) sortdata.elementAt(sortidx);
305: String sortname = currentsort.name().toString();
306: Vector constructors = currentsort.getConstructors();
307:
308: //---take each constructor
309: for (int constridx = 0; constridx < constructors.size(); constridx++) {
310:
311: ConstructorFunction konstr = (ConstructorFunction) constructors
312: .elementAt(constridx);
313:
314: //---and compare with each other construcotr
315: for (int comp = 0; comp < constructors.size(); comp++) {
316:
317: ConstructorFunction compkonstr = (ConstructorFunction) constructors
318: .elementAt(comp);
319:
320: //---comparison with self generates a 'different'-clause
321: if (constridx == comp) {
322:
323: if (konstr.arity() == 0) {
324:
325: //f.e. different(nil,nil) -> .
326: cs.add(new Clause("different("
327: + konstr.name().toString() + ","
328: + konstr.name().toString() + ")",
329: ""));
330: } /* if konstr.arity() !=0 */
331: else {
332:
333: String argX = new String();
334: String argY = new String();
335: String cnsqsame = new String();
336: String cnsqdiff = new String();
337:
338: for (int i = 0; i < konstr.arity(); i++) {
339:
340: String comma = (i > 0 ? "," : "");
341: String semicolon = (i > 0 ? ";" : "");
342: argX = argX + comma + "X" + i;
343: argY = argY + comma + "Y" + i;
344: cnsqsame = cnsqsame + comma + "same(X"
345: + i + ",Y" + i + ")";
346: cnsqdiff = cnsqdiff + semicolon
347: + "different(X" + i + ",Y" + i
348: + ")";
349:
350: } /* for i */
351:
352: String args = konstr.name().toString()
353: + "(" + argX + "),"
354: + konstr.name().toString() + "("
355: + argY + ")";
356: Clause same = new Clause("same(" + args
357: + ")", cnsqsame);
358: Clause different = new Clause("different("
359: + args + ")", cnsqdiff);
360: cs.add(same);
361: cs.add(different);
362:
363: } /* else */
364: } /* if constridx != comp*/
365:
366: //---comparison with other constructor generates 'same'-clause
367: else {
368:
369: // f.e. same(succ(_),null) -> .
370:
371: String args = new String();
372: for (int n = 0; n < compkonstr.arity(); n++) {
373:
374: args = args + ((n > 0) ? "," : "") + "_";
375:
376: }
377: args = "(" + args + ")";
378: String compstr = new String(compkonstr.name()
379: .toString()
380: + args);
381:
382: String args1 = new String();
383: for (int n = 0; n < konstr.arity(); n++) {
384:
385: args1 = args1 + ((n > 0) ? "," : "") + "_";
386:
387: }
388: args1 = "(" + args1 + ")";
389: String konstrstr = konstr.name().toString()
390: + args;
391:
392: cs.add(new Clause("same(" + konstrstr + ","
393: + compstr + ")", ""));
394:
395: } /*else */
396:
397: } /* for comp */
398: } /* for constridx */
399: } /* for sortidx */
400:
401: return cs;
402: }
403:
404: }
|