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.Semisequent;
16: import de.uka.ilkd.key.logic.Sequent;
17: import de.uka.ilkd.key.logic.op.IUpdateOperator;
18: import de.uka.ilkd.key.proof.Goal;
19: import de.uka.ilkd.key.rule.RuleApp;
20: import de.uka.ilkd.key.rule.TacletApp;
21: import de.uka.ilkd.key.strategy.RuleAppCost;
22:
23: /**
24: * Binary feature that returns true iff the hyper-tableaux simplification method
25: * approves the given application (which is supposed to be the application of a
26: * replace-known rule). Used terminology is defined in Diss. by Martin Giese.
27: */
28: public class SimplifyReplaceKnownCandidateFeature extends
29: AbstractPolarityFeature implements Feature {
30:
31: public final static Feature INSTANCE = new SimplifyReplaceKnownCandidateFeature();
32:
33: private SimplifyReplaceKnownCandidateFeature() {
34: }
35:
36: /**
37: * Compute the cost of a RuleApp.
38: * @param app the RuleApp
39: * @param pos position where <code>app</code> is to be applied
40: * @param goal the goal on which <code>app</code> is to be applied
41: * @return the cost of <code>app</code>
42: */
43: public RuleAppCost compute(RuleApp ruleApp, PosInOccurrence pos,
44: Goal goal) {
45: assert pos != null : "Feature is only applicable to rules with find";
46:
47: if (!isAllowedPosition(pos))
48: return BinaryFeature.TOP_COST;
49:
50: assert ruleApp instanceof TacletApp : "Feature is only applicable to taclet apps";
51:
52: final TacletApp app = (TacletApp) ruleApp;
53: final Sequent ifSeq = app.taclet().ifSequent();
54:
55: assert ifSeq.size() == 1 : "Wrong number of if-formulas.";
56:
57: final boolean ifForInAntec = ifSeq.succedent() == Semisequent.EMPTY_SEMISEQUENT;
58:
59: final Boolean pol = polarity(pos, new Boolean(pos.isInAntec()));
60:
61: final boolean approved = pol == null
62: || AbstractBetaFeature.alwaysReplace(pos.subTerm())
63: || pol.booleanValue() != ifForInAntec;
64:
65: return approved ? BinaryFeature.ZERO_COST
66: : BinaryFeature.TOP_COST;
67: }
68:
69: private boolean isAllowedPosition(PosInOccurrence pos) {
70: final PIOPathIterator it = pos.iterator();
71:
72: while (it.next() != -1) {
73: if (!(it.getSubTerm().op() instanceof IUpdateOperator))
74: return true;
75: }
76:
77: return false;
78: }
79: }
|