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 semisequent. Keeps track of added and
015: * removed formula to the semisequents.
016: */
017: public class SemisequentChangeInfo implements java.io.Serializable {
018:
019: /** contains the added formulas to the semisequent */
020: private ListOfConstrainedFormula added = SLListOfConstrainedFormula.EMPTY_LIST;
021: /** contains the removed formulas from the semisequent */
022: private ListOfConstrainedFormula removed = SLListOfConstrainedFormula.EMPTY_LIST;
023: /** contains the modified formulas from the semisequent */
024: private ListOfFormulaChangeInfo modified = SLListOfFormulaChangeInfo.EMPTY_LIST;
025: /** stores the redundance free formula list of the semisequent */
026: private ListOfConstrainedFormula modifiedSemisequent = SLListOfConstrainedFormula.EMPTY_LIST;
027: /**
028: * contains formulas that have been tried to add, but which have been rejected due to
029: * already existing formulas in the sequent subsuming these formulas
030: */
031: public ListOfConstrainedFormula rejected = SLListOfConstrainedFormula.EMPTY_LIST;
032:
033: /** */
034: private int lastFormulaIndex = -1;
035:
036: /** the resulting semisequent */
037: private Semisequent semisequent;
038:
039: public SemisequentChangeInfo() {
040: }
041:
042: public SemisequentChangeInfo(ListOfConstrainedFormula formulas) {
043: this .modifiedSemisequent = formulas;
044: }
045:
046: /**
047: * returns true if the semisequent has changed
048: */
049: public boolean hasChanged() {
050: return added != SLListOfConstrainedFormula.EMPTY_LIST
051: || removed != SLListOfConstrainedFormula.EMPTY_LIST
052: || modified != SLListOfFormulaChangeInfo.EMPTY_LIST;
053: }
054:
055: /**
056: * sets the list of constrained formula containing all formulas of
057: * the semisequent after the operation
058: */
059: public void setFormulaList(ListOfConstrainedFormula list) {
060: modifiedSemisequent = list;
061: }
062:
063: /**
064: * returns the list of constrained formula of the new semisequent
065: */
066: public ListOfConstrainedFormula getFormulaList() {
067: return modifiedSemisequent;
068: }
069:
070: /**
071: * logs an added formula at position idx
072: */
073: public void addedFormula(int idx, ConstrainedFormula cf) {
074: added = added.prepend(cf);
075: lastFormulaIndex = idx;
076: }
077:
078: /**
079: * logs a modified formula at position idx
080: */
081: public void modifiedFormula(int idx, FormulaChangeInfo fci) {
082: // This information can overwrite older records about removed
083: // formulas
084: removed = removed.removeAll(fci.getPositionOfModification()
085: .constrainedFormula());
086: modified = modified.prepend(fci);
087: lastFormulaIndex = idx;
088: }
089:
090: /**
091: * returns the list of all added constrained formulas
092: * @return ListOfConstrainedFormula added to the semisequent
093: */
094: public ListOfConstrainedFormula addedFormulas() {
095: return added;
096: }
097:
098: /**
099: * returns the list of all removed constrained formulas
100: * @return ListOfConstrainedFormula removed from the semisequent
101: */
102: public ListOfConstrainedFormula removedFormulas() {
103: return removed;
104: }
105:
106: /**
107: * returns a list of formulas that have been tried to add to
108: * the semisequent but got rejected as they were redundant
109: * @return list of formulas rejected due to redundancy
110: */
111: public ListOfConstrainedFormula rejectedFormulas() {
112: return this .rejected;
113: }
114:
115: /**
116: * adding formula <tt>f</tt> to the semisequent failed due to
117: * a redundance check. This means an equal or stronger formula
118: * is already present in the semisequent
119: * @param f the ConstrainedFormula
120: */
121: public void rejectedFormula(ConstrainedFormula f) {
122: this .rejected = this .rejected.append(f);
123: }
124:
125: /**
126: * returns the list of all modification positions
127: * @return ListOfConstrainedFormula modified within the
128: * semisequent
129: */
130: public ListOfFormulaChangeInfo modifiedFormulas() {
131: return modified;
132: }
133:
134: /**
135: * logs an added formula at position idx
136: */
137: public void removedFormula(int idx, ConstrainedFormula cf) {
138: removed = removed.prepend(cf);
139:
140: lastFormulaIndex = (lastFormulaIndex == idx) ? -1
141: : lastFormulaIndex > idx ? lastFormulaIndex - 1
142: : lastFormulaIndex;
143:
144: if (lastFormulaIndex < -1) {
145: lastFormulaIndex = -1;
146: }
147:
148: }
149:
150: /**
151: * returns the index of the last added formula
152: */
153: public int getIndex() {
154: return lastFormulaIndex;
155: }
156:
157: /**
158: * sets the resulting semisequent
159: */
160: public void setSemisequent(Semisequent semisequent) {
161: this .semisequent = semisequent;
162: }
163:
164: /**
165: * returns the semisequent that is the result of the change
166: * operation
167: */
168: public Semisequent semisequent() {
169: return semisequent;
170: }
171:
172: /**
173: * toString
174: */
175: public String toString() {
176: return "changed:" + hasChanged() + "\n added (pos):" + added
177: + "(" + lastFormulaIndex + ")" + "\n removed:"
178: + removed + "\n modified:" + modified
179: + "\n rejected:" + rejected + "\n new semisequent:"
180: + modifiedSemisequent;
181: }
182:
183: }
|