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;
012:
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.logic.op.Operator;
015: import de.uka.ilkd.key.logic.sort.Sort;
016: import de.uka.ilkd.key.proof.Goal;
017: import de.uka.ilkd.key.proof.IHTacletFilter;
018: import de.uka.ilkd.key.proof.Proof;
019: import de.uka.ilkd.key.proof.TacletFilter;
020: import de.uka.ilkd.key.proof.UpdateSimplificationRuleFilter;
021: import de.uka.ilkd.key.rule.ListOfRuleSet;
022: import de.uka.ilkd.key.rule.RuleApp;
023: import de.uka.ilkd.key.rule.RuleSet;
024: import de.uka.ilkd.key.rule.SLListOfRuleSet;
025: import de.uka.ilkd.key.strategy.feature.*;
026: import de.uka.ilkd.key.strategy.feature.instantiator.*;
027: import de.uka.ilkd.key.strategy.termProjection.*;
028: import de.uka.ilkd.key.strategy.termfeature.*;
029: import de.uka.ilkd.key.strategy.termgenerator.TermGenerator;
030:
031: /**
032: *
033: */
034: public abstract class AbstractFeatureStrategy implements Strategy {
035:
036: private final Proof proof;
037:
038: protected AbstractFeatureStrategy(Proof proof) {
039: this .proof = proof;
040: }
041:
042: /**
043: * @return Returns the proof.
044: */
045: protected Proof getProof() {
046: return proof;
047: }
048:
049: /**
050: * @param heuristics
051: * @param thenFeature
052: * @return
053: */
054: protected Feature ifHeuristics(String[] heuristics,
055: Feature thenFeature) {
056: return ConditionalFeature.createConditional(
057: getFilterFor(heuristics), thenFeature);
058: }
059:
060: /**
061: * @param heuristics
062: * @param thenFeature
063: * @param elseFeature
064: * @return
065: */
066: protected Feature ifHeuristics(String[] heuristics,
067: Feature thenFeature, Feature elseFeature) {
068: return ConditionalFeature.createConditional(
069: getFilterFor(heuristics), thenFeature, elseFeature);
070: }
071:
072: protected Feature longConst(long a) {
073: return ConstFeature.createConst(c(a));
074: }
075:
076: protected Feature inftyConst() {
077: return ConstFeature.createConst(infty());
078: }
079:
080: protected TermFeature any() {
081: return longTermConst(0);
082: }
083:
084: protected TermFeature longTermConst(long a) {
085: return ConstTermFeature.createConst(c(a));
086: }
087:
088: protected TermFeature inftyTermConst() {
089: return ConstTermFeature.createConst(infty());
090: }
091:
092: protected Feature add(Feature a, Feature b) {
093: return BinarySumFeature.createSum(a, b);
094: }
095:
096: protected Feature add(Feature a, Feature b, Feature c) {
097: return TernarySumFeature.createSum(a, b, c);
098: }
099:
100: protected TermFeature add(TermFeature a, TermFeature b) {
101: return BinarySumTermFeature.createSum(a, b);
102: }
103:
104: protected TermFeature add(TermFeature a, TermFeature b,
105: TermFeature c) {
106: // could be done more efficiently
107: return add(a, add(b, c));
108: }
109:
110: protected TermFeature or(TermFeature a, TermFeature b) {
111: return ifZero(a, longTermConst(0), b);
112: }
113:
114: protected TermFeature or(TermFeature a, TermFeature b, TermFeature c) {
115: return or(a, or(b, c));
116: }
117:
118: protected Feature or(Feature a, Feature b) {
119: return ifZero(a, longConst(0), b);
120: }
121:
122: protected Feature or(Feature a, Feature b, Feature c) {
123: return or(a, or(b, c));
124: }
125:
126: protected Feature ifZero(Feature cond, Feature thenFeature) {
127: return ShannonFeature
128: .createConditionalBinary(cond, thenFeature);
129: }
130:
131: protected Feature ifZero(Feature cond, Feature thenFeature,
132: Feature elseFeature) {
133: return ShannonFeature.createConditionalBinary(cond,
134: thenFeature, elseFeature);
135: }
136:
137: protected TermFeature ifZero(TermFeature cond,
138: TermFeature thenFeature) {
139: return ShannonTermFeature.createConditionalBinary(cond,
140: thenFeature);
141: }
142:
143: protected TermFeature ifZero(TermFeature cond,
144: TermFeature thenFeature, TermFeature elseFeature) {
145: return ShannonTermFeature.createConditionalBinary(cond,
146: thenFeature, elseFeature);
147: }
148:
149: protected Feature not(Feature f) {
150: return ifZero(f, inftyConst(), longConst(0));
151: }
152:
153: protected TermFeature not(TermFeature f) {
154: return ifZero(f, ConstTermFeature
155: .createConst(TopRuleAppCost.INSTANCE), longTermConst(0));
156: }
157:
158: protected Feature eq(Feature a, Feature b) {
159: return CompareCostsFeature.eq(a, b);
160: }
161:
162: protected Feature less(Feature a, Feature b) {
163: return CompareCostsFeature.less(a, b);
164: }
165:
166: protected Feature leq(Feature a, Feature b) {
167: return CompareCostsFeature.leq(a, b);
168: }
169:
170: /**
171: * @param names
172: * @param priority
173: * @return
174: */
175: protected Feature ifHeuristics(String[] names, int priority) {
176: return ConditionalFeature.createConditional(
177: getFilterFor(names), c(priority), c(0));
178: }
179:
180: /**
181: * @param priority
182: * @return
183: */
184: protected Feature selectSimplifier(long priority) {
185: return ConditionalFeature.createConditional(
186: UpdateSimplificationRuleFilter.INSTANCE,
187: longConst(priority));
188: }
189:
190: private RuleAppCost c(long p) {
191: return LongRuleAppCost.create(p);
192: }
193:
194: private RuleAppCost infty() {
195: return TopRuleAppCost.INSTANCE;
196: }
197:
198: protected TacletFilter getFilterFor(String[] p_names) {
199: ListOfRuleSet heur = SLListOfRuleSet.EMPTY_LIST;
200: for (int i = 0; i != p_names.length; ++i)
201: heur = heur.prepend(getHeuristic(p_names[i]));
202: return new IHTacletFilter(false, heur);
203: }
204:
205: protected RuleSet getHeuristic(String p_name) {
206: final NamespaceSet nss = getProof().getNamespaces();
207:
208: assert nss != null : "Rule set namespace not available.";
209:
210: final Namespace ns = nss.ruleSets();
211: final Named h = ns.lookup(new Name(p_name));
212:
213: assert h != null : "Did not find the rule set " + p_name;
214:
215: return (RuleSet) h;
216: }
217:
218: protected void bindRuleSet(RuleSetDispatchFeature d,
219: RuleSet ruleSet, Feature f) {
220: d.add(ruleSet, f);
221: }
222:
223: protected void bindRuleSet(RuleSetDispatchFeature d,
224: RuleSet ruleSet, long cost) {
225: bindRuleSet(d, ruleSet, longConst(cost));
226: }
227:
228: protected void bindRuleSet(RuleSetDispatchFeature d,
229: String ruleSet, Feature f) {
230: bindRuleSet(d, getHeuristic(ruleSet), f);
231: }
232:
233: protected void bindRuleSet(RuleSetDispatchFeature d,
234: String ruleSet, long cost) {
235: bindRuleSet(d, getHeuristic(ruleSet), longConst(cost));
236: }
237:
238: protected void clearRuleSetBindings(RuleSetDispatchFeature d,
239: RuleSet ruleSet) {
240: d.clear(ruleSet);
241: }
242:
243: protected void clearRuleSetBindings(RuleSetDispatchFeature d,
244: String ruleSet) {
245: d.clear(getHeuristic(ruleSet));
246: }
247:
248: /**
249: * Create a projection of taclet applications to the instantiation of the
250: * schema variables <code>schemaVar</code>. If <code>schemaVar</code>
251: * is not instantiated for a particular taclet app, an error will be raised
252: */
253: protected ProjectionToTerm instOf(String schemaVar) {
254: return SVInstantiationProjection.create(new Name(schemaVar),
255: true);
256: }
257:
258: /**
259: * Create a projection of taclet applications to the instantiation of the
260: * schema variables <code>schemaVar</code>. The projection will be
261: * partial and undefined for those taclet applications that do not
262: * instantiate <code>schemaVar</code>
263: */
264: protected ProjectionToTerm instOfNonStrict(String schemaVar) {
265: return SVInstantiationProjection.create(new Name(schemaVar),
266: false);
267: }
268:
269: protected ProjectionToTerm subAt(ProjectionToTerm t, PosInTerm pit) {
270: return SubtermProjection.create(t, pit);
271: }
272:
273: protected ProjectionToTerm sub(ProjectionToTerm t, int index) {
274: return SubtermProjection.create(t, PosInTerm.TOP_LEVEL
275: .down(index));
276: }
277:
278: protected ProjectionToTerm opTerm(Operator op,
279: ProjectionToTerm[] subTerms) {
280: return TermConstructionProjection.create(op, subTerms);
281: }
282:
283: protected ProjectionToTerm opTerm(Operator op,
284: ProjectionToTerm subTerm) {
285: return opTerm(op, new ProjectionToTerm[] { subTerm });
286: }
287:
288: protected ProjectionToTerm opTerm(Operator op,
289: ProjectionToTerm subTerm0, ProjectionToTerm subTerm1) {
290: return opTerm(op, new ProjectionToTerm[] { subTerm0, subTerm1 });
291: }
292:
293: protected Feature isInstantiated(String schemaVar) {
294: return InstantiatedSVFeature.create(new Name(schemaVar));
295: }
296:
297: protected TermFeature op(Operator op) {
298: return OperatorTF.create(op);
299: }
300:
301: protected TermFeature rec(TermFeature cond, TermFeature summand) {
302: return RecSubTermFeature.create(cond, summand);
303: }
304:
305: protected TermFeature sub(TermFeature sub0) {
306: return SubTermFeature.create(new TermFeature[] { sub0 });
307: }
308:
309: protected TermFeature sub(TermFeature sub0, TermFeature sub1) {
310: return SubTermFeature.create(new TermFeature[] { sub0, sub1 });
311: }
312:
313: protected TermFeature opSub(Operator op, TermFeature sub0) {
314: return add(op(op), sub(sub0));
315: }
316:
317: protected TermFeature opSub(Operator op, TermFeature sub0,
318: TermFeature sub1) {
319: return add(op(op), sub(sub0, sub1));
320: }
321:
322: protected TermFeature eq(TermBuffer t) {
323: return EqTermFeature.create(t);
324: }
325:
326: protected Feature eq(ProjectionToTerm t1, ProjectionToTerm t2) {
327: final TermBuffer buf = new TermBuffer();
328: return let(buf, t1, applyTF(t2, eq(buf)));
329: }
330:
331: protected Feature contains(ProjectionToTerm bigTerm,
332: ProjectionToTerm searchedTerm) {
333: final TermBuffer buf = new TermBuffer();
334: return let(buf, searchedTerm, applyTF(bigTerm, not(rec(any(),
335: not(eq(buf))))));
336: }
337:
338: protected Feature println(ProjectionToTerm t) {
339: return applyTF(t, PrintTermFeature.INSTANCE);
340: }
341:
342: protected TermFeature extendsTrans(Sort s) {
343: return SortExtendsTransTermFeature.create(s);
344: }
345:
346: /**
347: * Invoke the term feature <code>tf</code> on the term that instantiation
348: * of <code>schemaVar</code>. This is the strict/safe version that raises an
349: * error of <code>schemaVar</code> is not instantiated for a particular
350: * taclet app
351: */
352: protected Feature applyTF(String schemaVar, TermFeature tf) {
353: return applyTF(instOf(schemaVar), tf);
354: }
355:
356: /**
357: * Invoke the term feature <code>tf</code> on the term that instantiation
358: * of <code>schemaVar</code>. This is the non-strict/unsafe version that
359: * simply returns zero if <code>schemaVar</code> is not instantiated for a
360: * particular taclet app
361: */
362: protected Feature applyTFNonStrict(String schemaVar, TermFeature tf) {
363: return applyTFNonStrict(instOfNonStrict(schemaVar), tf);
364: }
365:
366: /**
367: * Evaluate the term feature <code>tf</code> for the term described by the
368: * projection <code>term</code>. If <code>term</code> is undefined for
369: * a particular rule app, an exception is raised
370: */
371: protected Feature applyTF(ProjectionToTerm term, TermFeature tf) {
372: return ApplyTFFeature.create(term, tf);
373: }
374:
375: /**
376: * Evaluate the term feature <code>tf</code> for the term described by the
377: * projection <code>term</code>. If <code>term</code> is undefined for
378: * a particular rule app, zero is returned
379: */
380: protected Feature applyTFNonStrict(ProjectionToTerm term,
381: TermFeature tf) {
382: return ApplyTFFeature.createNonStrict(term, tf,
383: LongRuleAppCost.ZERO_COST);
384: }
385:
386: private final BackTrackingManager btManager = new BackTrackingManager();
387:
388: protected BackTrackingManager getBtManager() {
389: return btManager;
390: }
391:
392: public final void instantiateApp(RuleApp app, PosInOccurrence pio,
393: Goal goal, RuleAppCostCollector collector) {
394: getBtManager().setup(app);
395: do {
396: final RuleAppCost cost = instantiateApp(app, pio, goal);
397: if (cost instanceof TopRuleAppCost)
398: continue;
399: final RuleApp res = getBtManager().getResultingapp();
400: if (res == app || res == null)
401: continue;
402: collector.collect(res, cost);
403: } while (getBtManager().backtrack());
404: }
405:
406: protected abstract RuleAppCost instantiateApp(RuleApp app,
407: PosInOccurrence pio, Goal goal);
408:
409: protected Feature forEach(TermBuffer x, TermGenerator gen,
410: Feature body) {
411: return ForEachCP.create(x, gen, body, getBtManager());
412: }
413:
414: protected Feature oneOf(Feature[] features) {
415: return OneOfCP.create(features, getBtManager());
416: }
417:
418: protected Feature oneOf(Feature feature0, Feature feature1) {
419: return oneOf(new Feature[] { feature0, feature1 });
420: }
421:
422: protected Feature sum(TermBuffer x, TermGenerator gen, Feature body) {
423: return ComprehendedSumFeature.create(x, gen, body);
424: }
425:
426: // it is possible to turn off the method <code>instantiate</code>,
427: // which can be useful in order to use the same feature definitions both for
428: // cost computation and instantiation
429:
430: private boolean instantiateActive = false;
431:
432: protected void enableInstantiate() {
433: instantiateActive = true;
434: }
435:
436: protected void disableInstantiate() {
437: instantiateActive = false;
438: }
439:
440: protected Feature instantiate(Name sv, ProjectionToTerm value) {
441: if (instantiateActive)
442: return SVInstantiationCP.create(sv, value, getBtManager());
443: else
444: return longConst(0);
445: }
446:
447: protected Feature let(TermBuffer x, ProjectionToTerm value,
448: Feature body) {
449: return LetFeature.create(x, value, body);
450: }
451:
452: protected Feature instantiate(String sv, ProjectionToTerm value) {
453: return instantiate(new Name(sv), value);
454: }
455:
456: protected Feature isSubSortFeature(ProjectionToTerm s1,
457: ProjectionToTerm s2) {
458: return SortComparisionFeature.create(s1, s2,
459: SortComparisionFeature.SUBSORT);
460: }
461:
462: protected Feature implicitCastNecessary(ProjectionToTerm s1) {
463: return ImplicitCastNecessary.create(s1);
464: }
465:
466: }
|