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 de.uka.ilkd.key.logic.IteratorOfTerm;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.proof.Goal;
017: import de.uka.ilkd.key.rule.RuleApp;
018: import de.uka.ilkd.key.strategy.LongRuleAppCost;
019: import de.uka.ilkd.key.strategy.RuleAppCost;
020: import de.uka.ilkd.key.strategy.feature.Feature;
021: import de.uka.ilkd.key.strategy.termProjection.TermBuffer;
022: import de.uka.ilkd.key.strategy.termgenerator.TermGenerator;
023:
024: /**
025: * Feature representing a <code>ChoicePoint</code> that iterates over the
026: * terms returned by a <code>TermGenerator</code>. The terms are stored in a
027: * <code>TermBuffer</code> one after the other and can subsequently be used
028: * to instantiate a rule application
029: */
030: public class ForEachCP implements Feature {
031:
032: private final BackTrackingManager manager;
033:
034: private final TermBuffer var;
035: private final TermGenerator generator;
036: private final Feature body;
037:
038: /**
039: * @param var
040: * <code>TermBuffer</code> in which the terms are going to
041: * be stored
042: * @param generator
043: * the terms that are to be iterated over
044: * @param body
045: * a feature that is supposed to be evaluated repeatedly for the
046: * possible values of <code>var</code>
047: */
048: public static Feature create(TermBuffer var,
049: TermGenerator generator, Feature body,
050: BackTrackingManager manager) {
051: return new ForEachCP(var, generator, body, manager);
052: }
053:
054: private ForEachCP(TermBuffer var, TermGenerator generator,
055: Feature body, BackTrackingManager manager) {
056: this .var = var;
057: this .generator = generator;
058: this .body = body;
059: this .manager = manager;
060: }
061:
062: public RuleAppCost compute(final RuleApp app,
063: final PosInOccurrence pos, final Goal goal) {
064: final Term outerVarContent = var.getContent();
065: var.setContent(null);
066:
067: manager.passChoicePoint(new CP(app, pos, goal), this );
068:
069: final RuleAppCost res;
070: if (var.getContent() != null)
071: res = body.compute(app, pos, goal);
072: else
073: res = LongRuleAppCost.ZERO_COST;
074:
075: var.setContent(outerVarContent);
076: return res;
077: }
078:
079: private final class CP implements ChoicePoint {
080: private final class BranchIterator implements
081: IteratorOfCPBranch {
082: private final IteratorOfTerm terms;
083: private final RuleApp oldApp;
084:
085: private BranchIterator(IteratorOfTerm terms, RuleApp oldApp) {
086: this .terms = terms;
087: this .oldApp = oldApp;
088: }
089:
090: public boolean hasNext() {
091: return terms.hasNext();
092: }
093:
094: public CPBranch next() {
095: final Term generatedTerm = terms.next();
096: return new CPBranch() {
097: public void choose() {
098: var.setContent(generatedTerm);
099: }
100:
101: public RuleApp getRuleAppForBranch() {
102: return oldApp;
103: }
104: };
105: }
106: }
107:
108: private final PosInOccurrence pos;
109: private final RuleApp app;
110: private final Goal goal;
111:
112: private CP(RuleApp app, PosInOccurrence pos, Goal goal) {
113: this .pos = pos;
114: this .app = app;
115: this .goal = goal;
116: }
117:
118: public IteratorOfCPBranch getBranches(RuleApp oldApp) {
119: return new BranchIterator(generator
120: .generate(app, pos, goal), oldApp);
121: }
122: }
123:
124: }
|