001// ***** This file is automatically generated from ThreeScalar.java.jpp
002package daikon.inv.ternary.threeScalar;
003
004import daikon.*;
005import daikon.inv.*;
006import daikon.inv.ternary.TernaryInvariant;
007import org.checkerframework.checker.interning.qual.Interned;
008import org.checkerframework.checker.lock.qual.GuardSatisfied;
009import org.plumelib.util.Intern;
010import typequals.prototype.qual.NonPrototype;
011import typequals.prototype.qual.Prototype;
012
013/**
014 * Abstract base class for invariants over three numeric variables. An example is {@code z = ax + by
015 * + c}.
016 */
017public abstract class ThreeFloat extends TernaryInvariant {
018  static final long serialVersionUID = 20020122L;
019
020  protected ThreeFloat(PptSlice ppt) {
021    super(ppt);
022  }
023
024  protected @Prototype ThreeFloat() {
025    super();
026  }
027
028  @Override
029  public final boolean valid_types(VarInfo[] vis) {
030
031    return ((vis.length == 3)
032            && vis[0].file_rep_type.isFloat()
033            && vis[1].file_rep_type.isFloat()
034            && vis[2].file_rep_type.isFloat());
035  }
036
037  public VarInfo var1(@GuardSatisfied ThreeFloat this) {
038    return ppt.var_infos[0];
039  }
040
041  public VarInfo var2(@GuardSatisfied ThreeFloat this) {
042    return ppt.var_infos[1];
043  }
044
045  public VarInfo var3(@GuardSatisfied ThreeFloat this) {
046    return ppt.var_infos[2];
047  }
048
049  @Override
050  public InvariantStatus check(@Interned Object val1, @Interned Object val2, @Interned Object val3, int mod_index, int count) {
051    // Tests for whether a value is missing should be performed before
052    // making this call, so as to reduce overall work.
053    assert ! falsified;
054    if ((mod_index < 0) || (mod_index > 8)) {
055      assert (mod_index >= 0) && (mod_index < 8)
056        : "var 1 " + ppt.var_infos[0].name() + " value = "
057         + val1 + "mod_index = " +  mod_index;
058    }
059    double v1 = ((Double) val1).doubleValue();
060    double v2 = ((Double) val2).doubleValue();
061    if (!(val3 instanceof Double)) {
062      System.out.println("val3 should be PRIMITIVE, but is " + val3.getClass());
063    }
064    double v3 = ((Double) val3).doubleValue();
065    if (mod_index == 0) {
066      return check_unmodified(v1, v2, v3, count);
067    } else {
068      return check_modified(v1, v2, v3, count);
069    }
070  }
071
072  @Override
073  public InvariantStatus add(@Interned Object val1, @Interned Object val2, @Interned Object val3, int mod_index, int count) {
074    // Tests for whether a value is missing should be performed before
075    // making this call, so as to reduce overall work.
076    assert ! falsified;
077    if ((mod_index < 0) || (mod_index > 8)) {
078      assert (mod_index >= 0) && (mod_index < 8)
079        : "var 1 " + ppt.var_infos[0].name() + " value = "
080         + val1 + "mod_index = " +  mod_index + " line "
081         + FileIO.get_linenum();
082    }
083    double v1 = ((Double) val1).doubleValue();
084    double v2 = ((Double) val2).doubleValue();
085    if (!(val3 instanceof Double)) {
086      System.out.printf("val3 should be PRIMITIVE, but is %s=%s, v2 is %s=%s%n",
087              val3.getClass().getName(), Debug.toString(val3),
088              val2.getClass().getName(), Debug.toString(val2));
089      System.out.println("our class = " + this.getClass().getName());
090      System.out.println("our slice = " + this.ppt);
091      PptSlice slice = this.ppt;
092      System.out.printf("var3 reptype = %s%n", slice.var_infos[2].rep_type);
093      assert (slice.var_infos[0].rep_type == ProglangType.INT)
094                  && (slice.var_infos[1].rep_type == ProglangType.INT)
095                  && (slice.var_infos[2].rep_type == ProglangType.INT);
096    }
097    double v3 = ((Double) val3).doubleValue();
098    if (mod_index == 0) {
099      return add_unmodified(v1, v2, v3, count);
100    } else {
101      return add_modified(v1, v2, v3, count);
102    }
103  }
104
105  /**
106   * Presents a sample to the invariant. Returns whether the sample is consistent with the
107   * invariant. Does not change the state of the invariant.
108   *
109   * @param count how many identical samples were observed in a row. For example, three calls to
110   * check_modified with a count parameter of 1 is equivalent to one call to check_modified with a
111   * count parameter of 3.
112   * @return whether or not the sample is consistent with the invariant
113   */
114  public abstract InvariantStatus check_modified(double v1, double v2, double v3, int count);
115
116  public InvariantStatus check_unmodified(double v1, double v2, double v3, int count) {
117    return InvariantStatus.NO_CHANGE;
118  }
119
120  /**
121   * Similar to {@link #check_modified} except that it can change the state of the invariant if
122   * necessary. If the invariant doesn't have any state, then the implementation should simply call
123   * {@link #check_modified}. This method need not check for falsification; that is done by the
124   * caller.
125   */
126  public abstract InvariantStatus add_modified(double v1, double v2, double v3, int count);
127
128  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
129  public InvariantStatus add_unmodified(double v1, double v2, double v3, int count) {
130    return InvariantStatus.NO_CHANGE;
131  }
132}