Source code

001// ***** This file is automatically generated from LinearTernary.java.jpp
002
003package daikon.inv.ternary.threeScalar;
004
005import daikon.*;
006import daikon.inv.*        ;
007import daikon.inv.DiscardCode;
008import daikon.inv.DiscardInfo;
009import daikon.inv.binary.twoScalar.*;
010import daikon.inv.unary.scalar.*;
011import daikon.suppress.NIS;
012import java.util.*;
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.checkerframework.framework.qual.Unused;
018import typequals.prototype.qual.NonPrototype;
019import typequals.prototype.qual.Prototype;
020
021/**
022 * Represents a Linear invariant over three double scalars {@code x},
023 * {@code y}, and {@code z}, of the form
024 * {@code ax + by + cz + d = 0}.
025 * The constants {@code a}, {@code b}, {@code c}, and
026 * {@code d} are mutually relatively prime, and the constant
027 * {@code a} is always positive.
028 */
029
030@SuppressWarnings("UnnecessaryParentheses")  // generated code, parens are sometimes necessary
031public class LinearTernaryFloat extends ThreeFloat {
032  static final long serialVersionUID = 20030822L;
033
034  // Variables starting with dkconfig_ should only be set via the
035  // daikon.config.Configuration interface.
036  /** Boolean. True iff LinearTernary invariants should be considered. */
037  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
038
039  public static final boolean debugLinearTernary = false;
040  // public static final boolean debugLinearTernary = true;
041
042  @Unused(when=Prototype.class)
043  public LinearTernaryCoreFloat core;
044
045  @SuppressWarnings("nullness") // circular initialization
046  protected LinearTernaryFloat(PptSlice ppt) {
047    super(ppt);
048    core = new LinearTernaryCoreFloat(this);
049  }
050
051  protected @Prototype LinearTernaryFloat() {
052    super();
053  }
054
055  private static @Prototype LinearTernaryFloat proto = new @Prototype LinearTernaryFloat();
056
057  /** Returns the prototype invariant for LinearTernaryFloat */
058  public static @Prototype LinearTernaryFloat get_proto() {
059    return proto;
060  }
061
062  @Override
063  public boolean enabled() {
064    return dkconfig_enabled;
065  }
066
067  @Override
068  public boolean instantiate_ok(VarInfo[] vis) {
069
070    if (!valid_types(vis)) {
071      return false;
072    }
073
074    // make sure the variables are integral
075    if (!vis[0].file_rep_type.isFloat()
076        || !vis[1].file_rep_type.isFloat()
077        || !vis[2].file_rep_type.isFloat())
078      return false;
079
080    // Don't create if any of the variables are constant.
081    // DynamicConstants will create this from LinearBinary
082    // and the constant value if/when all of its variables are non-constant
083    PptTopLevel parent = vis[0].ppt;
084    if (NIS.dkconfig_enabled && (parent.is_constant(vis[0])
085                                 || parent.is_constant(vis[1])
086                                 || parent.is_constant(vis[2])))
087      return false;
088
089    /*
090    // JHP: This code is removed because these sorts of static checks
091    // can't be reliably performed with equality sets (just because
092    // the leaders are obvious subsets, does not imply that all members
093    // are.  Eventually this should be moved to isObviousStatically()
094
095    VarInfo x = ppt.var_infos[0];
096    VarInfo y = ppt.var_infos[1];
097    VarInfo z = ppt.var_infos[2];
098
099    if (((x.derived instanceof SequenceLength)
100         && (((SequenceLength) x.derived).shift != 0))
101        || ((y.derived instanceof SequenceLength)
102            && (((SequenceLength) y.derived).shift != 0))
103        || ((z.derived instanceof SequenceLength)
104            && (((SequenceLength) z.derived).shift != 0))) {
105      // Do not instantiate z-1 = ax + by + c.  Instead, choose a different c.
106      Global.implied_noninstantiated_invariants += 1;
107      return null;
108    }
109
110    VarInfo x_summand = null;
111    VarInfo y_summand = null;
112    VarInfo z_summand = null;
113    if (x.derived instanceof SequenceSum) {
114      x_summand = ((SequenceSum) x.derived).base;
115    }
116    if (y.derived instanceof SequenceSum) {
117      y_summand = ((SequenceSum) y.derived).base;
118    }
119    if (z.derived instanceof SequenceSum) {
120    z_summand = ((SequenceSum) z.derived).base;
121    }
122
123    if ((x_summand != null) && (y_summand != null) && (z_summand != null)) {
124      // all 3 of x, y, and z are "sum(...)"
125      // avoid sum(a[0..i]) + sum(a[i..]) = sum(a[])
126
127      if (debugLinearTernary) {
128        System.out.println(ppt.varNames() + " 3 summands: " + x_summand.name + " " + y_summand.name + " " + z_summand.name);
129      }
130
131      VarInfo x_seq = x_summand.isDerivedSubSequenceOf();
132      VarInfo y_seq = y_summand.isDerivedSubSequenceOf();
133      VarInfo z_seq = z_summand.isDerivedSubSequenceOf();
134      if (x_seq == null) x_seq = x_summand;
135      if (y_seq == null) y_seq = y_summand;
136      if (z_seq == null) z_seq = z_summand;
137      VarInfo seq = x_seq;
138
139      if (debugLinearTernary) {
140        System.out.println(ppt.varNames() + " 3 sequences: " + x_seq.name + " " + y_seq.name + " " + z_seq.name);
141      }
142
143      if (((seq == x_summand) || (seq == y_summand) || (seq == z_summand))
144          && (x_seq == y_seq) && (x_seq == z_seq)) {
145        assert y_seq == z_seq;
146        if (debugLinearTernary) {
147          System.out.println(ppt.varNames() + " 3 sequences match");
148        }
149
150        SequenceFloatSubsequence part1 = null;
151        SequenceFloatSubsequence part2 = null;
152        for (int i = 0; i < 3; i++) {
153          VarInfo vi = ppt.var_infos[i];
154          VarInfo summand = ((SequenceSum) vi.derived).base;
155          if (debugLinearTernary) {
156            System.out.println("considering: " + summand.name + " " + vi.name);
157          }
158          if (summand.derived instanceof SequenceFloatSubsequence) {
159            SequenceFloatSubsequence sss = (SequenceFloatSubsequence) summand.derived;
160            if (sss.from_start) {
161              part1 = sss;
162            } else {
163              part2 = sss;
164            }
165          } else {
166            if (debugLinearTernary) {
167              System.out.println("Not subseq: " + summand.name + " " + vi.name);
168            }
169          }
170        }
171        if (debugLinearTernary) {
172          System.out.println(ppt.varNames() + " part1=" + part1 + ", part2=" + part2 + ", seq=" + seq.name);
173        }
174        if ((part1 != null) && (part2 != null)) {
175          // now part1, and part2 are set
176          if ((part1.sclvar() == part2.sclvar())
177              && (part1.index_shift + 1 == part2.index_shift)) {
178            if (debugLinearTernary) {
179              System.out.println("LinearTernary suppressed: " + ppt.varNames());
180            }
181            Global.implied_noninstantiated_invariants += 1;
182            return null;
183          }
184        }
185      }
186    } else if ((x_summand != null) && (y_summand != null)
187               || ((x_summand != null) && (z_summand != null))
188               || ((y_summand != null) && (z_summand != null))) {
189      // two of x, y, and z are "sum(...)"
190      // avoid sum(a[0..i-1]) + a[i] = sum(a[0..i])
191
192      // if (debugLinearTernary) {
193      //   System.out.println(ppt.varNames() + " 2 summands: " + x_summand + " " + y_summand + " " + z_summand);
194      // }
195
196      // The intention is that parta is a[0..i], partb is a[0..i-1], and
197      // notpart is a[i].
198      VarInfo parta;
199      VarInfo partb;
200      VarInfo notpart;
201
202      if (x_summand != null) {
203        parta = x;
204        if (y_summand != null) {
205          partb = y;
206          notpart = z;
207        } else {
208          partb = z;
209          notpart = y;
210        }
211      } else {
212        notpart = x;
213        parta = y;
214        partb = z;
215      }
216      parta = ((SequenceSum) parta.derived).base;
217      partb = ((SequenceSum) partb.derived).base;
218      VarInfo seq = null;
219      VarInfo eltindex = null;
220      if (notpart.derived instanceof SequenceFloatSubscript) {
221        SequenceFloatSubscript sss = (SequenceFloatSubscript) notpart.derived;
222        seq = sss.seqvar();
223        eltindex = sss.sclvar();
224      }
225      if ((seq != null)
226          && (seq == parta.isDerivedSubSequenceOf())
227          && (seq == partb.isDerivedSubSequenceOf())) {
228        // For now, don't deal with case where one variable is the entire
229        // sequence.
230        if (!((parta == seq) || (partb == seq))) {
231          SequenceFloatSubsequence a_sss = (SequenceFloatSubsequence) parta.derived;
232          SequenceFloatSubsequence b_sss = (SequenceFloatSubsequence) partb.derived;
233          if ((a_sss.sclvar() == eltindex)
234              && (b_sss.sclvar() == eltindex)) {
235            if ((a_sss.from_start
236                 && b_sss.from_start
237                 && (((a_sss.index_shift == -1) && (b_sss.index_shift == 0))
238                     || ((a_sss.index_shift == 0) && (b_sss.index_shift == -1))))
239                || ((!a_sss.from_start)
240                    && (!b_sss.from_start)
241                    && (((a_sss.index_shift == 0) && (b_sss.index_shift == 1))
242                        || ((a_sss.index_shift == 1) && (b_sss.index_shift == 0))))) {
243            Global.implied_noninstantiated_invariants += 1;
244            return null;
245            }
246          }
247        }
248      }
249    }
250    */
251
252    return true;
253  }
254
255  @Override
256  public LinearTernaryFloat instantiate_dyn(@Prototype LinearTernaryFloat this, PptSlice slice) {
257    return new LinearTernaryFloat(slice);
258  }
259
260  @SideEffectFree
261  @Override
262  public LinearTernaryFloat clone(@GuardSatisfied LinearTernaryFloat this) {
263    LinearTernaryFloat result = (LinearTernaryFloat) super.clone();
264    result.core = core.clone();
265    result.core.wrapper = result;
266    return result;
267  }
268
269  @Override
270  protected Invariant resurrect_done(int[] permutation) {
271    core.permute(permutation);
272    return this;
273  }
274
275  @Override
276  public String repr(@GuardSatisfied LinearTernaryFloat this) {
277    return "LinearTernaryFloat" + varNames() + ": falsified=" + falsified
278      + "; " + core.repr();
279  }
280
281  @SideEffectFree
282  @Override
283  public String format_using(@GuardSatisfied LinearTernaryFloat this, OutputFormat format) {
284    return core.format_using(format, var1().name_using(format),
285                        var2().name_using(format), var3().name_using(format));
286  }
287
288  // public String format_reversed() {
289  //   return core.format_reversed(var1().name.name(), var2().name.name(), var3().name.name());
290  // }
291
292  @Pure
293  @Override
294  public boolean isActive() {
295    return core.isActive();
296  }
297
298  public InvariantStatus setup(LinearBinaryFloat lb, VarInfo con_var,
299                                double con_val) {
300    return core.setup(lb, con_var, con_val);
301  }
302
303  public InvariantStatus setup(OneOfFloat oo, VarInfo v1, double con1,
304                                VarInfo v2, double con2) {
305    return core.setup(oo, v1, con1, v2, con2);
306  }
307
308  @Override
309  public InvariantStatus check_modified(double x, double y, double z, int count) {
310    return clone().add_modified(x, y, z, count);
311  }
312
313  @Override
314  public InvariantStatus add_modified(double x, double y, double z, int count) {
315    return core.add_modified(x, y, z, count);
316  }
317
318  @Override
319  public boolean enoughSamples(@GuardSatisfied LinearTernaryFloat this) {
320    return core.enoughSamples();
321  }
322
323  @Override
324  protected double computeConfidence() {
325    return core.computeConfidence();
326  }
327
328  @Pure
329  @Override
330  public boolean isExact() {
331    return true;
332  }
333
334  @Pure
335  @Override
336  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
337    DiscardInfo super_result = super.isObviousDynamically(vis);
338    if (super_result != null) {
339      return super_result;
340    }
341
342    if (core.a == 0 || core.b == 0 || core.c == 0) {
343      return new DiscardInfo(this, DiscardCode.obvious, "If a coefficient is 0, a LinearBinary should"
344                             + " exist over the other two variables");
345    }
346
347    return null;
348  }
349
350  @Pure
351  @Override
352  public boolean isSameFormula(Invariant other) {
353    return core.isSameFormula(((LinearTernaryFloat) other).core);
354  }
355
356  @Pure
357  @Override
358  public boolean isExclusiveFormula(Invariant other) {
359    if (other instanceof LinearTernaryFloat) {
360      return core.isExclusiveFormula(((LinearTernaryFloat) other).core);
361    }
362    return false;
363  }
364
365  // Look up a previously instantiated invariant.
366  public static @Nullable LinearTernaryFloat find(PptSlice ppt) {
367    assert ppt.arity() == 3;
368    for (Invariant inv : ppt.invs) {
369      if (inv instanceof LinearTernaryFloat) {
370        return (LinearTernaryFloat) inv;
371      }
372    }
373    return null;
374  }
375
376  // Returns a vector of LinearTernaryFloat objects.
377  // This ought to produce an iterator instead.
378  public static List<LinearTernaryFloat> findAll(VarInfo vi) {
379    List<LinearTernaryFloat> result = new ArrayList<>();
380    for (PptSlice view : vi.ppt.views_iterable()) {
381      if ((view.arity() == 3) && view.usesVar(vi)) {
382        LinearTernaryFloat lt = LinearTernaryFloat.find(view);
383        if (lt != null) {
384          result.add(lt);
385        }
386      }
387    }
388    return result;
389  }
390
391  @Override
392  public boolean mergeFormulasOk() {
393    return core.mergeFormulasOk();
394  }
395
396  /**
397   * Merge the invariants in invs to form a new invariant. Each must be a LinearTernaryFloat invariant. The
398   * work is done by the LinearTernary core
399   *
400   * @param invs list of invariants to merge. They should all be permuted to match the variable
401   *     order in parent_ppt.
402   * @param parent_ppt slice that will contain the new invariant
403   */
404  @Override
405  public @Nullable LinearTernaryFloat merge(List<Invariant> invs, PptSlice parent_ppt) {
406
407    // Create a matching list of cores
408    List<LinearTernaryCoreFloat> cores = new ArrayList<>();
409    for (Invariant inv : invs) {
410      cores.add(((LinearTernaryFloat) inv).core);
411    }
412
413    // Merge the cores and build a new invariant containing the merged core
414    LinearTernaryFloat result = new LinearTernaryFloat(parent_ppt);
415    LinearTernaryCoreFloat newcore = core.merge(cores, result);
416    if (newcore == null) {
417      return null;
418    }
419    result.core = newcore;
420    return result;
421  }
422}