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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017: package de.uka.ilkd.key.strategy.quantifierHeuristics;
018:
019: import java.util.HashMap;
020: import java.util.HashSet;
021: import java.util.Iterator;
022: import java.util.Map;
023: import java.util.Set;
024:
025: import de.uka.ilkd.key.logic.IteratorOfTerm;
026: import de.uka.ilkd.key.logic.ListOfTerm;
027: import de.uka.ilkd.key.logic.SLListOfTerm;
028: import de.uka.ilkd.key.logic.SetAsListOfTerm;
029: import de.uka.ilkd.key.logic.SetOfTerm;
030: import de.uka.ilkd.key.logic.Term;
031: import de.uka.ilkd.key.logic.TermBuilder;
032: import de.uka.ilkd.key.logic.TermFactory;
033: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
034: import de.uka.ilkd.key.logic.op.AttributeOp;
035: import de.uka.ilkd.key.logic.op.IUpdateOperator;
036: import de.uka.ilkd.key.logic.op.Modality;
037: import de.uka.ilkd.key.logic.op.Op;
038: import de.uka.ilkd.key.logic.op.Operator;
039: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
040: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
041: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
042: import de.uka.ilkd.key.logic.sort.Sort;
043: import de.uka.ilkd.key.util.LRUCache;
044:
045: /**
046: * This classe is used to select and store <code>Trigger</code>s
047: * for a quantified formula in Prenex CNF(PCNF).
048: */
049:
050: class TriggersSet {
051:
052: /**a <code>HashMap</code> from <code>Term</code> to
053: * <code>TriggersSet</code> uses to cache all created TriggersSets*/
054: private final static Map cache = new LRUCache(1000);
055:
056: /** Quantified formula of PCNF*/
057: private final Term allTerm;
058:
059: /**all <code>Trigger</code>s for <code>allTerm</code>*/
060: private SetOfTrigger allTriggers = SetAsListOfTrigger.EMPTY_SET;
061:
062: /**a <code>HashMap</code> from <code>Term</code> to <code>Trigger</code>
063: * which stores different subterms of <code>allTerm</code>
064: * with its according trigger */
065: private final Map termToTrigger = new HashMap();
066:
067: /**all universal variables of <code>allTerm</code>*/
068: private final SetOfQuantifiableVariable uniQuantifiedVariables;
069:
070: /**
071: * Replacement of the bound variables in <code>allTerm</code> with
072: * metavariables and constants
073: */
074: private final Substitution replacementWithMVs;
075:
076: private TriggersSet(Term allTerm) {
077: this .allTerm = allTerm;
078: replacementWithMVs = ReplacerOfQuanVariablesWithMetavariables
079: .createSubstitutionForVars(allTerm);
080: uniQuantifiedVariables = getAllUQS(allTerm);
081: initTriggers();
082: }
083:
084: static TriggersSet create(Term allTerm) {
085: TriggersSet trs = (TriggersSet) cache.get(allTerm);
086: if (trs == null) {
087: // add check whether it is in PCNF
088: trs = new TriggersSet(allTerm);
089: cache.put(allTerm, trs);
090: }
091: return trs;
092: }
093:
094: /**
095: * @param allterm
096: * @return return all univesal variables of <code>allterm</code>
097: */
098: private SetOfQuantifiableVariable getAllUQS(Term allterm) {
099: final Operator op = allterm.op();
100: if (op == Op.ALL) {
101: QuantifiableVariable v = allterm.varsBoundHere(0)
102: .getQuantifiableVariable(0);
103: return getAllUQS(allterm.sub(0)).add(v);
104: }
105: if (op == Op.EX)
106: return getAllUQS(allterm.sub(0));
107: return SetAsListOfQuantifiableVariable.EMPTY_SET;
108: }
109:
110: /**
111: * initial all <code>Trigger</code>s by finding triggers in every clauses
112: */
113: private void initTriggers() {
114: final QuantifiableVariable var = allTerm.varsBoundHere(0)
115: .getQuantifiableVariable(0);
116: final IteratorOfTerm it = TriggerUtils.iteratorByOperator(
117: TriggerUtils.discardQuantifiers(allTerm), Op.AND);
118: while (it.hasNext()) {
119: final Term clause = it.next();
120: // a trigger should contain the first variable of allTerm
121: if (clause.freeVars().contains(var)) {
122: ClauseTrigger ct = new ClauseTrigger(clause);
123: ct.createTriggers();
124: }
125: }
126: }
127:
128: /**
129: *
130: * @param trigger
131: * a <code>Term</code>
132: * @param qvs
133: * all universal variables of <code>trigger</code>
134: * @param isUnify
135: * true if <code>trigger</code>contains existential variable
136: * @param isElement
137: * true if the <code>Trigger</code> to be created is taken as a
138: * element of multi-trigger
139: * @return a <code>Trigger</code> with <code>trigger</code> as its term
140: */
141: private Trigger createUniTrigger(Term trigger,
142: SetOfQuantifiableVariable qvs, boolean isUnify,
143: boolean isElement) {
144: Trigger t = (Trigger) termToTrigger.get(trigger);
145: if (t == null) {
146: t = new UniTrigger(trigger, qvs, isUnify, isElement, this );
147: termToTrigger.put(trigger, t);
148: }
149: return t;
150: }
151:
152: /**
153: *
154: * @param trs
155: * @param clause
156: * a <code>Term</code> of clause form
157: * @param qvs
158: * all universal varaibles of all <code>clause</code>
159: * @return
160: */
161: private Trigger createMultiTrigger(SetOfTrigger trs, Term clause,
162: SetOfQuantifiableVariable qvs) {
163: return new MultiTrigger(trs, qvs, clause);
164: }
165:
166: /**
167: * this class is used to find <code>Trigger</code>s in a clause. And it
168: * will try to find triggers from every literals in this clause. Every
169: * substerm of literal that satify the conditions:(1)it should not be a
170: * variable, (2) it doesn't contain propersitional connectives, (3) it is
171: * not in loop, (4) it should contains all universal variables in the clause
172: * and the first variable of <code>allTerm</code> (5) it doesn't contain
173: * subtrigger, will be selected as an Uni-trigger. If a literal does not
174: * contain all universal variables in clause, a set of subterms of this
175: * literal will be selected as Multi-trigger's elements which are actually
176: * uni-triggers except that condition (2) will be changedand into that it
177: * contains all universal variables in the literal in. Afterwards, a set of
178: * multi-triggers will be constructed by combining thoes elements so that
179: * all variables in clause should be include by some of them.
180: */
181: private class ClauseTrigger {
182:
183: final Term clause;
184: /**all unversal variables of <code>clause</code>*/
185: final SetOfQuantifiableVariable selfUQVS;
186: /**elements which are uni-trigges and will be used to construct
187: *several multi-triggers for <code>clause</code> */
188: private SetOfTrigger elementsOfMultiTrigger = SetAsListOfTrigger.EMPTY_SET;
189:
190: public ClauseTrigger(Term clause) {
191: this .clause = clause;
192: selfUQVS = TriggerUtils.intersect(uniQuantifiedVariables,
193: clause.freeVars());
194:
195: }
196:
197: /**
198: *Searching uni-triggers and elements of multi-triggers in every
199: *literal in this <code>clause</code> and add those uni-triggers
200: *to the goal trigger set. At last construct multi-triggers from
201: * those elements.
202: */
203: public void createTriggers() {
204: final IteratorOfTerm it = TriggerUtils.iteratorByOperator(
205: clause, Op.OR);
206: while (it.hasNext()) {
207: final Term oriTerm = it.next();
208: final IteratorOfTerm it2 = expandIfThenElse(oriTerm)
209: .iterator();
210: while (it2.hasNext()) {
211: Term t = it2.next();
212: if (t.op() == Op.NOT)
213: t = t.sub(0);
214: recAddTriggers(t);
215: }
216: }
217: setMultiTriggers(elementsOfMultiTrigger.toArray(), 0);
218: }
219:
220: /**
221: * @param term one atom at the begining
222: * @param litQVS all universal variables of <code>term</code>
223: * @return true if find any trigger from <code>term</code>
224: */
225: private boolean recAddTriggers(Term term) {
226: if (!mightContainTriggers(term))
227: return false;
228:
229: final SetOfQuantifiableVariable uniVarsInTerm = TriggerUtils
230: .intersect(term.freeVars(), selfUQVS);
231:
232: boolean foundSubtriggers = false;
233: for (int i = 0; i < term.arity(); i++) {
234: final Term subTerm = term.sub(i);
235: final boolean found = recAddTriggers(subTerm);
236:
237: if (found && uniVarsInTerm.subset(subTerm.freeVars()))
238: foundSubtriggers = true;
239: }
240:
241: if (!foundSubtriggers) {
242: addUniTrigger(term);
243: return true;
244: }
245:
246: return foundSubtriggers;
247: }
248:
249: private SetOfTerm expandIfThenElse(Term t) {
250: final SetOfTerm[] possibleSubs = new SetOfTerm[t.arity()];
251: boolean changed = false;
252: for (int i = 0; i != t.arity(); ++i) {
253: final Term oriSub = t.sub(i);
254: possibleSubs[i] = expandIfThenElse(oriSub);
255: changed = changed || possibleSubs[i].size() != 1
256: || possibleSubs[i].iterator().next() != oriSub;
257: }
258:
259: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
260: if (t.op() == Op.IF_THEN_ELSE)
261: res = possibleSubs[1].union(possibleSubs[2]);
262:
263: if (!changed)
264: return res.add(t);
265:
266: final Term[] chosenSubs = new Term[t.arity()];
267: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[t
268: .arity()];
269: for (int i = 0; i != t.arity(); ++i)
270: boundVars[i] = t.varsBoundHere(i);
271:
272: return res.union(combineSubterms(t, possibleSubs,
273: chosenSubs, boundVars, 0));
274: }
275:
276: private SetOfTerm combineSubterms(Term oriTerm,
277: SetOfTerm[] possibleSubs, Term[] chosenSubs,
278: ArrayOfQuantifiableVariable[] boundVars, int i) {
279: if (i >= possibleSubs.length) {
280: final Term res = TermFactory.DEFAULT.createTerm(oriTerm
281: .op(), chosenSubs, boundVars, oriTerm
282: .javaBlock());
283: return SetAsListOfTerm.EMPTY_SET.add(res);
284: }
285:
286: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
287: final IteratorOfTerm it = possibleSubs[i].iterator();
288: while (it.hasNext()) {
289: chosenSubs[i] = it.next();
290: res = res.union(combineSubterms(oriTerm, possibleSubs,
291: chosenSubs, boundVars, i + 1));
292: }
293: return res;
294: }
295:
296: /**
297: * Check whether a given term (or a subterm of the term) might be a
298: * trigger candidate
299: */
300: private boolean mightContainTriggers(Term term) {
301: if (term.freeVars().size() == 0)
302: return false;
303: final Operator op = term.op();
304: if (op instanceof Modality || op instanceof IUpdateOperator
305: || op instanceof QuantifiableVariable)
306: return false;
307: if (!UniTrigger.passedLoopTest(term, allTerm))
308: return false;
309: return true;
310: }
311:
312: /**
313: * Further criteria for triggers. This is just a HACK, there should be
314: * a more general framework for characterising acceptable triggers
315: */
316: private boolean isAcceptableTrigger(Term term) {
317: final Operator op = term.op();
318:
319: // we do not want to match on expressions a.<created>
320: if (op instanceof AttributeOp) {
321: final AttributeOp attrOp = (AttributeOp) op;
322: if (attrOp.attribute().name().toString().endsWith(
323: "<created>"))
324: return false;
325: }
326:
327: // matching on equations and inequalities does not seem to have any
328: // positive effect for the time being
329: if (op == Op.EQUALS || "leq".equals(op.name().toString())
330: || "geq".equals(op.name().toString()))
331: return false;
332:
333: /*
334: if ( op == Op.EQUALS ) {
335: // we do not want to match on equations t = null
336: if ( term.sub ( 0 ).sort () == Sort.NULL
337: || term.sub ( 1 ).sort () == Sort.NULL ) return false;
338:
339: // we do not want to match on equations t = TRUE
340: if ( "TRUE".equals ( term.sub ( 0 ).op ().name ().toString () )
341: || "TRUE".equals ( term.sub ( 1 ).op ().name ().toString () ) )
342: return false;
343: }
344: */
345:
346: return true;
347: }
348:
349: /**
350: * add a uni-trigger to triggers set or add an element of
351: * multi-triggers for this clause
352: * @return <code>true</code> if a uni-trigger was added
353: */
354: private void addUniTrigger(Term term) {
355: if (!isAcceptableTrigger(term))
356: return;
357: final boolean isUnify = !term.freeVars().subset(selfUQVS);
358: final boolean isElement = !selfUQVS.subset(term.freeVars());
359: final SetOfQuantifiableVariable uniVarsInTerm = TriggerUtils
360: .intersect(term.freeVars(), selfUQVS);
361: Trigger t = createUniTrigger(term, uniVarsInTerm, isUnify,
362: isElement);
363: if (isElement)
364: elementsOfMultiTrigger = elementsOfMultiTrigger.add(t);
365: else
366: allTriggers = allTriggers.add(t);
367: }
368:
369: /**
370: * add a uni-trigger to triggers set or add an element of
371: * multi-triggers for this clause
372: * @return <code>true</code> if a uni-trigger was added
373: */
374: private boolean addMultiTrigger(Term term) {
375: if (!isAcceptableTrigger(term))
376: return false;
377: final boolean isUnify = !term.freeVars().subset(selfUQVS);
378: System.out.println(term);
379: final boolean isElement = !selfUQVS.subset(term.freeVars());
380: final SetOfQuantifiableVariable uniVarsInTerm = TriggerUtils
381: .intersect(term.freeVars(), selfUQVS);
382: Trigger t = createUniTrigger(term, uniVarsInTerm, isUnify,
383: isElement);
384: if (isElement) {
385: elementsOfMultiTrigger = elementsOfMultiTrigger.add(t);
386: return false;
387: } else {
388: allTriggers = allTriggers.add(t);
389: return true;
390: }
391: }
392:
393: /**
394: * find all possible combination of <code>ts</code>. Once a
395: * combination of elements contains all variables of this clause,
396: * it will be used to contruct the multi-trigger which will be
397: * add to triggers set
398: * @param ts elements of multi-triggers at the begining
399: * @param i
400: * @return
401: */
402: private Set setMultiTriggers(Trigger[] ts, int i) {
403: Set res = new HashSet();
404: if (i >= ts.length)
405: return res;
406: SetOfTrigger tsi = SetAsListOfTrigger.EMPTY_SET.add(ts[i]);
407: res.add(tsi);
408: Set nextTriggers = setMultiTriggers(ts, i + 1);
409: res.addAll(nextTriggers);
410: Iterator it = nextTriggers.iterator();
411: while (it.hasNext()) {
412: SetOfTrigger next = (SetOfTrigger) it.next();
413: next = next.add(ts[i]);
414: if (addMultiTrigger(next))
415: continue;
416: res.add(next);
417: }
418: return res;
419: }
420:
421: /**
422: * try to construct a multi-trigger by given <code>ts</code>
423: *
424: * @param trs
425: * a set of trigger
426: * @return true if <code>trs</code> contains all universal varaibles
427: * of this clause, and add the contstructed multi-trigger to
428: * triggers set
429: */
430: private boolean addMultiTrigger(SetOfTrigger trs) {
431: SetOfQuantifiableVariable mulqvs = SetAsListOfQuantifiableVariable.EMPTY_SET;
432: IteratorOfTrigger it = trs.iterator();
433: while (it.hasNext()) {
434: mulqvs = mulqvs.union(it.next().getTriggerTerm()
435: .freeVars());
436: }
437: if (selfUQVS.subset(mulqvs)) {
438: Trigger mt = createMultiTrigger(trs, clause, selfUQVS);
439: allTriggers = allTriggers.add(mt);
440: return true;
441: }
442: return false;
443: }
444: }
445:
446: public Term getQuantifiedFormula() {
447: return allTerm;
448: }
449:
450: public SetOfTrigger getAllTriggers() {
451: return allTriggers;
452: }
453:
454: public Substitution getReplacementWithMVs() {
455: return replacementWithMVs;
456: }
457:
458: public SetOfQuantifiableVariable getUniQuantifiedVariables() {
459: return uniQuantifiedVariables;
460: }
461: }
|