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  static final long serialVersionUID = 20020813L;
013
014  protected SingleFloatSequence(PptSlice ppt) {
015    super(ppt);
016  }
017
018  protected @Prototype SingleFloatSequence() {
019    super();
020  }
021
022  @Override
023  public final boolean valid_types(VarInfo[] vis) {
024    return ((vis.length == 1)
025        && vis[0].file_rep_type.baseIsFloat()
026        && vis[0].file_rep_type.isArray());
027  }
028
029  // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL.
030  // Subclasses need not override this except in special cases;
031  // just implement {@link #add_modified(Object,int)}.
032  @Override
033  public InvariantStatus add(@Interned Object val, int mod_index, int count) {
034    assert !falsified;
035    assert (mod_index >= 0) && (mod_index < 2);
036    assert Intern.isInterned(val);
037    // System.out.println("SingleFloatSequence.add(" + Arrays.toString(value) + ", " + modified + ",
038    // " + count + ")");
039    double[] value = (double[]) val;
040    if (value == null) {
041    } else if (mod_index == 0) {
042      return add_unmodified(value, count);
043    } else {
044      return add_modified(value, count);
045    }
046    return InvariantStatus.NO_CHANGE;
047  }
048
049  @Override
050  public InvariantStatus check(@Interned Object val, int mod_index, int count) {
051    assert !falsified;
052    assert (mod_index >= 0) && (mod_index < 2);
053    assert Intern.isInterned(val);
054    double[] value = (double[]) val;
055    if (value == null) {
056    } else if (mod_index == 0) {
057      return check_unmodified(value, count);
058    } else {
059      return check_modified(value, count);
060    }
061    return InvariantStatus.NO_CHANGE;
062  }
063
064  /**
065   * Similar to {@link #check_modified} except that it can change the state of the invariant if
066   * necessary. If the invariant doesn't have any state, then the implementation should simply call
067   * {@link #check_modified}. This method need not check for falsification; that is done by the
068   * caller.
069   */
070  public abstract InvariantStatus add_modified(double @Interned [] value, int count);
071
072  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
073  public InvariantStatus add_unmodified(double @Interned [] value, int count) {
074    return InvariantStatus.NO_CHANGE;
075  }
076
077  /**
078   * Presents a sample to the invariant. Returns whether the sample is consistent with the
079   * invariant. Does not change the state of the invariant.
080   *
081   * @param count how many identical samples were observed in a row. For example, three calls to
082   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
083   *     a count parameter of 3.
084   * @return whether or not the sample is consistent with the invariant
085   */
086  public abstract InvariantStatus check_modified(double @Interned [] value, int count);
087
088  public InvariantStatus check_unmodified(double @Interned [] value, int count) {
089    return InvariantStatus.NO_CHANGE;
090  }
091}