001package daikon.diff;
002
003import daikon.inv.Implication;
004import daikon.inv.Invariant;
005import java.util.Comparator;
006import org.checkerframework.dataflow.qual.Pure;
007
008/**
009 * Comparator for sorting invariants. If an invariant is an implication, its consequent is used
010 * instead of the whole invariant. If the consequents of two invariants are equal, the predicates
011 * are compared. The predicates and consequents themselves are compared using the Comparator c
012 * passed to the constructor. Some examples:
013 *
014 * <pre>
015 * this.compare(A&rArr;B, A&rArr;C) == c.compare(B, C)
016 * this.compare(B, A&rArr;C) == c.compare(B, C)
017 * this.compare(B, C) == c.compare(B, C)
018 * this.compare(A&rArr;C, B&rArr;C) == c.compare(A, B)
019 * </pre>
020 */
021public class ConsequentSortComparator implements Comparator<Invariant> {
022
023  private Comparator<Invariant> c;
024
025  public ConsequentSortComparator(Comparator<Invariant> c) {
026    this.c = c;
027  }
028
029  @Pure
030  @Override
031  public int compare(Invariant inv1, Invariant inv2) {
032    Implication imp1 = null;
033    Implication imp2 = null;
034    if (inv1 instanceof Implication) {
035      imp1 = (Implication) inv1;
036      inv1 = imp1.consequent();
037    }
038    if (inv2 instanceof Implication) {
039      imp2 = (Implication) inv2;
040      inv2 = imp2.consequent();
041    }
042
043    int result = c.compare(inv1, inv2);
044
045    if (result == 0 && imp1 != null && imp2 != null) {
046      return c.compare(imp1.predicate(), imp2.predicate());
047    } else {
048      return result;
049    }
050  }
051}