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  public @Nullable DiscardInfo isObviousImplied() {
062    return null;
063  }
064
065  @Pure
066  @Override
067  public boolean isSameInvariant(Invariant other) {
068    if (!getClass().equals(other.getClass())) {
069      return false;
070    }
071
072    Joiner otherAsJoiner = (Joiner) other;
073
074    if (left == otherAsJoiner.left && right == otherAsJoiner.right) {
075      return true;
076    }
077
078    return left.isSameInvariant(otherAsJoiner.left) && right.isSameInvariant(otherAsJoiner.right);
079  }
080
081  @Pure
082  @Override
083  public boolean isSameFormula(Invariant other) {
084    if (!getClass().equals(other.getClass())) {
085      return false;
086    }
087    Joiner other_joiner = (Joiner) other;
088    // Guards are necessary because the contract of isSameFormula states
089    // that the argument is of the same class as the receiver.
090    // Also use isSameInvariant because the joined parts might be over
091    // distinct slices; don't make "a=b => c=d" be isSameFormula as
092    // "e=f => g=h".
093    return ((left.getClass() == other_joiner.left.getClass())
094        // && left.isSameFormula(other_joiner.left)
095        && left.isSameInvariant(other_joiner.left)
096        && (right.getClass() == other_joiner.right.getClass())
097        // && right.isSameFormula(other_joiner.right)
098        && right.isSameInvariant(other_joiner.right));
099  }
100}