001// ***** This file is automatically generated from SequenceInitialFactory.java.jpp
002
003package daikon.derive.unary;
004
005import org.checkerframework.checker.nullness.qual.Nullable;
006import daikon.*;
007import java.util.logging.Logger;
008
009public final class SequenceInitialFactoryFloat extends UnaryDerivationFactory {
010
011  public static final Logger debug =
012    Logger.getLogger("daikon.derive.binary.SequenceInitialFactory");
013
014  @Override
015  public UnaryDerivation @Nullable [] instantiate(VarInfo vi) {
016    // System.out.println("SequenceInitialFactory.instantiate(" + vi + ")");
017    // return (UnaryDerivation)new SequenceFirst(vi);
018
019    if (!SequenceInitialFloat.dkconfig_enabled) {
020      return null;
021    }
022
023    if (vi.rep_type != ProglangType.DOUBLE_ARRAY) {
024      return null;
025    }
026
027    // System.out.println("SequenceInitial.applicable(" + vi.name + ") = "
028    //                    + SequenceInitial.applicable(vi));
029
030    if (!SequenceInitialFloat.applicable(vi)) {
031      Global.tautological_suppressed_derived_variables += 4;
032      return null;
033    }
034
035    // by default, we use the indices 0, 1, -1, -2.
036    int lowerbound = -2;
037    int upperbound = 1;
038
039    boolean suppress_zero = false;
040    // We know that var.~ll~[0] == var and var.~ll~.field[0] == var.field.
041    if (vi.isClosure()) {
042      suppress_zero = true;
043      if ((lowerbound == 0) && (upperbound == 0)) {
044        Global.tautological_suppressed_derived_variables += 4;
045      }
046        return null;
047    }
048
049    int num_invs = upperbound - lowerbound + 1 - (suppress_zero ? 1 : 0);
050    assert num_invs > 0
051        : "No SequenceInitial invariants to instantiate; lowerbound="
052            + lowerbound
053            + ", upperbound="
054            + upperbound
055            + ", suppress_zero="
056            + suppress_zero;
057    UnaryDerivation[] result = new UnaryDerivation[num_invs];
058    int j = 0;
059    for (int i = lowerbound; i <= upperbound; i++) {
060      if (!((i == 0) && suppress_zero)) {
061        result[j] = new SequenceInitialFloat(vi, i);
062        j++;
063      }
064    }
065    // No longer needed (I hope!).
066    // assert j == num_invs
067    //                   : "SequenceInitial(" + vi.name + "): "
068    //                   + "j=" + j + ", num_invs=" + num_invs
069    //                   + ",lowerbound=" + lowerbound
070    //                   + ", upperbound=" + upperbound
071    //                   + ", suppress_zero=" + suppress_zero;
072
073    Global.tautological_suppressed_derived_variables += 4 - num_invs;
074
075    return result;
076  }
077}