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.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.rule.TacletApp;
18: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
19: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
20:
21: /**
22: * Return zero iff the monomial <code>dividendSV</code> can be made smaller
23: * (in the polynomial reduction ordering) by adding or subtracting
24: * <code>divisorSV</code>
25: */
26: public abstract class ReducibleMonomialsFeature extends
27: BinaryTacletAppFeature {
28: private final ProjectionToTerm dividend, divisor;
29:
30: private ReducibleMonomialsFeature(ProjectionToTerm dividend,
31: ProjectionToTerm divisor) {
32: this .dividend = dividend;
33: this .divisor = divisor;
34: }
35:
36: public static Feature createReducible(ProjectionToTerm dividend,
37: ProjectionToTerm divisor) {
38: return new ReducibleMonomialsFeature(dividend, divisor) {
39: protected boolean checkReducibility(Monomial mDividend,
40: Monomial mDivisor) {
41: return mDivisor.reducible(mDividend);
42: }
43: };
44: }
45:
46: public static Feature createDivides(ProjectionToTerm dividend,
47: ProjectionToTerm divisor) {
48: return new ReducibleMonomialsFeature(dividend, divisor) {
49: protected boolean checkReducibility(Monomial mDividend,
50: Monomial mDivisor) {
51: return mDivisor.divides(mDividend);
52: }
53: };
54: }
55:
56: protected boolean filter(TacletApp app, PosInOccurrence pos,
57: Goal goal) {
58: final Term dividendT = dividend.toTerm(app, pos, goal);
59: final Term divisorT = divisor.toTerm(app, pos, goal);
60:
61: final Services services = goal.proof().getServices();
62: final Monomial mDividend = Monomial.create(dividendT, services);
63: final Monomial mDivisor = Monomial.create(divisorT, services);
64:
65: return checkReducibility(mDividend, mDivisor);
66: }
67:
68: protected abstract boolean checkReducibility(Monomial mDividend,
69: Monomial mDivisor);
70: }
|