001// ***** This file is automatically generated from SeqComparison.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import daikon.*; 006import daikon.Quantify.QuantFlags; 007import daikon.derive.binary.*; 008import daikon.inv.*; 009import daikon.suppress.*; 010import java.util.*; 011import java.util.logging.Logger; 012import org.checkerframework.checker.interning.qual.Interned; 013import org.checkerframework.checker.lock.qual.GuardSatisfied; 014import org.checkerframework.checker.nullness.qual.Nullable; 015import org.checkerframework.dataflow.qual.Pure; 016import org.checkerframework.dataflow.qual.SideEffectFree; 017import org.plumelib.util.ArraysPlume; 018import org.plumelib.util.Intern; 019import typequals.prototype.qual.NonPrototype; 020import typequals.prototype.qual.Prototype; 021 022/** 023 * Represents invariants between two sequences of double values. If order matters for each 024 * variable (which it does by default), then the sequences are compared lexically. Prints as 025 * {@code x[] < y[] lexically}. 026 * 027 028 * <p>If the auxiliary information (e.g., order matters) doesn't match between two variables, then 029 * this invariant cannot apply to those variables. 030 */ 031public class SeqSeqFloatLessThan extends TwoSequenceFloat 032 033{ 034 static final long serialVersionUID = 20030822L; 035 036 // Variables starting with dkconfig_ should only be set via the 037 // daikon.config.Configuration interface. 038 /** Boolean. True iff SeqSeqFloatLessThan invariants should be considered. */ 039 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 040 041 /** Debugging logger. */ 042 static final Logger debug = Logger.getLogger("daikon.inv.binary.twoSequence.SeqSeqFloatLessThan"); 043 044 static Comparator<double[]> comparator = Global.fuzzy.new DoubleArrayComparatorLexical(); 045 046 boolean orderMatters; 047 048 protected SeqSeqFloatLessThan(PptSlice ppt, boolean orderMatters) { 049 super(ppt); 050 this.orderMatters = orderMatters; 051 } 052 053 protected @Prototype SeqSeqFloatLessThan(boolean orderMatters) { 054 super(); 055 this.orderMatters = orderMatters; 056 } 057 058 protected SeqSeqFloatLessThan(SeqSeqFloatGreaterThan seq_swap) { 059 super(seq_swap.ppt); 060 orderMatters = seq_swap.orderMatters; 061 } 062 063 private static @Prototype SeqSeqFloatLessThan proto = new @Prototype SeqSeqFloatLessThan(true); 064 065 /** Returns the prototype invariant for SeqSeqFloatLessThan */ 066 public static @Prototype SeqSeqFloatLessThan get_proto() { 067 return proto; 068 } 069 070 @Override 071 public boolean enabled() { 072 return dkconfig_enabled; 073 } 074 075 @Override 076 public boolean instantiate_ok(VarInfo[] vis) { 077 078 if (!valid_types(vis)) { 079 return false; 080 } 081 082 VarInfo var1 = vis[0]; 083 VarInfo var2 = vis[1]; 084 ProglangType type1 = var1.type; 085 ProglangType type2 = var2.type; 086 087 // This intentonally checks dimensions(), not pseudoDimensions. 088 boolean only_eq = 089 !((type1.dimensions() == 1) 090 && type1.baseIsFloat() 091 && (type2.dimensions() == 1) 092 && type2.baseIsFloat()); 093 if (only_eq) { 094 return false; 095 } 096 097 // non equality comparisons don't make sense if the arrays aren't ordered 098 if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) { 099 return false; 100 } 101 102 return true; 103 } 104 105 @Override 106 protected SeqSeqFloatLessThan instantiate_dyn(@Prototype SeqSeqFloatLessThan this, PptSlice slice) { 107 boolean has_order = slice.var_infos[0].aux.hasOrder() && slice.var_infos[1].aux.hasOrder(); 108 return new SeqSeqFloatLessThan(slice, has_order); 109 } 110 111 @Override 112 protected Invariant resurrect_done_swapped() { 113 114 return new SeqSeqFloatGreaterThan(this); 115 } 116 117 @Override 118 public String repr(@GuardSatisfied SeqSeqFloatLessThan this) { 119 return "SeqSeqFloatLessThan" + varNames() + ": ,orderMatters=" + orderMatters 120 + ",enoughSamples=" + enoughSamples() 121 ; 122 } 123 124 @SideEffectFree 125 @Override 126 public String format_using(@GuardSatisfied SeqSeqFloatLessThan this, OutputFormat format) { 127 // System.out.println("Calling SeqSeqFloatLessThan.format for: " + repr()); 128 129 if (format == OutputFormat.SIMPLIFY) { 130 return format_simplify(); 131 } 132 133 if (format == OutputFormat.DAIKON) { 134 String name1 = var1().name_using(format); 135 String name2 = var2().name_using(format); 136 137 String lexically = (var1().aux.hasOrder() ? " (lexically)" : ""); 138 return name1 + " < " + name2 + lexically; 139 } 140 141 if (format == OutputFormat.CSHARPCONTRACT) { 142 143 if (var1().aux.hasOrder()) { 144 String name1 = var1().csharp_collection_string(); 145 String name2 = var2().csharp_collection_string(); 146 String dbc = "LlexLT".substring(1); 147 return name1 + "." + dbc + "(" + name2 + ")"; 148 } else { 149 return "\"SeqComparison.java.jpp: sequence comparison does not apply to unordered collections unimplemented\" != null)"; // interned 150 } 151 152 } 153 154 if (format.isJavaFamily()) { 155 String name1 = var1().name_using(format); 156 String name2 = var2().name_using(format); 157 158 return "daikon.Quant." 159 + (var1().aux.hasOrder() ? "lexLT" : "setEqual" ) 160 + "(" 161 + name1 162 + ", " 163 + name2 164 + ")"; 165 166 } 167 168 return format_unimplemented(format); 169 } 170 171 public String format_simplify(@GuardSatisfied SeqSeqFloatLessThan this) { 172 if (Invariant.dkconfig_simplify_define_predicates) { 173 return format_simplify_defined(); 174 } else { 175 return format_simplify_explicit(); 176 } 177 } 178 179 private String format_simplify_defined(@GuardSatisfied SeqSeqFloatLessThan this) { 180 String[] var1_name = var1().simplifyNameAndBounds(); 181 String[] var2_name = var2().simplifyNameAndBounds(); 182 if (var1_name == null || var2_name == null) { 183 return String.format("%s.format_simplify_defined(%s): var1_name=%s, var2_name=%s, for %s", 184 getClass().getSimpleName(), this, 185 Arrays.toString(var1_name), Arrays.toString(var2_name), format()); 186 } 187 return "(|lexical-<| " 188 + var1_name[0] + " " + var1_name[1] + " " + var1_name[2] + " " 189 + var2_name[0] + " " + var2_name[1] + " " + var2_name[2] + ")"; 190 } 191 192 private String format_simplify_explicit(@GuardSatisfied SeqSeqFloatLessThan this) { 193 194 String classname = this.getClass().toString().substring(6); 195 return "warning: method " + classname 196 + ".format_simplify_explicit() needs to be implemented: " + format(); 197 198 } 199 200 @Override 201 public InvariantStatus check_modified( 202 double @Interned [] v1, double @Interned [] v2, int count) { 203 /// This does not do the right thing; I really want to avoid comparisons 204 /// if one is missing, but not if one is zero-length. 205 // // Don't make comparisons with empty arrays. 206 // if ((v1.length == 0) || (v2.length == 0)) { 207 // return; 208 // } 209 210 int comparison = 0; 211 if (orderMatters) { 212 // Standard element wise comparison 213 comparison = comparator.compare(v1, v2); 214 } else { 215 // Do a double subset comparison 216 comparison = Global.fuzzy.isElemMatch(v1, v2) ? 0 : -1; 217 } 218 219 if (!(comparison < 0) ) { 220 return InvariantStatus.FALSIFIED; 221 } 222 return InvariantStatus.NO_CHANGE; 223 } 224 225 @Override 226 public InvariantStatus add_modified(double @Interned [] v1, double @Interned [] v2, int count) { 227 if (logDetail()) { 228 log("add_modified (%s, %s)", Arrays.toString(v1), Arrays.toString(v2)); 229 } 230 return check_modified(v1, v2, count); 231 } 232 233 @Override 234 protected double computeConfidence() { 235 236 return 1 - Math.pow(.5, ppt.num_values()); 237 } 238 239 @Pure 240 @Override 241 public boolean isSameFormula(Invariant o) { 242 return true; 243 } 244 245 @Pure 246 @Override 247 public boolean isExclusiveFormula(Invariant o) { 248 return false; 249 } 250 251 /** 252 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 253 * avoid circular isObvious relations. 254 */ 255 @Pure 256 @Override 257 public @Nullable DiscardInfo isObviousStatically_SomeInEquality() { 258 if (var1().equalitySet == var2().equalitySet) { 259 return isObviousStatically(this.ppt.var_infos); 260 } else { 261 return super.isObviousStatically_SomeInEquality(); 262 } 263 } 264 265 /** 266 * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to 267 * avoid circular isObvious relations. 268 */ 269 @Pure 270 @Override 271 public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() { 272 if (logOn()) { 273 log("Considering dynamically_someInEquality"); 274 } 275 if (var1().equalitySet == var2().equalitySet) { 276 return isObviousDynamically(this.ppt.var_infos); 277 } else { 278 return super.isObviousDynamically_SomeInEquality(); 279 } 280 } 281 282 @Pure 283 @Override 284 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 285 286 VarInfo var1 = vis[0]; 287 VarInfo var2 = vis[1]; 288 DiscardInfo di; 289 di = SubSequenceFloat.isObviousSubSequence(this, var1, var2); 290 if (di == null) { 291 di = SubSequenceFloat.isObviousSubSequence(this, var2, var1); 292 } 293 if (di != null) { 294 return di; 295 } 296 297 return super.isObviousStatically(vis); 298 } 299 300 @Pure 301 @Override 302 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 303 DiscardInfo super_result = super.isObviousDynamically(vis); 304 if (super_result != null) { 305 return super_result; 306 } 307 assert ppt != null; 308 309 Debug debug = new Debug(getClass(), ppt, vis); 310 311 if (logOn()) { 312 debug.log("Checking IsObviousDynamically"); 313 } 314 315 // Check to see if the same Pairwise invariant exists 316 DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, ""); 317 if (ppt.parent.check_implied(di, vis[0], vis[1], PairwiseFloatLessThan.get_proto())) { 318 di.add_implied_vis(vis); 319 return di; 320 } 321 322 // If either variable is a subsequence and the original arrays 323 // are related elementwise this isn't interesting 324 VarInfo v1 = vis[0]; 325 VarInfo v2 = vis[1]; 326 VarInfo arr1 = v1; 327 VarInfo arr2 = v2; 328 if (v1.derived instanceof SequenceFloatSubsequence) { 329 arr1 = ((SequenceFloatSubsequence) v1.derived).seqvar(); 330 } 331 if (v2.derived instanceof SequenceFloatSubsequence) { 332 arr2 = ((SequenceFloatSubsequence) v2.derived).seqvar(); 333 } 334 if (!isEqual() && ((arr1 != v1) || (arr2 != v2))) { 335 VarInfo[] avis = new VarInfo [] {arr1, arr2}; 336 PptSlice slice = this.ppt.parent.findSlice_unordered(avis); 337 if (slice != null) { 338 PairwiseFloatEqual picEQ = PairwiseFloatEqual.find(slice); 339 if (picEQ != null) { 340 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picEQ.format()); 341 } 342 PairwiseFloatLessThan picLT = PairwiseFloatLessThan.find(slice); 343 if (picLT != null) { 344 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picLT.format()); 345 } 346 PairwiseFloatGreaterThan picGT = PairwiseFloatGreaterThan.find(slice); 347 if (picGT != null) { 348 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picGT.format()); 349 } 350 PairwiseFloatLessEqual picLE = PairwiseFloatLessEqual.find(slice); 351 if (picLE != null) { 352 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picLE.format()); 353 } 354 PairwiseFloatGreaterEqual picGE = PairwiseFloatGreaterEqual.find(slice); 355 if (picGE != null) { 356 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + picGE.format()); 357 } 358 } 359 } 360 361 // Similarly, if either variable is a subsequence and the original 362 // arrays are related lexically this isn't interesting 363 if ((arr1 != v1) || (arr2 != v2)) { 364 if (arr1 == arr2) { 365 debug.log("Obvious Dynamic- subsequence from same array"); 366 return new DiscardInfo(this, DiscardCode.obvious, "Supersequences are related lexically"); 367 } 368 VarInfo[] avis = {arr1, arr2}; 369 debug.log("looking for " + avis[0].name() + " " + avis[1].name()); 370 PptSlice slice = this.ppt.parent.findSlice_unordered(avis); 371 debug.log("Found ppt " + slice); 372 if (slice != null) { 373 for (Invariant inv : slice.invs) { 374 debug.log("-- invariant " + inv.format()); 375 } 376 Invariant inv; 377 inv = SeqSeqFloatEqual.find(slice); 378 if (inv != null) { 379 if (logOn()) { 380 debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")"); 381 } 382 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format()); 383 } 384 inv = SeqSeqFloatLessThan.find(slice); 385 if (inv != null) { 386 if (logOn()) { 387 debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")"); 388 } 389 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format()); 390 } 391 inv = SeqSeqFloatGreaterThan.find(slice); 392 if (inv != null) { 393 if (logOn()) { 394 debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")"); 395 } 396 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format()); 397 } 398 inv = SeqSeqFloatLessEqual.find(slice); 399 if (inv != null) { 400 if (logOn()) { 401 debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")"); 402 } 403 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format()); 404 } 405 inv = SeqSeqFloatGreaterEqual.find(slice); 406 if (inv != null) { 407 if (logOn()) { 408 debug.log("Obvious Dynamic from " + inv.format() + "(" + inv.getClass() + ")"); 409 } 410 return new DiscardInfo(this, DiscardCode.obvious, "Implied by " + inv.format()); 411 } 412 } 413 } 414 415 // Check to see if these variables are obviously related 416 if (v1.isDerived() || v2.isDerived()) { 417 if (SubSequenceFloat.isObviousSubSequenceDynamically(this, v1, v2) 418 || SubSequenceFloat.isObviousSubSequenceDynamically(this, v2, v1)) { 419 if (logOn()) { 420 debug.log("Obvious SubSequence Dynamically"); 421 } 422 assert ppt != null; 423 return new DiscardInfo( 424 this, 425 DiscardCode.obvious, 426 "Both vars are derived and one is a subsequence of the other"); 427 } 428 } 429 430 return null; 431 } 432 433 @Override 434 public void repCheck() { 435 super.repCheck(); 436 /* 437 This code is no longer needed now that the can_be_x's are gone 438 if (!(this.can_be_eq || this.can_be_lt || this.can_be_gt) 439 && ppt.num_samples() != 0) { 440 System.err.println(this.repr()); 441 System.err.println(this.ppt.num_samples()); 442 throw new Error(); 443 } 444 */ 445 } 446 447 @Pure 448 public boolean isEqual() { 449 450 return false; 451 } 452 453 // Look up a previously instantiated invariant. 454 public static @Nullable SeqSeqFloatLessThan find(PptSlice ppt) { 455 assert ppt.arity() == 2; 456 for (Invariant inv : ppt.invs) { 457 if (inv instanceof SeqSeqFloatLessThan) { 458 return (SeqSeqFloatLessThan) inv; 459 } 460 } 461 return null; 462 } 463 464 /** Returns a list of non-instantiating suppressions for this invariant. */ 465 @Pure 466 @Override 467 public @Nullable NISuppressionSet get_ni_suppressions() { 468 return suppressions; 469 } 470 471 /** Definition of this invariant (the suppressee) */ 472 private static NISuppressee suppressee = new NISuppressee(SeqSeqFloatLessThan.class, 2); 473 474 // Suppressor definitions (used in suppressions below) 475 private static NISuppressor v1_pw_v2 = new NISuppressor(0, 1, PairwiseFloatLessThan.class); 476 477 private static NISuppressionSet suppressions = 478 new NISuppressionSet( 479 new NISuppression[] { 480 // pairwise => lexical 481 new NISuppression(v1_pw_v2, suppressee), 482 }); 483 484 @Override 485 public @Nullable @NonPrototype SeqSeqFloatLessThan merge( 486 @Prototype SeqSeqFloatLessThan this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) { 487 // Ignore the orderMatters field, because it is always the same (and is always true). 488 return (SeqSeqFloatLessThan) super.merge(invs, parent_ppt); 489 } 490}