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:
19: /**
20: * Auxiliary class that contains methods to compute the polarity of a
21: * position/subformula within a formula
22: */
23: public abstract class AbstractPolarityFeature {
24:
25: /**
26: * @param formulaPol
27: * the polarity of the complete formula (i.e. whether the formula
28: * is part of antecedent or succedent, <code>Boolean.TRUE</code>
29: * for antecedent)
30: * @return the polarity of the given position, which is
31: * <code>Boolean.TRUE</code>,<code>Boolean.FALSE</code> or
32: * <code>null</code>
33: */
34: protected Boolean polarity(PosInOccurrence pos, Boolean formulaPol) {
35: if (formulaPol == null)
36: return null;
37:
38: final PIOPathIterator it = pos.iterator();
39:
40: while (it.next() != -1) {
41: final Term t = it.getSubTerm();
42: final Operator op = t.op();
43:
44: if (op == Op.NOT || op == Op.IMP && it.getChild() == 0)
45: formulaPol = invert(formulaPol);
46: else if (op == Op.EQV
47: || (op == Op.IF_THEN_ELSE && it.getChild() == 0))
48: return null;
49: }
50:
51: return formulaPol;
52: }
53:
54: private Boolean invert(Boolean p) {
55: return p == null ? null : (p.booleanValue() ? Boolean.FALSE
56: : Boolean.TRUE);
57: }
58:
59: }
|