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;
12:
13: import de.uka.ilkd.key.logic.IteratorOfTerm;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.rule.RuleApp;
18: import de.uka.ilkd.key.strategy.LongRuleAppCost;
19: import de.uka.ilkd.key.strategy.RuleAppCost;
20: import de.uka.ilkd.key.strategy.TopRuleAppCost;
21: import de.uka.ilkd.key.strategy.termProjection.TermBuffer;
22: import de.uka.ilkd.key.strategy.termgenerator.TermGenerator;
23:
24: /**
25: * A feature that computes the sum of the values of a feature term when a given
26: * variable ranges over a sequence of terms
27: */
28: public class ComprehendedSumFeature implements Feature {
29:
30: private final TermBuffer var;
31: private final TermGenerator generator;
32: private final Feature body;
33:
34: /**
35: * @param var
36: * <code>TermBuffer</code> in which the terms are going to
37: * be stored
38: * @param generator
39: * the terms that are to be iterated over
40: * @param body
41: * a feature that is supposed to be evaluated repeatedly for the
42: * possible values of <code>var</code>
43: */
44: public static Feature create(TermBuffer var,
45: TermGenerator generator, Feature body) {
46: return new ComprehendedSumFeature(var, generator, body);
47: }
48:
49: private ComprehendedSumFeature(TermBuffer var,
50: TermGenerator generator, Feature body) {
51: this .var = var;
52: this .generator = generator;
53: this .body = body;
54: }
55:
56: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
57: Goal goal) {
58: final Term outerVarContent = var.getContent();
59:
60: final IteratorOfTerm it = generator.generate(app, pos, goal);
61: RuleAppCost res = LongRuleAppCost.ZERO_COST;
62: while (it.hasNext() && !(res instanceof TopRuleAppCost)) {
63: var.setContent(it.next());
64: res = res.add(body.compute(app, pos, goal));
65: }
66:
67: var.setContent(outerVarContent);
68: return res;
69: }
70: }
|