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: /**
014: * Helper class for managing a list of goals on which rules are applied.
015: * The class provides methods for removing a goal, and for updating the internal
016: * data structures after a rule has been applied.
017: */
018: public class DefaultGoalChooser implements IGoalChooser {
019:
020: /** the proof that is worked with */
021: private Proof proof;
022:
023: /** list of goals on which the strategy should be applied */
024: private ListOfGoal goalList;
025:
026: /** part of goalList that should be worked on next */
027: private ListOfGoal nextGoals;
028:
029: /** true iff all goals have satisfiable constraints */
030: private boolean allGoalsSatisfiable = false;
031:
032: /**
033: * Subset of the goals to which currently taclets are applied. First this
034: * is the list of goals with unsatisfiable constraints, later this is a
035: * subset of the goals having inconsistent constraints
036: */
037: protected ListOfGoal selectedList;
038:
039: private Node currentSubtreeRoot = null;
040:
041: public DefaultGoalChooser() {
042: }
043:
044: /* (non-Javadoc)
045: * @see de.uka.ilkd.key.proof.IGoalChooser#init(de.uka.ilkd.key.proof.Proof, de.uka.ilkd.key.proof.ListOfGoal)
046: */
047: public void init(Proof p_proof, ListOfGoal p_goals) {
048: allGoalsSatisfiable = false;
049: currentSubtreeRoot = null;
050: proof = p_proof;
051: setupGoals(p_goals);
052: }
053:
054: private void setupGoals(ListOfGoal p_goals) {
055: goalList = SLListOfGoal.EMPTY_LIST;
056: selectedList = SLListOfGoal.EMPTY_LIST;
057: nextGoals = SLListOfGoal.EMPTY_LIST;
058:
059: if (allGoalsSatisfiable) {
060: goalList = p_goals;
061: findMinimalSubtree(currentSubtreeRoot);
062: } else {
063: final IteratorOfGoal it = p_goals.iterator();
064:
065: while (it.hasNext()) {
066: final Goal goal = it.next();
067:
068: if (goal.getClosureConstraint().isSatisfiable())
069: goalList = goalList.prepend(goal);
070: else
071: selectedList = selectedList.prepend(goal);
072: }
073:
074: allGoalsSatisfiable = selectedList.isEmpty();
075:
076: if (allGoalsSatisfiable)
077: findMinimalSubtreeBelow(proof.root());
078: }
079: }
080:
081: private int nextGoalCounter = 0;
082:
083: /* (non-Javadoc)
084: * @see de.uka.ilkd.key.proof.IGoalChooser#getNextGoal()
085: */
086: public Goal getNextGoal() {
087: Goal result;
088:
089: if (allGoalsSatisfiable) {
090: if (nextGoals.isEmpty())
091: nextGoals = selectedList;
092:
093: if (nextGoals.isEmpty()) {
094: result = null;
095: } else {
096: result = nextGoals.head();
097: nextGoals = nextGoals.tail();
098: }
099: } else {
100: ++nextGoalCounter;
101: if (nextGoalCounter % 100 == 0)
102: selectedList = rotateList(selectedList);
103:
104: result = selectedList.isEmpty() ? null : selectedList
105: .head();
106: }
107:
108: return result;
109: }
110:
111: /* (non-Javadoc)
112: * @see de.uka.ilkd.key.proof.IGoalChooser#removeGoal(de.uka.ilkd.key.proof.Goal)
113: */
114: public void removeGoal(Goal p_goal) {
115: selectedList = selectedList.removeAll(p_goal);
116: nextGoals = SLListOfGoal.EMPTY_LIST;
117:
118: if (selectedList.isEmpty())
119: setupGoals(goalList);
120: }
121:
122: /* (non-Javadoc)
123: * @see de.uka.ilkd.key.proof.IGoalChooser#updateGoalList(de.uka.ilkd.key.proof.Node, de.uka.ilkd.key.proof.ListOfGoal)
124: */
125: public void updateGoalList(Node node, ListOfGoal newGoals) {
126: if (newGoals.isEmpty()
127: || (newGoals.tail().isEmpty() && newGoals.head().node() == node)) {
128: // Goals (may) have been closed, remove them from the goal lists
129: removeClosedGoals();
130: } else {
131: updateGoalListHelp(node, newGoals);
132: }
133:
134: if (proof.openGoals().isEmpty())
135: // proof has been closed
136: nextGoals = selectedList = goalList = SLListOfGoal.EMPTY_LIST;
137: else {
138: if (selectedList.isEmpty()
139: || (currentSubtreeRoot != null && isSatisfiableSubtree(currentSubtreeRoot)))
140: setupGoals(goalList.prepend(selectedList));
141: }
142: }
143:
144: private void updateGoalListHelp(Node node, ListOfGoal newGoals) {
145: ListOfGoal prevGoalList = SLListOfGoal.EMPTY_LIST;
146: boolean newGoalsInserted = false;
147:
148: nextGoals = SLListOfGoal.EMPTY_LIST;
149:
150: // Remove "node" and goals contained within "newGoals"
151: while (!selectedList.isEmpty()) {
152: final Goal goal = selectedList.head();
153: selectedList = selectedList.tail();
154:
155: if (node == goal.node() || newGoals.contains(goal)) {
156: // continue taclet apps at the next goal in list
157: nextGoals = selectedList;
158:
159: if (!newGoalsInserted) {
160: prevGoalList = insertNewGoals(newGoals,
161: prevGoalList);
162: newGoalsInserted = true;
163: }
164: } else {
165: prevGoalList = prevGoalList.prepend(goal);
166: }
167: }
168:
169: while (!prevGoalList.isEmpty()) {
170: selectedList = selectedList.prepend(prevGoalList.head());
171: prevGoalList = prevGoalList.tail();
172: }
173: }
174:
175: private ListOfGoal insertNewGoals(ListOfGoal newGoals,
176: ListOfGoal prevGoalList) {
177: final IteratorOfGoal it = newGoals.iterator();
178:
179: while (it.hasNext()) {
180: final Goal g = it.next();
181:
182: if (proof.openGoals().contains(g)) {
183: if (!allGoalsSatisfiable
184: && g.getClosureConstraint().isSatisfiable())
185: goalList = goalList.prepend(g);
186: else
187: prevGoalList = prevGoalList.prepend(g);
188: }
189: }
190: return prevGoalList;
191: }
192:
193: protected static ListOfGoal rotateList(ListOfGoal p_list) {
194: if (p_list.isEmpty())
195: return SLListOfGoal.EMPTY_LIST;
196:
197: return p_list.tail().append(p_list.head());
198: }
199:
200: private void removeClosedGoals() {
201: boolean changed = false;
202: IteratorOfGoal it = goalList.iterator();
203: goalList = SLListOfGoal.EMPTY_LIST;
204:
205: while (it.hasNext()) {
206: final Goal goal = it.next();
207: if (proof.openGoals().contains(goal))
208: // order of goals is not relevant
209: goalList = goalList.prepend(goal);
210: }
211:
212: it = selectedList.iterator();
213: ListOfGoal newList = SLListOfGoal.EMPTY_LIST;
214:
215: while (it.hasNext()) {
216: final Goal goal = it.next();
217: if (proof.openGoals().contains(goal)) {
218: if (!allGoalsSatisfiable
219: && goal.getClosureConstraint().isSatisfiable()) {
220: goalList = goalList.prepend(goal);
221: changed = true;
222: } else
223: newList = newList.prepend(goal);
224: } else
225: changed = true;
226: }
227:
228: if (changed) {
229: nextGoals = SLListOfGoal.EMPTY_LIST;
230:
231: // for "selectedList", order does matter
232: it = newList.iterator();
233: selectedList = SLListOfGoal.EMPTY_LIST;
234: while (it.hasNext())
235: selectedList = selectedList.prepend(it.next());
236: }
237: }
238:
239: /**
240: * Search for a minimal subtree of the proof tree which is not
241: * closable (constraints of its goals are inconsistent) below
242: * p_startNode
243: *
244: * PRECONDITION: * !isSatisfiableSubtree ( p_startNode )
245: * * all goals have satisfiable constraints
246: *
247: * @return true iff a non-empty subtree was found
248: */
249: private boolean findMinimalSubtreeBelow(Node p_startNode) {
250: Node node = p_startNode;
251:
252: while (node.childrenCount() == 1)
253: node = node.child(0);
254:
255: IteratorOfNode childrenIt = node.childrenIterator();
256:
257: while (childrenIt.hasNext()) {
258: final Node child = childrenIt.next();
259:
260: if (!isSatisfiableSubtree(child)
261: && findMinimalSubtreeBelow(child))
262: return true;
263: }
264:
265: currentSubtreeRoot = p_startNode;
266: childrenIt = node.leavesIterator();
267:
268: while (childrenIt.hasNext()) {
269: final Node child = childrenIt.next();
270: final Goal goal = proof.getGoal(child);
271:
272: if (goalList.contains(goal)) {
273: selectedList = selectedList.prepend(goal);
274: goalList = goalList.removeAll(goal);
275: }
276: }
277:
278: return !selectedList.isEmpty();
279:
280: }
281:
282: /**
283: * Search for a minimal subtree of the proof tree which is not
284: * closable (constraints of its goals are inconsistent) starting
285: * at p_startNode
286: *
287: * PRECONDITION: all goals have satisfiable constraints
288: */
289: private void findMinimalSubtree(Node p_startNode) {
290: while (isSatisfiableSubtree(p_startNode))
291: p_startNode = p_startNode.parent();
292:
293: if (!findMinimalSubtreeBelow(p_startNode))
294: findMinimalSubtreeBelow(proof.root());
295: }
296:
297: private boolean isSatisfiableSubtree(Node p_root) {
298: return p_root.getBranchSink().getResetConstraint()
299: .isSatisfiable();
300: }
301:
302: }
|