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