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: /**
014: * This class represents the succedent or antecendent part of a
015: * sequent. It is more or less a list without duplicates and subsumed
016: * formulas. This is ensured using method removeRedundancy. In future
017: * versions it can be enhanced to do other simplifications. A sequent
018: * and so a semisequent has to be immutable.
019: */
020: public class Semisequent {
021:
022: /** the empty semisequent (using singleton pattern) */
023: public static final Semisequent EMPTY_SEMISEQUENT = new Empty();
024: /** list with the Constraintformulae of the Semisequent */
025: private final ListOfConstrainedFormula seqList;
026:
027: /** used by inner class Empty*/
028: private Semisequent() {
029: seqList = SLListOfConstrainedFormula.EMPTY_LIST;
030: }
031:
032: /** creates a new Semisequent with the Semisequent elements in
033: * seqList */
034: private Semisequent(ListOfConstrainedFormula seqList) {
035: assert !seqList.isEmpty();
036: this .seqList = seqList;
037: }
038:
039: /** inserts an element at a specified index performing redundancy
040: * checks, this may result in returning same semisequent if
041: * inserting would create redundancies
042: * @param idx int encoding the place the element has to be put
043: * @param conForm ConstrainedFormula to be inserted
044: * @return a semi sequent change information object with the new semisequent
045: * and information which formulas have been added or removed
046: */
047: public SemisequentChangeInfo insert(int idx,
048: ConstrainedFormula conForm) {
049: return removeRedundance(idx, conForm);
050: }
051:
052: /** inserts the elements of the list at the specified index
053: * performing redundancy checks
054: * @param idx int encoding the place where the insertion starts
055: * @param insertionList ListOfConstrainedFormula to be inserted
056: * starting at idx
057: * @return a semi sequent change information object with the new semisequent
058: * and information which formulas have been added or removed
059: */
060: public SemisequentChangeInfo insert(int idx,
061: ListOfConstrainedFormula insertionList) {
062: return removeRedundance(idx, insertionList);
063: }
064:
065: /** inserts element at index 0 performing redundancy
066: * checks, this may result in returning same semisequent if
067: * inserting would create redundancies
068: * @param conForm ConstrainedFormula to be inserted
069: * @return a semi sequent change information object with the new semisequent
070: * and information which formulas have been added or removed
071: */
072: public SemisequentChangeInfo insertFirst(ConstrainedFormula conForm) {
073: return insert(0, conForm);
074: }
075:
076: /**
077: * inserts element at index 0 performing redundancy
078: * checks, this may result in returning same semisequent if
079: * inserting would create redundancies
080: * @param insertions ListOfConstrainedFormula to be inserted
081: * @return a semi sequent change information object with the new semisequent
082: * and information which formulas have been added or removed
083: */
084: public SemisequentChangeInfo insertFirst(
085: ListOfConstrainedFormula insertions) {
086: return insert(0, insertions);
087: }
088:
089: /** inserts element at the end of the semisequent performing
090: * redundancy checks, this may result in returning same
091: * semisequent if inserting would create redundancies
092: * @param conForm ConstrainedFormula to be inserted
093: * @return a semi sequent change information object with the new semisequent
094: * and information which formulas have been added or removed
095: */
096: public SemisequentChangeInfo insertLast(ConstrainedFormula conForm) {
097: return insert(size(), conForm);
098: }
099:
100: /**
101: * inserts the formulas of the list at the end of the semisequent
102: * performing redundancy checks, this may result in returning same
103: * semisequent if inserting would create redundancies
104: * @param insertions the ListOfConstrainedFormula to be inserted
105: * @return a semi sequent change information object with the new semisequent
106: * and information which formulas have been added or removed
107: */
108: public SemisequentChangeInfo insertLast(
109: ListOfConstrainedFormula insertions) {
110: return insert(size(), insertions);
111: }
112:
113: /**
114: * is this a semisequent that contains no formulas
115: * @return true if the semisequent contains no formulas
116: */
117: public boolean isEmpty() {
118: return seqList.isEmpty();
119: }
120:
121: /** .
122: * inserts new ConstrainedFormula at index idx and removes
123: * duplicates, perform simplifications etc.
124: * @return a semi sequent change information object with the new semisequent
125: * and information which formulas have been added or removed
126: */
127: private SemisequentChangeInfo removeRedundanceHelp(int idx,
128: ConstrainedFormula conForm, SemisequentChangeInfo semiCI) {
129: return removeRedundanceHelp(idx, conForm, semiCI, null);
130: }
131:
132: /** .
133: * inserts new ConstrainedFormula at index idx and removes
134: * duplicates, perform simplifications etc.
135: * @param fci null if the formula to be added is new, otherwise an
136: * object telling which formula is replaced with the new formula
137: * <code>conForm</code>, and what are the differences between the
138: * two formulas
139: * @return a semi sequent change information object with the new semisequent
140: * and information which formulas have been added or removed
141: */
142: private SemisequentChangeInfo removeRedundanceHelp(int idx,
143: ConstrainedFormula conForm, SemisequentChangeInfo semiCI,
144: FormulaChangeInfo fci) {
145:
146: // Search for equivalent formulas and weakest constraint
147: ListOfConstrainedFormula searchList = semiCI.getFormulaList();
148: ListOfConstrainedFormula newSeqList = SLListOfConstrainedFormula.EMPTY_LIST;
149: ConstrainedFormula cf;
150: Constraint c;
151: int pos = -1;
152:
153: while (searchList != SLListOfConstrainedFormula.EMPTY_LIST) {
154: ++pos;
155: cf = searchList.head();
156: searchList = searchList.tail();
157:
158: // for the moment we do not remove redundancy if intersection sorts are required
159: // Attention: just replacing null by new Services () slows KeY down by factor 3
160: c = Constraint.BOTTOM.unify(cf.formula(),
161: conForm.formula(), null);
162:
163: if (c.isAsWeakAs(cf.constraint())
164: || c.isAsWeakAs(conForm.constraint())) {
165: if (cf.constraint().isAsWeakAs(conForm.constraint())) {
166: semiCI.rejectedFormula(cf);
167: return semiCI; // semisequent already contains formula
168: } else if (cf.constraint().isAsStrongAs(
169: conForm.constraint())) {
170: semiCI.removedFormula(pos, cf);
171: if (idx > pos)
172: --idx;
173: --pos;
174: continue; // formula of the semisequent can be removed
175: }
176: }
177: newSeqList = newSeqList.prepend(cf);
178: }
179:
180: // compose resulting formula list
181: if (fci == null)
182: semiCI.addedFormula(idx, conForm);
183: else
184: semiCI.modifiedFormula(idx, fci);
185:
186: if (idx > pos) {
187: searchList = searchList.prepend(conForm);
188: }
189:
190: while (newSeqList != SLListOfConstrainedFormula.EMPTY_LIST) {
191: searchList = searchList.prepend(newSeqList.head());
192: newSeqList = newSeqList.tail();
193: if (idx == pos) {
194: searchList = searchList.prepend(conForm);
195: }
196: --pos;
197: }
198:
199: // add new formula list to result object
200: semiCI.setFormulaList(searchList);
201:
202: return semiCI;
203: }
204:
205: /** .
206: * inserts new ConstrainedFormulas starting at index idx and removes
207: * duplicates, perform simplifications etc.
208: * @param conForm the ListOfConstrainedFormula to be inserted at position idx
209: * @param idx an int that means insert conForm at the idx-th
210: * position in the semisequent
211: * @return a semi sequent change information object with the new semisequent
212: * and information which formulas have been added or removed
213: */
214: private SemisequentChangeInfo removeRedundance(int idx,
215: ListOfConstrainedFormula conForm, SemisequentChangeInfo sci) {
216:
217: int pos = idx;
218: ListOfConstrainedFormula oldFormulas = sci.getFormulaList();
219: final IteratorOfConstrainedFormula it = conForm.iterator();
220:
221: while (it.hasNext()) {
222: sci = removeRedundanceHelp(pos, it.next(), sci);
223:
224: if (sci.getFormulaList() != oldFormulas) {
225: pos = sci.getIndex() + 1;
226: oldFormulas = sci.getFormulaList();
227: }
228: }
229:
230: return complete(sci);
231: }
232:
233: /** .
234: * inserts new ConstrainedFormulas starting at index idx and removes
235: * duplicates, perform simplifications etc.
236: * @param conForm the ListOfConstrainedFormula to be inserted at position idx
237: * @param idx an int that means insert conForm at the idx-th
238: * position in the semisequent
239: * @return a semi sequent change information object with the new semisequent
240: * and information which formulas have been added or removed
241: */
242: private SemisequentChangeInfo removeRedundance(int idx,
243: ListOfConstrainedFormula conForm) {
244: return removeRedundance(idx, conForm,
245: new SemisequentChangeInfo(seqList));
246: }
247:
248: /** .
249: * inserts new ConstrainedFormula at index idx and removes
250: * duplicates, perform simplifications etc.
251: * @param conForm the ConstrainedFormula to be inserted at position idx
252: * @param idx an int that means insert conForm at the idx-th
253: * position in the semisequent
254: * @return new Semisequent with conForm at index idx and removed
255: * redundancies
256: */
257: private SemisequentChangeInfo removeRedundance(int idx,
258: ConstrainedFormula conForm) {
259: return complete(removeRedundanceHelp(idx, conForm,
260: new SemisequentChangeInfo(seqList)));
261: }
262:
263: /**
264: * replaces the element at place idx with conForm
265: *
266: * @param pos
267: * the PosInOccurrence describing the position of and within the
268: * formula below which the formula differs from the new formula
269: * <code>conForm</code>
270: * @param conForm
271: * the ConstrainedFormula replacing the old element at index idx
272: * @return a semi sequent change information object with the new semisequent
273: * and information which formulas have been added or removed
274: */
275: public SemisequentChangeInfo replace(PosInOccurrence pos,
276: ConstrainedFormula conForm) {
277: final int idx = indexOf(pos.constrainedFormula());
278: final FormulaChangeInfo fci = new FormulaChangeInfo(pos,
279: conForm);
280: return complete(removeRedundanceHelp(idx, conForm, remove(idx),
281: fci));
282: }
283:
284: /**
285: * replaces the <tt>idx</tt>-th formula by <tt>conForm</tt>
286: * @param idx the int with the position of the formula to be replaced
287: * @param conForm the ConstrainedFormula replacing the formula at the given position
288: * @return a SemisequentChangeInfo containing the new sequent and a diff to the old
289: * one
290: */
291: public SemisequentChangeInfo replace(int idx,
292: ConstrainedFormula conForm) {
293: return complete(removeRedundanceHelp(idx, conForm, remove(idx)));
294: }
295:
296: /**
297: * replaces the element at place idx with the first element of the
298: * given list and adds the rest of the list to the semisequent
299: * behind the replaced formula
300: * @param pos the formula to be replaced
301: * @param replacements the ListOfConstrainedFormula whose head
302: * replaces the element at index idx and the tail is added to the
303: * semisequent
304: * @return a semi sequent change information object with the new semisequent
305: * and information which formulas have been added or removed
306: */
307: public SemisequentChangeInfo replace(PosInOccurrence pos,
308: ListOfConstrainedFormula replacements) {
309: final int idx = indexOf(pos.constrainedFormula());
310: return removeRedundance(idx, replacements, remove(idx));
311: }
312:
313: public SemisequentChangeInfo replace(int idx,
314: ListOfConstrainedFormula replacements) {
315: return removeRedundance(idx, replacements, remove(idx));
316: }
317:
318: /** @return int counting the elements of this semisequent */
319: public int size() {
320: return seqList.size();
321: }
322:
323: /**
324: * creates a semisequent out of the semisequent change info (semiCI)
325: * object and hands it over to semiCI
326: */
327: protected SemisequentChangeInfo complete(
328: SemisequentChangeInfo semiCI) {
329:
330: final ListOfConstrainedFormula formulaList = semiCI
331: .getFormulaList();
332: if (formulaList.isEmpty()) {
333: semiCI.setSemisequent(EMPTY_SEMISEQUENT);
334: } else {
335: final Semisequent result = formulaList == seqList ? this
336: : new Semisequent(formulaList);
337: semiCI.setSemisequent(result);
338: }
339: return semiCI;
340: }
341:
342: /**
343: * removes an element
344: * @param idx int being the index of the element that has to
345: * be removed
346: * @return a semi sequent change information object with the new semisequent
347: * and information which formulas have been added or removed
348: */
349: public SemisequentChangeInfo remove(int idx) {
350:
351: ListOfConstrainedFormula newList = seqList;
352: ListOfConstrainedFormula queue = SLListOfConstrainedFormula.EMPTY_LIST;
353: int index = 0;
354:
355: if (idx < 0 || idx >= size()) {
356: return complete(new SemisequentChangeInfo(seqList));
357: }
358:
359: final ConstrainedFormula[] temp = new ConstrainedFormula[idx];
360:
361: while (index < idx) {// go to idx
362: temp[index] = newList.head();
363: newList = newList.tail();
364: index++;
365: }
366:
367: for (int k = index - 1; k >= 0; k--)
368: queue = queue.prepend(temp[k]);
369:
370: // remove the element that is at head of newList
371: final ConstrainedFormula removedFormula = newList.head();
372: newList = newList.tail();
373: newList = newList.prepend(queue);
374:
375: // create change info object
376: final SemisequentChangeInfo sci = new SemisequentChangeInfo(
377: newList);
378: sci.removedFormula(idx, removedFormula);
379:
380: return complete(sci);
381: }
382:
383: /**
384: * returns index of a ConstrainedFormula. An identity check ('==')
385: * is used when searching for the ConstrainedFormula, NOT equals on
386: * ConstrainedFormula, because a ConstrainedFormulae identifies the origin
387: * of a formula.
388: * @param conForm the ConstrainedFormula the index want to be
389: * determined
390: * @return index of conForm (-1 if not found)
391: */
392: public int indexOf(ConstrainedFormula conForm) {
393: ListOfConstrainedFormula searchList = seqList;
394: int index = 0;
395: while (searchList != SLListOfConstrainedFormula.EMPTY_LIST) {
396: if (searchList.head() == conForm) {
397: return index;
398: } else {
399: index++;
400: }
401: searchList = searchList.tail();
402: }
403: return -1;
404: }
405:
406: /** gets the element at a specific index
407: * @param idx int representing the index of the element we
408: * want to have
409: * @return ConstrainedFormula found at index idx
410: * @throws IndexOutOfBoundsException if idx is negative or
411: * greater or equal to {@link Sequent#size()}
412: */
413: public ConstrainedFormula get(int idx) {
414: if (idx < 0 || idx >= seqList.size()) {
415: throw new IndexOutOfBoundsException();
416: }
417: return seqList.take(idx).head();
418: }
419:
420: /** @return the first ConstrainedFormula of this Semisequent */
421: public ConstrainedFormula getFirst() {
422: return seqList.head();
423: }
424:
425: /** checks if a ConstrainedFormula is in this Semisequent
426: * (identity check)
427: * @param conForm the ConstraintForumla to look for
428: * @return true iff. conForm has been found in this
429: * Semisequent
430: */
431: public boolean contains(ConstrainedFormula conForm) {
432: return indexOf(conForm) != -1;
433: }
434:
435: /** checks if a ConstrainedFormula is in this Semisequent
436: * (equality check)
437: * @param conForm the ConstraintForumla to look for
438: * @return true iff. conForm has been found in this
439: * Semisequent
440: */
441: public boolean containsEqual(ConstrainedFormula conForm) {
442: return seqList.contains(conForm);
443: }
444:
445: /**
446: * returns iterator about the elements of the sequent
447: * @return IteratorOfConstrainedFormula
448: */
449: public IteratorOfConstrainedFormula iterator() {
450: return seqList.iterator();
451: }
452:
453: public ListOfConstrainedFormula toList() {
454: return seqList;
455: }
456:
457: public boolean equals(Object o) {
458: if (!(o instanceof Semisequent))
459: return false;
460: return seqList.equals(((Semisequent) o).seqList);
461: }
462:
463: public int hashCode() {
464: return seqList.hashCode();
465: }
466:
467: /** @return String representation of this Semisequent */
468: public String toString() {
469: return seqList.toString();
470: }
471:
472: // inner class used to represent an empty semisequent
473: private static class Empty extends Semisequent {
474:
475: private Empty() {
476: super ();
477: }
478:
479: /** inserts the element always at index 0 ignores the first
480: * argument
481: * @param idx int encoding the place the element has to be put
482: * @param conForm ConstrainedFormula to be inserted
483: * @return semisequent change information object with new semisequent
484: * with conForm at place idx
485: */
486: public SemisequentChangeInfo insert(int idx,
487: ConstrainedFormula conForm) {
488: return insertFirst(conForm);
489: }
490:
491: /** inserts the element at index 0
492: * @param conForm ConstrainedFormula to be inserted
493: * @return semisequent change information object with new semisequent
494: * with conForm at place idx
495: */
496: public SemisequentChangeInfo insertFirst(
497: ConstrainedFormula conForm) {
498: final SemisequentChangeInfo sci = new SemisequentChangeInfo(
499: SLListOfConstrainedFormula.EMPTY_LIST
500: .prepend(conForm));
501: sci.addedFormula(0, conForm);
502: return complete(sci);
503: }
504:
505: /** inserts the element at the end of the semisequent
506: * @param conForm ConstrainedFormula to be inserted
507: * @return semisequent change information object with new semisequent
508: * with conForm at place idx
509: */
510: public SemisequentChangeInfo insertLast(
511: ConstrainedFormula conForm) {
512: return insertFirst(conForm);
513: }
514:
515: /**
516: * is this a semisequent that contains no formulas
517: * @return true if the semisequent contains no formulas
518: */
519: public boolean isEmpty() {
520: return true;
521: }
522:
523: /** replaces the element at place idx with conForm
524: * @param idx an int specifying the index of the element that
525: * has to be replaced
526: * @param conForm the ConstrainedFormula replacing the old
527: * element at index idx
528: * @return semisequent change information object with new semisequent
529: * with conForm at place idx
530: */
531: public SemisequentChangeInfo replace(int idx,
532: ConstrainedFormula conForm) {
533: return insertFirst(conForm);
534: }
535:
536: /** @return int counting the elements of this semisequent */
537: public int size() {
538: return 0;
539: }
540:
541: /** removes an element
542: * @param idx int being the index of the element that has to
543: * be removed
544: * @return semisequent change information object with an empty
545: * semisequent as result
546: */
547: public SemisequentChangeInfo remove(int idx) {
548: return complete(new SemisequentChangeInfo(
549: SLListOfConstrainedFormula.EMPTY_LIST));
550: }
551:
552: /** returns index of a ConstrainedFormula
553: * @param conForm the ConstrainedFormula the index want to be
554: * determined
555: * @return index of conForm
556: */
557: public int indexOf(ConstrainedFormula conForm) {
558: return -1;
559: }
560:
561: /** gets the element at a specific index
562: * @param idx int representing the index of the element we
563: * want to have
564: * @return ConstrainedFormula found at index idx
565: */
566: public ConstrainedFormula get(int idx) {
567: return null;
568: }
569:
570: /** @return the first ConstrainedFormula of this Semisequent
571: */
572: public ConstrainedFormula getFirst() {
573: return null;
574: }
575:
576: /** checks if a ConstrainedFormula is in this Semisequent
577: * @param conForm the ConstraintForumla to look for
578: * @return true iff. conForm has been found in this
579: * Semisequent
580: */
581: public boolean contains(ConstrainedFormula conForm) {
582: return false;
583: }
584:
585: public boolean equals(Object o) {
586: return o == this ;
587: }
588:
589: public int hashCode() {
590: return 34567;
591: }
592:
593: /** @return String representation of this Semisequent */
594: public String toString() {
595: return "[]";
596: }
597:
598: }
599:
600: }
|