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.ConstrainedFormula;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Sequent;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.proof.Node;
18: import de.uka.ilkd.key.proof.RuleFilter;
19: import de.uka.ilkd.key.rule.RuleApp;
20:
21: /**
22: * Binary feature that returns zero iff the find-formula of the concerned rule
23: * app was introduced by a certain kind rule of rule (described via a
24: * <code>RuleFilter</code>)
25: */
26: public class FormulaAddedByRuleFeature extends BinaryFeature {
27:
28: private final RuleFilter filter;
29:
30: private FormulaAddedByRuleFeature(RuleFilter p_filter) {
31: filter = p_filter;
32: }
33:
34: public static Feature create(RuleFilter p_filter) {
35: return new FormulaAddedByRuleFeature(p_filter);
36: }
37:
38: public boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
39: assert pos != null : "Feature is only applicable to rules with find";
40:
41: final ConstrainedFormula cfma = pos.constrainedFormula();
42: final boolean antec = pos.isInAntec();
43:
44: Node node = goal.node();
45:
46: while (!node.root()) {
47: final Node par = node.parent();
48: final Sequent pseq = par.sequent();
49:
50: if (!(antec ? pseq.antecedent() : pseq.succedent())
51: .contains(cfma))
52: return filter.filter(par.getAppliedRuleApp().rule());
53:
54: node = par;
55: }
56:
57: return false;
58: }
59:
60: }
|