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.proof.Goal;
16: import de.uka.ilkd.key.rule.ListOfUpdatePair;
17: import de.uka.ilkd.key.rule.TacletApp;
18:
19: /**
20: * Binary feature that returns zero iff a certain Taclet app has not already
21: * been performed
22: */
23: public class NonDuplicateAppModPositionFeature extends
24: NonDuplicateAppFeature {
25:
26: public static final Feature INSTANCE = new NonDuplicateAppModPositionFeature();
27:
28: public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal) {
29: if (!app.ifInstsComplete()) {
30: return true;
31: }
32:
33: return !containsRuleApp(goal.appliedRuleApps(), app, pos);
34: }
35:
36: protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
37: PosInOccurrence newPio, PosInOccurrence oldPio) {
38: final Term newFocus = newPio.subTerm();
39: final Term oldFocus = oldPio.subTerm();
40: if (!newFocus.equals(oldFocus))
41: return false;
42: if (newFocus.isRigid())
43: return true;
44: final ListOfUpdatePair oldUpdateContext = oldApp
45: .instantiations().getUpdateContext();
46: final ListOfUpdatePair newUpdateContext = newApp
47: .instantiations().getUpdateContext();
48: return oldUpdateContext.equals(newUpdateContext);
49: }
50:
51: }
|