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.proof;
12:
13: import de.uka.ilkd.key.rule.Rule;
14: import de.uka.ilkd.key.rule.Taclet;
15:
16: /**
17: * Interface for filtering a list of TacletApps, for example to
18: * choose only taclets for interactive application or taclets
19: * belonging to some given heuristics.
20: */
21: public abstract class TacletFilter implements RuleFilter {
22: /**
23: * Trival TacletFilter that always returns true;
24: */
25: public static final TacletFilter TRUE = new TacletFilterTrue();
26:
27: public boolean filter(Rule rule) {
28: if (rule instanceof Taclet)
29: return filter((Taclet) rule);
30: return false;
31: }
32:
33: /**
34: * @return true iff <code>taclet</code> should be included in the
35: * result
36: */
37: protected abstract boolean filter(Taclet taclet);
38:
39: /**
40: * Trival TacletFilter that always returns true;
41: */
42: static class TacletFilterTrue extends TacletFilter {
43: protected boolean filter(Taclet taclet) {
44: return true;
45: }
46: }
47: }
|