Source code

001// ***** This file is automatically generated from SubSet.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.suppress.*;
008import java.util.*;
009import java.util.logging.Level;
010import java.util.logging.Logger;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012import org.checkerframework.checker.nullness.qual.NonNull;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.Pure;
015import org.checkerframework.dataflow.qual.SideEffectFree;
016import org.plumelib.util.ArraysPlume;
017import typequals.prototype.qual.NonPrototype;
018import typequals.prototype.qual.Prototype;
019
020/**
021 * Represents two sequences of double values where one of the sequences is a subset of the other; that
022 * is each element of one sequence appears in the other. Prints as either
023 * {@code x[] is a subset of y[]} or as {@code x[] is a superset of y[]}.
024 */
025public class SubSetFloat extends TwoSequenceFloat {
026  // We are Serializable, so we specify a version to allow changes to
027  // method signatures without breaking serialization.  If you add or
028  // remove fields, you should change this number to the current date.
029  static final long serialVersionUID = 20031024L;
030
031  private static final Logger debug =
032    Logger.getLogger("daikon.inv.binary.twoSequence.SubSetFloat");
033
034  // Variables starting with dkconfig_ should only be set via the
035  // daikon.config.Configuration interface.
036  /** Boolean. True iff SubSet invariants should be considered. */
037  public static boolean dkconfig_enabled = false;
038
039  protected SubSetFloat(PptSlice ppt) {
040    super(ppt);
041  }
042
043  protected @Prototype SubSetFloat() {
044    super();
045  }
046
047  private static @Prototype SubSetFloat proto = new @Prototype SubSetFloat();
048
049  /** Returns the prototype invariant for SubSetFloat */
050  public static @Prototype SubSetFloat get_proto() {
051    return proto;
052  }
053
054  /** returns whether or not this invariant is enabled */
055  @Override
056  public boolean enabled() {
057    return dkconfig_enabled;
058  }
059
060  @Override
061  public boolean instantiate_ok(VarInfo[] vis) {
062
063    if (!valid_types(vis)) {
064      return false;
065    }
066
067    return true;
068  }
069
070  /** instantiates the invariant on the specified slice */
071  @Override
072  public SubSetFloat instantiate_dyn(@Prototype SubSetFloat this, PptSlice slice) {
073    return new SubSetFloat(slice);
074  }
075
076  @Override
077  protected Invariant resurrect_done_swapped() {
078    return new SuperSetFloat(ppt);
079  }
080
081  @Override
082  public String repr(@GuardSatisfied SubSetFloat this) {
083    return "SubSetFloat" + varNames() + ": ,falsified=" + falsified;
084  }
085
086  @SideEffectFree
087  @Override
088  public String format_using(@GuardSatisfied SubSetFloat this, OutputFormat format) {
089    if (format == OutputFormat.DAIKON) {
090      return format();
091    }
092    if (format == OutputFormat.ESCJAVA) {
093      return format_esc();
094    }
095    if (format == OutputFormat.SIMPLIFY) {
096      return format_simplify();
097    }
098    if (format == OutputFormat.CSHARPCONTRACT) {
099      return format_csharp_contract();
100    }
101    if (format.isJavaFamily()) {
102      return format_java_family(format);
103    }
104
105    return format_unimplemented(format);
106  }
107
108  @SideEffectFree
109  @Override
110  public String format(@GuardSatisfied SubSetFloat this) {
111    String v1 = var1().name();
112    String v2 = var2().name();
113
114    return v1 + " is a subset of " + v2;
115  }
116
117  public String format_csharp_contract(@GuardSatisfied SubSetFloat this) {
118    String v1 = var1().csharp_collection_string();
119    String v2 = var2().csharp_collection_string();
120
121    return "Contract.ForAll(" + v1 + ", i => " + v2 + ".Contains(i))";
122  }
123
124  public String format_esc(@GuardSatisfied SubSetFloat this) {
125    String classname = this.getClass().toString().substring(6); // remove leading "class"
126    return "warning: method " + classname + ".format_esc() needs to be implemented: " + format();
127  }
128
129  public String format_simplify(@GuardSatisfied SubSetFloat this) {
130    if (Invariant.dkconfig_simplify_define_predicates) {
131      return format_simplify_defined();
132    } else {
133      return format_simplify_explicit();
134    }
135  }
136
137  private String format_simplify_defined(@GuardSatisfied SubSetFloat this) {
138
139    VarInfo subvar = var1();
140    VarInfo supervar = var2();
141
142    String[] sub_name = subvar.simplifyNameAndBounds();
143    String[] super_name = supervar.simplifyNameAndBounds();
144
145    if (sub_name == null || super_name == null) {
146      return String.format("%s.format_simplify_defined(%s): sub_name=%s, super_name=%s, for %s",
147                           getClass().getSimpleName(), this,
148                           Arrays.toString(sub_name), Arrays.toString(super_name), format());
149    }
150
151    return "(subset "
152      + sub_name[0] + " " + sub_name[1] + " " + sub_name[2] + " "
153      + super_name[0] + " " + super_name[1] + " " + super_name[2] + ")";
154  }
155
156  private String format_simplify_explicit(@GuardSatisfied SubSetFloat this) {
157
158    VarInfo subvar = var1();
159    VarInfo supervar = var2();
160
161    String[] sub_name = subvar.simplifyNameAndBounds();
162    String[] super_name = supervar.simplifyNameAndBounds();
163
164    if (sub_name == null || super_name == null) {
165      return String.format("%s.format_simplify_explicit(%s): sub_name=%s, super_name=%s, for %s",
166                           getClass().getSimpleName(), this,
167                           Arrays.toString(sub_name), Arrays.toString(super_name), format());
168    }
169
170    String indices[] = VarInfo.get_simplify_free_indices(subvar, supervar);
171
172    // (FORALL (a i j b ip jp)
173    //    (IFF (subset a i j b ip jp)
174    //         (FORALL (x)
175    //           (IMPLIES
176    //              (AND (<= i x) (<= x j))
177    //              (EXISTS (y)
178    //                  (AND (<= ip y) (<= y jp)
179    //                        (EQ (select (select elems a) x)
180    //                            (select (select elems b) y))))))))
181
182    return "(FORALL (" + indices[0] + ") (IMPLIES (AND (<= " + sub_name[1]
183      + " " + indices[0] + ") (<= " + indices[0] + " " + sub_name[2] + "))"
184      + "(EXISTS (" + indices[1] + ")(AND (<= " + super_name[1] + " "
185      + indices[1] + ") (<= " + indices[1] + " " + super_name[2]+ ")"
186      + "(EQ (select (select elems " + sub_name[0] + ") " + indices[0] + ") "
187      + "(select (select elems " + super_name[0] +") " + indices[1] + "))))))";
188
189  }
190
191  public String format_java_family(@GuardSatisfied SubSetFloat this, OutputFormat format) {
192
193    String v1 = var1().name_using(format);
194    String v2 = var2().name_using(format);
195
196    return "daikon.Quant.subsetOf(" + v1 + ", " + v2 + ")";
197  }
198
199  @Override
200  public InvariantStatus check_modified(double[] a1, double[] a2, int count) {
201
202    if (!Global.fuzzy.isSubset(a1, a2)) {
203
204      return InvariantStatus.FALSIFIED;
205    } else {
206      return InvariantStatus.NO_CHANGE;
207    }
208
209  }
210
211  @Override
212  public InvariantStatus add_modified(double[] a1, double[] a2, int count) {
213    if (debug.isLoggable(Level.FINE)) {
214      debug.fine(Arrays.toString(a1));
215      debug.fine(Arrays.toString(a2));
216    }
217    return check_modified(a1, a2, count);
218  }
219
220  @Override
221  protected double computeConfidence() {
222    return Invariant.CONFIDENCE_JUSTIFIED;
223  }
224
225  // Convenience name to make this easier to find.
226  @Pure
227  public static @Nullable DiscardInfo isObviousSubSet(Invariant inv, VarInfo subvar, VarInfo supervar) {
228    return SubSequenceFloat.isObviousSubSequence(inv, subvar, supervar);
229  }
230
231  @Pure
232  @Override
233  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
234    VarInfo var1 = vis[0];
235    VarInfo var2 = vis[1];
236
237    DiscardInfo di;
238    di = SubSetFloat.isObviousSubSet(this, var1, var2);
239    if (di == null) {
240      di = SubSetFloat.isObviousSubSet(this, var2, var1);
241    }
242    if (di != null) {
243      return di;
244    }
245
246    VarInfo subvar, supervar;
247
248    subvar = var1;
249    supervar = var2;
250
251    // Uninteresting if this is of the form x[0..i] subsequence
252    // x[0..j].  Not necessarily obvious.
253    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
254    if (subvar_super == supervar) {
255      debug.fine("  returning true because subvar_super == supervar");
256      return new DiscardInfo(this, DiscardCode.obvious, "x[0..i] subsequence of x[0..j] is uninteresting");
257    }
258
259    VarInfo supervar_super = supervar.isDerivedSubSequenceOf();
260    if (subvar_super != null && subvar_super == supervar_super) {
261      debug.fine("  returning true because subvar_super == supervar_super");
262      return new DiscardInfo(this, DiscardCode.obvious, "x[0..i] subsequence of x[0..j] is uninteresting");
263    }
264
265    di = SubSequence.isObviousSubSequence(this, var1, var2);
266    if (di == null) {
267      di = SubSequence.isObviousSubSequence(this, var2, var1);
268    }
269    if (di != null) {
270      return di;
271    }
272    return super.isObviousStatically(vis);
273  }
274
275  // Look up a previously instantiated SubSet relationship.
276  public static @Nullable SubSetFloat find(PptSlice ppt) {
277    assert ppt.arity() == 2;
278    for (Invariant inv : ppt.invs) {
279      if (inv instanceof SubSetFloat) {
280        return (SubSetFloat) inv;
281      }
282    }
283    return null;
284  }
285
286  @Pure
287  @Override
288  public boolean isSameFormula(Invariant other) {
289    assert other instanceof SubSetFloat;
290    return true;
291  }
292
293  /** NI suppressions, initialized in get_ni_suppressions() */
294  private static @Nullable NISuppressionSet suppressions = null;
295
296  /** returns the ni-suppressions for SubSetFloat */
297  @Pure
298  @Override
299  public NISuppressionSet get_ni_suppressions() {
300    if (suppressions == null) {
301      NISuppressee suppressee = new NISuppressee(SubSetFloat.class, 2);
302
303      // suppressor definitions (used in suppressions below)
304      NISuppressor v1_eq_v2 = new NISuppressor(0, 1, SeqSeqFloatEqual.class);
305      NISuppressor v1_pw_eq_v2 = new NISuppressor(0, 1, PairwiseFloatEqual.class);
306
307      // sub/super set suppressions.  We have both SeqSeq and Pairwise
308      // as suppressions because each can be enabled separately.
309      suppressions = new NISuppressionSet(
310          new NISuppression[] {
311              // a[] == b[] ==> a[] sub/superset b[]
312              new NISuppression(v1_eq_v2, suppressee),
313              // a[] == b[] ==> a[] sub/superset b[]
314              new NISuppression(v1_pw_eq_v2, suppressee),
315          });
316    }
317
318    return suppressions;
319  }
320}