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.PIOPathIterator;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.Op;
17: import de.uka.ilkd.key.logic.op.Operator;
18: import de.uka.ilkd.key.strategy.RuleAppCost;
19:
20: /**
21: * Feature that returns zero if there is no atom with negative polarity on a
22: * common d-path and on the left of the find-position within the find-formula as
23: * a formula of the antecedent. Used terminology is defined in Diss. by Martin
24: * Giese.
25: */
26: public class LeftmostNegAtomFeature extends AbstractBetaFeature {
27:
28: public final static Feature INSTANCE = new LeftmostNegAtomFeature();
29:
30: private LeftmostNegAtomFeature() {
31: }
32:
33: protected RuleAppCost doComputation(PosInOccurrence pos,
34: Term findTerm) {
35: final PIOPathIterator it = pos.iterator();
36: boolean positive = pos.isInAntec();
37:
38: while (it.next() != -1) {
39: final Term subTerm = it.getSubTerm();
40: final Operator op = subTerm.op();
41:
42: if (it.getChild() == 0) {
43: if (op == Op.NOT || op == Op.IMP)
44: positive = !positive;
45: else if (op == Op.EQV)
46: return BinaryFeature.ZERO_COST; // TODO
47:
48: continue;
49: }
50:
51: if (op == (positive ? Op.OR : Op.AND)) {
52: if (containsNegAtom(subTerm.sub(0), positive))
53: return BinaryFeature.TOP_COST;
54: } else if (positive && op == Op.IMP) {
55: if (containsNegAtom(subTerm.sub(0), false))
56: return BinaryFeature.TOP_COST;
57: } else if (op == Op.EQV)
58: return BinaryFeature.ZERO_COST; // TODO
59: }
60:
61: return BinaryFeature.ZERO_COST;
62: }
63:
64: }
|