Source code

001// ***** This file is automatically generated from NoDuplicates.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.derive.binary.SequencesJoinFloat;
008import daikon.derive.binary.SequencesPredicate;
009import daikon.inv.*;
010import daikon.inv.binary.twoSequence.*;
011import daikon.inv.unary.scalar.*;
012import daikon.suppress.*;
013import java.util.*;
014import java.util.logging.*;
015import org.checkerframework.checker.interning.qual.Interned;
016import org.checkerframework.checker.lock.qual.GuardSatisfied;
017import org.checkerframework.checker.nullness.qual.Nullable;
018import org.checkerframework.dataflow.qual.Pure;
019import org.checkerframework.dataflow.qual.SideEffectFree;
020import org.plumelib.util.Intern;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Represents sequences of double that contain no duplicate elements. Prints as
026 * {@code x[] contains no duplicates}.
027 */
028
029public class NoDuplicatesFloat extends SingleFloatSequence {
030  static final long serialVersionUID = 20040204L;
031
032  // Variables starting with dkconfig_ should only be set via the
033  // daikon.config.Configuration interface.
034  /** Boolean. True iff NoDuplicates invariants should be considered. */
035  public static boolean dkconfig_enabled = false;
036
037  /** Debug tracer. */
038  public static final Logger debug = Logger.getLogger("daikon.inv.unary.sequence.NoDuplicatesFloat");
039
040  protected NoDuplicatesFloat(PptSlice ppt) {
041    super(ppt);
042  }
043
044  protected @Prototype NoDuplicatesFloat() {
045    super();
046  }
047
048  private static @Prototype NoDuplicatesFloat proto = new @Prototype NoDuplicatesFloat();
049
050  /** Returns the prototype invariant for NoDuplicatesFloat */
051  public static @Prototype NoDuplicatesFloat get_proto() {
052    return proto;
053  }
054
055  @Override
056  public boolean enabled() {
057    return dkconfig_enabled;
058  }
059
060  @Override
061  public NoDuplicatesFloat instantiate_dyn(@Prototype NoDuplicatesFloat this, PptSlice slice) {
062    return new NoDuplicatesFloat(slice);
063  }
064
065  @Override
066  public String repr(@GuardSatisfied NoDuplicatesFloat this) {
067    return "NoDuplicatesFloat" + varNames() + ": ";
068  }
069
070  @SideEffectFree
071  @Override
072  public String format_using(@GuardSatisfied NoDuplicatesFloat this, OutputFormat format) {
073    if (debug.isLoggable(Level.FINE)) {
074      debug.fine(repr());
075    }
076
077    if (format == OutputFormat.DAIKON) {
078      return var().name() + " contains no duplicates";
079    }
080
081    if (format == OutputFormat.SIMPLIFY) {
082      return format_simplify();
083    }
084
085    if (format.isJavaFamily()) {
086      return format_java_family(format);
087    }
088
089    if (format == OutputFormat.CSHARPCONTRACT) {
090      return format_csharp_contract();
091    }
092
093    return format_unimplemented(format);
094  }
095
096  public String format_simplify(@GuardSatisfied NoDuplicatesFloat this) {
097    String[] form = VarInfo.simplify_quantify(QuantFlags.distinct(), var(),
098                                               var());
099    return form[0] + "(NEQ " + form[1] + " " + form[2] + ")"
100      + form[3];
101  }
102
103  public String format_java_family(@GuardSatisfied NoDuplicatesFloat this, OutputFormat format) {
104    return "daikon.Quant.noDups(" + var().name_using(format) + ")";
105  }
106
107  public String format_csharp_contract(@GuardSatisfied NoDuplicatesFloat this) {
108    String collection = var().csharp_collection_string();
109    return collection + ".Distinct().Count() == " + collection + ".Count()";
110  }
111
112  @Override
113  public InvariantStatus check_modified(double @Interned [] a, int count) {
114    // if (logDetail())
115    //   log ("sample " + Arrays.toString (a));
116    for (int i = 1; i < a.length; i++) {
117      for (int j = 0; j < i; j++) {
118        if (Global.fuzzy.eq(a[i], a[j])) {
119          return InvariantStatus.FALSIFIED;
120        }
121      }
122    }
123    return InvariantStatus.NO_CHANGE;
124  }
125
126  @Override
127  public InvariantStatus add_modified(double @Interned [] a, int count) {
128    InvariantStatus status = check_modified(a, count);
129    if (debug.isLoggable(Level.FINE) && (status == InvariantStatus.FALSIFIED)) {
130      debug.fine("Destroying myself with: " + var().name());
131      debug.fine(Arrays.toString(a));
132    }
133    return status;
134  }
135
136  @Override
137  protected double computeConfidence() {
138    // num_no_dup_values() would be more appropriate
139    // return 1 - Math.pow(.9, ((PptSlice1) ppt).num_no_dup_values());
140    return 1 - Math.pow(.9, ((PptSlice1) ppt).num_samples());
141  }
142
143  @Pure
144  @Override
145  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
146    if (!vis[0].aux.hasDuplicates()) {
147      return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically");
148    }
149    return super.isObviousStatically(vis);
150  }
151
152  /**
153   * Checks to see if this is obvious over the specified variables Implements the following checks:
154   *
155   * <pre>
156   *   (A[] subsequence B[]) ^ (B[] has nodups) &rArr; A[] has nodups
157   *   (A[] sorted by &gt;) v (A[] sorted by &lt;) &rArr; A[] has nodups
158   * </pre>
159   *
160   * JHP: The first check is not valid because we can't rely on transitive checks because of missing
161   * (if B[] is missing, A[] could have dups on those samples),
162   */
163  @Pure
164  @Override
165  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
166    DiscardInfo super_result = super.isObviousDynamically(vis);
167    if (super_result != null) {
168      return super_result;
169    }
170
171    // If the maximum size of the array is <= 1, then this is
172    // obvious
173    ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) vis[0].get_value_set();
174    if (vs.max_length() <= 1) {
175      return new DiscardInfo(this, DiscardCode.obvious, "Size of " + vis[0]
176                               + " is <= " + vs.max_length());
177    }
178
179    // For every other NoDuplicates at this program point, see if there is a
180    // subsequence relationship between that array and this one.
181    VarInfo v1 = vis[0];
182
183    PptTopLevel parent = ppt.parent;
184
185    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
186      Invariant inv = itor.next();
187      if ((inv instanceof NoDuplicatesFloat) && (inv != this) && inv.enoughSamples()) {
188        VarInfo v2 = inv.ppt.var_infos[0];
189        if (SubSequenceFloat.isObviousSubSequenceDynamically(this, v1, v2)) {
190          // System.out.println("obvious: " + format() + "   because of " + inv.format());
191          log("Obvious- Obvious sub sequence with %s", inv.format());
192          return new DiscardInfo(this, DiscardCode.obvious, "Invariant holds over a supersequence");
193        }
194      }
195    }
196
197    // If the sequence is sorted by < or >, then there are obviously no duplicates
198
199    PptSlice slice = this.ppt.parent.findSlice_unordered(vis);
200    if (slice != null) {
201      for (Invariant inv : slice.invs) {
202        if ((inv instanceof EltwiseIntLessThan)
203            || (inv instanceof EltwiseFloatLessThan)
204            || (inv instanceof EltwiseIntGreaterThan)
205            || (inv instanceof EltwiseFloatGreaterThan)) {
206          return new DiscardInfo(this, DiscardCode.obvious, "Sequence is sorted: " + inv.format());
207        }
208      }
209    }
210
211    return null;
212  }
213
214  @Pure
215  @Override
216  public boolean isSameFormula(Invariant other) {
217    assert other instanceof NoDuplicatesFloat;
218    return true;
219  }
220}