001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.strategy.feature;
012:
013: import java.math.BigInteger;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.PosInOccurrence;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
019: import de.uka.ilkd.key.proof.Goal;
020: import de.uka.ilkd.key.rule.TacletApp;
021: import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
022: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
023:
024: /**
025: * Return zero only if the value of one (left) polynomial always will be (less
026: * or equal) or (less) than the value of a second (right) polynomial.
027: * Both polynomials can optionally be multiplied with some constant before
028: * comparison.
029: */
030: public abstract class PolynomialValuesCmpFeature extends
031: BinaryTacletAppFeature {
032:
033: private final ProjectionToTerm left, right, leftCoeff, rightCoeff;
034:
035: protected PolynomialValuesCmpFeature(ProjectionToTerm left,
036: ProjectionToTerm right, ProjectionToTerm leftCoeff,
037: ProjectionToTerm rightCoeff) {
038: this .left = left;
039: this .right = right;
040: this .leftCoeff = leftCoeff;
041: this .rightCoeff = rightCoeff;
042: }
043:
044: public static Feature lt(ProjectionToTerm left,
045: ProjectionToTerm right) {
046: return lt(left, right, null, null);
047: }
048:
049: public static Feature lt(ProjectionToTerm left,
050: ProjectionToTerm right, ProjectionToTerm leftCoeff,
051: ProjectionToTerm rightCoeff) {
052: return new PolynomialValuesCmpFeature(left, right, leftCoeff,
053: rightCoeff) {
054: protected boolean compare(Polynomial leftPoly,
055: Polynomial rightPoly) {
056: return leftPoly.valueLess(rightPoly);
057: }
058: };
059: }
060:
061: public static Feature leq(ProjectionToTerm left,
062: ProjectionToTerm right) {
063: return leq(left, right, null, null);
064: }
065:
066: public static Feature leq(ProjectionToTerm left,
067: ProjectionToTerm right, ProjectionToTerm leftCoeff,
068: ProjectionToTerm rightCoeff) {
069: return new PolynomialValuesCmpFeature(left, right, leftCoeff,
070: rightCoeff) {
071: protected boolean compare(Polynomial leftPoly,
072: Polynomial rightPoly) {
073: return leftPoly.valueLeq(rightPoly);
074: }
075: };
076: }
077:
078: public static Feature eq(ProjectionToTerm left,
079: ProjectionToTerm right) {
080: return eq(left, right, null, null);
081: }
082:
083: public static Feature eq(ProjectionToTerm left,
084: ProjectionToTerm right, ProjectionToTerm leftCoeff,
085: ProjectionToTerm rightCoeff) {
086: return new PolynomialValuesCmpFeature(left, right, leftCoeff,
087: rightCoeff) {
088: protected boolean compare(Polynomial leftPoly,
089: Polynomial rightPoly) {
090: return leftPoly.valueEq(rightPoly);
091: }
092: };
093: }
094:
095: public static Feature divides(ProjectionToTerm left,
096: ProjectionToTerm right) {
097: return divides(left, right, null, null);
098: }
099:
100: public static Feature divides(ProjectionToTerm left,
101: ProjectionToTerm right, ProjectionToTerm leftCoeff,
102: ProjectionToTerm rightCoeff) {
103: return new PolynomialValuesCmpFeature(left, right, leftCoeff,
104: rightCoeff) {
105: protected boolean compare(Polynomial leftPoly,
106: Polynomial rightPoly) {
107: // we currently only support constant polynomials
108: assert leftPoly.getParts().isEmpty();
109: assert rightPoly.getParts().isEmpty();
110: if (leftPoly.getConstantTerm().signum() == 0)
111: return true;
112: if (rightPoly.getConstantTerm().signum() == 0)
113: return false;
114: return leftPoly.getConstantTerm().mod(
115: rightPoly.getConstantTerm().abs()).signum() == 0;
116: }
117: };
118: }
119:
120: protected boolean filter(TacletApp app, PosInOccurrence pos,
121: Goal goal) {
122: return compare(getPolynomial(left, leftCoeff, app, pos, goal),
123: getPolynomial(right, rightCoeff, app, pos, goal));
124: }
125:
126: protected abstract boolean compare(Polynomial leftPoly,
127: Polynomial rightPoly);
128:
129: private Polynomial getPolynomial(ProjectionToTerm polyProj,
130: ProjectionToTerm coeffProj, TacletApp app,
131: PosInOccurrence pos, Goal goal) {
132: final Services services = goal.proof().getServices();
133: final Polynomial poly = Polynomial.create(polyProj.toTerm(app,
134: pos, goal), services);
135:
136: if (coeffProj == null)
137: return poly;
138: final Term coeffT = coeffProj.toTerm(app, pos, goal);
139: if (coeffT == null)
140: return poly;
141:
142: final BigInteger coeff = new BigInteger(AbstractMetaOperator
143: .convertToDecimalString(coeffT, services));
144: return poly.multiply(coeff);
145: }
146: }
|