001package daikon.diff;
002
003import daikon.inv.Invariant;
004import java.io.PrintStream;
005import java.util.logging.Level;
006import java.util.logging.Logger;
007import org.checkerframework.checker.nullness.qual.Nullable;
008
009/** Prints the differing invariant pairs. */
010public class PrintDifferingInvariantsVisitor extends PrintAllVisitor {
011
012  /** Logger for debugging information. */
013  public static final Logger debug = Logger.getLogger("daikon.diff.DetailedStatisticsVisitor");
014
015  /** Create an instance of PrintDifferingInvariantsVisitor. */
016  public PrintDifferingInvariantsVisitor(PrintStream ps, boolean verbose, boolean printEmptyPpts) {
017    super(ps, verbose, printEmptyPpts);
018  }
019
020  @Override
021  public void visit(InvNode node) {
022    Invariant inv1 = node.getInv1();
023    Invariant inv2 = node.getInv2();
024    if (shouldPrint(inv1, inv2)) {
025      super.visit(node);
026    }
027  }
028
029  /**
030   * Returns true if the pair of invariants should be printed, depending on their type,
031   * relationship, and printability.
032   */
033  protected boolean shouldPrint(@Nullable Invariant inv1, @Nullable Invariant inv2) {
034    int rel = DetailedStatisticsVisitor.determineRelationship(inv1, inv2);
035    if (rel == DetailedStatisticsVisitor.REL_SAME_JUST1_JUST2
036        || rel == DetailedStatisticsVisitor.REL_SAME_UNJUST1_UNJUST2
037        || rel == DetailedStatisticsVisitor.REL_DIFF_UNJUST1_UNJUST2
038        || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST1
039        || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST2) {
040      if (debug.isLoggable(Level.FINE)) {
041        debug.fine(" Returning false");
042      }
043
044      return false;
045    }
046
047    if ((inv1 == null || !inv1.isWorthPrinting()) && (inv2 == null || !inv2.isWorthPrinting())) {
048      if (debug.isLoggable(Level.FINE)) {
049        debug.fine(" Returning false");
050      }
051      return false;
052    }
053
054    if (debug.isLoggable(Level.FINE)) {
055      debug.fine(" Returning true");
056    }
057
058    return true;
059  }
060}