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