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 de.uka.ilkd.key.logic.PosInOccurrence;
014: import de.uka.ilkd.key.proof.Goal;
015: import de.uka.ilkd.key.rule.RuleApp;
016: import de.uka.ilkd.key.strategy.LongRuleAppCost;
017: import de.uka.ilkd.key.strategy.RuleAppCost;
018: import de.uka.ilkd.key.strategy.TopRuleAppCost;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * A feature that applies an affine transformation to the result of
023: * a given feature.
024: * As a special case, it can be used to scale the given feature.
025: */
026: public abstract class ScaleFeature implements Feature {
027:
028: /** the base feature */
029: private final Feature feature;
030:
031: protected ScaleFeature(Feature p_feature) {
032: feature = p_feature;
033: }
034:
035: /**
036: * Create a feature that scales the result of the base feature.
037: * @param f the base feature
038: * @param coeff the coefficient to be applied to the result of
039: * <code>f</code>
040: */
041: public static Feature createScaled(Feature f, double coeff) {
042: return createAffine(f, coeff, 0);
043: }
044:
045: /**
046: * Create a feature that applies an affine transformation to the result of
047: * the base feature.
048: * The transformation is described by a coefficient and an offset.
049: * @param f the base feature
050: * @param coeff the coefficient to be applied to the result of
051: * <code>f</code>
052: * @param offset the offset to be added to the result of <code>f</code>
053: * (after multiplication with <code>coeff</code>)
054: */
055: public static Feature createAffine(Feature f, double coeff,
056: long offset) {
057: return new MultFeature(f, coeff, offset);
058: }
059:
060: /**
061: * Create a feature that applies an affine transformation to the result of
062: * the base feature.
063: * The transformation is described by two points in the domain and their
064: * images.
065: * @param f the base feature
066: * @param dom0 point 0 in the domain
067: * @param dom1 point 1 in the domain
068: * @param img0 point 0 in the image
069: * @param img1 point 1 in the image
070: */
071: public static Feature createAffine(Feature f, RuleAppCost dom0,
072: RuleAppCost dom1, RuleAppCost img0, RuleAppCost img1) {
073: Debug.assertFalse(dom0.equals(dom1),
074: "Two different points are needed to define the "
075: + "affine transformation");
076: if (img0.equals(img1))
077: return ConstFeature.createConst(img0);
078:
079: // now the two points of the domain (resp. of the image) are distinct
080:
081: if (dom0 instanceof TopRuleAppCost) {
082: return firstDomInfty(f, dom1, img0, img1);
083: } else {
084: if (img1 instanceof TopRuleAppCost)
085: return firstDomInfty(f, dom0, img1, img0);
086: else {
087:
088: // the points of the domain are finite
089: if (img0 instanceof TopRuleAppCost) {
090: return firstImgInfty(f, dom0, dom1, img1);
091: } else {
092: if (img1 instanceof TopRuleAppCost)
093: return firstImgInfty(f, dom1, img0, img1);
094: else {
095: return realAffine(f, dom0, dom1, img0, img1);
096: }
097: }
098:
099: }
100: }
101: }
102:
103: private static Feature firstDomInfty(Feature f, RuleAppCost dom1,
104: RuleAppCost img0, RuleAppCost img1) {
105: if (img0 instanceof TopRuleAppCost) {
106: final long img1Val = getValue(img1);
107: final long dom1Val = getValue(dom1);
108: return createAffine(f, 1.0, img1Val - dom1Val);
109: } else {
110: if (img1 instanceof TopRuleAppCost)
111: return ShannonFeature.createConditional(f,
112: TopRuleAppCost.INSTANCE, img0,
113: TopRuleAppCost.INSTANCE);
114: else
115: return ShannonFeature.createConditional(f,
116: TopRuleAppCost.INSTANCE, img0, img1);
117: }
118: }
119:
120: private static Feature firstImgInfty(Feature f, RuleAppCost dom0,
121: RuleAppCost dom1, RuleAppCost img1) {
122: return ShannonFeature.createConditional(f, dom1, img1,
123: TopRuleAppCost.INSTANCE);
124: }
125:
126: public static Feature realAffine(Feature f, RuleAppCost dom0,
127: RuleAppCost dom1, RuleAppCost img0, RuleAppCost img1) {
128: final double img0Val = getValue(img0);
129: final double img1Val = getValue(img1);
130: final double dom0Val = getValue(dom0);
131: final double dom1Val = getValue(dom1);
132:
133: final double coeff = (img1Val - img0Val) / (dom1Val - dom0Val);
134: final long offset = (long) (img0Val - (dom0Val * coeff));
135: return createAffine(f, coeff, offset);
136: }
137:
138: /**
139: * @param cost
140: * @return
141: */
142: private static long getValue(RuleAppCost cost) {
143: if (!(cost instanceof LongRuleAppCost))
144: illegalCostError(cost);
145: return ((LongRuleAppCost) cost).getValue();
146: }
147:
148: protected static void illegalCostError(final RuleAppCost cost) {
149: Debug.fail("Don't know what to do with cost class "
150: + cost.getClass());
151: }
152:
153: protected Feature getFeature() {
154: return feature;
155: }
156:
157: protected static boolean isZero(double p) {
158: return Math.abs(p) < 0.0000001;
159: }
160:
161: private static class MultFeature extends ScaleFeature {
162: /** the coefficient */
163: private final double coeff;
164: /** the offset */
165: private final long offset;
166:
167: private MultFeature(Feature f, double p_coeff, long p_offset) {
168: super (f);
169: coeff = p_coeff;
170: offset = p_offset;
171: }
172:
173: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
174: Goal goal) {
175: final RuleAppCost cost = getFeature().compute(app, pos,
176: goal);
177: long costVal;
178:
179: if (cost instanceof TopRuleAppCost) {
180: if (isZero(coeff))
181: costVal = 0;
182: else
183: return TopRuleAppCost.INSTANCE;
184: } else if (cost instanceof LongRuleAppCost) {
185: costVal = ((LongRuleAppCost) cost).getValue();
186: } else {
187: illegalCostError(cost);
188: return null;
189: }
190:
191: return LongRuleAppCost.create((long) (coeff * costVal)
192: + offset);
193: }
194: }
195:
196: }
|