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.Constraint;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.rule.TacletApp;
17:
18: /**
19: * A binary feature that returns zero iff the constraint of the given taclet app
20: * is stronger than the original constraint of the formula to which the rule is
21: * applied (i.e. replacewith-clauses are changed into add-clauses). For taclets
22: * that do not have a find-clause, the app constraint is compared with the
23: * conjunction of the constraints attached to matched if-formulas.
24: */
25: public class ConstraintStrengthenFeature extends
26: AbstractConstraintStrengthenFeature {
27:
28: public final static Feature INSTANCE = new ConstraintStrengthenFeature();
29:
30: private ConstraintStrengthenFeature() {
31: }
32:
33: protected boolean filter(TacletApp app, PosInOccurrence pos,
34: Goal goal) {
35: final Constraint formulaConstraint;
36: if (pos == null) {
37: // there is no find-part, we are instead using constraints of the
38: // if-formulas
39: if (app.ifInstsComplete()) {
40: formulaConstraint = getIfConstraint(app, goal.proof()
41: .getServices());
42: } else {
43: return false;
44: }
45: } else {
46: formulaConstraint = pos.constrainedFormula().constraint();
47: }
48:
49: return !formulaConstraint.isAsStrongAs(app.constraint());
50: }
51:
52: }
|