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.ConstrainedFormula;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Semisequent;
16: import de.uka.ilkd.key.proof.Goal;
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. Contrary to <code>NonDuplicateAppFeature</code>, this feature
22: * is also able to handle failing meta-constructs correctly (these constructs
23: * return equal, but not identical formulas in case of a failure), but is less
24: * efficient.
25: */
26: public class EqNonDuplicateAppFeature extends
27: AbstractNonDuplicateAppFeature {
28:
29: public static final Feature INSTANCE = new EqNonDuplicateAppFeature();
30:
31: private EqNonDuplicateAppFeature() {
32: }
33:
34: public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal) {
35: assert pos != null : "Feature is only applicable to rules with find";
36:
37: if (!app.ifInstsComplete())
38: return true;
39:
40: return noDuplicateFindTaclet(app, pos, goal);
41: }
42:
43: protected boolean semiSequentContains(Semisequent semisequent,
44: ConstrainedFormula cfma) {
45: return semisequent.containsEqual(cfma);
46: }
47:
48: protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
49: PosInOccurrence newPio, PosInOccurrence oldPio) {
50: return oldPio.eqEquals(newPio);
51: }
52: }
|