001package daikon.diff;
002
003import daikon.PptTopLevel;
004import daikon.inv.Invariant;
005import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
006import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
007import org.checkerframework.checker.nullness.qual.Nullable;
008import org.checkerframework.checker.nullness.qual.RequiresNonNull;
009
010/** Computes A - B, where A and B are the two sets of invariants. */
011public class MinusVisitor extends DepthFirstVisitor {
012
013  private InvMap result = new InvMap();
014  private @MonotonicNonNull PptTopLevel currentPpt;
015
016  /** If the first ppt is non-null, it should be part of the result. */
017  @Override
018  public void visit(PptNode node) {
019    PptTopLevel ppt1 = node.getPpt1();
020    if (ppt1 != null) {
021      result.addPpt(ppt1);
022      currentPpt = ppt1;
023      super.visit(node);
024    }
025  }
026
027  /** Possibly add the first invariant to the result set. */
028  @Override
029  @SuppressWarnings(
030      "nullness:contracts.precondition.override" // visitor invariant, because the PptNode has
031  // already been visited
032  )
033  @RequiresNonNull("currentPpt")
034  public void visit(InvNode node) {
035    Invariant inv1 = node.getInv1();
036    Invariant inv2 = node.getInv2();
037    if (shouldAdd(inv1, inv2)) {
038      result.add(currentPpt, inv1);
039    }
040  }
041
042  /**
043   * If the first invariant is non-null and justified, and the second one is null or unjustified,
044   * the first invariant should be added.
045   */
046  @EnsuresNonNullIf(result = true, expression = "#1")
047  private static boolean shouldAdd(@Nullable Invariant inv1, @Nullable Invariant inv2) {
048    return (inv1 != null) && (inv2 == null);
049  }
050
051  /** Returns the InvMap generated as a result of the traversal. */
052  public InvMap getResult() {
053    return result;
054  }
055}