001package daikon.inv;
002
003import daikon.PptSlice;
004import daikon.PptSlice0;
005import daikon.PptTopLevel;
006import org.checkerframework.checker.lock.qual.GuardSatisfied;
007import org.checkerframework.checker.nullness.qual.Nullable;
008import org.checkerframework.dataflow.qual.Pure;
009import org.checkerframework.dataflow.qual.SideEffectFree;
010
011public abstract class Joiner extends Invariant {
012
013  static final long serialVersionUID = 20030822L;
014
015  public Invariant left;
016  public Invariant right;
017
018  protected Joiner(PptSlice ppt) {
019    super(ppt);
020    throw new Error("Don't instantiate a Joiner this way.");
021  }
022
023  Joiner(PptSlice ppt, Invariant left, Invariant right) {
024    super(ppt);
025    assert ppt instanceof PptSlice0;
026
027    this.left = left;
028    this.right = right;
029  }
030
031  protected Joiner(PptTopLevel ppt, Invariant left, Invariant right) {
032    // Need a duplicate check
033
034    this(ppt.joiner_view, left, right);
035  }
036
037  @Override
038  public abstract String repr(@GuardSatisfied Joiner this);
039
040  // I think we don't resurrect joiners
041  @Override
042  protected Invariant resurrect_done(int[] permutation) {
043    throw new UnsupportedOperationException();
044  }
045
046  @SideEffectFree
047  @Override
048  public abstract String format_using(@GuardSatisfied Joiner this, OutputFormat format);
049
050  @Pure
051  @Override
052  public boolean isValidEscExpression() {
053    return left.isValidEscExpression() && right.isValidEscExpression();
054  }
055
056  @Pure
057  public boolean isObviousDerived() {
058    return false;
059  }
060
061  /**
062   * DiscardInfo is not used for this invariant
063   *
064   * @return null
065   */
066  @Pure
067  public @Nullable DiscardInfo isObviousImplied() {
068    return null;
069  }
070
071  @Pure
072  @Override
073  public boolean isSameInvariant(Invariant other) {
074    if (!getClass().equals(other.getClass())) {
075      return false;
076    }
077
078    Joiner otherAsJoiner = (Joiner) other;
079
080    if (left == otherAsJoiner.left && right == otherAsJoiner.right) {
081      return true;
082    }
083
084    return left.isSameInvariant(otherAsJoiner.left) && right.isSameInvariant(otherAsJoiner.right);
085  }
086
087  @Pure
088  @Override
089  public boolean isSameFormula(Invariant other) {
090    if (!getClass().equals(other.getClass())) {
091      return false;
092    }
093    Joiner other_joiner = (Joiner) other;
094    // Guards are necessary because the contract of isSameFormula states
095    // that the argument is of the same class as the receiver.
096    // Also use isSameInvariant because the joined parts might be over
097    // distinct slices; don't make "a=b => c=d" be isSameFormula as
098    // "e=f => g=h".
099    return ((left.getClass() == other_joiner.left.getClass())
100        // && left.isSameFormula(other_joiner.left)
101        && left.isSameInvariant(other_joiner.left)
102        && (right.getClass() == other_joiner.right.getClass())
103        // && right.isSameFormula(other_joiner.right)
104        && right.isSameInvariant(other_joiner.right));
105  }
106}