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