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.logic.op.Metavariable;
16: import de.uka.ilkd.key.logic.op.SchemaVariable;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.FindTaclet;
19: import de.uka.ilkd.key.rule.TacletApp;
20:
21: /**
22: * Feature that returns zero if and only if the focus of the application in
23: * question is not a metavariable or if the find-expression of the taclet only
24: * is a single schema variable
25: */
26: public class NotWithinMVFeature extends BinaryTacletAppFeature {
27:
28: public static Feature INSTANCE = new NotWithinMVFeature();
29:
30: private NotWithinMVFeature() {
31: }
32:
33: protected boolean filter(TacletApp app, PosInOccurrence pos,
34: Goal goal) {
35: if (pos == null)
36: return true;
37:
38: if (!(pos.subTerm().op() instanceof Metavariable))
39: return true;
40:
41: final FindTaclet t = (FindTaclet) app.taclet();
42: final Term findExpr = t.find();
43: return findExpr.op() instanceof SchemaVariable;
44: }
45:
46: }
|