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 junit.framework.TestCase;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.logic.sort.ArraySort;
019: import de.uka.ilkd.key.logic.sort.ArraySortImpl;
020: import de.uka.ilkd.key.logic.sort.ClassInstanceSortImpl;
021: import de.uka.ilkd.key.logic.sort.Sort;
022: import de.uka.ilkd.key.proof.*;
023: import de.uka.ilkd.key.rule.TacletForTests;
024: import de.uka.ilkd.key.rule.UpdateSimplifier;
025: import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPairImpl;
026: import de.uka.ilkd.key.rule.updatesimplifier.Update;
027:
028: /**
029: *
030: */
031: public class TestUpdateFactory extends TestCase {
032:
033: private Proof proof;
034:
035: private Namespace variables = new Namespace();
036: private Namespace functions = new Namespace();
037: private Namespace sorts = new Namespace();
038:
039: private ProgramVariable[] pv;
040:
041: private TermFactory tf = TermFactory.DEFAULT;
042:
043: private Sort testSort0;
044: private Sort testSort1;
045: private Sort testSort2;
046: private Sort cloneable;
047: private Sort serializable;
048: private Sort integerSort;
049:
050: // t : testSort1
051: private Term t;
052: // i : testSort1
053: private Term i;
054: // o : testSort1
055: private Term o;
056: // u : testSort1
057: private Term u;
058: // o.a
059: private Term oa;
060: // u.a
061: private Term ua;
062:
063: private Term phi;
064: private Term psi;
065:
066: // arrays
067: private ArraySort arraySort1;
068: private ArraySort arraySort2;
069:
070: private Term a;
071: private Term b;
072:
073: private NonRigidFunction nonRigidTargetOp;
074: private Term nonRigidTarget;
075:
076: // var : variable of integerSort
077: private QuantifiableVariable var;
078: private Term varT;
079:
080: // var2 : variable of integerSort
081: private QuantifiableVariable var2;
082: private Term var2T;
083:
084: // f: int * int -> int
085: private Function f;
086:
087: // f(var, var2)
088: private Term fvarvar2;
089:
090: // a[var] : array of testSort 1
091: private Term avar;
092: // b[var] : array of testSort 1
093: private Term bvar;
094: // a[var2] : array of testSort 1
095: private Term avar2;
096: // a[f(var,var2)] : array of testSort 1
097: private Term avarvar2;
098: // b[var2] : array of testSort 1
099: private Term bvar2;
100:
101: private Function woRelation;
102:
103: private UpdateSimplifier simplifier;
104:
105: public TestUpdateFactory(String s) {
106: super (s);
107: }
108:
109: public void setUp() {
110: testSort0 = new ClassInstanceSortImpl(new Name("testSort0"),
111: false);
112: testSort1 = new ClassInstanceSortImpl(new Name("testSort1"),
113: testSort0, false);
114: testSort2 = new ClassInstanceSortImpl(new Name("testSort2"),
115: testSort0, false);
116: cloneable = new ClassInstanceSortImpl(new Name("cloneable"),
117: testSort1, false);
118:
119: serializable = new ClassInstanceSortImpl(new Name(
120: "serializable"), testSort1, false);
121:
122: KeYJavaType kjt = new KeYJavaType(new ClassDeclaration(
123: new ProgramElementName("Object"),
124: new ProgramElementName("java.lang.Object")), testSort1);
125: sorts.add(testSort0);
126: sorts.add(testSort1);
127: sorts.add(testSort2);
128: sorts.add(cloneable);
129: sorts.add(serializable);
130:
131: pv = new ProgramVariable[7];
132: for (int i = 0; i < pv.length; i++) {
133: ProgramElementName name;
134: switch (i) {
135: case 1:
136: name = new ProgramElementName("t");
137: break;
138: case 2:
139: name = new ProgramElementName("i");
140: break;
141: case 3:
142: name = new ProgramElementName("o");
143: break;
144: case 4:
145: name = new ProgramElementName("u");
146: break;
147: case 5:
148: name = new ProgramElementName("a");
149: break;
150: default:
151: name = new ProgramElementName("pv" + i);
152: break;
153: }
154: pv[i] = new LocationVariable(name, kjt);
155: variables.add(pv[i]);
156: }
157:
158: // just initialize the parser
159: parseTerm("{t:=i} o");
160: // for the systematic tests
161:
162: t = tf.createFunctionTerm(pv[1]);
163: i = tf.createFunctionTerm(pv[2]);
164: o = tf.createFunctionTerm(pv[3]);
165: u = tf.createFunctionTerm(pv[4]);
166:
167: oa = tf.createAttributeTerm(pv[5], o);
168: ua = tf.createAttributeTerm(pv[5], u);
169:
170: arraySort1 = ArraySortImpl.getArraySort(testSort1, testSort0,
171: cloneable, serializable);
172: arraySort2 = ArraySortImpl.getArraySort(testSort2, testSort0,
173: cloneable, serializable);
174:
175: ProgramVariable a_var = new LocationVariable(
176: new ProgramElementName("_a"), arraySort1);
177: ProgramVariable b_var = new LocationVariable(
178: new ProgramElementName("_b"), arraySort1);
179: ProgramVariable c_var = new LocationVariable(
180: new ProgramElementName("_c"), arraySort2);
181:
182: functions.add(a_var);
183: functions.add(b_var);
184: functions.add(c_var);
185:
186: a = tf.createFunctionTerm(a_var);
187: b = tf.createFunctionTerm(b_var);
188:
189: integerSort = TacletForTests.services().getTypeConverter()
190: .getIntegerLDT().targetSort();
191: sorts.add(integerSort);
192:
193: nonRigidTargetOp = new NonRigidFunction(new Name("target"),
194: Sort.FORMULA, new Sort[0]);
195: functions.add(nonRigidTargetOp);
196: nonRigidTarget = tf.createFunctionTerm(nonRigidTargetOp);
197:
198: Function phiSym = new RigidFunction(new Name("phi"),
199: Sort.FORMULA, new Sort[0]);
200: functions.add(phiSym);
201: phi = tf.createFunctionTerm(phiSym);
202:
203: Function psiSym = new RigidFunction(new Name("psi"),
204: Sort.FORMULA, new Sort[0]);
205: functions.add(psiSym);
206: psi = tf.createFunctionTerm(psiSym);
207:
208: f = new RigidFunction(new Name("f"), integerSort, new Sort[] {
209: integerSort, integerSort });
210: functions.add(f);
211:
212: var = new LogicVariable(new Name("var"), integerSort);
213: varT = tf.createVariableTerm((LogicVariable) var);
214:
215: avar = tf
216: .createArrayTerm(ArrayOp.getArrayOp(a.sort()), a, varT);
217: bvar = tf
218: .createArrayTerm(ArrayOp.getArrayOp(b.sort()), b, varT);
219:
220: var2 = new LogicVariable(new Name("var2"), integerSort);
221: var2T = tf.createVariableTerm((LogicVariable) var2);
222:
223: avar2 = tf.createArrayTerm(ArrayOp.getArrayOp(a.sort()), a,
224: var2T);
225: bvar2 = tf.createArrayTerm(ArrayOp.getArrayOp(b.sort()), b,
226: var2T);
227:
228: fvarvar2 = tf.createFunctionTerm(f, varT, var2T);
229: avarvar2 = tf.createArrayTerm(ArrayOp.getArrayOp(a.sort()), a,
230: fvarvar2);
231:
232: woRelation = new RigidFunction(new Name("quanUpdateLeqInt"),
233: Sort.FORMULA, new Sort[] { integerSort, integerSort });
234: functions.add(woRelation);
235:
236: proof = new Proof(TacletForTests.services());
237: proof.setSimplifier(new UpdateSimplifier());
238:
239: Goal g = new Goal(
240: new Node(proof, Sequent.EMPTY_SEQUENT),
241: new RuleAppIndex(new TacletAppIndex(new TacletIndex()),
242: new BuiltInRuleAppIndex(new BuiltInRuleIndex())));
243: proof.setRoot(g.node());
244: proof.add(g);
245:
246: proof.setNamespaces(new NamespaceSet(new Namespace(),
247: functions, sorts, new Namespace(), new Namespace(),
248: variables));
249: simplifier = proof.getSettings()
250: .getSimultaneousUpdateSimplifierSettings()
251: .getSimplifier();
252: }
253:
254: public void tearDown() {
255: clear(null, null, null, null, null, null, null, null, null,
256: null, null, null, null, null, null, null, null, null,
257: null, null, null, null, null, null, null, null, null,
258: null, null, null, null, null, null, null, null, null,
259: null, null, null);
260: }
261:
262: private Term parseTerm(String termstr) {
263: return TacletForTests.parseTerm(termstr, new NamespaceSet(
264: new Namespace(), functions, sorts, new Namespace(),
265: new Namespace(), variables));
266: }
267:
268: private void assertEqualUpdates(final Update u1, final Update u2) {
269: assertEquals("Updates are expected to be equal: " + u1
270: + " and " + u2, u1.locationCount(), u2.locationCount());
271: for (int i = 0; i != u1.locationCount(); ++i)
272: assertEquals("Updates are expected to be equal: " + u1
273: + " and " + u2, u1.location(i), u2.location(i));
274: }
275:
276: private void assertEqualsModRenaming(Term t1, Term expected) {
277: assertTrue("Expected " + expected + ", but got " + t1, t1
278: .equalsModRenaming(expected));
279: }
280:
281: private void assertUnequalsModRenaming(Term t1, Term expected) {
282: assertFalse("Got something which is explicitly wrong: " + t1,
283: t1.equalsModRenaming(expected));
284: }
285:
286: public void testElementaryPVUpdates() {
287: final Services services = proof.getServices();
288: final UpdateFactory fac = new UpdateFactory(services,
289: simplifier);
290:
291: final Update u1 = fac.elementaryUpdate(t, i);
292: assertEquals(proof.simplifier().simplify(u1, nonRigidTarget,
293: services), parseTerm("{t := i} target"));
294:
295: final Update u2 = fac.skip();
296: assertEquals(proof.simplifier().simplify(u2, nonRigidTarget,
297: services), tf.createUpdateTerm(new Term[0],
298: new Term[0], nonRigidTarget));
299:
300: final Update u3 = fac.parallel(u1, u2);
301: assertEqualUpdates(u1, u3);
302:
303: final Update u4 = fac.elementaryUpdate(t, o);
304: assertEquals(proof.simplifier().simplify(u4, nonRigidTarget,
305: services), parseTerm("{t := o} target"));
306:
307: final Update u5 = fac.parallel(u1, u4);
308: assertEquals(parseTerm("{t := o} target"), proof.simplifier()
309: .simplify(u5, nonRigidTarget, services));
310:
311: final Update u6 = fac.sequential(u1, u4);
312: assertEquals(parseTerm("{t := o} target"), proof.simplifier()
313: .simplify(u6, nonRigidTarget, services));
314: }
315:
316: public void testElementaryAttrUpdates() {
317: final Services services = proof.getServices();
318: final UpdateFactory fac = new UpdateFactory(services,
319: simplifier);
320:
321: final Update u1 = fac.elementaryUpdate(o, u);
322: assertEquals(proof.simplifier().simplify(u1, nonRigidTarget,
323: services), parseTerm("{o := u} target"));
324:
325: final Update u2 = fac.elementaryUpdate(oa, i);
326: final AssignmentPairImpl wanted2 = new AssignmentPairImpl(
327: (Location) oa.op(), new Term[] { oa.sub(0) }, i);
328: assertTrue(
329: "Unexpected update: " + u2 + ", expected " + wanted2,
330: u2.locationCount() == 1
331: && u2.getAssignmentPair(0).equals(wanted2));
332:
333: final Update u3 = fac.elementaryUpdate(ua, i);
334: final AssignmentPairImpl wanted3 = new AssignmentPairImpl(
335: (Location) ua.op(), new Term[] { ua.sub(0) }, i);
336: assertTrue(
337: "Unexpected update: " + u3 + ", expected " + wanted3,
338: u3.locationCount() == 1
339: && u3.getAssignmentPair(0).equals(wanted3));
340:
341: final Update u4 = fac.parallel(u1, u3);
342: final Update u5 = fac.sequential(u1, u2);
343: final Update u6 = fac.sequential(u3, u1);
344: assertEqualUpdates(u4, u5);
345: assertEquals(proof.simplifier().simplify(u4, nonRigidTarget,
346: services), proof.simplifier().simplify(u6,
347: nonRigidTarget, services));
348: }
349:
350: public void testGuardedUpdates() {
351: final Services services = proof.getServices();
352: final UpdateFactory fac = new UpdateFactory(services,
353: simplifier);
354:
355: final Update u1 = fac.guard(phi, fac.elementaryUpdate(o, u));
356: assertEquals(proof.simplifier().simplify(u1, nonRigidTarget,
357: services), parseTerm("{\\if (phi) o := u} target"));
358:
359: final Update u2 = fac.parallel(u1, fac.elementaryUpdate(t, i));
360: assertEquals(proof.simplifier().simplify(u2, nonRigidTarget,
361: services),
362: parseTerm("{\\if (phi) o := u || t := i} target"));
363:
364: final Update u3 = fac.guard(psi, u2);
365: assertEquals(
366: proof.simplifier().simplify(u3, nonRigidTarget,
367: services),
368: parseTerm("{\\if (psi & phi) o := u || \\if (psi) t := i} target"));
369:
370: final Update u4 = fac.guard(tf.createJunctorTerm(Op.TRUE), u3);
371: assertEqualUpdates(u3, u4);
372:
373: final Update u5 = fac.guard(tf.createJunctorTerm(Op.FALSE), u3);
374: assertEquals(proof.simplifier().simplify(fac.skip(),
375: nonRigidTarget, services), proof.simplifier().simplify(
376: u5, nonRigidTarget, services));
377: }
378:
379: public void testQuantifiedUpdates() {
380: // the following test very much reflect the current state of optimizing
381: // the UpdateFactory; the particular shape of guards could change a lot
382: // later
383:
384: final Services services = proof.getServices();
385: final UpdateFactory fac = new UpdateFactory(services,
386: simplifier);
387: final Update u1 = fac.quantify(var, fac.elementaryUpdate(avar,
388: u));
389: assertEqualsModRenaming(proof.simplifier().simplify(u1,
390: nonRigidTarget, services),
391: parseTerm("{\\for int var; _a[var] := u} target"));
392:
393: // subsumption
394: final Update u2 = fac.parallel(u1, u1);
395: final Update u3 = fac.sequential(u1, u1);
396: assertEqualsModRenaming(proof.simplifier().simplify(u2,
397: nonRigidTarget, services),
398: parseTerm("{\\for int var; _a[var] := u} target"));
399: assertEqualsModRenaming(proof.simplifier().simplify(u3,
400: nonRigidTarget, services),
401: parseTerm("{\\for int var; _a[var] := u} target"));
402:
403: // quantifying a variable twice is meaningless
404: final Update u4 = fac.quantify(var, u1);
405: assertEqualUpdates(u1, u4);
406:
407: final Update u5 = fac.quantify(var, fac.parallel(fac
408: .elementaryUpdate(avar, u), fac.elementaryUpdate(bvar,
409: u)));
410: assertEqualsModRenaming(
411: proof.simplifier().simplify(u5, nonRigidTarget,
412: services),
413: parseTerm("{\\for int var; _a[var] := u ||"
414: + "\\for int var; \\if (\\forall int varPrime; (quanUpdateLeqInt(var,varPrime) | !(_b=_a & var=varPrime))) _b[var] := u} target"));
415:
416: final Update u10 = fac.quantify(var, fac.parallel(fac.quantify(
417: var, fac.elementaryUpdate(avar, u)), fac
418: .elementaryUpdate(bvar, u)));
419: assertEqualsModRenaming(
420: proof.simplifier().simplify(u10, nonRigidTarget,
421: services),
422: parseTerm("{\\for int var; _a[var] := u ||"
423: + "\\for int var; \\if (\\forall int varPrime; (quanUpdateLeqInt(var,varPrime) | !_b=_a)) _b[var] := u} target"));
424:
425: final Update u11 = fac.quantify(var, fac.parallel(fac
426: .elementaryUpdate(bvar, u), fac.quantify(var, fac
427: .elementaryUpdate(avar, u))));
428: assertEqualsModRenaming(proof.simplifier().simplify(u11,
429: nonRigidTarget, services),
430: parseTerm("{\\for int var; _b[var] := u ||"
431: + "\\for int var; _a[var] := u} target"));
432: assertUnequalsModRenaming(proof.simplifier().simplify(u11,
433: nonRigidTarget, services),
434: parseTerm("{\\for int var; _a[var] := u ||"
435: + "\\for int var; _b[var] := u} target"));
436:
437: final Update u6 = fac.quantify(var, fac.elementaryUpdate(o, u));
438: assertEqualsModRenaming(proof.simplifier().simplify(u6,
439: nonRigidTarget, services), parseTerm("{o := u} target"));
440:
441: final Update u7 = fac.quantify(var, fac.parallel(u5, fac
442: .elementaryUpdate(o, avar)));
443: assertEqualsModRenaming(
444: proof.simplifier().simplify(u7, nonRigidTarget,
445: services),
446: parseTerm("{\\for int var; _a[var] := u ||"
447: + "\\for int var; \\if (\\forall int varPrime; (quanUpdateLeqInt(var,varPrime) | !(_b=_a & var=varPrime))) _b[var] := u ||"
448: + "\\for int var; o := _a[var]} target"));
449:
450: final Update u8 = fac.guard(tf.createFunctionTerm(woRelation,
451: varT, var2T), fac.elementaryUpdate(avar, bvar2));
452: final Update u9 = fac.quantify(var2, fac.quantify(var, u8));
453: assertEqualsModRenaming(
454: proof.simplifier().simplify(u9, nonRigidTarget,
455: services),
456: parseTerm("{\\for (int var2; int var) \\if(quanUpdateLeqInt(var, var2)) _a[var] := _b[var2]} target"));
457:
458: final Update u12 = fac.quantify(var, fac.parallel(fac
459: .elementaryUpdate(bvar, u), fac.quantify(var2, fac
460: .elementaryUpdate(avarvar2, u))));
461: assertEqualsModRenaming(
462: proof.simplifier().simplify(u12, nonRigidTarget,
463: services),
464: parseTerm("{\\for int var; _b[var] := u || "
465: + "\\for (int var; int var2)"
466: + " \\if (\\forall int varPrime;"
467: + " (quanUpdateLeqInt(var,varPrime) |"
468: + " !(_a=_b & f(var,var2)=varPrime))) _a[f(var,var2)] := u} target"));
469: }
470:
471: public void testConstruction() {
472: final Services services = proof.getServices();
473: final UpdateFactory fac = new UpdateFactory(services,
474: simplifier);
475:
476: final Update u1 = fac.quantify(var, fac.elementaryUpdate(avar,
477: bvar));
478:
479: // the same by directly using the TermFactory; we are using two
480: // different bound variables for different subterms (that have to be
481: // unified by QuanUpdateOperator)
482: final Term[] subTerms = new Term[] { a, var2T, bvar,
483: nonRigidTarget };
484: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[4];
485: boundVars[0] = new ArrayOfQuantifiableVariable(
486: new QuantifiableVariable[] { var });
487: boundVars[1] = new ArrayOfQuantifiableVariable(
488: new QuantifiableVariable[] { var2 });
489: boundVars[2] = boundVars[0];
490: boundVars[3] = new ArrayOfQuantifiableVariable();
491:
492: final QuanUpdateOperator op = QuanUpdateOperator
493: .createUpdateOp(new Term[] { avar2 },
494: new boolean[] { false });
495: final Term updTerm = tf.createQuanUpdateTerm(op, subTerms,
496: boundVars);
497:
498: assertEqualsModRenaming(proof.simplifier().simplify(u1,
499: nonRigidTarget, services), updTerm);
500: }
501:
502: public void testApplicationWithCollision() {
503: final Services services = proof.getServices();
504: final UpdateFactory fac = new UpdateFactory(services,
505: simplifier);
506:
507: final Update u2 = fac.elementaryUpdate(avar, bvar);
508: final Update u1 = fac.quantify(var, u2);
509:
510: // otherwise we don't have a real collision ...
511: assertSame(u1.getAssignmentPair(0).boundVars()
512: .getQuantifiableVariable(0), var);
513:
514: assertEqualsModRenaming(proof.simplifier().simplify(u1, avar,
515: services), bvar);
516: assertEqualsModRenaming(proof.simplifier().simplify(u2, avar,
517: services), bvar);
518:
519: // try to substitute a free variable in a quantifier scope ...
520: final Term quantifierFor = tf.createQuantifierTerm(Op.ALL, var,
521: tf.createEqualityTerm(o, avar));
522: final Update u3 = fac.elementaryUpdate(o, bvar);
523:
524: final Term resultFor = tf.createQuantifierTerm(Op.ALL, var2, tf
525: .createEqualityTerm(bvar, avar2));
526: assertEqualsModRenaming(proof.simplifier().simplify(u3,
527: quantifierFor, services), resultFor);
528: }
529:
530: public void testCollisionWhenAddingGuard() {
531: final Services services = proof.getServices();
532: final UpdateFactory fac = new UpdateFactory(services,
533: simplifier);
534:
535: final Update u1 = fac.guard(tf.createEqualityTerm(avar, bvar),
536: fac.quantify(var, fac.elementaryUpdate(avar, bvar)));
537: final Update u2 = fac.guard(tf.createEqualityTerm(avar, bvar),
538: fac.quantify(var2, fac.elementaryUpdate(avar2, bvar2)));
539: assertEqualsModRenaming(proof.simplifier().simplify(u1,
540: nonRigidTarget, services), proof.simplifier().simplify(
541: u2, nonRigidTarget, services));
542: }
543:
544: public void testEffectLess() {
545: // test that an earlier bug is no longer present:
546: // the update factory correctly creates effectless assignment
547: // updates a:=a, the different constructors provided by the factory
548: // do not eliminate such assignments
549:
550: final UpdateFactory fac = new UpdateFactory(
551: proof.getServices(), simplifier);
552:
553: final Update effectFull = fac.elementaryUpdate(o, u);
554:
555: final Update effectLess0 = fac.elementaryUpdate(o, o);
556: final Update effectLess1 = fac.parallel(effectLess0,
557: effectLess0);
558: final Update effectLess2 = fac.sequential(effectLess0,
559: effectLess0);
560: final Update effectLess3 = fac.quantify(var, effectLess0);
561: final Update effectLess4 = fac.guard(tf
562: .createJunctorTerm(Op.TRUE), effectLess0);
563: final Update effectLess5 = fac.apply(fac.skip(), effectLess0);
564:
565: assertEquals(o, fac.apply(
566: fac.parallel(effectFull, effectLess0), o));
567: assertEquals(o, fac.apply(
568: fac.parallel(effectFull, effectLess1), o));
569: assertEquals(o, fac.apply(
570: fac.parallel(effectFull, effectLess2), o));
571: assertEquals(o, fac.apply(
572: fac.parallel(effectFull, effectLess3), o));
573: assertEquals(o, fac.apply(
574: fac.parallel(effectFull, effectLess4), o));
575: assertEquals(o, fac.apply(
576: fac.parallel(effectFull, effectLess5), o));
577: }
578:
579: private void clear(Proof proof, Namespace variables,
580: Namespace functions, Namespace sorts, ProgramVariable[] pv,
581: TermFactory tf, Sort testSort0, Sort testSort1,
582: Sort testSort2, Sort cloneable, Sort serializable,
583: Sort integerSort, Term t, Term i, Term o, Term u, Term oa,
584: Term ua, Term phi, Term psi, ArraySort arraySort1,
585: ArraySort arraySort2, Term a, Term b,
586: NonRigidFunction nonRigidTargetOp, Term nonRigidTarget,
587: QuantifiableVariable var, Term varT,
588: QuantifiableVariable var2, Term var2T, Function f,
589: Term fvarvar2, Term avar, Term bvar, Term avar2,
590: Term avarvar2, Term bvar2, Function woRelation,
591: UpdateSimplifier simplifier) {
592: this.proof = proof;
593: this.variables = variables;
594: this.functions = functions;
595: this.sorts = sorts;
596: this.pv = pv;
597: this.tf = tf;
598: this.testSort0 = testSort0;
599: this.testSort1 = testSort1;
600: this.testSort2 = testSort2;
601: this.cloneable = cloneable;
602: this.serializable = serializable;
603: this.integerSort = integerSort;
604: this.t = t;
605: this.i = i;
606: this.o = o;
607: this.u = u;
608: this.oa = oa;
609: this.ua = ua;
610: this.phi = phi;
611: this.psi = psi;
612: this.arraySort1 = arraySort1;
613: this.arraySort2 = arraySort2;
614: this.a = a;
615: this.b = b;
616: this.nonRigidTargetOp = nonRigidTargetOp;
617: this.nonRigidTarget = nonRigidTarget;
618: this.var = var;
619: this.varT = varT;
620: this.var2 = var2;
621: this.var2T = var2T;
622: this.f = f;
623: this.fvarvar2 = fvarvar2;
624: this.avar = avar;
625: this.bvar = bvar;
626: this.avar2 = avar2;
627: this.avarvar2 = avarvar2;
628: this.bvar2 = bvar2;
629: this.woRelation = woRelation;
630: this.simplifier = simplifier;
631: }
632: }
|