001  // #define PAIRWISEINTEQUAL PairwiseStringEqual
002
003// ***** This file is automatically generated from SeqComparison.java.jpp
004
005package daikon.inv.binary.twoSequence;
006
007import daikon.*;
008import daikon.Quantify.QuantFlags;
009import daikon.derive.binary.*;
010import daikon.inv.*;
011import daikon.suppress.*;
012import java.util.*;
013import java.util.logging.Logger;
014import org.checkerframework.checker.interning.qual.Interned;
015import org.checkerframework.checker.lock.qual.GuardSatisfied;
016import org.checkerframework.checker.nullness.qual.Nullable;
017import org.checkerframework.dataflow.qual.Pure;
018import org.checkerframework.dataflow.qual.SideEffectFree;
019import org.plumelib.util.ArraysPlume;
020import org.plumelib.util.Intern;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Represents invariants between two sequences of String values. If order matters for each
026 * variable (which it does by default), then the sequences are compared lexically. Prints as
027 * {@code x[] == y[] lexically}.
028 *
029
030 * <p>If order doesn't matter for each variable, then the sequences are compared to see if they are
031 * set equivalent. Prints as {@code x[] == y[]}.
032 *
033
034 * <p>If the auxiliary information (e.g., order matters) doesn't match between two variables, then
035 * this invariant cannot apply to those variables.
036 */
037public class SeqSeqStringEqual extends TwoSequenceString
038
039  implements EqualityComparison
040
041{
042  static final long serialVersionUID = 20030822L;
043
044  // Variables starting with dkconfig_ should only be set via the
045  // daikon.config.Configuration interface.
046  /** Boolean. True iff SeqSeqStringEqual invariants should be considered. */
047  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
048
049  /** Debugging logger. */
050  static final Logger debug = Logger.getLogger("daikon.inv.binary.twoSequence.SeqSeqStringEqual");
051
052  static Comparator<String[]> comparator = ArraysPlume.StringArrayComparatorLexical.it;
053
054  boolean orderMatters;
055
056  protected SeqSeqStringEqual(PptSlice ppt, boolean orderMatters) {
057    super(ppt);
058    this.orderMatters = orderMatters;
059  }
060
061  protected @Prototype SeqSeqStringEqual(boolean orderMatters) {
062    super();
063    this.orderMatters = orderMatters;
064  }
065
066  private static @Prototype SeqSeqStringEqual proto = new @Prototype SeqSeqStringEqual(true);
067
068  /** Returns the prototype invariant for SeqSeqStringEqual */
069  public static @Prototype SeqSeqStringEqual get_proto() {
070    return proto;
071  }
072
073  @Override
074  public boolean enabled() {
075    return dkconfig_enabled;
076  }
077
078  @Override
079  public boolean instantiate_ok(VarInfo[] vis) {
080
081    if (!valid_types(vis)) {
082      return false;
083    }
084
085    return true;
086  }
087
088  @Override
089  protected SeqSeqStringEqual instantiate_dyn(@Prototype SeqSeqStringEqual this, PptSlice slice) {
090    boolean has_order = slice.var_infos[0].aux.hasOrder() && slice.var_infos[1].aux.hasOrder();
091    return new SeqSeqStringEqual(slice, has_order);
092  }
093
094  @Override
095  protected Invariant resurrect_done_swapped() {
096
097    return this;
098  }
099
100  @Override
101  public String repr(@GuardSatisfied SeqSeqStringEqual this) {
102    return "SeqSeqStringEqual" + varNames() + ": ,orderMatters=" + orderMatters
103      + ",enoughSamples=" + enoughSamples()
104      ;
105  }
106
107  @SideEffectFree
108  @Override
109  public String format_using(@GuardSatisfied SeqSeqStringEqual this, OutputFormat format) {
110    // System.out.println("Calling SeqSeqStringEqual.format for: " + repr());
111
112    if (format == OutputFormat.SIMPLIFY) {
113      return format_simplify();
114    }
115
116    if (format == OutputFormat.DAIKON) {
117      String name1 = var1().name_using(format);
118      String name2 = var2().name_using(format);
119
120      return name1 + " == " + name2;
121    }
122
123    if (format == OutputFormat.CSHARPCONTRACT) {
124
125      String[] split1 = var1().csharp_array_split();
126      String[] split2 = var2().csharp_array_split();
127      // Pairwise equal.
128      return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + ".Equals(" + split2[0] + "[i]" + split2[1] + "))";
129    }
130
131    if (format.isJavaFamily()) {
132      String name1 = var1().name_using(format);
133      String name2 = var2().name_using(format);
134
135      return "daikon.Quant.pairwiseEqual(" + name1 + ", " + name2 + ")";
136    }
137
138    return format_unimplemented(format);
139  }
140
141  public String format_simplify(@GuardSatisfied SeqSeqStringEqual this) {
142    if (Invariant.dkconfig_simplify_define_predicates) {
143      return format_simplify_defined();
144    } else {
145      return format_simplify_explicit();
146    }
147  }
148
149  private String format_simplify_defined(@GuardSatisfied SeqSeqStringEqual this) {
150    String[] var1_name = var1().simplifyNameAndBounds();
151    String[] var2_name = var2().simplifyNameAndBounds();
152    if (var1_name == null || var2_name == null) {
153      return String.format("%s.format_simplify_defined(%s): var1_name=%s, var2_name=%s, for %s",
154                           getClass().getSimpleName(), this,
155                           Arrays.toString(var1_name), Arrays.toString(var2_name), format());
156    }
157    return "(|lexical-==| "
158      + var1_name[0] + " " + var1_name[1] + " " + var1_name[2] + " "
159      + var2_name[0] + " " + var2_name[1] + " " + var2_name[2] + ")";
160  }
161
162  private String format_simplify_explicit(@GuardSatisfied SeqSeqStringEqual this) {
163
164      // A simple case: if two sequences are lexically equal iff they
165      // are elementwise equal.
166      String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(),
167                                                 var1(), var2());
168      return form[0]
169        + "(EQ " + form[1] + " " + form[2] + ")" + form[3];
170
171  }
172
173  @Override
174  public InvariantStatus check_modified(
175      String @Interned [] v1, String @Interned [] v2, int count) {
176    /// This does not do the right thing; I really want to avoid comparisons
177    /// if one is missing, but not if one is zero-length.
178    // // Don't make comparisons with empty arrays.
179    // if ((v1.length == 0) || (v2.length == 0)) {
180    //   return;
181    // }
182
183    int comparison = 0;
184    if (orderMatters) {
185      // Standard element wise comparison
186       comparison = comparator.compare(v1, v2);
187    } else {
188      // Do a double subset comparison
189      comparison = (ArraysPlume.isSubset(v1, v2) && ArraysPlume.isSubset( v2, v1)) ? 0 : -1;
190    }
191
192    if (!(comparison == 0) ) {
193      return InvariantStatus.FALSIFIED;
194    }
195    return InvariantStatus.NO_CHANGE;
196  }
197
198  @Override
199  public InvariantStatus add_modified(String @Interned [] v1, String @Interned [] v2, int count) {
200    if (logDetail()) {
201      log("add_modified (%s, %s)", Arrays.toString(v1), Arrays.toString(v2));
202    }
203        return check_modified(v1, v2, count);
204  }
205
206  @Override
207  protected double computeConfidence() {
208
209    // It's an equality invariant
210    if (ppt.num_samples() == 0) {
211      return Invariant.CONFIDENCE_UNJUSTIFIED;
212    } else {
213      return Invariant.CONFIDENCE_JUSTIFIED;
214    }
215
216  }
217
218  // For Comparison interface
219  @Override
220  public double eq_confidence() {
221      return getConfidence();
222  }
223
224  @Pure
225  @Override
226  public boolean isSameFormula(Invariant o) {
227    return true;
228  }
229
230  @Pure
231  @Override
232  public boolean isExclusiveFormula(Invariant o) {
233    return false;
234  }
235
236  /**
237   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
238   * avoid circular isObvious relations.
239   */
240  @Pure
241  @Override
242  public @Nullable DiscardInfo isObviousStatically_SomeInEquality() {
243    if (var1().equalitySet == var2().equalitySet) {
244      return isObviousStatically(this.ppt.var_infos);
245    } else {
246      return super.isObviousStatically_SomeInEquality();
247    }
248  }
249
250  /**
251   * Since this invariant can be a postProcessed equality, we have to handle isObvious especially to
252   * avoid circular isObvious relations.
253   */
254  @Pure
255  @Override
256  public @Nullable DiscardInfo isObviousDynamically_SomeInEquality() {
257    if (logOn()) {
258      log("Considering dynamically_someInEquality");
259    }
260    if (var1().equalitySet == var2().equalitySet) {
261      return isObviousDynamically(this.ppt.var_infos);
262    } else {
263      return super.isObviousDynamically_SomeInEquality();
264    }
265  }
266
267  @Pure
268  @Override
269  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
270
271    return super.isObviousStatically(vis);
272  }
273
274  @Pure
275  @Override
276  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
277    DiscardInfo super_result = super.isObviousDynamically(vis);
278    if (super_result != null) {
279      return super_result;
280    }
281    assert ppt != null;
282
283    return null;
284  }
285
286  @Override
287  public void repCheck() {
288    super.repCheck();
289    /*
290      This code is no longer needed now that the can_be_x's are gone
291    if (!(this.can_be_eq || this.can_be_lt || this.can_be_gt)
292        && ppt.num_samples() != 0) {
293      System.err.println(this.repr());
294      System.err.println(this.ppt.num_samples());
295      throw new Error();
296    }
297    */
298  }
299
300  @Pure
301  public boolean isEqual() {
302
303    return true;
304  }
305
306  // Look up a previously instantiated invariant.
307  public static @Nullable SeqSeqStringEqual find(PptSlice ppt) {
308    assert ppt.arity() == 2;
309    for (Invariant inv : ppt.invs) {
310      if (inv instanceof SeqSeqStringEqual) {
311        return (SeqSeqStringEqual) inv;
312      }
313    }
314    return null;
315  }
316
317  /** Returns a list of non-instantiating suppressions for this invariant. */
318  @Pure
319  @Override
320  public @Nullable NISuppressionSet get_ni_suppressions() {
321    return suppressions;
322  }
323
324    private static @Nullable NISuppressionSet suppressions = null;
325
326  @Override
327  public @Nullable @NonPrototype SeqSeqStringEqual merge(
328      @Prototype SeqSeqStringEqual this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
329    // Ignore the orderMatters field, because it is always the same (and is always true).
330    return (SeqSeqStringEqual) super.merge(invs, parent_ppt);
331  }
332}