001package daikon.inv;
002
003import daikon.PptSlice;
004import daikon.PptTopLevel;
005import org.checkerframework.checker.lock.qual.GuardSatisfied;
006import org.checkerframework.dataflow.qual.Pure;
007
008/**
009 * This is a special implication invariant that guards any invariants that are over variables that
010 * are sometimes missing. For example, if the invariant {@code a.x = 0} is true, the guarded
011 * implication is {@code a != null => a.x = 0}.
012 */
013public class GuardingImplication extends Implication {
014  static final long serialVersionUID = 20020725L;
015
016  private GuardingImplication(
017      PptSlice ppt, Invariant predicate, Invariant consequent, boolean iff) {
018    super(ppt, predicate, consequent, iff, predicate, consequent);
019  }
020
021  // Do not call this!  The only location these should be created is in
022  // Invariant.createGuardedInvariant().  (I need to find a way to enforce this.)
023  // A GuardingImplication is never installed in a PptMap -- it's only
024  // printed by using format_using.
025  public static GuardingImplication makeGuardingImplication(
026      PptTopLevel ppt, Invariant predicate, Invariant consequent, boolean iff) {
027    assert predicate != null;
028    assert consequent != null;
029
030    // No duplicate check because the way it is set up no duplicates should
031    // occur:  No invariants are duplicates, and since each guarding
032    // implication is based off of an existing invariant in a PptSlice, we
033    // are guarenteed no duplicate guarding implications exist.
034
035    GuardingImplication result =
036        new GuardingImplication(ppt.joiner_view, predicate, consequent, iff);
037    return result;
038  }
039
040  @Pure
041  @Override
042  public boolean isWorthPrinting() {
043    return right.isWorthPrinting();
044    // return !right.isObvious();
045  }
046
047  @Override
048  public boolean enoughSamples(@GuardSatisfied GuardingImplication this) {
049    return right.enoughSamples();
050  }
051
052  @Override
053  public double computeConfidence() {
054    return right.computeConfidence();
055  }
056}