001package daikon.inv.filter;
002
003import daikon.inv.DiscardInfo;
004import daikon.inv.Invariant;
005import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
006
007public class ObviousFilter extends InvariantFilter {
008  @Override
009  public String getDescription() {
010    return "Suppress obvious invariants";
011  }
012
013  /** Boolean. If true, ObviousFilter is initially turned on. */
014  public static boolean dkconfig_enabled = true;
015
016  public ObviousFilter() {
017    isOn = dkconfig_enabled;
018  }
019
020  @Override
021  @SuppressWarnings("nullness") // condition hidden in local variable
022  @EnsuresNonNullIf(result = true, expression = "#1.isObvious()")
023  boolean shouldDiscardInvariant(Invariant invariant) {
024    // if ((invariant.ppt.arity() == 1) || invariant.isEqualityComparison()) {
025    DiscardInfo discard = invariant.isObvious();
026    if (discard != null) {
027      invariant.log("discard because %s", discard.discardString());
028    }
029    return (discard != null);
030    /* } else {
031    // if y cmp f(x_0,x_1, ..., x_n) and x_n is a constant, then we can
032    // write y cmp f'(x_0,x_1,...,x_n-1), so we loop through the var_infos
033    // array of invariant and return true if any var is constant since an implying
034    // invariant should appear with some function over fewer variables.
035    for (int i = 0; i < invariant.ppt.var_infos.length; i++) {
036      VarInfo var = invariant.ppt.var_infos[i];
037      PptSlice slice = invariant.ppt.parent.findSlice(var);
038      if (slice != null) {
039        Invariant oo = null;
040        int num_elts = -1;
041        if (var.type.isIntegral()) {
042          oo = OneOfScalar.find(slice);
043          if (oo != null) {
044            num_elts = ((OneOfScalar) oo).num_elts();
045            }
046        } else if (var.type.isFloat()) {
047          oo = OneOfFloat.find(slice);
048          if (oo != null) {
049            num_elts = ((OneOfFloat) oo).num_elts();
050            }
051        } else if (var.type.baseIsIntegral()) {
052          oo = EltOneOf.find(slice);
053          if (oo != null) {
054            num_elts = ((EltOneOf) oo).num_elts();
055            }
056        } else if (var.type.baseIsFloat()) {
057            oo = EltOneOfFloat.find(slice);
058            if (oo != null) {
059              num_elts = ((EltOneOfFloat) oo).num_elts();
060              }
061        }
062        if ((oo != null) && (num_elts == 1)) {
063          invariant.discardCode = DiscardCode.obvious;
064          invariant.discardString = "Variable " + var.name.name() + "is a constant";
065          return true;
066        }
067      }
068    }
069    return invariant.isObvious();
070    }*/
071  }
072}