Source code

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