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: package de.uka.ilkd.key.strategy.feature;
011:
012: import de.uka.ilkd.key.logic.PosInOccurrence;
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.op.Modality;
015: import de.uka.ilkd.key.logic.op.Op;
016: import de.uka.ilkd.key.logic.op.Quantifier;
017: import de.uka.ilkd.key.proof.Goal;
018: import de.uka.ilkd.key.rule.RuleApp;
019: import de.uka.ilkd.key.strategy.RuleAppCost;
020: import de.uka.ilkd.key.util.LRUCache;
021:
022: /**
023: * This abstract class contains some auxiliary methods for the selection of
024: * beta rules that are supposed to be applied. Used terminology is defined in
025: * Diss. by Martin Giese.
026: */
027: public abstract class AbstractBetaFeature implements Feature {
028:
029: /*
030: * Table of formulas which could be splitted using the beta rule
031: * This is the cache the method "isBetaCandidate" uses
032: *
033: * keys: Term values: TermInfo
034: */
035: private static LRUCache betaCandidates = new LRUCache(1000);
036:
037: /** helper for computing maxPosPath_* in TermInfo */
038: private static MaxPosPathHelper maxPosPathHelper = new MaxPosPathHelper();
039:
040: /** helper for computing maxDPath_* in TermInfo */
041: private static MaxDPathHelper maxDPathHelper = new MaxDPathHelper();
042:
043: /**
044: * Get the informations about a term
045: */
046: private static TermInfo termInfo(Term p_t) {
047: TermInfo ti;
048: synchronized (betaCandidates) {
049: ti = (TermInfo) betaCandidates.get(p_t);
050: }
051:
052: if (ti == null) {
053: ti = new TermInfo();
054:
055: ti.purePosPath_positive = hasPurePosPathHelp(p_t, true);
056: ti.purePosPath_negative = hasPurePosPathHelp(p_t, false);
057:
058: ti.maxPosPath_positive = maxPosPathHelp(p_t, true);
059: ti.maxPosPath_negative = maxPosPathHelp(p_t, false);
060:
061: ti.maxDPath_positive = maxDPathHelp(p_t, true);
062: ti.maxDPath_negative = maxDPathHelp(p_t, false);
063:
064: ti.containsNegAtom_positive = containsNegAtomHelp(p_t, true);
065: ti.containsNegAtom_negative = containsNegAtomHelp(p_t,
066: false);
067:
068: ti.containsQuantifier = containsQuantifierHelp(p_t);
069:
070: ti.candidate = candidateHelp(p_t, ti);
071:
072: synchronized (betaCandidates) {
073: if (betaCandidates.size() > 1000)
074: betaCandidates.clear();
075: betaCandidates.put(p_t, ti);
076: }
077: }
078:
079: return ti;
080: }
081:
082: private abstract static class MaxPathHelper {
083: public int compute(Term p_t, boolean p_positive) {
084: if (p_t.op() == (p_positive ? Op.AND : Op.OR))
085: return compute(p_t.sub(0), p_positive)
086: + compute(p_t.sub(1), p_positive);
087:
088: else if (p_t.op() == (p_positive ? Op.OR : Op.AND))
089: return Math.max(compute(p_t.sub(0), p_positive),
090: compute(p_t.sub(1), p_positive));
091:
092: else if (p_t.op() == Op.NOT)
093: return compute(p_t.sub(0), !p_positive);
094:
095: else if (p_positive && p_t.op() == Op.IMP)
096: return Math.max(compute(p_t.sub(0), !p_positive),
097: compute(p_t.sub(1), p_positive));
098:
099: else if (!p_positive && p_t.op() == Op.IMP)
100: return compute(p_t.sub(0), !p_positive)
101: + compute(p_t.sub(1), p_positive);
102:
103: else if (p_positive && p_t.op() == Op.EQV)
104: return Math.max(compute(p_t.sub(0), p_positive)
105: + compute(p_t.sub(1), p_positive), compute(p_t
106: .sub(0), !p_positive)
107: + compute(p_t.sub(1), !p_positive));
108:
109: else if (!p_positive && p_t.op() == Op.EQV)
110: return Math.max(compute(p_t.sub(0), !p_positive)
111: + compute(p_t.sub(1), p_positive), compute(p_t
112: .sub(0), p_positive)
113: + compute(p_t.sub(1), !p_positive));
114:
115: return computeDefault(p_t, p_positive);
116: }
117:
118: protected abstract int computeDefault(Term p_t,
119: boolean p_positive);
120: }
121:
122: private static class MaxPosPathHelper extends MaxPathHelper {
123: protected int computeDefault(Term p_t, boolean p_positive) {
124: if (alwaysReplace(p_t))
125: return 1;
126:
127: return p_positive ? 0 : 1;
128: }
129: }
130:
131: private static class MaxDPathHelper extends MaxPathHelper {
132: protected int computeDefault(Term p_t, boolean p_positive) {
133: return 1;
134: }
135: }
136:
137: private static int maxPosPathHelp(Term p_t, boolean p_positive) {
138: return maxPosPathHelper.compute(p_t, p_positive);
139: }
140:
141: private static int maxDPathHelp(Term p_t, boolean p_positive) {
142: return maxDPathHelper.compute(p_t, p_positive);
143: }
144:
145: /**
146: * TODO: It would be nice to integrate this with the framework for
147: * computing maxPosPath/maxDPath, however different return types pose
148: * a problem. Perhaps this could be solved using generics?
149: */
150: private static boolean hasPurePosPathHelp(Term p_t,
151: boolean p_positive) {
152: if (p_t.op() == (p_positive ? Op.AND : Op.OR))
153: return hasPurePosPath(p_t.sub(0), p_positive)
154: && hasPurePosPath(p_t.sub(1), p_positive);
155:
156: else if (p_t.op() == (p_positive ? Op.OR : Op.AND))
157: return hasPurePosPath(p_t.sub(0), p_positive)
158: || hasPurePosPath(p_t.sub(1), p_positive);
159:
160: else if (p_t.op() == Op.NOT)
161: return hasPurePosPath(p_t.sub(0), !p_positive);
162:
163: else if (p_positive && p_t.op() == Op.IMP)
164: return hasPurePosPath(p_t.sub(0), !p_positive)
165: || hasPurePosPath(p_t.sub(1), p_positive);
166:
167: else if (!p_positive && p_t.op() == Op.IMP)
168: return hasPurePosPath(p_t.sub(0), !p_positive)
169: && hasPurePosPath(p_t.sub(1), p_positive);
170:
171: else if (p_positive && p_t.op() == Op.EQV)
172: return (hasPurePosPath(p_t.sub(0), p_positive) && hasPurePosPath(
173: p_t.sub(1), p_positive))
174: || (hasPurePosPath(p_t.sub(0), !p_positive) && hasPurePosPath(
175: p_t.sub(1), !p_positive));
176:
177: else if (!p_positive && p_t.op() == Op.EQV)
178: return (hasPurePosPath(p_t.sub(0), !p_positive) && hasPurePosPath(
179: p_t.sub(1), p_positive))
180: || (hasPurePosPath(p_t.sub(0), p_positive) && hasPurePosPath(
181: p_t.sub(1), !p_positive));
182:
183: else if (alwaysReplace(p_t))
184: return true;
185:
186: return !p_positive;
187: }
188:
189: private static boolean containsNegAtomHelp(Term p_t,
190: boolean p_positive) {
191: if (p_t.op() == Op.AND || p_t.op() == Op.OR)
192: return containsNegAtom(p_t.sub(0), p_positive)
193: || containsNegAtom(p_t.sub(1), p_positive);
194:
195: else if (p_t.op() == Op.NOT)
196: return containsNegAtom(p_t.sub(0), !p_positive);
197:
198: else if (p_t.op() == Op.IMP)
199: return containsNegAtom(p_t.sub(0), !p_positive)
200: || containsNegAtom(p_t.sub(1), p_positive);
201:
202: else if (p_t.op() == Op.EQV || alwaysReplace(p_t))
203: return true;
204:
205: return !p_positive;
206: }
207:
208: private static boolean containsQuantifierHelp(Term p_t) {
209: if (p_t.op() == Op.AND || p_t.op() == Op.OR
210: || p_t.op() == Op.IMP || p_t.op() == Op.EQV)
211: return containsQuantifier(p_t.sub(0))
212: || containsQuantifier(p_t.sub(1));
213: else if (p_t.op() == Op.NOT)
214: return containsQuantifier(p_t.sub(0));
215: else
216: return alwaysReplace(p_t);
217: }
218:
219: private static Object candidateHelp(Term p_t, TermInfo p_ti) {
220: if (p_t.op() == Op.IMP || p_t.op() == Op.OR)
221: return isBetaCandidateHelp(p_ti, false) ? TermInfo.CAND_LEFT
222: : TermInfo.CAND_NEVER;
223: else if (p_t.op() == Op.AND)
224: return isBetaCandidateHelp(p_ti, true) ? TermInfo.CAND_RIGHT
225: : TermInfo.CAND_NEVER;
226: else if (p_t.op() == Op.EQV) {
227: if (isBetaCandidateHelp(p_ti, true))
228: return isBetaCandidateHelp(p_ti, false) ? TermInfo.CAND_BOTH
229: : TermInfo.CAND_RIGHT;
230: else
231: return isBetaCandidateHelp(p_ti, false) ? TermInfo.CAND_LEFT
232: : TermInfo.CAND_NEVER;
233: }
234:
235: return TermInfo.CAND_NEVER;
236: }
237:
238: private static boolean isBetaCandidateHelp(TermInfo p_ti,
239: boolean p_positive) {
240: /* return p_ti.containsQuantifier
241: || ( p_positive ? p_ti.purePosPath_positive
242: : p_ti.purePosPath_negative ); */
243: return p_ti.containsQuantifier
244: || (p_positive ? p_ti.maxPosPath_positive
245: : p_ti.maxPosPath_negative) > 1;
246: }
247:
248: /**
249: * p_t contains a d-path consisting only of positive literals (as a formula
250: * of the antecedent)
251: */
252: protected static boolean hasPurePosPath(Term p_t, boolean p_positive) {
253: TermInfo ti = termInfo(p_t);
254: return p_positive ? ti.purePosPath_positive
255: : ti.purePosPath_negative;
256: }
257:
258: /**
259: * The maximal number of positive literals occurring within a
260: * d-path of "p_t" as a formula of the antecedent
261: */
262: protected static int maxPosPath(Term p_t, boolean p_positive) {
263: TermInfo ti = termInfo(p_t);
264: return p_positive ? ti.maxPosPath_positive
265: : ti.maxPosPath_negative;
266: }
267:
268: /**
269: * The length (number of literals) of the maximum d-path of the given
270: * formula as a formula of the antecedent
271: */
272: protected static int maxDPath(Term p_t, boolean p_positive) {
273: TermInfo ti = termInfo(p_t);
274: return p_positive ? ti.maxDPath_positive : ti.maxDPath_negative;
275: }
276:
277: /**
278: * @return true iff "p_t" contains a quantifier or a modality
279: */
280: protected static boolean containsQuantifier(Term p_t) {
281: TermInfo ti = termInfo(p_t);
282: return ti.containsQuantifier;
283: }
284:
285: /**
286: * @return true iff the given
287: * formula contains a negated atom as a formula of the antecedent
288: */
289: protected static boolean containsNegAtom(Term p_t,
290: boolean p_positive) {
291: TermInfo ti = termInfo(p_t);
292: return p_positive ? ti.containsNegAtom_positive
293: : ti.containsNegAtom_negative;
294: }
295:
296: /**
297: * @return true iff the sign of "p_t" is not relevant (quantifiers
298: * etc. could be positive or negative)
299: */
300: public static boolean alwaysReplace(Term p_t) {
301: return p_t.op() instanceof Modality
302: || p_t.op() instanceof Quantifier;
303: }
304:
305: /**
306: * @return true iff the formula p_t could be splitted using the
307: * beta rule
308: */
309: protected static boolean isBetaCandidate(Term p_t, boolean p_inAntec) {
310: TermInfo ti = termInfo(p_t);
311: return ti.candidate == TermInfo.CAND_BOTH
312: || ti.candidate == (p_inAntec ? TermInfo.CAND_LEFT
313: : TermInfo.CAND_RIGHT);
314: }
315:
316: /**
317: * Informations about a term as cached within "betaCandidates"
318: */
319: private static class TermInfo {
320:
321: public static final Integer CAND_NEVER = new Integer(0);
322: public static final Integer CAND_LEFT = new Integer(1);
323: public static final Integer CAND_RIGHT = new Integer(2);
324: public static final Integer CAND_BOTH = new Integer(3);
325:
326: /** formula is positive (not negated) */
327: public int maxPosPath_positive;
328:
329: public boolean purePosPath_positive;
330:
331: // length of the maximum d-path
332: public int maxDPath_positive;
333:
334: /** formula contains a negative atom */
335: public boolean containsNegAtom_positive;
336:
337: /** formula is negated */
338: public int maxPosPath_negative;
339:
340: public boolean purePosPath_negative;
341:
342: // length of the maximum d-path
343: public int maxDPath_negative;
344:
345: /** formula contains a negative atom */
346: public boolean containsNegAtom_negative;
347:
348: /** formula contains a quantifier or modality */
349: public boolean containsQuantifier;
350:
351: /** one of CAND_* */
352: public Object candidate;
353: }
354:
355: /**
356: * Compute the cost of a RuleApp.
357: * @param app the RuleApp
358: * @param pos position where <code>app</code> is to be applied
359: * @param goal the goal on which <code>app</code> is to be applied
360: * @return the cost of <code>app</code>
361: */
362: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
363: Goal goal) {
364: assert pos != null : "Feature is only applicable to rules with find";
365:
366: final Term findTerm = pos.constrainedFormula().formula();
367:
368: return doComputation(pos, findTerm);
369: }
370:
371: protected abstract RuleAppCost doComputation(PosInOccurrence pos,
372: Term findTerm);
373:
374: }
|