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 de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
015: import de.uka.ilkd.key.pp.SequentPrintFilter;
016:
017: /** This class represents a sequent. A sequent consists of an
018: * antecedent and succedent. As a sequent is persistent there is no
019: * public constructor.
020: * <p>
021: * A sequent is created either by using one of
022: * the composition methods, that are
023: * {@link Sequent#createSequent},
024: * {@link Sequent#createAnteSequent} and
025: * {@link Sequent#createSuccSequent}
026: * or by inserting formulas directly into {@link Sequent#EMPTY_SEQUENT}.
027: */
028: public class Sequent {
029:
030: public static final Sequent EMPTY_SEQUENT = new NILSequent();
031:
032: /**
033: * creates a new Sequent with empty succedent
034: * @param ante the Semisequent that plays the antecedent part
035: * @return the new sequent or the EMPTY_SEQUENT if both antec and succ
036: * are same as EMPTY_SEMISEQUENT
037: */
038: public static Sequent createAnteSequent(Semisequent ante) {
039: if (ante.isEmpty()) {
040: return EMPTY_SEQUENT;
041: }
042: return new Sequent(ante, Semisequent.EMPTY_SEMISEQUENT);
043: }
044:
045: /**
046: * creates a new Sequent
047: * @param ante the Semisequent that plays the antecedent part
048: * @param succ the Semisequent that plays the succedent part
049: * @return the new sequent or the EMPTY_SEQUENT if both antec and succ
050: * are same as EMPTY_SEMISEQUENT
051: */
052: public static Sequent createSequent(Semisequent ante,
053: Semisequent succ) {
054: if (ante.isEmpty() && succ.isEmpty()) {
055: return EMPTY_SEQUENT;
056: }
057: return new Sequent(ante, succ);
058: }
059:
060: /**
061: * creates a new Sequent with empty antecedent
062: * @param succ the Semisequent that plays the succedent part
063: * @return the new sequent or the EMPTY_SEQUENT if both antec and succ
064: * are same as EMPTY_SEMISEQUENT
065: */
066: public static Sequent createSuccSequent(Semisequent succ) {
067: if (succ.isEmpty()) {
068: return EMPTY_SEQUENT;
069: }
070: return new Sequent(Semisequent.EMPTY_SEMISEQUENT, succ);
071: }
072:
073: private final Semisequent antecedent;
074:
075: private final Semisequent succedent;
076:
077: /**
078: * must only be called by NILSequent
079: *
080: */
081: private Sequent() {
082: antecedent = Semisequent.EMPTY_SEMISEQUENT;
083: succedent = Semisequent.EMPTY_SEMISEQUENT;
084: }
085:
086: /** creates new Sequent with antecedence and succedence */
087: private Sequent(Semisequent antecedent, Semisequent succedent) {
088: assert !antecedent.isEmpty() || !succedent.isEmpty();
089: this .antecedent = antecedent;
090: this .succedent = succedent;
091: }
092:
093: /**
094: * adds a formula to the antecedent (or succedent) of the
095: * sequent. Depending on the value of first the formulas are
096: * inserted at the beginning or end of the ante-/succedent.
097: * (NOTICE:Sequent determines
098: * index using identy (==) not equality.)
099: * @param cf the ConstrainedFormula to be added
100: * @param antec boolean selecting the correct semisequent where to
101: * insert the formulas. If set to true, the antecedent is taken
102: * otherwise the succedent.
103: * @param first boolean if true the formula is added at the
104: * beginning of the ante-/succedent, otherwise to the end
105: * @return a SequentChangeInfo which contains the new sequent and
106: * information which formulas have been added or removed
107: */
108: public SequentChangeInfo addFormula(ConstrainedFormula cf,
109: boolean antec, boolean first) {
110:
111: final Semisequent seq = antec ? antecedent : succedent;
112:
113: final SemisequentChangeInfo semiCI = first ? seq
114: .insertFirst(cf) : seq.insertLast(cf);
115:
116: return SequentChangeInfo.createSequentChangeInfo(antec, semiCI,
117: composeSequent(antec, semiCI.semisequent()), this );
118: }
119:
120: /**
121: * adds a formula to the sequent at the given
122: * position. (NOTICE:Sequent determines
123: * index using identy (==) not equality.)
124: * @param cf a ConstrainedFormula to be added
125: * @param p a PosInOccurrence describes position in the sequent
126: * @return a SequentChangeInfo which contains the new sequent and
127: * information which formulas have been added or removed
128: */
129: public SequentChangeInfo addFormula(ConstrainedFormula cf,
130: PosInOccurrence p) {
131: final Semisequent seq = getSemisequent(p);
132:
133: final SemisequentChangeInfo semiCI = seq.insert(seq.indexOf(p
134: .constrainedFormula()), cf);
135:
136: return SequentChangeInfo.createSequentChangeInfo(p.isInAntec(),
137: semiCI, composeSequent(p, semiCI.semisequent()), this );
138: }
139:
140: /**
141: * adds list of formulas to the antecedent (or succedent) of the
142: * sequent. Depending on the value of first the formulas are
143: * inserted at the beginning or end of the ante-/succedent.
144: * (NOTICE:Sequent determines
145: * index using identity (==) not equality.)
146: * @param insertions the ListOfConstrainedFormula to be added
147: * @param antec boolean selecting the correct semisequent where to
148: * insert the formulas. If set to true, the antecedent is taken
149: * otherwise the succedent.
150: * @param first boolean if true the formulas are added at the
151: * beginning of the ante-/succedent, otherwise to the end
152: * @return a SequentChangeInfo which contains the new sequent and
153: * information which formulas have been added or removed
154: */
155: public SequentChangeInfo addFormula(
156: ListOfConstrainedFormula insertions, boolean antec,
157: boolean first) {
158:
159: final Semisequent seq = antec ? antecedent : succedent;
160:
161: final SemisequentChangeInfo semiCI = first ? seq
162: .insertFirst(insertions) : seq.insertLast(insertions);
163:
164: return SequentChangeInfo.createSequentChangeInfo(antec, semiCI,
165: composeSequent(antec, semiCI.semisequent()), this );
166: }
167:
168: /** adds the formulas of list insertions to the sequent starting at
169: * position p. (NOTICE:Sequent determines
170: * index using identy (==) not equality.)
171: * @param insertions a ListOfConstrainedFormula with the formulas to be added
172: * @param p the PosInOccurrence describing the position where to
173: * insert the formulas
174: * @return a SequentChangeInfo which contains the new sequent and
175: * information which formulas have been added or removed
176: */
177: public SequentChangeInfo addFormula(
178: ListOfConstrainedFormula insertions, PosInOccurrence p) {
179: final Semisequent seq = getSemisequent(p);
180:
181: final SemisequentChangeInfo semiCI = seq.insert(seq.indexOf(p
182: .constrainedFormula()), insertions);
183:
184: return SequentChangeInfo.createSequentChangeInfo(p.isInAntec(),
185: semiCI, composeSequent(p, semiCI.semisequent()), this );
186: }
187:
188: /** returns semisequent of the antecedent to work with */
189: public Semisequent antecedent() {
190: return antecedent;
191: }
192:
193: /**
194: * replaces the formula at the given position with another one
195: * (NOTICE:Sequent determines
196: * index using identity (==) not equality.)
197: * @param newCF the ConstrainedFormula replacing the old one
198: * @param p a PosInOccurrence describes position in the sequent
199: * @return a SequentChangeInfo which contains the new sequent and
200: * information which formulas have been added or removed
201: */
202: public SequentChangeInfo changeFormula(ConstrainedFormula newCF,
203: PosInOccurrence p) {
204: final SemisequentChangeInfo semiCI = getSemisequent(p).replace(
205: p, newCF);
206:
207: return SequentChangeInfo.createSequentChangeInfo(p.isInAntec(),
208: semiCI, composeSequent(p, semiCI.semisequent()), this );
209: }
210:
211: /**
212: * replaces the formula at position p with the head of the given
213: * list and adds the remaining list elements to the sequent
214: * (NOTICE:Sequent determines
215: * index using identity (==) not equality.)
216: * @param replacements the ListOfConstrainedFormula whose head
217: * replaces the formula at position p and adds the rest of the list
218: * behind the changed formula
219: * @param p a PosInOccurrence describing the position of the formula
220: * to be replaced
221: * @return a SequentChangeInfo which contains the new sequent and
222: * information which formulas have been added or removed
223: */
224: public SequentChangeInfo changeFormula(
225: ListOfConstrainedFormula replacements, PosInOccurrence p) {
226:
227: final SemisequentChangeInfo semiCI = getSemisequent(p).replace(
228: p, replacements);
229:
230: final SequentChangeInfo sci = SequentChangeInfo
231: .createSequentChangeInfo(p.isInAntec(), semiCI,
232: composeSequent(p, semiCI.semisequent()), this );
233:
234: return sci;
235: }
236:
237: /** returns creates a new sequent out of the current sequent with a
238: * replaced antecedent if antec is true, otherwise the succedent is
239: * replaced by the given semisequent seq.
240: */
241: private Sequent composeSequent(boolean antec, Semisequent seq) {
242: if (seq.isEmpty()) {
243: if (!antec && antecedent().isEmpty()) {
244: return EMPTY_SEQUENT;
245: } else if (antec && succedent().isEmpty()) {
246: return EMPTY_SEQUENT;
247: }
248: }
249: return new Sequent(antec ? seq : antecedent(),
250: antec ? succedent() : seq);
251: }
252:
253: /** returns new Sequent with replaced antecedent if
254: * PosInOccurrence describes a ConstrainedFormula in the antecedent,
255: * the succedent is replaced otherwise.
256: * The new semisequent is seq.
257: */
258: private Sequent composeSequent(PosInOccurrence p, Semisequent seq) {
259: return composeSequent(p.isInAntec(), seq);
260: }
261:
262: /**
263: * determines if the sequent is empty.
264: * @return true iff the sequent consists of two instances of
265: * Semisequent.EMPTY_SEMISEQUENT
266: */
267: public boolean isEmpty() {
268: return antecedent().isEmpty() && succedent().isEmpty();
269: }
270:
271: public boolean equals(Object o) {
272: if (!(o instanceof Sequent))
273: return false;
274: final Sequent o1 = (Sequent) o;
275: return antecedent.equals(o1.antecedent())
276: && succedent.equals(o1.succedent());
277: }
278:
279: public int formulaNumberInSequent(boolean inAntec,
280: ConstrainedFormula cfma) {
281: int n = inAntec ? 0 : antecedent.size();
282: final IteratorOfConstrainedFormula formIter = inAntec ? antecedent
283: .iterator()
284: : succedent.iterator();
285: while (formIter.hasNext()) {
286: n++;
287: if (formIter.next().equals(cfma))
288: return n;
289: }
290: throw new RuntimeException("Ghost formula " + cfma
291: + " in sequent " + this + " [antec=" + inAntec + "]");
292: }
293:
294: public ConstrainedFormula getFormulabyNr(int formulaNumber) {
295: if (formulaNumber <= 0 || formulaNumber > size()) {
296: throw new RuntimeException("No formula nr. "
297: + formulaNumber + " in seq. " + this );
298: }
299: if (formulaNumber <= antecedent.size()) {
300: return antecedent.get(formulaNumber - 1);
301: }
302: return succedent.get((formulaNumber - 1) - antecedent.size());
303: }
304:
305: /** returns the semisequent in which the ConstrainedFormula described
306: * by PosInOccurrence p lies
307: */
308: private Semisequent getSemisequent(PosInOccurrence p) {
309: return p.isInAntec() ? antecedent() : succedent();
310: }
311:
312: public int hashCode() {
313: return antecedent.hashCode() * 17 + succedent.hashCode();
314: }
315:
316: /** returns iterator about all ConstrainedFormulae of the sequent
317: * @return iterator about all ConstrainedFormulae of the sequent
318: */
319: public IteratorOfConstrainedFormula iterator() {
320: return new SequentIterator(antecedent(), succedent());
321: }
322:
323: public boolean numberInAntec(int formulaNumber) {
324: return formulaNumber <= antecedent.size();
325: }
326:
327: public void prettyprint(de.uka.ilkd.key.pp.LogicPrinter printer) {
328: printer.printSequent(this );
329: }
330:
331: public void prettyprint(de.uka.ilkd.key.pp.LogicPrinter printer,
332: SequentPrintFilter filter) {
333: printer.printSequent(this , filter);
334: }
335:
336: public StringBuffer prettyprint(Services services) {
337: de.uka.ilkd.key.pp.LogicPrinter lp = (new de.uka.ilkd.key.pp.LogicPrinter(
338: new de.uka.ilkd.key.pp.ProgramPrinter(null),
339: de.uka.ilkd.key.pp.NotationInfo.createInstance(),
340: services));
341: lp.printSequent(this );
342: return lp.result();
343: }
344:
345: /** removes the formula at position p (NOTICE:Sequent determines
346: * index using identity (==) not equality.)
347: * @param p a PosInOccurrence that describes position in the sequent
348: * @return a SequentChangeInfo which contains the new sequent and
349: * information which formulas have been added or removed
350: */
351: public SequentChangeInfo removeFormula(PosInOccurrence p) {
352: final Semisequent seq = getSemisequent(p);
353:
354: final SemisequentChangeInfo semiCI = seq.remove(seq.indexOf(p
355: .constrainedFormula()));
356:
357: final SequentChangeInfo sci = SequentChangeInfo
358: .createSequentChangeInfo(p.isInAntec(), semiCI,
359: composeSequent(p, semiCI.semisequent()), this );
360:
361: return sci;
362: }
363:
364: public int size() {
365: return antecedent().size() + succedent().size();
366: }
367:
368: /** returns semisequent of the succedent to work with */
369: public Semisequent succedent() {
370: return succedent;
371: }
372:
373: /** String representation of the sequent
374: * @return String representation of the sequent */
375: public String toString() {
376: return antecedent().toString() + "==>" + succedent().toString();
377: }
378:
379: /**
380: * returns true iff the given variable is bound in a formula of a
381: * ConstrainedFormula in this sequent.
382: * @param v the bound variable to search for
383: */
384: public boolean varIsBound(QuantifiableVariable v) {
385: final IteratorOfConstrainedFormula it = iterator();
386: while (it.hasNext()) {
387: final BoundVarsVisitor bvv = new BoundVarsVisitor();
388: it.next().formula().execPostOrder(bvv);
389: if (bvv.getBoundVariables().contains(v)) {
390: return true;
391: }
392: }
393: return false;
394: }
395:
396: static class NILSequent extends Sequent {
397:
398: public boolean isEmpty() {
399: return true;
400: }
401:
402: public IteratorOfConstrainedFormula iterator() {
403: return SLListOfConstrainedFormula.EMPTY_LIST.iterator();
404: }
405:
406: public boolean varIsBound(QuantifiableVariable v) {
407: return false;
408: }
409:
410: }
411:
412: static class SequentIterator implements
413: IteratorOfConstrainedFormula {
414:
415: private final IteratorOfConstrainedFormula anteIt;
416: private final IteratorOfConstrainedFormula succIt;
417:
418: SequentIterator(Semisequent ante, Semisequent succ) {
419: this .anteIt = ante.iterator();
420: this .succIt = succ.iterator();
421: }
422:
423: public boolean hasNext() {
424: return anteIt.hasNext() || succIt.hasNext();
425: }
426:
427: public ConstrainedFormula next() {
428: if (anteIt.hasNext()) {
429: return anteIt.next();
430: }
431: return succIt.next();
432: }
433:
434: }
435:
436: }
|