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: // This file is part of KeY - Integrated Deductive Software Design
09: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.strategy.feature;
19:
20: import de.uka.ilkd.key.logic.ConstrainedFormula;
21: import de.uka.ilkd.key.logic.PosInOccurrence;
22: import de.uka.ilkd.key.logic.Semisequent;
23: import de.uka.ilkd.key.proof.Goal;
24: import de.uka.ilkd.key.rule.IteratorOfRuleApp;
25: import de.uka.ilkd.key.rule.ListOfRuleApp;
26: import de.uka.ilkd.key.rule.TacletApp;
27:
28: /**
29: * Binary feature that returns zero iff a certain Taclet app has not already
30: * been performed
31: */
32: public class NonDuplicateAppFeature extends
33: AbstractNonDuplicateAppFeature {
34:
35: public static final Feature INSTANCE = new NonDuplicateAppFeature();
36:
37: protected boolean containsRuleApp(ListOfRuleApp list,
38: TacletApp rapp, PosInOccurrence pio) {
39:
40: final IteratorOfRuleApp it = list.iterator();
41: while (it.hasNext()) {
42: if (sameApplication(it.next(), rapp, pio))
43: return true;
44: }
45:
46: return false;
47: }
48:
49: public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal) {
50: if (!app.ifInstsComplete()) {
51: return true;
52: }
53:
54: if (pos == null) {
55: return !containsRuleApp(goal.appliedRuleApps(), app, pos);
56: }
57:
58: return noDuplicateFindTaclet(app, pos, goal);
59: }
60:
61: protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
62: PosInOccurrence newPio, PosInOccurrence oldPio) {
63: return oldPio.equals(newPio);
64: }
65:
66: protected boolean semiSequentContains(Semisequent semisequent,
67: ConstrainedFormula cfma) {
68: return semisequent.contains(cfma);
69: }
70: }
|