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.proof;
012:
013: import java.util.HashMap;
014:
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.util.Debug;
017:
018: /**
019: * Class to manage the tags of the formulas of a sequent (node). Instances of
020: * this class are stored by instances of the <code>Goal</code> class, and are
021: * not immutable
022: */
023: public class FormulaTagManager {
024:
025: /** Maps for the assignment of tags to formulas and vice versa */
026:
027: /** Key: FormulaTag Value: FormulaInfo */
028: private final HashMap tagToFormulaInfo;
029:
030: /** Key: PosInOccurrence Value: FormulaTag */
031: private final HashMap pioToTag;
032:
033: /**
034: * Create a new manager that is initialised with the formulas of the given
035: * sequent
036: */
037: FormulaTagManager(Goal p_goal) {
038: tagToFormulaInfo = new HashMap();
039: pioToTag = new HashMap();
040: createNewTags(p_goal);
041: }
042:
043: private FormulaTagManager(HashMap p_tagToPIO, HashMap p_pioToTag) {
044: tagToFormulaInfo = p_tagToPIO;
045: pioToTag = p_pioToTag;
046: }
047:
048: /**
049: * @return the tag of the formula at the given position
050: */
051: public FormulaTag getTagForPos(PosInOccurrence p_pio) {
052: return (FormulaTag) pioToTag.get(p_pio);
053: }
054:
055: /**
056: * @return The current position of the formula with the given tag; the
057: * sequent attribute of the returned <code>PosInOccurrence</code> can
058: * be obsolete and refer to a previous node. If no formula is assigned to
059: * the given tag, <code>null</code> is returned
060: */
061: public PosInOccurrence getPosForTag(FormulaTag p_tag) {
062: final FormulaInfo info = getFormulaInfo(p_tag);
063: if (info == null)
064: return null;
065: return info.pio;
066: }
067:
068: /**
069: * @return The age (as obtained by <code>Goal.getTime()</code>) of the
070: * formula, i.e. the time when the formula was introduced resp. when
071: * the last modification was applied to the formula. If no formula
072: * is assigned to the given tag, <code>0</code> is returned
073: */
074: public long getAgeForTag(FormulaTag p_tag) {
075: final FormulaInfo info = getFormulaInfo(p_tag);
076: if (info == null)
077: return 0;
078: return info.age;
079: }
080:
081: /**
082: * @return All modifications that were applied to the formula
083: * with the given tag since the creation of the tag, starting with the
084: * most recent one
085: */
086: public ListOfFormulaChangeInfo getModifications(FormulaTag p_tag) {
087: return getFormulaInfo(p_tag).modifications;
088: }
089:
090: public void sequentChanged(Goal source, SequentChangeInfo sci) {
091: removeTags(sci, true, source);
092: removeTags(sci, false, source);
093:
094: updateTags(sci, true, source);
095: updateTags(sci, false, source);
096:
097: addTags(sci, true, source);
098: addTags(sci, false, source);
099: }
100:
101: private void updateTags(SequentChangeInfo sci, boolean p_antec,
102: Goal p_goal) {
103: final IteratorOfFormulaChangeInfo infoIt = sci
104: .modifiedFormulas(p_antec).iterator();
105: while (infoIt.hasNext())
106: updateTag(infoIt.next(), sci.sequent(), p_goal);
107: }
108:
109: private void addTags(SequentChangeInfo sci, boolean p_antec,
110: Goal p_goal) {
111: final IteratorOfConstrainedFormula cfmaIt = sci.addedFormulas(
112: p_antec).iterator();
113: while (cfmaIt.hasNext()) {
114: final PosInOccurrence pio = new PosInOccurrence(cfmaIt
115: .next(), PosInTerm.TOP_LEVEL, p_antec);
116: createNewTag(pio, p_goal);
117: }
118: }
119:
120: private void removeTags(SequentChangeInfo sci, boolean p_antec,
121: Goal p_goal) {
122: final IteratorOfConstrainedFormula cfmaIt = sci
123: .removedFormulas(p_antec).iterator();
124: while (cfmaIt.hasNext()) {
125: final PosInOccurrence pio = new PosInOccurrence(cfmaIt
126: .next(), PosInTerm.TOP_LEVEL, p_antec);
127: removeTag(pio);
128: }
129: }
130:
131: public Object clone() {
132: return new FormulaTagManager(
133: (HashMap) tagToFormulaInfo.clone(), (HashMap) pioToTag
134: .clone());
135: }
136:
137: public FormulaTagManager copy() {
138: return (FormulaTagManager) clone();
139: }
140:
141: /**
142: * Create new tags for all formulas of a sequent
143: * @param p_goal The sequent
144: */
145: private void createNewTags(Goal p_goal) {
146: createNewTags(p_goal, false);
147: createNewTags(p_goal, true);
148: }
149:
150: /**
151: * Create new tags for all formulas of a semisequent
152: * @param p_goal The sequent that contains the semisequent
153: * @param p_antec true iff the formulas of the antecedent should be added
154: */
155: private void createNewTags(Goal p_goal, boolean p_antec) {
156: final Sequent seq = p_goal.sequent();
157: final Semisequent ss = p_antec ? seq.antecedent() : seq
158: .succedent();
159: final IteratorOfConstrainedFormula cfmaIt = ss.iterator();
160:
161: while (cfmaIt.hasNext()) {
162: final PosInOccurrence pio = new PosInOccurrence(cfmaIt
163: .next(), PosInTerm.TOP_LEVEL, p_antec);
164: createNewTag(pio, p_goal);
165: }
166: }
167:
168: /**
169: * Add a new tag to the maps
170: * @param p_pio The formula for which a new tag is supposed to be created
171: */
172: private void createNewTag(PosInOccurrence p_pio, Goal p_goal) {
173: final FormulaTag tag = new FormulaTag();
174: tagToFormulaInfo.put(tag, new FormulaInfo(p_pio, p_goal
175: .getTime()));
176: pioToTag.put(p_pio, tag);
177: }
178:
179: /**
180: * Remove the entries for the given formulas from the maps
181: */
182: private void removeTag(PosInOccurrence p_pio) {
183: final FormulaTag tag = getTagForPos(p_pio);
184:
185: Debug.assertFalse(tag == null,
186: "Tried to remove a tag that does not exist");
187:
188: tagToFormulaInfo.remove(tag);
189: putInQueryCache(tag, null);
190: pioToTag.remove(p_pio);
191: }
192:
193: private void updateTag(FormulaChangeInfo p_info, Sequent p_newSeq,
194: Goal p_goal) {
195: final PosInOccurrence oldPIO = p_info
196: .getPositionOfModification().topLevel();
197: final FormulaTag tag = getTagForPos(oldPIO);
198: final FormulaInfo oldInfo = getFormulaInfo(tag);
199: final FormulaInfo newInfo = oldInfo.addModification(p_info,
200: p_newSeq, p_goal.getTime());
201:
202: tagToFormulaInfo.put(tag, newInfo);
203: putInQueryCache(tag, newInfo);
204: pioToTag.remove(oldPIO);
205: pioToTag.put(newInfo.pio, tag);
206: }
207:
208: ////////////////////////////////////////////////////////////////////////////
209: // Simple cache for <code>getFormulaInfo</code>
210:
211: private FormulaTag lastTagQueried = null;
212: private FormulaInfo lastQueryResult = null;
213:
214: private void putInQueryCache(FormulaTag p_tag, FormulaInfo p_info) {
215: lastTagQueried = p_tag;
216: lastQueryResult = p_info;
217: }
218:
219: ////////////////////////////////////////////////////////////////////////////
220:
221: private FormulaInfo getFormulaInfo(FormulaTag p_tag) {
222: if (lastTagQueried != p_tag)
223: putInQueryCache(p_tag, (FormulaInfo) tagToFormulaInfo
224: .get(p_tag));
225: return lastQueryResult;
226: }
227:
228: /**
229: * Class that holds information about a formula, namely the current position
230: * (<code>PosInOccurrence</code>) as well as a list of the modifications
231: * that have been applied to the formula so far. Instances of this class
232: * are immutable
233: */
234: private static class FormulaInfo {
235: public final PosInOccurrence pio;
236: /** All modifications that have been applied to the formula
237: * since the creation of the tag. The most recent modification
238: * is the first element of the list */
239: public final ListOfFormulaChangeInfo modifications;
240:
241: /**
242: * The age (as obtained by <code>Goal.getTime()</code>) of the formula,
243: * i.e. the time when the formula was introduced resp. when the last
244: * modification was applied to the formula
245: */
246: public final long age;
247:
248: public FormulaInfo(PosInOccurrence p_pio, long p_age) {
249: this (p_pio, SLListOfFormulaChangeInfo.EMPTY_LIST, p_age);
250: }
251:
252: private FormulaInfo(PosInOccurrence p_pio,
253: ListOfFormulaChangeInfo p_modifications, long p_age) {
254: pio = p_pio;
255: modifications = p_modifications;
256: age = p_age;
257: }
258:
259: public FormulaInfo addModification(FormulaChangeInfo p_info,
260: Sequent p_newSeq, long p_age) {
261: final PosInOccurrence newPIO = new PosInOccurrence(p_info
262: .getNewFormula(), PosInTerm.TOP_LEVEL, pio
263: .isInAntec());
264:
265: return new FormulaInfo(newPIO, modifications
266: .prepend(p_info), p_age);
267: }
268: }
269:
270: }
|