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: package de.uka.ilkd.key.strategy.termfeature;
09:
10: import de.uka.ilkd.key.logic.Term;
11: import de.uka.ilkd.key.logic.op.Modality;
12: import de.uka.ilkd.key.logic.op.Operator;
13: import de.uka.ilkd.key.logic.op.ProgramMethod;
14: import de.uka.ilkd.key.logic.op.Quantifier;
15:
16: /**
17: * Returns zero iff a term contains a program or (optionally) a query expression
18: */
19: public class ContainsExecutableCodeTermFeature extends
20: BinaryTermFeature {
21:
22: private final boolean considerQueries;
23:
24: private ContainsExecutableCodeTermFeature(boolean considerQueries) {
25: this .considerQueries = considerQueries;
26: }
27:
28: public final static TermFeature PROGRAMS = new ContainsExecutableCodeTermFeature(
29: false);
30: public final static TermFeature PROGRAMS_OR_QUERIES = new ContainsExecutableCodeTermFeature(
31: true);
32:
33: protected boolean filter(Term t) {
34: return containsExec(t);
35: }
36:
37: private boolean containsExec(Term t) {
38: if (t.isRigid())
39: return false;
40:
41: final Operator op = t.op();
42: if (op instanceof Quantifier)
43: return false;
44:
45: if (op instanceof Modality)
46: return true;
47: if (considerQueries && op instanceof ProgramMethod)
48: return true;
49:
50: for (int i = 0; i != op.arity(); ++i) {
51: final boolean res = filter(t.sub(i));
52: if (res)
53: return true;
54: }
55:
56: return false;
57: }
58:
59: }
|