// ***** This file is automatically generated from OneOf.java.jpp

package daikon.inv.unary.sequence;

import daikon.*;
import daikon.inv.*;
import daikon.inv.unary.OneOf;

import java.io.*;
import java.util.logging.Logger;
import java.util.logging.Level;
import java.util.*;

import org.checkerframework.checker.initialization.qual.Initialized;
import org.checkerframework.checker.interning.qual.Interned;
import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.qual.Unused;
import org.plumelib.reflection.Signatures;
import org.plumelib.util.ArraysPlume;
import org.plumelib.util.Intern;
import org.plumelib.util.StringsPlume;
import org.plumelib.util.UtilPlume;
import typequals.prototype.qual.NonPrototype;
import typequals.prototype.qual.Prototype;

// This subsumes an "exact" invariant that says the value is always exactly
// a specific value.  Do I want to make that a separate invariant
// nonetheless?  Probably not, as this will simplify implication and such.

  /**
   * Represents long[] variables that take on only a few distinct values. Prints as either
   * {@code x == c} (when there is only one value) or as {@code x one of {c1, c2, c3}}
   * (when there are multiple values).

   */

@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
public final class OneOfSequence extends SingleScalarSequence implements OneOf {
  static final long serialVersionUID = 20030822L;

  /** Debugging logger. */
  public static final Logger debug =
    Logger.getLogger(OneOfSequence.class.getName());

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /** Boolean. True iff OneOf invariants should be considered. */
  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;

  /**
   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
   * {@code size} items).
   */

  public static int dkconfig_size = 3;

  /**
   * Boolean. If true, invariants describing hashcode-typed variables as having any particular value
   * will have an artificial value substituted for the exact hashhode values. The artificial values
   * will stay the same from run to run even if the actual hashcode values change (as long as the
   * OneOf invariants remain the same). If false, hashcodes will be formatted as the application of
   * a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode.
   * One might wish to omit the exact values of the hashcodes because they are usually
   * uninteresting; this is the same reason they print in the native Daikon format, for instance, as
   * {@code var has only one value} rather than {@code var == 150924732}.
   */
  public static boolean dkconfig_omit_hashcode_values_Simplify = false;

  // Probably needs to keep its own list of the values, and number of each seen.
  // (That depends on the slice; maybe not until the slice is cleared out.
  // But so few values is cheap, so this is quite fine for now and long-term.)

  @Unused(when=Prototype.class)
  private long[] @Interned [] elts;
  @Unused(when=Prototype.class)
  private int num_elts;

  @Prototype OneOfSequence() {
    super();
  }

  OneOfSequence(PptSlice slice) {
    super(slice);

    // Elements are interned, so can test with ==
    // (in the general online case, it's not worth interning).
    elts = new long[dkconfig_size] @Interned [];

    num_elts = 0;

    // var() is initialized by the super constructor
    assert var().is_array() :
      String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array",
                     "OneOfSequence", var().name(), var().type, var().rep_type);

  }

  private static @Prototype OneOfSequence proto = new @Prototype OneOfSequence();

  /** Returns the prototype invariant for OneOfSequence */
  public static @Prototype OneOfSequence get_proto() {
    return proto;
  }

  @Override
  public boolean enabled() {
    return dkconfig_enabled;
  }

  @Override
  public OneOfSequence instantiate_dyn(@Prototype OneOfSequence this, PptSlice slice) {
    return new OneOfSequence(slice);
  }

  @Pure
  public boolean is_boolean(@GuardSatisfied OneOfSequence this) {
    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
  }
  @Pure
  public boolean is_hashcode(@GuardSatisfied OneOfSequence this) {
    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
  }

  @SideEffectFree
  @Override
  public OneOfSequence clone(@GuardSatisfied OneOfSequence this) {
    OneOfSequence result = (OneOfSequence) super.clone();
    result.elts = elts.clone();

    for (int i = 0; i < num_elts; i++) {
      result.elts[i] = Intern.intern(elts[i].clone());
    }

    result.num_elts = this.num_elts;
    return result;
  }

  @Override
  public int num_elts() {
    return num_elts;
  }

  @Override
  public Object elt() {
    return elt(0);
  }

  public Object elt(int index) {
    if (num_elts <= index) {
      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
    }

    return elts[index];
  }

  static Comparator<long[]> comparator = ArraysPlume.LongArrayComparatorLexical.it;

  private void sort_rep(@GuardSatisfied OneOfSequence this) {
    Arrays.sort(elts, 0, num_elts , comparator);
  }

  public long @Interned [] min_elt() {
    if (num_elts == 0) {
      throw new Error("Represents no elements");
    }
    sort_rep();
    return elts[0];
  }

  public long @Interned [] max_elt() {
    if (num_elts == 0) {
      throw new Error("Represents no elements");
    }
    sort_rep();
    return elts[num_elts - 1];
  }

  // Assumes the other array is already sorted
  public boolean compare_rep(int num_other_elts, long[] @Interned [] other_elts) {
    if (num_elts != num_other_elts) {
      return false;
    }
    sort_rep();
    for (int i = 0; i < num_elts; i++) {
      if (!((elts[i]) == (other_elts[i]))) { // elements are interned
        return false;
      }
    }
    return true;
  }

  private String subarray_rep(@GuardSatisfied OneOfSequence this) {
    // Not so efficient an implementation, but simple;
    // and how often will we need to print this anyway?
    sort_rep();
    StringJoiner sj = new StringJoiner(", ", "{ ", " }");
    for (int i = 0; i < num_elts; i++) {

      if (PrintInvariants.dkconfig_static_const_infer) {
        boolean curVarMatch = false;
        PptTopLevel pptt = ppt.parent;
        for (VarInfo vi : pptt.var_infos) {
          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
            Object constantVal = vi.constantValue();
            if (constantVal.equals(elts[i])) {
              sj.add(vi.name());
              curVarMatch = true;
            }
          }
        }

        if (curVarMatch == false) {
          sj.add(Arrays.toString(elts[i]));
        }
      } else {
        sj.add(Arrays.toString(elts[i]));
      }

    }
    return sj.toString();
  }

  @Override
  public String repr(@GuardSatisfied OneOfSequence this) {
    return "OneOfSequence" + varNames() + ": falsified=" + falsified
      + ", num_elts=" + num_elts
      + ", elts=" + subarray_rep();
  }

  private boolean all_nulls(@GuardSatisfied OneOfSequence this, int value_no) {
    long @Interned [] seq = elts[value_no];
    for (int i = 0; i < seq.length; i++) {
      if (seq[i] != 0) {
        return false;
      }
    }
    return true;
  }
  private boolean no_nulls(@GuardSatisfied OneOfSequence this, int value_no) {
    long @Interned [] seq = elts[value_no];
    for (int i = 0; i < seq.length; i++) {
      if (seq[i] == 0) {
        return false;
      }
    }
    return true;
  }

  @SideEffectFree
  @Override
  public String format_using(@GuardSatisfied OneOfSequence this, OutputFormat format) {
    sort_rep();

    if (format.isJavaFamily()) {
      return format_java_family(format);
    }

    if (format == OutputFormat.DAIKON) {
      return format_daikon();
    } else if (format == OutputFormat.SIMPLIFY) {
      return format_simplify();
    } else if (format == OutputFormat.ESCJAVA) {
      String result = format_esc();
      return result;
    } else if (format == OutputFormat.CSHARPCONTRACT) {
      return format_csharp_contract();
    } else {
      return format_unimplemented(format);
    }
  }

  public String format_daikon(@GuardSatisfied OneOfSequence this) {
    String varname = var().name();
    if (num_elts == 1) {

        if (is_hashcode()) {
          // we only have one value, because add_modified dies if more
          assert num_elts == 1;
          long @Interned [] value = elts[0];
          if (value.length == 0) {
            return varname + " == []";
          } else if ((value.length == 1) && (value[0] == 0)) {
            return varname + " == [null]";
          } else if (no_nulls(0)) {
            return varname + " contains no nulls and has only one value, of length " + value.length;
          } else if (all_nulls(0)) {
            return varname + " contains only nulls and has only one value, of length " + value.length;
          } else {
            return varname + " has only one value, of length " + value.length;
          }
        } else {
          if (PrintInvariants.dkconfig_static_const_infer) {
            PptTopLevel pptt = ppt.parent;
            for (VarInfo vi : pptt.var_infos) {
              if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
                Object constantVal = vi.constantValue();
                if (constantVal.equals(elts[0])) {
                  return varname + " == " + vi.name();
                }
              }
            }
          }
          return varname + " == " + Arrays.toString(elts[0]);
        }

    } else {
      return varname + " one of " + subarray_rep();
    }
  }

  public String format_esc(@GuardSatisfied OneOfSequence this) {
    sort_rep();

    String result;

    String length = null;
    String forall = null;

    if (is_hashcode()) {
      // we only have one value, because add_modified dies if more
      assert num_elts == 1;
      long @Interned [] value = elts[0];
      if (var().isArray()) {
        length = null;
        if (!var().isSlice()) {
          length = var().get_length().esc_name() + " == " + value.length;
        }
        String[] form = VarInfo.esc_quantify(var());
        if (no_nulls(0)) {
          forall = form[0] + "(" + form[1] + " != null)" + form[2];
        } else if (all_nulls(0)) {
          forall = form[0] + "(" + form[1] + " == null)" + form[2];
        }
      }
    }

    if (length == null) {
      if (forall == null) {
        return format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
      } else {
        result = forall;
      }
    } else {
      if (forall == null) {
        result = length;
      } else {
        result = "(" + length + ") && (" + forall + ")";
      }
    }

    return result;
  }

public String format_csharp_contract(@GuardSatisfied OneOfSequence this) {

    @NonNull @Initialized String result;

  result = "(\"oneOf.java.jpp: SEQUENCE unimplemented\" != null)"; // "interned"

    return result;
  }

  public String format_java_family(@GuardSatisfied OneOfSequence this, OutputFormat format) {

    String result;

    result = "(\"oneOf.java.jpp: SEQUENCE unimplemented\" != null)"; // "interned"

    return result;
  }

  public String format_simplify(@GuardSatisfied OneOfSequence this) {

    // if (is_hashcode() && dkconfig_omit_hashcode_values_Simplify)
    //   return "(AND)";

    sort_rep();

    String result;

    StringBuilder resultBuf = new StringBuilder();
    for (int i = 0; i < num_elts; i++) {
      long @Interned [] seq = elts[i];
      String offset = null;
      String contents = null;
      String[] bounds_name;
      String length = var().get_simplify_size_name();
      // if ((length == null) && var().name.isApplySizeSafe())
      //  System.out.printf("var %s, type %s, is_array %b%n", var().name(),
      //                     var().type, var().type.isArray());
      if (length != null) {
        length = "(EQ " + length + " "+ simplify_format_long(seq.length) + ")";
      } else if ((bounds_name = var().get_simplify_slice_bounds()) != null) {
        String size = "(+ 1 (- " + bounds_name[1] +" " + bounds_name[0] + "))";
        length = "(EQ " + size + " " + simplify_format_long(seq.length) + ")";
        offset = bounds_name[0];
      }

      if (is_hashcode()) {
        String[] form = VarInfo.simplify_quantify(var());
        if (no_nulls(i)) {
          contents = form[0] + "(NEQ " + form[1] + "  null)" + form[2];
        } else if (all_nulls(i)) {
          contents = form[0] + "(EQ " + form[1] + "  null)" + form[2];
        }
      } else {
        StringBuilder contentsBuf = new StringBuilder();
        for (int j = 0; j < seq.length; j++) {
          if (j + 3 < seq.length
              && ((seq[j]) == ( seq[j + 1]))
              && ((seq[j]) == ( seq[j + 2]))
              && ((seq[j]) == ( seq[j + 3]))) {
            // Compress a sequence of adjacent values
            int k = j + 4;
            for (; k < seq.length; k++) {
              if (!((seq[j]) == ( seq[k]))) {
                break;
              }
            }
            k--;
            String index_name = VarInfo.get_simplify_free_index(var());
            String cond_left;
            String cond_right;
            if (offset == null) {
              cond_left  = "(<= " + j + " " + index_name + ")";
              cond_right = "(<= " + index_name + " " + k + ")";
            } else {
              cond_left = "(<= (+ " + offset + " " + j + ") "
                + index_name + ")";
              cond_right = "(>= (+ " + offset + " " + k + ") "
                + index_name + ")";
            }
            String cond = "(AND " + cond_left + " " + cond_right + ")";
            String nth = var().get_simplify_selectNth(index_name, true, 0);
            String eq = "(EQ " + nth + " " + simplify_format_long(seq[j]) + ")";
            String implies = "(IMPLIES " + cond + " " + eq + ")";
            String forall = "(FORALL (" + index_name + ") " + implies + ")";
            contentsBuf.append(" " + forall);
            j = k;
          } else {
            // Output a single value
            String nth = var().get_simplify_selectNth_lower(j);
            if (nth == null) {
              String classname = this.getClass().toString().substring(6);
              result = "warning: method " + classname
                + ".format_simplify() needs to fix selectNth(): " + format();
              return result;
            }
            String value = simplify_format_long(seq[j]);
            contentsBuf.append(" (EQ " + nth + " " + value + ")");
            // if (nth.contains ("--orig__a"))
            //   System.out.printf("regular orig__a%n");

          }
        }
        if (seq.length > 1) {
          contents = "(AND " + contentsBuf.toString() + ")";
        } else if (seq.length == 1) {
          contents = contentsBuf.toString().substring(1);
        } else if (seq.length == 0) {
          contents = null; // back from ""
        }
      }
      if (length == null && contents == null) {
        resultBuf.append(" ");
      } else if (length == null && contents != null) {
        resultBuf.append(" " + contents);
      } else if (length != null && contents == null) {
        resultBuf.append(" " + length);
      } else {
        assert length != null && contents != null;
        resultBuf.append(" (AND " + length + " " + contents + ")");
      }

      }
    if (num_elts > 1) {
      result = "(OR" + resultBuf.toString() + ")";
    } else if (num_elts == 1) {
      // chop leading space
      result = resultBuf.toString().substring(1);
    } else if (num_elts == 0) {
      return format_too_few_samples(OutputFormat.SIMPLIFY, null);
    } else {
      throw new Error("this can't happen");
      // result = null;
    }
    if (result.trim().equals("")) {
      result = "format_simplify() failed on a weird OneOf";
    }

    if (result.indexOf("format_simplify") == -1) {
      daikon.simplify.SimpUtil.assert_well_formed(result);
    }
    return result;
  }

  @Override
  public InvariantStatus add_modified(long @Interned [] a, int count) {
    return runValue(a, count, true);
  }

  @Override
  public InvariantStatus check_modified(long @Interned [] a, int count) {
    return runValue(a, count, false);
  }

  private InvariantStatus runValue(long @Interned [] v, int count, boolean mutate) {
    InvariantStatus status;
    if (mutate) {
      status = add_mod_elem(v, count);
    } else {
      status = check_mod_elem(v, count);
    }
    if (status == InvariantStatus.FALSIFIED) {
      if (logOn() && mutate) {
        StringBuilder eltString = new StringBuilder();
        for (int i = 0; i < num_elts; i++) {
          eltString.append(Arrays.toString(elts[i]) + " ");
        }
        log("destroyed on sample %s previous vals = {%s} num_elts = %s",
             Arrays.toString(v), eltString, num_elts);
      }
      return InvariantStatus.FALSIFIED;
    }
    return status;
  }

  /**
   * Adds a single sample to the invariant. Returns
   * the appropriate InvariantStatus from the result
   * of adding the sample to this.
   */
  public InvariantStatus add_mod_elem(long @Interned [] v, int count) {
    InvariantStatus status = check_mod_elem(v, count);
    if (status == InvariantStatus.WEAKENED) {
      elts[num_elts] = v;
      num_elts++;
    }
    return status;
  }

  /**
   * Checks a single sample to the invariant. Returns
   * the appropriate InvariantStatus from the result
   * of adding the sample to this.
   */
  public InvariantStatus check_mod_elem(long @Interned [] v, int count) {

    // Look for v in our list of previously seen values.  If it's
    // found, we're all set.
    for (int i = 0; i < num_elts; i++) {
      // if (logDetail())
      //  log ("add_modified (" + v + ")");
      if (((elts[i]) == ( v))) {
        return InvariantStatus.NO_CHANGE;
      }
    }

    if (num_elts == dkconfig_size) {
      return InvariantStatus.FALSIFIED;
    }

    if (is_hashcode() && (num_elts == 1)) {
      return InvariantStatus.FALSIFIED;
    }

    return InvariantStatus.WEAKENED;
  }

  @Override
  protected double computeConfidence() {
    // This is not ideal.
    if (num_elts == 0) {
      return Invariant.CONFIDENCE_UNJUSTIFIED;
    } else {
      return Invariant.CONFIDENCE_JUSTIFIED;
    }
  }

  @Pure
  @Override
  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
    // Static constants are necessarily OneOf precisely one value.
    // This removes static constants from the output, which might not be
    // desirable if the user doesn't know their actual value.
    if (vis[0].isStaticConstant()) {
      assert num_elts <= 1;
      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
    }
    return super.isObviousStatically(vis);
  }

  @Override
  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    VarInfo v = vis[0];

    // We can check if all values in the element sequence match
    // with the ones we know about (useful for booleans and numeric
    // enumerations).
    if (v.aux.hasValue(VarInfoAux.VALID_VALUES)
        && v.aux.hasValue(VarInfoAux.MAXIMUM_LENGTH)
        && v.aux.hasValue(VarInfoAux.MINIMUM_LENGTH)
        && v.aux.getInt(VarInfoAux.MAXIMUM_LENGTH) == 1
        && v.aux.getInt(VarInfoAux.MINIMUM_LENGTH) == 1) {

      String[] vsValidValues       = v.aux.getList(VarInfoAux.VALID_VALUES);
      Set<Long> setValidValues = new TreeSet<>();
      for (String s : vsValidValues) {
        setValidValues.add(Long.valueOf(s));
      }
      Set<Long> setValuesInvariant = new TreeSet<>();
      for (long @Interned [] e : elts) {
        if (e == null) {
  continue;
}
        for (Long b : e) {
          setValuesInvariant.add(b);
        }
      }
      if (setValidValues.equals(setValuesInvariant)) {
        return new DiscardInfo(this, DiscardCode.obvious,
          "The value list matches the allowed value list");
      }
    }

    return null;
  }

  /**
   * Oneof can merge different formulas from lower points to create a single formula at an upper
   * point.
   */
  @Override
  public boolean mergeFormulasOk() {
    return true;
  }

  @Pure
  @Override
  public boolean isSameFormula(Invariant o) {
    OneOfSequence other = (OneOfSequence) o;
    if (num_elts != other.num_elts) {
      return false;
    }
    if (num_elts == 0 && other.num_elts == 0) {
      return true;
    }

    sort_rep();
    other.sort_rep();

    // All nonzero hashcode values should be considered equal to each other
    //
    // Examples:
    // inv1     inv2     result
    // -------  -------  ------
    // {19,23}  {91,0}   false
    // {19,23}  {91,32}  true
    // {19,0}   {91,0}   true
    // {0,0}    {0,0}    true

    if (is_hashcode() && other.is_hashcode()) {
      // we only have one value, because add_modified dies if more
      assert num_elts == 1 && other.num_elts == 1;

      long @Interned [] thisSeq = elts[0];
      long @Interned [] otherSeq = other.elts[0];
      if (thisSeq.length != otherSeq.length) {
        return false;
      }

      for (int i = 0; i < thisSeq.length; i++) {
        if ((thisSeq[i] == 0 && otherSeq[i] != 0)
            || (thisSeq[i] != 0 && otherSeq[i] == 0)) {
          return false;
        }
      }

      return true;
    }

    for (int i = 0; i < num_elts; i++) {
      if (!((elts[i]) == (other.elts[i]))) {
        return false;
      }
    }

    return true;
  }

  @Pure
  @Override
  public boolean isExclusiveFormula(Invariant o) {
    if (o instanceof OneOfSequence) {
      OneOfSequence other = (OneOfSequence) o;

      if (num_elts == 0 || other.num_elts == 0) {
        return false;
      }
      for (int i = 0; i < num_elts; i++) {
        for (int j = 0; j < other.num_elts; j++) {
          if (((elts[i]) == (other.elts[j]))) // elements are interned
            return false;
        }
      }

      // Be even more aggressive about rejecting these for use in
      // implications in this case, since, we'd be printing them as
      // "true"
      /*
      if (dkconfig_omit_hashcode_values_Simplify
          && (is_hashcode() || other.is_hashcode())) {
        return false;
      }
      */

      return true;
    }

    return false;
  }

  @Override
  public boolean hasUninterestingConstant() {

    for (int i = 0; i < num_elts; i++) {
      for (int j = 0; j < elts[i].length; j++) {
        if (elts[i][j] < -1 || elts[i][j] > 2) {
          return true;
        }
      }
    }

    return false;
  }

  @Pure
  @Override
  public boolean isExact() {
    return num_elts == 1;
  }

  // Look up a previously instantiated invariant.
  public static @Nullable OneOfSequence find(PptSlice ppt) {
    assert ppt.arity() == 1;
    for (Invariant inv : ppt.invs) {
      if (inv instanceof OneOfSequence) {
        return (OneOfSequence) inv;
      }
    }
    return null;
  }

  // Interning is lost when an object is serialized and deserialized.
  // Manually re-intern any interned fields upon deserialization.
  private void readObject(ObjectInputStream in) throws IOException,
    ClassNotFoundException {
    in.defaultReadObject();

    for (int i = 0; i < num_elts; i++) {
      elts[i] = Intern.intern(elts[i]);
    }
  }

  /**
   * Merge the invariants in invs to form a new invariant. Each must be a OneOfSequence invariant.
   * This code finds all of the oneof values from each of the invariants and returns the merged
   * invariant (if any).
   *
   * @param invs list of invariants to merge. The invariants must all be of the same type and should
   *     come from the children of parent_ppt. They should also all be permuted to match the
   *     variable order in parent_ppt.
   * @param parent_ppt slice that will contain the new invariant
   */
  @Override
  public @Nullable OneOfSequence merge(List<Invariant> invs, PptSlice parent_ppt) {

    // Create the initial parent invariant from the first child
    OneOfSequence  first = (OneOfSequence) invs.get(0);
    OneOfSequence result = first.clone();
    result.ppt = parent_ppt;

      for (int i = 0; i < result.num_elts; i++) {
        result.elts[i] = Intern.intern(result.elts[i]);
      }

    // Loop through the rest of the child invariants
    for (int i = 1; i < invs.size(); i++ ) {

      // Get this invariant
      OneOfSequence inv = (OneOfSequence) invs.get(i);

      // Loop through each distinct value found in this child and add
      // it to the parent.  If the invariant is falsified, there is no parent
      // invariant
      for (int j = 0; j < inv.num_elts; j++) {
        long @Interned [] val = inv.elts[j];

        val = Intern.intern(val);

        InvariantStatus status = result.add_mod_elem(val, 1);
        if (status == InvariantStatus.FALSIFIED) {

          result.log("%s", "child value '" + Arrays.toString(val) + "' destroyed oneof");

          return null;
        }
      }
    }

    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
    return result;
  }

  /**
   * Setup the invariant with the specified elements. Normally used when searching for a specified
   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
   */
  public void set_one_of_val(long[][] vals) {

    num_elts = vals.length;
    for (int i = 0; i < num_elts; i++) {
      elts[i] = Intern.intern(vals[i]);
    }
  }

  /**
   * Returns true if every element in this invariant is contained in the specified state. For
   * example if x = 1 and the state contains 1 and 2, true will be returned.
   */
  @Override
  public boolean state_match(Object state) {

    if (num_elts == 0) {
      return false;
    }

    if (!(state instanceof long[] @Interned [])) {
      // Daikon is about to crash.  Produce some debugging output.
      System.out.printf("state = %s [%s]%n", state, state.getClass());
      System.out.printf("problem with %s%n", this);
    }
    long[] @Interned [] e = (long[] @Interned []) state;
    for (int i = 0; i < num_elts; i++) {
      boolean match = false;
      for (int j = 0; j < e.length; j++) {
        if (elts[i] == e[j]) {
          match = true;
          break;
        }
      }
      if (!match) {
        return false;
      }
    }
    return true;
  }

}
