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: * Records the changes made to a sequent. Keeps track of added and removed
015: * formula to one of the semisequents. The intersection of added and removed
016: * formulas of the same semisequent may not be empty, in particular this means
017: * that a formula added and removed afterwards will occur in both lists. The
018: * situation where this can happen is that a list of formulas had to be added to
019: * the sequent and the list has not been redundance free.
020: */
021: public class SequentChangeInfo implements java.io.Serializable {
022:
023: /** change information related to the antecedent, this means the
024: * there added and removed formulas*/
025: private SemisequentChangeInfo antecedent;
026:
027: /** change information related to the antecedent, this means the
028: * there added and removed formulas*/
029: private SemisequentChangeInfo succedent;
030:
031: /**
032: * the sequent before the changes
033: */
034: private Sequent originalSequent;
035:
036: /**
037: * the sequent after the changes
038: */
039: private Sequent resultingSequent;
040:
041: /**
042: * creates a new sequent change info whose semisequent described by position
043: * pos has changed. The made changes are stored in semiCI and the resulting
044: * sequent is given by result
045: *
046: * @param pos the PosInOccurrence describing the semisequent where
047: * the changes took place
048: * @param semiCI the SemisequentChangeInfo describing the changes in
049: * detail (which formulas have been added/removed)
050: * @return the sequent change information object describing the
051: * complete changes made to the sequent together with the operations
052: * result.
053: */
054: public static SequentChangeInfo createSequentChangeInfo(
055: PosInOccurrence pos, SemisequentChangeInfo semiCI,
056: Sequent result, Sequent original) {
057: return createSequentChangeInfo(pos.isInAntec(), semiCI, result,
058: original);
059: }
060:
061: /**
062: * creates a new sequent change info whose semisequent described by the
063: * value of the selector antec (true selects antecedent; false selects
064: * succedent) has changed. The made changes are stored in semiCI and the
065: * resulting sequent is given by result
066: *
067: * @param antec a boolean indicating if the given semisequent change information
068: * describes the changes of the antecedent or succedent
069: * @param semiCI the SemisequentChangeInfo describing the
070: * changes in detail (which formulas have been added/removed)
071: * @param result the Sequent which is the result of the changes
072: * @param original the Sequent to which the described changes have been
073: * applied
074: * @return the sequent change information object describing the
075: * complete changes made to the sequent together with the operations
076: * result. */
077: public static SequentChangeInfo createSequentChangeInfo(
078: boolean antec, SemisequentChangeInfo semiCI,
079: Sequent result, Sequent original) {
080: if (antec) {
081: return new SequentChangeInfo(semiCI, null, result, original);
082: } else {
083: return new SequentChangeInfo(null, semiCI, result, original);
084: }
085: }
086:
087: /**
088: * creates a new sequent change info whose semisequents have changed.
089: * The made changes are stored in semiCI and the resulting sequent is given
090: * by result
091: *
092: * @param anteCI the SemisequentChangeInfo describing the changes of the
093: * antecedent in detail (which formulas have been added/removed)
094: * @param sucCI the SemisequentChangeInfo describing the changes of the
095: * succedent detail (which formulas have been added/removed)
096: * @return the sequent change information object describing the
097: * complete changes made to the sequent together with the operations
098: * result. */
099: public static SequentChangeInfo createSequentChangeInfo(
100: SemisequentChangeInfo anteCI, SemisequentChangeInfo sucCI,
101: Sequent result, Sequent original) {
102: return new SequentChangeInfo(anteCI, sucCI, result, original);
103: }
104:
105: /**
106: * creates a new sequent change information object. Therefore it
107: * combines the changes to the semisequents of the sequent.
108: * @param antecedent the SemisequentChangeInfo describing the changes of
109: * the antecedent
110: * @param succedent the SemisequentChangeInfo describing the changes of
111: * the succedent
112: * @param resultingSequent the Sequent being the result of the changes
113: * @param originalSequent the Sequent that has been transformed
114: */
115: private SequentChangeInfo(SemisequentChangeInfo antecedent,
116: SemisequentChangeInfo succedent, Sequent resultingSequent,
117: Sequent originalSequent) {
118: this .antecedent = antecedent;
119: this .succedent = succedent;
120: this .resultingSequent = resultingSequent;
121: this .originalSequent = originalSequent;
122: }
123:
124: /**
125: * returns true iff the sequent has been changed by the operation
126: * @return true iff the sequent has been changed by the operation
127: */
128: public boolean hasChanged() {
129: return antecedent.hasChanged() || succedent.hasChanged();
130: }
131:
132: /**
133: * returns true if the selected part of sequent has changed. Thereby the
134: * flag 'antec' specifies the selection: true selects the antecedent and
135: * false the succedent of the sequent.
136: *
137: * @return true iff the sequent has been changed by the operation */
138: public boolean hasChanged(boolean antec) {
139: return antec ? (antecedent != null && antecedent.hasChanged())
140: : (succedent != null && succedent.hasChanged());
141: }
142:
143: public SemisequentChangeInfo getSemisequentChangeInfo(boolean antec) {
144: return antec ? antecedent : succedent;
145: }
146:
147: /**
148: * The formulas added to one of the semisequents are returned. The selected
149: * semisequent depends on the value of selector 'antec' which is the
150: * antecedent if 'antec' is true and the succedent otherwise.
151: *
152: * @param antec a boolean used to select one of the two semisequents
153: * of a sequent (true means antecedent; false means succedent)
154: * @return list of formulas added to the selected semisequent
155: */
156: public ListOfConstrainedFormula addedFormulas(boolean antec) {
157: return antec ? (antecedent != null ? antecedent.addedFormulas()
158: : SLListOfConstrainedFormula.EMPTY_LIST)
159: : (succedent != null ? succedent.addedFormulas()
160: : SLListOfConstrainedFormula.EMPTY_LIST);
161: }
162:
163: /**
164: * The formulas added to the sequent are returned as a concatenated list of
165: * the formulas added to each semisequent.
166: * @return list of formulas added to sequent
167: */
168: public ListOfConstrainedFormula addedFormulas() {
169: return addedFormulas(true).size() > addedFormulas(false).size() ? addedFormulas(
170: false).prepend(addedFormulas(true))
171: : addedFormulas(true).prepend(addedFormulas(false));
172: }
173:
174: /**
175: * The formulas removed from one of the semisequents are returned. The
176: * selected semisequent depends on the value of selector 'antec' which is
177: * the antecedent if 'antec' is true and the succedent otherwise.
178: *
179: * @param antec a boolean used to select one of the two semisequents
180: * of a sequent (true means antecedent; false means succedent)
181: * @return list of formulas removed from the selected semisequent
182: */
183: public ListOfConstrainedFormula removedFormulas(boolean antec) {
184: return antec ? (antecedent != null ? antecedent
185: .removedFormulas()
186: : SLListOfConstrainedFormula.EMPTY_LIST)
187: : (succedent != null ? succedent.removedFormulas()
188: : SLListOfConstrainedFormula.EMPTY_LIST);
189: }
190:
191: /**
192: * The formulas removed from the sequent are returned as a
193: * concatenated list of the formulas removed from each semisequent.
194: * @return list of formulas removed from the sequent
195: */
196: public ListOfConstrainedFormula removedFormulas() {
197: return removedFormulas(true).size() > removedFormulas(false)
198: .size() ? removedFormulas(false).prepend(
199: removedFormulas(true)) : removedFormulas(true).prepend(
200: removedFormulas(false));
201: }
202:
203: /**
204: * The formulas modified within one of the semisequents are
205: * returned. The selected semisequent depends on the value of
206: * selector 'antec' which is the antecedent if 'antec' is true and
207: * the succedent otherwise.
208: *
209: * @param antec a boolean used to select one of the two semisequents
210: * of a sequent (true means antecedent; false means succedent)
211: * @return list of formulas modified within the selected semisequent
212: */
213: public ListOfFormulaChangeInfo modifiedFormulas(boolean antec) {
214: return antec ? (antecedent != null ? antecedent
215: .modifiedFormulas()
216: : SLListOfFormulaChangeInfo.EMPTY_LIST)
217: : (succedent != null ? succedent.modifiedFormulas()
218: : SLListOfFormulaChangeInfo.EMPTY_LIST);
219: }
220:
221: /**
222: * The formulas modified within the sequent are returned as a
223: * concatenated list of the formulas modified within each each
224: * semisequent.
225: * @return list of formulas modified to sequent
226: */
227: public ListOfFormulaChangeInfo modifiedFormulas() {
228: return modifiedFormulas(true).size() > modifiedFormulas(false)
229: .size() ? modifiedFormulas(false).prepend(
230: modifiedFormulas(true)) : modifiedFormulas(true)
231: .prepend(modifiedFormulas(false));
232: }
233:
234: /**
235: * Returns the formulas that have been rejected when trying to add as being redundant.
236: * @param antec a boolean used to select one of the two semisequents
237: * of a sequent (true means antecedent; false means succedent)
238: * @return list of formulas rejected when trying to add to the selected semisequent
239: */
240: public ListOfConstrainedFormula rejectedFormulas(boolean antec) {
241: return antec ? (antecedent != null ? antecedent
242: .rejectedFormulas()
243: : SLListOfConstrainedFormula.EMPTY_LIST)
244: : (succedent != null ? succedent.rejectedFormulas()
245: : SLListOfConstrainedFormula.EMPTY_LIST);
246: }
247:
248: /**
249: * Returns the formulas that have been rejected when trying to add as being redundant.
250: * @return list of rejected formulas
251: */
252: public ListOfConstrainedFormula rejectedFormulas() {
253: return rejectedFormulas(true).size() > rejectedFormulas(false)
254: .size() ? rejectedFormulas(false).prepend(
255: rejectedFormulas(true)) : rejectedFormulas(true)
256: .prepend(rejectedFormulas(false));
257: }
258:
259: /**
260: * @return the original sequent
261: */
262: public Sequent getOriginalSequent() {
263: return originalSequent;
264: }
265:
266: /**
267: * returns the resulting sequent
268: * @return the resulting sequent
269: */
270: public Sequent sequent() {
271: return resultingSequent;
272: }
273:
274: /**
275: * toString helper
276: */
277: private String toStringHelp(boolean antec) {
278: String result = "";
279: if (hasChanged(antec)) {
280: result += "\t added:" + addedFormulas(antec);
281: result += "\t removed:" + removedFormulas(antec);
282: result += "\t modified:" + modifiedFormulas(antec);
283: }
284: return result;
285: }
286:
287: /**
288: * toString
289: */
290: public String toString() {
291: String result = "antecedent: " + hasChanged(true);
292: result += toStringHelp(true);
293:
294: result += "\n succedent: " + hasChanged(false);
295: result += toStringHelp(false);
296:
297: return result;
298: }
299:
300: }
|