001package daikon.inv.unary.sequence;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.InvariantStatus;
006import org.checkerframework.checker.interning.qual.Interned;
007import org.plumelib.util.Intern;
008import typequals.prototype.qual.Prototype;
009
010/** Abstract base class for invariants over one variable of type {@code double[]}. */
011public abstract class SingleFloatSequence extends SingleSequence {
012  // We are Serializable, so we specify a version to allow changes to
013  // method signatures without breaking serialization.  If you add or
014  // remove fields, you should change this number to the current date.
015  static final long serialVersionUID = 20020813L;
016
017  protected SingleFloatSequence(PptSlice ppt) {
018    super(ppt);
019  }
020
021  protected @Prototype SingleFloatSequence() {
022    super();
023  }
024
025  /** Returns whether or not the specified types are valid. */
026  @Override
027  public final boolean valid_types(VarInfo[] vis) {
028    return ((vis.length == 1)
029        && vis[0].file_rep_type.baseIsFloat()
030        && vis[0].file_rep_type.isArray());
031  }
032
033  // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL.
034  // Subclasses need not override this except in special cases;
035  // just implement {@link #add_modified(Object,int)}.
036  @Override
037  public InvariantStatus add(@Interned Object val, int mod_index, int count) {
038    assert !falsified;
039    assert (mod_index >= 0) && (mod_index < 2);
040    assert Intern.isInterned(val);
041    // System.out.println("SingleFloatSequence.add(" + Arrays.toString(value) + ", " + modified + ",
042    // " + count + ")");
043    double[] value = (double[]) val;
044    if (value == null) {
045    } else if (mod_index == 0) {
046      return add_unmodified(value, count);
047    } else {
048      return add_modified(value, count);
049    }
050    return InvariantStatus.NO_CHANGE;
051  }
052
053  @Override
054  public InvariantStatus check(@Interned Object val, int mod_index, int count) {
055    assert !falsified;
056    assert (mod_index >= 0) && (mod_index < 2);
057    assert Intern.isInterned(val);
058    double[] value = (double[]) val;
059    if (value == null) {
060    } else if (mod_index == 0) {
061      return check_unmodified(value, count);
062    } else {
063      return check_modified(value, count);
064    }
065    return InvariantStatus.NO_CHANGE;
066  }
067
068  /**
069   * Similar to {@link #check_modified} except that it can change the state of the invariant if
070   * necessary. If the invariant doesn't have any state, then the implementation should simply call
071   * {@link #check_modified}. This method need not check for falsification; that is done by the
072   * caller.
073   */
074  public abstract InvariantStatus add_modified(double @Interned [] value, int count);
075
076  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
077  public InvariantStatus add_unmodified(double @Interned [] value, int count) {
078    return InvariantStatus.NO_CHANGE;
079  }
080
081  /**
082   * Presents a sample to the invariant. Returns whether the sample is consistent with the
083   * invariant. Does not change the state of the invariant.
084   *
085   * @param count how many identical samples were observed in a row. For example, three calls to
086   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
087   *     a count parameter of 3.
088   * @return whether or not the sample is consistent with the invariant
089   */
090  public abstract InvariantStatus check_modified(double @Interned [] value, int count);
091
092  public InvariantStatus check_unmodified(double @Interned [] value, int count) {
093    return InvariantStatus.NO_CHANGE;
094  }
095}