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 java.util.HashMap;
14:
15: import de.uka.ilkd.key.rule.ListOfRuleSet;
16: import de.uka.ilkd.key.rule.Taclet;
17:
18: /**
19: * Filter that selects taclets using the method <code>admissible</code> of the
20: * <code>Taclet</code> class, i.e. with respect to active heuristics and the
21: * <code>interactive</code> flag.
22: * If the interactive flag is
23: * set the following procedure is used: the non-interactive marked
24: * rules are only taken if the given list of heuristics contains at
25: * least one heuristic of that rule. If the interactive flag is not
26: * set, a rule is taken if the intersection between the given
27: * heuristics and the heuristics of the rule is not empty.
28: */
29: public class IHTacletFilter extends TacletFilter {
30: private final boolean interactive;
31: private final ListOfRuleSet heuristics;
32:
33: private final HashMap filterCache = new HashMap(2000);
34:
35: public IHTacletFilter(boolean interactive, ListOfRuleSet heuristics) {
36: this .interactive = interactive;
37: this .heuristics = heuristics;
38: }
39:
40: /**
41: * @return true iff <code>taclet</code> should be included in the
42: * result
43: */
44: public boolean filter(Taclet taclet) {
45: if (!interactive) {
46: Boolean b = (Boolean) filterCache.get(taclet);
47: if (b == null) {
48: b = taclet.admissible(interactive, heuristics) ? Boolean.TRUE
49: : Boolean.FALSE;
50: filterCache.put(taclet, b);
51: }
52: return b == Boolean.TRUE;
53: }
54: // in interactive case we do not need to cache; the user is too slow ;-)
55: return taclet.admissible(interactive, heuristics);
56: }
57: }
|