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.PosInOccurrence;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.strategy.RuleAppCost;
16:
17: /**
18: * Binary feature that returns zero iff the focus of a rule contains a
19: * quantifier
20: *
21: * NB: this can nowadays be done more nicely using term features
22: */
23: public class ContainsQuantifierFeature extends AbstractBetaFeature {
24:
25: public final static Feature INSTANCE = new ContainsQuantifierFeature();
26:
27: private ContainsQuantifierFeature() {
28: }
29:
30: protected RuleAppCost doComputation(PosInOccurrence pos,
31: Term findTerm) {
32: return containsQuantifier(findTerm) ? BinaryFeature.ZERO_COST
33: : BinaryFeature.TOP_COST;
34: }
35:
36: }
|