001package daikon.diff;
002
003import daikon.PptTopLevel;
004import daikon.inv.Invariant;
005import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
006import org.checkerframework.checker.nullness.qual.NonNull;
007import org.checkerframework.checker.nullness.qual.RequiresNonNull;
008
009/** Computes A union B, where A and B are the two sets of invariants. */
010public class UnionVisitor extends DepthFirstVisitor {
011
012  private InvMap result = new InvMap();
013  private @MonotonicNonNull PptTopLevel currentPpt;
014
015  public InvMap getResult() {
016    return result;
017  }
018
019  /** Every node has at least one non-null ppt. Add one of the non-null ppt to the result. */
020  @Override
021  public void visit(PptNode node) {
022    PptTopLevel ppt1 = node.getPpt1();
023    PptTopLevel ppt2 = node.getPpt2();
024    @SuppressWarnings(
025        "nullness") // application invariant: at least one of ppt1 and ppt2 is non-null
026    @NonNull PptTopLevel pptNonNull = (ppt1 != null ? ppt1 : ppt2);
027    result.addPpt(pptNonNull);
028    currentPpt = pptNonNull;
029    super.visit(node);
030  }
031
032  /**
033   * If only one invariant is non-null, always add it. If two invariants are non-null, add the
034   * invariant with the better (higher) confidence.
035   */
036  @Override
037  @SuppressWarnings(
038      "nullness:contracts.precondition.override" // visitor invariant, because the PptNode has
039  // already been visited
040  )
041  @RequiresNonNull("currentPpt")
042  // visitor invariant
043  public void visit(InvNode node) {
044    Invariant inv1 = node.getInv1();
045    Invariant inv2 = node.getInv2();
046    if (inv1 == null) {
047      assert inv2 != null : "@AssumeAssertion(nullness): at least one of inv1 and inv2 is non-null";
048      result.add(currentPpt, inv2);
049    } else if (inv2 == null) {
050      result.add(currentPpt, inv1);
051    } else {
052      if (inv1.getConfidence() >= inv2.getConfidence()) {
053        result.add(currentPpt, inv1);
054      } else {
055        result.add(currentPpt, inv2);
056      }
057    }
058  }
059}