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}