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

package daikon.inv.unary.scalar;

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

  import daikon.derive.unary.*;
  import daikon.inv.binary.sequenceScalar.*;
  import daikon.inv.unary.sequence.*;

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 double 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 OneOfFloat extends SingleFloat implements OneOf {
  static final long serialVersionUID = 20030822L;

  /** Debugging logger. */
  public static final Logger debug =
    Logger.getLogger(OneOfFloat.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;

  // 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 double[] elts;
  @Unused(when=Prototype.class)
  private int num_elts;

  @Prototype OneOfFloat() {
    super();
  }

  OneOfFloat(PptSlice slice) {
    super(slice);

    elts = new double[dkconfig_size];

    num_elts = 0;

  }

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

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

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

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

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

  @SideEffectFree
  @Override
  public OneOfFloat clone(@GuardSatisfied OneOfFloat this) {
    OneOfFloat result = (OneOfFloat) super.clone();
    result.elts = elts.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 Intern.internedDouble(elts[index]);
  }

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

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

  public double 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, double[] other_elts) {
    if (num_elts != num_other_elts) {
      return false;
    }
    sort_rep();
    for (int i = 0; i < num_elts; i++) {
      if (!(Global.fuzzy.eq(elts[i], other_elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other_elts[i])))) { // elements are interned
        return false;
      }
    }
    return true;
  }

  private String subarray_rep(@GuardSatisfied OneOfFloat 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())) {
            // If variable is a double, then use fuzzy comparison
            if (vi.rep_type == ProglangType.DOUBLE) {
              Double constantVal = (Double)vi.constantValue();
              if (Global.fuzzy.eq(constantVal, elts[i]) || (Double.isNaN(constantVal) && Double.isNaN(elts[i]))) {
                sj.add(vi.name());
                curVarMatch = true;
              }
            }
            // Otherwise just use the equals method
            else {
              Object constantVal = vi.constantValue();
              if (constantVal.equals(elts[i])) {
                sj.add(vi.name());
                curVarMatch = true;
              }
            }
          }
        }

        if (curVarMatch == false) {
          sj.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
        }
      } else {
        sj.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
      }

    }
    return sj.toString();
  }

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

  public double[] getElts() {
    double[] temp = new double[elts.length];
    for (int i = 0; i < elts.length; i++) {
      temp[i] = elts[i];
    }
    return temp;
  }

  @SideEffectFree
  @Override
  public String format_using(@GuardSatisfied OneOfFloat 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 OneOfFloat this) {
    String varname = var().name();
    if (num_elts == 1) {

        if (PrintInvariants.dkconfig_static_const_infer) {
          PptTopLevel pptt = ppt.parent;
          for (VarInfo vi : pptt.var_infos) {
            if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
              if (vi.rep_type == ProglangType.DOUBLE) {
                Double constantVal = (Double)vi.constantValue();
                if (Global.fuzzy.eq(constantVal, elts[0]) || (Double.isNaN(constantVal) && Double.isNaN(elts[0]))) {
                  return varname + " == " + vi.name();
                }
              } else {
                Object constantVal = vi.constantValue();
                if (constantVal.equals(elts[0])) {
                  return varname + " == " + vi.name();
                }
              }
            }
          }
        }
        return varname + " == " + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0]));
    } else {
      return varname + " one of " + subarray_rep();
    }
  }

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

    String varname = var().esc_name();

    String result;

    {
      result = "";
      for (int i = 0; i < num_elts; i++) {
        if (i != 0) { result += " || "; }
        result += varname + " == " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
      }
    }

    return result;
  }

public String format_csharp_contract(@GuardSatisfied OneOfFloat this) {

    @NonNull @Initialized String result;

  String varname = var().csharp_name();

      if (num_elts == 1) {
        result = varname + " == " + elts[0];
      } else {
        List<String> e = new ArrayList<>();
        for (int i = 0; i < num_elts; i++) {
          e.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
        }
        String exp = String.join(", ", e);

        if (var().is_array() && !var().isDerived()) {
          String[] split = var().csharp_array_split();
          result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf(" + exp + "))";
        } else {
          result = varname + ".OneOf(" + exp + ")";
        }
      }

    return result;
  }

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

    String result;

    // Setting up the name of the unary variable
    String varname = var().name_using(format);

    {
      result = "";
      for (int i = 0; i < num_elts; i++) {
        if (i != 0) {
          result += " || ";
        }

        result += "daikon.Quant.fuzzy.eq(" + varname + ", " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])) + ")";

      }
    }

    return result;
  }

  public String format_simplify(@GuardSatisfied OneOfFloat this) {

    sort_rep();

    String varname =
      var().simplifyFixup(var().name_using(OutputFormat.SIMPLIFY));

    String result;

    {
      result = "";
      for (int i = 0; i < num_elts; i++) {
        result += " (EQ " + varname + " " + simplify_format_double(elts[i]) + ")";
      }
      if (num_elts > 1) {
        result = "(OR" + result + ")";
      } else if (num_elts == 1) {
        // chop leading space
        result = result.substring(1);
      } else {
        // Haven't actually seen any data, so we're vacuously true
        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
      }
    }

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

  @Override
  public InvariantStatus add_modified(double a, int count) {
    return runValue(a, count, true);
  }

  @Override
  public InvariantStatus check_modified(double a, int count) {
    return runValue(a, count, false);
  }

  private InvariantStatus runValue(double 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((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])) + " ");
        }
        log("destroyed on sample %s previous vals = {%s} num_elts = %s",
             (Double.isNaN(v) ? "Double.NaN" : String.valueOf(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(double 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(double 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 ((Global.fuzzy.eq(elts[i], v) || (Double.isNaN(elts[i]) && Double.isNaN( v)))) {
        return InvariantStatus.NO_CHANGE;
      }
    }

    if (num_elts == dkconfig_size) {
      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);
  }

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

    VarInfo v = vis[0];

    Debug dlog = new Debug(getClass(), ppt, vis);

    if (logOn()) {
      dlog.log("enter isObviousDynamically");
    }

      // We can use the minvalue and maxvalue custom attributes here: if
      // minimum value and maximum value are the same as the reported
      // value, then we can suppress this invariant
      if (num_elts == 1
          && v.aux.hasValue(VarInfoAux.MINIMUM_VALUE)
          && v.aux.hasValue(VarInfoAux.MAXIMUM_VALUE)) {
        int min = v.aux.getInt(VarInfoAux.MINIMUM_VALUE),
            max = v.aux.getInt(VarInfoAux.MAXIMUM_VALUE);
        if (min == max && min == elts[0]) {
          return new DiscardInfo(
              this,
              DiscardCode.obvious,
              v.name() + "'s value matches with the expected value");
        }
      }

      // We can check if all values in the list match with the ones we know about
      // (useful for booleans and numeric enumerations).
      if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
        String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
        Set<Double> setValidValues = new TreeSet<>();
        for (String s : vsValidValues) {
          setValidValues.add(Double.valueOf(s));
        }
        Set<Double> setValuesInvariant = new TreeSet<>();
        for (double e : elts) {
          setValuesInvariant.add(e);
        }
        if (setValidValues.equals(setValuesInvariant)) {
          return new DiscardInfo(this, DiscardCode.obvious,
            "The value list matches the allowed value list");
        }
      }

    // Obvious if we are 'size(array) == 0'  The thinking is that this
    // will also always show up as 'array == []' which is a little more
    // illuminating.  At this point we insist that we are a SequenceLength
    // derivation of a base (underived) array.  Its quite possible this should
    // just apply to all arrays.
    if (v.isDerived() && (v.derived instanceof SequenceLength)
      && (num_elts == 1) && (elts[0] == 0)) {
      @NonNull VarInfo b = v.derived.getBase(0);
      if (!b.isDerived()) {
        if (logOn()) {
          dlog.log("isObviousDynamically '" + v.name()
                    + " == 0' ==> '" + b.name() + " == []'");
        }
        return new DiscardInfo(this, DiscardCode.obvious, "size(array) == 0 is implied by array == []");
      }
    }

    if (v.isDerived() && (v.derived instanceof SequenceLength)) {
      @NonNull SequenceLength sl = (SequenceLength) v.derived;
      if (sl.shift != 0) {
        String discardString = v.name() + " is derived with shift!=0 (shift==" + sl.shift + ")";
        return new DiscardInfo(this, DiscardCode.obvious, discardString);
      }
    }

    // For every EltOneOfFloat at this program point, see if this variable is
    // an obvious member of that sequence.
    PptTopLevel parent = ppt.parent;
    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
      Invariant inv = itor.next();
      if ((inv instanceof EltOneOfFloat) && inv.enoughSamples()) {
        VarInfo v1 = var();
        VarInfo v2 = inv.ppt.var_infos[0];
        // System.out.println("isObviousImplied: calling  Member.isObviousMember(" + v1.name + ", " + v2.name + ")");
        // Don't use isEqualToObviousMember:  that is too subtle
        // and eliminates desirable invariants such as "return == null".
        if (Member.isObviousMember(v1, v2)) {
          EltOneOfFloat other = (EltOneOfFloat) inv;
          if (num_elts == other.num_elts()) {
            sort_rep();
            if (other.compare_rep(num_elts, elts)) {
              // System.out.println("isObviousImplied true");
              String discardString = v1.name()+" is a member of "+v2.name()+" for which this Invariant also holds";
              return new DiscardInfo(this, DiscardCode.obvious, discardString);
            }
          }
        }
      }
    }

    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) {
    OneOfFloat other = (OneOfFloat) o;
    if (num_elts != other.num_elts) {
      return false;
    }
    if (num_elts == 0 && other.num_elts == 0) {
      return true;
    }

    sort_rep();
    other.sort_rep();

    for (int i = 0; i < num_elts; i++) {
      if (!(Global.fuzzy.eq(elts[i], other.elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[i])))) {
        return false;
      }
    }

    return true;
  }

  @Pure
  @Override
  public boolean isExclusiveFormula(Invariant o) {
    if (o instanceof OneOfFloat) {
      OneOfFloat other = (OneOfFloat) 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 ((Global.fuzzy.eq(elts[i], other.elts[j]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[j])))) // elements are interned
            return false;
        }
      }

      return true;
    }

    // Many more checks can be added here:  against nonzero, modulus, etc.
    if ((o instanceof NonZeroFloat) && (num_elts == 1) && (elts[0] == 0)) {
      return true;
    }
    double elts_min = Double.MAX_VALUE;
    double elts_max = Double.MIN_VALUE;
    for (int i = 0; i < num_elts; i++) {
      elts_min = Math.min(elts_min, elts[i]);
      elts_max = Math.max(elts_max, elts[i]);
    }
    if ((o instanceof LowerBoundFloat) && (elts_max < ((LowerBoundFloat)o).min())) {
      return true;
    }
    if ((o instanceof UpperBoundFloat) && (elts_min > ((UpperBoundFloat)o).max())) {
      return true;
    }

    return false;
  }

  @Override
  public boolean hasUninterestingConstant() {

    for (int i = 0; i < num_elts; i++) {
      if (elts[i] < -1.0 || elts[i] > 2.0 || elts[i] != (long)elts[i]) {
        return true;
      }
    }

    return false;
  }

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

  // Look up a previously instantiated invariant.
  public static @Nullable OneOfFloat find(PptSlice ppt) {
    assert ppt.arity() == 1;
    for (Invariant inv : ppt.invs) {
      if (inv instanceof OneOfFloat) {
        return (OneOfFloat) 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 OneOfFloat 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 OneOfFloat merge(List<Invariant> invs, PptSlice parent_ppt) {

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

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

      // Get this invariant
      OneOfFloat inv = (OneOfFloat) 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++) {
        double val = inv.elts[j];

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

          result.log("%s", "child value '" + 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(double[] 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 double[])) {
      // 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);
    }
    double[] e = (double[]) 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;
  }

}
