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.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.logic.PosInOccurrence;
16: import de.uka.ilkd.key.proof.ConstraintTableModel;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.proof.Proof;
19: import de.uka.ilkd.key.rule.TacletApp;
20:
21: /**
22: * This feature is similar to <code>ConstraintStrengthenFeature</code>, but
23: * instead of just comparing the constraint resulting from a rule application
24: * with the original constraint of the find-formula of the application, the new
25: * constraint is compared with the joint of the original constraint and the user
26: * constraint. I.e. the feature returns zero iff the new constraint is stronger
27: * than <code>userConstraint.join(formulaConstraint)</code>.
28: */
29: public class ConstraintStrengthenFeatureUC extends
30: AbstractConstraintStrengthenFeature {
31:
32: private final ConstraintTableModel userConstraint;
33:
34: private ConstraintStrengthenFeatureUC(
35: ConstraintTableModel userConstraint) {
36: this .userConstraint = userConstraint;
37: }
38:
39: public static Feature create(Proof proof) {
40: return new ConstraintStrengthenFeatureUC(proof
41: .getUserConstraint());
42: }
43:
44: protected boolean filter(TacletApp app, PosInOccurrence pos,
45: Goal goal) {
46: if (app.constraint().isBottom())
47: return false;
48:
49: final Services services = goal.proof().getServices();
50: final Constraint formulaConstraint;
51: if (pos == null) {
52: // there is no find-part, we are instead using constraints of the
53: // if-formulas
54: if (app.ifInstsComplete()) {
55: formulaConstraint = getIfConstraint(app, services);
56: } else {
57: return false;
58: }
59: } else {
60: formulaConstraint = pos.constrainedFormula().constraint();
61: }
62:
63: final Constraint uc = userConstraint.getConstraint();
64: if (formulaConstraint.isBottom() && uc.isBottom())
65: return true;
66:
67: final Constraint oriConstraint = formulaConstraint.join(uc,
68: services);
69: return !oriConstraint.isAsStrongAs(app.constraint());
70: }
71:
72: }
|