01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.strategy.feature.instantiator;
12:
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.RuleApp;
16: import de.uka.ilkd.key.strategy.RuleAppCost;
17: import de.uka.ilkd.key.strategy.feature.Feature;
18:
19: public class OneOfCP implements Feature {
20:
21: private final BackTrackingManager manager;
22: private final Feature features[];
23:
24: private int theChosenOne;
25: private final ChoicePoint cp = new CP();
26:
27: private OneOfCP(BackTrackingManager manager, Feature[] features) {
28: this .manager = manager;
29: this .features = features;
30: }
31:
32: public static Feature create(Feature[] features,
33: BackTrackingManager manager) {
34: return new OneOfCP(manager, features);
35: }
36:
37: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
38: Goal goal) {
39: manager.passChoicePoint(cp, this );
40: return features[theChosenOne].compute(app, pos, goal);
41: }
42:
43: private final class CP implements ChoicePoint {
44: private final class BranchIterator implements
45: IteratorOfCPBranch {
46: private int num = 0;
47: private final RuleApp oldApp;
48:
49: public BranchIterator(RuleApp oldApp) {
50: this .oldApp = oldApp;
51: }
52:
53: public boolean hasNext() {
54: return num < features.length;
55: }
56:
57: public CPBranch next() {
58: final int chosen = num++;
59: return new CPBranch() {
60: public void choose() {
61: theChosenOne = chosen;
62: }
63:
64: public RuleApp getRuleAppForBranch() {
65: return oldApp;
66: }
67: };
68: }
69: }
70:
71: public IteratorOfCPBranch getBranches(RuleApp oldApp) {
72: return new BranchIterator(oldApp);
73: }
74: }
75: }
|