001 // ***** This file is automatically generated from Quant.java.jpp and QuantBody.java.jpp.
002
003 package daikon;
004
005 import java.util.*;
006 import java.lang.reflect.*;
007
008 /**
009 * The Quant library provides routines that operate on arrays and
010 * collections.
011 *
012 * These routines are used by the Java family of output
013 * formats. This allows invariants to be output as snippets of
014 * executable (Java) code. For example, an invariant like
015 * <pre>
016 * a[] elements >= 1
017 * </pre>
018 * is output (in the Java, JML, and DBC formats) as something like
019 * <pre>
020 * daikon.Quant.eltsGTE(a, 1)
021 * </pre>
022 *
023 * <h3>Naming</h3>
024 *
025 * The library methods have names of the following forms, where OP
026 * indicates an operation: Equal, NotEqual, GT (greater than), GTE
027 * (greater than or equal to), LT, LTE.
028 * <ul>
029 * <li>pairwiseOP. Apply OP to corresponding elements of two arrays:
030 * a[0] OP b[0], a[1] OP b[1], etc.
031 * <li>eltsOP. Apply OP to each element of one array, and a scalar:
032 * a[0] OP x, a[1] OP x, etc.
033 * <li>eltwiseOP: Apply OP to adjacent elements of one array:
034 * a[0] OP a[1], a[1] OP a[2], etc.
035 * <li>lexOP: Determine lexical ordering:
036 * compare two arrays pairwise, stopping as soon as the result is known.
037 * <li>eltsOPindex: Apply op to array elements and their indices:
038 * a[0] OP 0, a[1] OP 1, etc.
039 * </ul>
040 *
041 * <h3>Equality semantics</h3>
042 *
043 * Whenever a method involves comparing two elements for equality, this is
044 * always "==" equality (even for Objects and Strings).
045 *
046 * <h3>No exceptions thrown</h3>
047 *
048 * The library strives not to throw exceptions, even if illegal arguments
049 * are passed to the routines. This has two consequences.<p>
050 *
051 * First, each predicate (boolean method) returns false when invoked on an
052 * illegal argument such as a null collection (array or Collection).<p>
053 *
054 * Second, each accessor method returns a default "bad" value if inovked on
055 * an illegal argument. For example, the default value for the double type
056 * is Double.NaN.<p>
057 *
058 * The rationale for the decision to never throw exceptions is that we wish
059 * to be able to invoke the Quant methods at run time without distrubing
060 * execution of a program, and without forcing clients to write a try
061 * .. catch block around each invocation.<p>
062 *
063 * A downside of the decision is that if the default value is returned, it
064 * may be impossible for a client to determine whether the method really
065 * returned that value, or whether the invocation involved an illegal
066 * argument. To avoid this problem, it is generally better to use a Quant
067 * library predicate rather than returning a value and then testing it
068 * externally.
069 */
070 public final class Quant {
071 private Quant() { throw new Error("do not instantiate"); }
072
073 public static utilMDE.FuzzyFloat fuzzy = new utilMDE.FuzzyFloat();
074
075 /** Returns the size of the array or collection.
076 * If the argument is null or not an array or collection, returns a
077 * default value (Integer.MAX_VALUE).
078 * Thus, for an array a, this never throws an exception, though a.length may.
079 */
080 // Not called from Quant; provided only for external use.
081 /* pure */ public static int size(Object o) {
082 if (o == null) { return Integer.MAX_VALUE; } // return default value
083 java.lang.Class<?> c = o.getClass();
084 if (c.isArray()) {
085 return java.lang.reflect.Array.getLength(o);
086 } else if (o instanceof Collection<?>) {
087 return ((Collection<?>)o).size();
088 } else {
089 return Integer.MAX_VALUE; // return default value
090 }
091 }
092
093 /** Returns the size of the collection.
094 * If the argument is null, returns a default value (Integer.MAX_VALUE).
095 */
096 // Not called from Quant; provided only for external use.
097 /* pure */ public static int size(Collection<?> o) {
098 if (o == null) { return Integer.MAX_VALUE; } // return default value
099 return o.size();
100 }
101
102 /** True iff the sequence contains no null elements. */
103 /* pure */ public static boolean eltsNonNull(Object[] seq1) {
104 if (seq1 == null) { return false; }
105 for (int i = 0 ; i < seq1.length ; i++) {
106 if (seq1[i] == null) {
107 return false;
108 }
109 }
110 return true;
111 }
112
113 ///////////////////////////////////////////////////////////////////////////
114 /// Methods for "boolean" (from QuantBody.java.jpp)
115 ///
116
117 /** Returns the ith element of the array or collection argument.
118 * If the argument is null or not an array or collection, returns a
119 * default value (false).
120 **/
121 /* pure */ public static boolean getElement_boolean (Object o, long i) {
122 if (o == null) { return false; } // return default value
123 java.lang.Class<?> c = o.getClass();
124 if (c.isArray()) {
125 return java.lang.reflect.Array.getBoolean (o, (int)i);
126 } else if (o instanceof java.util.AbstractCollection<?>) {
127 return java.lang.reflect.Array.getBoolean (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
128 } else {
129 return false; // return default value
130 }
131 }
132
133 /* pure */ public static boolean getElement_boolean (boolean[] arr, long i) {
134 if (arr == null) { return false; } // return default value
135 return arr[(int)i];
136 }
137
138 private static boolean eq(boolean x, boolean y) {
139 return (x == y);
140 }
141
142 private static boolean ne(boolean x, boolean y) {
143 return x != y;
144 }
145
146 /** True iff both sequences are non-null and have the same length. */
147 /* pure */ public static boolean sameLength(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
148 return ((seq1 != null)
149 && (seq2 != null)
150 && seq1.length == seq2.length);
151 }
152
153 /**
154 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
155 * If either array is null, returns null.
156 * If either array is empty, returns only those elements in the other array.
157 * If both arrays are empty, returns a new empty array.
158 */
159 /* pure */ public static boolean /*@PolyNull*/ [] concat(boolean /*@PolyNull*/ [] seq1, boolean /*@PolyNull*/ [] seq2) {
160 if (seq1 == null) { return null; }
161 if (seq2 == null) { return null; }
162 return utilMDE.ArraysMDE.concat(seq1, seq2);
163 }
164
165 /**
166 * Returns an array that is equivalent to the set union of seq1 and seq2.
167 * This method gives no assurances about the order or repetition of elements:
168 * elements may be repeated, and their order may be different from the
169 * order of elements in seq1 and seq2.
170 */
171 /* pure */ public static boolean /*@PolyNull*/ [] union(boolean /*@PolyNull*/ [] seq1, boolean /*@PolyNull*/ [] seq2) {
172 if (seq1 == null) { return null; }
173 if (seq2 == null) { return null; }
174 return concat(seq1, seq2);
175 }
176
177 /**
178 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
179 * This method gives no assurances about the order or repetition of elements:
180 * elements may be repeated, and their order may be different from the
181 * order of elements in seq1 and seq2.
182 */
183 /* pure */ public static boolean /*@PolyNull*/ [] intersection(boolean /*@PolyNull*/ [] seq1, boolean /*@PolyNull*/ [] seq2) {
184 if (seq1 == null) { return null; }
185 if (seq2 == null) { return null; }
186 boolean[] intermediate = new boolean[Math.min(seq1.length, seq2.length)];
187 int length = 0;
188 for (int i = 0 ; i < seq1.length ; i++) {
189 if (memberOf(seq1[i], seq2) ) {
190 intermediate[length++] = seq1[i];
191 }
192 }
193 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
194 }
195
196 /**
197 * Returns an array that is equivalent to the set difference of seq1 and seq2.
198 * This method gives no assurances about the order or repetition of elements:
199 * elements may be repeated, and their order may be different from the
200 * order of elements in seq1 and seq2.
201 */
202 /* pure */ public static boolean /*@PolyNull*/ [] setDiff(boolean /*@PolyNull*/ [] seq1, boolean /*@PolyNull*/ [] seq2) {
203 if (seq1 == null) { return null; }
204 if (seq2 == null) { return null; }
205 boolean[] intermediate = new boolean[seq1.length];
206 int length = 0;
207 for (int i = 0 ; i < seq1.length ; i++) {
208 if (!memberOf(seq1[i], seq2)) {
209 intermediate[length++] = seq1[i];
210 }
211 }
212 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
213 }
214
215 /**
216 * Retuns true iff seq1 and seq2 are equal when considered as sets.
217 */
218 /* pure */ public static boolean setEqual(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
219 if (seq1 == null) { return false; }
220 if (seq2 == null) { return false; }
221 for (int i = 0; i < seq1.length ; i++) {
222 if (!memberOf(seq1[i], seq2) ) {
223 return false;
224 }
225 }
226 for (int i = 0; i < seq2.length ; i++) {
227 if (!memberOf(seq2[i], seq1) ) {
228 return false;
229 }
230 }
231 return true;
232 }
233
234 /** True iff seq1 is the reverse of seq2.
235 *
236 * Meaning (in pseudo-FOL):
237 *
238 * <pre>
239 * /\ seq1.length == seq2.length
240 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
241 * </pre>
242 *
243 */
244 /* pure */ public static boolean isReverse(boolean[] seq1, boolean[] seq2) {
245 if (! sameLength(seq1, seq2)) { return false; }
246 assert seq1 != null && seq2 != null; // because sameLength() = true
247 int length = seq1.length;
248 for (int i = 0 ; i < length ; i++) {
249 if (ne(seq1[i], seq2[length - i - 1])) {
250 return false;
251 }
252 }
253 return true;
254 }
255
256 /**
257 * True iff seq1 is a subset of seq2, when the sequences are
258 * considered as sets.
259 */
260 /* pure */ public static boolean subsetOf(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
261 if (seq1 == null) { return false; }
262 if (seq2 == null) { return false; }
263 for (int i = 0 ; i < seq1.length ; i++) {
264 if (!memberOf(seq1[i], seq2)) {
265 return false;
266 }
267 }
268 return true;
269 }
270
271 /**
272 * Returns true iff seq contains no duplicate elements.
273 */
274 /* pure */ public static boolean noDups(boolean /*@Nullable*/ [] seq) {
275 if (seq == null) { return false; }
276 return utilMDE.ArraysMDE.noDuplicates(seq);
277 }
278
279 /**
280 * Returns true iff elt is in array arr.
281 */
282 /* pure */ public static boolean memberOf(boolean elt, boolean /*@Nullable*/ [] arr) {
283 if (arr == null) { return false; }
284 for (int i = 0 ; i < arr.length ; i++) {
285 if (eq(arr[i], elt)) { return true; }
286 }
287 return false;
288 }
289
290 /**
291 * Returns a subsequence of seq with first elements seq[start] and
292 * last element seq[end].
293 */
294 /* pure */ public static boolean /*@PolyNull*/ [] slice(boolean /*@PolyNull*/ [] seq, int start, int end) {
295 if (seq == null) { return null; }
296 int sliceStart = start;
297 int sliceEnd = end;
298 if (start < 0) { return new boolean[] { }; }
299 if (end > seq.length-1) { return new boolean[] { }; }
300 if (sliceStart > sliceEnd) { return new boolean[] { }; }
301 int length = sliceEnd - sliceStart + 1;
302 return utilMDE.ArraysMDE.subarray(seq, sliceStart, length);
303 }
304
305 /* pure */ public static boolean /*@PolyNull*/ [] slice(boolean /*@PolyNull*/ [] seq, long start, int end) {
306 return slice(seq, (int)start, end);
307 }
308 /* pure */ public static boolean /*@PolyNull*/ [] slice(boolean /*@PolyNull*/ [] seq, int start, long end) {
309 return slice(seq, start, (int)end);
310 }
311 /* pure */ public static boolean /*@PolyNull*/ [] slice(boolean /*@PolyNull*/ [] seq, long start, long end) {
312 return slice(seq, (int)start, (int)end);
313 }
314
315 /** True iff all elements in arr equal elt.
316 *
317 * Meaning (in pseudo-FOL):
318 *
319 * forall i in { 0..arr.length-1 } : arr[i] == elt
320 *
321 */
322 /* pure */ public static boolean eltsEqual(boolean /*@Nullable*/ [] arr, boolean elt) {
323 if (arr == null) { return false; }
324 for (int i = 0 ; i < arr.length ; i++) {
325 if (ne(arr[i], elt)) { return false; }
326 }
327 return true;
328 }
329
330 /** True iff every element in arr does not equal elt.
331 *
332 * Meaning (in pseudo-FOL):
333 *
334 * forall i in { 0..arr.length-1 } : arr[i] != elt
335 *
336 */
337 /* pure */ public static boolean eltsNotEqual(boolean /*@Nullable*/ [] arr, boolean elt) {
338 if (arr == null) { return false; }
339 for (int i = 0 ; i < arr.length ; i++) {
340 if (eq(arr[i], elt)) { return false; }
341 }
342 return true;
343 }
344
345 /** True iff seq1 and seq2 have the same length, and every seq1[i] == seq2[i].
346 *
347 * Meaning (in pseudo-FOL):
348 *
349 * /\ seq1.length == se2.length
350 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[i]
351 *
352 */
353
354 /* pure */ public static boolean pairwiseEqual(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
355 if (! sameLength(seq1, seq2)) { return false; }
356 assert seq1 != null && seq2 != null; // because sameLength() = true
357 for (int i = 0 ; i < seq1.length ; i++) {
358 if (ne(seq1[i], seq2[i])) {
359 return false;
360 }
361 }
362 return true;
363 }
364
365 /** True iff seq1 and seq2 have the same length, and every seq1[i] != seq2[i].
366 *
367 * Meaning (in pseudo-FOL):
368 *
369 * /\ seq1.length == se2.length
370 * /\ forall i in { 0..seq1.length-1 } : seq1[i] != seq2[i]
371 *
372 */
373 /* pure */ public static boolean pairwiseNotEqual(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
374 if (! sameLength(seq1, seq2)) { return false; }
375 assert seq1 != null && seq2 != null; // because sameLength() = true
376 for (int i = 0 ; i < seq1.length ; i++) {
377 if (eq(seq1[i], seq2[i])) {
378 return false;
379 }
380 }
381 return true;
382 }
383
384 /**
385 * Returns true iff seq1 is lexically equal to seq2.
386 * For equality, "lexically" and "pairwise" are the same.
387 */
388 /* pure */ public static boolean lexEqual(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
389 if (seq1 == null) { return false; }
390 if (seq2 == null) { return false; }
391 return pairwiseEqual(seq1, seq2);
392 }
393
394 /**
395 * Returns true iff seq1 is lexically not equal to seq2.
396 */
397 /* pure */ public static boolean lexNotEqual(boolean /*@Nullable*/ [] seq1, boolean /*@Nullable*/ [] seq2) {
398 if (seq1 == null) { return false; }
399 if (seq2 == null) { return false; }
400 return !lexEqual(seq1, seq2);
401 }
402
403 /** True iff for all applicable i, every seq[i] == seq[i+1].
404 *
405 * Meaning (in pseudo-FOL):
406 *
407 * forall i in { 0..seq.length-2 } : seq[i] == seq[i+1]
408 *
409 */
410 /* pure */ public static boolean eltwiseEqual(boolean /*@Nullable*/ [] seq) {
411 if (seq == null) { return false; }
412 for (int i = 0 ; i < seq.length ; i++) {
413 if (i < seq.length-1) {
414 if (ne(seq[i], seq[i+1])) {
415 return false;
416 }
417 }
418 }
419 return true;
420 }
421
422 /** True iff for all applicable i, every seq[i] != seq[i+1].
423 *
424 * Meaning (in pseudo-FOL):
425 *
426 * forall i in { 0..seq.length-2 } : seq[i] != seq[i+1]
427 *
428 */
429 /* pure */ public static boolean eltwiseNotEqual(boolean /*@Nullable*/ [] seq) {
430 if (seq == null) { return false; }
431 for (int i = 0 ; i < seq.length ; i++) {
432 if (i < seq.length-1) {
433 if (eq(seq[i], seq[i+1])) {
434 return false;
435 }
436 }
437 }
438 return true;
439 }
440
441 /// Deferencing (accessing) fields
442
443 /**
444 * collectboolean accepts an object and a list of fields (one of which is
445 * of array type, and the rest of which are not), and produces an array in
446 * which the original object has had the given fields accessed.
447 *
448 * Daikon creates invariants over "variables" such as the following.
449 *
450 * x.arr[].z The result of collecting all elements y.z for all y's
451 * in array x.arr.
452 * arr[].y.z The result of collecting all elements x.y.z for all x's
453 * in array arr.
454 * x.y.z[] The result of collecting all elements in array x.y.z[]
455 *
456 * The collectboolean() method does this collecting work.
457 *
458 * Given an object (x, arr, or x, correspondingly, in the above examples)
459 * and a "field string" (arr.z, y.z, or y.z, correspondingly, in the
460 * above example), the collect method collects the elements the result
461 * from following the fields, one of which is assumed to be an array.
462 *
463 * requires: fieldStr.length() > 0 and object != null
464 * requires: fieldStr contains only field names, no "[]" strings.
465 *
466 * requires: the method only works for field sequences with exactly
467 * one field representing an array. For example, the collection
468 * a[].b[].c will fail.
469 *
470 * If the resulting collection is of non-primitive type, then collect
471 * returns an array of type Object[].
472 *
473 * Returns null if any array or field access causes an exception.
474 */
475 /* pure */ public static boolean /*@Nullable*/ [] collectboolean (Object object, String fieldStr) {
476
477 if (object == null) { return null; }
478 if (fieldStr == null) { return null; }
479
480 //assert fieldStr != null && !"".equals(fieldStr);
481 String[] fieldNames = fieldStr.split("\\.");
482 boolean[] retval = collectboolean (object, fieldNames, 0);
483 //System.err.println("%%% fieldArray returned: " + utilMDE.ArraysMDE.toString(retval));
484 return retval;
485 }
486
487 /** Helper method for collectboolean(Object, String).
488 * Operates on the fields specified in fields[fieldsStartIdx..].
489 * @see collectboolean(Object, String)
490 */
491 /* pure */ private static boolean /*@Nullable*/ [] collectboolean (Object object,
492 String[] fields, int fieldsStartIdx) {
493
494 if (object == null) { return null; }
495 assert (fields != null);
496 assert (fieldsStartIdx >= 0 && fieldsStartIdx < fields.length);
497
498 Object fieldObj = null;
499 try {
500 Field field = (object instanceof java.lang.Class<?>)
501 ? ((Class<?>)object).getDeclaredField(fields[fieldsStartIdx])
502 : object.getClass().getDeclaredField(fields[fieldsStartIdx]);
503 field.setAccessible(true);
504 // Class cls = field.getType();
505 fieldObj = field.get(object);
506 //System.out.println("***fieldObj="+fieldObj);
507
508 } catch (Exception e) {
509 return null;
510
511 }
512
513 if (fieldObj == null) {
514 return null;
515 }
516
517 // base case: just accessed the last field
518 if (fields.length - 1 == fieldsStartIdx) {
519
520 if (fieldObj.getClass().isArray()) {
521 // last field is an array
522 return (boolean[])fieldObj;
523 } else {
524 // This hack should be removed in favor of, at "oneEltArray = ..."
525 // below, calling a version of collectboolean_field that throws an
526 // error. Then, this case becomes a run-time error. -MDE
527
528 // Just one element; return a one-element array.
529 //assert cls.equals(Boolean.TYPE);
530 return new boolean[] { ((Boolean)fieldObj).booleanValue() };
531 }
532 } else {
533 // recursive case: more fields to access after this one
534
535 if (daikon.ProglangType.list_implementors.contains(fieldObj.getClass().getName())) {
536
537 java.util.AbstractCollection<?> collection = (java.util.AbstractCollection<?>)fieldObj;
538 boolean[] intermediate = new boolean[collection.size()];
539 int index = 0;
540 for (Iterator<?> i = collection.iterator() ; i.hasNext() ; ) {
541 boolean[] oneEltArray = collectboolean (i.next(), fields, fieldsStartIdx + 1);
542 //assert oneEltArray.length == 1;
543 intermediate[index++] = oneEltArray[0];
544 }
545 return intermediate;
546 } else if (fieldObj.getClass().isArray()) {
547
548 // collect elements across array
549 boolean[] intermediate = new boolean[Array.getLength(fieldObj)];
550 for (int i = 0 ; i < intermediate.length ; i++) {
551 boolean[] oneEltArray = collectboolean (Array.get(fieldObj, i),
552 fields, fieldsStartIdx + 1);
553 //assert oneEltArray.length == 1;
554 intermediate[i] = oneEltArray[0];
555 }
556 return intermediate;
557 } else {
558
559 return collectboolean (fieldObj, fields, fieldsStartIdx + 1);
560 }
561 }
562 }
563
564 // Returns the results of dereferencing the fields specified in
565 // fields[fieldsStartIdx..] for 'object'.
566 // Returns a default value if any field access causes an exception.
567 /* pure */ public static boolean collectboolean_field (Object object, String fieldStr) {
568
569 if (object == null) { return false; } // return default value
570 if (fieldStr == null) { return false; } // return default value
571
572 String[] fieldNames = fieldStr.split("\\.");
573
574 // Holds the intermediate (and final) result
575 Object fieldObj = object;
576
577 for (int i = 0 ; i < fieldNames.length ; i++) {
578
579 String fieldName = fieldNames[i];
580
581 try {
582 Field field =
583 (fieldObj instanceof java.lang.Class<?>)
584 ? ((Class<?>)fieldObj).getDeclaredField(fieldName)
585 : fieldObj.getClass().getDeclaredField(fieldName);
586 field.setAccessible(true);
587 fieldObj = field.get(fieldObj);
588
589 } catch (Exception e) {
590 return false; // return default value
591
592 }
593
594 }
595
596 return ((Boolean)fieldObj).booleanValue();
597 }
598
599 ///////////////////////////////////////////////////////////////////////////
600 /// Methods for "byte" (from QuantBody.java.jpp)
601 ///
602
603 /** Returns the ith element of the array or collection argument.
604 * If the argument is null or not an array or collection, returns a
605 * default value (Byte.MAX_VALUE).
606 **/
607 /* pure */ public static byte getElement_byte (Object o, long i) {
608 if (o == null) { return Byte.MAX_VALUE; } // return default value
609 java.lang.Class<?> c = o.getClass();
610 if (c.isArray()) {
611 return java.lang.reflect.Array.getByte (o, (int)i);
612 } else if (o instanceof java.util.AbstractCollection<?>) {
613 return java.lang.reflect.Array.getByte (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
614 } else {
615 return Byte.MAX_VALUE; // return default value
616 }
617 }
618
619 /* pure */ public static byte getElement_byte (byte[] arr, long i) {
620 if (arr == null) { return Byte.MAX_VALUE; } // return default value
621 return arr[(int)i];
622 }
623
624 private static boolean eq(byte x, byte y) {
625 return (x == y);
626 }
627
628 private static boolean ne(byte x, byte y) {
629 return x != y;
630 }
631
632 private static boolean lt(byte x, byte y) {
633 return x < y;
634 }
635
636 private static boolean lte(byte x, byte y) {
637 return x <= y;
638 }
639
640 private static boolean gt(byte x, byte y) {
641 return x > y;
642 }
643
644 private static boolean gte(byte x, byte y) {
645 return x >= y;
646 }
647
648 /** True iff both sequences are non-null and have the same length. */
649 /* pure */ public static boolean sameLength(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
650 return ((seq1 != null)
651 && (seq2 != null)
652 && seq1.length == seq2.length);
653 }
654
655 /** True iff both sequences are non-null and have the same length. */
656 /* pure */ public static boolean sameLength(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
657 return ((seq1 != null)
658 && (seq2 != null)
659 && seq1.length == seq2.length);
660 }
661
662 /** True iff both sequences have the same length, and all seq2[i] divide seq1[i].
663 *
664 * Meaning (in pseudo-FOL):
665 *
666 * <pre>
667 * /\ seq1.length == seq2.length
668 * /\ forall i in { 0..seq2.length-1 } : seq2[i] divides seq1[i]
669 * </pre>
670 *
671 */
672 /* pure */ public static boolean pairwiseDivides(byte[] seq1, byte[] seq2) {
673 if (! sameLength(seq1, seq2)) { return false; }
674 assert seq1 != null && seq2 != null; // because sameLength() = true
675 for (int i = 0 ; i < seq1.length ; i++) {
676 if (ne(seq1[i] % seq2[i], 0)) {
677 return false;
678 }
679 }
680 return true;
681 }
682 /* pure */ public static boolean pairwiseDivides(byte[] seq1, int[] seq2) {
683 if (! sameLength(seq1, seq2)) { return false; }
684 assert seq1 != null && seq2 != null; // because sameLength() = true
685 for (int i = 0 ; i < seq1.length ; i++) {
686 if (ne(seq1[i] % seq2[i], 0)) {
687 return false;
688 }
689 }
690 return true;
691 }
692
693 /** True iff both sequences have the same length, and all seq1[i] == seq2[i] * seq2[i].
694 *
695 * Meaning (in pseudo-FOL):
696 *
697 * <pre>
698 * /\ seq1.length == seq2.length
699 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == seq2[i] * seq2[i]
700 * </pre>
701 *
702 */
703 /* pure */ public static boolean pairwiseSquare(byte[] seq1, byte[] seq2) {
704 if (! sameLength(seq1, seq2)) { return false; }
705 assert seq1 != null && seq2 != null; // because sameLength() = true
706 for (int i = 0 ; i < seq1.length ; i++) {
707 if (ne(seq1[i], seq2[i] * seq2[i])) {
708 return false;
709 }
710 }
711 return true;
712 }
713 /* pure */ public static boolean pairwiseSquare(byte[] seq1, int[] seq2) {
714 if (! sameLength(seq1, seq2)) { return false; }
715 assert seq1 != null && seq2 != null; // because sameLength() = true
716 for (int i = 0 ; i < seq1.length ; i++) {
717
718 if (ne(seq1[i], seq2[i] * seq2[i])) {
719
720 return false;
721 }
722 }
723 return true;
724 }
725
726 /**
727 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
728 * If either array is null, returns null.
729 * If either array is empty, returns only those elements in the other array.
730 * If both arrays are empty, returns a new empty array.
731 */
732 /* pure */ public static byte /*@PolyNull*/ [] concat(byte /*@PolyNull*/ [] seq1, byte /*@PolyNull*/ [] seq2) {
733 if (seq1 == null) { return null; }
734 if (seq2 == null) { return null; }
735 return utilMDE.ArraysMDE.concat(seq1, seq2);
736 }
737
738 /* pure */ public static int /*@PolyNull*/ [] concat(byte /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
739 if (seq1 == null) { return null; }
740 if (seq2 == null) { return null; }
741 // Cannot just use utilMDE.ArraysMDE.concat because the two arrays
742 // have different types. This essentially inlines that method.
743 int newLength = seq1.length + seq2.length;
744 int[] retval = new int[newLength];
745
746 for (int j = 0 ; j < seq1.length ; j++) {
747 retval[j] = seq1[j];
748 }
749 System.arraycopy(seq2, 0, retval, seq1.length, seq2.length);
750
751 return retval;
752 }
753
754 /**
755 * Returns an array that is equivalent to the set union of seq1 and seq2.
756 * This method gives no assurances about the order or repetition of elements:
757 * elements may be repeated, and their order may be different from the
758 * order of elements in seq1 and seq2.
759 */
760 /* pure */ public static byte /*@PolyNull*/ [] union(byte /*@PolyNull*/ [] seq1, byte /*@PolyNull*/ [] seq2) {
761 if (seq1 == null) { return null; }
762 if (seq2 == null) { return null; }
763 return concat(seq1, seq2);
764 }
765
766 /* pure */ public static int /*@PolyNull*/ [] union(byte /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
767 if (seq1 == null) { return null; }
768 if (seq2 == null) { return null; }
769 return concat(seq1, seq2);
770 }
771
772 /**
773 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
774 * This method gives no assurances about the order or repetition of elements:
775 * elements may be repeated, and their order may be different from the
776 * order of elements in seq1 and seq2.
777 */
778 /* pure */ public static byte /*@PolyNull*/ [] intersection(byte /*@PolyNull*/ [] seq1, byte /*@PolyNull*/ [] seq2) {
779 if (seq1 == null) { return null; }
780 if (seq2 == null) { return null; }
781 byte[] intermediate = new byte[Math.min(seq1.length, seq2.length)];
782 int length = 0;
783 for (int i = 0 ; i < seq1.length ; i++) {
784 if (memberOf(seq1[i], seq2) ) {
785 intermediate[length++] = seq1[i];
786 }
787 }
788 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
789 }
790
791 /* pure */ public static int /*@PolyNull*/ [] intersection(byte /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
792 if (seq1 == null) { return null; }
793 if (seq2 == null) { return null; }
794 int[] intermediate = new int[Math.min(seq1.length, seq2.length)];
795 int length = 0;
796 for (int i = 0 ; i < seq1.length ; i++) {
797 if (memberOf(seq1[i], seq2) ) {
798 intermediate[length++] = seq1[i];
799 }
800 }
801 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
802 }
803
804 /**
805 * Returns an array that is equivalent to the set difference of seq1 and seq2.
806 * This method gives no assurances about the order or repetition of elements:
807 * elements may be repeated, and their order may be different from the
808 * order of elements in seq1 and seq2.
809 */
810 /* pure */ public static byte /*@PolyNull*/ [] setDiff(byte /*@PolyNull*/ [] seq1, byte /*@PolyNull*/ [] seq2) {
811 if (seq1 == null) { return null; }
812 if (seq2 == null) { return null; }
813 byte[] intermediate = new byte[seq1.length];
814 int length = 0;
815 for (int i = 0 ; i < seq1.length ; i++) {
816 if (!memberOf(seq1[i], seq2)) {
817 intermediate[length++] = seq1[i];
818 }
819 }
820 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
821 }
822
823 /* pure */ public static int /*@PolyNull*/ [] setDiff(byte /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
824 if (seq1 == null) { return null; }
825 if (seq2 == null) { return null; }
826 int[] intermediate = new int[seq1.length];
827 int length = 0;
828 for (int i = 0 ; i < seq1.length ; i++) {
829 if (!memberOf(seq1[i], seq2)) {
830 intermediate[length++] = seq1[i];
831 }
832 }
833 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
834 }
835
836 /**
837 * Retuns true iff seq1 and seq2 are equal when considered as sets.
838 */
839 /* pure */ public static boolean setEqual(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
840 if (seq1 == null) { return false; }
841 if (seq2 == null) { return false; }
842 for (int i = 0; i < seq1.length ; i++) {
843 if (!memberOf(seq1[i], seq2) ) {
844 return false;
845 }
846 }
847 for (int i = 0; i < seq2.length ; i++) {
848 if (!memberOf(seq2[i], seq1) ) {
849 return false;
850 }
851 }
852 return true;
853 }
854
855 /* pure */ public static boolean setEqual(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
856 if (seq1 == null) { return false; }
857 if (seq2 == null) { return false; }
858 for (int i = 0; i < seq1.length ; i++) {
859 if (!memberOf(seq1[i], seq2) ) {
860 return false;
861 }
862 }
863 for (int i = 0; i < seq2.length ; i++) {
864 if (!memberOf(seq2[i], seq1) ) {
865 return false;
866 }
867 }
868 return true;
869 }
870
871 /** True iff seq1 is the reverse of seq2.
872 *
873 * Meaning (in pseudo-FOL):
874 *
875 * <pre>
876 * /\ seq1.length == seq2.length
877 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
878 * </pre>
879 *
880 */
881 /* pure */ public static boolean isReverse(byte[] seq1, byte[] seq2) {
882 if (! sameLength(seq1, seq2)) { return false; }
883 assert seq1 != null && seq2 != null; // because sameLength() = true
884 int length = seq1.length;
885 for (int i = 0 ; i < length ; i++) {
886 if (ne(seq1[i], seq2[length - i - 1])) {
887 return false;
888 }
889 }
890 return true;
891 }
892
893 /* pure */ public static boolean isReverse(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
894 if (! sameLength(seq1, seq2)) { return false; }
895 assert seq1 != null && seq2 != null; // because sameLength() = true
896 int length = seq1.length;
897 for (int i = 0 ; i < length ; i++) {
898 if (ne(seq1[i], seq2[length - i - 1])) {
899 return false;
900 }
901 }
902 return true;
903 }
904
905 /**
906 * True iff seq1 is a subset of seq2, when the sequences are
907 * considered as sets.
908 */
909 /* pure */ public static boolean subsetOf(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
910 if (seq1 == null) { return false; }
911 if (seq2 == null) { return false; }
912 for (int i = 0 ; i < seq1.length ; i++) {
913 if (!memberOf(seq1[i], seq2)) {
914 return false;
915 }
916 }
917 return true;
918 }
919
920 /* pure */ public static boolean subsetOf(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
921 if (seq1 == null) { return false; }
922 if (seq2 == null) { return false; }
923 for (int i = 0 ; i < seq1.length ; i++) {
924 if (!memberOf(seq1[i], seq2)) {
925 return false;
926 }
927 }
928 return true;
929 }
930
931 /**
932 * Returns true iff seq contains no duplicate elements.
933 */
934 /* pure */ public static boolean noDups(byte /*@Nullable*/ [] seq) {
935 if (seq == null) { return false; }
936 return utilMDE.ArraysMDE.noDuplicates(seq);
937 }
938
939 /**
940 * Returns true iff elt is in array arr.
941 */
942 /* pure */ public static boolean memberOf(byte elt, byte /*@Nullable*/ [] arr) {
943 if (arr == null) { return false; }
944 for (int i = 0 ; i < arr.length ; i++) {
945 if (eq(arr[i], elt)) { return true; }
946 }
947 return false;
948 }
949
950 /* pure */ public static boolean memberOf(byte elt, int /*@Nullable*/ [] arr) {
951 if (arr == null) { return false; }
952 for (int i = 0 ; i < arr.length ; i++) {
953 if (eq(arr[i], elt)) { return true; }
954 }
955 return false;
956 }
957
958 /* pure */ public static boolean memberOf(long elt, byte /*@Nullable*/ [] arr) {
959 if (arr == null) { return false; }
960 for (int i = 0 ; i < arr.length ; i++) {
961 if (eq(arr[i], elt)) { return true; }
962 }
963 return false;
964 }
965
966 /**
967 * Returns a subsequence of seq with first elements seq[start] and
968 * last element seq[end].
969 */
970 /* pure */ public static byte /*@PolyNull*/ [] slice(byte /*@PolyNull*/ [] seq, int start, int end) {
971 if (seq == null) { return null; }
972 int sliceStart = start;
973 int sliceEnd = end;
974 if (start < 0) { return new byte[] { }; }
975 if (end > seq.length-1) { return new byte[] { }; }
976 if (sliceStart > sliceEnd) { return new byte[] { }; }
977 int length = sliceEnd - sliceStart + 1;
978 return utilMDE.ArraysMDE.subarray(seq, sliceStart, length);
979 }
980
981 /* pure */ public static byte /*@PolyNull*/ [] slice(byte /*@PolyNull*/ [] seq, long start, int end) {
982 return slice(seq, (int)start, end);
983 }
984 /* pure */ public static byte /*@PolyNull*/ [] slice(byte /*@PolyNull*/ [] seq, int start, long end) {
985 return slice(seq, start, (int)end);
986 }
987 /* pure */ public static byte /*@PolyNull*/ [] slice(byte /*@PolyNull*/ [] seq, long start, long end) {
988 return slice(seq, (int)start, (int)end);
989 }
990
991 /** True iff all elements in arr equal elt.
992 *
993 * Meaning (in pseudo-FOL):
994 *
995 * forall i in { 0..arr.length-1 } : arr[i] == elt
996 *
997 */
998 /* pure */ public static boolean eltsEqual(byte /*@Nullable*/ [] arr, byte elt) {
999 if (arr == null) { return false; }
1000 for (int i = 0 ; i < arr.length ; i++) {
1001 if (ne(arr[i], elt)) { return false; }
1002 }
1003 return true;
1004 }
1005
1006 /* pure */ public static boolean eltsEqual(byte /*@Nullable*/ [] arr, int elt) {
1007 if (arr == null) { return false; }
1008 for (int i = 0 ; i < arr.length ; i++) {
1009 if (ne(arr[i], elt)) { return false; }
1010 }
1011 return true;
1012 }
1013
1014 /** True iff every element in arr does not equal elt.
1015 *
1016 * Meaning (in pseudo-FOL):
1017 *
1018 * forall i in { 0..arr.length-1 } : arr[i] != elt
1019 *
1020 */
1021 /* pure */ public static boolean eltsNotEqual(byte /*@Nullable*/ [] arr, byte elt) {
1022 if (arr == null) { return false; }
1023 for (int i = 0 ; i < arr.length ; i++) {
1024 if (eq(arr[i], elt)) { return false; }
1025 }
1026 return true;
1027 }
1028
1029 /* pure */ public static boolean eltsNotEqual(byte /*@Nullable*/ [] arr, int elt) {
1030 if (arr == null) { return false; }
1031 for (int i = 0 ; i < arr.length ; i++) {
1032 if (eq(arr[i], elt)) { return false; }
1033 }
1034 return true;
1035 }
1036
1037 /** True iff every element in arr is greater than elt.
1038 *
1039 * Meaning (in pseudo-FOL):
1040 *
1041 * forall i in { 0..arr.length-1 } : arr[i] > elt
1042 *
1043 */
1044 /* pure */ public static boolean eltsGT(byte /*@Nullable*/ [] arr, byte elt) {
1045 if (arr == null) { return false; }
1046 for (int i = 0 ; i < arr.length ; i++) {
1047 if (lte(arr[i], elt)) { return false; }
1048 }
1049 return true;
1050 }
1051
1052 /* pure */ public static boolean eltsGT(byte /*@Nullable*/ [] arr, int elt) {
1053 if (arr == null) { return false; }
1054 for (int i = 0 ; i < arr.length ; i++) {
1055 if (lte(arr[i], elt)) { return false; }
1056 }
1057 return true;
1058 }
1059
1060 /** True iff every element in arr is greater than or equal to elt.
1061 *
1062 * Meaning (in pseudo-FOL):
1063 *
1064 * forall i in { 0..arr.length-1 } : arr[i] >= elt
1065 *
1066 */
1067 /* pure */ public static boolean eltsGTE(byte /*@Nullable*/ [] arr, byte elt) {
1068 if (arr == null) { return false; }
1069 for (int i = 0 ; i < arr.length ; i++) {
1070 if (lt(arr[i], elt)) { return false; }
1071 }
1072 return true;
1073 }
1074
1075 /* pure */ public static boolean eltsGTE(byte /*@Nullable*/ [] arr, int elt) {
1076 if (arr == null) { return false; }
1077 for (int i = 0 ; i < arr.length ; i++) {
1078 if (lt(arr[i], elt)) { return false; }
1079 }
1080 return true;
1081 }
1082
1083 /** True iff every element in arr is less than elt.
1084 *
1085 * Meaning (in pseudo-FOL):
1086 *
1087 * forall i in { 0..arr.length-1 } : arr[i] < elt
1088 *
1089 */
1090 /* pure */ public static boolean eltsLT(byte /*@Nullable*/ [] arr, byte elt) {
1091 if (arr == null) { return false; }
1092 for (int i = 0 ; i < arr.length ; i++) {
1093 if (gte(arr[i], elt)) { return false; }
1094 }
1095 return true;
1096 }
1097
1098 /* pure */ public static boolean eltsLT(byte /*@Nullable*/ [] arr, int elt) {
1099 if (arr == null) { return false; }
1100 for (int i = 0 ; i < arr.length ; i++) {
1101 if (gte(arr[i], elt)) { return false; }
1102 }
1103 return true;
1104 }
1105
1106 /** True iff every element in arr is less than or equal to elt.
1107 *
1108 * Meaning (in pseudo-FOL):
1109 *
1110 * forall i in { 0..arr.length-1 } : arr[i] <= elt
1111 *
1112 */
1113 /* pure */ public static boolean eltsLTE(byte /*@Nullable*/ [] arr, byte elt) {
1114 if (arr == null) { return false; }
1115 for (int i = 0 ; i < arr.length ; i++) {
1116 if (gt(arr[i], elt)) { return false; }
1117 }
1118 return true;
1119 }
1120
1121 /* pure */ public static boolean eltsLTE(byte /*@Nullable*/ [] arr, int elt) {
1122 if (arr == null) { return false; }
1123 for (int i = 0 ; i < arr.length ; i++) {
1124 if (gt(arr[i], elt)) { return false; }
1125 }
1126 return true;
1127 }
1128
1129 /** True iff seq1 and seq2 have the same length, and every seq1[i] == seq2[i].
1130 *
1131 * Meaning (in pseudo-FOL):
1132 *
1133 * /\ seq1.length == se2.length
1134 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[i]
1135 *
1136 */
1137
1138 /* pure */ public static boolean pairwiseEqual(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1139 if (! sameLength(seq1, seq2)) { return false; }
1140 assert seq1 != null && seq2 != null; // because sameLength() = true
1141 for (int i = 0 ; i < seq1.length ; i++) {
1142 if (ne(seq1[i], seq2[i])) {
1143 return false;
1144 }
1145 }
1146 return true;
1147 }
1148
1149 /* pure */ public static boolean pairwiseEqual(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1150 if (! sameLength(seq1, seq2)) { return false; }
1151 assert seq1 != null && seq2 != null; // because sameLength() = true
1152 for (int i = 0 ; i < seq1.length ; i++) {
1153 if (ne(seq1[i], seq2[i])) {
1154 return false;
1155 }
1156 }
1157 return true;
1158 }
1159
1160 /** True iff seq1 and seq2 have the same length, and every seq1[i] != seq2[i].
1161 *
1162 * Meaning (in pseudo-FOL):
1163 *
1164 * /\ seq1.length == se2.length
1165 * /\ forall i in { 0..seq1.length-1 } : seq1[i] != seq2[i]
1166 *
1167 */
1168 /* pure */ public static boolean pairwiseNotEqual(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1169 if (! sameLength(seq1, seq2)) { return false; }
1170 assert seq1 != null && seq2 != null; // because sameLength() = true
1171 for (int i = 0 ; i < seq1.length ; i++) {
1172 if (eq(seq1[i], seq2[i])) {
1173 return false;
1174 }
1175 }
1176 return true;
1177 }
1178
1179 /* pure */ public static boolean pairwiseNotEqual(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1180 if (! sameLength(seq1, seq2)) { return false; }
1181 assert seq1 != null && seq2 != null; // because sameLength() = true
1182 for (int i = 0 ; i < seq1.length ; i++) {
1183 if (eq(seq1[i], seq2[i])) {
1184 return false;
1185 }
1186 }
1187 return true;
1188 }
1189
1190 /** True iff seq1 and seq2 have the same length, and every seq1[i] < seq2[i].
1191 *
1192 * Meaning (in pseudo-FOL):
1193 *
1194 * /\ seq1.length == se2.length
1195 * /\ forall i in { 0..seq1.length-1 } : seq1[i] < seq2[i]
1196 *
1197 */
1198 /* pure */ public static boolean pairwiseLT(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1199 if (! sameLength(seq1, seq2)) { return false; }
1200 assert seq1 != null && seq2 != null; // because sameLength() = true
1201 for (int i = 0 ; i < seq1.length ; i++) {
1202 if (gte(seq1[i], seq2[i])) {
1203 return false;
1204 }
1205 }
1206 return true;
1207 }
1208
1209 /* pure */ public static boolean pairwiseLT(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1210 if (! sameLength(seq1, seq2)) { return false; }
1211 assert seq1 != null && seq2 != null; // because sameLength() = true
1212 for (int i = 0 ; i < seq1.length ; i++) {
1213 if (gte(seq1[i], seq2[i])) {
1214 return false;
1215 }
1216 }
1217 return true;
1218 }
1219
1220 /** True iff seq1 and seq2 have the same length, and every seq1[i] <= seq2[i].
1221 * Meaning (in pseudo-FOL):
1222 *
1223 * /\ seq1.length == se2.length
1224 * /\ forall i in { 0..seq1.length-1 } : seq1[i] <= seq2[i]
1225 *
1226 */
1227 /* pure */ public static boolean pairwiseLTE(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1228 if (! sameLength(seq1, seq2)) { return false; }
1229 assert seq1 != null && seq2 != null; // because sameLength() = true
1230 for (int i = 0 ; i < seq1.length ; i++) {
1231 if (gt(seq1[i], seq2[i])) {
1232 return false;
1233 }
1234 }
1235 return true;
1236 }
1237
1238 /* pure */ public static boolean pairwiseLTE(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1239 if (! sameLength(seq1, seq2)) { return false; }
1240 assert seq1 != null && seq2 != null; // because sameLength() = true
1241 for (int i = 0 ; i < seq1.length ; i++) {
1242 if (gt(seq1[i], seq2[i])) {
1243 return false;
1244 }
1245 }
1246 return true;
1247 }
1248
1249 /** True iff seq1 and seq2 have the same length, and every seq1[i] > seq2[i].
1250 * Meaning (in pseudo-FOL):
1251 *
1252 * /\ seq1.length == se2.length
1253 * /\ forall i in { 0..seq1.length-1 } : seq1[i] > seq2[i]
1254 *
1255 */
1256 /* pure */ public static boolean pairwiseGT(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1257 if (! sameLength(seq1, seq2)) { return false; }
1258 assert seq1 != null && seq2 != null; // because sameLength() = true
1259 for (int i = 0 ; i < seq1.length ; i++) {
1260 if (lte(seq1[i], seq2[i])) {
1261 return false;
1262 }
1263 }
1264 return true;
1265 }
1266
1267 /* pure */ public static boolean pairwiseGT(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1268 if (! sameLength(seq1, seq2)) { return false; }
1269 assert seq1 != null && seq2 != null; // because sameLength() = true
1270 for (int i = 0 ; i < seq1.length ; i++) {
1271 if (lte(seq1[i], seq2[i])) {
1272 return false;
1273 }
1274 }
1275 return true;
1276 }
1277
1278 /** True iff seq1 and seq2 have the same length, and every seq1[i] >= seq2[i].
1279 * Meaning (in pseudo-FOL):
1280 *
1281 * /\ seq1.length == se2.length
1282 * /\ forall i in { 0..seq1.length-1 } : seq1[i] >= seq2[i]
1283 *
1284 */
1285 /* pure */ public static boolean pairwiseGTE(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1286 if (! sameLength(seq1, seq2)) { return false; }
1287 assert seq1 != null && seq2 != null; // because sameLength() = true
1288 for (int i = 0 ; i < seq1.length ; i++) {
1289 if (lt(seq1[i], seq2[i])) {
1290 return false;
1291 }
1292 }
1293 return true;
1294 }
1295
1296 /* pure */ public static boolean pairwiseGTE(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1297 if (! sameLength(seq1, seq2)) { return false; }
1298 assert seq1 != null && seq2 != null; // because sameLength() = true
1299 for (int i = 0 ; i < seq1.length ; i++) {
1300 if (lt(seq1[i], seq2[i])) {
1301 return false;
1302 }
1303 }
1304 return true;
1305 }
1306
1307 /**
1308 * Returns true iff seq1 is lexically equal to seq2.
1309 * For equality, "lexically" and "pairwise" are the same.
1310 */
1311 /* pure */ public static boolean lexEqual(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1312 if (seq1 == null) { return false; }
1313 if (seq2 == null) { return false; }
1314 return pairwiseEqual(seq1, seq2);
1315 }
1316
1317 /* pure */ public static boolean lexEqual(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1318 if (seq1 == null) { return false; }
1319 if (seq2 == null) { return false; }
1320 return pairwiseEqual(seq1, seq2);
1321 }
1322
1323 /**
1324 * Returns true iff seq1 is lexically not equal to seq2.
1325 */
1326 /* pure */ public static boolean lexNotEqual(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1327 if (seq1 == null) { return false; }
1328 if (seq2 == null) { return false; }
1329 return !lexEqual(seq1, seq2);
1330 }
1331
1332 /* pure */ public static boolean lexNotEqual(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1333 if (seq1 == null) { return false; }
1334 if (seq2 == null) { return false; }
1335 return !lexEqual(seq1, seq2);
1336 }
1337
1338 /**
1339 * Returns true iff seq1 is lexically < seq2.
1340 */
1341 /* pure */ public static boolean lexLT(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1342 if (seq1 == null) { return false; }
1343 if (seq2 == null) { return false; }
1344 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1345 for (int i = 0 ; i < minlength ; i++) {
1346 if (gt(seq1[i], seq2[i])) {
1347 return false;
1348 } else if (lt(seq1[i], seq2[i])) {
1349 return true;
1350 }
1351 }
1352 if (seq1.length >= seq2.length) {
1353 return false;
1354 }
1355 return true;
1356 }
1357
1358 /* pure */ public static boolean lexLT(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1359 if (seq1 == null) { return false; }
1360 if (seq2 == null) { return false; }
1361 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1362 for (int i = 0 ; i < minlength ; i++) {
1363 if (gt(seq1[i], seq2[i])) {
1364 return false;
1365 } else if (lt(seq1[i], seq2[i])) {
1366 return true;
1367 }
1368 }
1369 if (seq1.length >= seq2.length) {
1370 return false;
1371 }
1372 return true;
1373 }
1374
1375 /**
1376 * Returns true iff seq1 is lexically <= to seq2.
1377 */
1378 /* pure */ public static boolean lexLTE(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1379 if (seq1 == null) { return false; }
1380 if (seq2 == null) { return false; }
1381 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1382 for (int i = 0 ; i < minlength ; i++) {
1383 if (gt(seq1[i], seq2[i])) {
1384 return false;
1385 } else if (lt(seq1[i], seq2[i])) {
1386 return true;
1387 }
1388 }
1389 if (seq1.length > seq2.length) {
1390 return false;
1391 }
1392 return true;
1393 }
1394
1395 /* pure */ public static boolean lexLTE(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1396 if (seq1 == null) { return false; }
1397 if (seq2 == null) { return false; }
1398 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1399 for (int i = 0 ; i < minlength ; i++) {
1400 if (gt(seq1[i], seq2[i])) {
1401 return false;
1402 } else if (lt(seq1[i], seq2[i])) {
1403 return true;
1404 }
1405 }
1406 if (seq1.length > seq2.length) {
1407 return false;
1408 }
1409 return true;
1410 }
1411
1412 /**
1413 * Returns true iff seq1 is lexically > to seq2.
1414 */
1415 /* pure */ public static boolean lexGT(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1416 if (seq1 == null) { return false; }
1417 if (seq2 == null) { return false; }
1418 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1419 for (int i = 0 ; i < minlength ; i++) {
1420 if (lt(seq1[i], seq2[i])) {
1421 return false;
1422 } else if (gt(seq1[i], seq2[i])) {
1423 return true;
1424 }
1425 }
1426 if (seq1.length <= seq2.length) {
1427 return false;
1428 }
1429 return true;
1430 }
1431
1432 /* pure */ public static boolean lexGT(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1433 if (seq1 == null) { return false; }
1434 if (seq2 == null) { return false; }
1435 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1436 for (int i = 0 ; i < minlength ; i++) {
1437 if (lt(seq1[i], seq2[i])) {
1438 return false;
1439 } else if (gt(seq1[i], seq2[i])) {
1440 return true;
1441 }
1442 }
1443 if (seq1.length <= seq2.length) {
1444 return false;
1445 }
1446 return true;
1447 }
1448
1449 /**
1450 * Returns true iff seq1 is lexically >= to seq2.
1451 */
1452 /* pure */ public static boolean lexGTE(byte /*@Nullable*/ [] seq1, byte /*@Nullable*/ [] seq2) {
1453 if (seq1 == null) { return false; }
1454 if (seq2 == null) { return false; }
1455 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1456 for (int i = 0 ; i < minlength ; i++) {
1457 if (lt(seq1[i], seq2[i])) {
1458 return false;
1459 } else if (gt(seq1[i], seq2[i])) {
1460 return true;
1461 }
1462 }
1463 if (seq1.length < seq2.length) {
1464 return false;
1465 }
1466 return true;
1467 }
1468
1469 /* pure */ public static boolean lexGTE(byte /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
1470 if (seq1 == null) { return false; }
1471 if (seq2 == null) { return false; }
1472 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
1473 for (int i = 0 ; i < minlength ; i++) {
1474 if (lt(seq1[i], seq2[i])) {
1475 return false;
1476 } else if (gt(seq1[i], seq2[i])) {
1477 return true;
1478 }
1479 }
1480 if (seq1.length < seq2.length) {
1481 return false;
1482 }
1483 return true;
1484 }
1485
1486 /** True iff for all applicable i, every seq[i] == seq[i+1].
1487 *
1488 * Meaning (in pseudo-FOL):
1489 *
1490 * forall i in { 0..seq.length-2 } : seq[i] == seq[i+1]
1491 *
1492 */
1493 /* pure */ public static boolean eltwiseEqual(byte /*@Nullable*/ [] seq) {
1494 if (seq == null) { return false; }
1495 for (int i = 0 ; i < seq.length ; i++) {
1496 if (i < seq.length-1) {
1497 if (ne(seq[i], seq[i+1])) {
1498 return false;
1499 }
1500 }
1501 }
1502 return true;
1503 }
1504
1505 /** True iff for all applicable i, every seq[i] != seq[i+1].
1506 *
1507 * Meaning (in pseudo-FOL):
1508 *
1509 * forall i in { 0..seq.length-2 } : seq[i] != seq[i+1]
1510 *
1511 */
1512 /* pure */ public static boolean eltwiseNotEqual(byte /*@Nullable*/ [] seq) {
1513 if (seq == null) { return false; }
1514 for (int i = 0 ; i < seq.length ; i++) {
1515 if (i < seq.length-1) {
1516 if (eq(seq[i], seq[i+1])) {
1517 return false;
1518 }
1519 }
1520 }
1521 return true;
1522 }
1523
1524 /** True iff for all applicable i, every seq[i] < seq[i+1].
1525 *
1526 * Meaning (in pseudo-FOL):
1527 *
1528 * forall i in { 0..seq.length-2 } : seq[i] < seq[i+1]
1529 *
1530 */
1531 /* pure */ public static boolean eltwiseLT(byte /*@Nullable*/ [] seq) {
1532 if (seq == null) { return false; }
1533 for (int i = 0 ; i < seq.length ; i++) {
1534 if (i < seq.length-1) {
1535 if (gte(seq[i], seq[i+1])) {
1536 return false;
1537 }
1538 }
1539 }
1540 return true;
1541 }
1542
1543 /** True iff for all applicable i, every seq[i] <= seq[i+1].
1544 *
1545 * Meaning (in pseudo-FOL):
1546 *
1547 * forall i in { 0..seq.length-2 } : seq[i] <= seq[i+1]
1548 *
1549 */
1550 /* pure */ public static boolean eltwiseLTE(byte /*@Nullable*/ [] seq) {
1551 if (seq == null) { return false; }
1552 for (int i = 0 ; i < seq.length ; i++) {
1553 if (i < seq.length-1) {
1554 if (gt(seq[i], seq[i+1])) {
1555 return false;
1556 }
1557 }
1558 }
1559 return true;
1560 }
1561
1562 /** True iff for all applicable i, every seq[i] > seq[i+1].
1563 *
1564 * Meaning (in pseudo-FOL):
1565 *
1566 * forall i in { 0..seq.length-2 } : seq[i] > seq[i+1]
1567 *
1568 */
1569 /* pure */ public static boolean eltwiseGT(byte /*@Nullable*/ [] seq) {
1570 if (seq == null) { return false; }
1571 for (int i = 0 ; i < seq.length ; i++) {
1572 if (i < seq.length-1) {
1573 if (lte(seq[i], seq[i+1])) {
1574 return false;
1575 }
1576 }
1577 }
1578 return true;
1579 }
1580
1581 /** True iff for all applicable i, every seq[i] >= seq[i+1].
1582 *
1583 * Meaning (in pseudo-FOL):
1584 *
1585 * forall i in { 0..seq.length-2 } : seq[i] >= seq[i+1]
1586 *
1587 */
1588 /* pure */ public static boolean eltwiseGTE(byte /*@Nullable*/ [] seq) {
1589 if (seq == null) { return false; }
1590 for (int i = 0 ; i < seq.length ; i++) {
1591 if (i < seq.length-1) {
1592 if (lt(seq[i], seq[i+1])) {
1593 return false;
1594 }
1595 }
1596 }
1597 return true;
1598 }
1599
1600 /** True iff for all applicable i, every seq[i] == i.
1601 *
1602 * Meaning (in pseudo-FOL):
1603 *
1604 * forall i in { 0..seq.length-1 } : seq[i] == i
1605 *
1606 */
1607 /* pure */ public static boolean eltsEqualIndex(byte /*@Nullable*/ [] seq) {
1608 if (seq == null) { return false; }
1609 for (int i = 0 ; i < seq.length ; i++) {
1610 if (ne(seq[i], i)) {
1611 return false;
1612 }
1613 }
1614 return true;
1615 }
1616
1617 /** True iff for all applicable i, every seq[i] != i.
1618 *
1619 * Meaning (in pseudo-FOL):
1620 *
1621 * forall i in { 0..seq.length-1 } : seq[i] != i
1622 *
1623 */
1624 /* pure */ public static boolean eltsNotEqualIndex(byte /*@Nullable*/ [] seq) {
1625 if (seq == null) { return false; }
1626 for (int i = 0 ; i < seq.length ; i++) {
1627 if (eq(seq[i], i)) {
1628 return false;
1629 }
1630 }
1631 return true;
1632 }
1633
1634 /** True iff for all applicable i, every seq[i] < i.
1635 *
1636 * Meaning (in pseudo-FOL):
1637 *
1638 * forall i in { 0..seq.length-1 } : seq[i] < i
1639 *
1640 */
1641 /* pure */ public static boolean eltsLtIndex(byte /*@Nullable*/ [] seq) {
1642 if (seq == null) { return false; }
1643 for (int i = 0 ; i < seq.length ; i++) {
1644 if (gte(seq[i], i)) {
1645 return false;
1646 }
1647 }
1648 return true;
1649 }
1650
1651 /** True iff for all applicable i, every seq[i] <= i.
1652 *
1653 * Meaning (in pseudo-FOL):
1654 *
1655 * forall i in { 0..seq.length-1 } : seq[i] <= i
1656 *
1657 */
1658 /* pure */ public static boolean eltsLteIndex(byte /*@Nullable*/ [] seq) {
1659 if (seq == null) { return false; }
1660 for (int i = 0 ; i < seq.length ; i++) {
1661 if (gt(seq[i], i)) {
1662 return false;
1663 }
1664 }
1665 return true;
1666 }
1667
1668 /** True iff for all applicable i, every seq[i] > i.
1669 *
1670 * Meaning (in pseudo-FOL):
1671 *
1672 * forall i in { 0..seq.length-1 } : seq[i] > i
1673 *
1674 */
1675 /* pure */ public static boolean eltsGtIndex(byte /*@Nullable*/ [] seq) {
1676 if (seq == null) { return false; }
1677 for (int i = 0 ; i < seq.length ; i++) {
1678 if (lte(seq[i], i)) {
1679 return false;
1680 }
1681 }
1682 return true;
1683 }
1684
1685 /** True iff for all applicable i, every seq[i] >= i.
1686 *
1687 * Meaning (in pseudo-FOL):
1688 *
1689 * forall i in { 0..seq.length-1 } : seq[i] >= i
1690 *
1691 */
1692 /* pure */ public static boolean eltsGteIndex(byte /*@Nullable*/ [] seq) {
1693 if (seq == null) { return false; }
1694 for (int i = 0 ; i < seq.length ; i++) {
1695 if (lt(seq[i], i)) {
1696 return false;
1697 }
1698 }
1699 return true;
1700 }
1701
1702 /// Deferencing (accessing) fields
1703
1704 /**
1705 * collectbyte accepts an object and a list of fields (one of which is
1706 * of array type, and the rest of which are not), and produces an array in
1707 * which the original object has had the given fields accessed.
1708 *
1709 * Daikon creates invariants over "variables" such as the following.
1710 *
1711 * x.arr[].z The result of collecting all elements y.z for all y's
1712 * in array x.arr.
1713 * arr[].y.z The result of collecting all elements x.y.z for all x's
1714 * in array arr.
1715 * x.y.z[] The result of collecting all elements in array x.y.z[]
1716 *
1717 * The collectbyte() method does this collecting work.
1718 *
1719 * Given an object (x, arr, or x, correspondingly, in the above examples)
1720 * and a "field string" (arr.z, y.z, or y.z, correspondingly, in the
1721 * above example), the collect method collects the elements the result
1722 * from following the fields, one of which is assumed to be an array.
1723 *
1724 * requires: fieldStr.length() > 0 and object != null
1725 * requires: fieldStr contains only field names, no "[]" strings.
1726 *
1727 * requires: the method only works for field sequences with exactly
1728 * one field representing an array. For example, the collection
1729 * a[].b[].c will fail.
1730 *
1731 * If the resulting collection is of non-primitive type, then collect
1732 * returns an array of type Object[].
1733 *
1734 * Returns null if any array or field access causes an exception.
1735 */
1736 /* pure */ public static byte /*@Nullable*/ [] collectbyte (Object object, String fieldStr) {
1737
1738 if (object == null) { return null; }
1739 if (fieldStr == null) { return null; }
1740
1741 //assert fieldStr != null && !"".equals(fieldStr);
1742 String[] fieldNames = fieldStr.split("\\.");
1743 byte[] retval = collectbyte (object, fieldNames, 0);
1744 //System.err.println("%%% fieldArray returned: " + utilMDE.ArraysMDE.toString(retval));
1745 return retval;
1746 }
1747
1748 /** Helper method for collectbyte(Object, String).
1749 * Operates on the fields specified in fields[fieldsStartIdx..].
1750 * @see collectbyte(Object, String)
1751 */
1752 /* pure */ private static byte /*@Nullable*/ [] collectbyte (Object object,
1753 String[] fields, int fieldsStartIdx) {
1754
1755 if (object == null) { return null; }
1756 assert (fields != null);
1757 assert (fieldsStartIdx >= 0 && fieldsStartIdx < fields.length);
1758
1759 Object fieldObj = null;
1760 try {
1761 Field field = (object instanceof java.lang.Class<?>)
1762 ? ((Class<?>)object).getDeclaredField(fields[fieldsStartIdx])
1763 : object.getClass().getDeclaredField(fields[fieldsStartIdx]);
1764 field.setAccessible(true);
1765 // Class cls = field.getType();
1766 fieldObj = field.get(object);
1767 //System.out.println("***fieldObj="+fieldObj);
1768
1769 } catch (Exception e) {
1770 return null;
1771
1772 }
1773
1774 if (fieldObj == null) {
1775 return null;
1776 }
1777
1778 // base case: just accessed the last field
1779 if (fields.length - 1 == fieldsStartIdx) {
1780
1781 if (fieldObj.getClass().isArray()) {
1782 // last field is an array
1783 return (byte[])fieldObj;
1784 } else {
1785 // This hack should be removed in favor of, at "oneEltArray = ..."
1786 // below, calling a version of collectbyte_field that throws an
1787 // error. Then, this case becomes a run-time error. -MDE
1788
1789 // Just one element; return a one-element array.
1790 //assert cls.equals(Byte.TYPE);
1791 return new byte[] { ((Byte)fieldObj).byteValue() };
1792 }
1793 } else {
1794 // recursive case: more fields to access after this one
1795
1796 if (daikon.ProglangType.list_implementors.contains(fieldObj.getClass().getName())) {
1797
1798 java.util.AbstractCollection<?> collection = (java.util.AbstractCollection<?>)fieldObj;
1799 byte[] intermediate = new byte[collection.size()];
1800 int index = 0;
1801 for (Iterator<?> i = collection.iterator() ; i.hasNext() ; ) {
1802 byte[] oneEltArray = collectbyte (i.next(), fields, fieldsStartIdx + 1);
1803 //assert oneEltArray.length == 1;
1804 intermediate[index++] = oneEltArray[0];
1805 }
1806 return intermediate;
1807 } else if (fieldObj.getClass().isArray()) {
1808
1809 // collect elements across array
1810 byte[] intermediate = new byte[Array.getLength(fieldObj)];
1811 for (int i = 0 ; i < intermediate.length ; i++) {
1812 byte[] oneEltArray = collectbyte (Array.get(fieldObj, i),
1813 fields, fieldsStartIdx + 1);
1814 //assert oneEltArray.length == 1;
1815 intermediate[i] = oneEltArray[0];
1816 }
1817 return intermediate;
1818 } else {
1819
1820 return collectbyte (fieldObj, fields, fieldsStartIdx + 1);
1821 }
1822 }
1823 }
1824
1825 // Returns the results of dereferencing the fields specified in
1826 // fields[fieldsStartIdx..] for 'object'.
1827 // Returns a default value if any field access causes an exception.
1828 /* pure */ public static byte collectbyte_field (Object object, String fieldStr) {
1829
1830 if (object == null) { return Byte.MAX_VALUE; } // return default value
1831 if (fieldStr == null) { return Byte.MAX_VALUE; } // return default value
1832
1833 String[] fieldNames = fieldStr.split("\\.");
1834
1835 // Holds the intermediate (and final) result
1836 Object fieldObj = object;
1837
1838 for (int i = 0 ; i < fieldNames.length ; i++) {
1839
1840 String fieldName = fieldNames[i];
1841
1842 try {
1843 Field field =
1844 (fieldObj instanceof java.lang.Class<?>)
1845 ? ((Class<?>)fieldObj).getDeclaredField(fieldName)
1846 : fieldObj.getClass().getDeclaredField(fieldName);
1847 field.setAccessible(true);
1848 fieldObj = field.get(fieldObj);
1849
1850 } catch (Exception e) {
1851 return Byte.MAX_VALUE; // return default value
1852
1853 }
1854
1855 }
1856
1857 return ((Byte)fieldObj).byteValue();
1858 }
1859
1860 ///////////////////////////////////////////////////////////////////////////
1861 /// Methods for "char" (from QuantBody.java.jpp)
1862 ///
1863
1864 /** Returns the ith element of the array or collection argument.
1865 * If the argument is null or not an array or collection, returns a
1866 * default value (Character.MAX_VALUE).
1867 **/
1868 /* pure */ public static char getElement_char (Object o, long i) {
1869 if (o == null) { return Character.MAX_VALUE; } // return default value
1870 java.lang.Class<?> c = o.getClass();
1871 if (c.isArray()) {
1872 return java.lang.reflect.Array.getChar (o, (int)i);
1873 } else if (o instanceof java.util.AbstractCollection<?>) {
1874 return java.lang.reflect.Array.getChar (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
1875 } else {
1876 return Character.MAX_VALUE; // return default value
1877 }
1878 }
1879
1880 /* pure */ public static char getElement_char (char[] arr, long i) {
1881 if (arr == null) { return Character.MAX_VALUE; } // return default value
1882 return arr[(int)i];
1883 }
1884
1885 private static boolean eq(char x, char y) {
1886 return (x == y);
1887 }
1888
1889 private static boolean ne(char x, char y) {
1890 return x != y;
1891 }
1892
1893 private static boolean lt(char x, char y) {
1894 return x < y;
1895 }
1896
1897 private static boolean lte(char x, char y) {
1898 return x <= y;
1899 }
1900
1901 private static boolean gt(char x, char y) {
1902 return x > y;
1903 }
1904
1905 private static boolean gte(char x, char y) {
1906 return x >= y;
1907 }
1908
1909 /** True iff both sequences are non-null and have the same length. */
1910 /* pure */ public static boolean sameLength(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
1911 return ((seq1 != null)
1912 && (seq2 != null)
1913 && seq1.length == seq2.length);
1914 }
1915
1916 /**
1917 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
1918 * If either array is null, returns null.
1919 * If either array is empty, returns only those elements in the other array.
1920 * If both arrays are empty, returns a new empty array.
1921 */
1922 /* pure */ public static char /*@PolyNull*/ [] concat(char /*@PolyNull*/ [] seq1, char /*@PolyNull*/ [] seq2) {
1923 if (seq1 == null) { return null; }
1924 if (seq2 == null) { return null; }
1925 return utilMDE.ArraysMDE.concat(seq1, seq2);
1926 }
1927
1928 /**
1929 * Returns an array that is equivalent to the set union of seq1 and seq2.
1930 * This method gives no assurances about the order or repetition of elements:
1931 * elements may be repeated, and their order may be different from the
1932 * order of elements in seq1 and seq2.
1933 */
1934 /* pure */ public static char /*@PolyNull*/ [] union(char /*@PolyNull*/ [] seq1, char /*@PolyNull*/ [] seq2) {
1935 if (seq1 == null) { return null; }
1936 if (seq2 == null) { return null; }
1937 return concat(seq1, seq2);
1938 }
1939
1940 /**
1941 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
1942 * This method gives no assurances about the order or repetition of elements:
1943 * elements may be repeated, and their order may be different from the
1944 * order of elements in seq1 and seq2.
1945 */
1946 /* pure */ public static char /*@PolyNull*/ [] intersection(char /*@PolyNull*/ [] seq1, char /*@PolyNull*/ [] seq2) {
1947 if (seq1 == null) { return null; }
1948 if (seq2 == null) { return null; }
1949 char[] intermediate = new char[Math.min(seq1.length, seq2.length)];
1950 int length = 0;
1951 for (int i = 0 ; i < seq1.length ; i++) {
1952 if (memberOf(seq1[i], seq2) ) {
1953 intermediate[length++] = seq1[i];
1954 }
1955 }
1956 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
1957 }
1958
1959 /**
1960 * Returns an array that is equivalent to the set difference of seq1 and seq2.
1961 * This method gives no assurances about the order or repetition of elements:
1962 * elements may be repeated, and their order may be different from the
1963 * order of elements in seq1 and seq2.
1964 */
1965 /* pure */ public static char /*@PolyNull*/ [] setDiff(char /*@PolyNull*/ [] seq1, char /*@PolyNull*/ [] seq2) {
1966 if (seq1 == null) { return null; }
1967 if (seq2 == null) { return null; }
1968 char[] intermediate = new char[seq1.length];
1969 int length = 0;
1970 for (int i = 0 ; i < seq1.length ; i++) {
1971 if (!memberOf(seq1[i], seq2)) {
1972 intermediate[length++] = seq1[i];
1973 }
1974 }
1975 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
1976 }
1977
1978 /**
1979 * Retuns true iff seq1 and seq2 are equal when considered as sets.
1980 */
1981 /* pure */ public static boolean setEqual(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
1982 if (seq1 == null) { return false; }
1983 if (seq2 == null) { return false; }
1984 for (int i = 0; i < seq1.length ; i++) {
1985 if (!memberOf(seq1[i], seq2) ) {
1986 return false;
1987 }
1988 }
1989 for (int i = 0; i < seq2.length ; i++) {
1990 if (!memberOf(seq2[i], seq1) ) {
1991 return false;
1992 }
1993 }
1994 return true;
1995 }
1996
1997 /** True iff seq1 is the reverse of seq2.
1998 *
1999 * Meaning (in pseudo-FOL):
2000 *
2001 * <pre>
2002 * /\ seq1.length == seq2.length
2003 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
2004 * </pre>
2005 *
2006 */
2007 /* pure */ public static boolean isReverse(char[] seq1, char[] seq2) {
2008 if (! sameLength(seq1, seq2)) { return false; }
2009 assert seq1 != null && seq2 != null; // because sameLength() = true
2010 int length = seq1.length;
2011 for (int i = 0 ; i < length ; i++) {
2012 if (ne(seq1[i], seq2[length - i - 1])) {
2013 return false;
2014 }
2015 }
2016 return true;
2017 }
2018
2019 /**
2020 * True iff seq1 is a subset of seq2, when the sequences are
2021 * considered as sets.
2022 */
2023 /* pure */ public static boolean subsetOf(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2024 if (seq1 == null) { return false; }
2025 if (seq2 == null) { return false; }
2026 for (int i = 0 ; i < seq1.length ; i++) {
2027 if (!memberOf(seq1[i], seq2)) {
2028 return false;
2029 }
2030 }
2031 return true;
2032 }
2033
2034 /**
2035 * Returns true iff seq contains no duplicate elements.
2036 */
2037 /* pure */ public static boolean noDups(char /*@Nullable*/ [] seq) {
2038 if (seq == null) { return false; }
2039 return utilMDE.ArraysMDE.noDuplicates(seq);
2040 }
2041
2042 /**
2043 * Returns true iff elt is in array arr.
2044 */
2045 /* pure */ public static boolean memberOf(char elt, char /*@Nullable*/ [] arr) {
2046 if (arr == null) { return false; }
2047 for (int i = 0 ; i < arr.length ; i++) {
2048 if (eq(arr[i], elt)) { return true; }
2049 }
2050 return false;
2051 }
2052
2053 /**
2054 * Returns a subsequence of seq with first elements seq[start] and
2055 * last element seq[end].
2056 */
2057 /* pure */ public static char /*@PolyNull*/ [] slice(char /*@PolyNull*/ [] seq, int start, int end) {
2058 if (seq == null) { return null; }
2059 int sliceStart = start;
2060 int sliceEnd = end;
2061 if (start < 0) { return new char[] { }; }
2062 if (end > seq.length-1) { return new char[] { }; }
2063 if (sliceStart > sliceEnd) { return new char[] { }; }
2064 int length = sliceEnd - sliceStart + 1;
2065 return utilMDE.ArraysMDE.subarray(seq, sliceStart, length);
2066 }
2067
2068 /* pure */ public static char /*@PolyNull*/ [] slice(char /*@PolyNull*/ [] seq, long start, int end) {
2069 return slice(seq, (int)start, end);
2070 }
2071 /* pure */ public static char /*@PolyNull*/ [] slice(char /*@PolyNull*/ [] seq, int start, long end) {
2072 return slice(seq, start, (int)end);
2073 }
2074 /* pure */ public static char /*@PolyNull*/ [] slice(char /*@PolyNull*/ [] seq, long start, long end) {
2075 return slice(seq, (int)start, (int)end);
2076 }
2077
2078 /** True iff all elements in arr equal elt.
2079 *
2080 * Meaning (in pseudo-FOL):
2081 *
2082 * forall i in { 0..arr.length-1 } : arr[i] == elt
2083 *
2084 */
2085 /* pure */ public static boolean eltsEqual(char /*@Nullable*/ [] arr, char elt) {
2086 if (arr == null) { return false; }
2087 for (int i = 0 ; i < arr.length ; i++) {
2088 if (ne(arr[i], elt)) { return false; }
2089 }
2090 return true;
2091 }
2092
2093 /** True iff every element in arr does not equal elt.
2094 *
2095 * Meaning (in pseudo-FOL):
2096 *
2097 * forall i in { 0..arr.length-1 } : arr[i] != elt
2098 *
2099 */
2100 /* pure */ public static boolean eltsNotEqual(char /*@Nullable*/ [] arr, char elt) {
2101 if (arr == null) { return false; }
2102 for (int i = 0 ; i < arr.length ; i++) {
2103 if (eq(arr[i], elt)) { return false; }
2104 }
2105 return true;
2106 }
2107
2108 /** True iff every element in arr is greater than elt.
2109 *
2110 * Meaning (in pseudo-FOL):
2111 *
2112 * forall i in { 0..arr.length-1 } : arr[i] > elt
2113 *
2114 */
2115 /* pure */ public static boolean eltsGT(char /*@Nullable*/ [] arr, char elt) {
2116 if (arr == null) { return false; }
2117 for (int i = 0 ; i < arr.length ; i++) {
2118 if (lte(arr[i], elt)) { return false; }
2119 }
2120 return true;
2121 }
2122
2123 /** True iff every element in arr is greater than or equal to elt.
2124 *
2125 * Meaning (in pseudo-FOL):
2126 *
2127 * forall i in { 0..arr.length-1 } : arr[i] >= elt
2128 *
2129 */
2130 /* pure */ public static boolean eltsGTE(char /*@Nullable*/ [] arr, char elt) {
2131 if (arr == null) { return false; }
2132 for (int i = 0 ; i < arr.length ; i++) {
2133 if (lt(arr[i], elt)) { return false; }
2134 }
2135 return true;
2136 }
2137
2138 /** True iff every element in arr is less than elt.
2139 *
2140 * Meaning (in pseudo-FOL):
2141 *
2142 * forall i in { 0..arr.length-1 } : arr[i] < elt
2143 *
2144 */
2145 /* pure */ public static boolean eltsLT(char /*@Nullable*/ [] arr, char elt) {
2146 if (arr == null) { return false; }
2147 for (int i = 0 ; i < arr.length ; i++) {
2148 if (gte(arr[i], elt)) { return false; }
2149 }
2150 return true;
2151 }
2152
2153 /** True iff every element in arr is less than or equal to elt.
2154 *
2155 * Meaning (in pseudo-FOL):
2156 *
2157 * forall i in { 0..arr.length-1 } : arr[i] <= elt
2158 *
2159 */
2160 /* pure */ public static boolean eltsLTE(char /*@Nullable*/ [] arr, char elt) {
2161 if (arr == null) { return false; }
2162 for (int i = 0 ; i < arr.length ; i++) {
2163 if (gt(arr[i], elt)) { return false; }
2164 }
2165 return true;
2166 }
2167
2168 /** True iff seq1 and seq2 have the same length, and every seq1[i] == seq2[i].
2169 *
2170 * Meaning (in pseudo-FOL):
2171 *
2172 * /\ seq1.length == se2.length
2173 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[i]
2174 *
2175 */
2176
2177 /* pure */ public static boolean pairwiseEqual(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2178 if (! sameLength(seq1, seq2)) { return false; }
2179 assert seq1 != null && seq2 != null; // because sameLength() = true
2180 for (int i = 0 ; i < seq1.length ; i++) {
2181 if (ne(seq1[i], seq2[i])) {
2182 return false;
2183 }
2184 }
2185 return true;
2186 }
2187
2188 /** True iff seq1 and seq2 have the same length, and every seq1[i] != seq2[i].
2189 *
2190 * Meaning (in pseudo-FOL):
2191 *
2192 * /\ seq1.length == se2.length
2193 * /\ forall i in { 0..seq1.length-1 } : seq1[i] != seq2[i]
2194 *
2195 */
2196 /* pure */ public static boolean pairwiseNotEqual(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2197 if (! sameLength(seq1, seq2)) { return false; }
2198 assert seq1 != null && seq2 != null; // because sameLength() = true
2199 for (int i = 0 ; i < seq1.length ; i++) {
2200 if (eq(seq1[i], seq2[i])) {
2201 return false;
2202 }
2203 }
2204 return true;
2205 }
2206
2207 /** True iff seq1 and seq2 have the same length, and every seq1[i] < seq2[i].
2208 *
2209 * Meaning (in pseudo-FOL):
2210 *
2211 * /\ seq1.length == se2.length
2212 * /\ forall i in { 0..seq1.length-1 } : seq1[i] < seq2[i]
2213 *
2214 */
2215 /* pure */ public static boolean pairwiseLT(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2216 if (! sameLength(seq1, seq2)) { return false; }
2217 assert seq1 != null && seq2 != null; // because sameLength() = true
2218 for (int i = 0 ; i < seq1.length ; i++) {
2219 if (gte(seq1[i], seq2[i])) {
2220 return false;
2221 }
2222 }
2223 return true;
2224 }
2225
2226 /** True iff seq1 and seq2 have the same length, and every seq1[i] <= seq2[i].
2227 * Meaning (in pseudo-FOL):
2228 *
2229 * /\ seq1.length == se2.length
2230 * /\ forall i in { 0..seq1.length-1 } : seq1[i] <= seq2[i]
2231 *
2232 */
2233 /* pure */ public static boolean pairwiseLTE(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2234 if (! sameLength(seq1, seq2)) { return false; }
2235 assert seq1 != null && seq2 != null; // because sameLength() = true
2236 for (int i = 0 ; i < seq1.length ; i++) {
2237 if (gt(seq1[i], seq2[i])) {
2238 return false;
2239 }
2240 }
2241 return true;
2242 }
2243
2244 /** True iff seq1 and seq2 have the same length, and every seq1[i] > seq2[i].
2245 * Meaning (in pseudo-FOL):
2246 *
2247 * /\ seq1.length == se2.length
2248 * /\ forall i in { 0..seq1.length-1 } : seq1[i] > seq2[i]
2249 *
2250 */
2251 /* pure */ public static boolean pairwiseGT(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2252 if (! sameLength(seq1, seq2)) { return false; }
2253 assert seq1 != null && seq2 != null; // because sameLength() = true
2254 for (int i = 0 ; i < seq1.length ; i++) {
2255 if (lte(seq1[i], seq2[i])) {
2256 return false;
2257 }
2258 }
2259 return true;
2260 }
2261
2262 /** True iff seq1 and seq2 have the same length, and every seq1[i] >= seq2[i].
2263 * Meaning (in pseudo-FOL):
2264 *
2265 * /\ seq1.length == se2.length
2266 * /\ forall i in { 0..seq1.length-1 } : seq1[i] >= seq2[i]
2267 *
2268 */
2269 /* pure */ public static boolean pairwiseGTE(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2270 if (! sameLength(seq1, seq2)) { return false; }
2271 assert seq1 != null && seq2 != null; // because sameLength() = true
2272 for (int i = 0 ; i < seq1.length ; i++) {
2273 if (lt(seq1[i], seq2[i])) {
2274 return false;
2275 }
2276 }
2277 return true;
2278 }
2279
2280 /**
2281 * Returns true iff seq1 is lexically equal to seq2.
2282 * For equality, "lexically" and "pairwise" are the same.
2283 */
2284 /* pure */ public static boolean lexEqual(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2285 if (seq1 == null) { return false; }
2286 if (seq2 == null) { return false; }
2287 return pairwiseEqual(seq1, seq2);
2288 }
2289
2290 /**
2291 * Returns true iff seq1 is lexically not equal to seq2.
2292 */
2293 /* pure */ public static boolean lexNotEqual(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2294 if (seq1 == null) { return false; }
2295 if (seq2 == null) { return false; }
2296 return !lexEqual(seq1, seq2);
2297 }
2298
2299 /**
2300 * Returns true iff seq1 is lexically < seq2.
2301 */
2302 /* pure */ public static boolean lexLT(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2303 if (seq1 == null) { return false; }
2304 if (seq2 == null) { return false; }
2305 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
2306 for (int i = 0 ; i < minlength ; i++) {
2307 if (gt(seq1[i], seq2[i])) {
2308 return false;
2309 } else if (lt(seq1[i], seq2[i])) {
2310 return true;
2311 }
2312 }
2313 if (seq1.length >= seq2.length) {
2314 return false;
2315 }
2316 return true;
2317 }
2318
2319 /**
2320 * Returns true iff seq1 is lexically <= to seq2.
2321 */
2322 /* pure */ public static boolean lexLTE(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2323 if (seq1 == null) { return false; }
2324 if (seq2 == null) { return false; }
2325 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
2326 for (int i = 0 ; i < minlength ; i++) {
2327 if (gt(seq1[i], seq2[i])) {
2328 return false;
2329 } else if (lt(seq1[i], seq2[i])) {
2330 return true;
2331 }
2332 }
2333 if (seq1.length > seq2.length) {
2334 return false;
2335 }
2336 return true;
2337 }
2338
2339 /**
2340 * Returns true iff seq1 is lexically > to seq2.
2341 */
2342 /* pure */ public static boolean lexGT(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2343 if (seq1 == null) { return false; }
2344 if (seq2 == null) { return false; }
2345 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
2346 for (int i = 0 ; i < minlength ; i++) {
2347 if (lt(seq1[i], seq2[i])) {
2348 return false;
2349 } else if (gt(seq1[i], seq2[i])) {
2350 return true;
2351 }
2352 }
2353 if (seq1.length <= seq2.length) {
2354 return false;
2355 }
2356 return true;
2357 }
2358
2359 /**
2360 * Returns true iff seq1 is lexically >= to seq2.
2361 */
2362 /* pure */ public static boolean lexGTE(char /*@Nullable*/ [] seq1, char /*@Nullable*/ [] seq2) {
2363 if (seq1 == null) { return false; }
2364 if (seq2 == null) { return false; }
2365 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
2366 for (int i = 0 ; i < minlength ; i++) {
2367 if (lt(seq1[i], seq2[i])) {
2368 return false;
2369 } else if (gt(seq1[i], seq2[i])) {
2370 return true;
2371 }
2372 }
2373 if (seq1.length < seq2.length) {
2374 return false;
2375 }
2376 return true;
2377 }
2378
2379 /** True iff for all applicable i, every seq[i] == seq[i+1].
2380 *
2381 * Meaning (in pseudo-FOL):
2382 *
2383 * forall i in { 0..seq.length-2 } : seq[i] == seq[i+1]
2384 *
2385 */
2386 /* pure */ public static boolean eltwiseEqual(char /*@Nullable*/ [] seq) {
2387 if (seq == null) { return false; }
2388 for (int i = 0 ; i < seq.length ; i++) {
2389 if (i < seq.length-1) {
2390 if (ne(seq[i], seq[i+1])) {
2391 return false;
2392 }
2393 }
2394 }
2395 return true;
2396 }
2397
2398 /** True iff for all applicable i, every seq[i] != seq[i+1].
2399 *
2400 * Meaning (in pseudo-FOL):
2401 *
2402 * forall i in { 0..seq.length-2 } : seq[i] != seq[i+1]
2403 *
2404 */
2405 /* pure */ public static boolean eltwiseNotEqual(char /*@Nullable*/ [] seq) {
2406 if (seq == null) { return false; }
2407 for (int i = 0 ; i < seq.length ; i++) {
2408 if (i < seq.length-1) {
2409 if (eq(seq[i], seq[i+1])) {
2410 return false;
2411 }
2412 }
2413 }
2414 return true;
2415 }
2416
2417 /** True iff for all applicable i, every seq[i] < seq[i+1].
2418 *
2419 * Meaning (in pseudo-FOL):
2420 *
2421 * forall i in { 0..seq.length-2 } : seq[i] < seq[i+1]
2422 *
2423 */
2424 /* pure */ public static boolean eltwiseLT(char /*@Nullable*/ [] seq) {
2425 if (seq == null) { return false; }
2426 for (int i = 0 ; i < seq.length ; i++) {
2427 if (i < seq.length-1) {
2428 if (gte(seq[i], seq[i+1])) {
2429 return false;
2430 }
2431 }
2432 }
2433 return true;
2434 }
2435
2436 /** True iff for all applicable i, every seq[i] <= seq[i+1].
2437 *
2438 * Meaning (in pseudo-FOL):
2439 *
2440 * forall i in { 0..seq.length-2 } : seq[i] <= seq[i+1]
2441 *
2442 */
2443 /* pure */ public static boolean eltwiseLTE(char /*@Nullable*/ [] seq) {
2444 if (seq == null) { return false; }
2445 for (int i = 0 ; i < seq.length ; i++) {
2446 if (i < seq.length-1) {
2447 if (gt(seq[i], seq[i+1])) {
2448 return false;
2449 }
2450 }
2451 }
2452 return true;
2453 }
2454
2455 /** True iff for all applicable i, every seq[i] > seq[i+1].
2456 *
2457 * Meaning (in pseudo-FOL):
2458 *
2459 * forall i in { 0..seq.length-2 } : seq[i] > seq[i+1]
2460 *
2461 */
2462 /* pure */ public static boolean eltwiseGT(char /*@Nullable*/ [] seq) {
2463 if (seq == null) { return false; }
2464 for (int i = 0 ; i < seq.length ; i++) {
2465 if (i < seq.length-1) {
2466 if (lte(seq[i], seq[i+1])) {
2467 return false;
2468 }
2469 }
2470 }
2471 return true;
2472 }
2473
2474 /** True iff for all applicable i, every seq[i] >= seq[i+1].
2475 *
2476 * Meaning (in pseudo-FOL):
2477 *
2478 * forall i in { 0..seq.length-2 } : seq[i] >= seq[i+1]
2479 *
2480 */
2481 /* pure */ public static boolean eltwiseGTE(char /*@Nullable*/ [] seq) {
2482 if (seq == null) { return false; }
2483 for (int i = 0 ; i < seq.length ; i++) {
2484 if (i < seq.length-1) {
2485 if (lt(seq[i], seq[i+1])) {
2486 return false;
2487 }
2488 }
2489 }
2490 return true;
2491 }
2492
2493 /** True iff for all applicable i, every seq[i] == i.
2494 *
2495 * Meaning (in pseudo-FOL):
2496 *
2497 * forall i in { 0..seq.length-1 } : seq[i] == i
2498 *
2499 */
2500 /* pure */ public static boolean eltsEqualIndex(char /*@Nullable*/ [] seq) {
2501 if (seq == null) { return false; }
2502 for (int i = 0 ; i < seq.length ; i++) {
2503 if (ne(seq[i], i)) {
2504 return false;
2505 }
2506 }
2507 return true;
2508 }
2509
2510 /** True iff for all applicable i, every seq[i] != i.
2511 *
2512 * Meaning (in pseudo-FOL):
2513 *
2514 * forall i in { 0..seq.length-1 } : seq[i] != i
2515 *
2516 */
2517 /* pure */ public static boolean eltsNotEqualIndex(char /*@Nullable*/ [] seq) {
2518 if (seq == null) { return false; }
2519 for (int i = 0 ; i < seq.length ; i++) {
2520 if (eq(seq[i], i)) {
2521 return false;
2522 }
2523 }
2524 return true;
2525 }
2526
2527 /** True iff for all applicable i, every seq[i] < i.
2528 *
2529 * Meaning (in pseudo-FOL):
2530 *
2531 * forall i in { 0..seq.length-1 } : seq[i] < i
2532 *
2533 */
2534 /* pure */ public static boolean eltsLtIndex(char /*@Nullable*/ [] seq) {
2535 if (seq == null) { return false; }
2536 for (int i = 0 ; i < seq.length ; i++) {
2537 if (gte(seq[i], i)) {
2538 return false;
2539 }
2540 }
2541 return true;
2542 }
2543
2544 /** True iff for all applicable i, every seq[i] <= i.
2545 *
2546 * Meaning (in pseudo-FOL):
2547 *
2548 * forall i in { 0..seq.length-1 } : seq[i] <= i
2549 *
2550 */
2551 /* pure */ public static boolean eltsLteIndex(char /*@Nullable*/ [] seq) {
2552 if (seq == null) { return false; }
2553 for (int i = 0 ; i < seq.length ; i++) {
2554 if (gt(seq[i], i)) {
2555 return false;
2556 }
2557 }
2558 return true;
2559 }
2560
2561 /** True iff for all applicable i, every seq[i] > i.
2562 *
2563 * Meaning (in pseudo-FOL):
2564 *
2565 * forall i in { 0..seq.length-1 } : seq[i] > i
2566 *
2567 */
2568 /* pure */ public static boolean eltsGtIndex(char /*@Nullable*/ [] seq) {
2569 if (seq == null) { return false; }
2570 for (int i = 0 ; i < seq.length ; i++) {
2571 if (lte(seq[i], i)) {
2572 return false;
2573 }
2574 }
2575 return true;
2576 }
2577
2578 /** True iff for all applicable i, every seq[i] >= i.
2579 *
2580 * Meaning (in pseudo-FOL):
2581 *
2582 * forall i in { 0..seq.length-1 } : seq[i] >= i
2583 *
2584 */
2585 /* pure */ public static boolean eltsGteIndex(char /*@Nullable*/ [] seq) {
2586 if (seq == null) { return false; }
2587 for (int i = 0 ; i < seq.length ; i++) {
2588 if (lt(seq[i], i)) {
2589 return false;
2590 }
2591 }
2592 return true;
2593 }
2594
2595 /// Deferencing (accessing) fields
2596
2597 /**
2598 * collectchar accepts an object and a list of fields (one of which is
2599 * of array type, and the rest of which are not), and produces an array in
2600 * which the original object has had the given fields accessed.
2601 *
2602 * Daikon creates invariants over "variables" such as the following.
2603 *
2604 * x.arr[].z The result of collecting all elements y.z for all y's
2605 * in array x.arr.
2606 * arr[].y.z The result of collecting all elements x.y.z for all x's
2607 * in array arr.
2608 * x.y.z[] The result of collecting all elements in array x.y.z[]
2609 *
2610 * The collectchar() method does this collecting work.
2611 *
2612 * Given an object (x, arr, or x, correspondingly, in the above examples)
2613 * and a "field string" (arr.z, y.z, or y.z, correspondingly, in the
2614 * above example), the collect method collects the elements the result
2615 * from following the fields, one of which is assumed to be an array.
2616 *
2617 * requires: fieldStr.length() > 0 and object != null
2618 * requires: fieldStr contains only field names, no "[]" strings.
2619 *
2620 * requires: the method only works for field sequences with exactly
2621 * one field representing an array. For example, the collection
2622 * a[].b[].c will fail.
2623 *
2624 * If the resulting collection is of non-primitive type, then collect
2625 * returns an array of type Object[].
2626 *
2627 * Returns null if any array or field access causes an exception.
2628 */
2629 /* pure */ public static char /*@Nullable*/ [] collectchar (Object object, String fieldStr) {
2630
2631 if (object == null) { return null; }
2632 if (fieldStr == null) { return null; }
2633
2634 //assert fieldStr != null && !"".equals(fieldStr);
2635 String[] fieldNames = fieldStr.split("\\.");
2636 char[] retval = collectchar (object, fieldNames, 0);
2637 //System.err.println("%%% fieldArray returned: " + utilMDE.ArraysMDE.toString(retval));
2638 return retval;
2639 }
2640
2641 /** Helper method for collectchar(Object, String).
2642 * Operates on the fields specified in fields[fieldsStartIdx..].
2643 * @see collectchar(Object, String)
2644 */
2645 /* pure */ private static char /*@Nullable*/ [] collectchar (Object object,
2646 String[] fields, int fieldsStartIdx) {
2647
2648 if (object == null) { return null; }
2649 assert (fields != null);
2650 assert (fieldsStartIdx >= 0 && fieldsStartIdx < fields.length);
2651
2652 Object fieldObj = null;
2653 try {
2654 Field field = (object instanceof java.lang.Class<?>)
2655 ? ((Class<?>)object).getDeclaredField(fields[fieldsStartIdx])
2656 : object.getClass().getDeclaredField(fields[fieldsStartIdx]);
2657 field.setAccessible(true);
2658 // Class cls = field.getType();
2659 fieldObj = field.get(object);
2660 //System.out.println("***fieldObj="+fieldObj);
2661
2662 } catch (Exception e) {
2663 return null;
2664
2665 }
2666
2667 if (fieldObj == null) {
2668 return null;
2669 }
2670
2671 // base case: just accessed the last field
2672 if (fields.length - 1 == fieldsStartIdx) {
2673
2674 if (fieldObj.getClass().isArray()) {
2675 // last field is an array
2676 return (char[])fieldObj;
2677 } else {
2678 // This hack should be removed in favor of, at "oneEltArray = ..."
2679 // below, calling a version of collectchar_field that throws an
2680 // error. Then, this case becomes a run-time error. -MDE
2681
2682 // Just one element; return a one-element array.
2683 //assert cls.equals(Character.TYPE);
2684 return new char[] { ((Character)fieldObj).charValue() };
2685 }
2686 } else {
2687 // recursive case: more fields to access after this one
2688
2689 if (daikon.ProglangType.list_implementors.contains(fieldObj.getClass().getName())) {
2690
2691 java.util.AbstractCollection<?> collection = (java.util.AbstractCollection<?>)fieldObj;
2692 char[] intermediate = new char[collection.size()];
2693 int index = 0;
2694 for (Iterator<?> i = collection.iterator() ; i.hasNext() ; ) {
2695 char[] oneEltArray = collectchar (i.next(), fields, fieldsStartIdx + 1);
2696 //assert oneEltArray.length == 1;
2697 intermediate[index++] = oneEltArray[0];
2698 }
2699 return intermediate;
2700 } else if (fieldObj.getClass().isArray()) {
2701
2702 // collect elements across array
2703 char[] intermediate = new char[Array.getLength(fieldObj)];
2704 for (int i = 0 ; i < intermediate.length ; i++) {
2705 char[] oneEltArray = collectchar (Array.get(fieldObj, i),
2706 fields, fieldsStartIdx + 1);
2707 //assert oneEltArray.length == 1;
2708 intermediate[i] = oneEltArray[0];
2709 }
2710 return intermediate;
2711 } else {
2712
2713 return collectchar (fieldObj, fields, fieldsStartIdx + 1);
2714 }
2715 }
2716 }
2717
2718 // Returns the results of dereferencing the fields specified in
2719 // fields[fieldsStartIdx..] for 'object'.
2720 // Returns a default value if any field access causes an exception.
2721 /* pure */ public static char collectchar_field (Object object, String fieldStr) {
2722
2723 if (object == null) { return Character.MAX_VALUE; } // return default value
2724 if (fieldStr == null) { return Character.MAX_VALUE; } // return default value
2725
2726 String[] fieldNames = fieldStr.split("\\.");
2727
2728 // Holds the intermediate (and final) result
2729 Object fieldObj = object;
2730
2731 for (int i = 0 ; i < fieldNames.length ; i++) {
2732
2733 String fieldName = fieldNames[i];
2734
2735 try {
2736 Field field =
2737 (fieldObj instanceof java.lang.Class<?>)
2738 ? ((Class<?>)fieldObj).getDeclaredField(fieldName)
2739 : fieldObj.getClass().getDeclaredField(fieldName);
2740 field.setAccessible(true);
2741 fieldObj = field.get(fieldObj);
2742
2743 } catch (Exception e) {
2744 return Character.MAX_VALUE; // return default value
2745
2746 }
2747
2748 }
2749
2750 return ((Character)fieldObj).charValue();
2751 }
2752
2753 ///////////////////////////////////////////////////////////////////////////
2754 /// Methods for "double" (from QuantBody.java.jpp)
2755 ///
2756
2757 /** Returns the ith element of the array or collection argument.
2758 * If the argument is null or not an array or collection, returns a
2759 * default value (Double.NaN).
2760 **/
2761 /* pure */ public static double getElement_double (Object o, long i) {
2762 if (o == null) { return Double.NaN; } // return default value
2763 java.lang.Class<?> c = o.getClass();
2764 if (c.isArray()) {
2765 return java.lang.reflect.Array.getDouble (o, (int)i);
2766 } else if (o instanceof java.util.AbstractCollection<?>) {
2767 return java.lang.reflect.Array.getDouble (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
2768 } else {
2769 return Double.NaN; // return default value
2770 }
2771 }
2772
2773 /* pure */ public static double getElement_double (double[] arr, long i) {
2774 if (arr == null) { return Double.NaN; } // return default value
2775 return arr[(int)i];
2776 }
2777
2778 private static boolean eq(double x, double y) {
2779 return fuzzy.eq(x,y);
2780 }
2781
2782 private static boolean ne(double x, double y) {
2783 return fuzzy.ne(x,y);
2784 }
2785
2786 private static boolean lt(double x, double y) {
2787 return fuzzy.lt(x,y);
2788 }
2789
2790 private static boolean lte(double x, double y) {
2791 return fuzzy.lte(x,y);
2792 }
2793
2794 private static boolean gt(double x, double y) {
2795 return fuzzy.gt(x,y);
2796 }
2797
2798 private static boolean gte(double x, double y) {
2799 return fuzzy.gte(x,y);
2800 }
2801
2802 /** True iff both sequences are non-null and have the same length. */
2803 /* pure */ public static boolean sameLength(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
2804 return ((seq1 != null)
2805 && (seq2 != null)
2806 && seq1.length == seq2.length);
2807 }
2808
2809 /** True iff both sequences are non-null and have the same length. */
2810 /* pure */ public static boolean sameLength(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
2811 return ((seq1 != null)
2812 && (seq2 != null)
2813 && seq1.length == seq2.length);
2814 }
2815
2816 /** True iff both sequences have the same length, and all seq2[i] divide seq1[i].
2817 *
2818 * Meaning (in pseudo-FOL):
2819 *
2820 * <pre>
2821 * /\ seq1.length == seq2.length
2822 * /\ forall i in { 0..seq2.length-1 } : seq2[i] divides seq1[i]
2823 * </pre>
2824 *
2825 */
2826 /* pure */ public static boolean pairwiseDivides(double[] seq1, double[] seq2) {
2827 if (! sameLength(seq1, seq2)) { return false; }
2828 assert seq1 != null && seq2 != null; // because sameLength() = true
2829 for (int i = 0 ; i < seq1.length ; i++) {
2830 if (ne(seq1[i] % seq2[i], 0)) {
2831 return false;
2832 }
2833 }
2834 return true;
2835 }
2836 /* pure */ public static boolean pairwiseDivides(double[] seq1, float[] seq2) {
2837 if (! sameLength(seq1, seq2)) { return false; }
2838 assert seq1 != null && seq2 != null; // because sameLength() = true
2839 for (int i = 0 ; i < seq1.length ; i++) {
2840 if (ne(seq1[i] % seq2[i], 0)) {
2841 return false;
2842 }
2843 }
2844 return true;
2845 }
2846
2847 /** True iff both sequences have the same length, and all seq1[i] == seq2[i] * seq2[i].
2848 *
2849 * Meaning (in pseudo-FOL):
2850 *
2851 * <pre>
2852 * /\ seq1.length == seq2.length
2853 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == seq2[i] * seq2[i]
2854 * </pre>
2855 *
2856 */
2857 /* pure */ public static boolean pairwiseSquare(double[] seq1, double[] seq2) {
2858 if (! sameLength(seq1, seq2)) { return false; }
2859 assert seq1 != null && seq2 != null; // because sameLength() = true
2860 for (int i = 0 ; i < seq1.length ; i++) {
2861 if (ne(seq1[i], seq2[i] * seq2[i])) {
2862 return false;
2863 }
2864 }
2865 return true;
2866 }
2867 /* pure */ public static boolean pairwiseSquare(double[] seq1, float[] seq2) {
2868 if (! sameLength(seq1, seq2)) { return false; }
2869 assert seq1 != null && seq2 != null; // because sameLength() = true
2870 for (int i = 0 ; i < seq1.length ; i++) {
2871
2872 if (ne(seq1[i], ((double) seq2[i]) * ((double) seq2[i]))) {
2873
2874 return false;
2875 }
2876 }
2877 return true;
2878 }
2879
2880 /**
2881 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
2882 * If either array is null, returns null.
2883 * If either array is empty, returns only those elements in the other array.
2884 * If both arrays are empty, returns a new empty array.
2885 */
2886 /* pure */ public static double /*@PolyNull*/ [] concat(double /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
2887 if (seq1 == null) { return null; }
2888 if (seq2 == null) { return null; }
2889 return utilMDE.ArraysMDE.concat(seq1, seq2);
2890 }
2891
2892 /* pure */ public static double /*@PolyNull*/ [] concat(double /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
2893 if (seq1 == null) { return null; }
2894 if (seq2 == null) { return null; }
2895 // Cannot just use utilMDE.ArraysMDE.concat because the two arrays
2896 // have different types. This essentially inlines that method.
2897 int newLength = seq1.length + seq2.length;
2898 double[] retval = new double[newLength];
2899
2900 System.arraycopy(seq1, 0, retval, 0, seq1.length);
2901 for (int j = 0 ; j < seq2.length ; j++) {
2902 retval[seq1.length+j] = seq2[j];
2903 }
2904
2905 return retval;
2906 }
2907
2908 /**
2909 * Returns an array that is equivalent to the set union of seq1 and seq2.
2910 * This method gives no assurances about the order or repetition of elements:
2911 * elements may be repeated, and their order may be different from the
2912 * order of elements in seq1 and seq2.
2913 */
2914 /* pure */ public static double /*@PolyNull*/ [] union(double /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
2915 if (seq1 == null) { return null; }
2916 if (seq2 == null) { return null; }
2917 return concat(seq1, seq2);
2918 }
2919
2920 /* pure */ public static double /*@PolyNull*/ [] union(double /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
2921 if (seq1 == null) { return null; }
2922 if (seq2 == null) { return null; }
2923 return concat(seq1, seq2);
2924 }
2925
2926 /**
2927 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
2928 * This method gives no assurances about the order or repetition of elements:
2929 * elements may be repeated, and their order may be different from the
2930 * order of elements in seq1 and seq2.
2931 */
2932 /* pure */ public static double /*@PolyNull*/ [] intersection(double /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
2933 if (seq1 == null) { return null; }
2934 if (seq2 == null) { return null; }
2935 double[] intermediate = new double[Math.min(seq1.length, seq2.length)];
2936 int length = 0;
2937 for (int i = 0 ; i < seq1.length ; i++) {
2938 if (memberOf(seq1[i], seq2) ) {
2939 intermediate[length++] = seq1[i];
2940 }
2941 }
2942 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
2943 }
2944
2945 /* pure */ public static double /*@PolyNull*/ [] intersection(double /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
2946 if (seq1 == null) { return null; }
2947 if (seq2 == null) { return null; }
2948 double[] intermediate = new double[Math.min(seq1.length, seq2.length)];
2949 int length = 0;
2950 for (int i = 0 ; i < seq1.length ; i++) {
2951 if (memberOf(seq1[i], seq2) ) {
2952 intermediate[length++] = seq1[i];
2953 }
2954 }
2955 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
2956 }
2957
2958 /**
2959 * Returns an array that is equivalent to the set difference of seq1 and seq2.
2960 * This method gives no assurances about the order or repetition of elements:
2961 * elements may be repeated, and their order may be different from the
2962 * order of elements in seq1 and seq2.
2963 */
2964 /* pure */ public static double /*@PolyNull*/ [] setDiff(double /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
2965 if (seq1 == null) { return null; }
2966 if (seq2 == null) { return null; }
2967 double[] intermediate = new double[seq1.length];
2968 int length = 0;
2969 for (int i = 0 ; i < seq1.length ; i++) {
2970 if (!memberOf(seq1[i], seq2)) {
2971 intermediate[length++] = seq1[i];
2972 }
2973 }
2974 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
2975 }
2976
2977 /* pure */ public static double /*@PolyNull*/ [] setDiff(double /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
2978 if (seq1 == null) { return null; }
2979 if (seq2 == null) { return null; }
2980 double[] intermediate = new double[seq1.length];
2981 int length = 0;
2982 for (int i = 0 ; i < seq1.length ; i++) {
2983 if (!memberOf(seq1[i], seq2)) {
2984 intermediate[length++] = seq1[i];
2985 }
2986 }
2987 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
2988 }
2989
2990 /**
2991 * Retuns true iff seq1 and seq2 are equal when considered as sets.
2992 */
2993 /* pure */ public static boolean setEqual(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
2994 if (seq1 == null) { return false; }
2995 if (seq2 == null) { return false; }
2996 for (int i = 0; i < seq1.length ; i++) {
2997 if (!memberOf(seq1[i], seq2) ) {
2998 return false;
2999 }
3000 }
3001 for (int i = 0; i < seq2.length ; i++) {
3002 if (!memberOf(seq2[i], seq1) ) {
3003 return false;
3004 }
3005 }
3006 return true;
3007 }
3008
3009 /* pure */ public static boolean setEqual(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3010 if (seq1 == null) { return false; }
3011 if (seq2 == null) { return false; }
3012 for (int i = 0; i < seq1.length ; i++) {
3013 if (!memberOf(seq1[i], seq2) ) {
3014 return false;
3015 }
3016 }
3017 for (int i = 0; i < seq2.length ; i++) {
3018 if (!memberOf(seq2[i], seq1) ) {
3019 return false;
3020 }
3021 }
3022 return true;
3023 }
3024
3025 /** True iff seq1 is the reverse of seq2.
3026 *
3027 * Meaning (in pseudo-FOL):
3028 *
3029 * <pre>
3030 * /\ seq1.length == seq2.length
3031 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
3032 * </pre>
3033 *
3034 */
3035 /* pure */ public static boolean isReverse(double[] seq1, double[] seq2) {
3036 if (! sameLength(seq1, seq2)) { return false; }
3037 assert seq1 != null && seq2 != null; // because sameLength() = true
3038 int length = seq1.length;
3039 for (int i = 0 ; i < length ; i++) {
3040 if (ne(seq1[i], seq2[length - i - 1])) {
3041 return false;
3042 }
3043 }
3044 return true;
3045 }
3046
3047 /* pure */ public static boolean isReverse(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3048 if (! sameLength(seq1, seq2)) { return false; }
3049 assert seq1 != null && seq2 != null; // because sameLength() = true
3050 int length = seq1.length;
3051 for (int i = 0 ; i < length ; i++) {
3052 if (ne(seq1[i], seq2[length - i - 1])) {
3053 return false;
3054 }
3055 }
3056 return true;
3057 }
3058
3059 /**
3060 * True iff seq1 is a subset of seq2, when the sequences are
3061 * considered as sets.
3062 */
3063 /* pure */ public static boolean subsetOf(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3064 if (seq1 == null) { return false; }
3065 if (seq2 == null) { return false; }
3066 for (int i = 0 ; i < seq1.length ; i++) {
3067 if (!memberOf(seq1[i], seq2)) {
3068 return false;
3069 }
3070 }
3071 return true;
3072 }
3073
3074 /* pure */ public static boolean subsetOf(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3075 if (seq1 == null) { return false; }
3076 if (seq2 == null) { return false; }
3077 for (int i = 0 ; i < seq1.length ; i++) {
3078 if (!memberOf(seq1[i], seq2)) {
3079 return false;
3080 }
3081 }
3082 return true;
3083 }
3084
3085 /**
3086 * Returns true iff seq contains no duplicate elements.
3087 */
3088 /* pure */ public static boolean noDups(double /*@Nullable*/ [] seq) {
3089 if (seq == null) { return false; }
3090 return utilMDE.ArraysMDE.noDuplicates(seq);
3091 }
3092
3093 /**
3094 * Returns true iff elt is in array arr.
3095 */
3096 /* pure */ public static boolean memberOf(double elt, double /*@Nullable*/ [] arr) {
3097 if (arr == null) { return false; }
3098 for (int i = 0 ; i < arr.length ; i++) {
3099 if (eq(arr[i], elt)) { return true; }
3100 }
3101 return false;
3102 }
3103
3104 /* pure */ public static boolean memberOf(double elt, float /*@Nullable*/ [] arr) {
3105 if (arr == null) { return false; }
3106 for (int i = 0 ; i < arr.length ; i++) {
3107 if (eq(arr[i], elt)) { return true; }
3108 }
3109 return false;
3110 }
3111
3112 /**
3113 * Returns a subsequence of seq with first elements seq[start] and
3114 * last element seq[end].
3115 */
3116 /* pure */ public static double /*@PolyNull*/ [] slice(double /*@PolyNull*/ [] seq, int start, int end) {
3117 if (seq == null) { return null; }
3118 int sliceStart = start;
3119 int sliceEnd = end;
3120 if (start < 0) { return new double[] { }; }
3121 if (end > seq.length-1) { return new double[] { }; }
3122 if (sliceStart > sliceEnd) { return new double[] { }; }
3123 int length = sliceEnd - sliceStart + 1;
3124 return utilMDE.ArraysMDE.subarray(seq, sliceStart, length);
3125 }
3126
3127 /* pure */ public static double /*@PolyNull*/ [] slice(double /*@PolyNull*/ [] seq, long start, int end) {
3128 return slice(seq, (int)start, end);
3129 }
3130 /* pure */ public static double /*@PolyNull*/ [] slice(double /*@PolyNull*/ [] seq, int start, long end) {
3131 return slice(seq, start, (int)end);
3132 }
3133 /* pure */ public static double /*@PolyNull*/ [] slice(double /*@PolyNull*/ [] seq, long start, long end) {
3134 return slice(seq, (int)start, (int)end);
3135 }
3136
3137 /** True iff all elements in arr equal elt.
3138 *
3139 * Meaning (in pseudo-FOL):
3140 *
3141 * forall i in { 0..arr.length-1 } : arr[i] == elt
3142 *
3143 */
3144 /* pure */ public static boolean eltsEqual(double /*@Nullable*/ [] arr, double elt) {
3145 if (arr == null) { return false; }
3146 for (int i = 0 ; i < arr.length ; i++) {
3147 if (ne(arr[i], elt)) { return false; }
3148 }
3149 return true;
3150 }
3151
3152 /* pure */ public static boolean eltsEqual(double /*@Nullable*/ [] arr, float elt) {
3153 if (arr == null) { return false; }
3154 for (int i = 0 ; i < arr.length ; i++) {
3155 if (ne(arr[i], elt)) { return false; }
3156 }
3157 return true;
3158 }
3159
3160 /** True iff every element in arr does not equal elt.
3161 *
3162 * Meaning (in pseudo-FOL):
3163 *
3164 * forall i in { 0..arr.length-1 } : arr[i] != elt
3165 *
3166 */
3167 /* pure */ public static boolean eltsNotEqual(double /*@Nullable*/ [] arr, double elt) {
3168 if (arr == null) { return false; }
3169 for (int i = 0 ; i < arr.length ; i++) {
3170 if (eq(arr[i], elt)) { return false; }
3171 }
3172 return true;
3173 }
3174
3175 /* pure */ public static boolean eltsNotEqual(double /*@Nullable*/ [] arr, float elt) {
3176 if (arr == null) { return false; }
3177 for (int i = 0 ; i < arr.length ; i++) {
3178 if (eq(arr[i], elt)) { return false; }
3179 }
3180 return true;
3181 }
3182
3183 /** True iff every element in arr is greater than elt.
3184 *
3185 * Meaning (in pseudo-FOL):
3186 *
3187 * forall i in { 0..arr.length-1 } : arr[i] > elt
3188 *
3189 */
3190 /* pure */ public static boolean eltsGT(double /*@Nullable*/ [] arr, double elt) {
3191 if (arr == null) { return false; }
3192 for (int i = 0 ; i < arr.length ; i++) {
3193 if (lte(arr[i], elt)) { return false; }
3194 }
3195 return true;
3196 }
3197
3198 /* pure */ public static boolean eltsGT(double /*@Nullable*/ [] arr, float elt) {
3199 if (arr == null) { return false; }
3200 for (int i = 0 ; i < arr.length ; i++) {
3201 if (lte(arr[i], elt)) { return false; }
3202 }
3203 return true;
3204 }
3205
3206 /** True iff every element in arr is greater than or equal to elt.
3207 *
3208 * Meaning (in pseudo-FOL):
3209 *
3210 * forall i in { 0..arr.length-1 } : arr[i] >= elt
3211 *
3212 */
3213 /* pure */ public static boolean eltsGTE(double /*@Nullable*/ [] arr, double elt) {
3214 if (arr == null) { return false; }
3215 for (int i = 0 ; i < arr.length ; i++) {
3216 if (lt(arr[i], elt)) { return false; }
3217 }
3218 return true;
3219 }
3220
3221 /* pure */ public static boolean eltsGTE(double /*@Nullable*/ [] arr, float elt) {
3222 if (arr == null) { return false; }
3223 for (int i = 0 ; i < arr.length ; i++) {
3224 if (lt(arr[i], elt)) { return false; }
3225 }
3226 return true;
3227 }
3228
3229 /** True iff every element in arr is less than elt.
3230 *
3231 * Meaning (in pseudo-FOL):
3232 *
3233 * forall i in { 0..arr.length-1 } : arr[i] < elt
3234 *
3235 */
3236 /* pure */ public static boolean eltsLT(double /*@Nullable*/ [] arr, double elt) {
3237 if (arr == null) { return false; }
3238 for (int i = 0 ; i < arr.length ; i++) {
3239 if (gte(arr[i], elt)) { return false; }
3240 }
3241 return true;
3242 }
3243
3244 /* pure */ public static boolean eltsLT(double /*@Nullable*/ [] arr, float elt) {
3245 if (arr == null) { return false; }
3246 for (int i = 0 ; i < arr.length ; i++) {
3247 if (gte(arr[i], elt)) { return false; }
3248 }
3249 return true;
3250 }
3251
3252 /** True iff every element in arr is less than or equal to elt.
3253 *
3254 * Meaning (in pseudo-FOL):
3255 *
3256 * forall i in { 0..arr.length-1 } : arr[i] <= elt
3257 *
3258 */
3259 /* pure */ public static boolean eltsLTE(double /*@Nullable*/ [] arr, double elt) {
3260 if (arr == null) { return false; }
3261 for (int i = 0 ; i < arr.length ; i++) {
3262 if (gt(arr[i], elt)) { return false; }
3263 }
3264 return true;
3265 }
3266
3267 /* pure */ public static boolean eltsLTE(double /*@Nullable*/ [] arr, float elt) {
3268 if (arr == null) { return false; }
3269 for (int i = 0 ; i < arr.length ; i++) {
3270 if (gt(arr[i], elt)) { return false; }
3271 }
3272 return true;
3273 }
3274
3275 /** True iff seq1 and seq2 have the same length, and every seq1[i] == seq2[i].
3276 *
3277 * Meaning (in pseudo-FOL):
3278 *
3279 * /\ seq1.length == se2.length
3280 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[i]
3281 *
3282 */
3283
3284 /* pure */ public static boolean pairwiseEqual(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3285 if (! sameLength(seq1, seq2)) { return false; }
3286 assert seq1 != null && seq2 != null; // because sameLength() = true
3287 for (int i = 0 ; i < seq1.length ; i++) {
3288 if (Double.isNaN(seq1[i]) && Double.isNaN(seq2[i])) {
3289 continue;
3290 }
3291 if (ne(seq1[i], seq2[i])) {
3292 return false;
3293 }
3294 }
3295 return true;
3296 }
3297
3298 /* pure */ public static boolean pairwiseEqual(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3299 if (! sameLength(seq1, seq2)) { return false; }
3300 assert seq1 != null && seq2 != null; // because sameLength() = true
3301 for (int i = 0 ; i < seq1.length ; i++) {
3302 if (ne(seq1[i], seq2[i])) {
3303 return false;
3304 }
3305 }
3306 return true;
3307 }
3308
3309 /** True iff seq1 and seq2 have the same length, and every seq1[i] != seq2[i].
3310 *
3311 * Meaning (in pseudo-FOL):
3312 *
3313 * /\ seq1.length == se2.length
3314 * /\ forall i in { 0..seq1.length-1 } : seq1[i] != seq2[i]
3315 *
3316 */
3317 /* pure */ public static boolean pairwiseNotEqual(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3318 if (! sameLength(seq1, seq2)) { return false; }
3319 assert seq1 != null && seq2 != null; // because sameLength() = true
3320 for (int i = 0 ; i < seq1.length ; i++) {
3321 if (eq(seq1[i], seq2[i])) {
3322 return false;
3323 }
3324 }
3325 return true;
3326 }
3327
3328 /* pure */ public static boolean pairwiseNotEqual(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3329 if (! sameLength(seq1, seq2)) { return false; }
3330 assert seq1 != null && seq2 != null; // because sameLength() = true
3331 for (int i = 0 ; i < seq1.length ; i++) {
3332 if (eq(seq1[i], seq2[i])) {
3333 return false;
3334 }
3335 }
3336 return true;
3337 }
3338
3339 /** True iff seq1 and seq2 have the same length, and every seq1[i] < seq2[i].
3340 *
3341 * Meaning (in pseudo-FOL):
3342 *
3343 * /\ seq1.length == se2.length
3344 * /\ forall i in { 0..seq1.length-1 } : seq1[i] < seq2[i]
3345 *
3346 */
3347 /* pure */ public static boolean pairwiseLT(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3348 if (! sameLength(seq1, seq2)) { return false; }
3349 assert seq1 != null && seq2 != null; // because sameLength() = true
3350 for (int i = 0 ; i < seq1.length ; i++) {
3351 if (gte(seq1[i], seq2[i])) {
3352 return false;
3353 }
3354 }
3355 return true;
3356 }
3357
3358 /* pure */ public static boolean pairwiseLT(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3359 if (! sameLength(seq1, seq2)) { return false; }
3360 assert seq1 != null && seq2 != null; // because sameLength() = true
3361 for (int i = 0 ; i < seq1.length ; i++) {
3362 if (gte(seq1[i], seq2[i])) {
3363 return false;
3364 }
3365 }
3366 return true;
3367 }
3368
3369 /** True iff seq1 and seq2 have the same length, and every seq1[i] <= seq2[i].
3370 * Meaning (in pseudo-FOL):
3371 *
3372 * /\ seq1.length == se2.length
3373 * /\ forall i in { 0..seq1.length-1 } : seq1[i] <= seq2[i]
3374 *
3375 */
3376 /* pure */ public static boolean pairwiseLTE(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3377 if (! sameLength(seq1, seq2)) { return false; }
3378 assert seq1 != null && seq2 != null; // because sameLength() = true
3379 for (int i = 0 ; i < seq1.length ; i++) {
3380 if (gt(seq1[i], seq2[i])) {
3381 return false;
3382 }
3383 }
3384 return true;
3385 }
3386
3387 /* pure */ public static boolean pairwiseLTE(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3388 if (! sameLength(seq1, seq2)) { return false; }
3389 assert seq1 != null && seq2 != null; // because sameLength() = true
3390 for (int i = 0 ; i < seq1.length ; i++) {
3391 if (gt(seq1[i], seq2[i])) {
3392 return false;
3393 }
3394 }
3395 return true;
3396 }
3397
3398 /** True iff seq1 and seq2 have the same length, and every seq1[i] > seq2[i].
3399 * Meaning (in pseudo-FOL):
3400 *
3401 * /\ seq1.length == se2.length
3402 * /\ forall i in { 0..seq1.length-1 } : seq1[i] > seq2[i]
3403 *
3404 */
3405 /* pure */ public static boolean pairwiseGT(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3406 if (! sameLength(seq1, seq2)) { return false; }
3407 assert seq1 != null && seq2 != null; // because sameLength() = true
3408 for (int i = 0 ; i < seq1.length ; i++) {
3409 if (lte(seq1[i], seq2[i])) {
3410 return false;
3411 }
3412 }
3413 return true;
3414 }
3415
3416 /* pure */ public static boolean pairwiseGT(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3417 if (! sameLength(seq1, seq2)) { return false; }
3418 assert seq1 != null && seq2 != null; // because sameLength() = true
3419 for (int i = 0 ; i < seq1.length ; i++) {
3420 if (lte(seq1[i], seq2[i])) {
3421 return false;
3422 }
3423 }
3424 return true;
3425 }
3426
3427 /** True iff seq1 and seq2 have the same length, and every seq1[i] >= seq2[i].
3428 * Meaning (in pseudo-FOL):
3429 *
3430 * /\ seq1.length == se2.length
3431 * /\ forall i in { 0..seq1.length-1 } : seq1[i] >= seq2[i]
3432 *
3433 */
3434 /* pure */ public static boolean pairwiseGTE(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3435 if (! sameLength(seq1, seq2)) { return false; }
3436 assert seq1 != null && seq2 != null; // because sameLength() = true
3437 for (int i = 0 ; i < seq1.length ; i++) {
3438 if (lt(seq1[i], seq2[i])) {
3439 return false;
3440 }
3441 }
3442 return true;
3443 }
3444
3445 /* pure */ public static boolean pairwiseGTE(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3446 if (! sameLength(seq1, seq2)) { return false; }
3447 assert seq1 != null && seq2 != null; // because sameLength() = true
3448 for (int i = 0 ; i < seq1.length ; i++) {
3449 if (lt(seq1[i], seq2[i])) {
3450 return false;
3451 }
3452 }
3453 return true;
3454 }
3455
3456 /**
3457 * Returns true iff seq1 is lexically equal to seq2.
3458 * For equality, "lexically" and "pairwise" are the same.
3459 */
3460 /* pure */ public static boolean lexEqual(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3461 if (seq1 == null) { return false; }
3462 if (seq2 == null) { return false; }
3463 return pairwiseEqual(seq1, seq2);
3464 }
3465
3466 /* pure */ public static boolean lexEqual(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3467 if (seq1 == null) { return false; }
3468 if (seq2 == null) { return false; }
3469 return pairwiseEqual(seq1, seq2);
3470 }
3471
3472 /**
3473 * Returns true iff seq1 is lexically not equal to seq2.
3474 */
3475 /* pure */ public static boolean lexNotEqual(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3476 if (seq1 == null) { return false; }
3477 if (seq2 == null) { return false; }
3478 return !lexEqual(seq1, seq2);
3479 }
3480
3481 /* pure */ public static boolean lexNotEqual(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3482 if (seq1 == null) { return false; }
3483 if (seq2 == null) { return false; }
3484 return !lexEqual(seq1, seq2);
3485 }
3486
3487 /**
3488 * Returns true iff seq1 is lexically < seq2.
3489 */
3490 /* pure */ public static boolean lexLT(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3491 if (seq1 == null) { return false; }
3492 if (seq2 == null) { return false; }
3493 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3494 for (int i = 0 ; i < minlength ; i++) {
3495 if (gt(seq1[i], seq2[i])) {
3496 return false;
3497 } else if (lt(seq1[i], seq2[i])) {
3498 return true;
3499 }
3500 }
3501 if (seq1.length >= seq2.length) {
3502 return false;
3503 }
3504 return true;
3505 }
3506
3507 /* pure */ public static boolean lexLT(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3508 if (seq1 == null) { return false; }
3509 if (seq2 == null) { return false; }
3510 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3511 for (int i = 0 ; i < minlength ; i++) {
3512 if (gt(seq1[i], seq2[i])) {
3513 return false;
3514 } else if (lt(seq1[i], seq2[i])) {
3515 return true;
3516 }
3517 }
3518 if (seq1.length >= seq2.length) {
3519 return false;
3520 }
3521 return true;
3522 }
3523
3524 /**
3525 * Returns true iff seq1 is lexically <= to seq2.
3526 */
3527 /* pure */ public static boolean lexLTE(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3528 if (seq1 == null) { return false; }
3529 if (seq2 == null) { return false; }
3530 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3531 for (int i = 0 ; i < minlength ; i++) {
3532 if (gt(seq1[i], seq2[i])) {
3533 return false;
3534 } else if (lt(seq1[i], seq2[i])) {
3535 return true;
3536 }
3537 }
3538 if (seq1.length > seq2.length) {
3539 return false;
3540 }
3541 return true;
3542 }
3543
3544 /* pure */ public static boolean lexLTE(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3545 if (seq1 == null) { return false; }
3546 if (seq2 == null) { return false; }
3547 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3548 for (int i = 0 ; i < minlength ; i++) {
3549 if (gt(seq1[i], seq2[i])) {
3550 return false;
3551 } else if (lt(seq1[i], seq2[i])) {
3552 return true;
3553 }
3554 }
3555 if (seq1.length > seq2.length) {
3556 return false;
3557 }
3558 return true;
3559 }
3560
3561 /**
3562 * Returns true iff seq1 is lexically > to seq2.
3563 */
3564 /* pure */ public static boolean lexGT(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3565 if (seq1 == null) { return false; }
3566 if (seq2 == null) { return false; }
3567 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3568 for (int i = 0 ; i < minlength ; i++) {
3569 if (lt(seq1[i], seq2[i])) {
3570 return false;
3571 } else if (gt(seq1[i], seq2[i])) {
3572 return true;
3573 }
3574 }
3575 if (seq1.length <= seq2.length) {
3576 return false;
3577 }
3578 return true;
3579 }
3580
3581 /* pure */ public static boolean lexGT(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3582 if (seq1 == null) { return false; }
3583 if (seq2 == null) { return false; }
3584 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3585 for (int i = 0 ; i < minlength ; i++) {
3586 if (lt(seq1[i], seq2[i])) {
3587 return false;
3588 } else if (gt(seq1[i], seq2[i])) {
3589 return true;
3590 }
3591 }
3592 if (seq1.length <= seq2.length) {
3593 return false;
3594 }
3595 return true;
3596 }
3597
3598 /**
3599 * Returns true iff seq1 is lexically >= to seq2.
3600 */
3601 /* pure */ public static boolean lexGTE(double /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
3602 if (seq1 == null) { return false; }
3603 if (seq2 == null) { return false; }
3604 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3605 for (int i = 0 ; i < minlength ; i++) {
3606 if (lt(seq1[i], seq2[i])) {
3607 return false;
3608 } else if (gt(seq1[i], seq2[i])) {
3609 return true;
3610 }
3611 }
3612 if (seq1.length < seq2.length) {
3613 return false;
3614 }
3615 return true;
3616 }
3617
3618 /* pure */ public static boolean lexGTE(double /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
3619 if (seq1 == null) { return false; }
3620 if (seq2 == null) { return false; }
3621 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
3622 for (int i = 0 ; i < minlength ; i++) {
3623 if (lt(seq1[i], seq2[i])) {
3624 return false;
3625 } else if (gt(seq1[i], seq2[i])) {
3626 return true;
3627 }
3628 }
3629 if (seq1.length < seq2.length) {
3630 return false;
3631 }
3632 return true;
3633 }
3634
3635 /** True iff for all applicable i, every seq[i] == seq[i+1].
3636 *
3637 * Meaning (in pseudo-FOL):
3638 *
3639 * forall i in { 0..seq.length-2 } : seq[i] == seq[i+1]
3640 *
3641 */
3642 /* pure */ public static boolean eltwiseEqual(double /*@Nullable*/ [] seq) {
3643 if (seq == null) { return false; }
3644 for (int i = 0 ; i < seq.length ; i++) {
3645 if (i < seq.length-1) {
3646 if (ne(seq[i], seq[i+1])) {
3647 return false;
3648 }
3649 }
3650 }
3651 return true;
3652 }
3653
3654 /** True iff for all applicable i, every seq[i] != seq[i+1].
3655 *
3656 * Meaning (in pseudo-FOL):
3657 *
3658 * forall i in { 0..seq.length-2 } : seq[i] != seq[i+1]
3659 *
3660 */
3661 /* pure */ public static boolean eltwiseNotEqual(double /*@Nullable*/ [] seq) {
3662 if (seq == null) { return false; }
3663 for (int i = 0 ; i < seq.length ; i++) {
3664 if (i < seq.length-1) {
3665 if (eq(seq[i], seq[i+1])) {
3666 return false;
3667 }
3668 }
3669 }
3670 return true;
3671 }
3672
3673 /** True iff for all applicable i, every seq[i] < seq[i+1].
3674 *
3675 * Meaning (in pseudo-FOL):
3676 *
3677 * forall i in { 0..seq.length-2 } : seq[i] < seq[i+1]
3678 *
3679 */
3680 /* pure */ public static boolean eltwiseLT(double /*@Nullable*/ [] seq) {
3681 if (seq == null) { return false; }
3682 for (int i = 0 ; i < seq.length ; i++) {
3683 if (i < seq.length-1) {
3684 if (gte(seq[i], seq[i+1])) {
3685 return false;
3686 }
3687 }
3688 }
3689 return true;
3690 }
3691
3692 /** True iff for all applicable i, every seq[i] <= seq[i+1].
3693 *
3694 * Meaning (in pseudo-FOL):
3695 *
3696 * forall i in { 0..seq.length-2 } : seq[i] <= seq[i+1]
3697 *
3698 */
3699 /* pure */ public static boolean eltwiseLTE(double /*@Nullable*/ [] seq) {
3700 if (seq == null) { return false; }
3701 for (int i = 0 ; i < seq.length ; i++) {
3702 if (i < seq.length-1) {
3703 if (gt(seq[i], seq[i+1])) {
3704 return false;
3705 }
3706 }
3707 }
3708 return true;
3709 }
3710
3711 /** True iff for all applicable i, every seq[i] > seq[i+1].
3712 *
3713 * Meaning (in pseudo-FOL):
3714 *
3715 * forall i in { 0..seq.length-2 } : seq[i] > seq[i+1]
3716 *
3717 */
3718 /* pure */ public static boolean eltwiseGT(double /*@Nullable*/ [] seq) {
3719 if (seq == null) { return false; }
3720 for (int i = 0 ; i < seq.length ; i++) {
3721 if (i < seq.length-1) {
3722 if (lte(seq[i], seq[i+1])) {
3723 return false;
3724 }
3725 }
3726 }
3727 return true;
3728 }
3729
3730 /** True iff for all applicable i, every seq[i] >= seq[i+1].
3731 *
3732 * Meaning (in pseudo-FOL):
3733 *
3734 * forall i in { 0..seq.length-2 } : seq[i] >= seq[i+1]
3735 *
3736 */
3737 /* pure */ public static boolean eltwiseGTE(double /*@Nullable*/ [] seq) {
3738 if (seq == null) { return false; }
3739 for (int i = 0 ; i < seq.length ; i++) {
3740 if (i < seq.length-1) {
3741 if (lt(seq[i], seq[i+1])) {
3742 return false;
3743 }
3744 }
3745 }
3746 return true;
3747 }
3748
3749 /** True iff for all applicable i, every seq[i] == i.
3750 *
3751 * Meaning (in pseudo-FOL):
3752 *
3753 * forall i in { 0..seq.length-1 } : seq[i] == i
3754 *
3755 */
3756 /* pure */ public static boolean eltsEqualIndex(double /*@Nullable*/ [] seq) {
3757 if (seq == null) { return false; }
3758 for (int i = 0 ; i < seq.length ; i++) {
3759 if (ne(seq[i], i)) {
3760 return false;
3761 }
3762 }
3763 return true;
3764 }
3765
3766 /** True iff for all applicable i, every seq[i] != i.
3767 *
3768 * Meaning (in pseudo-FOL):
3769 *
3770 * forall i in { 0..seq.length-1 } : seq[i] != i
3771 *
3772 */
3773 /* pure */ public static boolean eltsNotEqualIndex(double /*@Nullable*/ [] seq) {
3774 if (seq == null) { return false; }
3775 for (int i = 0 ; i < seq.length ; i++) {
3776 if (eq(seq[i], i)) {
3777 return false;
3778 }
3779 }
3780 return true;
3781 }
3782
3783 /** True iff for all applicable i, every seq[i] < i.
3784 *
3785 * Meaning (in pseudo-FOL):
3786 *
3787 * forall i in { 0..seq.length-1 } : seq[i] < i
3788 *
3789 */
3790 /* pure */ public static boolean eltsLtIndex(double /*@Nullable*/ [] seq) {
3791 if (seq == null) { return false; }
3792 for (int i = 0 ; i < seq.length ; i++) {
3793 if (gte(seq[i], i)) {
3794 return false;
3795 }
3796 }
3797 return true;
3798 }
3799
3800 /** True iff for all applicable i, every seq[i] <= i.
3801 *
3802 * Meaning (in pseudo-FOL):
3803 *
3804 * forall i in { 0..seq.length-1 } : seq[i] <= i
3805 *
3806 */
3807 /* pure */ public static boolean eltsLteIndex(double /*@Nullable*/ [] seq) {
3808 if (seq == null) { return false; }
3809 for (int i = 0 ; i < seq.length ; i++) {
3810 if (gt(seq[i], i)) {
3811 return false;
3812 }
3813 }
3814 return true;
3815 }
3816
3817 /** True iff for all applicable i, every seq[i] > i.
3818 *
3819 * Meaning (in pseudo-FOL):
3820 *
3821 * forall i in { 0..seq.length-1 } : seq[i] > i
3822 *
3823 */
3824 /* pure */ public static boolean eltsGtIndex(double /*@Nullable*/ [] seq) {
3825 if (seq == null) { return false; }
3826 for (int i = 0 ; i < seq.length ; i++) {
3827 if (lte(seq[i], i)) {
3828 return false;
3829 }
3830 }
3831 return true;
3832 }
3833
3834 /** True iff for all applicable i, every seq[i] >= i.
3835 *
3836 * Meaning (in pseudo-FOL):
3837 *
3838 * forall i in { 0..seq.length-1 } : seq[i] >= i
3839 *
3840 */
3841 /* pure */ public static boolean eltsGteIndex(double /*@Nullable*/ [] seq) {
3842 if (seq == null) { return false; }
3843 for (int i = 0 ; i < seq.length ; i++) {
3844 if (lt(seq[i], i)) {
3845 return false;
3846 }
3847 }
3848 return true;
3849 }
3850
3851 /// Deferencing (accessing) fields
3852
3853 /**
3854 * collectdouble accepts an object and a list of fields (one of which is
3855 * of array type, and the rest of which are not), and produces an array in
3856 * which the original object has had the given fields accessed.
3857 *
3858 * Daikon creates invariants over "variables" such as the following.
3859 *
3860 * x.arr[].z The result of collecting all elements y.z for all y's
3861 * in array x.arr.
3862 * arr[].y.z The result of collecting all elements x.y.z for all x's
3863 * in array arr.
3864 * x.y.z[] The result of collecting all elements in array x.y.z[]
3865 *
3866 * The collectdouble() method does this collecting work.
3867 *
3868 * Given an object (x, arr, or x, correspondingly, in the above examples)
3869 * and a "field string" (arr.z, y.z, or y.z, correspondingly, in the
3870 * above example), the collect method collects the elements the result
3871 * from following the fields, one of which is assumed to be an array.
3872 *
3873 * requires: fieldStr.length() > 0 and object != null
3874 * requires: fieldStr contains only field names, no "[]" strings.
3875 *
3876 * requires: the method only works for field sequences with exactly
3877 * one field representing an array. For example, the collection
3878 * a[].b[].c will fail.
3879 *
3880 * If the resulting collection is of non-primitive type, then collect
3881 * returns an array of type Object[].
3882 *
3883 * Returns null if any array or field access causes an exception.
3884 */
3885 /* pure */ public static double /*@Nullable*/ [] collectdouble (Object object, String fieldStr) {
3886
3887 if (object == null) { return null; }
3888 if (fieldStr == null) { return null; }
3889
3890 //assert fieldStr != null && !"".equals(fieldStr);
3891 String[] fieldNames = fieldStr.split("\\.");
3892 double[] retval = collectdouble (object, fieldNames, 0);
3893 //System.err.println("%%% fieldArray returned: " + utilMDE.ArraysMDE.toString(retval));
3894 return retval;
3895 }
3896
3897 /** Helper method for collectdouble(Object, String).
3898 * Operates on the fields specified in fields[fieldsStartIdx..].
3899 * @see collectdouble(Object, String)
3900 */
3901 /* pure */ private static double /*@Nullable*/ [] collectdouble (Object object,
3902 String[] fields, int fieldsStartIdx) {
3903
3904 if (object == null) { return null; }
3905 assert (fields != null);
3906 assert (fieldsStartIdx >= 0 && fieldsStartIdx < fields.length);
3907
3908 Object fieldObj = null;
3909 try {
3910 Field field = (object instanceof java.lang.Class<?>)
3911 ? ((Class<?>)object).getDeclaredField(fields[fieldsStartIdx])
3912 : object.getClass().getDeclaredField(fields[fieldsStartIdx]);
3913 field.setAccessible(true);
3914 // Class cls = field.getType();
3915 fieldObj = field.get(object);
3916 //System.out.println("***fieldObj="+fieldObj);
3917
3918 } catch (Exception e) {
3919 return null;
3920
3921 }
3922
3923 if (fieldObj == null) {
3924 return null;
3925 }
3926
3927 // base case: just accessed the last field
3928 if (fields.length - 1 == fieldsStartIdx) {
3929
3930 if (fieldObj.getClass().isArray()) {
3931 // last field is an array
3932 return (double[])fieldObj;
3933 } else {
3934 // This hack should be removed in favor of, at "oneEltArray = ..."
3935 // below, calling a version of collectdouble_field that throws an
3936 // error. Then, this case becomes a run-time error. -MDE
3937
3938 // Just one element; return a one-element array.
3939 //assert cls.equals(Double.TYPE);
3940 return new double[] { ((Double)fieldObj).doubleValue() };
3941 }
3942 } else {
3943 // recursive case: more fields to access after this one
3944
3945 if (daikon.ProglangType.list_implementors.contains(fieldObj.getClass().getName())) {
3946
3947 java.util.AbstractCollection<?> collection = (java.util.AbstractCollection<?>)fieldObj;
3948 double[] intermediate = new double[collection.size()];
3949 int index = 0;
3950 for (Iterator<?> i = collection.iterator() ; i.hasNext() ; ) {
3951 double[] oneEltArray = collectdouble (i.next(), fields, fieldsStartIdx + 1);
3952 //assert oneEltArray.length == 1;
3953 intermediate[index++] = oneEltArray[0];
3954 }
3955 return intermediate;
3956 } else if (fieldObj.getClass().isArray()) {
3957
3958 // collect elements across array
3959 double[] intermediate = new double[Array.getLength(fieldObj)];
3960 for (int i = 0 ; i < intermediate.length ; i++) {
3961 double[] oneEltArray = collectdouble (Array.get(fieldObj, i),
3962 fields, fieldsStartIdx + 1);
3963 //assert oneEltArray.length == 1;
3964 intermediate[i] = oneEltArray[0];
3965 }
3966 return intermediate;
3967 } else {
3968
3969 return collectdouble (fieldObj, fields, fieldsStartIdx + 1);
3970 }
3971 }
3972 }
3973
3974 // Returns the results of dereferencing the fields specified in
3975 // fields[fieldsStartIdx..] for 'object'.
3976 // Returns a default value if any field access causes an exception.
3977 /* pure */ public static double collectdouble_field (Object object, String fieldStr) {
3978
3979 if (object == null) { return Double.NaN; } // return default value
3980 if (fieldStr == null) { return Double.NaN; } // return default value
3981
3982 String[] fieldNames = fieldStr.split("\\.");
3983
3984 // Holds the intermediate (and final) result
3985 Object fieldObj = object;
3986
3987 for (int i = 0 ; i < fieldNames.length ; i++) {
3988
3989 String fieldName = fieldNames[i];
3990
3991 try {
3992 Field field =
3993 (fieldObj instanceof java.lang.Class<?>)
3994 ? ((Class<?>)fieldObj).getDeclaredField(fieldName)
3995 : fieldObj.getClass().getDeclaredField(fieldName);
3996 field.setAccessible(true);
3997 fieldObj = field.get(fieldObj);
3998
3999 } catch (Exception e) {
4000 return Double.NaN; // return default value
4001
4002 }
4003
4004 }
4005
4006 return ((Double)fieldObj).doubleValue();
4007 }
4008
4009 ///////////////////////////////////////////////////////////////////////////
4010 /// Methods for "float" (from QuantBody.java.jpp)
4011 ///
4012
4013 /** Returns the ith element of the array or collection argument.
4014 * If the argument is null or not an array or collection, returns a
4015 * default value (Float.NaN).
4016 **/
4017 /* pure */ public static float getElement_float (Object o, long i) {
4018 if (o == null) { return Float.NaN; } // return default value
4019 java.lang.Class<?> c = o.getClass();
4020 if (c.isArray()) {
4021 return java.lang.reflect.Array.getFloat (o, (int)i);
4022 } else if (o instanceof java.util.AbstractCollection<?>) {
4023 return java.lang.reflect.Array.getFloat (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
4024 } else {
4025 return Float.NaN; // return default value
4026 }
4027 }
4028
4029 /* pure */ public static float getElement_float (float[] arr, long i) {
4030 if (arr == null) { return Float.NaN; } // return default value
4031 return arr[(int)i];
4032 }
4033
4034 private static boolean eq(float x, float y) {
4035 return fuzzy.eq(x,y);
4036 }
4037
4038 private static boolean ne(float x, float y) {
4039 return fuzzy.ne(x,y);
4040 }
4041
4042 private static boolean lt(float x, float y) {
4043 return fuzzy.lt(x,y);
4044 }
4045
4046 private static boolean lte(float x, float y) {
4047 return fuzzy.lte(x,y);
4048 }
4049
4050 private static boolean gt(float x, float y) {
4051 return fuzzy.gt(x,y);
4052 }
4053
4054 private static boolean gte(float x, float y) {
4055 return fuzzy.gte(x,y);
4056 }
4057
4058 /** True iff both sequences are non-null and have the same length. */
4059 /* pure */ public static boolean sameLength(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4060 return ((seq1 != null)
4061 && (seq2 != null)
4062 && seq1.length == seq2.length);
4063 }
4064
4065 /** True iff both sequences are non-null and have the same length. */
4066 /* pure */ public static boolean sameLength(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4067 return ((seq1 != null)
4068 && (seq2 != null)
4069 && seq1.length == seq2.length);
4070 }
4071
4072 /** True iff both sequences have the same length, and all seq2[i] divide seq1[i].
4073 *
4074 * Meaning (in pseudo-FOL):
4075 *
4076 * <pre>
4077 * /\ seq1.length == seq2.length
4078 * /\ forall i in { 0..seq2.length-1 } : seq2[i] divides seq1[i]
4079 * </pre>
4080 *
4081 */
4082 /* pure */ public static boolean pairwiseDivides(float[] seq1, float[] seq2) {
4083 if (! sameLength(seq1, seq2)) { return false; }
4084 assert seq1 != null && seq2 != null; // because sameLength() = true
4085 for (int i = 0 ; i < seq1.length ; i++) {
4086 if (ne(seq1[i] % seq2[i], 0)) {
4087 return false;
4088 }
4089 }
4090 return true;
4091 }
4092 /* pure */ public static boolean pairwiseDivides(float[] seq1, double[] seq2) {
4093 if (! sameLength(seq1, seq2)) { return false; }
4094 assert seq1 != null && seq2 != null; // because sameLength() = true
4095 for (int i = 0 ; i < seq1.length ; i++) {
4096 if (ne(seq1[i] % seq2[i], 0)) {
4097 return false;
4098 }
4099 }
4100 return true;
4101 }
4102
4103 /** True iff both sequences have the same length, and all seq1[i] == seq2[i] * seq2[i].
4104 *
4105 * Meaning (in pseudo-FOL):
4106 *
4107 * <pre>
4108 * /\ seq1.length == seq2.length
4109 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == seq2[i] * seq2[i]
4110 * </pre>
4111 *
4112 */
4113 /* pure */ public static boolean pairwiseSquare(float[] seq1, float[] seq2) {
4114 if (! sameLength(seq1, seq2)) { return false; }
4115 assert seq1 != null && seq2 != null; // because sameLength() = true
4116 for (int i = 0 ; i < seq1.length ; i++) {
4117 if (ne(seq1[i], seq2[i] * seq2[i])) {
4118 return false;
4119 }
4120 }
4121 return true;
4122 }
4123 /* pure */ public static boolean pairwiseSquare(float[] seq1, double[] seq2) {
4124 if (! sameLength(seq1, seq2)) { return false; }
4125 assert seq1 != null && seq2 != null; // because sameLength() = true
4126 for (int i = 0 ; i < seq1.length ; i++) {
4127
4128 if (ne(seq1[i], seq2[i] * seq2[i])) {
4129
4130 return false;
4131 }
4132 }
4133 return true;
4134 }
4135
4136 /**
4137 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
4138 * If either array is null, returns null.
4139 * If either array is empty, returns only those elements in the other array.
4140 * If both arrays are empty, returns a new empty array.
4141 */
4142 /* pure */ public static float /*@PolyNull*/ [] concat(float /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
4143 if (seq1 == null) { return null; }
4144 if (seq2 == null) { return null; }
4145 return utilMDE.ArraysMDE.concat(seq1, seq2);
4146 }
4147
4148 /* pure */ public static double /*@PolyNull*/ [] concat(float /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
4149 if (seq1 == null) { return null; }
4150 if (seq2 == null) { return null; }
4151 // Cannot just use utilMDE.ArraysMDE.concat because the two arrays
4152 // have different types. This essentially inlines that method.
4153 int newLength = seq1.length + seq2.length;
4154 double[] retval = new double[newLength];
4155
4156 for (int j = 0 ; j < seq1.length ; j++) {
4157 retval[j] = seq1[j];
4158 }
4159 System.arraycopy(seq2, 0, retval, seq1.length, seq2.length);
4160
4161 return retval;
4162 }
4163
4164 /**
4165 * Returns an array that is equivalent to the set union of seq1 and seq2.
4166 * This method gives no assurances about the order or repetition of elements:
4167 * elements may be repeated, and their order may be different from the
4168 * order of elements in seq1 and seq2.
4169 */
4170 /* pure */ public static float /*@PolyNull*/ [] union(float /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
4171 if (seq1 == null) { return null; }
4172 if (seq2 == null) { return null; }
4173 return concat(seq1, seq2);
4174 }
4175
4176 /* pure */ public static double /*@PolyNull*/ [] union(float /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
4177 if (seq1 == null) { return null; }
4178 if (seq2 == null) { return null; }
4179 return concat(seq1, seq2);
4180 }
4181
4182 /**
4183 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
4184 * This method gives no assurances about the order or repetition of elements:
4185 * elements may be repeated, and their order may be different from the
4186 * order of elements in seq1 and seq2.
4187 */
4188 /* pure */ public static float /*@PolyNull*/ [] intersection(float /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
4189 if (seq1 == null) { return null; }
4190 if (seq2 == null) { return null; }
4191 float[] intermediate = new float[Math.min(seq1.length, seq2.length)];
4192 int length = 0;
4193 for (int i = 0 ; i < seq1.length ; i++) {
4194 if (memberOf(seq1[i], seq2) ) {
4195 intermediate[length++] = seq1[i];
4196 }
4197 }
4198 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
4199 }
4200
4201 /* pure */ public static double /*@PolyNull*/ [] intersection(float /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
4202 if (seq1 == null) { return null; }
4203 if (seq2 == null) { return null; }
4204 double[] intermediate = new double[Math.min(seq1.length, seq2.length)];
4205 int length = 0;
4206 for (int i = 0 ; i < seq1.length ; i++) {
4207 if (memberOf(seq1[i], seq2) ) {
4208 intermediate[length++] = seq1[i];
4209 }
4210 }
4211 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
4212 }
4213
4214 /**
4215 * Returns an array that is equivalent to the set difference of seq1 and seq2.
4216 * This method gives no assurances about the order or repetition of elements:
4217 * elements may be repeated, and their order may be different from the
4218 * order of elements in seq1 and seq2.
4219 */
4220 /* pure */ public static float /*@PolyNull*/ [] setDiff(float /*@PolyNull*/ [] seq1, float /*@PolyNull*/ [] seq2) {
4221 if (seq1 == null) { return null; }
4222 if (seq2 == null) { return null; }
4223 float[] intermediate = new float[seq1.length];
4224 int length = 0;
4225 for (int i = 0 ; i < seq1.length ; i++) {
4226 if (!memberOf(seq1[i], seq2)) {
4227 intermediate[length++] = seq1[i];
4228 }
4229 }
4230 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
4231 }
4232
4233 /* pure */ public static double /*@PolyNull*/ [] setDiff(float /*@PolyNull*/ [] seq1, double /*@PolyNull*/ [] seq2) {
4234 if (seq1 == null) { return null; }
4235 if (seq2 == null) { return null; }
4236 double[] intermediate = new double[seq1.length];
4237 int length = 0;
4238 for (int i = 0 ; i < seq1.length ; i++) {
4239 if (!memberOf(seq1[i], seq2)) {
4240 intermediate[length++] = seq1[i];
4241 }
4242 }
4243 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
4244 }
4245
4246 /**
4247 * Retuns true iff seq1 and seq2 are equal when considered as sets.
4248 */
4249 /* pure */ public static boolean setEqual(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4250 if (seq1 == null) { return false; }
4251 if (seq2 == null) { return false; }
4252 for (int i = 0; i < seq1.length ; i++) {
4253 if (!memberOf(seq1[i], seq2) ) {
4254 return false;
4255 }
4256 }
4257 for (int i = 0; i < seq2.length ; i++) {
4258 if (!memberOf(seq2[i], seq1) ) {
4259 return false;
4260 }
4261 }
4262 return true;
4263 }
4264
4265 /* pure */ public static boolean setEqual(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4266 if (seq1 == null) { return false; }
4267 if (seq2 == null) { return false; }
4268 for (int i = 0; i < seq1.length ; i++) {
4269 if (!memberOf(seq1[i], seq2) ) {
4270 return false;
4271 }
4272 }
4273 for (int i = 0; i < seq2.length ; i++) {
4274 if (!memberOf(seq2[i], seq1) ) {
4275 return false;
4276 }
4277 }
4278 return true;
4279 }
4280
4281 /** True iff seq1 is the reverse of seq2.
4282 *
4283 * Meaning (in pseudo-FOL):
4284 *
4285 * <pre>
4286 * /\ seq1.length == seq2.length
4287 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
4288 * </pre>
4289 *
4290 */
4291 /* pure */ public static boolean isReverse(float[] seq1, float[] seq2) {
4292 if (! sameLength(seq1, seq2)) { return false; }
4293 assert seq1 != null && seq2 != null; // because sameLength() = true
4294 int length = seq1.length;
4295 for (int i = 0 ; i < length ; i++) {
4296 if (ne(seq1[i], seq2[length - i - 1])) {
4297 return false;
4298 }
4299 }
4300 return true;
4301 }
4302
4303 /* pure */ public static boolean isReverse(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4304 if (! sameLength(seq1, seq2)) { return false; }
4305 assert seq1 != null && seq2 != null; // because sameLength() = true
4306 int length = seq1.length;
4307 for (int i = 0 ; i < length ; i++) {
4308 if (ne(seq1[i], seq2[length - i - 1])) {
4309 return false;
4310 }
4311 }
4312 return true;
4313 }
4314
4315 /**
4316 * True iff seq1 is a subset of seq2, when the sequences are
4317 * considered as sets.
4318 */
4319 /* pure */ public static boolean subsetOf(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4320 if (seq1 == null) { return false; }
4321 if (seq2 == null) { return false; }
4322 for (int i = 0 ; i < seq1.length ; i++) {
4323 if (!memberOf(seq1[i], seq2)) {
4324 return false;
4325 }
4326 }
4327 return true;
4328 }
4329
4330 /* pure */ public static boolean subsetOf(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4331 if (seq1 == null) { return false; }
4332 if (seq2 == null) { return false; }
4333 for (int i = 0 ; i < seq1.length ; i++) {
4334 if (!memberOf(seq1[i], seq2)) {
4335 return false;
4336 }
4337 }
4338 return true;
4339 }
4340
4341 /**
4342 * Returns true iff seq contains no duplicate elements.
4343 */
4344 /* pure */ public static boolean noDups(float /*@Nullable*/ [] seq) {
4345 if (seq == null) { return false; }
4346 return utilMDE.ArraysMDE.noDuplicates(seq);
4347 }
4348
4349 /**
4350 * Returns true iff elt is in array arr.
4351 */
4352 /* pure */ public static boolean memberOf(float elt, float /*@Nullable*/ [] arr) {
4353 if (arr == null) { return false; }
4354 for (int i = 0 ; i < arr.length ; i++) {
4355 if (eq(arr[i], elt)) { return true; }
4356 }
4357 return false;
4358 }
4359
4360 /* pure */ public static boolean memberOf(float elt, double /*@Nullable*/ [] arr) {
4361 if (arr == null) { return false; }
4362 for (int i = 0 ; i < arr.length ; i++) {
4363 if (eq(arr[i], elt)) { return true; }
4364 }
4365 return false;
4366 }
4367
4368 /**
4369 * Returns a subsequence of seq with first elements seq[start] and
4370 * last element seq[end].
4371 */
4372 /* pure */ public static float /*@PolyNull*/ [] slice(float /*@PolyNull*/ [] seq, int start, int end) {
4373 if (seq == null) { return null; }
4374 int sliceStart = start;
4375 int sliceEnd = end;
4376 if (start < 0) { return new float[] { }; }
4377 if (end > seq.length-1) { return new float[] { }; }
4378 if (sliceStart > sliceEnd) { return new float[] { }; }
4379 int length = sliceEnd - sliceStart + 1;
4380 return utilMDE.ArraysMDE.subarray(seq, sliceStart, length);
4381 }
4382
4383 /* pure */ public static float /*@PolyNull*/ [] slice(float /*@PolyNull*/ [] seq, long start, int end) {
4384 return slice(seq, (int)start, end);
4385 }
4386 /* pure */ public static float /*@PolyNull*/ [] slice(float /*@PolyNull*/ [] seq, int start, long end) {
4387 return slice(seq, start, (int)end);
4388 }
4389 /* pure */ public static float /*@PolyNull*/ [] slice(float /*@PolyNull*/ [] seq, long start, long end) {
4390 return slice(seq, (int)start, (int)end);
4391 }
4392
4393 /** True iff all elements in arr equal elt.
4394 *
4395 * Meaning (in pseudo-FOL):
4396 *
4397 * forall i in { 0..arr.length-1 } : arr[i] == elt
4398 *
4399 */
4400 /* pure */ public static boolean eltsEqual(float /*@Nullable*/ [] arr, float elt) {
4401 if (arr == null) { return false; }
4402 for (int i = 0 ; i < arr.length ; i++) {
4403 if (ne(arr[i], elt)) { return false; }
4404 }
4405 return true;
4406 }
4407
4408 /* pure */ public static boolean eltsEqual(float /*@Nullable*/ [] arr, double elt) {
4409 if (arr == null) { return false; }
4410 for (int i = 0 ; i < arr.length ; i++) {
4411 if (ne(arr[i], elt)) { return false; }
4412 }
4413 return true;
4414 }
4415
4416 /** True iff every element in arr does not equal elt.
4417 *
4418 * Meaning (in pseudo-FOL):
4419 *
4420 * forall i in { 0..arr.length-1 } : arr[i] != elt
4421 *
4422 */
4423 /* pure */ public static boolean eltsNotEqual(float /*@Nullable*/ [] arr, float elt) {
4424 if (arr == null) { return false; }
4425 for (int i = 0 ; i < arr.length ; i++) {
4426 if (eq(arr[i], elt)) { return false; }
4427 }
4428 return true;
4429 }
4430
4431 /* pure */ public static boolean eltsNotEqual(float /*@Nullable*/ [] arr, double elt) {
4432 if (arr == null) { return false; }
4433 for (int i = 0 ; i < arr.length ; i++) {
4434 if (eq(arr[i], elt)) { return false; }
4435 }
4436 return true;
4437 }
4438
4439 /** True iff every element in arr is greater than elt.
4440 *
4441 * Meaning (in pseudo-FOL):
4442 *
4443 * forall i in { 0..arr.length-1 } : arr[i] > elt
4444 *
4445 */
4446 /* pure */ public static boolean eltsGT(float /*@Nullable*/ [] arr, float elt) {
4447 if (arr == null) { return false; }
4448 for (int i = 0 ; i < arr.length ; i++) {
4449 if (lte(arr[i], elt)) { return false; }
4450 }
4451 return true;
4452 }
4453
4454 /* pure */ public static boolean eltsGT(float /*@Nullable*/ [] arr, double elt) {
4455 if (arr == null) { return false; }
4456 for (int i = 0 ; i < arr.length ; i++) {
4457 if (lte(arr[i], elt)) { return false; }
4458 }
4459 return true;
4460 }
4461
4462 /** True iff every element in arr is greater than or equal to elt.
4463 *
4464 * Meaning (in pseudo-FOL):
4465 *
4466 * forall i in { 0..arr.length-1 } : arr[i] >= elt
4467 *
4468 */
4469 /* pure */ public static boolean eltsGTE(float /*@Nullable*/ [] arr, float elt) {
4470 if (arr == null) { return false; }
4471 for (int i = 0 ; i < arr.length ; i++) {
4472 if (lt(arr[i], elt)) { return false; }
4473 }
4474 return true;
4475 }
4476
4477 /* pure */ public static boolean eltsGTE(float /*@Nullable*/ [] arr, double elt) {
4478 if (arr == null) { return false; }
4479 for (int i = 0 ; i < arr.length ; i++) {
4480 if (lt(arr[i], elt)) { return false; }
4481 }
4482 return true;
4483 }
4484
4485 /** True iff every element in arr is less than elt.
4486 *
4487 * Meaning (in pseudo-FOL):
4488 *
4489 * forall i in { 0..arr.length-1 } : arr[i] < elt
4490 *
4491 */
4492 /* pure */ public static boolean eltsLT(float /*@Nullable*/ [] arr, float elt) {
4493 if (arr == null) { return false; }
4494 for (int i = 0 ; i < arr.length ; i++) {
4495 if (gte(arr[i], elt)) { return false; }
4496 }
4497 return true;
4498 }
4499
4500 /* pure */ public static boolean eltsLT(float /*@Nullable*/ [] arr, double elt) {
4501 if (arr == null) { return false; }
4502 for (int i = 0 ; i < arr.length ; i++) {
4503 if (gte(arr[i], elt)) { return false; }
4504 }
4505 return true;
4506 }
4507
4508 /** True iff every element in arr is less than or equal to elt.
4509 *
4510 * Meaning (in pseudo-FOL):
4511 *
4512 * forall i in { 0..arr.length-1 } : arr[i] <= elt
4513 *
4514 */
4515 /* pure */ public static boolean eltsLTE(float /*@Nullable*/ [] arr, float elt) {
4516 if (arr == null) { return false; }
4517 for (int i = 0 ; i < arr.length ; i++) {
4518 if (gt(arr[i], elt)) { return false; }
4519 }
4520 return true;
4521 }
4522
4523 /* pure */ public static boolean eltsLTE(float /*@Nullable*/ [] arr, double elt) {
4524 if (arr == null) { return false; }
4525 for (int i = 0 ; i < arr.length ; i++) {
4526 if (gt(arr[i], elt)) { return false; }
4527 }
4528 return true;
4529 }
4530
4531 /** True iff seq1 and seq2 have the same length, and every seq1[i] == seq2[i].
4532 *
4533 * Meaning (in pseudo-FOL):
4534 *
4535 * /\ seq1.length == se2.length
4536 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[i]
4537 *
4538 */
4539
4540 /* pure */ public static boolean pairwiseEqual(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4541 if (! sameLength(seq1, seq2)) { return false; }
4542 assert seq1 != null && seq2 != null; // because sameLength() = true
4543 for (int i = 0 ; i < seq1.length ; i++) {
4544 if (Float.isNaN(seq1[i]) && Float.isNaN(seq2[i])) {
4545 continue;
4546 }
4547 if (ne(seq1[i], seq2[i])) {
4548 return false;
4549 }
4550 }
4551 return true;
4552 }
4553
4554 /* pure */ public static boolean pairwiseEqual(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4555 if (! sameLength(seq1, seq2)) { return false; }
4556 assert seq1 != null && seq2 != null; // because sameLength() = true
4557 for (int i = 0 ; i < seq1.length ; i++) {
4558 if (ne(seq1[i], seq2[i])) {
4559 return false;
4560 }
4561 }
4562 return true;
4563 }
4564
4565 /** True iff seq1 and seq2 have the same length, and every seq1[i] != seq2[i].
4566 *
4567 * Meaning (in pseudo-FOL):
4568 *
4569 * /\ seq1.length == se2.length
4570 * /\ forall i in { 0..seq1.length-1 } : seq1[i] != seq2[i]
4571 *
4572 */
4573 /* pure */ public static boolean pairwiseNotEqual(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4574 if (! sameLength(seq1, seq2)) { return false; }
4575 assert seq1 != null && seq2 != null; // because sameLength() = true
4576 for (int i = 0 ; i < seq1.length ; i++) {
4577 if (eq(seq1[i], seq2[i])) {
4578 return false;
4579 }
4580 }
4581 return true;
4582 }
4583
4584 /* pure */ public static boolean pairwiseNotEqual(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4585 if (! sameLength(seq1, seq2)) { return false; }
4586 assert seq1 != null && seq2 != null; // because sameLength() = true
4587 for (int i = 0 ; i < seq1.length ; i++) {
4588 if (eq(seq1[i], seq2[i])) {
4589 return false;
4590 }
4591 }
4592 return true;
4593 }
4594
4595 /** True iff seq1 and seq2 have the same length, and every seq1[i] < seq2[i].
4596 *
4597 * Meaning (in pseudo-FOL):
4598 *
4599 * /\ seq1.length == se2.length
4600 * /\ forall i in { 0..seq1.length-1 } : seq1[i] < seq2[i]
4601 *
4602 */
4603 /* pure */ public static boolean pairwiseLT(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4604 if (! sameLength(seq1, seq2)) { return false; }
4605 assert seq1 != null && seq2 != null; // because sameLength() = true
4606 for (int i = 0 ; i < seq1.length ; i++) {
4607 if (gte(seq1[i], seq2[i])) {
4608 return false;
4609 }
4610 }
4611 return true;
4612 }
4613
4614 /* pure */ public static boolean pairwiseLT(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4615 if (! sameLength(seq1, seq2)) { return false; }
4616 assert seq1 != null && seq2 != null; // because sameLength() = true
4617 for (int i = 0 ; i < seq1.length ; i++) {
4618 if (gte(seq1[i], seq2[i])) {
4619 return false;
4620 }
4621 }
4622 return true;
4623 }
4624
4625 /** True iff seq1 and seq2 have the same length, and every seq1[i] <= seq2[i].
4626 * Meaning (in pseudo-FOL):
4627 *
4628 * /\ seq1.length == se2.length
4629 * /\ forall i in { 0..seq1.length-1 } : seq1[i] <= seq2[i]
4630 *
4631 */
4632 /* pure */ public static boolean pairwiseLTE(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4633 if (! sameLength(seq1, seq2)) { return false; }
4634 assert seq1 != null && seq2 != null; // because sameLength() = true
4635 for (int i = 0 ; i < seq1.length ; i++) {
4636 if (gt(seq1[i], seq2[i])) {
4637 return false;
4638 }
4639 }
4640 return true;
4641 }
4642
4643 /* pure */ public static boolean pairwiseLTE(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4644 if (! sameLength(seq1, seq2)) { return false; }
4645 assert seq1 != null && seq2 != null; // because sameLength() = true
4646 for (int i = 0 ; i < seq1.length ; i++) {
4647 if (gt(seq1[i], seq2[i])) {
4648 return false;
4649 }
4650 }
4651 return true;
4652 }
4653
4654 /** True iff seq1 and seq2 have the same length, and every seq1[i] > seq2[i].
4655 * Meaning (in pseudo-FOL):
4656 *
4657 * /\ seq1.length == se2.length
4658 * /\ forall i in { 0..seq1.length-1 } : seq1[i] > seq2[i]
4659 *
4660 */
4661 /* pure */ public static boolean pairwiseGT(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4662 if (! sameLength(seq1, seq2)) { return false; }
4663 assert seq1 != null && seq2 != null; // because sameLength() = true
4664 for (int i = 0 ; i < seq1.length ; i++) {
4665 if (lte(seq1[i], seq2[i])) {
4666 return false;
4667 }
4668 }
4669 return true;
4670 }
4671
4672 /* pure */ public static boolean pairwiseGT(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4673 if (! sameLength(seq1, seq2)) { return false; }
4674 assert seq1 != null && seq2 != null; // because sameLength() = true
4675 for (int i = 0 ; i < seq1.length ; i++) {
4676 if (lte(seq1[i], seq2[i])) {
4677 return false;
4678 }
4679 }
4680 return true;
4681 }
4682
4683 /** True iff seq1 and seq2 have the same length, and every seq1[i] >= seq2[i].
4684 * Meaning (in pseudo-FOL):
4685 *
4686 * /\ seq1.length == se2.length
4687 * /\ forall i in { 0..seq1.length-1 } : seq1[i] >= seq2[i]
4688 *
4689 */
4690 /* pure */ public static boolean pairwiseGTE(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4691 if (! sameLength(seq1, seq2)) { return false; }
4692 assert seq1 != null && seq2 != null; // because sameLength() = true
4693 for (int i = 0 ; i < seq1.length ; i++) {
4694 if (lt(seq1[i], seq2[i])) {
4695 return false;
4696 }
4697 }
4698 return true;
4699 }
4700
4701 /* pure */ public static boolean pairwiseGTE(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4702 if (! sameLength(seq1, seq2)) { return false; }
4703 assert seq1 != null && seq2 != null; // because sameLength() = true
4704 for (int i = 0 ; i < seq1.length ; i++) {
4705 if (lt(seq1[i], seq2[i])) {
4706 return false;
4707 }
4708 }
4709 return true;
4710 }
4711
4712 /**
4713 * Returns true iff seq1 is lexically equal to seq2.
4714 * For equality, "lexically" and "pairwise" are the same.
4715 */
4716 /* pure */ public static boolean lexEqual(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4717 if (seq1 == null) { return false; }
4718 if (seq2 == null) { return false; }
4719 return pairwiseEqual(seq1, seq2);
4720 }
4721
4722 /* pure */ public static boolean lexEqual(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4723 if (seq1 == null) { return false; }
4724 if (seq2 == null) { return false; }
4725 return pairwiseEqual(seq1, seq2);
4726 }
4727
4728 /**
4729 * Returns true iff seq1 is lexically not equal to seq2.
4730 */
4731 /* pure */ public static boolean lexNotEqual(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4732 if (seq1 == null) { return false; }
4733 if (seq2 == null) { return false; }
4734 return !lexEqual(seq1, seq2);
4735 }
4736
4737 /* pure */ public static boolean lexNotEqual(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4738 if (seq1 == null) { return false; }
4739 if (seq2 == null) { return false; }
4740 return !lexEqual(seq1, seq2);
4741 }
4742
4743 /**
4744 * Returns true iff seq1 is lexically < seq2.
4745 */
4746 /* pure */ public static boolean lexLT(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4747 if (seq1 == null) { return false; }
4748 if (seq2 == null) { return false; }
4749 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4750 for (int i = 0 ; i < minlength ; i++) {
4751 if (gt(seq1[i], seq2[i])) {
4752 return false;
4753 } else if (lt(seq1[i], seq2[i])) {
4754 return true;
4755 }
4756 }
4757 if (seq1.length >= seq2.length) {
4758 return false;
4759 }
4760 return true;
4761 }
4762
4763 /* pure */ public static boolean lexLT(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4764 if (seq1 == null) { return false; }
4765 if (seq2 == null) { return false; }
4766 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4767 for (int i = 0 ; i < minlength ; i++) {
4768 if (gt(seq1[i], seq2[i])) {
4769 return false;
4770 } else if (lt(seq1[i], seq2[i])) {
4771 return true;
4772 }
4773 }
4774 if (seq1.length >= seq2.length) {
4775 return false;
4776 }
4777 return true;
4778 }
4779
4780 /**
4781 * Returns true iff seq1 is lexically <= to seq2.
4782 */
4783 /* pure */ public static boolean lexLTE(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4784 if (seq1 == null) { return false; }
4785 if (seq2 == null) { return false; }
4786 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4787 for (int i = 0 ; i < minlength ; i++) {
4788 if (gt(seq1[i], seq2[i])) {
4789 return false;
4790 } else if (lt(seq1[i], seq2[i])) {
4791 return true;
4792 }
4793 }
4794 if (seq1.length > seq2.length) {
4795 return false;
4796 }
4797 return true;
4798 }
4799
4800 /* pure */ public static boolean lexLTE(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4801 if (seq1 == null) { return false; }
4802 if (seq2 == null) { return false; }
4803 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4804 for (int i = 0 ; i < minlength ; i++) {
4805 if (gt(seq1[i], seq2[i])) {
4806 return false;
4807 } else if (lt(seq1[i], seq2[i])) {
4808 return true;
4809 }
4810 }
4811 if (seq1.length > seq2.length) {
4812 return false;
4813 }
4814 return true;
4815 }
4816
4817 /**
4818 * Returns true iff seq1 is lexically > to seq2.
4819 */
4820 /* pure */ public static boolean lexGT(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4821 if (seq1 == null) { return false; }
4822 if (seq2 == null) { return false; }
4823 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4824 for (int i = 0 ; i < minlength ; i++) {
4825 if (lt(seq1[i], seq2[i])) {
4826 return false;
4827 } else if (gt(seq1[i], seq2[i])) {
4828 return true;
4829 }
4830 }
4831 if (seq1.length <= seq2.length) {
4832 return false;
4833 }
4834 return true;
4835 }
4836
4837 /* pure */ public static boolean lexGT(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4838 if (seq1 == null) { return false; }
4839 if (seq2 == null) { return false; }
4840 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4841 for (int i = 0 ; i < minlength ; i++) {
4842 if (lt(seq1[i], seq2[i])) {
4843 return false;
4844 } else if (gt(seq1[i], seq2[i])) {
4845 return true;
4846 }
4847 }
4848 if (seq1.length <= seq2.length) {
4849 return false;
4850 }
4851 return true;
4852 }
4853
4854 /**
4855 * Returns true iff seq1 is lexically >= to seq2.
4856 */
4857 /* pure */ public static boolean lexGTE(float /*@Nullable*/ [] seq1, float /*@Nullable*/ [] seq2) {
4858 if (seq1 == null) { return false; }
4859 if (seq2 == null) { return false; }
4860 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4861 for (int i = 0 ; i < minlength ; i++) {
4862 if (lt(seq1[i], seq2[i])) {
4863 return false;
4864 } else if (gt(seq1[i], seq2[i])) {
4865 return true;
4866 }
4867 }
4868 if (seq1.length < seq2.length) {
4869 return false;
4870 }
4871 return true;
4872 }
4873
4874 /* pure */ public static boolean lexGTE(float /*@Nullable*/ [] seq1, double /*@Nullable*/ [] seq2) {
4875 if (seq1 == null) { return false; }
4876 if (seq2 == null) { return false; }
4877 int minlength = (seq1.length < seq2.length) ? seq1.length : seq2.length;
4878 for (int i = 0 ; i < minlength ; i++) {
4879 if (lt(seq1[i], seq2[i])) {
4880 return false;
4881 } else if (gt(seq1[i], seq2[i])) {
4882 return true;
4883 }
4884 }
4885 if (seq1.length < seq2.length) {
4886 return false;
4887 }
4888 return true;
4889 }
4890
4891 /** True iff for all applicable i, every seq[i] == seq[i+1].
4892 *
4893 * Meaning (in pseudo-FOL):
4894 *
4895 * forall i in { 0..seq.length-2 } : seq[i] == seq[i+1]
4896 *
4897 */
4898 /* pure */ public static boolean eltwiseEqual(float /*@Nullable*/ [] seq) {
4899 if (seq == null) { return false; }
4900 for (int i = 0 ; i < seq.length ; i++) {
4901 if (i < seq.length-1) {
4902 if (ne(seq[i], seq[i+1])) {
4903 return false;
4904 }
4905 }
4906 }
4907 return true;
4908 }
4909
4910 /** True iff for all applicable i, every seq[i] != seq[i+1].
4911 *
4912 * Meaning (in pseudo-FOL):
4913 *
4914 * forall i in { 0..seq.length-2 } : seq[i] != seq[i+1]
4915 *
4916 */
4917 /* pure */ public static boolean eltwiseNotEqual(float /*@Nullable*/ [] seq) {
4918 if (seq == null) { return false; }
4919 for (int i = 0 ; i < seq.length ; i++) {
4920 if (i < seq.length-1) {
4921 if (eq(seq[i], seq[i+1])) {
4922 return false;
4923 }
4924 }
4925 }
4926 return true;
4927 }
4928
4929 /** True iff for all applicable i, every seq[i] < seq[i+1].
4930 *
4931 * Meaning (in pseudo-FOL):
4932 *
4933 * forall i in { 0..seq.length-2 } : seq[i] < seq[i+1]
4934 *
4935 */
4936 /* pure */ public static boolean eltwiseLT(float /*@Nullable*/ [] seq) {
4937 if (seq == null) { return false; }
4938 for (int i = 0 ; i < seq.length ; i++) {
4939 if (i < seq.length-1) {
4940 if (gte(seq[i], seq[i+1])) {
4941 return false;
4942 }
4943 }
4944 }
4945 return true;
4946 }
4947
4948 /** True iff for all applicable i, every seq[i] <= seq[i+1].
4949 *
4950 * Meaning (in pseudo-FOL):
4951 *
4952 * forall i in { 0..seq.length-2 } : seq[i] <= seq[i+1]
4953 *
4954 */
4955 /* pure */ public static boolean eltwiseLTE(float /*@Nullable*/ [] seq) {
4956 if (seq == null) { return false; }
4957 for (int i = 0 ; i < seq.length ; i++) {
4958 if (i < seq.length-1) {
4959 if (gt(seq[i], seq[i+1])) {
4960 return false;
4961 }
4962 }
4963 }
4964 return true;
4965 }
4966
4967 /** True iff for all applicable i, every seq[i] > seq[i+1].
4968 *
4969 * Meaning (in pseudo-FOL):
4970 *
4971 * forall i in { 0..seq.length-2 } : seq[i] > seq[i+1]
4972 *
4973 */
4974 /* pure */ public static boolean eltwiseGT(float /*@Nullable*/ [] seq) {
4975 if (seq == null) { return false; }
4976 for (int i = 0 ; i < seq.length ; i++) {
4977 if (i < seq.length-1) {
4978 if (lte(seq[i], seq[i+1])) {
4979 return false;
4980 }
4981 }
4982 }
4983 return true;
4984 }
4985
4986 /** True iff for all applicable i, every seq[i] >= seq[i+1].
4987 *
4988 * Meaning (in pseudo-FOL):
4989 *
4990 * forall i in { 0..seq.length-2 } : seq[i] >= seq[i+1]
4991 *
4992 */
4993 /* pure */ public static boolean eltwiseGTE(float /*@Nullable*/ [] seq) {
4994 if (seq == null) { return false; }
4995 for (int i = 0 ; i < seq.length ; i++) {
4996 if (i < seq.length-1) {
4997 if (lt(seq[i], seq[i+1])) {
4998 return false;
4999 }
5000 }
5001 }
5002 return true;
5003 }
5004
5005 /** True iff for all applicable i, every seq[i] == i.
5006 *
5007 * Meaning (in pseudo-FOL):
5008 *
5009 * forall i in { 0..seq.length-1 } : seq[i] == i
5010 *
5011 */
5012 /* pure */ public static boolean eltsEqualIndex(float /*@Nullable*/ [] seq) {
5013 if (seq == null) { return false; }
5014 for (int i = 0 ; i < seq.length ; i++) {
5015 if (ne(seq[i], i)) {
5016 return false;
5017 }
5018 }
5019 return true;
5020 }
5021
5022 /** True iff for all applicable i, every seq[i] != i.
5023 *
5024 * Meaning (in pseudo-FOL):
5025 *
5026 * forall i in { 0..seq.length-1 } : seq[i] != i
5027 *
5028 */
5029 /* pure */ public static boolean eltsNotEqualIndex(float /*@Nullable*/ [] seq) {
5030 if (seq == null) { return false; }
5031 for (int i = 0 ; i < seq.length ; i++) {
5032 if (eq(seq[i], i)) {
5033 return false;
5034 }
5035 }
5036 return true;
5037 }
5038
5039 /** True iff for all applicable i, every seq[i] < i.
5040 *
5041 * Meaning (in pseudo-FOL):
5042 *
5043 * forall i in { 0..seq.length-1 } : seq[i] < i
5044 *
5045 */
5046 /* pure */ public static boolean eltsLtIndex(float /*@Nullable*/ [] seq) {
5047 if (seq == null) { return false; }
5048 for (int i = 0 ; i < seq.length ; i++) {
5049 if (gte(seq[i], i)) {
5050 return false;
5051 }
5052 }
5053 return true;
5054 }
5055
5056 /** True iff for all applicable i, every seq[i] <= i.
5057 *
5058 * Meaning (in pseudo-FOL):
5059 *
5060 * forall i in { 0..seq.length-1 } : seq[i] <= i
5061 *
5062 */
5063 /* pure */ public static boolean eltsLteIndex(float /*@Nullable*/ [] seq) {
5064 if (seq == null) { return false; }
5065 for (int i = 0 ; i < seq.length ; i++) {
5066 if (gt(seq[i], i)) {
5067 return false;
5068 }
5069 }
5070 return true;
5071 }
5072
5073 /** True iff for all applicable i, every seq[i] > i.
5074 *
5075 * Meaning (in pseudo-FOL):
5076 *
5077 * forall i in { 0..seq.length-1 } : seq[i] > i
5078 *
5079 */
5080 /* pure */ public static boolean eltsGtIndex(float /*@Nullable*/ [] seq) {
5081 if (seq == null) { return false; }
5082 for (int i = 0 ; i < seq.length ; i++) {
5083 if (lte(seq[i], i)) {
5084 return false;
5085 }
5086 }
5087 return true;
5088 }
5089
5090 /** True iff for all applicable i, every seq[i] >= i.
5091 *
5092 * Meaning (in pseudo-FOL):
5093 *
5094 * forall i in { 0..seq.length-1 } : seq[i] >= i
5095 *
5096 */
5097 /* pure */ public static boolean eltsGteIndex(float /*@Nullable*/ [] seq) {
5098 if (seq == null) { return false; }
5099 for (int i = 0 ; i < seq.length ; i++) {
5100 if (lt(seq[i], i)) {
5101 return false;
5102 }
5103 }
5104 return true;
5105 }
5106
5107 /// Deferencing (accessing) fields
5108
5109 /**
5110 * collectfloat accepts an object and a list of fields (one of which is
5111 * of array type, and the rest of which are not), and produces an array in
5112 * which the original object has had the given fields accessed.
5113 *
5114 * Daikon creates invariants over "variables" such as the following.
5115 *
5116 * x.arr[].z The result of collecting all elements y.z for all y's
5117 * in array x.arr.
5118 * arr[].y.z The result of collecting all elements x.y.z for all x's
5119 * in array arr.
5120 * x.y.z[] The result of collecting all elements in array x.y.z[]
5121 *
5122 * The collectfloat() method does this collecting work.
5123 *
5124 * Given an object (x, arr, or x, correspondingly, in the above examples)
5125 * and a "field string" (arr.z, y.z, or y.z, correspondingly, in the
5126 * above example), the collect method collects the elements the result
5127 * from following the fields, one of which is assumed to be an array.
5128 *
5129 * requires: fieldStr.length() > 0 and object != null
5130 * requires: fieldStr contains only field names, no "[]" strings.
5131 *
5132 * requires: the method only works for field sequences with exactly
5133 * one field representing an array. For example, the collection
5134 * a[].b[].c will fail.
5135 *
5136 * If the resulting collection is of non-primitive type, then collect
5137 * returns an array of type Object[].
5138 *
5139 * Returns null if any array or field access causes an exception.
5140 */
5141 /* pure */ public static float /*@Nullable*/ [] collectfloat (Object object, String fieldStr) {
5142
5143 if (object == null) { return null; }
5144 if (fieldStr == null) { return null; }
5145
5146 //assert fieldStr != null && !"".equals(fieldStr);
5147 String[] fieldNames = fieldStr.split("\\.");
5148 float[] retval = collectfloat (object, fieldNames, 0);
5149 //System.err.println("%%% fieldArray returned: " + utilMDE.ArraysMDE.toString(retval));
5150 return retval;
5151 }
5152
5153 /** Helper method for collectfloat(Object, String).
5154 * Operates on the fields specified in fields[fieldsStartIdx..].
5155 * @see collectfloat(Object, String)
5156 */
5157 /* pure */ private static float /*@Nullable*/ [] collectfloat (Object object,
5158 String[] fields, int fieldsStartIdx) {
5159
5160 if (object == null) { return null; }
5161 assert (fields != null);
5162 assert (fieldsStartIdx >= 0 && fieldsStartIdx < fields.length);
5163
5164 Object fieldObj = null;
5165 try {
5166 Field field = (object instanceof java.lang.Class<?>)
5167 ? ((Class<?>)object).getDeclaredField(fields[fieldsStartIdx])
5168 : object.getClass().getDeclaredField(fields[fieldsStartIdx]);
5169 field.setAccessible(true);
5170 // Class cls = field.getType();
5171 fieldObj = field.get(object);
5172 //System.out.println("***fieldObj="+fieldObj);
5173
5174 } catch (Exception e) {
5175 return null;
5176
5177 }
5178
5179 if (fieldObj == null) {
5180 return null;
5181 }
5182
5183 // base case: just accessed the last field
5184 if (fields.length - 1 == fieldsStartIdx) {
5185
5186 if (fieldObj.getClass().isArray()) {
5187 // last field is an array
5188 return (float[])fieldObj;
5189 } else {
5190 // This hack should be removed in favor of, at "oneEltArray = ..."
5191 // below, calling a version of collectfloat_field that throws an
5192 // error. Then, this case becomes a run-time error. -MDE
5193
5194 // Just one element; return a one-element array.
5195 //assert cls.equals(Float.TYPE);
5196 return new float[] { ((Float)fieldObj).floatValue() };
5197 }
5198 } else {
5199 // recursive case: more fields to access after this one
5200
5201 if (daikon.ProglangType.list_implementors.contains(fieldObj.getClass().getName())) {
5202
5203 java.util.AbstractCollection<?> collection = (java.util.AbstractCollection<?>)fieldObj;
5204 float[] intermediate = new float[collection.size()];
5205 int index = 0;
5206 for (Iterator<?> i = collection.iterator() ; i.hasNext() ; ) {
5207 float[] oneEltArray = collectfloat (i.next(), fields, fieldsStartIdx + 1);
5208 //assert oneEltArray.length == 1;
5209 intermediate[index++] = oneEltArray[0];
5210 }
5211 return intermediate;
5212 } else if (fieldObj.getClass().isArray()) {
5213
5214 // collect elements across array
5215 float[] intermediate = new float[Array.getLength(fieldObj)];
5216 for (int i = 0 ; i < intermediate.length ; i++) {
5217 float[] oneEltArray = collectfloat (Array.get(fieldObj, i),
5218 fields, fieldsStartIdx + 1);
5219 //assert oneEltArray.length == 1;
5220 intermediate[i] = oneEltArray[0];
5221 }
5222 return intermediate;
5223 } else {
5224
5225 return collectfloat (fieldObj, fields, fieldsStartIdx + 1);
5226 }
5227 }
5228 }
5229
5230 // Returns the results of dereferencing the fields specified in
5231 // fields[fieldsStartIdx..] for 'object'.
5232 // Returns a default value if any field access causes an exception.
5233 /* pure */ public static float collectfloat_field (Object object, String fieldStr) {
5234
5235 if (object == null) { return Float.NaN; } // return default value
5236 if (fieldStr == null) { return Float.NaN; } // return default value
5237
5238 String[] fieldNames = fieldStr.split("\\.");
5239
5240 // Holds the intermediate (and final) result
5241 Object fieldObj = object;
5242
5243 for (int i = 0 ; i < fieldNames.length ; i++) {
5244
5245 String fieldName = fieldNames[i];
5246
5247 try {
5248 Field field =
5249 (fieldObj instanceof java.lang.Class<?>)
5250 ? ((Class<?>)fieldObj).getDeclaredField(fieldName)
5251 : fieldObj.getClass().getDeclaredField(fieldName);
5252 field.setAccessible(true);
5253 fieldObj = field.get(fieldObj);
5254
5255 } catch (Exception e) {
5256 return Float.NaN; // return default value
5257
5258 }
5259
5260 }
5261
5262 return ((Float)fieldObj).floatValue();
5263 }
5264
5265 ///////////////////////////////////////////////////////////////////////////
5266 /// Methods for "int" (from QuantBody.java.jpp)
5267 ///
5268
5269 /** Returns the ith element of the array or collection argument.
5270 * If the argument is null or not an array or collection, returns a
5271 * default value (Integer.MAX_VALUE).
5272 **/
5273 /* pure */ public static int getElement_int (Object o, long i) {
5274 if (o == null) { return Integer.MAX_VALUE; } // return default value
5275 java.lang.Class<?> c = o.getClass();
5276 if (c.isArray()) {
5277 return java.lang.reflect.Array.getInt (o, (int)i);
5278 } else if (o instanceof java.util.AbstractCollection<?>) {
5279 return java.lang.reflect.Array.getInt (((java.util.AbstractCollection<?>)o).toArray(), (int)i);
5280 } else {
5281 return Integer.MAX_VALUE; // return default value
5282 }
5283 }
5284
5285 /* pure */ public static int getElement_int (int[] arr, long i) {
5286 if (arr == null) { return Integer.MAX_VALUE; } // return default value
5287 return arr[(int)i];
5288 }
5289
5290 private static boolean eq(int x, int y) {
5291 return (x == y);
5292 }
5293
5294 private static boolean ne(int x, int y) {
5295 return x != y;
5296 }
5297
5298 private static boolean lt(int x, int y) {
5299 return x < y;
5300 }
5301
5302 private static boolean lte(int x, int y) {
5303 return x <= y;
5304 }
5305
5306 private static boolean gt(int x, int y) {
5307 return x > y;
5308 }
5309
5310 private static boolean gte(int x, int y) {
5311 return x >= y;
5312 }
5313
5314 /** True iff both sequences are non-null and have the same length. */
5315 /* pure */ public static boolean sameLength(int /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
5316 return ((seq1 != null)
5317 && (seq2 != null)
5318 && seq1.length == seq2.length);
5319 }
5320
5321 /** True iff both sequences are non-null and have the same length. */
5322 /* pure */ public static boolean sameLength(int /*@Nullable*/ [] seq1, long /*@Nullable*/ [] seq2) {
5323 return ((seq1 != null)
5324 && (seq2 != null)
5325 && seq1.length == seq2.length);
5326 }
5327
5328 /** True iff both sequences have the same length, and all seq2[i] divide seq1[i].
5329 *
5330 * Meaning (in pseudo-FOL):
5331 *
5332 * <pre>
5333 * /\ seq1.length == seq2.length
5334 * /\ forall i in { 0..seq2.length-1 } : seq2[i] divides seq1[i]
5335 * </pre>
5336 *
5337 */
5338 /* pure */ public static boolean pairwiseDivides(int[] seq1, int[] seq2) {
5339 if (! sameLength(seq1, seq2)) { return false; }
5340 assert seq1 != null && seq2 != null; // because sameLength() = true
5341 for (int i = 0 ; i < seq1.length ; i++) {
5342 if (ne(seq1[i] % seq2[i], 0)) {
5343 return false;
5344 }
5345 }
5346 return true;
5347 }
5348 /* pure */ public static boolean pairwiseDivides(int[] seq1, long[] seq2) {
5349 if (! sameLength(seq1, seq2)) { return false; }
5350 assert seq1 != null && seq2 != null; // because sameLength() = true
5351 for (int i = 0 ; i < seq1.length ; i++) {
5352 if (ne(seq1[i] % seq2[i], 0)) {
5353 return false;
5354 }
5355 }
5356 return true;
5357 }
5358
5359 /** True iff both sequences have the same length, and all seq1[i] == seq2[i] * seq2[i].
5360 *
5361 * Meaning (in pseudo-FOL):
5362 *
5363 * <pre>
5364 * /\ seq1.length == seq2.length
5365 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == seq2[i] * seq2[i]
5366 * </pre>
5367 *
5368 */
5369 /* pure */ public static boolean pairwiseSquare(int[] seq1, int[] seq2) {
5370 if (! sameLength(seq1, seq2)) { return false; }
5371 assert seq1 != null && seq2 != null; // because sameLength() = true
5372 for (int i = 0 ; i < seq1.length ; i++) {
5373 if (ne(seq1[i], seq2[i] * seq2[i])) {
5374 return false;
5375 }
5376 }
5377 return true;
5378 }
5379 /* pure */ public static boolean pairwiseSquare(int[] seq1, long[] seq2) {
5380 if (! sameLength(seq1, seq2)) { return false; }
5381 assert seq1 != null && seq2 != null; // because sameLength() = true
5382 for (int i = 0 ; i < seq1.length ; i++) {
5383
5384 if (ne(seq1[i], seq2[i] * seq2[i])) {
5385
5386 return false;
5387 }
5388 }
5389 return true;
5390 }
5391
5392 /** True iff both sequences have the same length, and all seq1[i] == ~ seq2[i].
5393 *
5394 * Meaning (in pseudo-FOL):
5395 *
5396 * <pre>
5397 * /\ seq1.length == seq2.length
5398 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == ~ seq2[i]
5399 * </pre>
5400 *
5401 */
5402 /* pure */ public static boolean pairwiseBitwiseComplement(int[] seq1, int[] seq2) {
5403 if (! sameLength(seq1, seq2)) { return false; }
5404 assert seq1 != null && seq2 != null; // because sameLength() = true
5405 for (int i = 0 ; i < seq1.length ; i++) {
5406 if (seq1[i] != ~seq2[i]) {
5407 return false;
5408 }
5409 }
5410 return true;
5411 }
5412 /* pure */ public static boolean pairwiseBitwiseComplement(int[] seq1, long[] seq2) {
5413 if (! sameLength(seq1, seq2)) { return false; }
5414 assert seq1 != null && seq2 != null; // because sameLength() = true
5415 for (int i = 0 ; i < seq1.length ; i++) {
5416 if (seq1[i] != ~seq2[i]) {
5417 return false;
5418 }
5419 }
5420 return true;
5421 }
5422
5423 /* pure */ public static boolean pairwiseBitwiseComplement(Object[] seq1, Object[] seq2) {
5424 if (! sameLength(seq1, seq2)) { return false; }
5425 assert seq1 != null && seq2 != null; // because sameLength() = true
5426 if (! eltsNonNull(seq1)) { return false; }
5427 if (! eltsNonNull(seq2)) { return false; }
5428 int[] hashArr1 = new int[seq1.length];
5429 for (int i = 0 ; i < seq1.length ; i++) {
5430 hashArr1[i] = seq1[i].hashCode();
5431 }
5432 int[] hashArr2 = new int[seq2.length];
5433 for (int i = 0 ; i < seq2.length ; i++) {
5434 hashArr2[i] = seq2[i].hashCode();
5435 }
5436 return pairwiseBitwiseComplement(hashArr1, hashArr2);
5437 }
5438
5439 /** True iff both sequences have the same length, and all seq1[i] == (seq2[i] | seq1[i]).
5440 *
5441 * Meaning (in pseudo-FOL):
5442 *
5443 * <pre>
5444 * /\ seq1.length == seq2.length
5445 * /\ forall i in { 0..seq2.length-1 } : seq1[i] == (seq2[i] | seq1[i])
5446 * </pre>
5447 *
5448 */
5449 /* pure */ public static boolean pairwiseBitwiseSubset(int[] seq1, int[] seq2) {
5450 if (seq1 == null) { return false; }
5451 if (seq2 == null) { return false; }
5452 if (seq1.length != seq2.length) {
5453 return false;
5454 }
5455 for (int i = 0 ; i < seq1.length ; i++) {
5456 if (ne(seq1[i], (seq2[i] | seq1[i]))) {
5457 return false;
5458 }
5459 }
5460 return true;
5461 }
5462 /* pure */ public static boolean pairwiseBitwiseSubset(int[] seq1, long[] seq2) {
5463 if (! sameLength(seq1, seq2)) { return false; }
5464 assert seq1 != null && seq2 != null; // because sameLength() = true
5465 for (int i = 0 ; i < seq1.length ; i++) {
5466 if (ne(seq1[i], (seq2[i] | seq1[i]))) {
5467 return false;
5468 }
5469 }
5470 return true;
5471 }
5472
5473 /* pure */ public static boolean pairwiseBitwiseSubset(Object[] seq1, Object[] seq2) {
5474 if (! sameLength(seq1, seq2)) { return false; }
5475 assert seq1 != null && seq2 != null; // because sameLength() = true
5476 if (! eltsNonNull(seq1)) { return false; }
5477 if (! eltsNonNull(seq2)) { return false; }
5478 int[] hashArr1 = new int[seq1.length];
5479 for (int i = 0 ; i < seq1.length ; i++) {
5480 hashArr1[i] = seq1[i].hashCode();
5481 }
5482 int[] hashArr2 = new int[seq2.length];
5483 for (int i = 0 ; i < seq2.length ; i++) {
5484 hashArr2[i] = seq2[i].hashCode();
5485 }
5486 return pairwiseBitwiseSubset(hashArr1, hashArr2);
5487 }
5488
5489 /**
5490 * Returns the array { seq1[0], ..., seq1[seq1.length-1], seq2[0], ... , seq2[seq2.length-1] }
5491 * If either array is null, returns null.
5492 * If either array is empty, returns only those elements in the other array.
5493 * If both arrays are empty, returns a new empty array.
5494 */
5495 /* pure */ public static int /*@PolyNull*/ [] concat(int /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
5496 if (seq1 == null) { return null; }
5497 if (seq2 == null) { return null; }
5498 return utilMDE.ArraysMDE.concat(seq1, seq2);
5499 }
5500
5501 /* pure */ public static long /*@PolyNull*/ [] concat(int /*@PolyNull*/ [] seq1, long /*@PolyNull*/ [] seq2) {
5502 if (seq1 == null) { return null; }
5503 if (seq2 == null) { return null; }
5504 // Cannot just use utilMDE.ArraysMDE.concat because the two arrays
5505 // have different types. This essentially inlines that method.
5506 int newLength = seq1.length + seq2.length;
5507 long[] retval = new long[newLength];
5508
5509 for (int j = 0 ; j < seq1.length ; j++) {
5510 retval[j] = seq1[j];
5511 }
5512 System.arraycopy(seq2, 0, retval, seq1.length, seq2.length);
5513
5514 return retval;
5515 }
5516
5517 /**
5518 * Returns an array that is equivalent to the set union of seq1 and seq2.
5519 * This method gives no assurances about the order or repetition of elements:
5520 * elements may be repeated, and their order may be different from the
5521 * order of elements in seq1 and seq2.
5522 */
5523 /* pure */ public static int /*@PolyNull*/ [] union(int /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
5524 if (seq1 == null) { return null; }
5525 if (seq2 == null) { return null; }
5526 return concat(seq1, seq2);
5527 }
5528
5529 /* pure */ public static long /*@PolyNull*/ [] union(int /*@PolyNull*/ [] seq1, long /*@PolyNull*/ [] seq2) {
5530 if (seq1 == null) { return null; }
5531 if (seq2 == null) { return null; }
5532 return concat(seq1, seq2);
5533 }
5534
5535 /**
5536 * Returns an array that is equivalent to the set intersection of seq1 and seq2.
5537 * This method gives no assurances about the order or repetition of elements:
5538 * elements may be repeated, and their order may be different from the
5539 * order of elements in seq1 and seq2.
5540 */
5541 /* pure */ public static int /*@PolyNull*/ [] intersection(int /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
5542 if (seq1 == null) { return null; }
5543 if (seq2 == null) { return null; }
5544 int[] intermediate = new int[Math.min(seq1.length, seq2.length)];
5545 int length = 0;
5546 for (int i = 0 ; i < seq1.length ; i++) {
5547 if (memberOf(seq1[i], seq2) ) {
5548 intermediate[length++] = seq1[i];
5549 }
5550 }
5551 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
5552 }
5553
5554 /* pure */ public static long /*@PolyNull*/ [] intersection(int /*@PolyNull*/ [] seq1, long /*@PolyNull*/ [] seq2) {
5555 if (seq1 == null) { return null; }
5556 if (seq2 == null) { return null; }
5557 long[] intermediate = new long[Math.min(seq1.length, seq2.length)];
5558 int length = 0;
5559 for (int i = 0 ; i < seq1.length ; i++) {
5560 if (memberOf(seq1[i], seq2) ) {
5561 intermediate[length++] = seq1[i];
5562 }
5563 }
5564 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
5565 }
5566
5567 /**
5568 * Returns an array that is equivalent to the set difference of seq1 and seq2.
5569 * This method gives no assurances about the order or repetition of elements:
5570 * elements may be repeated, and their order may be different from the
5571 * order of elements in seq1 and seq2.
5572 */
5573 /* pure */ public static int /*@PolyNull*/ [] setDiff(int /*@PolyNull*/ [] seq1, int /*@PolyNull*/ [] seq2) {
5574 if (seq1 == null) { return null; }
5575 if (seq2 == null) { return null; }
5576 int[] intermediate = new int[seq1.length];
5577 int length = 0;
5578 for (int i = 0 ; i < seq1.length ; i++) {
5579 if (!memberOf(seq1[i], seq2)) {
5580 intermediate[length++] = seq1[i];
5581 }
5582 }
5583 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
5584 }
5585
5586 /* pure */ public static long /*@PolyNull*/ [] setDiff(int /*@PolyNull*/ [] seq1, long /*@PolyNull*/ [] seq2) {
5587 if (seq1 == null) { return null; }
5588 if (seq2 == null) { return null; }
5589 long[] intermediate = new long[seq1.length];
5590 int length = 0;
5591 for (int i = 0 ; i < seq1.length ; i++) {
5592 if (!memberOf(seq1[i], seq2)) {
5593 intermediate[length++] = seq1[i];
5594 }
5595 }
5596 return utilMDE.ArraysMDE.subarray(intermediate, 0, length);
5597 }
5598
5599 /**
5600 * Retuns true iff seq1 and seq2 are equal when considered as sets.
5601 */
5602 /* pure */ public static boolean setEqual(int /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
5603 if (seq1 == null) { return false; }
5604 if (seq2 == null) { return false; }
5605 for (int i = 0; i < seq1.length ; i++) {
5606 if (!memberOf(seq1[i], seq2) ) {
5607 return false;
5608 }
5609 }
5610 for (int i = 0; i < seq2.length ; i++) {
5611 if (!memberOf(seq2[i], seq1) ) {
5612 return false;
5613 }
5614 }
5615 return true;
5616 }
5617
5618 /* pure */ public static boolean setEqual(int /*@Nullable*/ [] seq1, long /*@Nullable*/ [] seq2) {
5619 if (seq1 == null) { return false; }
5620 if (seq2 == null) { return false; }
5621 for (int i = 0; i < seq1.length ; i++) {
5622 if (!memberOf(seq1[i], seq2) ) {
5623 return false;
5624 }
5625 }
5626 for (int i = 0; i < seq2.length ; i++) {
5627 if (!memberOf(seq2[i], seq1) ) {
5628 return false;
5629 }
5630 }
5631 return true;
5632 }
5633
5634 /** True iff seq1 is the reverse of seq2.
5635 *
5636 * Meaning (in pseudo-FOL):
5637 *
5638 * <pre>
5639 * /\ seq1.length == seq2.length
5640 * /\ forall i in { 0..seq1.length-1 } : seq1[i] == seq2[seq2.length-1-i]
5641 * </pre>
5642 *
5643 */
5644 /* pure */ public static boolean isReverse(int[] seq1, int[] seq2) {
5645 if (! sameLength(seq1, seq2)) { return false; }
5646 assert seq1 != null && seq2 != null; // because sameLength() = true
5647 int length = seq1.length;
5648 for (int i = 0 ; i < length ; i++) {
5649 if (ne(seq1[i], seq2[length - i - 1])) {
5650 return false;
5651 }
5652 }
5653 return true;
5654 }
5655
5656 /* pure */ public static boolean isReverse(int /*@Nullable*/ [] seq1, long /*@Nullable*/ [] seq2) {
5657 if (! sameLength(seq1, seq2)) { return false; }
5658 assert seq1 != null && seq2 != null; // because sameLength() = true
5659 int length = seq1.length;
5660 for (int i = 0 ; i < length ; i++) {
5661 if (ne(seq1[i], seq2[length - i - 1])) {
5662 return false;
5663 }
5664 }
5665 return true;
5666 }
5667
5668 /** True iff all elements in elts occur once or more in arr;
5669 * that is, elts is a subset of arr.
5670 *
5671 * Meaning (in pseudo-FOL):
5672 *
5673 * forall i in { 0..elt.length-1 } : elt[i] element_of arr
5674 *
5675 */
5676 /* pure */ public static boolean subsetOf(/*@Nullable*/ Object elts, /*@Nullable*/ Object arr) {
5677 if (arr == null) { return false; }
5678 if (elts == null) { return false; }
5679 if (!(elts.getClass().isArray() && arr.getClass().isArray())) {
5680 //throw new IllegalArgumentException("both arguments must be arrays.");
5681 return false;
5682 }
5683 // We know that the two arguments are arrays of different types; if
5684 // they had been of the same type, then one of the more specific
5685 // overriding versions of this method would have been called.
5686
5687 // This implementation simply calls either subsetOf(long[], long[]) or
5688 // subsetOf(double[], double[]).
5689
5690 Class<?> eltsType = elts.getClass().getComponentType();
5691 Class<?> arrType = arr.getClass().getComponentType();
5692 if (isIntegralType(eltsType) && isIntegralType(arrType)) {
5693 // Both arrays are int/long
5694 // Cast both arrays to long and call subsetOf(long[],long[])
5695 long[] elts_long;
5696 if (eltsType == Long.class) {
5697 elts_long = (long[]) elts;
5698 } else {
5699 elts_long = new long[Array.getLength(elts)];
5700 for (int i = 0 ; i < elts_long.length ; i++) {
5701 elts_long[i] = Array.getLong(elts, i);
5702 }
5703 }
5704 long[] arr_long;
5705 if (arrType == Long.class) {
5706 arr_long = (long[]) arr;
5707 } else {
5708 arr_long = new long[Array.getLength(arr)];
5709 for (int i = 0 ; i < arr_long.length ; i++) {
5710 arr_long[i] = Array.getLong(arr, i);
5711 }
5712 }
5713 return subsetOf(elts_long, arr_long);
5714 } else if (isNumericType(eltsType) && isNumericType(arrType)) {
5715 // At least one array is float/double.
5716 // Cast both arrays to double and call subsetOf(double[],double[])
5717 double[] elts_double = new double[Array.getLength(elts)];
5718 for (int i = 0 ; i < elts_double.length ; i++) {
5719 elts_double[i] = Array.getDouble(elts, i);
5720 }
5721 double[] arr_double = new double[Array.getLength(arr)];
5722 for (int i = 0 ; i < arr_double.length ; i++) {
5723 arr_double[i] = Array.getDouble(arr, i);
5724 }
5725 return subsetOf(elts_double, arr_double);
5726 } else {
5727 // throw new IllegalArgumentException("both arguments must be arrays of numeric types.");
5728 return false;
5729 }
5730
5731 }
5732
5733 /**
5734 * True iff seq1 is a subset of seq2, when the sequences are
5735 * considered as sets.
5736 */
5737 /* pure */ public static boolean subsetOf(int /*@Nullable*/ [] seq1, int /*@Nullable*/ [] seq2) {
5738 if (seq1 == null) { return false; }
5739 if (seq2 == null) { return false; }
5740 for (int i = 0 ; i < seq1.length ; i++) {
5741 if (!memberOf(seq1[i], seq2)) {
5742 return false;
5743 }
5744 }
5745 return true;
5746 }
5747
5748 /* pure */ public static boolean subsetOf(int /*@Nullable*/ [] seq1, long /*@Nullable*/ [] seq2) {
5749 if (seq1 == null) { return false; }
5750 if (seq2 == null) { return false; }
5751 for (int i = 0 ; i < seq1.length ; i++) {
5752 if (!memberOf(seq1[i], seq2)) {
5753 return false;
5754 }
5755 }
5756 return true;
5757 }
5758
5759 /**
5760 * Returns true iff seq contains no duplicate elements.
5761 */
5762 /* pure */ public static boolean noDups(int /*@Nullable*/ [] seq) {
5763 if (seq == null) { return false; }