Source code

001// ***** This file is automatically generated from OneOf.java.jpp
002
003package daikon.inv.unary.scalar;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.unary.OneOf;
008
009  import daikon.derive.unary.*;
010  import daikon.inv.binary.sequenceScalar.*;
011  import daikon.inv.unary.sequence.*;
012
013import java.io.*;
014import java.util.logging.Logger;
015import java.util.logging.Level;
016import java.util.*;
017
018import org.checkerframework.checker.initialization.qual.Initialized;
019import org.checkerframework.checker.interning.qual.Interned;
020import org.checkerframework.checker.lock.qual.GuardSatisfied;
021import org.checkerframework.checker.nullness.qual.NonNull;
022import org.checkerframework.checker.nullness.qual.Nullable;
023import org.checkerframework.dataflow.qual.Pure;
024import org.checkerframework.dataflow.qual.SideEffectFree;
025import org.checkerframework.framework.qual.Unused;
026import org.plumelib.reflection.Signatures;
027import org.plumelib.util.ArraysPlume;
028import org.plumelib.util.Intern;
029import org.plumelib.util.StringsPlume;
030import org.plumelib.util.UtilPlume;
031import typequals.prototype.qual.NonPrototype;
032import typequals.prototype.qual.Prototype;
033
034// This subsumes an "exact" invariant that says the value is always exactly
035// a specific value.  Do I want to make that a separate invariant
036// nonetheless?  Probably not, as this will simplify implication and such.
037
038  /**
039   * Represents double variables that take on only a few distinct values. Prints as either
040   * {@code x == c} (when there is only one value) or as {@code x one of {c1, c2, c3}}
041   * (when there are multiple values).
042
043   */
044
045@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
046public final class OneOfFloat extends SingleFloat implements OneOf {
047  // We are Serializable, so we specify a version to allow changes to
048  // method signatures without breaking serialization.  If you add or
049  // remove fields, you should change this number to the current date.
050  static final long serialVersionUID = 20030822L;
051
052  /** Debugging logger. */
053  public static final Logger debug =
054    Logger.getLogger(OneOfFloat.class.getName());
055
056  // Variables starting with dkconfig_ should only be set via the
057  // daikon.config.Configuration interface.
058  /** Boolean. True iff OneOf invariants should be considered. */
059  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
060
061  /**
062   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
063   * {@code size} items).
064   */
065
066  public static int dkconfig_size = 3;
067
068  // Probably needs to keep its own list of the values, and number of each seen.
069  // (That depends on the slice; maybe not until the slice is cleared out.
070  // But so few values is cheap, so this is quite fine for now and long-term.)
071
072  @Unused(when=Prototype.class)
073  private double[] elts;
074  @Unused(when=Prototype.class)
075  private int num_elts;
076
077  @Prototype OneOfFloat() {
078    super();
079  }
080
081  OneOfFloat(PptSlice slice) {
082    super(slice);
083
084    elts = new double[dkconfig_size];
085
086    num_elts = 0;
087
088  }
089
090  private static @Prototype OneOfFloat proto = new @Prototype OneOfFloat();
091
092  /** Returns the prototype invariant for OneOfFloat */
093  public static @Prototype OneOfFloat get_proto() {
094    return proto;
095  }
096
097  /** returns whether or not this invariant is enabled */
098  @Override
099  public boolean enabled() {
100    return dkconfig_enabled;
101  }
102
103  /** instantiate an invariant on the specified slice */
104  @Override
105  public OneOfFloat instantiate_dyn(@Prototype OneOfFloat this, PptSlice slice) {
106    return new OneOfFloat(slice);
107  }
108
109  @Pure
110  public boolean is_boolean(@GuardSatisfied OneOfFloat this) {
111    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
112  }
113  @Pure
114  public boolean is_hashcode(@GuardSatisfied OneOfFloat this) {
115    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
116  }
117
118  @SideEffectFree
119  @Override
120  public OneOfFloat clone(@GuardSatisfied OneOfFloat this) {
121    OneOfFloat result = (OneOfFloat) super.clone();
122    result.elts = elts.clone();
123
124    result.num_elts = this.num_elts;
125    return result;
126  }
127
128  @Override
129  public int num_elts() {
130    return num_elts;
131  }
132
133  @Override
134  public Object elt() {
135    return elt(0);
136  }
137
138  public Object elt(int index) {
139    if (num_elts <= index) {
140      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
141    }
142
143    return Intern.internedDouble(elts[index]);
144  }
145
146  private void sort_rep(@GuardSatisfied OneOfFloat this) {
147    Arrays.sort(elts, 0, num_elts );
148  }
149
150  public double min_elt() {
151    if (num_elts == 0) {
152      throw new Error("Represents no elements");
153    }
154    sort_rep();
155    return elts[0];
156  }
157
158  public double max_elt() {
159    if (num_elts == 0) {
160      throw new Error("Represents no elements");
161    }
162    sort_rep();
163    return elts[num_elts - 1];
164  }
165
166  // Assumes the other array is already sorted
167  public boolean compare_rep(int num_other_elts, double[] other_elts) {
168    if (num_elts != num_other_elts) {
169      return false;
170    }
171    sort_rep();
172    for (int i = 0; i < num_elts; i++) {
173      if (!(Global.fuzzy.eq(elts[i], other_elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other_elts[i])))) { // elements are interned
174        return false;
175      }
176    }
177    return true;
178  }
179
180  private String subarray_rep(@GuardSatisfied OneOfFloat this) {
181    // Not so efficient an implementation, but simple;
182    // and how often will we need to print this anyway?
183    sort_rep();
184    StringBuilder sb = new StringBuilder();
185    sb.append("{ ");
186    for (int i = 0; i < num_elts; i++) {
187      if (i != 0) {
188        sb.append(", ");
189      }
190
191      if (PrintInvariants.dkconfig_static_const_infer) {
192        boolean curVarMatch = false;
193        PptTopLevel pptt = ppt.parent;
194        for (VarInfo vi : pptt.var_infos) {
195          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
196            // If variable is a double, then use fuzzy comparison
197            if (vi.rep_type == ProglangType.DOUBLE) {
198              Double constantVal = (Double)vi.constantValue();
199              if (Global.fuzzy.eq(constantVal, elts[i]) || (Double.isNaN(constantVal) && Double.isNaN(elts[i]))) {
200                sb.append(vi.name());
201                curVarMatch = true;
202              }
203            }
204            // Otherwise just use the equals method
205            else {
206              Object constantVal = vi.constantValue();
207              if (constantVal.equals(elts[i])) {
208                sb.append(vi.name());
209                curVarMatch = true;
210              }
211            }
212          }
213        }
214
215        if (curVarMatch == false) {
216          sb.append((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
217        }
218      } else {
219        sb.append((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
220      }
221
222    }
223    sb.append(" }");
224    return sb.toString();
225  }
226
227  @Override
228  public String repr(@GuardSatisfied OneOfFloat this) {
229    return "OneOfFloat" + varNames() + ": falsified=" + falsified
230      + ", num_elts=" + num_elts
231      + ", elts=" + subarray_rep();
232  }
233
234  public double[] getElts() {
235    double[] temp = new double[elts.length];
236    for (int i = 0; i < elts.length; i++) {
237      temp[i] = elts[i];
238    }
239    return temp;
240  }
241
242  @SideEffectFree
243  @Override
244  public String format_using(@GuardSatisfied OneOfFloat this, OutputFormat format) {
245    sort_rep();
246
247    if (format.isJavaFamily()) {
248      return format_java_family(format);
249    }
250
251    if (format == OutputFormat.DAIKON) {
252      return format_daikon();
253    } else if (format == OutputFormat.SIMPLIFY) {
254      return format_simplify();
255    } else if (format == OutputFormat.ESCJAVA) {
256      String result = format_esc();
257      return result;
258    } else if (format == OutputFormat.CSHARPCONTRACT) {
259      return format_csharp_contract();
260    } else {
261      return format_unimplemented(format);
262    }
263  }
264
265  public String format_daikon(@GuardSatisfied OneOfFloat this) {
266    String varname = var().name();
267    if (num_elts == 1) {
268
269        if (PrintInvariants.dkconfig_static_const_infer) {
270          PptTopLevel pptt = ppt.parent;
271          for (VarInfo vi : pptt.var_infos) {
272            if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
273              if (vi.rep_type == ProglangType.DOUBLE) {
274                Double constantVal = (Double)vi.constantValue();
275                if (Global.fuzzy.eq(constantVal, elts[0]) || (Double.isNaN(constantVal) && Double.isNaN(elts[0]))) {
276                  return varname + " == " + vi.name();
277                }
278              } else {
279                Object constantVal = vi.constantValue();
280                if (constantVal.equals(elts[0])) {
281                  return varname + " == " + vi.name();
282                }
283              }
284            }
285          }
286        }
287        return varname + " == " + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0]));
288    } else {
289      return varname + " one of " + subarray_rep();
290    }
291  }
292
293  public String format_esc(@GuardSatisfied OneOfFloat this) {
294    sort_rep();
295
296    String varname = var().esc_name();
297
298    String result;
299
300    {
301      result = "";
302      for (int i = 0; i < num_elts; i++) {
303        if (i != 0) { result += " || "; }
304        result += varname + " == " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
305      }
306    }
307
308    return result;
309  }
310
311public String format_csharp_contract(@GuardSatisfied OneOfFloat this) {
312
313    @NonNull @Initialized String result;
314
315  String varname = var().csharp_name();
316
317      if (num_elts == 1) {
318        result = varname + " == " + elts[0];
319      } else {
320        List<String> e = new ArrayList<>();
321        for (int i = 0; i < num_elts; i++) {
322          e.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
323        }
324        String exp = String.join(", ", e);
325
326        if (var().is_array() && !var().isDerived()) {
327          String[] split = var().csharp_array_split();
328          result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf(" + exp + "))";
329        } else {
330          result = varname + ".OneOf(" + exp + ")";
331        }
332      }
333
334    return result;
335  }
336
337  public String format_java_family(@GuardSatisfied OneOfFloat this, OutputFormat format) {
338
339    String result;
340
341    // Setting up the name of the unary variable
342    String varname = var().name_using(format);
343
344    {
345      result = "";
346      for (int i = 0; i < num_elts; i++) {
347        if (i != 0) { result += " || "; }
348
349        result += "daikon.Quant.fuzzy.eq(" + varname + ", " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])) + ")";
350
351      }
352    }
353
354    return result;
355  }
356
357  public String format_simplify(@GuardSatisfied OneOfFloat this) {
358
359    sort_rep();
360
361    String varname =
362      var().simplifyFixup(var().name_using(OutputFormat.SIMPLIFY));
363
364    String result;
365
366    {
367      result = "";
368      for (int i = 0; i < num_elts; i++) {
369        result += " (EQ " + varname + " " + simplify_format_double(elts[i]) + ")";
370      }
371      if (num_elts > 1) {
372        result = "(OR" + result + ")";
373      } else if (num_elts == 1) {
374        // chop leading space
375        result = result.substring(1);
376      } else {
377        // Haven't actually seen any data, so we're vacuously true
378        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
379      }
380    }
381
382    if (result.indexOf("format_simplify") == -1) {
383      daikon.simplify.SimpUtil.assert_well_formed(result);
384    }
385    return result;
386  }
387
388  @Override
389  public InvariantStatus add_modified(double a, int count) {
390    return runValue(a, count, true);
391  }
392
393  @Override
394  public InvariantStatus check_modified(double a, int count) {
395    return runValue(a, count, false);
396  }
397
398  private InvariantStatus runValue(double v, int count, boolean mutate) {
399    InvariantStatus status;
400    if (mutate) {
401      status = add_mod_elem(v, count);
402    } else {
403      status = check_mod_elem(v, count);
404    }
405    if (status == InvariantStatus.FALSIFIED) {
406      if (logOn() && mutate) {
407        StringBuilder eltString = new StringBuilder();
408        for (int i = 0; i < num_elts; i++) {
409          eltString.append((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])) + " ");
410        }
411        log("destroyed on sample %s previous vals = {%s} num_elts = %s",
412             (Double.isNaN(v) ? "Double.NaN" : String.valueOf(v)), eltString, num_elts);
413      }
414      return InvariantStatus.FALSIFIED;
415    }
416    return status;
417  }
418
419  /**
420   * Adds a single sample to the invariant. Returns
421   * the appropriate InvariantStatus from the result
422   * of adding the sample to this.
423   */
424  public InvariantStatus add_mod_elem(double v, int count) {
425    InvariantStatus status = check_mod_elem(v, count);
426    if (status == InvariantStatus.WEAKENED) {
427      elts[num_elts] = v;
428      num_elts++;
429    }
430    return status;
431  }
432
433  /**
434   * Checks a single sample to the invariant. Returns
435   * the appropriate InvariantStatus from the result
436   * of adding the sample to this.
437   */
438  public InvariantStatus check_mod_elem(double v, int count) {
439
440    // Look for v in our list of previously seen values.  If it's
441    // found, we're all set.
442    for (int i = 0; i < num_elts; i++) {
443      // if (logDetail())
444      //  log ("add_modified (" + v + ")");
445      if ((Global.fuzzy.eq(elts[i], v) || (Double.isNaN(elts[i]) && Double.isNaN( v)))) {
446        return InvariantStatus.NO_CHANGE;
447      }
448    }
449
450    if (num_elts == dkconfig_size) {
451      return InvariantStatus.FALSIFIED;
452    }
453
454    return InvariantStatus.WEAKENED;
455  }
456
457  @Override
458  protected double computeConfidence() {
459    // This is not ideal.
460    if (num_elts == 0) {
461      return Invariant.CONFIDENCE_UNJUSTIFIED;
462    } else {
463      return Invariant.CONFIDENCE_JUSTIFIED;
464    }
465  }
466
467  @Pure
468  @Override
469  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
470    // Static constants are necessarily OneOf precisely one value.
471    // This removes static constants from the output, which might not be
472    // desirable if the user doesn't know their actual value.
473    if (vis[0].isStaticConstant()) {
474      assert num_elts <= 1;
475      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
476    }
477    return super.isObviousStatically(vis);
478  }
479
480  @Pure
481  @Override
482  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
483    DiscardInfo super_result = super.isObviousDynamically(vis);
484    if (super_result != null) {
485      return super_result;
486    }
487
488    VarInfo v = vis[0];
489
490    Debug dlog = new Debug(getClass(), ppt, vis);
491
492    if (logOn()) {
493      dlog.log("enter isObviousDynamically");
494    }
495
496      // We can use the minvalue and maxvalue custom attributes here: if
497      // minimum value and maximum value are the same as the reported
498      // value, then we can suppress this invariant
499      if (num_elts == 1
500          && v.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
501          && v.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
502        int min = v.aux.getInt(VarInfoAux.MINIMUM_VALUE),
503            max = v.aux.getInt(VarInfoAux.MAXIMUM_VALUE);
504        if (min == max && min == elts[0]) {
505          return new DiscardInfo(
506              this,
507              DiscardCode.obvious,
508              v.name() + "'s value matches with the expected value");
509        }
510      }
511
512      // We can check if all values in the list match with the ones we know about
513      // (useful for booleans and numeric enumerations).
514      if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
515        String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
516        Set<Double> setValidValues = new TreeSet<>();
517        for (String s : vsValidValues) {
518          setValidValues.add(Double.valueOf(s));
519        }
520        Set<Double> setValuesInvariant = new TreeSet<>();
521        for (double e : elts) {
522          setValuesInvariant.add(e);
523        }
524        if (setValidValues.equals(setValuesInvariant)) {
525          return new DiscardInfo(this, DiscardCode.obvious,
526            "The value list matches the allowed value list");
527        }
528      }
529
530    // Obvious if we are 'size(array) == 0'  The thinking is that this
531    // will also always show up as 'array == []' which is a little more
532    // illuminating.  At this point we insist that we are a SequenceLength
533    // derivation of a base (underived) array.  Its quite possible this should
534    // just apply to all arrays.
535    if (v.isDerived() && (v.derived instanceof SequenceLength)
536      && (num_elts == 1) && (elts[0] == 0)) {
537      @NonNull VarInfo b = v.derived.getBase(0);
538      if (!b.isDerived()) {
539        if (logOn()) {
540          dlog.log("isObviousDynamically '" + v.name()
541                    + " == 0' ==> '" + b.name() + " == []'");
542        }
543        return new DiscardInfo(this, DiscardCode.obvious, "size(array) == 0 is implied by array == []");
544      }
545    }
546
547    if (v.isDerived() && (v.derived instanceof SequenceLength)) {
548      @NonNull SequenceLength sl = (SequenceLength) v.derived;
549      if (sl.shift != 0) {
550        String discardString = v.name() + " is derived with shift!=0 (shift==" + sl.shift + ")";
551        return new DiscardInfo(this, DiscardCode.obvious, discardString);
552      }
553    }
554
555    // For every EltOneOfFloat at this program point, see if this variable is
556    // an obvious member of that sequence.
557    PptTopLevel parent = ppt.parent;
558    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
559      Invariant inv = itor.next();
560      if ((inv instanceof EltOneOfFloat) && inv.enoughSamples()) {
561        VarInfo v1 = var();
562        VarInfo v2 = inv.ppt.var_infos[0];
563        // System.out.println("isObviousImplied: calling  Member.isObviousMember(" + v1.name + ", " + v2.name + ")");
564        // Don't use isEqualToObviousMember:  that is too subtle
565        // and eliminates desirable invariants such as "return == null".
566        if (Member.isObviousMember(v1, v2)) {
567          EltOneOfFloat other = (EltOneOfFloat) inv;
568          if (num_elts == other.num_elts()) {
569            sort_rep();
570            if (other.compare_rep(num_elts, elts)) {
571              // System.out.println("isObviousImplied true");
572              String discardString = v1.name()+" is a member of "+v2.name()+" for which this Invariant also holds";
573              return new DiscardInfo(this, DiscardCode.obvious, discardString);
574            }
575          }
576        }
577      }
578    }
579
580    return null;
581  }
582
583  /**
584   * Oneof can merge different formulas from lower points to create a single formula at an upper
585   * point.
586   */
587  @Override
588  public boolean mergeFormulasOk() {
589    return true;
590  }
591
592  @Pure
593  @Override
594  public boolean isSameFormula(Invariant o) {
595    OneOfFloat other = (OneOfFloat) o;
596    if (num_elts != other.num_elts) {
597      return false;
598    }
599    if (num_elts == 0 && other.num_elts == 0) {
600      return true;
601    }
602
603    sort_rep();
604    other.sort_rep();
605
606    for (int i = 0; i < num_elts; i++) {
607      if (!(Global.fuzzy.eq(elts[i], other.elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[i])))) {
608        return false;
609      }
610    }
611
612    return true;
613  }
614
615  @Pure
616  @Override
617  public boolean isExclusiveFormula(Invariant o) {
618    if (o instanceof OneOfFloat) {
619      OneOfFloat other = (OneOfFloat) o;
620
621      if (num_elts == 0 || other.num_elts == 0) {
622        return false;
623      }
624      for (int i = 0; i < num_elts; i++) {
625        for (int j = 0; j < other.num_elts; j++) {
626          if ((Global.fuzzy.eq(elts[i], other.elts[j]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[j])))) // elements are interned
627            return false;
628        }
629      }
630
631      return true;
632    }
633
634    // Many more checks can be added here:  against nonzero, modulus, etc.
635    if ((o instanceof NonZeroFloat) && (num_elts == 1) && (elts[0] == 0)) {
636      return true;
637    }
638    double elts_min = Double.MAX_VALUE;
639    double elts_max = Double.MIN_VALUE;
640    for (int i = 0; i < num_elts; i++) {
641      elts_min = Math.min(elts_min, elts[i]);
642      elts_max = Math.max(elts_max, elts[i]);
643    }
644    if ((o instanceof LowerBoundFloat) && (elts_max < ((LowerBoundFloat)o).min())) {
645      return true;
646    }
647    if ((o instanceof UpperBoundFloat) && (elts_min > ((UpperBoundFloat)o).max())) {
648      return true;
649    }
650
651    return false;
652  }
653
654  @Override
655  public boolean hasUninterestingConstant() {
656
657    for (int i = 0; i < num_elts; i++) {
658      if (elts[i] < -1.0 || elts[i] > 2.0 || elts[i] != (long)elts[i]) {
659        return true;
660      }
661    }
662
663    return false;
664  }
665
666  @Pure
667  @Override
668  public boolean isExact() {
669    return num_elts == 1;
670  }
671
672  // Look up a previously instantiated invariant.
673  public static @Nullable OneOfFloat find(PptSlice ppt) {
674    assert ppt.arity() == 1;
675    for (Invariant inv : ppt.invs) {
676      if (inv instanceof OneOfFloat) {
677        return (OneOfFloat) inv;
678      }
679    }
680    return null;
681  }
682
683  // Interning is lost when an object is serialized and deserialized.
684  // Manually re-intern any interned fields upon deserialization.
685  private void readObject(ObjectInputStream in) throws IOException,
686    ClassNotFoundException {
687    in.defaultReadObject();
688
689    for (int i = 0; i < num_elts; i++) {
690      elts[i] = Intern.intern(elts[i]);
691    }
692  }
693
694  /**
695   * Merge the invariants in invs to form a new invariant. Each must be a OneOfFloat invariant.
696   * This code finds all of the oneof values from each of the invariants and returns the merged
697   * invariant (if any).
698   *
699   * @param invs list of invariants to merge. The invariants must all be of the same type and should
700   *     come from the children of parent_ppt. They should also all be permuted to match the
701   *     variable order in parent_ppt.
702   * @param parent_ppt slice that will contain the new invariant
703   */
704  @Override
705  public @Nullable Invariant merge(List<Invariant> invs, PptSlice parent_ppt) {
706
707    // Create the initial parent invariant from the first child
708    OneOfFloat  first = (OneOfFloat) invs.get(0);
709    OneOfFloat result = first.clone();
710    result.ppt = parent_ppt;
711
712    // Loop through the rest of the child invariants
713    for (int i = 1; i < invs.size(); i++ ) {
714
715      // Get this invariant
716      OneOfFloat inv = (OneOfFloat) invs.get(i);
717
718      // Loop through each distinct value found in this child and add
719      // it to the parent.  If the invariant is falsified, there is no parent
720      // invariant
721      for (int j = 0; j < inv.num_elts; j++) {
722        double val = inv.elts[j];
723
724        InvariantStatus status = result.add_mod_elem(val, 1);
725        if (status == InvariantStatus.FALSIFIED) {
726
727          result.log("%s", "child value '" + val + "' destroyed oneof");
728
729          return null;
730        }
731      }
732    }
733
734    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
735    return result;
736  }
737
738  /**
739   * Setup the invariant with the specified elements. Normally used when searching for a specified
740   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
741   */
742  public void set_one_of_val(double[] vals) {
743
744    num_elts = vals.length;
745    for (int i = 0; i < num_elts; i++) {
746      elts[i] = Intern.intern(vals[i]);
747    }
748  }
749
750  /**
751   * Returns true if every element in this invariant is contained in the specified state. For
752   * example if x = 1 and the state contains 1 and 2, true will be returned.
753   */
754  @Override
755  public boolean state_match(Object state) {
756
757    if (num_elts == 0) {
758      return false;
759    }
760
761    if (!(state instanceof double[])) {
762      // Daikon is about to crash.  Produce some debugging output.
763      System.out.printf("state = %s [%s]%n", state, state.getClass());
764      System.out.printf("problem with %s%n", this);
765    }
766    double[] e = (double[]) state;
767    for (int i = 0; i < num_elts; i++) {
768      boolean match = false;
769      for (int j = 0; j < e.length; j++) {
770        if (elts[i] == e[j]) {
771          match = true;
772          break;
773        }
774      }
775      if (!match) {
776        return false;
777      }
778    }
779    return true;
780  }
781
782}