001package daikon.diff;
002
003import daikon.PptConditional;
004import daikon.inv.Implication;
005import daikon.inv.Invariant;
006import java.util.ArrayList;
007import java.util.HashSet;
008import java.util.Iterator;
009import java.util.List;
010import org.checkerframework.checker.nullness.qual.Nullable;
011
012/**
013 * <B>ConsequentExtractorVisitor</B> is a visitor that takes in RootNode tree used by the other
014 * visitors in Diff and only modifies the first inv tree out of the pair of two inv trees (the
015 * second tree is never read or modified).
016 *
017 * <p>The goal is to take the right hand side of any implication and extract it for later use. The
018 * implementation completely replaces the previous inv tree with the a new inv tree. The new inv
019 * tree contains only the extracted consequents of the original inv tree.
020 */
021public class ConsequentExtractorVisitor extends DepthFirstVisitor {
022
023  private int nonce;
024
025  // Gets rid of repeated reports
026  private HashSet<String> repeatFilter = new HashSet<>();
027
028  // Accumulation of extracted consequents
029  private List<Invariant> accum = new ArrayList<>();
030
031  public ConsequentExtractorVisitor() {
032    nonce = 0;
033  }
034
035  @Override
036  public void visit(PptNode node) {
037    assert node.getPpt1() != null
038        : "@AssumeAssertion(nullness): method precondition: has a (non-null) consequent";
039    if (node.getPpt1() instanceof PptConditional) {
040      return;
041    }
042    System.out.println(node.getPpt1().name);
043    repeatFilter.clear();
044    accum.clear();
045    super.visit(node);
046    // clear all of the old ppts
047
048    for (Iterator<InvNode> i = node.children(); i.hasNext(); ) {
049      InvNode child = i.next();
050      if (child.getInv1() != null) {
051        child.getInv1().ppt.invs.clear();
052      }
053    }
054    /*
055    for (Invariant inv : accum) {
056        inv.ppt.invs.clear();
057    }
058    */
059    // Now add back everything in accum
060    for (Invariant inv : accum) {
061      inv.ppt.addInvariant(inv);
062    }
063    System.out.println("NONCE: " + nonce);
064  }
065
066  /**
067   * The idea is to check if the node is an Implication Invariant. If not, immediately remove the
068   * invariant. Otherwise, extract the Consequent, remove the Implication, and then add the
069   * consequent to the list.
070   */
071  @Override
072  public void visit(InvNode node) {
073    Invariant inv1 = node.getInv1();
074    // do nothing if the invariant does not exist
075    if (inv1 != null) {
076      if (inv1.justified() && (inv1 instanceof Implication)) {
077        nonce++;
078        Implication imp = (Implication) inv1;
079        if (repeatFilter.add(imp.consequent().format())) {
080          // inv1.ppt.invs.add (imp.consequent());
081          accum.add(imp.consequent());
082        }
083        // add both sides of a biimplication
084        if (imp.iff == true) {
085          if (repeatFilter.add(imp.predicate().format())) {
086            // inv1.ppt.invs.add (imp.predicate());
087            accum.add(imp.predicate());
088          }
089        }
090      }
091      inv1.ppt.removeInvariant(inv1);
092      System.out.println(inv1.ppt.invs.size() + " " + repeatFilter.size());
093    } else {
094
095    }
096  }
097
098  /**
099   * Returns true if the pair of invariants should be printed, depending on their type,
100   * relationship, and printability.
101   */
102  protected boolean shouldPrint(@Nullable Invariant inv1, @Nullable Invariant inv2) {
103    int rel = DetailedStatisticsVisitor.determineRelationship(inv1, inv2);
104    if (rel == DetailedStatisticsVisitor.REL_SAME_JUST1_JUST2
105        || rel == DetailedStatisticsVisitor.REL_SAME_UNJUST1_UNJUST2
106        || rel == DetailedStatisticsVisitor.REL_DIFF_UNJUST1_UNJUST2
107        || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST1
108        || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST2) {
109      return false;
110    }
111
112    if ((inv1 == null || !inv1.isWorthPrinting()) && (inv2 == null || !inv2.isWorthPrinting())) {
113      return false;
114    }
115
116    return true;
117  }
118}