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.feature.instantiator;
012:
013: import java.util.ArrayList;
014: import java.util.Stack;
015:
016: import de.uka.ilkd.key.rule.RuleApp;
017:
018: /**
019: * Manager for the <code>ChoicePoint</code>s that can occur during the
020: * evaluation of a feature term, taking care of the different branches offered
021: * by the points, and that is able to systematically explore the resulting
022: * search space and enumerate all resulting rule applications.
023: * <code>ChoicePoint</code>s have to register themselves (using method
024: * <code>passChoicePoint</code>) each time they are invoked during evaluation
025: * of the feature term, and are asked by the manager for their branches. The
026: * manager simulates a backtracking behaviour by repeated evaluation of the
027: * feature term.
028: */
029: public class BackTrackingManager {
030:
031: /**
032: * The original rule application in question, i.e., the application without
033: * the changes that can possibly be applied by <code>ChoicePoint</code>s
034: */
035: private RuleApp initialApp = null;
036:
037: /**
038: * Stack of <code>IteratorOfCPBranch</code>: the branches of
039: * <code>ChoicePoint</code>s that have not yet been taken, the branches
040: * of later points being further up in the stack
041: */
042: private final Stack choices = new Stack();
043:
044: /**
045: * List of <code>CPBranch</code>: the branches that are taken in the
046: * current evaluation run
047: */
048: private final ArrayList chosenBranches = new ArrayList();
049:
050: /**
051: * The position within <code>choices</code> during the current evaluation
052: * run (the number of <code>ChoicePoint</code>s that occured so far
053: * during the current evaluation)
054: */
055: private int position = 0;
056:
057: /**
058: * Method that has to be invoked by each feature that represents a choice
059: * point, each time the feature is invoked during evaluation of the feature
060: * term
061: *
062: * @param cp
063: * the <code>ChoicePoint</code> in question (which does not
064: * have to be the same object as the feature, and which does not
065: * have to be the same object over different evaluations of the
066: * feature term)
067: * @param ticket
068: * a unique object (as unique as possible) that has to be
069: * provided by the feature in order to ensure that the same
070: * sequence of choice points occurs during the next evaluation
071: * run (after backtracking). The <code>ticket</code> must not
072: * change between two evaluation runs of the feature term
073: */
074: public void passChoicePoint(ChoicePoint cp, Object ticket) {
075: assert initialApp != null;
076: assertValidTicket(ticket);
077: assert chosenBranches.size() == choices.size();
078:
079: if (position == choices.size()) {
080: // phase where we have to ask the choice-points for possibilities
081: addChoicePoint(cp);
082: } else {
083: assert choices.size() > position;
084: // phase where we have to "replay" choices that have already
085: // been made
086: ((CPBranch) chosenBranches.get(position)).choose();
087: }
088:
089: ++position;
090:
091: }
092:
093: /**
094: * Method that has to be called before a sequence of evaluation runs of a
095: * feature term.
096: *
097: * @param initialApp
098: * the original rule application in question
099: */
100: public void setup(RuleApp initialApp) {
101: this .initialApp = initialApp;
102: choices.clear();
103: chosenBranches.clear();
104: tickets.clear();
105: position = 0;
106: }
107:
108: /**
109: * In the end of an evaluation run of a feature term, this method has to be
110: * called for checking whether it is possible to backtrack and whether a
111: * further evaluation run is necessary
112: *
113: * @return <code>true</code> iff there are paths left to explore, i.e., if
114: * evaluation should run a further time
115: */
116: public boolean backtrack() {
117: position = 0;
118:
119: while (!choices.isEmpty()) {
120: final IteratorOfCPBranch chs = (IteratorOfCPBranch) choices
121: .pop();
122: chosenBranches.remove(chosenBranches.size() - 1);
123:
124: if (chs.hasNext()) {
125: pushChoices(chs, chs.next());
126: return true;
127: }
128:
129: tickets.remove(tickets.size() - 1);
130: }
131:
132: // make sure that no further choicepoints occur until <code>setup</code>
133: // is invoked the next time
134: setup(null);
135:
136: return false;
137: }
138:
139: /**
140: * @return the resulting rule application when all choice points have
141: * applied their modifications
142: */
143: public RuleApp getResultingapp() {
144: return getOldRuleApp();
145: }
146:
147: private void pushChoices(IteratorOfCPBranch remainingChoices,
148: CPBranch chosen) {
149: choices.push(remainingChoices);
150: chosenBranches.add(chosen);
151: }
152:
153: private void addChoicePoint(ChoicePoint cp) {
154: final RuleApp oldApp = getOldRuleApp();
155: if (oldApp == null) {
156: // This means that an earlier <code>ChoicePoint</code> did not have
157: // any branches. It is necessary to backtrack and to choose a
158: // different branch for one of the <code>ChoicePoint</code>s before
159: // the failing <code>ChoicePoint</code>, but first we have to finish
160: // the current evaluation run of the feature term
161: cancelChoicePoint();
162: return;
163: }
164:
165: final IteratorOfCPBranch chs = cp.getBranches(oldApp);
166: if (!chs.hasNext()) {
167: // This <code>ChoicePoint</code> does not have any branches
168: cancelChoicePoint();
169: return;
170: }
171:
172: final CPBranch chosen = chs.next();
173: pushChoices(chs, chosen);
174: chosen.choose();
175: }
176:
177: private void cancelChoicePoint() {
178: pushChoices(SLListOfCPBranch.EMPTY_LIST.iterator(), null);
179: }
180:
181: /**
182: * List of <code>Object</code>: each <code>ChoicePoint</code> has to
183: * install a ticket, which is used as a sanity check when the evaluation of
184: * a feature term is repeated. This is a simple runtime measure for ensuring
185: * that the feature evaluation is deterministic
186: */
187: private final ArrayList tickets = new ArrayList();
188:
189: private void assertValidTicket(Object ticket) {
190: if (tickets.size() > position) {
191: assert tickets.get(position) == ticket;
192: } else {
193: assert tickets.size() == position;
194: tickets.add(ticket);
195: }
196: }
197:
198: private RuleApp getOldRuleApp() {
199: if (chosenBranches.isEmpty())
200: return initialApp;
201: final CPBranch branch = (CPBranch) chosenBranches
202: .get(position - 1);
203: if (branch == null)
204: return null;
205: return branch.getRuleAppForBranch();
206: }
207:
208: }
|