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: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: ///
17: package de.uka.ilkd.key.strategy.termfeature;
18:
19: import de.uka.ilkd.key.logic.Term;
20: import de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature;
21: import de.uka.ilkd.key.strategy.termfeature.TermFeature;
22:
23: /**
24: * return zero cost if given term does not contain any free variables.
25: */
26: public class ClosedExpressionTermFeature extends BinaryTermFeature {
27:
28: public static final TermFeature INSTANCE = new ClosedExpressionTermFeature();
29:
30: private ClosedExpressionTermFeature() {
31: }
32:
33: protected boolean filter(Term term) {
34: return term.freeVars().size() == 0;
35: }
36:
37: }
|