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.strategy;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.BooleanContainer;
015: import de.uka.ilkd.key.logic.Constraint;
016: import de.uka.ilkd.key.logic.PosInOccurrence;
017: import de.uka.ilkd.key.proof.Goal;
018: import de.uka.ilkd.key.proof.Proof;
019: import de.uka.ilkd.key.proof.RuleAppIndex;
020: import de.uka.ilkd.key.rule.RuleApp;
021: import de.uka.ilkd.key.rule.TacletApp;
022:
023: public class QueueRuleApplicationManager implements
024: AutomatedRuleApplicationManager {
025:
026: /** The goal this manager belongs to */
027: private Goal goal = null;
028:
029: /** The priority queue containing all possible next rule applications,
030: * ordered by the costs the strategy object has assigned to them */
031: private HeapOfRuleAppContainer queue = null;
032:
033: private HeapOfRuleAppContainer secQueue = null;
034:
035: /** rule apps that have been deferred during the last call
036: * of <code>next</code>, but that could be still relevant */
037: private ListOfRuleAppContainer workingList = null;
038:
039: private static final int PRIMARY_QUEUE = 0;
040: private static final int SECONDARY_QUEUE = 1;
041: private static final int WORKING_LIST = 2;
042:
043: private RuleApp nextRuleApp = null;
044: private long nextRuleTime;
045: private RuleAppCost nextRuleAppCost = null;
046:
047: public void setGoal(Goal p_goal) {
048: goal = p_goal;
049: }
050:
051: /**
052: * Clear the heap of applicable rules
053: */
054: public void clearCache() {
055: queue = null;
056: secQueue = null;
057: workingList = null;
058: clearNextRuleApp();
059: }
060:
061: /**
062: * Add all rules to the heap that are not reported via the <code>RuleListener</code>
063: * connection
064: */
065: private void ensureQueueExists() {
066: if (queue != null)
067: return;
068:
069: if (getGoal() == null) {
070: clearCache();
071: return;
072: }
073:
074: queue = LeftistHeapOfRuleAppContainer.EMPTY_HEAP;
075: secQueue = LeftistHeapOfRuleAppContainer.EMPTY_HEAP;
076: workingList = SLListOfRuleAppContainer.EMPTY_LIST;
077:
078: // to support encapsulating rule managers (delegation, like in
079: // <code>FocussedRuleApplicationManager</code>) the rule index
080: // reports its contents to the rule manager of the goal, which is not
081: // necessarily this object
082: getGoal().ruleAppIndex().reportAutomatedRuleApps(
083: getGoal().getRuleAppManager(), getServices(),
084: getUserConstraint());
085: // printQueue(queue);
086: }
087:
088: /**
089: * Implementation of the method from <code>NewRuleListener</code>. The new
090: * rule app is added to the heap
091: */
092: public void ruleAdded(RuleApp rule, PosInOccurrence pos) {
093: //System.out.println ( "Rule added: " + rule + "\n");
094:
095: // ensureQueueExists ();
096:
097: if (queue == null)
098: // then the heap has to be rebuilt completely anyway, and the new
099: // rule app is not of interest for us
100: return;
101:
102: push(RuleAppContainer.createAppContainers(rule, pos, getGoal(),
103: getStrategy()).iterator(), PRIMARY_QUEUE);
104: }
105:
106: /**
107: * Add a number of new rule apps to the heap
108: */
109: private void push(IteratorOfRuleAppContainer it, int target) {
110: while (it.hasNext())
111: push(it.next(), target);
112: }
113:
114: /**
115: * Add a new rule app to the heap, provided that the rule app is not
116: * infinitely expensive
117: */
118: private void push(RuleAppContainer c, int target) {
119: if (c.getCost() instanceof TopRuleAppCost)
120: return;
121:
122: switch (target) {
123: case PRIMARY_QUEUE:
124: queue = queue.insert(c);
125: break;
126: case SECONDARY_QUEUE:
127: secQueue = secQueue.insert(c);
128: break;
129: case WORKING_LIST:
130: workingList = workingList.prepend(c);
131: break;
132: }
133: }
134:
135: /**
136: * @return the first applicable rule app, i.e. the least expensive element
137: * of the heap that is not obsolete and caches the result of this
138: * operation to save some time the next time the method
139: * nextAndCache() or next() is called. A call of next() empties the
140: * cache again.
141: */
142: public RuleApp peekNext() {
143: ensureNextRuleAppExists();
144: return nextRuleApp;
145: }
146:
147: public RuleAppCost peekCost() {
148: ensureNextRuleAppExists();
149: return nextRuleAppCost;
150: }
151:
152: /**
153: * @return the first applicable rule app, i.e. the least expensive element
154: * of the heap that is not obsolete
155: */
156: public RuleApp next() {
157: ensureNextRuleAppExists();
158:
159: final RuleApp res = nextRuleApp;
160: clearNextRuleApp();
161:
162: return res;
163: }
164:
165: private void clearNextRuleApp() {
166: nextRuleApp = null;
167: nextRuleAppCost = null;
168: }
169:
170: private void ensureNextRuleAppExists() {
171: ensureQueueExists();
172:
173: final long currentTime = getGoal().getTime();
174: if (currentTime != nextRuleTime) {
175: clearNextRuleApp();
176: nextRuleTime = currentTime;
177: }
178:
179: if (nextRuleApp != null)
180: return;
181:
182: final RuleAppIndex index = getGoal().ruleAppIndex();
183: index.fillCache();
184:
185: // printQueue(queue);
186: // printQueue(secQueue);
187:
188: createFurtherApps();
189:
190: ensureNextRuleAppExistsHelp();
191:
192: // System.out.println("Queue size: " + queue.size());
193: // System.out.println("Secondary queue size: " + secQueue.size());
194: // System.out.println("Working list size: " + workingList.size());
195:
196: queue = queue.insert(secQueue);
197: secQueue = LeftistHeapOfRuleAppContainer.EMPTY_HEAP;
198: }
199:
200: private void ensureNextRuleAppExistsHelp() {
201: final BooleanContainer secondaryQueueUsed = new BooleanContainer();
202: clearNextRuleApp();
203:
204: while (nextRuleApp == null
205: && (!queue.isEmpty() || !secQueue.isEmpty())) {
206: final RuleAppContainer c = getMinRuleApp(secondaryQueueUsed);
207: // printContainer ( "considering rule ", c );
208:
209: nextRuleApp = c.completeRuleApp(getGoal(), getStrategy());
210:
211: if (nextRuleApp == null) {
212: if (!secondaryQueueUsed.val())
213: createFurtherRuleApps(c, true);
214: else
215: push(c, WORKING_LIST);
216: } else {
217: nextRuleAppCost = c.getCost();
218:
219: // the found rule app will be re-evaluated when calling
220: // <code>next()</code> the next time; all other considered rule
221: // apps can be put into the primary queue immediately
222: queue = queue.insert(workingList.iterator());
223: workingList = SLListOfRuleAppContainer.EMPTY_LIST;
224: push(c, WORKING_LIST);
225: }
226:
227: // if (res != null) {
228: // printContainer ( "selected rule ", c );
229: // }
230: }
231: }
232:
233: private RuleAppContainer getMinRuleApp(
234: BooleanContainer usedSecondary) {
235: if (queue.isEmpty()) {
236: usedSecondary.setVal(true);
237: final RuleAppContainer c = secQueue.findMin();
238: secQueue = secQueue.deleteMin();
239: return c;
240: }
241:
242: if (secQueue.isEmpty()) {
243: usedSecondary.setVal(false);
244: final RuleAppContainer c = queue.findMin();
245: queue = queue.deleteMin();
246: return c;
247: }
248:
249: final RuleAppContainer priC = queue.findMin();
250: final RuleAppContainer secC = secQueue.findMin();
251:
252: usedSecondary.setVal(priC.compareTo(secC) > 0);
253:
254: if (usedSecondary.val()) {
255: secQueue = secQueue.deleteMin();
256: return secC;
257: } else {
258: queue = queue.deleteMin();
259: return priC;
260: }
261: }
262:
263: /**
264: * Call the method <code>createFurtherApps</code> for all elements of
265: * the list <code>consideredRecently</code>, and clear the list. The new
266: * rule apps are added to the heap
267: */
268: private void createFurtherApps() {
269: final IteratorOfRuleAppContainer it = workingList.iterator();
270: workingList = SLListOfRuleAppContainer.EMPTY_LIST;
271:
272: while (it.hasNext())
273: createFurtherRuleApps(it.next(), true);
274: }
275:
276: private void createFurtherRuleApps(RuleAppContainer app,
277: boolean secondary) {
278: push(
279: app.createFurtherApps(getGoal(), getStrategy())
280: .iterator(), secondary ? SECONDARY_QUEUE
281: : PRIMARY_QUEUE);
282: }
283:
284: /**
285: * The goal this manager belongs to
286: */
287: private Goal getGoal() {
288: return goal;
289: }
290:
291: private Services getServices() {
292: return getProof().getServices();
293: }
294:
295: private Constraint getUserConstraint() {
296: return getProof().getUserConstraint().getConstraint();
297: }
298:
299: private Proof getProof() {
300: return getGoal().proof();
301: }
302:
303: private Strategy getStrategy() {
304: return getGoal().getGoalStrategy();
305: }
306:
307: public AutomatedRuleApplicationManager copy() {
308: return (AutomatedRuleApplicationManager) clone();
309: }
310:
311: public Object clone() {
312: QueueRuleApplicationManager res = new QueueRuleApplicationManager();
313: res.queue = queue;
314: res.secQueue = secQueue;
315: res.workingList = workingList;
316: return res;
317: }
318:
319: void printQueue(HeapOfRuleAppContainer p_queue) {
320: IteratorOfRuleAppContainer it = p_queue.sortedIterator();
321:
322: System.out.println("---- start of queue ----");
323:
324: int n = 0;
325: while (it.hasNext()) {
326: n++;
327: final RuleAppContainer container = it.next();
328:
329: final String prefix = n + ") ";
330: printContainer(prefix, container);
331: }
332:
333: System.out.println("---- end of queue ----");
334: }
335:
336: private void printContainer(String prefix,
337: RuleAppContainer container) {
338: final RuleApp ruleApp = container.getRuleApp();
339: String message = prefix + ruleApp.rule().name() + " with cost "
340: + container.getCost();
341:
342: if (ruleApp instanceof TacletApp) {
343: TacletApp tacletApp = (TacletApp) ruleApp;
344: if (!tacletApp.ifInstsComplete()) {
345: message = message + " (unmatched if-formulas)";
346: }
347: if (!tacletApp.instsSufficientlyComplete()) {
348: message = message + " (incomplete)";
349: }
350: }
351:
352: System.out.println(message);
353: }
354: }
|