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:
018: package de.uka.ilkd.key.parser.ocl;
019:
020: import java.util.HashMap;
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.logic.Name;
025: import de.uka.ilkd.key.logic.Namespace;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermBuilder;
028: import de.uka.ilkd.key.logic.op.*;
029: import de.uka.ilkd.key.logic.sort.*;
030: import de.uka.ilkd.key.proof.OpReplacer;
031: import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory;
032: import de.uka.ilkd.key.util.Debug;
033:
034: /**
035: * ATTENTION: This is not a real factory in the sense of the design
036: * pattern "Factory"!
037: *
038: *
039: * This Class creates all necessary functions (for the
040: * ocl-translation).
041: * It also creates axioms, defining the semantics of the created functions
042: * and puts them into the AxiomCollector.
043: *
044: * Don't forget to reset (resetFactory) the factory for initialization!
045: *
046: */
047: public class FunctionFactory {
048:
049: public static final FunctionFactory INSTANCE = new FunctionFactory();
050:
051: private static final TermBuilder tb = TermBuilder.DF;
052:
053: private static final CreatedAttributeTermFactory createdFactory = CreatedAttributeTermFactory.INSTANCE;
054:
055: private Namespace functionNS;
056:
057: private Services services = null;
058:
059: private int axiomVarCounter = 0;
060: private static final String axiomVarPrefix = "_oclAV";
061: private SetOfLogicVariable createdVars;
062:
063: private Namespace functions;
064:
065: private AxiomCollector axiomCollector;
066:
067: private FunctionFactory() {
068: }
069:
070: /**
071: * initialises the required parameters for the FunctionFactory to work properly
072: * <b>ATTENTION:</b> must be called once before any of the other non-static methods.
073: * Sets all parameters to initial values - any prior changes get lost!
074: *
075: * @param services
076: * @param ac
077: */
078: public void resetFactory(Services services, AxiomCollector ac) {
079: assert services != null;
080: this .services = services;
081: this .functions = services.getNamespaces().functions();
082: this .axiomVarCounter = 0;
083: this .createdVars = SetAsListOfLogicVariable.EMPTY_SET;
084: this .functionNS = new Namespace();
085: this .axiomCollector = ac;
086: }
087:
088: /**
089: *
090: * creates an appropriate function-symbol representing allInstances of the given sort
091: * and the axiom that specifies the meaning of this function-symbol
092: *
093: * C.allInstances()
094: *
095: * @param csort CollectionSort of the function-symbol
096: */
097: public Function createAllInstancesConstant(CollectionSort csort) {
098:
099: // lookup function
100: Function allInst = (Function) functionNS.lookup(new Name(csort
101: .elementSort().name().toString()
102: + "::allInstances"));
103: if (allInst != null) {
104: return allInst;
105: }
106:
107: // create function-Symbol
108: allInst = new NonRigidFunction(new Name(csort.elementSort()
109: .name().toString()
110: + "::allInstances"), csort, new Sort[] {});
111:
112: this .functionNS.add(allInst);
113:
114: // create axiom
115: Function isIn = (Function) this .functions.lookup(new Name(csort
116: .name().toString()
117: + "::includes"));
118: LogicVariable v = createVar(csort.elementSort());
119:
120: Term subTerm = tb.func(isIn, tb.func(allInst), tb.var(v));
121: Term axiom = createdFactory.createCreatedNotNullQuantifierTerm(
122: services, Op.ALL, v, subTerm);
123:
124: axiomCollector.collectAxiom(allInst, axiom);
125:
126: Function instOf = (Function) this .functions.lookup(new Name(
127: csort.elementSort().name().toString() + "::instance"));
128:
129: LogicVariable jObject = createVar(services.getJavaInfo()
130: .getJavaLangObjectAsSort());
131:
132: subTerm = tb.imp(tb.func(isIn, tb.func(allInst), tb.tf()
133: .createCastTerm(((AbstractSort) csort.elementSort()),
134: tb.var(jObject))), tb.equals(tb.func(instOf, tb
135: .var(jObject)), tb.TRUE(services)));
136:
137: axiom = createdFactory.createCreatedNotNullQuantifierTerm(
138: services, Op.ALL, jObject, subTerm);
139:
140: axiomCollector.collectAxiom(allInst, axiom);
141:
142: return allInst;
143: }
144:
145: /**
146: *
147: * creates an appropriate function-symbol representing allInstances of the given sort
148: * and the axiom that specifies the meaning of this function-symbol
149: *
150: * @param sort Element-Sort of the function-symbol
151: */
152: public Function createAllInstancesConstant(Sort sort) {
153: return createAllInstancesConstant(getSetSort(sort));
154: }
155:
156: /**
157: *
158: * creates an appropriate function-symbol representing select for the given term
159: * and adds the axioms that specifie the meaning of this function-symbol to the
160: * local axiom-list
161: *
162: * c->select(e | b)
163: *
164: * @param selectVar Translation of e
165: * @param selectTerm Translation of b
166: * @throws OCLTranslationError
167: */
168: public Function createSelectFunction(LogicVariable selectVar,
169: Term selectTerm, int collectionType)
170: throws OCLTranslationError {
171: CollectionSort csort = getCollectionSort(selectVar.sort(),
172: collectionType);
173: assert csort != null;
174:
175: // lookup function
176: Function f = (Function) functionNS.lookup(new Name(csort
177: .elementSort().toString()
178: + "::select[" + selectTerm.toString() + "]"));
179: // Function f = (Function) functionNS.lookup(new Name(csort.elementSort().toString()+"::select"));
180: if (f != null) {
181: return f;
182: }
183:
184: SetOfQuantifiableVariable vars = selectTerm.freeVars();
185: // selectVar is NOT free in this sense.
186: vars = vars.remove(selectVar);
187:
188: Sort[] sorts = new Sort[vars.size() + 1];
189: Term[] varTerms1 = new Term[vars.size() + 1];
190: Term[] varTerms2 = new Term[vars.size() + 1];
191: LogicVariable[] qvars1 = new LogicVariable[vars.size()];
192: LogicVariable[] qvars2 = new LogicVariable[vars.size() + 2];
193:
194: for (int i = 0; i < vars.size(); i++) {
195: sorts[i + 1] = vars.toArray()[i].sort();
196: varTerms1[i + 1] = tb
197: .var((LogicVariable) vars.toArray()[i]);
198: varTerms2[i + 1] = tb
199: .var((LogicVariable) vars.toArray()[i]);
200: qvars1[i] = (LogicVariable) vars.toArray()[i];
201: qvars2[i + 2] = (LogicVariable) vars.toArray()[i];
202: }
203:
204: sorts[0] = csort;
205:
206: //create new function-symbol
207: Function selectE = new RigidFunction(new Name(csort
208: .elementSort().toString()
209: + "::select[" + selectTerm.toString() + "]"),
210: // Function selectE = new RigidFunction( new Name(csort.elementSort().toString()+"::select"),
211: csort, sorts);
212:
213: functionNS.add(selectE);
214:
215: // create axioms
216: Function emptyCollection = getEmptyCollection(csort
217: .elementSort(), collectionType);
218:
219: // axiom 1
220: varTerms1[0] = tb.func(emptyCollection);
221: Term axiom1 = tb.equals(tb.func(selectE, varTerms1), tb
222: .func(emptyCollection));
223:
224: if (qvars1.length > 0) {
225: axiom1 = createdFactory.createCreatedNotNullQuantifierTerm(
226: services, Op.ALL, qvars1, axiom1);
227: }
228:
229: axiomCollector.collectAxiom(selectE, axiom1);
230:
231: // axiom 2
232: qvars2[0] = createVar(csort);
233: qvars2[1] = createVar(csort.elementSort());
234:
235: varTerms1[0] = including(tb.var(qvars2[0]), tb.var(qvars2[1]));
236:
237: varTerms2[0] = tb.var(qvars2[0]);
238:
239: Term axiom2 = tb.imp(replaceVar(selectVar, qvars2[1],
240: selectTerm), tb.equals(tb.func(selectE, varTerms1),
241: including(tb.func(selectE, varTerms2), tb
242: .var(qvars2[1]))));
243:
244: axiom2 = createdFactory.createCreatedNotNullQuantifierTerm(
245: services, Op.ALL, qvars2, axiom2);
246:
247: axiomCollector.collectAxiom(selectE, axiom2);
248:
249: // axiom 3
250: Term axiom3 = tb.imp(tb.not(replaceVar(selectVar, qvars2[1],
251: selectTerm)), tb.equals(tb.func(selectE, varTerms1), tb
252: .func(selectE, varTerms2)));
253:
254: axiom3 = createdFactory.createCreatedNotNullQuantifierTerm(
255: services, Op.ALL, qvars2, axiom3);
256:
257: axiomCollector.collectAxiom(selectE, axiom3);
258:
259: return selectE;
260: }
261:
262: /**
263: *
264: * creates an appropriate function-symbol representing reject for the given term
265: * and adds the axioms that specifie the meaning of this function-symbol to the
266: * local axiom-list
267: *
268: * c->reject(e | b)
269: *
270: * @param rejectVar Translation of e
271: * @param rejectTerm Translation of b
272: * @throws OCLTranslationError
273: */
274: public Function createRejectFunction(LogicVariable rejectVar,
275: Term rejectTerm, int collectionType)
276: throws OCLTranslationError {
277: return createSelectFunction(rejectVar, tb.not(rejectTerm),
278: collectionType);
279: }
280:
281: /**
282: *
283: * creates an appropriate function-symbol representing collect for the given term
284: * and adds the axioms that specifie the meaning of this function-symbol to the
285: * local axiom-list
286: *
287: * c->collect(e | b)
288: *
289: * @param collectVar Translation of e
290: * @param selectTerm Translation of b
291: * @throws OCLTranslationError
292: */
293: public Function createCollectFunction(LogicVariable collectVar,
294: Term collectTerm, int collectionType)
295: throws OCLTranslationError {
296:
297: CollectionSort csort = getCollectionSort(collectVar.sort(),
298: collectionType);
299:
300: CollectionSort resSort = (collectionType == OCLCollection.OCL_SET) ? getBagSort(collectTerm
301: .sort())
302: : getCollectionSort(collectTerm.sort(), collectionType);
303:
304: // lookup function
305: Function f = (Function) functionNS.lookup(new Name(csort
306: .elementSort().toString()
307: + "::collect"));
308: if (f != null) {
309: return f;
310: }
311:
312: SetOfQuantifiableVariable vars = collectTerm.freeVars();
313:
314: // collectVar is NOT free in collectTerm in this sense
315: vars = vars.remove(collectVar);
316:
317: Sort[] signature = new Sort[vars.size() + 1];
318: Term[] varTerms1 = new Term[vars.size() + 1];
319: Term[] varTerms2 = new Term[vars.size() + 1];
320: LogicVariable[] qvars1 = new LogicVariable[vars.size()];
321: LogicVariable[] qvars2 = new LogicVariable[vars.size() + 2];
322:
323: for (int i = 0; i < vars.size(); i++) {
324: signature[i + 1] = vars.toArray()[i].sort();
325: varTerms1[i + 1] = tb
326: .var((LogicVariable) vars.toArray()[i]);
327: varTerms2[i + 1] = tb
328: .var((LogicVariable) vars.toArray()[i]);
329: qvars1[i] = (LogicVariable) vars.toArray()[i];
330: qvars2[i + 2] = (LogicVariable) vars.toArray()[i];
331: }
332:
333: signature[0] = csort;
334:
335: //create new function-symbol
336: Function collectE = new RigidFunction(new Name(csort
337: .elementSort().toString()
338: + "::collect"), resSort, signature);
339:
340: functionNS.add(collectE);
341:
342: // create axioms
343: // axiom 1
344: Function emptyCollectionT = getEmptyCollection(csort
345: .elementSort(), collectionType);
346: assert emptyCollectionT != null;
347:
348: Function emptyCollectionS = (collectionType == OCLCollection.OCL_SET) ? getEmptyBag(collectTerm
349: .sort())
350: : getEmptyCollection(collectTerm.sort(), collectionType);
351: assert emptyCollectionS != null;
352:
353: varTerms1[0] = tb.func(emptyCollectionT);
354: Term axiom1 = tb.equals(tb.func(collectE, varTerms1), tb
355: .func(emptyCollectionS));
356:
357: if (qvars1.length > 0) {
358: axiom1 = createdFactory.createCreatedNotNullQuantifierTerm(
359: services, Op.ALL, qvars1, axiom1);
360: }
361:
362: axiomCollector.collectAxiom(collectE, axiom1);
363:
364: System.out.println("Creating axiom2");
365: // axiom 2
366: qvars2[0] = createVar(csort);
367: qvars2[1] = createVar(csort.elementSort());
368:
369: varTerms1[0] = including(tb.var(qvars2[0]), tb.var(qvars2[1]));
370:
371: varTerms2[0] = (collectionType == OCLCollection.OCL_SET) ? excluding(
372: tb.var(qvars2[0]), tb.var(qvars2[1]))
373: : tb.var(qvars2[0]);
374:
375: Term eq2 = null;
376:
377: if (collectTerm.sort() instanceof AbstractNonCollectionSort) {
378: eq2 = including(tb.func(collectE, varTerms2), replaceVar(
379: collectVar, qvars2[1], collectTerm));
380: } else if (collectTerm.sort() instanceof AbstractCollectionSort) {
381: System.out.println("Building union");
382: eq2 = union(tb.func(collectE, varTerms2), replaceVar(
383: collectVar, qvars2[1], collectTerm));
384: System.out.println("union-term: " + eq2);
385: } else {
386: raiseError("wrong sort in collectTerm!");
387: }
388:
389: System.out.println("axiom2");
390: Term axiom2 = tb.equals(tb.func(collectE, varTerms1), eq2);
391:
392: axiom2 = createdFactory.createCreatedNotNullQuantifierTerm(
393: services, Op.ALL, qvars2, axiom2);
394:
395: axiomCollector.collectAxiom(collectE, axiom2);
396:
397: System.out.println("Returning from Collect-Creation");
398: return collectE;
399: }
400:
401: private void raiseError(String msg) throws OCLTranslationError {
402: throw new OCLTranslationError(
403: "Error while generating Functions: " + msg);
404: }
405:
406: private Term replaceVar(LogicVariable lv1, LogicVariable lv2,
407: Term term) {
408: Map map = new HashMap();
409: map.put(lv1, lv2);
410: OpReplacer or = new OpReplacer(map);
411: return or.replace(term);
412: }
413:
414: /**
415: *
416: * @return Conjunction of subTerms
417: */
418: public static Term buildAddTerm(Term[] subTerms) {
419: Term result = tb.tt();
420: for (int i = 0; i < subTerms.length; i++) {
421: result = tb.and(result, subTerms[i]);
422: }
423:
424: return result;
425: }
426:
427: /**
428: * Returns the corresponding CollectionSort of the given sort
429: * @param sort
430: * @param collectionType the concrete collection type according to OCLCollection
431: * @return <b>null</b> if no AbstractNonCollectionSort is given,
432: * otherwise the corresponding CollectionSort is returned.
433: */
434: public static CollectionSort getCollectionSort(Sort sort,
435: int collectionType) {
436: CollectionSort ssort = null;
437:
438: if (sort instanceof AbstractNonCollectionSort) {
439: switch (collectionType) {
440: case OCLCollection.OCL_SET:
441: ssort = ((AbstractNonCollectionSort) sort).getSetSort();
442: break;
443: case OCLCollection.OCL_BAG:
444: ssort = ((AbstractNonCollectionSort) sort).getBagSort();
445: break;
446: case OCLCollection.OCL_SEQUENCE:
447: ssort = ((AbstractNonCollectionSort) sort)
448: .getSequenceSort();
449: break;
450: }
451: } else if (sort instanceof AbstractCollectionSort) {
452: switch (collectionType) {
453: case OCLCollection.OCL_SET:
454: ssort = ((AbstractNonCollectionSort) ((AbstractCollectionSort) sort)
455: .elementSort()).getSetSort();
456: break;
457: case OCLCollection.OCL_BAG:
458: ssort = ((AbstractNonCollectionSort) ((AbstractCollectionSort) sort)
459: .elementSort()).getBagSort();
460: break;
461: case OCLCollection.OCL_SEQUENCE:
462: ssort = ((AbstractNonCollectionSort) ((AbstractCollectionSort) sort)
463: .elementSort()).getSequenceSort();
464: break;
465: }
466: }
467:
468: return ssort;
469: }
470:
471: public static CollectionSort getSetSort(Sort sort) {
472: return getCollectionSort(sort, OCLCollection.OCL_SET);
473: }
474:
475: public static CollectionSort getBagSort(Sort sort) {
476: return getCollectionSort(sort, OCLCollection.OCL_BAG);
477: }
478:
479: public static CollectionSort getSequenceSort(Sort sort) {
480: return getCollectionSort(sort, OCLCollection.OCL_SEQUENCE);
481: }
482:
483: /**
484: * Returns the function-symbol representing emptyCollection of the given type and sort
485: *
486: * @param elementsort of the collection
487: * @return function-symbol representing emptyCollection
488: */
489: public Function getEmptyCollection(Sort sort, int collectionType) {
490:
491: CollectionSort ssort = getCollectionSort(sort, collectionType);
492:
493: String functionName = null;
494:
495: switch (collectionType) {
496: case OCLCollection.OCL_SET:
497: functionName = "::emptySet";
498: break;
499: case OCLCollection.OCL_BAG:
500: functionName = "::emptyBag";
501: break;
502: case OCLCollection.OCL_SEQUENCE:
503: functionName = "::emptySequence";
504: break;
505: }
506:
507: Function f = (Function) this .functions.lookup(new Name(ssort
508: .name().toString()
509: + functionName));
510:
511: return f;
512: }
513:
514: /**
515: * Returns the function-symbol representing emptySet of the given sort
516: *
517: * @param sort may be the elementsort or the collectionsort
518: * @return function-symbol representing emptySet
519: */
520: public Function getEmptySet(Sort sort) {
521: return getEmptyCollection(sort, OCLCollection.OCL_SET);
522: }
523:
524: /**
525: * Returns the function-symbol representing emptyBag of the given sort
526: *
527: * @param sort may be the elementsort or the collectionsort
528: * @return function-symbol representing emptyBag
529: */
530: public Function getEmptyBag(Sort sort) {
531: return getEmptyCollection(sort, OCLCollection.OCL_BAG);
532: }
533:
534: /**
535: * Returns the function-symbol representing emptySequence of the given sort
536: *
537: * @param sort may be the elementsort or the collectionsort
538: * @return function-symbol representing emptySequence
539: */
540: public Function getEmptySequence(Sort sort) {
541: return getEmptyCollection(sort, OCLCollection.OCL_SEQUENCE);
542: }
543:
544: public Term including(Term setSymbol, Term element)
545: throws OCLTranslationError {
546:
547: if (!(setSymbol.sort() instanceof AbstractCollectionSort)
548: || !(element.sort()
549: .extendsTrans(((AbstractCollectionSort) setSymbol
550: .sort()).elementSort()))) {
551:
552: raiseError("including failed since the terms used have wrong sorts\n"
553: + "Sorts were: "
554: + setSymbol.sort()
555: + " "
556: + element.sort());
557: }
558:
559: Function inc = (Function) this .functions.lookup(new Name(
560: setSymbol.sort().name().toString() + "::including"));
561:
562: return tb.func(inc, setSymbol, element);
563: }
564:
565: public Term excluding(Term setSymbol, Term element)
566: throws OCLTranslationError {
567:
568: if (!(setSymbol.sort() instanceof AbstractCollectionSort)
569: || !(element.sort()
570: .extendsTrans(((AbstractCollectionSort) setSymbol
571: .sort()).elementSort()))) {
572:
573: raiseError("including failed since the terms used have wrong sorts\n"
574: + "Sorts were: "
575: + setSymbol.sort()
576: + " "
577: + element.sort());
578: }
579:
580: Function inc = (Function) this .functions.lookup(new Name(
581: setSymbol.sort().name().toString() + "::excluding"));
582:
583: return tb.func(inc, setSymbol, element);
584: }
585:
586: public Term union(Term t1, Term t2) throws OCLTranslationError {
587:
588: if (!(t1.sort() instanceof AbstractCollectionSort)
589: || !(t2.sort() instanceof AbstractCollectionSort)) {
590: raiseError("no collection-sorts in union" + "Sorts were: "
591: + t1.sort() + " " + t2.sort());
592: }
593:
594: Sort s = null;
595: if (((AbstractCollectionSort) t1.sort()).elementSort()
596: .extendsTrans(
597: ((AbstractCollectionSort) t2.sort())
598: .elementSort())) {
599: s = t2.sort();
600: } else if (((AbstractCollectionSort) t2.sort()).elementSort()
601: .extendsTrans(
602: ((AbstractCollectionSort) t1.sort())
603: .elementSort())) {
604: s = t1.sort();
605: } else {
606: raiseError("union failed since the terms used have diffrent sorts\n"
607: + "Sorts were: " + t1.sort() + " " + t2.sort());
608: }
609: assert s != null;
610:
611: final Function union = (Function) this .functions
612: .lookup(new Name(s.name().toString() + "::union"));
613:
614: return tb.func(union, t1, t2);
615: }
616:
617: public Term simplify(Term t) {
618:
619: if (t.op().name().toString().indexOf("::union") != -1) {
620: if (t.sub(1).op().name().toString().indexOf("::including") != -1) {
621: if (t.sub(1).sub(0).op().name().toString().indexOf(
622: "::emptySet") != -1) {
623: t = tb.func((Function) t.sub(1).op(), t.sub(0), t
624: .sub(1).sub(1));
625: }
626: } else if (t.sub(0).op().name().toString().indexOf(
627: "::including") != -1) {
628: if (t.sub(0).sub(0).op().name().toString().indexOf(
629: "::emptySet") != -1) {
630: t = tb.func((Function) t.sub(0).op(), t.sub(1), t
631: .sub(0).sub(1));
632: }
633: }
634: }
635:
636: return t;
637: }
638:
639: public Term createRangedSet(Term lowerBound, Term upperBound,
640: Function leq) throws OCLTranslationError {
641:
642: if (lowerBound.sort() != upperBound.sort()) {
643: raiseError("Set{" + lowerBound.toString() + ".."
644: + upperBound.toString() + "} : sorts don't match");
645: }
646:
647: SetOfQuantifiableVariable vars = lowerBound.freeVars().union(
648: upperBound.freeVars());
649:
650: Sort[] sorts = new Sort[vars.size()];
651: Term[] varTerms = new Term[vars.size()];
652: LogicVariable[] qvars = new LogicVariable[vars.size() + 1];
653:
654: for (int i = 0; i < vars.size(); i++) {
655: sorts[i] = vars.toArray()[i].sort();
656: varTerms[i] = tb.var((LogicVariable) vars.toArray()[i]);
657: qvars[i + 1] = (LogicVariable) vars.toArray()[i];
658: }
659:
660: //create new function
661: Function setE = new RigidFunction(new Name("set::["
662: + lowerBound.toString() + ".." + upperBound.toString()
663: + "]"), getSetSort(lowerBound.sort()), sorts);
664:
665: functionNS.add(setE);
666:
667: //create axiom
668: LogicVariable v = createVar(lowerBound.sort());
669: qvars[0] = v;
670:
671: Term axiom1 = createRangedCollectionAxiom1(lowerBound,
672: upperBound, setE, leq, varTerms, qvars);
673:
674: axiomCollector.collectAxiom(setE, axiom1);
675:
676: return tb.func(setE, varTerms);
677: }
678:
679: public Term createRangedBag(Term lowerBound, Term upperBound,
680: Function leq) throws OCLTranslationError {
681:
682: if (lowerBound.sort() != upperBound.sort()) {
683: raiseError("Bag{" + lowerBound.toString() + ".."
684: + upperBound.toString() + "} : sorts don't match");
685: }
686:
687: SetOfQuantifiableVariable vars = lowerBound.freeVars().union(
688: upperBound.freeVars());
689:
690: Sort[] sorts = new Sort[vars.size()];
691: Term[] varTerms = new Term[vars.size()];
692: LogicVariable[] qvars = new LogicVariable[vars.size() + 1];
693:
694: for (int i = 0; i < vars.size(); i++) {
695: sorts[i] = vars.toArray()[i].sort();
696: varTerms[i] = tb.var((LogicVariable) vars.toArray()[i]);
697: qvars[i + 1] = (LogicVariable) vars.toArray()[i];
698: }
699:
700: //create new function
701: Function bagE = new RigidFunction(new Name("bag::["
702: + lowerBound.toString() + ".." + upperBound.toString()
703: + "]"), getBagSort(lowerBound.sort()), sorts);
704:
705: functionNS.add(bagE);
706:
707: //create axiom 1
708: LogicVariable v = createVar(lowerBound.sort());
709: qvars[0] = v;
710:
711: Term axiom1 = createRangedCollectionAxiom1(lowerBound,
712: upperBound, bagE, leq, varTerms, qvars);
713:
714: axiomCollector.collectAxiom(bagE, axiom1);
715:
716: // create axiom 2
717: Term axiom2 = createRangedCollectionAxiom2(bagE, leq, varTerms,
718: qvars);
719:
720: axiomCollector.collectAxiom(bagE, axiom2);
721:
722: return tb.func(bagE, varTerms);
723: }
724:
725: public Term createRangedSequence(Term lowerBound, Term upperBound,
726: Function leq) throws OCLTranslationError {
727:
728: if (lowerBound.sort() != upperBound.sort()) {
729: raiseError("Sequence{" + lowerBound.toString() + ".."
730: + upperBound.toString() + "} : sorts don't match");
731: }
732:
733: SetOfQuantifiableVariable vars = lowerBound.freeVars().union(
734: upperBound.freeVars());
735:
736: Sort[] sorts = new Sort[vars.size()];
737: Term[] varTerms = new Term[vars.size()];
738: LogicVariable[] qvars = new LogicVariable[vars.size() + 1];
739: LogicVariable[] qvars2 = new LogicVariable[vars.size() + 2];
740:
741: for (int i = 0; i < vars.size(); i++) {
742: sorts[i] = vars.toArray()[i].sort();
743: varTerms[i] = tb.var((LogicVariable) vars.toArray()[i]);
744: qvars[i + 1] = (LogicVariable) vars.toArray()[i];
745: qvars2[i + 2] = (LogicVariable) vars.toArray()[i];
746: }
747:
748: //create new function
749: Function sequenceE = new RigidFunction(new Name("sequence::["
750: + lowerBound.toString() + ".." + upperBound.toString()
751: + "]"), getSequenceSort(lowerBound.sort()), sorts);
752:
753: functionNS.add(sequenceE);
754:
755: LogicVariable v = createVar(lowerBound.sort());
756: qvars[0] = v;
757:
758: Term axiom1 = createRangedCollectionAxiom1(lowerBound,
759: upperBound, sequenceE, leq, varTerms, qvars);
760:
761: axiomCollector.collectAxiom(sequenceE, axiom1);
762:
763: Term axiom2 = createRangedCollectionAxiom2(sequenceE, leq,
764: varTerms, qvars);
765:
766: axiomCollector.collectAxiom(sequenceE, axiom2);
767:
768: // create axiom 3
769:
770: qvars2[0] = v;
771: qvars2[1] = createVar(lowerBound.sort());
772:
773: Term axiom3 = createRangedCollectionAxiom3(sequenceE, leq,
774: varTerms, qvars2);
775:
776: axiomCollector.collectAxiom(sequenceE, axiom3);
777:
778: return tb.func(sequenceE, varTerms);
779: }
780:
781: private Term createRangedCollectionAxiom1(Term lowerBound,
782: Term upperBound, Function funcSymbol, Function leq,
783: Term[] varTerms, LogicVariable[] qvars) {
784:
785: Function isIn = (Function) this .functions.lookup(new Name(
786: funcSymbol.sort().name() + "::includes"));
787:
788: Term vterm = tb.var(qvars[0]);
789:
790: Term subTerm = tb.and(tb.func(leq, new Term[] { lowerBound,
791: vterm }), tb
792: .func(leq, new Term[] { vterm, upperBound }));
793:
794: subTerm = tb.equals(tb.func(isIn,
795: tb.func(funcSymbol, varTerms), vterm), subTerm);
796:
797: Term axiom = createdFactory.createCreatedNotNullQuantifierTerm(
798: services, Op.ALL, qvars, subTerm);
799:
800: return axiom;
801:
802: }
803:
804: private Term createRangedCollectionAxiom2(Function funcSymbol,
805: Function leq, Term[] varTerms, LogicVariable[] qvars) {
806:
807: Function count = (Function) this .functions.lookup(new Name(
808: funcSymbol.sort().name() + "::count"));
809:
810: Term subTerm = tb.func(leq, tb.func(count, new Term[] {
811: tb.func(funcSymbol, varTerms), tb.var(qvars[0]) }), tb
812: .zTerm(services, "1"));
813:
814: Term axiom2 = createdFactory
815: .createCreatedNotNullQuantifierTerm(services, Op.ALL,
816: qvars, subTerm);
817:
818: return axiom2;
819:
820: }
821:
822: private Term createRangedCollectionAxiom3(Function funcSymbol,
823: Function leq, Term[] varTerms, LogicVariable[] qvars) {
824:
825: Function at = (Function) this .functions.lookup(new Name(
826: funcSymbol.sort().name() + "::at"));
827:
828: Term subTerm = tb.imp(tb.func(leq, tb.var(qvars[0]), tb
829: .var(qvars[1])), tb.func(leq, tb.func(at, tb.func(
830: funcSymbol, varTerms), tb.var(qvars[0])), tb.func(at,
831: tb.func(funcSymbol, varTerms), tb.var(qvars[1]))));
832:
833: Term axiom3 = createdFactory
834: .createCreatedNotNullQuantifierTerm(services, Op.ALL,
835: qvars, subTerm);
836:
837: return axiom3;
838:
839: }
840:
841: private LogicVariable createVar(Sort sort) {
842: LogicVariable v = new LogicVariable(new Name(axiomVarPrefix
843: + axiomVarCounter++), sort);
844: createdVars = createdVars.add(v);
845: return v;
846: }
847:
848: public Term unionAndSimplify(Term t1, Term t2)
849: throws OCLTranslationError {
850:
851: Term res = union(t1, t2);
852: Term oldRes;
853: do {
854: oldRes = res;
855: res = simplify(res);
856: } while (!oldRes.equals(res));
857:
858: return res;
859: }
860:
861: /**
862: * returns the namespace which holds all the created functions
863: * @return
864: */
865: public Namespace getFunctions() {
866: return this .functionNS;
867: }
868:
869: /**
870: * returns the list of created variables which are used in the axioms
871: * @return
872: */
873: public SetOfLogicVariable getCreatedVars() {
874: return this.createdVars;
875: }
876:
877: }
|