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