Source Code Cross Referenced for TermFactory.java in  » Testing » KeY » de » uka » ilkd » key » logic » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.logic 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.