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