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.logic;
012:
013: import java.util.*;
014:
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.*;
017: import de.uka.ilkd.key.rule.ListOfUpdatePair;
018: import de.uka.ilkd.key.rule.UpdatePair;
019: import de.uka.ilkd.key.util.Debug;
020: import de.uka.ilkd.key.util.LRUCache;
021:
022: /**
023: * The TermFactory is the <em>only</em> way to create terms using constructos of
024: * class Term or any of its subclasses. It is the
025: * only class that implements and may exploit knowledge about sub
026: * classes of {@link Term} all other classes of the system only know
027: * about terms what the {@link Term} class offers them.
028: *
029: * This class is used to encapsulate knowledge about the internal term structures.
030: * See {@link de.uka.ilkd.key.logic.TermBuilder} for more convienient methods to create
031: * terms.
032: */
033: public class TermFactory {
034:
035: /**
036: * class used a key for term cache if more than one composite needs
037: * to be compared
038: * Attention: for complex terms comparing may be too expensive in these
039: * cases do not cache them
040: */
041: static class CacheKey {
042:
043: private final static Object DUMMY_KEY_COMPOSITE = new Object();
044:
045: private final Object o1, o2, o3;
046:
047: /**
048: * the first key composite is compared by identity
049: * the second key composite is compared via equals
050: * @param o1 the first key composite
051: * @param o2 the second key composite (non null)
052: */
053: public CacheKey(Object o1, Object o2) {
054: this .o1 = o1;
055: this .o2 = o2;
056: this .o3 = DUMMY_KEY_COMPOSITE;
057: }
058:
059: /**
060: * the first key composite is compared by identity
061: * the second and third key composite is compared via equals
062: * @param o1 the first key composite
063: * @param o2 the second key composite (non null)
064: * @param o3 the third key composite (non null)
065: */
066: public CacheKey(Object o1, Object o2, Object o3) {
067: this .o1 = o1;
068: this .o2 = o2;
069: this .o3 = o3;
070: }
071:
072: public int hashCode() {
073: return o1.hashCode() + 17 * o2.hashCode() + 7
074: * o3.hashCode();
075: }
076:
077: public boolean equals(Object o) {
078: if (!(o instanceof CacheKey)) {
079: return false;
080: }
081: final CacheKey ck = (CacheKey) o;
082: return o1 == ck.o1 && o2.equals(ck.o2) && o3.equals(ck.o3);
083: }
084:
085: }
086:
087: private static Map cache = Collections
088: .synchronizedMap(new LRUCache(5000));
089:
090: /** An instance of TermFactory */
091: public static final TermFactory DEFAULT = new TermFactory();
092:
093: private static final Term[] NO_SUBTERMS = new Term[0];
094:
095: /** creates t[index] with top operand op
096: */
097: public Term createArrayTerm(ArrayOp op, Term t, Term index) {
098: if (op == null) {
099: throw new IllegalArgumentException("null-Operator at"
100: + "TermFactory");
101: }
102: return new OpTerm(op, new Term[] { t, index }).checked();
103: }
104:
105: /**
106: * creates a term representing a shadowed array access on the
107: * <code>index</code>-th component of <code>t</code>
108: * @param op the ShadowArrayOp used to access "shadowed memory
109: * areas"
110: * @param t the Term representing the array whose
111: * <code>index</code> component is accessed
112: * @param index the Term describing the index of the array
113: * component to be accessed
114: * @param shadownum the Term describing the nested scope of
115: * shadowed access
116: * @returns the term representing a shadowed array access on the
117: * <code>index</code> component of <code>t</code> with a shadow
118: * depth of <code>shadownum</code>
119: */
120: public Term createShadowArrayTerm(ShadowArrayOp op, Term t,
121: Term index, Term shadownum) {
122: if (op == null) {
123: throw new IllegalArgumentException(
124: "Creation of a shadowed array access term"
125: + "failed due to missing operator.");
126: }
127: return new OpTerm(op, new Term[] { t, index, shadownum })
128: .checked();
129: }
130:
131: /**
132: * creates a term representing a shadowed access on a multi
133: * dimensional array. The exact component is specified by the
134: * array of indices.
135: * @param op the ShadowArrayOp used to access "shadowed memory
136: * areas"
137: * @param t the Term representing the array whose
138: * <code>index</code> component is accessed
139: * @param index an array of Term specifying the array component to
140: * be accessed
141: * @param shadownum the Term describing the nested scope of
142: * shadowed access
143: * @returns the term representing a shadowed array access on the
144: * specified component of <code>t</code> with a shadow
145: * depth of <code>shadownum</code>
146: */
147: public Term createShadowArrayTerm(ShadowArrayOp op, Term t,
148: Term[] index, Term shadownum) {
149: if (op == null) {
150: throw new IllegalArgumentException(
151: "null-Operator at TermFactory");
152: }
153: final Term[] t1 = new Term[3];
154: t1[0] = t;
155:
156: for (int i = 0; i < index.length; i++) {
157: t1[1] = index[i];
158: t1[2] = shadownum;
159: t1[0] = new OpTerm(op, t1).checked();
160: }
161:
162: return t1[0];
163: }
164:
165: /**
166: * creates a term representing an array access on the
167: * <code>index</code>-th component of <code>t</code>
168: * @param op the ArrayOp used to access an array of type of
169: * <code>t</code>
170: * @param t the Term representing the array to be accessed
171: * @param index the Term describing the index of the array
172: * component to be accessed
173: */
174: public Term createArrayTerm(ArrayOp op, Term t, Term[] index) {
175: if (op == null) {
176: throw new IllegalArgumentException(
177: "null-Operator at TermFactory");
178: }
179: final Term[] t1 = new Term[2];
180: t1[0] = t;
181: for (int i = 0; i < index.length; i++) {
182: t1[1] = index[i];
183: t1[0] = new OpTerm(op, t1).checked();
184: }
185: return t1[0];
186: }
187:
188: /**
189: * @param arrayOp the shadowed or normal version of the array
190: * access operator
191: * @param subs array of subterms
192: * @return the term representing an array access
193: */
194: public Term createArrayTerm(ArrayOp arrayOp, Term[] subs) {
195: if (arrayOp == null) {
196: throw new IllegalArgumentException(
197: "null-Operator at TermFactory");
198: }
199: Term arrayTerm;
200: if (subs.length == 2) {
201: // we cache only the most common case
202: final CacheKey key = new CacheKey(arrayOp, subs[0], subs[1]);
203: arrayTerm = (Term) cache.get(key);
204: if (arrayTerm == null) {
205: arrayTerm = new OpTerm(arrayOp, subs).checked();
206: cache.put(key, arrayTerm);
207: }
208:
209: } else {
210: arrayTerm = new OpTerm(arrayOp, subs).checked();
211: }
212:
213: return arrayTerm;
214: }
215:
216: public Term createAttributeTerm(AttributeOp op, Term term) {
217: Debug.assertFalse(op instanceof ShadowedOperator,
218: "Tried to create a shadowed attribute.");
219: if (op.attribute() instanceof ProgramVariable
220: && ((ProgramVariable) op.attribute()).isStatic()) {
221: return new OpTerm(op.attribute(), NO_SUBTERMS).checked();
222: }
223: return new OpTerm(op, new Term[] { term }).checked();
224: }
225:
226: /**
227: * creates a term representing an attribute access
228: * @param attrOp the AttributeOp representing the attribute to be accessed
229: * @param subs an array of Term containing the subterms (usually of
230: * length 1 but may have length 2 for shadowed accesses)
231: * @return the term <code>subs[0].attr</code>
232: * (or <code>subs[0]^(subs[1]).attr)</code>)
233: */
234: public Term createAttributeTerm(AttributeOp attrOp, Term[] subs) {
235: if (attrOp instanceof ShadowedOperator) {
236: return createShadowAttributeTerm(
237: (ShadowAttributeOp) attrOp, subs[0], subs[1]);
238: }
239: return createAttributeTerm(attrOp, subs[0]);
240: }
241:
242: /** creates an attribute term that references to a field of a class
243: * @param var the variable the attribute term references to
244: * @param term the Term describing the class/object of which the
245: * attribute value has to be determined
246: * @return the attribute term "term.var"
247: */
248: public Term createAttributeTerm(ProgramVariable var, Term term) {
249: if (var.isStatic()) {
250: return createVariableTerm(var);
251: }
252:
253: final CacheKey key = new CacheKey(var, term);
254: Term attrTerm = (Term) cache.get(key);
255: if (attrTerm == null) {
256: attrTerm = new OpTerm(AttributeOp.getAttributeOp(var),
257: new Term[] { term }).checked();
258: cache.put(key, attrTerm);
259: }
260: return attrTerm;
261: }
262:
263: /**
264: * creates an attribute term that references to a field of a class
265: * @param var the variable the attribute term references to
266: * @param term the Term describing the class/object of which the
267: * attribute value has to be determined
268: * @return the attribute term "term.var"
269: */
270: public Term createAttributeTerm(SchemaVariable var, Term term) {
271: return new OpTerm(AttributeOp
272: .getAttributeOp((IProgramVariable) var),
273: new Term[] { term }).checked();
274: }
275:
276: public Term createBoxTerm(JavaBlock javaBlock, Term subTerm) {
277: return createProgramTerm(Op.BOX, javaBlock, subTerm);
278: }
279:
280: public Term createDiamondTerm(JavaBlock javaBlock, Term subTerm) {
281: return createProgramTerm(Op.DIA, javaBlock, subTerm);
282: }
283:
284: /**
285: * creates a EqualityTerm with a given equality operator. USE THIS WITH
286: * CARE! THERE IS NO CHECK THAT THE EQUALITY OPERATOR MATCHES THE TERMS.
287: */
288: public Term createEqualityTerm(Equality op, Term[] subTerms) {
289: return new OpTerm(op, subTerms).checked();
290: }
291:
292: /**
293: * creates an EqualityTerm with a given equality operator. USE THIS WITH
294: * CARE! THERE IS NO CHECK THAT THE EQUALITY OPERATOR MATCHES THE TERMS.
295: */
296: public Term createEqualityTerm(Equality op, Term t1, Term t2) {
297: return createEqualityTerm(op, new Term[] { t1, t2 });
298: }
299:
300: /** create an EqualityTerm with the correct equality symbol for
301: * the sorts involved, according to {@link Sort#getEqualitySymbol}
302: */
303: public Term createEqualityTerm(Term t1, Term t2) {
304: return createEqualityTerm(new Term[] { t1, t2 });
305:
306: }
307:
308: /** create an EqualityTerm with the correct equality symbol for
309: * the sorts involved, according to {@link Sort#getEqualitySymbol}
310: */
311: public Term createEqualityTerm(Term[] terms) {
312: Equality eq = terms[0].sort().getEqualitySymbol();
313: if (terms[0].op() instanceof SchemaVariable) {
314: eq = terms[1].sort().getEqualitySymbol();
315: }
316: if (eq == null)
317: eq = Op.EQUALS;
318:
319: return createEqualityTerm(eq, terms);
320: }
321:
322: public Term createFunctionTerm(TermSymbol op) {
323: Term result = (Term) cache.get(op);
324: if (result == null) {
325: result = createFunctionTerm(op, NO_SUBTERMS);
326: cache.put(op, result);
327: }
328: return result;
329: }
330:
331: public Term createFunctionTerm(TermSymbol op, Term s1) {
332: final CacheKey key = new CacheKey(op, s1);
333: Term result = (Term) cache.get(key);
334: if (result == null) {
335: result = createFunctionTerm(op, new Term[] { s1 });
336: cache.put(key, result);
337: }
338: return result;
339: }
340:
341: public Term createFunctionTerm(TermSymbol op, Term s1, Term s2) {
342: final CacheKey key = new CacheKey(op, s1, s2);
343: Term result = (Term) cache.get(key);
344: if (result == null) {
345: result = createFunctionTerm(op, new Term[] { s1, s2 });
346: cache.put(key, result);
347: }
348: return result;
349: }
350:
351: /**
352: * creates a term representing a function or predicate
353: * @param op a TermSymbol which is the top level operator of the
354: * function term to be created
355: * @param subTerms array of Term containing the sub terms,
356: * usually the function's or predicate's arguments
357: * @return a term with <code>op</code> as top level symbol and
358: * the terms in <code>subTerms</code> as arguments (direct
359: * subterms)
360: */
361: public Term createFunctionTerm(TermSymbol op, Term[] subTerms) {
362: if (op == null)
363: throw new IllegalArgumentException("null-Operator at"
364: + "TermFactory");
365:
366: return new OpTerm(op, subTerms).checked();
367: }
368:
369: //For OCL simplification
370:
371: /** creates a term representing an OCL expression with a
372: * collection operation as top operator that
373: * takes an OclExpression as argument (not "iterate")
374: * @param op the OCL collection operation
375: * @param varBoundHere the iterator variable
376: * @param subs subs[0] is the collection and subs[1] is the
377: * expression in which the iterator variable is bound
378: */
379:
380: public Term createFunctionWithBoundVarsTerm(TermSymbol op,
381: PairOfTermArrayAndBoundVarsArray subs) {
382: return createFunctionWithBoundVarsTerm(op, subs.getTerms(),
383: subs.getBoundVars());
384: }
385:
386: public Term createFunctionWithBoundVarsTerm(TermSymbol op,
387: Term[] subTerms, ArrayOfQuantifiableVariable[] boundVars) {
388: if (boundVars != null) {
389: return new BoundVarsTerm(op, subTerms, boundVars).checked();
390: } else {
391: return createFunctionTerm(op, subTerms);
392: }
393: }
394:
395: /**
396: * Create an 'if-then-else' term (or formula)
397: */
398: public Term createIfThenElseTerm(Term condF, Term thenT, Term elseT) {
399: return new OpTerm(Op.IF_THEN_ELSE, new Term[] { condF, thenT,
400: elseT });
401: }
402:
403: /**
404: * Create an 'ifEx-then-else' term (or formula)
405: */
406: public Term createIfExThenElseTerm(
407: ArrayOfQuantifiableVariable exVars, Term condF, Term thenT,
408: Term elseT) {
409: return new IfExThenElseTerm(Op.IF_EX_THEN_ELSE, new Term[] {
410: condF, thenT, elseT }, exVars).checked();
411: }
412:
413: /** some methods to handle the equality for formulas (equiv - operator) ... */
414: public Term createJunctorTerm(Equality op, Term t1, Term t2) {
415: return createEqualityTerm(op, new Term[] { t1, t2 });
416: }
417:
418: public Term createJunctorTerm(Equality op, Term[] subTerms) {
419: return createEqualityTerm(op, subTerms);
420: }
421:
422: public Term createJunctorTermAndSimplify(Equality op, Term t1,
423: Term t2) {
424: if (op == Op.EQV) {
425: if (t1.op() == Op.TRUE)
426: return t2;
427: if (t2.op() == Op.TRUE)
428: return t1;
429: if (t1.op() == Op.FALSE)
430: return createJunctorTermAndSimplify(Op.NOT, t2);
431: if (t2.op() == Op.FALSE)
432: return createJunctorTermAndSimplify(Op.NOT, t1);
433: if (t1.equals(t2))
434: return createJunctorTerm(Op.TRUE);
435: }
436: return createEqualityTerm(op, new Term[] { t1, t2 });
437: }
438:
439: public Term createJunctorTerm(Junctor op) {
440: return createJunctorTerm(op, NO_SUBTERMS);
441: }
442:
443: public Term createJunctorTerm(Junctor op, Term t1) {
444: return createJunctorTerm(op, new Term[] { t1 });
445: }
446:
447: public Term createJunctorTerm(Junctor op, Term t1, Term t2) {
448: return createJunctorTerm(op, new Term[] { t1, t2 });
449: }
450:
451: /** creates a JunctorTerm with top operator op, some subterms
452: * @param op Operator at the top of the termstructure that starts
453: * here
454: * @param subTerms an array containing subTerms (an array with length 0 if
455: * there are no more subterms */
456: public Term createJunctorTerm(Junctor op, Term[] subTerms) {
457: if (op == null)
458: throw new IllegalArgumentException("null-Operator at"
459: + "TermFactory");
460: return new OpTerm(op, subTerms).checked();
461: }
462:
463: /** some methods for the creation of junctor terms with automatically performed simplification
464: * like ( b /\ true ) == (b) ...
465: * Currently only the AND, OR, IMP Operators will be simplified (if possible)
466: */
467: public Term createJunctorTermAndSimplify(Junctor op, Term t1) {
468: if (op == Op.NOT) {
469: if (t1.op() == Op.TRUE) {
470: return createJunctorTerm(Op.FALSE);
471: } else if (t1.op() == Op.FALSE) {
472: return createJunctorTerm(Op.TRUE);
473: }
474: }
475: return createJunctorTerm(op, t1);
476: }
477:
478: /** some methods for the creation of junctor terms with automatically performed simplification
479: * like ( b /\ true ) == (b) ...
480: * Currently only the AND, OR, IMP Operators will be simplified (if possible)
481: */
482: public Term createJunctorTermAndSimplify(Junctor op, Term t1,
483: Term t2) {
484: if (op == Op.AND) {
485: // if one of the terms is false the expression is false as a whole
486: if (t1.op() == Op.FALSE || t2.op() == Op.FALSE)
487: return createJunctorTerm(Op.FALSE);
488: // if one of the terms is true skip the subterm.
489: if (t1.op() == Op.TRUE) {
490: return t2;
491: } else if (t2.op() == Op.TRUE) {
492: return t1;
493: } else { // nothing to simplifiy ...
494: return createJunctorTerm(op, t1, t2);
495: }
496: } else if (op == Op.OR) {
497: // if one of the terms is true the expression is true as a whole
498: if (t1.op() == Op.TRUE || t2.op() == Op.TRUE)
499: return createJunctorTerm(Op.TRUE);
500: // if one of the terms is false skip the subterm.
501: if (t1.op() == Op.FALSE) {
502: return t2;
503: } else if (t2.op() == Op.FALSE) {
504: return t1;
505: } else { // nothing to simplifiy ...
506: return createJunctorTerm(op, t1, t2);
507: }
508: } else if (op == Op.IMP) {
509: if (t1.op() == Op.FALSE || t2.op() == Op.TRUE)
510: // then the expression is true as a whole
511: return createJunctorTerm(Op.TRUE);
512: // if t1 is true or t2 is false skip that subterm.
513: if (t1.op() == Op.TRUE) {
514: return t2;
515: } else if (t2.op() == Op.FALSE) {
516: return createJunctorTermAndSimplify(Op.NOT, t1);
517: } else { // nothing to simplifiy ...
518: return createJunctorTerm(op, t1, t2);
519: }
520: } else { // all other Junctors ...
521: return createJunctorTerm(op, t1, t2);
522: }
523: }
524:
525: /** creates a OpTerm with a meta operator as top operator. These
526: * terms are only used in the replacewith areas of taclets. And are
527: * replaced by the SyntacticalReplaceVisitor
528: * @param op Operator at the top of the termstructure that starts
529: * here
530: * @param subTerms an array containing subTerms (an array with length 0 if
531: * there are no more subterms
532: */
533: public Term createMetaTerm(MetaOperator op, Term[] subTerms) {
534: if (op == null)
535: throw new IllegalArgumentException("null-Operator at"
536: + "TermFactory");
537: return new OpTerm(op, subTerms).checked();
538: }
539:
540: public Term createProgramTerm(Operator op, JavaBlock javaBlock,
541: Term subTerm) {
542: return new ProgramTerm(op, javaBlock, subTerm).checked();
543: }
544:
545: public Term createProgramTerm(Operator op, JavaBlock javaBlock,
546: Term[] subTerms) {
547: return new ProgramTerm(op, javaBlock, subTerms).checked();
548: }
549:
550: /**
551: * creates a quantifier term
552: * @param quant the Quantifier (all, exist) which binds the
553: * variables in <code>varsBoundHere</code>
554: * @param varsBoundHere an array of QuantifiableVariable
555: * containing all variables bound by the quantifier
556: * @param subTerm the Term where the variables are bound
557: * @return the quantified term
558: */
559: public Term createQuantifierTerm(Quantifier quant,
560: ArrayOfQuantifiableVariable varsBoundHere, Term subTerm) {
561: if (varsBoundHere.size() <= 1) {
562: return new QuantifierTerm(quant, varsBoundHere, subTerm)
563: .checked();
564: } else {
565: Term qt = subTerm;
566: for (int i = varsBoundHere.size() - 1; i >= 0; i--) {
567: QuantifiableVariable qv = varsBoundHere
568: .getQuantifiableVariable(i);
569: qt = createQuantifierTerm(quant, qv, qt);
570: }
571: return qt;
572: }
573: }
574:
575: /**
576: * creates a quantifier term
577: * @param op Operator representing the
578: * Quantifier (all, exist) of this term
579: * @param varsBoundHere a QuantifiableVariable representing the only bound
580: * variable of this quantifier.
581: */
582: public Term createQuantifierTerm(Quantifier quant,
583: QuantifiableVariable var, Term subTerm) {
584: return createQuantifierTerm(quant,
585: new QuantifiableVariable[] { var }, subTerm);
586: }
587:
588: /**
589: * creates a quantifier term
590: * @param op Operator representing the
591: * Quantifier (all, exist) of this term
592: * @param varsBoundHere an
593: * array of QuantifiableVariable containing all variables bound by the
594: * quantifier
595: */
596: public Term createQuantifierTerm(Quantifier quant,
597: QuantifiableVariable[] varsBoundHere, Term subTerm) {
598: return createQuantifierTerm(quant,
599: new ArrayOfQuantifiableVariable(varsBoundHere), subTerm);
600: }
601:
602: public Term createShadowAttributeTerm(ProgramVariable var,
603: Term term, Term shadownum) {
604: return new OpTerm(ShadowAttributeOp.getShadowAttributeOp(var),
605: new Term[] { term, shadownum }).checked();
606: }
607:
608: public Term createShadowAttributeTerm(SchemaVariable var,
609: Term term, Term shadownum) {
610: return new OpTerm(ShadowAttributeOp
611: .getShadowAttributeOp((IProgramVariable) var),
612: new Term[] { term, shadownum }).checked();
613: }
614:
615: public Term createShadowAttributeTerm(ShadowAttributeOp op,
616: Term term, Term shadownum) {
617: return new OpTerm(op, new Term[] { term, shadownum }).checked();
618: }
619:
620: /** creates a substitution term
621: * @param substVar the QuantifiableVariable to be substituted
622: * @param substTerm the Term that replaces substVar
623: * @param origTerm the Term that is substituted
624: */
625: public Term createSubstitutionTerm(SubstOp op,
626: QuantifiableVariable substVar, Term substTerm, Term origTerm) {
627: return new SubstitutionTerm(op, substVar, new Term[] {
628: substTerm, origTerm }).checked();
629: }
630:
631: /** creates a substitution term
632: * @param op the replacement variable
633: * @param substVar the QuantifiableVariable to be substituted
634: * @param subs an array of Term where subs[0] is the term that
635: * replaces the variable substVar in subs[1]
636: */
637: public Term createSubstitutionTerm(SubstOp op,
638: QuantifiableVariable substVar, Term[] subs) {
639: return new SubstitutionTerm(op, substVar, subs).checked();
640: }
641:
642: /**
643: * helper method for term creation (reduces duplicate code)
644: */
645: private Term createTermWithNoBoundVariables(Operator op,
646: Term[] subTerms, JavaBlock javaBlock) {
647: if (op instanceof Equality) {
648: return createEqualityTerm(subTerms);
649: } else if (op instanceof TermSymbol) {
650: return createFunctionTerm((TermSymbol) op, subTerms);
651: } else if (op instanceof Junctor) {
652: return createJunctorTerm((Junctor) op, subTerms);
653: } else if (op instanceof AnonymousUpdate) {
654: return createAnonymousUpdateTerm((AnonymousUpdate) op,
655: subTerms[0]);
656: } else if (op instanceof Modality) {
657: return createProgramTerm((Modality) op, javaBlock,
658: subTerms[0]);
659: } else if (op instanceof AccessOp) {
660: if (op instanceof ShadowAttributeOp) {
661: return createShadowAttributeTerm(
662: (ShadowAttributeOp) op, subTerms[0],
663: subTerms[1]);
664: } else if (op instanceof AttributeOp) {
665: return createAttributeTerm((AttributeOp) op,
666: subTerms[0]);
667: } else if (op instanceof ArrayOp) {
668: return createArrayTerm((ArrayOp) op, subTerms);
669: } else {
670: Debug.fail("Unknown access operator" + op);
671: return null;
672: }
673: } else if (op instanceof IfThenElse) {
674: return createIfThenElseTerm(subTerms[0], subTerms[1],
675: subTerms[2]);
676: } else if (op instanceof MetaOperator) {
677: return createMetaTerm((MetaOperator) op, subTerms);
678: } else {
679: de.uka.ilkd.key.util.Debug
680: .fail("Should never be"
681: + " reached. Missing case for class", op
682: .getClass());
683: return null;
684: }
685: }
686:
687: public Term createTerm(Operator op, Term[] subTerms,
688: ArrayOfQuantifiableVariable vars, JavaBlock javaBlock) {
689: if (op == null) {
690: throw new IllegalArgumentException(
691: "null-Operator at TermFactory");
692: } else if (op instanceof Quantifier) {
693: return createQuantifierTerm((Quantifier) op, vars,
694: subTerms[0]);
695: } else if (op instanceof QuanUpdateOperator) {
696: final ArrayOfQuantifiableVariable[] bv = new ArrayOfQuantifiableVariable[subTerms.length];
697: final QuanUpdateOperator updOp = (QuanUpdateOperator) op;
698: Arrays.fill(bv, new ArrayOfQuantifiableVariable());
699: bv[0] = vars;
700: return createQuanUpdateTerm(updOp, subTerms, bv);
701: } else if (op instanceof IfExThenElse) {
702: return createIfExThenElseTerm(vars, subTerms[0],
703: subTerms[1], subTerms[2]);
704: } else if (op instanceof SubstOp) {
705: return createSubstitutionTerm((SubstOp) op, vars
706: .getQuantifiableVariable(0), subTerms);
707: } else {
708: return createTermWithNoBoundVariables(op, subTerms,
709: javaBlock);
710: }
711: }
712:
713: public Term createTerm(Operator op, Term[] subTerms,
714: ArrayOfQuantifiableVariable[] bv, JavaBlock javaBlock) {
715: if (op == null) {
716: throw new IllegalArgumentException(
717: "null-Operator at TermFactory");
718: } else if (op instanceof Quantifier) {
719: return createQuantifierTerm((Quantifier) op, bv[0],
720: subTerms[0]);
721: } else if (op instanceof QuanUpdateOperator) {
722: final QuanUpdateOperator updOp = (QuanUpdateOperator) op;
723: if (bv == null) {
724: bv = new ArrayOfQuantifiableVariable[subTerms.length];
725: java.util.Arrays.fill(bv,
726: new ArrayOfQuantifiableVariable());
727: }
728: return createQuanUpdateTerm(updOp, subTerms, bv);
729: } else if (op instanceof IfExThenElse) {
730: final Term[] resTerms = new Term[3];
731: System.arraycopy(subTerms, 0, resTerms, 0, 3);
732: final ArrayOfQuantifiableVariable exVars = BoundVariableTools.DEFAULT
733: .unifyBoundVariables(bv, resTerms, 0, 2);
734: return createIfExThenElseTerm(exVars, resTerms[0],
735: resTerms[1], resTerms[2]);
736: } else if (op instanceof SubstOp) {
737: return createSubstitutionTerm((SubstOp) op, bv[1]
738: .getQuantifiableVariable(0), subTerms);
739: } else if (op instanceof TermSymbol) {
740: // special treatment for OCL operators binding variables
741: return createFunctionWithBoundVarsTerm((TermSymbol) op,
742: subTerms, bv);
743: } else {
744: return createTermWithNoBoundVariables(op, subTerms,
745: javaBlock);
746: }
747: }
748:
749: //
750: // CHANGE these two methods! vars should be something like an
751: // array of arrays!
752: //
753:
754: /**
755: * creates a term using the other methods of this class depending on the
756: * given operator. If the kind of term is known before (without using
757: * if-else cascades on the kind of operator) the other methods in this
758: * factory should be preferred. Depending on the needed parameters for
759: * the terms that should be created some of the parameters of this method
760: * might be ignored.
761: * @param op the top level operator for the new term.
762: * @param subTerms the subterms for the new term. The first n elements
763: * are taken if op is a Junctor or TermSymbol and n is the arity
764: * of op. Only the first entry is taken if op is a Quantifier or
765: * a Diamond. The first (representing the replacing term
766: * for a variable) and the second (representing the term behind the
767: * substitution operator) entries are taken if op is a SubstOp.
768: * @param vars the variables that are bound to a subterm. Not considered
769: * if op is a Junctor, TermSymbol or Diamond. If op is a
770: * SubstOp only the first element is taken and the variable is bound to
771: * the second subterm. In all other cases all variables are taken and
772: * bound to the first subterm.
773: * @param javaBlock representing a java code block. Only taken if op is a
774: * Diamond.
775: * @return the created Term
776: */
777: public Term createTerm(Operator op, Term[] subTerms,
778: QuantifiableVariable[] vars, JavaBlock javaBlock) {
779: return createTerm(op, subTerms,
780: new ArrayOfQuantifiableVariable(vars), javaBlock);
781: }
782:
783: /**
784: * creates an update term like
785: * <code>{pair0}..{pairN}target</code>
786: */
787: public Term createUpdateTerm(ListOfUpdatePair pairs, Term target) {
788: if (pairs.size() > 1) {
789: return createUpdateTerm(pairs.head(), (createUpdateTerm(
790: pairs.tail(), target)));
791: } else {
792: return createUpdateTerm(pairs.head(), target);
793: }
794: }
795:
796: /**
797: * creates the update term <code>{loc:=value}target</code>
798: * @param loc the Term representing the location to be updated
799: * @param value the Term representing the value the location is updated to
800: * @param target the Term on which the update is applied
801: * @return the update term described above
802: */
803: public Term createUpdateTerm(Term loc, Term value, Term target) {
804: return createUpdateTerm(new Term[] { loc },
805: new Term[] { value }, target);
806: }
807:
808: /**
809: * creates an update term
810: * <code>{locs[0]:=values[0],...,locs[n]:=values[n]}target</code>
811: * where <code>n</code> is the length of the location array.
812: * @param locs an array of Term describing the updates locations
813: * @param values an array of Term describing the values to which
814: * the locations are updated
815: * @param target the Term on which the update is applied to
816: * @return the update term as described above
817: */
818: public Term createUpdateTerm(Term[] locs, Term[] values, Term target) {
819: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[locs.length];
820: Arrays.fill(boundVars, new ArrayOfQuantifiableVariable());
821: final Term[] guards = new Term[locs.length];
822: Arrays.fill(guards, createJunctorTerm(Op.TRUE));
823:
824: return createQuanUpdateTerm(boundVars, guards, locs, values,
825: target);
826: }
827:
828: public Term createUpdateTerm(UpdatePair pair, Term target) {
829:
830: final IUpdateOperator op = pair.updateOperator();
831:
832: if (op instanceof AnonymousUpdate) {
833: return createAnonymousUpdateTerm((AnonymousUpdate) op,
834: target);
835: }
836:
837: final Term[] subs = new Term[pair.arity() + 1];
838:
839: for (int i = 0; i < subs.length - 1; i++) {
840: subs[i] = pair.sub(i);
841: }
842:
843: subs[subs.length - 1] = target;
844:
845: if (op instanceof QuanUpdateOperator) {
846: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[pair
847: .arity() + 1];
848: for (int i = 0; i < subs.length - 1; i++)
849: boundVars[i] = pair.varsBoundHere(i);
850: boundVars[subs.length - 1] = new ArrayOfQuantifiableVariable();
851: return createQuanUpdateTerm((QuanUpdateOperator) op, subs,
852: boundVars);
853: } else {
854: Debug.fail("Unknown update operator: " + op);
855: return null; // unreachable
856: }
857: }
858:
859: /**
860: * creates a normalized simultaneous update term
861: *
862: * @param op
863: * the UpdateOperator
864: * @param subs
865: * the subterm of the simultaneous update term to be created
866: * @return the normalized simultaneous update term
867: */
868: public Term createNormalizedQuanUpdateTerm(QuanUpdateOperator op,
869: Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub) {
870: return op.normalize(boundVarsPerSub, subs);
871: }
872:
873: /**
874: * creates a simultaneous update-term
875: *
876: * @param subs
877: * the sub-terms
878: */
879: public Term createQuanUpdateTerm(QuanUpdateOperator op,
880: Term[] subs, ArrayOfQuantifiableVariable[] boundVarsPerSub) {
881: final ArrayOfQuantifiableVariable[] boundVars = op
882: .toBoundVarsPerAssignment(boundVarsPerSub, subs);
883: return new QuanUpdateTerm(op, subs, boundVars).checked();
884: }
885:
886: /**
887: * creates an update term which is not in normalform order (usually usage of
888: * this method is discouraged)
889: *
890: * @return creates an update term which is not in normalform order
891: */
892: public Term createQuanUpdateTermUnordered(QuanUpdateOperator op,
893: Term[] subs, ArrayOfQuantifiableVariable[] boundVars) {
894:
895: return new QuanUpdateTerm(op, subs, boundVars).checked();
896: }
897:
898: /**
899: * creates a normalized update term
900: * <code>{locs[0]:=values[0],...,locs[n]:=values[n]}target</code> where
901: * <code>n</code> is the length of the location array.
902: *
903: * @param locs
904: * an array of Term describing the updates locations
905: * @param values
906: * an array of Term describing the values to which the locations
907: * are updated
908: * @param target
909: * the Term on which the update is applied to
910: * @return the update term as described above
911: */
912: public Term createQuanUpdateTerm(
913: ArrayOfQuantifiableVariable[] boundVars, Term[] guards,
914: Term[] locs, Term[] values, Term target) {
915:
916: return QuanUpdateOperator.normalize(boundVars, guards, locs,
917: values, target);
918: }
919:
920: /**
921: * creates a term consisting of the given variable.
922: * @param v the variable
923: */
924: public Term createVariableTerm(LogicVariable v) {
925: Term varTerm = (Term) cache.get(v);
926: if (varTerm == null) {
927: varTerm = new OpTerm(v, NO_SUBTERMS).checked();
928: cache.put(v, varTerm);
929: }
930: return varTerm;
931: }
932:
933: /**
934: * creates a variable term representing the given programvariable
935: * @param v the ProgramVariable to be represented
936: * @return variable <code>v</code> as term
937: */
938: public Term createVariableTerm(ProgramVariable v) {
939: Term varTerm = (Term) cache.get(v);
940: if (varTerm == null) {
941: varTerm = new OpTerm(v, NO_SUBTERMS).checked();
942: cache.put(v, varTerm);
943: }
944: return varTerm;
945: }
946:
947: /**
948: * creates a term with schemavariable <code>v</code> as top level operator
949: * @param v the SchemaVariable to be represented
950: * @return the term <code>v</code>
951: */
952: public Term createVariableTerm(SchemaVariable v) {
953: Term varTerm = (Term) cache.get(v);
954: if (varTerm == null) {
955: varTerm = new OpTerm(v, NO_SUBTERMS).checked();
956: cache.put(v, varTerm);
957: }
958: return varTerm;
959: }
960:
961: /**
962: * creates an anonymous update applied to the given target term
963: * @param op the AnonymousUpdate operator
964: * @param subs the array of Term containing the
965: * @return
966: */
967: public Term createAnonymousUpdateTerm(AnonymousUpdate op, Term sub) {
968: return new UpdateTerm(op, new Term[] { sub });
969: }
970:
971: /**
972: * creates an anonymous update applied to the given target term
973: * @param name
974: * @param target
975: * @return
976: */
977: public Term createAnonymousUpdateTerm(Name name, Term target) {
978: return createAnonymousUpdateTerm(AnonymousUpdate
979: .getAnonymousOperator(name), target);
980: }
981:
982: /** creates a cast of term with to the given sort */
983: public Term createCastTerm(AbstractSort sort, Term with) {
984: return createFunctionTerm(sort.getCastSymbol(), with);
985: }
986:
987: }
|