Source code

001// ***** This file is automatically generated from SubSequence.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.derive.*;
007import daikon.derive.binary.*;
008import daikon.derive.ternary.*;
009import daikon.inv.*;
010import daikon.inv.unary.sequence.*;
011import daikon.suppress.*;
012import java.util.*;
013import java.util.logging.Level;
014import java.util.logging.Logger;
015import org.checkerframework.checker.lock.qual.GuardSatisfied;
016import org.checkerframework.checker.nullness.qual.NonNull;
017import org.checkerframework.checker.nullness.qual.Nullable;
018import org.checkerframework.dataflow.qual.Pure;
019import org.checkerframework.dataflow.qual.SideEffectFree;
020import org.plumelib.util.ArraysPlume;
021import org.plumelib.util.IPair;
022import org.plumelib.util.UtilPlume;
023import typequals.prototype.qual.NonPrototype;
024import typequals.prototype.qual.Prototype;
025
026/**
027 * Represents two sequences of long values where one sequence is a subsequence of the
028 * other. Prints as {@code x[] is a subsequence of y[]}.
029 */
030
031public class SubSequence extends TwoSequence {
032  static final long serialVersionUID = 20031024L;
033
034  private static final Logger debug =
035    Logger.getLogger("daikon.inv.binary.twoSequence.SubSequence");
036
037  // Variables starting with dkconfig_ should only be set via the
038  // daikon.config.Configuration interface.
039  /** Boolean. True iff SubSequence invariants should be considered. */
040  public static boolean dkconfig_enabled = false;
041
042  protected SubSequence(PptSlice ppt) {
043    super(ppt);
044  }
045
046  protected @Prototype SubSequence() {
047    super();
048  }
049
050  private static @Prototype SubSequence proto = new @Prototype SubSequence();
051
052  /** Returns the prototype invariant for SubSequence */
053  public static @Prototype SubSequence get_proto() {
054    return proto;
055  }
056
057  @Override
058  public boolean enabled() {
059    return dkconfig_enabled;
060  }
061
062  @Override
063  protected SubSequence instantiate_dyn(@Prototype SubSequence this, PptSlice slice) {
064    return new SubSequence(slice);
065  }
066
067  @Override
068  protected Invariant resurrect_done_swapped() {
069    return new SuperSequence(ppt);
070  }
071
072  @SideEffectFree
073  @Override
074  public String format_using(@GuardSatisfied SubSequence this, OutputFormat format) {
075    if (format == OutputFormat.DAIKON) {
076      return format_daikon();
077    }
078    if (format == OutputFormat.SIMPLIFY) {
079      return format_simplify();
080    }
081    if (format == OutputFormat.CSHARPCONTRACT) {
082      return format_csharp_contract();
083    }
084    if (format.isJavaFamily()) {
085      return format_unimplemented(format);
086    }
087
088    return format_unimplemented(format);
089  }
090
091  public String format_daikon(@GuardSatisfied SubSequence this) {
092    String v1 = var1().name();
093    String v2 = var2().name();
094    return v1 + " is a subsequence of " + v2;
095  }
096
097  public String format_csharp_contract(@GuardSatisfied SubSequence this) {
098    String v1 = var1().csharp_collection_string();
099    String v2 = var2().csharp_collection_string();
100    return v1 + ".IsSubsequence(" + v2 + ")";
101  }
102
103  public String format_simplify(@GuardSatisfied SubSequence this) {
104    if (Invariant.dkconfig_simplify_define_predicates) {
105      return format_simplify_defined();
106    } else {
107      return format_simplify_explicit();
108    }
109  }
110
111  private String format_simplify_defined(@GuardSatisfied SubSequence this) {
112    String[] sub_name = var1().simplifyNameAndBounds();
113    String[] super_name = var2().simplifyNameAndBounds();
114
115    if (sub_name == null || super_name == null) {
116        return String.format("%s.format_simplify_defined(%s): sub_name=%s, super_name=%s, for %s",
117                             getClass().getSimpleName(), this,
118                             Arrays.toString(sub_name), Arrays.toString(super_name), format());
119    }
120
121    return "(subsequence "
122      + sub_name[0] + " " + sub_name[1] + " " + sub_name[2] + " "
123      + super_name[0] + " " + super_name[1] + " " + super_name[2] + ")";
124  }
125
126  // This is apparently broken somehow, though from the logs it's not
127  // clear how. -- smcc
128  private String format_simplify_explicit(@GuardSatisfied SubSequence this) {
129    return "format_simplify disabled";
130
131    /* Since this doesn't work (since at least april 2003)
132       and it uses quant in complex ways,
133       its just commented out (jhp 8/3/2006)
134
135    // (exists k s.t. (forall i, j; (i bounds & j bounds & (i = j + k)) ==> ...))
136
137    QuantifyReturn qret = QuantHelper.quantify(new VarInfoName[]
138                                { var1().name, var2().name} );
139    assert qret.bound_vars.size() == 2;
140    assert qret.root_primes.length == 2;
141
142    // These variables are, in order: Example element, free Index
143    // variable, Lower bound, Upper bound, Span
144    String aE, aI, aL, aH, aS; // a = subsequence
145    String bE, bI, bL, bH, bS; // b = supersequence
146    {
147      VarInfoName[] boundv;
148
149      boundv = qret.bound_vars.get(0);
150      aE = qret.root_primes[0].simplify_name();
151      aI = boundv[0].simplify_name();
152      aL = boundv[1].simplify_name();
153      aH = boundv[2].simplify_name();
154      aS = "(+ (- " + aH + " " + aL + ") 1)";
155
156      boundv = qret.bound_vars.get(1);
157      bE = qret.root_primes[1].simplify_name();
158      bI = boundv[0].simplify_name();
159      bL = boundv[1].simplify_name();
160      bH = boundv[2].simplify_name();
161      bS = "(+ (- " + bH + " " + bL + ") 1)";
162    }
163
164    // This invariant would not have been given data if a value was
165    // missing - for example, if a slice had a negative length.  We
166    // must predicate this invariant on the values being sensible.
167
168    String sensible = "(AND (>= " + aS + " 0) (>= " + bS + " 0))";
169
170    // This invariant would have been falsified if the subsequence A
171    // length was ever zero.  Also, this invariant would have been
172    // falsified if the subsequence A was ever longer than the
173    // supersequence B.
174
175    String length_stmt = "(AND (NEQ " + aS + " 0) (>= " + bS + " " + aS + "))";
176
177    // Subsequence means that there exists an offset in supersequence
178    // B, where (1) the offset is non-negative, (2) the offset doesn't
179    // cause the matching to push past the end of B, and (3) for all
180    // indices less than the span of subsequence A, (4) the elements
181    // starting from A_low and B_low+offset are equal.
182
183    String index = "|__index|";
184    String shift = "|__shift|";
185    String subseq_stmt =
186      "(EXISTS (" + shift + ") (AND "
187      + "(<= 0 " + shift + ") "                          // 1
188      + "(<= (+ " + shift + " " + aS + ") " + bS + ") "  // 2
189      + "(FORALL (" + index + ") (IMPLIES (AND (<= 0 " + index + ") (< " + index + " " + aS + ")) " // 3
190      + "(EQ "
191      + aE.replace(aI, "(+ " + aL + " " + index + ")") + " "
192      + bE.replace(bI, "(+ (+ " + bL + " " + index + ") " + shift + ")") + ")))))";
193
194    // So, when this in sensible, we know that both the length and
195    // subseq statements hold.
196
197    String result = "(IMPLIES " + sensible + " (AND " + length_stmt + " " + subseq_stmt + "))";
198    return result;
199    */
200  }
201
202  @Override
203  public InvariantStatus check_modified(long[] a1, long[] a2,
204                                        int count) {
205    if ((a1 == null) || (a2 == null)) {
206      return InvariantStatus.FALSIFIED;
207    }
208
209      int result = ArraysPlume.indexOf(a2, a1);
210
211    if (result == -1) {
212      return InvariantStatus.FALSIFIED;
213    } else {
214      return InvariantStatus.NO_CHANGE;
215    }
216  }
217
218  @Override
219  public InvariantStatus add_modified(long[] a1, long[] a2,
220                                      int count) {
221    InvariantStatus is = check_modified(a1, a2, count);
222    if ((is == InvariantStatus.FALSIFIED) && Debug.logOn()) {
223      log("%s destroyed by %s %s",
224           format(), Debug.toString(a1),
225           Debug.toString(a2));
226    }
227    return is;
228  }
229
230  @Override
231  protected double computeConfidence() {
232    return Invariant.CONFIDENCE_JUSTIFIED;
233  }
234
235  /** Returns a DiscardInfo, or null if the Invariant is not an obvious subsequence.
236@return a DiscardInfo, or null if the Invariant is not an obvious subsequence  */
237  @Pure
238  public static @Nullable DiscardInfo isObviousSubSequence(Invariant inv, VarInfo subvar, VarInfo supervar) {
239    IPair<DiscardCode,String> pcds = isObviousSubSequence(subvar, supervar);
240    if (pcds == null) {
241      return null;
242    } else {
243      return new DiscardInfo(inv, pcds.first, pcds.second);
244    }
245  }
246
247  /**
248   * Returns a IPair of a DiscardCode and a discardReason string, or null if the Invariant is not an
249   * obvious subsequence.
250   * @return a IPair of a DiscardCode and a discardReason string, or null if the Invariant is not an
251   *   obvious subsequence
252   */
253  @Pure
254  public static @Nullable IPair<DiscardCode,String> isObviousSubSequence(VarInfo subvar, VarInfo supervar) {
255    // Must typecheck since this could be called with non-sequence variables in
256    // some methods.
257    ProglangType rep1 = subvar.rep_type;
258    ProglangType rep2 = supervar.rep_type;
259    if (!(((rep1 == ProglangType.INT_ARRAY)
260           && (rep2 == ProglangType.INT_ARRAY))
261          || ((rep1 == ProglangType.DOUBLE_ARRAY)
262           && (rep2 == ProglangType.DOUBLE_ARRAY))
263          || ((rep1 == ProglangType.STRING_ARRAY)
264           && (rep2 == ProglangType.STRING_ARRAY))
265          )) {
266      return null;
267    }
268
269    if (debug.isLoggable(Level.FINE)) {
270      debug.fine("isObviousSubSequence "
271                  + subvar.name() + " in " + supervar.name());
272    }
273
274    // Standard discard reason/string
275    DiscardCode discardCode = DiscardCode.obvious;
276    String discardString = subvar.name()+" obvious subset/subsequence of "+supervar.name();
277
278    // For unions and intersections, it probably doesn't make sense to
279    // do subsequence or subset detection.  This is mainly to prevent
280    // invariants of the form (x subset of union(x, y)) but this means
281    // we also miss those of the form (z subset of union(x,y)) which
282    // might be useful.  Subsequence, however, seems totally useless
283    // on unions and intersections.
284    if (supervar.derived instanceof  SequenceScalarIntersection
285        || supervar.derived instanceof SequenceScalarUnion
286        || subvar.derived instanceof SequenceScalarIntersection
287        || subvar.derived instanceof SequenceScalarUnion) {
288      discardCode = DiscardCode.obvious;
289      discardString = "Invariants involving subsets/subsequences of unions/intersections are suppressed";
290      debug.fine("  returning true because of union or intersection");
291      return IPair.<DiscardCode,String>of(discardCode, discardString);
292    }
293
294    if (subvar.derived instanceof SequencesPredicate) {
295      // It's not useful that predicate(x[], b[]) is a subsequence or subset
296      // of x[]
297      SequencesPredicate derived = (SequencesPredicate) subvar.derived;
298      if (derived.var1().equals(supervar)) {
299        discardCode = DiscardCode.obvious;
300        discardString = subvar.name()+" is derived from "+supervar.name();
301        debug.fine("  returning true because of predicate slicing");
302        return IPair.of(discardCode, discardString + " [pred slicing]");
303      }
304    }
305
306    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
307    if (subvar_super == null) {
308      // If it's not a union, intersection or a subsequence, it's not obvious
309      debug.fine("  returning false because subvar_super == null");
310      return null;
311    }
312
313    if (subvar_super == supervar) {
314      // System.out.println("SubSequence.isObviousDerived(" + subvar.name() + ", " + supervar.name + ") = true");
315      // System.out.println("  details: subvar_super=" + subvar_super.name + "; supervar_super=" + supervar.isDerivedSubSequenceOf() == null ? "null" : supervar.isDerivedSubSequenceOf().name);
316      discardCode = DiscardCode.obvious;
317      discardString = subvar.name()+"=="+supervar.name();
318      debug.fine("  returning true because subvar_super == supervar");
319      return IPair.of(discardCode,
320                     discardString + " [subvar_super == supervar]");
321    }
322
323    // a[i+a..j+b] cmp a[i+c..j+d]
324    VarInfo supervar_super = supervar.isDerivedSubSequenceOf();
325    // we know subvar_super != null due to check above
326    if (subvar_super == supervar_super) {
327      // both sequences are derived from the same supersequence
328      if ((subvar.derived instanceof SequenceScalarSubsequence
329           || subvar.derived instanceof SequenceScalarArbitrarySubsequence)
330          && (supervar.derived instanceof SequenceScalarSubsequence
331           || supervar.derived instanceof SequenceScalarArbitrarySubsequence)) {
332        // In "A[i..j] subseq B[k..l]": i=sub_left_var, j=sub_right_var,
333        //  k=super_left_var, l=super_right_var.
334        VarInfo sub_left_var = null, sub_right_var = null,
335          super_left_var = null, super_right_var = null;
336        // I'm careful not to access foo_shift unless foo_var has been set
337        // to a non-null value, but Java is too stupid to recognize that.
338        int sub_left_shift = 42, sub_right_shift = 69, super_left_shift = 1492,
339          super_right_shift = 1776;
340        if (subvar.derived instanceof SequenceScalarSubsequence) {
341          SequenceScalarSubsequence sub = (SequenceScalarSubsequence)subvar.derived;
342          if (sub.from_start) {
343            sub_right_var = sub.sclvar();
344            sub_right_shift = sub.index_shift;
345          } else {
346            sub_left_var = sub.sclvar();
347            sub_left_shift = sub.index_shift;
348          }
349        } else if (subvar.derived instanceof SequenceScalarArbitrarySubsequence) {
350          SequenceScalarArbitrarySubsequence sub = (SequenceScalarArbitrarySubsequence)subvar.derived;
351          sub_left_var = sub.startvar();
352          sub_left_shift = (sub.left_closed ? 0 : 1);
353          sub_right_var = sub.endvar();
354          sub_right_shift = (sub.right_closed ? 0 : -1);
355        } else {
356          throw new Error();
357        }
358        if (supervar.derived instanceof SequenceScalarSubsequence) {
359          SequenceScalarSubsequence super_ = (SequenceScalarSubsequence)supervar.derived;
360          if (super_.from_start) {
361            super_right_var = super_.sclvar();
362            super_right_shift = super_.index_shift;
363          } else {
364            super_left_var = super_.sclvar();
365            super_left_shift = super_.index_shift;
366          }
367        } else if (supervar.derived instanceof SequenceScalarArbitrarySubsequence) {
368          SequenceScalarArbitrarySubsequence super_ = (SequenceScalarArbitrarySubsequence)supervar.derived;
369          super_left_var = super_.startvar();
370          super_left_shift = (super_.left_closed ? 0 : 1);
371          super_right_var = super_.endvar();
372          super_right_shift = (super_.right_closed ? 0 : -1);
373        } else {
374          throw new Error();
375        }
376        boolean left_included = false, right_included = false;
377        if (super_left_var == null) {
378          left_included = true;
379        }
380        if (super_left_var == sub_left_var) {
381          if (super_left_shift < sub_left_shift) {
382            left_included = true;
383          }
384        }
385        if (super_right_var == null) {
386          right_included = true;
387        }
388        if (super_right_var == sub_right_var) {
389          if (super_right_shift > sub_right_shift) {
390            right_included = true;
391          }
392        }
393        if (left_included && right_included) {
394          discardCode = DiscardCode.obvious;
395          discardString = subvar.name()+" obvious subset/subsequence of "+supervar.name();
396          return IPair.of(discardCode, discardString + " [obvious]")
397;
398        }
399      } else if ((subvar.derived instanceof SequenceStringSubsequence)
400                 && (supervar.derived instanceof SequenceStringSubsequence)) {
401        // Copied from (an old version) just above
402        // XXX I think this code is dead; why isn't it just produced
403        // from the above by macro expansion? -smcc
404        SequenceStringSubsequence sss1 = (SequenceStringSubsequence) subvar.derived;
405        SequenceStringSubsequence sss2 = (SequenceStringSubsequence) supervar.derived;
406        VarInfo index1 = sss1.sclvar();
407        int shift1 = sss1.index_shift;
408        boolean start1 = sss1.from_start;
409        VarInfo index2 = sss2.sclvar();
410        int shift2 = sss2.index_shift;
411        boolean start2 = sss2.from_start;
412        if (index1 == index2) {
413          if (start1 == true && start2 == true) {
414            if (shift1 <= shift2) {
415              return IPair.of(discardCode, discardString + " [shift1]");
416            }
417          } else if (start1 == false && start2 == false) {
418            if (shift1 >= shift2) {
419              return IPair.of(discardCode, discardString + " [shift2]");
420            }
421          }
422        }
423      } else {
424        throw new Error("how can this happen? " + subvar.name()
425                        + " " + (subvar.derived == null
426                               ? "(not derived)"
427                               : subvar.derived.getClass())
428                        + " " + supervar.name()
429                        + " " + (supervar.derived == null
430                                 ? "(not derived)"
431                                 : supervar.derived.getClass()));
432      }
433    }
434
435    return null;
436  }
437
438  // Look up a previously instantiated SubSequence relationship.
439  public static @Nullable SubSequence find(PptSlice ppt) {
440    assert ppt.arity() == 2;
441    for (Invariant inv : ppt.invs) {
442      if (inv instanceof SubSequence) {
443        return (SubSequence) inv;
444      }
445    }
446    return null;
447  }
448
449  @Pure
450  @Override
451  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
452
453    VarInfo subvar = var1(vis);
454    VarInfo supervar = var2(vis);
455
456    // check for x[i..j] subsequence of x[]
457    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
458    if (subvar_super == supervar) {
459      debug.fine("  returning true because subvar_super == supervar");
460      return new DiscardInfo(this, DiscardCode.obvious,
461                    "x[i..j] subsequence of x[] is obvious");
462    }
463
464    DiscardInfo di = SubSequence.isObviousSubSequence(this, subvar, supervar);
465    if (di != null) {
466      return di;
467    }
468
469    // JHP: This is not a valid obvious check, since it doesn't imply that
470    // the invariant is true.
471    if (!subvar.aux.hasOrder()
472        || !supervar.aux.hasOrder()) {
473      // Doesn't make sense to consider subsequence if order doens't matter
474      return new DiscardInfo(this, DiscardCode.obvious,
475                    "Order doesn't matter, so subsequence is meaningless");
476    }
477
478    return super.isObviousStatically(vis);
479  }
480
481  // Two ways to go about this:
482  //   * look at all subseq relationships, see if one is over a variable of
483  //     interest
484  //   * look at all variables derived from the
485
486  // (Seems overkill to check for other transitive relationships.
487  // Eventually that is probably the right thing, however.)
488  @Pure
489  @Override
490  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
491
492    // System.out.println("checking isObviousImplied for: " + format());
493    if (debug.isLoggable(Level.FINE)) {
494      debug.fine("isObviousDynamically: checking " + vis[0].name() + " in " + vis[1].name());
495    }
496
497    DiscardInfo super_result = super.isObviousDynamically(vis);
498    if (super_result != null) {
499      return super_result;
500    }
501
502    VarInfo subvar = var1(vis);
503    VarInfo supervar = var2(vis);
504
505    // JHP: The next check is an un-interesting check, not
506    // an obvious check.  We need to figure out how to resolve this.
507
508    // Uninteresting if this is of the form x[0..i] subsequence
509    // x[0..j].  Not necessarily obvious.
510    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
511    VarInfo supervar_super = supervar.isDerivedSubSequenceOf();
512    if (subvar_super != null && subvar_super == supervar_super) {
513      debug.fine("  returning true because subvar_super == supervar_super");
514      return new DiscardInfo(this, DiscardCode.obvious,
515                    "x[0..i] subsequence of x[0..j] is uninteresting");
516    }
517
518    if (isObviousSubSequenceDynamically(this, subvar, supervar)) {
519      return new DiscardInfo(this, DiscardCode.obvious, subvar.name()
520                             + " is an obvious subsequence of "
521                             + supervar.name());
522    }
523    return null;
524  }
525
526  /**
527   * Returns true if the two original variables are related in a way that makes subsequence or
528   * subset detection not informative.
529   */
530  public static boolean isObviousSubSequenceDynamically(Invariant inv,
531                            VarInfo subvar, VarInfo supervar) {
532
533    VarInfo [] vis = {subvar, supervar};
534
535    ProglangType rep1 = subvar.rep_type;
536    ProglangType rep2 = supervar.rep_type;
537    if (!(((rep1 == ProglangType.INT_ARRAY)
538           && (rep2 == ProglangType.INT_ARRAY))
539          || ((rep1 == ProglangType.DOUBLE_ARRAY)
540           && (rep2 == ProglangType.DOUBLE_ARRAY))
541          || ((rep1 == ProglangType.STRING_ARRAY)
542           && (rep2 == ProglangType.STRING_ARRAY))
543          )) {
544            return false;
545          }
546
547    if (debug.isLoggable(Level.FINE)) {
548      debug.fine("Checking isObviousSubSequenceDynamically "
549                   + subvar.name() + " in " + supervar.name());
550    }
551
552    DiscardInfo di = isObviousSubSequence(inv, subvar, supervar);
553    if (di != null) {
554      inv.log("ObvSubSeq- true from isObviousSubSequence: %s", di.discardString());
555      return true;
556    }
557    debug.fine("  not isObviousSubSequence(statically)");
558
559    PptTopLevel ppt_parent = subvar.ppt;
560
561    // If the elements of supervar are always the same (EltOneOf),
562    // we aren't going to learn anything new from this invariant,
563    // since each sequence should have an EltOneOf over it.
564    if (false) {
565      PptSlice1 slice = ppt_parent.findSlice(supervar);
566      if (slice == null) {
567        System.out.println("No slice: parent =" + ppt_parent);
568      } else {
569        System.out.println("Slice var =" + slice.var_infos[0]);
570        for (Invariant superinv : slice.invs) {
571          System.out.println("Inv = " + superinv);
572          if (superinv instanceof EltOneOf) {
573            EltOneOf eltinv = (EltOneOf) superinv;
574            if (eltinv.num_elts() > 0) {
575              inv.log(" obvious because of %s", eltinv.format());
576              return true;
577            }
578          }
579        }
580      }
581    }
582
583    // Obvious if subvar is always just []
584    if (true) {
585      PptSlice1 slice = ppt_parent.findSlice(subvar);
586      if (slice != null) {
587        for (Invariant subinv : slice.invs) {
588          if (subinv instanceof OneOfSequence) {
589            OneOfSequence seqinv = (OneOfSequence) subinv;
590            if (seqinv.num_elts() == 1) {
591              Object elt = seqinv.elt();
592              if (elt instanceof long[] && ((long[]) elt).length == 0) {
593                Debug.log(debug, inv.getClass(), inv.ppt, vis,
594                                "ObvSubSeq- True from subvar being []");
595                return true;
596              }
597              if (elt instanceof double[] && ((double[]) elt).length == 0) {
598                inv.log("ObvSubSeq- True from subvar being []");
599                return true;
600              }
601            }
602          }
603        }
604      }
605    }
606
607    // Check for a[0..i] subseq a[0..j] but i < j.
608    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
609    VarInfo supervar_super = supervar.isDerivedSubSequenceOf();
610
611    if (subvar_super != null && subvar_super == supervar_super) {
612      // both sequences are derived from the same supersequence
613      if ((subvar.derived instanceof SequenceScalarSubsequence
614           || subvar.derived instanceof SequenceScalarArbitrarySubsequence)
615          && (supervar.derived instanceof SequenceScalarSubsequence
616           || supervar.derived instanceof SequenceScalarArbitrarySubsequence)) {
617        VarInfo sub_left_var = null, sub_right_var = null,
618          super_left_var = null, super_right_var = null;
619        // I'm careful not to access foo_shift unless foo_var has been set
620        // to a non-null value, but Java is too stupid to recognize that.
621        int sub_left_shift = 42, sub_right_shift = 69, super_left_shift = 1492,
622          super_right_shift = 1776;
623        if (subvar.derived instanceof SequenceScalarSubsequence) {
624          SequenceScalarSubsequence sub = (SequenceScalarSubsequence)subvar.derived;
625          if (sub.from_start) {
626            sub_right_var = sub.sclvar();
627            sub_right_shift = sub.index_shift;
628          } else {
629            sub_left_var = sub.sclvar();
630            sub_left_shift = sub.index_shift;
631          }
632        } else if (subvar.derived instanceof SequenceScalarArbitrarySubsequence) {
633          SequenceScalarArbitrarySubsequence sub = (SequenceScalarArbitrarySubsequence)subvar.derived;
634          sub_left_var = sub.startvar();
635          sub_left_shift = (sub.left_closed ? 0 : 1);
636          sub_right_var = sub.endvar();
637          sub_right_shift = (sub.right_closed ? 0 : -1);
638        } else {
639          throw new Error();
640        }
641        if (supervar.derived instanceof SequenceScalarSubsequence) {
642          SequenceScalarSubsequence super_ = (SequenceScalarSubsequence)supervar.derived;
643          if (super_.from_start) {
644            super_right_var = super_.sclvar();
645            super_right_shift = super_.index_shift;
646          } else {
647            super_left_var = super_.sclvar();
648            super_left_shift = super_.index_shift;
649          }
650        } else if (supervar.derived instanceof SequenceScalarArbitrarySubsequence) {
651          SequenceScalarArbitrarySubsequence super_ = (SequenceScalarArbitrarySubsequence)supervar.derived;
652          super_left_var = super_.startvar();
653          super_left_shift = (super_.left_closed ? 0 : 1);
654          super_right_var = super_.endvar();
655          super_right_shift = (super_.right_closed ? 0 : -1);
656        } else {
657          throw new Error();
658        }
659        boolean left_included, right_included;
660        if (super_left_var == null) {
661          left_included = true;
662        } else if (sub_left_var == null) // we know super_left_var != null here
663          left_included = false;
664        else {
665          left_included =
666            VarInfo.compare_vars(super_left_var, super_left_shift,
667                                   sub_left_var, sub_left_shift,
668                                   true /* <= */);
669        }
670        if (super_right_var == null) {
671          right_included = true;
672        } else if (sub_right_var == null) // we know super_right_var != null here
673          right_included = false;
674        else {
675          right_included =
676            VarInfo.compare_vars(super_right_var, super_right_shift,
677                                   sub_right_var, sub_right_shift,
678                                   false /* >= */);
679        }
680//         System.out.println("Is " + subvar.name() + " contained in "
681//                            + supervar.name()
682//                            + "? left: " + left_included + ", right: "
683//                            + right_included);
684        if (left_included && right_included) {
685          inv.log("ObvSubSeq- True a[0..i] subseq a[0..j] and i < j");
686          return true;
687        }
688      } else if ((subvar.derived instanceof SequenceStringSubsequence)
689                 && (supervar.derived instanceof SequenceStringSubsequence)) {
690        // Copied from just above
691        SequenceStringSubsequence sss1 = (SequenceStringSubsequence) subvar.derived;
692        SequenceStringSubsequence sss2 = (SequenceStringSubsequence) supervar.derived;
693        VarInfo index1 = sss1.sclvar();
694        int shift1 = sss1.index_shift;
695        boolean start1 = sss1.from_start;
696        VarInfo index2 = sss2.sclvar();
697        int shift2 = sss2.index_shift;
698        boolean start2 = sss2.from_start;
699        if (start1 == start2) {
700          if (VarInfo.compare_vars(index1, shift1, index2, shift2, start1)) {
701            inv.log("True from comparing indices");
702            return true;
703          }
704        }
705      } else {
706        throw new Error("how can this happen? " + subvar.name()
707                        + " " + (subvar.derived == null
708                               ? "(not derived)"
709                               : subvar.derived.getClass())
710                        + " " + supervar.name()
711                        + " " + (supervar.derived == null
712                                 ? "(not derived)"
713                                 : supervar.derived.getClass()));
714      }
715
716    }
717
718    // Also need to check A[0..i] subseq A[0..j] via compare_vars.
719
720    // A subseq B[0..n] => A subseq B
721
722    List<Derivation> derivees = supervar.derivees();
723    // For each variable derived from supervar ("B")
724    for (Derivation der : derivees) {
725      // System.out.println("  ... der = " + der.getVarInfo().name() + " " + der);
726      if (der instanceof SequenceScalarSubsequence) {
727        // If that variable is "B[0..n]"
728        VarInfo supervar_part = der.getVarInfo();
729        // Get the canonical version; being equal to it is good enough.
730        if (supervar_part.get_equalitySet_leader() == subvar) {
731          Debug.log(debug, inv.getClass(), inv.ppt, vis,
732                "ObvSubSeq- True from canonical leader");
733          return true;
734        }
735
736        if (supervar_part.isCanonical()) {
737          if (subvar == supervar_part) {
738            System.err.println("Error: variables "
739                                + subvar.name()
740                                + " and "
741                                + supervar_part.name()
742                                + " are identical.  Canonical");
743            System.err.println(subvar.isCanonical());
744            System.err.println(supervar_part.isCanonical());
745            throw new Error();
746          }
747
748          // Check to see if there is a subsequence over the supervar
749          if (ppt_parent.is_subsequence(subvar, supervar_part)) {
750            if (Debug.logOn()) {
751              inv.log("ObvSubSeq- true from A subseq B[0..n] %s/%s",
752                       subvar.name(), supervar_part.name());
753            }
754            return true;
755          }
756        }
757      }
758    }
759    return false;
760  }
761
762  @Pure
763  @Override
764  public boolean isSameFormula(Invariant inv) {
765    assert inv instanceof SubSequence;
766    return true;
767  }
768
769  /** returns the ni-suppressions for SubSequence */
770  @Pure
771  @Override
772  public NISuppressionSet get_ni_suppressions() {
773    return suppressions;
774  }
775
776  /** definition of this invariant (the suppressee) */
777  private static NISuppressee suppressee = new NISuppressee(SubSequence.class, 2);
778
779  // suppressor definitions (used in suppressions below)
780  private static NISuppressor v1_eq_v2 = new NISuppressor(0, 1, SeqSeqIntEqual.class);
781  private static NISuppressor v1_pw_eq_v2 = new NISuppressor(0, 1, PairwiseIntEqual.class);
782
783  // sub/super sequence suppressions.  We have both SeqSeq and Pairwise
784  // as suppressions because each can be enabled separately.
785  private static NISuppressionSet suppressions =
786    new NISuppressionSet(
787        new NISuppression[] {
788          // a[] == b[] ==> a[] sub/superset b[]
789          new NISuppression(v1_eq_v2, suppressee),
790          // a[] == b[] ==> a[] sub/superset b[]
791          new NISuppression(v1_pw_eq_v2, suppressee),
792        });
793
794}