001// ***** This file is automatically generated from PairwiseLinearBinary.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.inv.*;
008import daikon.inv.DiscardCode;
009import daikon.inv.DiscardInfo;
010import daikon.inv.binary.twoScalar.*;
011import java.util.*;
012import org.checkerframework.checker.interning.qual.Interned;
013import org.checkerframework.checker.lock.qual.GuardSatisfied;
014import org.checkerframework.checker.nullness.qual.Nullable;
015import org.checkerframework.dataflow.qual.Pure;
016import org.checkerframework.dataflow.qual.SideEffectFree;
017import org.plumelib.util.Intern;
018import typequals.prototype.qual.NonPrototype;
019import typequals.prototype.qual.Prototype;
020
021/**
022 * Represents a linear invariant (i.e., {@code y = ax + b}) between the corresponding elements
023 * of two sequences of double values. Each {@code (x[i], y[i])} pair is examined. Thus,
024 * {@code x[0]} is compared to {@code y[0]}, {@code x[1]} to {@code y[1]} and so
025 * forth. Prints as {@code y[] = a * x[] + b}.
026 */
027public class PairwiseLinearBinaryFloat extends TwoSequenceFloat {
028  static final long serialVersionUID = 20030822L;
029
030  // Variables starting with dkconfig_ should only be set via the
031  // daikon.config.Configuration interface.
032  /** Boolean. True iff PairwiseLinearBinary invariants should be considered. */
033  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
034
035  public LinearBinaryCoreFloat core;
036
037  @SuppressWarnings("nullness") // circular initialization
038  protected PairwiseLinearBinaryFloat(PptSlice ppt) {
039    super(ppt);
040    core = new LinearBinaryCoreFloat(this);
041  }
042
043  @SuppressWarnings("nullness") // circular initialization
044  protected @Prototype PairwiseLinearBinaryFloat() {
045    super();
046    // Do we need a core in a prototype invariant?
047    core = new LinearBinaryCoreFloat(this);
048  }
049
050  private static @Prototype PairwiseLinearBinaryFloat proto = new @Prototype PairwiseLinearBinaryFloat();
051
052  /** Returns the prototype invariant for PairwiseLinearBinaryFloat. */
053  public static @Prototype PairwiseLinearBinaryFloat get_proto() {
054    return proto;
055  }
056
057  @Override
058  public boolean enabled() {
059    return dkconfig_enabled;
060  }
061
062  @Override
063  protected PairwiseLinearBinaryFloat instantiate_dyn(@Prototype PairwiseLinearBinaryFloat this, PptSlice slice) {
064    return new PairwiseLinearBinaryFloat(slice);
065  }
066
067  @SideEffectFree
068  @Override
069  public PairwiseLinearBinaryFloat clone(@GuardSatisfied PairwiseLinearBinaryFloat this) {
070    PairwiseLinearBinaryFloat result = (PairwiseLinearBinaryFloat) super.clone();
071    result.core = core.clone();
072    result.core.wrapper = result;
073    return result;
074  }
075
076  @Override
077  protected Invariant resurrect_done_swapped() {
078    core.swap();
079    return this;
080  }
081
082  @Override
083  public String repr(@GuardSatisfied PairwiseLinearBinaryFloat this) {
084    return "PairwiseLinearBinaryFloat" + varNames() + ": falsified=" + falsified
085      + "; " + core.repr();
086  }
087
088  @SideEffectFree
089  @Override
090  public String format_using(@GuardSatisfied PairwiseLinearBinaryFloat this, OutputFormat format) {
091    if (core.a == 0 && core.b == 0 && core.c == 0) {
092      return format_too_few_samples(format, null);
093    }
094
095    if (format == OutputFormat.DAIKON) {
096      return format_daikon();
097    }
098    // if (format == OutputFormat.JML) {
099    //   return format_jml();
100    // }
101    if (format == OutputFormat.SIMPLIFY) {
102      return format_simplify();
103    }
104    if (format == OutputFormat.CSHARPCONTRACT) {
105      return format_csharp();
106    }
107
108    return format_unimplemented(format);
109  }
110
111  public String format_daikon(@GuardSatisfied PairwiseLinearBinaryFloat this) {
112    return core.format_using(OutputFormat.DAIKON, var1().name(),
113                             var2().name());
114  }
115
116  public String format_simplify(@GuardSatisfied PairwiseLinearBinaryFloat this) {
117    String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(),
118                                               var1(), var2());
119    return form[0] + LinearBinaryCoreFloat.format_simplify(form[1], form[2],
120                                               core.a, core.b, core.c)
121      + form[3];
122  }
123
124  public String format_csharp(@GuardSatisfied PairwiseLinearBinaryFloat this) {
125
126    String[] split1 = var1().csharp_array_split();
127    String[] split2 = var2().csharp_array_split();
128
129    return "Contract.ForAll(0, " + split1[0]
130      + ".Count(), i => "
131      + core.format_using(OutputFormat.CSHARPCONTRACT, split1[0] + "[i]" + split1[1], split2[0] + "[i]" + split2[1])
132      + ")";
133  }
134
135  @Override
136  public InvariantStatus check_modified(double @Interned [] x_arr, double @Interned [] y_arr, int count) {
137    return clone().add_modified(x_arr, y_arr, count);
138  }
139
140  @Override
141  public InvariantStatus add_modified(double @Interned [] x_arr, double @Interned [] y_arr, int count) {
142    if (x_arr.length != y_arr.length) {
143      return InvariantStatus.FALSIFIED;
144    }
145    int len = x_arr.length;
146    // int len = Math.min(x_arr.length, y_arr.length);
147
148    for (int i = 0; i < len; i++) {
149      double x = x_arr[i];
150      double y = y_arr[i];
151
152      if (core.add_modified(x, y, count) == InvariantStatus.FALSIFIED) {
153        return InvariantStatus.FALSIFIED;
154      }
155    }
156    return InvariantStatus.NO_CHANGE;
157  }
158
159  @Override
160  protected double computeConfidence() {
161    return core.computeConfidence();
162  }
163
164  @Pure
165  @Override
166  public boolean isSameFormula(Invariant other) {
167    return core.isSameFormula(((PairwiseLinearBinaryFloat) other).core);
168  }
169
170  @Pure
171  @Override
172  public boolean isExclusiveFormula(Invariant other) {
173    if (other instanceof PairwiseLinearBinaryFloat) {
174      return core.isExclusiveFormula(((PairwiseLinearBinaryFloat) other).core);
175    }
176    return false;
177  }
178
179  @Pure
180  @Override
181  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
182    DiscardInfo super_result = super.isObviousDynamically(vis);
183    if (super_result != null) {
184      return super_result;
185    }
186
187    if (core.a == 0) {
188      return new DiscardInfo(this, DiscardCode.obvious, var2().name() + " is constant");
189    }
190    if (core.b == 0) {
191      return new DiscardInfo(this, DiscardCode.obvious, var1().name() + " is constant");
192    }
193//    if (core.a == 1 && core.b == 0) {
194//      return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
195//    }
196    if (core.a == -core.b && core.c == 0) {
197     return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
198    }
199    return null;
200  }
201
202  @Pure
203  @Override
204  public boolean isActive() {
205    return core.isActive();
206  }
207
208  @Override
209  public boolean mergeFormulasOk() {
210    return core.mergeFormulasOk();
211  }
212
213  /**
214   * Merge the invariants in invs to form a new invariant. Each must be a PairwiseLinearBinaryFloat invariant. The
215   * work is done by the LinearBinary core
216   *
217   * @param invs list of invariants to merge. They should all be permuted to match the variable
218   *     order in parent_ppt.
219   * @param parent_ppt slice that will contain the new invariant
220   */
221  @Override
222  public @Nullable PairwiseLinearBinaryFloat merge(List<Invariant> invs, PptSlice parent_ppt) {
223
224    // Create a matching list of cores
225    List<LinearBinaryCoreFloat> cores = new ArrayList<>();
226    for (Invariant inv : invs) {
227      cores.add(((PairwiseLinearBinaryFloat) inv).core);
228    }
229
230    // Merge the cores and build a new invariant containing the merged core
231    PairwiseLinearBinaryFloat result = new PairwiseLinearBinaryFloat(parent_ppt);
232    LinearBinaryCoreFloat newcore = core.merge(cores, result);
233    if (newcore == null) {
234      return null;
235    }
236    result.core = newcore;
237    return result;
238  }
239}