Source code

001// ***** This file is automatically generated from FunctionBinary.java.jpp
002// ***** (and files it recursively includes).
003
004package daikon.inv.ternary.threeScalar;
005
006import daikon.*;
007import daikon.derive.unary.*;
008import daikon.inv.*;
009import daikon.inv.binary.twoScalar.*;
010import daikon.inv.unary.scalar.*;
011import daikon.suppress.*;
012import java.lang.reflect.*;
013import java.util.*;
014import java.util.logging.Logger;
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.MathPlume;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Base class for each of the FunctionBinaryFloat functions and permutatons. Most of the work is done
026 * here. The subclasses basically define the function and return information describing the function
027 * and permutation to these methods.
028 */
029@SuppressWarnings("UnusedVariable")  // generated code, complex rules for when var is used
030public abstract class FunctionBinaryFloat extends ThreeFloat {
031  // We are Serializable, so we specify a version to allow changes to
032  // method signatures without breaking serialization.  If you add or
033  // remove fields, you should change this number to the current date.
034  static final long serialVersionUID = 20031030L;
035
036  /** Boolean. True if FunctionBinaryFloat invariants should be considered. */
037  public static boolean dkconfig_enabled = false;
038
039  public static Logger debug =
040    Logger.getLogger("daikon.inv.ternary.threeScalar.#CLASSNAME");
041
042  static final int[][] var_indices;
043  static {
044    var_indices = new int[7][];
045    var_indices[1] = new int[] { 0, 1, 2 };
046    var_indices[2] = new int[] { 1, 0, 2 };
047    var_indices[3] = new int[] { 2, 0, 1 };
048    var_indices[4] = new int[] { 0, 2, 1 };
049    var_indices[5] = new int[] { 1, 2, 0 };
050    var_indices[6] = new int[] { 2, 1, 0 };
051  }
052
053  protected FunctionBinaryFloat(PptSlice ppt) {
054    super(ppt);
055  }
056
057  protected @Prototype FunctionBinaryFloat() {
058    super();
059  }
060
061  /** returns whether or not this invariant is enabled */
062  @Override
063  public boolean enabled() {
064    return dkconfig_enabled;
065  }
066
067  /** FunctionBinaryFloat is only valid on isFloat() types. */
068  @Override
069  public boolean instantiate_ok(VarInfo[] vis) {
070
071    if (!valid_types(vis)) {
072      return false;
073    }
074
075    // Make sure that each variable is integral (not boolean or hashcode)
076    if (!vis[0].file_rep_type.isFloat()
077        || !vis[1].file_rep_type.isFloat()
078        || !vis[2].file_rep_type.isFloat())
079      return false;
080
081    return true;
082  }
083
084  // check_modified relies on func having no side effects.
085  abstract double func(double arg1, double arg2);
086  @Pure
087  abstract boolean is_symmetric();
088  abstract String[] get_method_name(@GuardSatisfied FunctionBinaryFloat this);
089  abstract int get_var_order(@GuardSatisfied FunctionBinaryFloat this);
090  abstract void set_function_id(int function_id);
091  abstract int get_function_id();
092
093  /**
094   * Map from function name (eg, MultiplyLong, MinimumFloat) to an array of instances (one for each
095   * valid permutation) for that function.
096   */
097  private static Map<String,@Prototype FunctionBinaryFloat[]> functions = new LinkedHashMap<>();
098
099  /**
100   * A list indexed by function number to an array of instances (one for each valid permutation) for
101   * that function. The array is the same one as is stored in the functions Map. This provides a
102   * faster access mechanism once we have the function id (which are calculated the first time
103   * through).
104   */
105  private static List<@Prototype FunctionBinaryFloat[]> func_list = new ArrayList<>();
106
107  private static void build_func_list() {
108
109    // Reflection seems to confuse clover
110    ///CLOVER:OFF
111
112    // Build the map of functions to array of instances for that function
113    debug.fine("Processing FunctionBinaryFloat");
114    functions = new LinkedHashMap<>();
115    @SuppressWarnings("unchecked")
116    Class<@Prototype FunctionBinaryFloat>[] subclasses = (Class<@Prototype FunctionBinaryFloat>[]) FunctionBinaryFloat.class.getDeclaredClasses();
117    for (int ii = 0; ii < subclasses.length; ii++) {
118      Class<@Prototype FunctionBinaryFloat> subc = subclasses[ii];
119      String function = subc.getName();
120      if (function.indexOf("CLOVER") >= 0) {
121        continue;
122      }
123      function = function.replaceFirst(".*FunctionBinary\\$", "");
124      function = function.replaceFirst("_.*", "");
125      if (function.equals("SubClass")) {
126        continue;
127      }
128      @Prototype FunctionBinaryFloat[] fb_arr = functions.get(function);
129      if (fb_arr == null) {
130        fb_arr = new @Prototype FunctionBinaryFloat[7];
131        functions.put(function, fb_arr);
132        func_list.add(fb_arr);
133      }
134      int func_id = func_list.indexOf(fb_arr);
135      @SuppressWarnings({"nonprototype"})
136      @Prototype FunctionBinaryFloat fb;
137      try {
138        Constructor<@Prototype FunctionBinaryFloat> con = subc.getDeclaredConstructor(new Class<?>[] {});
139        fb = con.newInstance(new Object[] {});
140      }  catch (Exception e) {
141        throw new Error(" can't create instance for " + subc.getName()
142                        + ": '" + e + "' ii = " + ii);
143      }
144      assert fb_arr[fb.get_var_order()] == null;
145      fb_arr[fb.get_var_order()] = fb;
146      fb.set_function_id(func_id);
147      debug.fine("Adding " + function + " " + fb.getClass().getName()
148                  + " " + fb.get_var_order() + " " + fb.get_function_id());
149    }
150    ///CLOVER:ON
151  }
152
153  /** Returns a list of all of the FunctionBinaryFloat prototype invariants. */
154  public static List<@Prototype Invariant> get_proto_all() {
155
156    List<@Prototype Invariant> result = new ArrayList<>();
157
158    // If this is the first call
159    if (functions.isEmpty()) {
160      build_func_list();
161    }
162
163    // Get the proto invariant for all of the subclasses and return them
164    for (@Prototype FunctionBinaryFloat[] fb_arr : func_list) {
165      for (int jj = 1; jj < fb_arr.length; jj++) {
166        @Prototype FunctionBinaryFloat fb = fb_arr[jj];
167        if (fb != null) {
168          result.add(fb);
169        }
170      }
171    }
172    return result;
173  }
174
175  /** Permuted result var. */
176  public VarInfo resultVar() {
177    return ppt.var_infos[var_indices[get_var_order()][0]];
178  }
179
180  /** Permuted arg1 var. */
181  public VarInfo argVar1() {
182    return ppt.var_infos[var_indices[get_var_order()][1]];
183  }
184
185  /** Permuted arg2 var. */
186  public VarInfo argVar2() {
187    return ppt.var_infos[var_indices[get_var_order()][2]];
188  }
189
190  /**
191   * Apply the specified sample to the function, returning the result. The caller is responsible
192   * for permuting the arguments.
193   */
194  public InvariantStatus check_ordered(double result, double arg1,
195                                      double arg2, int count) {
196    // This implementation relies on func having no side effects.
197    try {
198      if (!Global.fuzzy.eq(result, func(arg1, arg2))) {
199        return InvariantStatus.FALSIFIED;
200      }
201    } catch (Exception e) {
202        return InvariantStatus.FALSIFIED;
203    }
204    return InvariantStatus.NO_CHANGE;
205  }
206
207  /**
208   * Apply the specified sample to the function, returning the result. The caller is responsible
209   * for permuting the arguments.
210   */
211  public InvariantStatus add_ordered(double result, double arg1,
212                                      double arg2, int count) {
213    return check_ordered(result, arg1, arg2, count);
214  }
215
216  /**
217   * Reorganize our already-seen state as if the variables had shifted order underneath us
218   * (re-arrangement given by the permutation). We accomplish this by returning the class that
219   * corresponds to the new permutation.
220   */
221  @Override
222  protected Invariant resurrect_done(int[] permutation) {
223
224    assert permutation.length == 3;
225    assert ArraysPlume.fnIsPermutation(permutation);
226
227    int[] new_order = new int[3];
228    int[] old_order = var_indices[get_var_order()];
229
230    // "permutation" is a permutation on the var_info array. old_order
231    // was the permutation that took the formatted invariant to the
232    // var_info array, so old_order^-1 is the permutation from the
233    // var_info array to the old formatted invariant. We want to find
234    // a new_order so that when we first do "permutation", then
235    // apply the new permutation from the var_info array to the
236    // formatted invariant, we get the same formatted invariant.
237    // What we want, then. is:
238    //    new_order^-1 o permutation = old_order^-1
239    // rearranging, this is equivalent to
240    //    new_order = permutation o old_order
241    new_order[0] = permutation[old_order[0]];
242    new_order[1] = permutation[old_order[1]];
243    new_order[2] = permutation[old_order[2]];
244
245    // Force symmetric functions into a canonical form so that
246    // we can match them when necessary and they always print the same.
247    // For example, order of 0, 1, 2 and 0, 2, 1 represent the same
248    // invariant for a symmetric function.  This forces them to always
249    // be represented as 0, 1, 2
250    if (is_symmetric()) {
251      if (new_order[2] < new_order[1]) {
252        int tmp = new_order[2];
253        new_order[2] = new_order[1];
254        new_order[1] = tmp;
255      }
256    }
257
258    // Look for the new order in the list of possible orders
259    int var_order = -1;
260    for (int i = 0; i < var_indices.length; i++) {
261      if (Arrays.equals(new_order, var_indices[i])) {
262        var_order = i;
263        break;
264      }
265    }
266    assert var_order != -1;
267
268    // If the var order hasn't changed, we don't need to do anything
269    if (var_order == get_var_order()) {
270      return this;
271    }
272
273    // Find the class that corresponds to the new order
274    if (functions.isEmpty()) {
275      build_func_list();
276    }
277    int func_id = get_function_id();
278    @Prototype FunctionBinaryFloat[] fb_arr = func_list.get(func_id);
279    assert fb_arr != null;
280    for (int ii = 0; ii < fb_arr.length; ii++) {
281      if ((fb_arr[ii] != null) && (fb_arr[ii].get_var_order() == var_order)) {
282        return fb_arr[ii].instantiate_dyn(ppt);
283      }
284    }
285
286    throw new Error("Could not find new ordering");
287  }
288
289  @Override
290  public String repr(@GuardSatisfied FunctionBinaryFloat this) {
291    return format();
292  }
293
294  @SideEffectFree
295  @Override
296  public String format_using(@GuardSatisfied FunctionBinaryFloat this, OutputFormat format) {
297    if (format == OutputFormat.SIMPLIFY) {
298      return format_simplify();
299    }
300    if (format == OutputFormat.CSHARPCONTRACT) {
301      return format_csharp_contract();
302    }
303
304    int var_order = get_var_order();
305    String[] methodname = get_method_name();
306
307    VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]];
308    VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]];
309    VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]];
310
311    String argresult_name = argresultvi.name_using(format);
312    String arg1_name = arg1vi.name_using(format);
313    String arg2_name = arg2vi.name_using(format);
314
315    if (format == OutputFormat.DAIKON) {
316      return argresult_name + " == (" + methodname[0] + arg1_name
317        + methodname[1] + arg2_name + methodname[2] + ")";
318    }
319
320    if (format.isJavaFamily()) {
321      if (methodname[1].equals(" || ") || methodname[1].equals(" && ")) {
322        return "(" +  argresult_name + " != 0) == ((" + methodname[0] + arg1_name + " != 0)"
323          + methodname[1] + "(" + arg2_name + methodname[2] + " != 0))";
324      } else {
325        return argresult_name + " == (" + methodname[0] + arg1_name
326          + methodname[1] + arg2_name + methodname[2] + ")";
327      }
328    }
329
330    return format_unimplemented(format);
331  }
332
333  public String format_simplify(@GuardSatisfied FunctionBinaryFloat this) {
334    int var_order = get_var_order();
335    String[] methodname = get_method_name();
336    VarInfo[] vis = ppt.var_infos;
337
338    String result = vis[var_indices[var_order][0]].simplifyFixedupName();
339    String arg1 = vis[var_indices[var_order][1]].simplifyFixedupName();
340    String arg2 = vis[var_indices[var_order][2]].simplifyFixedupName();
341    String func = null;
342    if (methodname[1].equals(" * ")) {
343      func = "*";
344    } else if (methodname[1].equals(" | ")) {
345      func = "|java-bitwise-or|";
346    } else if (methodname[1].equals(" || ")) {
347      func = "|java-logical-or|";
348    } else if (methodname[1].equals(", ")) {
349      if (methodname[0].equals("java.lang.Math.min(")) {
350        func = "min";
351      } else if (methodname[0].equals("java.lang.Math.max(")) {
352        func = "max";
353      } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) {
354        func = "gcd";
355      } else if (methodname[0].equals("java.lang.Math.pow(")) {
356        func = "pow";
357      } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) {
358        func = "|java-logical-xor|";
359      }
360    } else {
361      assert methodname[0].equals("");
362      assert methodname[2].equals("");
363      func = "|java-" + methodname[1].trim() + "|";
364    }
365    if (func == null) {
366      return "format_simplify_contract() doesn't know function " + methodname[0] + "-"
367        + methodname[1] + "-" + methodname[2];
368    }
369    return "(EQ " + result + " (" + func + " " + arg1 + " " + arg2 + "))";
370  }
371
372  public String format_csharp_contract(@GuardSatisfied FunctionBinaryFloat this) {
373    int var_order = get_var_order();
374    String[] methodname = get_method_name();
375
376    VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]];
377    VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]];
378    VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]];
379    String result = argresultvi.csharp_name();
380    String arg1 = arg1vi.csharp_name();
381    String arg2 = arg2vi.csharp_name();
382    String operator = null;
383
384    if (methodname[1].equals(" * ")) {
385      operator = "*";
386    } else if (methodname[1].equals(" | ")) {
387      operator = "|";
388    } else if (methodname[1].equals(" & ")) {
389      operator = "&";
390    } else if (methodname[1].equals(" / ")) {
391      operator = "/";
392    } else if (methodname[1].equals(" ^ ")) {
393      operator = "^";
394    } else if (methodname[1].equals(" % ")) {
395      operator = "%";
396    } else if (methodname[1].equals(" && ")) {
397      operator = "&&";
398    } else if (methodname[1].equals(" || ")) {
399      operator = "||";
400    } else if (methodname[1].equals(" >> ")) {
401      operator = ">>";
402    } else if (methodname[1].equals(" >>> ")) {
403      return result + " == " + arg1 + ".UnsignedRightShift(" + arg2 + ")";
404      //return result + " == CSharpDaikonLib.Extensions.UnsignedRightShift(" + arg1 + ", " + arg2 + ")";
405    } else if (methodname[1].equals(" << ")) {
406      operator = "<<";
407    }
408
409    if (operator != null) {
410      return result + " == (" + arg1 + " " + operator + " " + arg2 + ")";
411    }
412
413    String func = null;
414    if (methodname[1].equals(", ")) {
415      if (methodname[0].equals("java.lang.Math.min(")) {
416        func = "Math.Min";
417      } else if (methodname[0].equals("java.lang.Math.max(")) {
418        func = "Math.Max";
419      } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) {
420        return result + " == CSharpDaikonLib.Extensions.GCD(" + arg1 + ", " + arg2 + ")";
421      } else if (methodname[0].equals("java.lang.Math.pow(")) {
422        return result + " == " + arg1 + ".Pow(" + arg2 + ")";
423      } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) {
424        return result + " == (" + arg1 + " ^ " + arg2 + ")";
425      }
426    } else {
427      assert methodname[0].equals("");
428      assert methodname[2].equals("");
429      func = "|" + methodname[1].trim() + "|";
430    }
431
432    if (func == null) {
433      return "format_csharp_contract() doesn't know function " + methodname[0] + "-" + methodname[1] + "-" + methodname[2];
434    }
435    return result + " == " + func + "(" + arg1 + ", " + arg2 + ")";
436  }
437
438  // If our classes match, we must match
439  @Pure
440  @Override
441  public boolean isSameFormula(Invariant other) {
442    return true;
443  }
444  @Override
445  public double computeConfidence() {
446    if (logOn()) {
447      VarInfo v1 = ppt.var_infos[0];
448      VarInfo v2 = ppt.var_infos[1];
449      VarInfo v3 = ppt.var_infos[2];
450      log("computeConfidence(%s: num_values = %s, num_values(%s)=%s, num_values(%s)=%s, num_values(%s)=%s",
451          format(), ppt.num_values(),
452          v1.name(), ppt.parent.num_values(v1),
453          v2.name(), ppt.parent.num_values(v2),
454          v3.name(), ppt.parent.num_values(v3));
455    }
456    return Invariant.conf_is_ge(ppt.num_values(), 5);
457  }
458
459  /** If the arg is a sequence size, return the sequence; otherwise return null. */
460  private @Nullable VarInfo sized_sequence(VarInfo size) {
461    if (size.derived instanceof SequenceLength) {
462      return ((SequenceLength)size.derived).base;
463    }
464    return null;
465  }
466
467  @Pure
468  @Override
469  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
470
471    DiscardInfo super_result = super.isObviousDynamically(vis);
472    if (super_result != null) {
473      return super_result;
474    }
475
476    // Discard if any two of the three variables are the sizes of the
477    // same arrays.
478    VarInfo arr1 = sized_sequence(vis[0]);
479    VarInfo arr2 = sized_sequence(vis[1]);
480    VarInfo arr3 = sized_sequence(vis[2]);
481    if (((arr1 != null) && (arr1 == arr2))
482        || ((arr1 != null) && (arr1 == arr3))
483        || ((arr2 != null) && (arr2 == arr3))) {
484      return new DiscardInfo(this, DiscardCode.obvious,
485                    "two are sizes of same array:  "
486                    + vis[0].name() + " "
487                    + vis[1].name() + " "
488                    + vis[2].name());
489    }
490
491    return null;
492  }
493
494  // default is that it is not this function, overriden in the subclass
495  @Pure
496  public boolean isMultiply() {
497    return false;
498  }
499
500/**
501 * Represents the invariant {@code x = Multiply(y, z)} over three double
502 * scalars. 
503 */
504public static class MultiplyDouble_xyz extends FunctionBinaryFloat {
505  // We are Serializable, so we specify a version to allow changes to
506  // method signatures without breaking serialization.  If you add or
507  // remove fields, you should change this number to the current date.
508  static final long serialVersionUID = 20031030L;
509
510  private static @Prototype MultiplyDouble_xyz proto = new @Prototype MultiplyDouble_xyz ();
511
512  /** Returns the prototype invariant for MultiplyDouble_xyz */
513  public static @Prototype MultiplyDouble_xyz get_proto() {
514    return proto;
515  }
516
517  /** instantiate an invariant on the specified slice */
518  @Override
519  protected MultiplyDouble_xyz instantiate_dyn(@Prototype MultiplyDouble_xyz this, PptSlice slice) {
520    return new MultiplyDouble_xyz (slice);
521  }
522
523  private MultiplyDouble_xyz (PptSlice slice) {
524    super(slice);
525  }
526
527  public @Prototype MultiplyDouble_xyz () {
528    super();
529  }
530
531  private static String[] method_name = new String[] {"", " * ", ""};
532
533  @Override
534  public String[] get_method_name(@GuardSatisfied MultiplyDouble_xyz this) {
535    return method_name;
536  }
537
538  private static int function_id = -1;
539
540  @Override
541  public int get_function_id() {
542    return function_id;
543  }
544
545  @Override
546  public void set_function_id(int function_id) {
547    assert MultiplyDouble_xyz.function_id == -1;
548    MultiplyDouble_xyz.function_id = function_id;
549  }
550
551  private static int var_order = 1;
552
553  @Override
554  public int get_var_order(@GuardSatisfied MultiplyDouble_xyz this) {
555    return var_order;
556  }
557
558  @Pure
559  @Override
560  public boolean is_symmetric() {
561
562      return true;
563  }
564
565  @Override
566
567  public double func(double y, double z) {
568
569    return y * z;
570  }
571
572  @Override
573  public InvariantStatus check_modified(double x, double y,
574                                      double z, int count) {
575    return check_ordered(x, y, z, count);
576  }
577
578  @Override
579  public InvariantStatus add_modified(double x, double y,
580                                      double z, int count) {
581    if (Debug.logDetail()) {
582      log("result=%s, arg1=%s, arg2=%s", x, y, z);
583    }
584    return add_ordered(x, y, z, count);
585  }
586
587  @Pure
588  @Override
589  public boolean isMultiply() {
590    return true;
591  }
592
593  @Pure
594  @Override
595  public boolean isExact() {
596    return true;
597  }
598
599  /** Returns a list of non-instantiating suppressions for this invariant. */
600  @Pure
601  @Override
602  public @Nullable NISuppressionSet get_ni_suppressions() {
603    if (NIS.dkconfig_enabled && dkconfig_enabled) {
604      return suppressions;
605    } else {
606      return null;
607    }
608  }
609
610  /** definition of this invariant (the suppressee) */
611  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_xyz.class, 3);
612
613  // suppressor definitions (used below)
614  private static NISuppressor result_eq_arg1 =
615      new NISuppressor(0, 1, FloatEqual.class);
616  private static NISuppressor result_eq_arg2 =
617      new NISuppressor(0, 2, FloatEqual.class);
618  private static NISuppressor arg1_eq_arg2 =
619      new NISuppressor(1, 2, FloatEqual.class);
620
621  private static NISuppressor result_lt_arg1 =
622      new NISuppressor(0, 1, FloatLessThan.class);
623  private static NISuppressor result_lt_arg2 =
624      new NISuppressor(0, 2, FloatLessThan.class);
625  private static NISuppressor arg1_lt_arg2 =
626      new NISuppressor(1, 2, FloatLessThan.class);
627  private static NISuppressor arg2_lt_arg1 =
628      new NISuppressor(2, 1, FloatLessThan.class);
629
630  private static NISuppressor result_le_arg1 =
631      new NISuppressor(0, 1, FloatLessEqual.class);
632  private static NISuppressor result_le_arg2 =
633      new NISuppressor(0, 2, FloatLessEqual.class);
634  private static NISuppressor arg1_le_arg2 =
635      new NISuppressor(1, 2, FloatLessEqual.class);
636  private static NISuppressor arg2_le_arg1 =
637      new NISuppressor(2, 1, FloatLessEqual.class);
638
639  private static NISuppressor result_track0_arg1 =
640      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
641  private static NISuppressor result_track0_arg2 =
642      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
643  private static NISuppressor arg1_track0_arg2 =
644      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
645  private static NISuppressor arg1_track0_result =
646      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
647  private static NISuppressor arg2_track0_result =
648      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
649  private static NISuppressor arg2_track0_arg1 =
650      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
651
652  private static NISuppressor result_eq_1 =
653      new NISuppressor(0, RangeFloat.EqualOne.class);
654  private static NISuppressor arg1_eq_1 =
655      new NISuppressor(1, RangeFloat.EqualOne.class);
656  private static NISuppressor arg2_eq_1 =
657      new NISuppressor(2, RangeFloat.EqualOne.class);
658
659  private static NISuppressor result_eq_0 =
660      new NISuppressor(0, RangeFloat.EqualZero.class);
661  private static NISuppressor arg1_eq_0 =
662      new NISuppressor(1, RangeFloat.EqualZero.class);
663  private static NISuppressor arg2_eq_0 =
664      new NISuppressor(2, RangeFloat.EqualZero.class);
665
666  private static NISuppressor result_ne_0 =
667      new NISuppressor(0, NonZeroFloat.class);
668  private static NISuppressor arg1_ne_0 =
669      new NISuppressor(1, NonZeroFloat.class);
670  private static NISuppressor arg2_ne_0 =
671      new NISuppressor(2, NonZeroFloat.class);
672
673  private static NISuppressor result_ge_0 =
674      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
675  private static NISuppressor arg1_ge_0 =
676      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
677  private static NISuppressor arg2_ge_0 =
678      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
679
680  private static NISuppressor result_ge_64 =
681      new NISuppressor(0, RangeInt.GreaterEqual64.class);
682  private static NISuppressor arg1_ge_64 =
683      new NISuppressor(1, RangeInt.GreaterEqual64.class);
684  private static NISuppressor arg2_ge_64 =
685      new NISuppressor(2, RangeInt.GreaterEqual64.class);
686
687    private static NISuppressionSet suppressions =
688      new NISuppressionSet(
689          new NISuppression[] {
690
691            // (r == 0) && (y == 0) ==> r = y * z
692            new NISuppression(result_eq_0, arg1_eq_0, suppressee),
693
694            // (r == 0) && (z == 0) ==> r = y * z
695            new NISuppression(result_eq_0, arg2_eq_0, suppressee),
696
697            // (r == y) && (z == 1) ==> r = y * z
698            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
699
700            // (r == z) && (y == 1) ==> r = y * z
701            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),
702
703          });
704
705  // Create a suppression factory for functionBinary
706
707}
708
709/**
710 * Represents the invariant {@code y = Multiply(x, z)} over three double
711 * scalars. 
712 */
713public static class MultiplyDouble_yxz extends FunctionBinaryFloat {
714  // We are Serializable, so we specify a version to allow changes to
715  // method signatures without breaking serialization.  If you add or
716  // remove fields, you should change this number to the current date.
717  static final long serialVersionUID = 20031030L;
718
719  private static @Prototype MultiplyDouble_yxz proto = new @Prototype MultiplyDouble_yxz ();
720
721  /** Returns the prototype invariant for MultiplyDouble_yxz */
722  public static @Prototype MultiplyDouble_yxz get_proto() {
723    return proto;
724  }
725
726  /** instantiate an invariant on the specified slice */
727  @Override
728  protected MultiplyDouble_yxz instantiate_dyn(@Prototype MultiplyDouble_yxz this, PptSlice slice) {
729    return new MultiplyDouble_yxz (slice);
730  }
731
732  private MultiplyDouble_yxz (PptSlice slice) {
733    super(slice);
734  }
735
736  public @Prototype MultiplyDouble_yxz () {
737    super();
738  }
739
740  private static String[] method_name = new String[] {"", " * ", ""};
741
742  @Override
743  public String[] get_method_name(@GuardSatisfied MultiplyDouble_yxz this) {
744    return method_name;
745  }
746
747  private static int function_id = -1;
748
749  @Override
750  public int get_function_id() {
751    return function_id;
752  }
753
754  @Override
755  public void set_function_id(int function_id) {
756    assert MultiplyDouble_yxz.function_id == -1;
757    MultiplyDouble_yxz.function_id = function_id;
758  }
759
760  private static int var_order = 2;
761
762  @Override
763  public int get_var_order(@GuardSatisfied MultiplyDouble_yxz this) {
764    return var_order;
765  }
766
767  @Pure
768  @Override
769  public boolean is_symmetric() {
770
771      return true;
772  }
773
774  @Override
775
776  public double func(double x, double z) {
777
778    return x * z;
779  }
780
781  @Override
782  public InvariantStatus check_modified(double x, double y,
783                                      double z, int count) {
784    return check_ordered(y, x, z, count);
785  }
786
787  @Override
788  public InvariantStatus add_modified(double x, double y,
789                                      double z, int count) {
790    if (Debug.logDetail()) {
791      log("result=%s, arg1=%s, arg2=%s", y, x, z);
792    }
793    return add_ordered(y, x, z, count);
794  }
795
796  @Pure
797  @Override
798  public boolean isMultiply() {
799    return true;
800  }
801
802  @Pure
803  @Override
804  public boolean isExact() {
805    return true;
806  }
807
808  /** Returns a list of non-instantiating suppressions for this invariant. */
809  @Pure
810  @Override
811  public @Nullable NISuppressionSet get_ni_suppressions() {
812    if (NIS.dkconfig_enabled && dkconfig_enabled) {
813      return suppressions;
814    } else {
815      return null;
816    }
817  }
818
819  /** definition of this invariant (the suppressee) */
820  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_yxz.class, 3);
821
822  // suppressor definitions (used below)
823  private static NISuppressor result_eq_arg1 =
824      new NISuppressor(1, 0, FloatEqual.class);
825  private static NISuppressor result_eq_arg2 =
826      new NISuppressor(1, 2, FloatEqual.class);
827  private static NISuppressor arg1_eq_arg2 =
828      new NISuppressor(0, 2, FloatEqual.class);
829
830  private static NISuppressor result_lt_arg1 =
831      new NISuppressor(1, 0, FloatLessThan.class);
832  private static NISuppressor result_lt_arg2 =
833      new NISuppressor(1, 2, FloatLessThan.class);
834  private static NISuppressor arg1_lt_arg2 =
835      new NISuppressor(0, 2, FloatLessThan.class);
836  private static NISuppressor arg2_lt_arg1 =
837      new NISuppressor(2, 0, FloatLessThan.class);
838
839  private static NISuppressor result_le_arg1 =
840      new NISuppressor(1, 0, FloatLessEqual.class);
841  private static NISuppressor result_le_arg2 =
842      new NISuppressor(1, 2, FloatLessEqual.class);
843  private static NISuppressor arg1_le_arg2 =
844      new NISuppressor(0, 2, FloatLessEqual.class);
845  private static NISuppressor arg2_le_arg1 =
846      new NISuppressor(2, 0, FloatLessEqual.class);
847
848  private static NISuppressor result_track0_arg1 =
849      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
850  private static NISuppressor result_track0_arg2 =
851      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
852  private static NISuppressor arg1_track0_arg2 =
853      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
854  private static NISuppressor arg1_track0_result =
855      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
856  private static NISuppressor arg2_track0_result =
857      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
858  private static NISuppressor arg2_track0_arg1 =
859      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
860
861  private static NISuppressor result_eq_1 =
862      new NISuppressor(1, RangeFloat.EqualOne.class);
863  private static NISuppressor arg1_eq_1 =
864      new NISuppressor(0, RangeFloat.EqualOne.class);
865  private static NISuppressor arg2_eq_1 =
866      new NISuppressor(2, RangeFloat.EqualOne.class);
867
868  private static NISuppressor result_eq_0 =
869      new NISuppressor(1, RangeFloat.EqualZero.class);
870  private static NISuppressor arg1_eq_0 =
871      new NISuppressor(0, RangeFloat.EqualZero.class);
872  private static NISuppressor arg2_eq_0 =
873      new NISuppressor(2, RangeFloat.EqualZero.class);
874
875  private static NISuppressor result_ne_0 =
876      new NISuppressor(1, NonZeroFloat.class);
877  private static NISuppressor arg1_ne_0 =
878      new NISuppressor(0, NonZeroFloat.class);
879  private static NISuppressor arg2_ne_0 =
880      new NISuppressor(2, NonZeroFloat.class);
881
882  private static NISuppressor result_ge_0 =
883      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
884  private static NISuppressor arg1_ge_0 =
885      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
886  private static NISuppressor arg2_ge_0 =
887      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
888
889  private static NISuppressor result_ge_64 =
890      new NISuppressor(1, RangeInt.GreaterEqual64.class);
891  private static NISuppressor arg1_ge_64 =
892      new NISuppressor(0, RangeInt.GreaterEqual64.class);
893  private static NISuppressor arg2_ge_64 =
894      new NISuppressor(2, RangeInt.GreaterEqual64.class);
895
896    private static NISuppressionSet suppressions =
897      new NISuppressionSet(
898          new NISuppression[] {
899
900            // (r == 0) && (x == 0) ==> r = x * z
901            new NISuppression(result_eq_0, arg1_eq_0, suppressee),
902
903            // (r == 0) && (z == 0) ==> r = x * z
904            new NISuppression(result_eq_0, arg2_eq_0, suppressee),
905
906            // (r == x) && (z == 1) ==> r = x * z
907            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
908
909            // (r == z) && (x == 1) ==> r = x * z
910            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),
911
912          });
913
914  // Create a suppression factory for functionBinary
915
916}
917
918/**
919 * Represents the invariant {@code z = Multiply(x, y)} over three double
920 * scalars. 
921 */
922public static class MultiplyDouble_zxy extends FunctionBinaryFloat {
923  // We are Serializable, so we specify a version to allow changes to
924  // method signatures without breaking serialization.  If you add or
925  // remove fields, you should change this number to the current date.
926  static final long serialVersionUID = 20031030L;
927
928  private static @Prototype MultiplyDouble_zxy proto = new @Prototype MultiplyDouble_zxy ();
929
930  /** Returns the prototype invariant for MultiplyDouble_zxy */
931  public static @Prototype MultiplyDouble_zxy get_proto() {
932    return proto;
933  }
934
935  /** instantiate an invariant on the specified slice */
936  @Override
937  protected MultiplyDouble_zxy instantiate_dyn(@Prototype MultiplyDouble_zxy this, PptSlice slice) {
938    return new MultiplyDouble_zxy (slice);
939  }
940
941  private MultiplyDouble_zxy (PptSlice slice) {
942    super(slice);
943  }
944
945  public @Prototype MultiplyDouble_zxy () {
946    super();
947  }
948
949  private static String[] method_name = new String[] {"", " * ", ""};
950
951  @Override
952  public String[] get_method_name(@GuardSatisfied MultiplyDouble_zxy this) {
953    return method_name;
954  }
955
956  private static int function_id = -1;
957
958  @Override
959  public int get_function_id() {
960    return function_id;
961  }
962
963  @Override
964  public void set_function_id(int function_id) {
965    assert MultiplyDouble_zxy.function_id == -1;
966    MultiplyDouble_zxy.function_id = function_id;
967  }
968
969  private static int var_order = 3;
970
971  @Override
972  public int get_var_order(@GuardSatisfied MultiplyDouble_zxy this) {
973    return var_order;
974  }
975
976  @Pure
977  @Override
978  public boolean is_symmetric() {
979
980      return true;
981  }
982
983  @Override
984
985  public double func(double x, double y) {
986
987    return x * y;
988  }
989
990  @Override
991  public InvariantStatus check_modified(double x, double y,
992                                      double z, int count) {
993    return check_ordered(z, x, y, count);
994  }
995
996  @Override
997  public InvariantStatus add_modified(double x, double y,
998                                      double z, int count) {
999    if (Debug.logDetail()) {
1000      log("result=%s, arg1=%s, arg2=%s", z, x, y);
1001    }
1002    return add_ordered(z, x, y, count);
1003  }
1004
1005  @Pure
1006  @Override
1007  public boolean isMultiply() {
1008    return true;
1009  }
1010
1011  @Pure
1012  @Override
1013  public boolean isExact() {
1014    return true;
1015  }
1016
1017  /** Returns a list of non-instantiating suppressions for this invariant. */
1018  @Pure
1019  @Override
1020  public @Nullable NISuppressionSet get_ni_suppressions() {
1021    if (NIS.dkconfig_enabled && dkconfig_enabled) {
1022      return suppressions;
1023    } else {
1024      return null;
1025    }
1026  }
1027
1028  /** definition of this invariant (the suppressee) */
1029  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_zxy.class, 3);
1030
1031  // suppressor definitions (used below)
1032  private static NISuppressor result_eq_arg1 =
1033      new NISuppressor(2, 0, FloatEqual.class);
1034  private static NISuppressor result_eq_arg2 =
1035      new NISuppressor(2, 1, FloatEqual.class);
1036  private static NISuppressor arg1_eq_arg2 =
1037      new NISuppressor(0, 1, FloatEqual.class);
1038
1039  private static NISuppressor result_lt_arg1 =
1040      new NISuppressor(2, 0, FloatLessThan.class);
1041  private static NISuppressor result_lt_arg2 =
1042      new NISuppressor(2, 1, FloatLessThan.class);
1043  private static NISuppressor arg1_lt_arg2 =
1044      new NISuppressor(0, 1, FloatLessThan.class);
1045  private static NISuppressor arg2_lt_arg1 =
1046      new NISuppressor(1, 0, FloatLessThan.class);
1047
1048  private static NISuppressor result_le_arg1 =
1049      new NISuppressor(2, 0, FloatLessEqual.class);
1050  private static NISuppressor result_le_arg2 =
1051      new NISuppressor(2, 1, FloatLessEqual.class);
1052  private static NISuppressor arg1_le_arg2 =
1053      new NISuppressor(0, 1, FloatLessEqual.class);
1054  private static NISuppressor arg2_le_arg1 =
1055      new NISuppressor(1, 0, FloatLessEqual.class);
1056
1057  private static NISuppressor result_track0_arg1 =
1058      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
1059  private static NISuppressor result_track0_arg2 =
1060      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
1061  private static NISuppressor arg1_track0_arg2 =
1062      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
1063  private static NISuppressor arg1_track0_result =
1064      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
1065  private static NISuppressor arg2_track0_result =
1066      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
1067  private static NISuppressor arg2_track0_arg1 =
1068      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
1069
1070  private static NISuppressor result_eq_1 =
1071      new NISuppressor(2, RangeFloat.EqualOne.class);
1072  private static NISuppressor arg1_eq_1 =
1073      new NISuppressor(0, RangeFloat.EqualOne.class);
1074  private static NISuppressor arg2_eq_1 =
1075      new NISuppressor(1, RangeFloat.EqualOne.class);
1076
1077  private static NISuppressor result_eq_0 =
1078      new NISuppressor(2, RangeFloat.EqualZero.class);
1079  private static NISuppressor arg1_eq_0 =
1080      new NISuppressor(0, RangeFloat.EqualZero.class);
1081  private static NISuppressor arg2_eq_0 =
1082      new NISuppressor(1, RangeFloat.EqualZero.class);
1083
1084  private static NISuppressor result_ne_0 =
1085      new NISuppressor(2, NonZeroFloat.class);
1086  private static NISuppressor arg1_ne_0 =
1087      new NISuppressor(0, NonZeroFloat.class);
1088  private static NISuppressor arg2_ne_0 =
1089      new NISuppressor(1, NonZeroFloat.class);
1090
1091  private static NISuppressor result_ge_0 =
1092      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
1093  private static NISuppressor arg1_ge_0 =
1094      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
1095  private static NISuppressor arg2_ge_0 =
1096      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
1097
1098  private static NISuppressor result_ge_64 =
1099      new NISuppressor(2, RangeInt.GreaterEqual64.class);
1100  private static NISuppressor arg1_ge_64 =
1101      new NISuppressor(0, RangeInt.GreaterEqual64.class);
1102  private static NISuppressor arg2_ge_64 =
1103      new NISuppressor(1, RangeInt.GreaterEqual64.class);
1104
1105    private static NISuppressionSet suppressions =
1106      new NISuppressionSet(
1107          new NISuppression[] {
1108
1109            // (r == 0) && (x == 0) ==> r = x * y
1110            new NISuppression(result_eq_0, arg1_eq_0, suppressee),
1111
1112            // (r == 0) && (y == 0) ==> r = x * y
1113            new NISuppression(result_eq_0, arg2_eq_0, suppressee),
1114
1115            // (r == x) && (y == 1) ==> r = x * y
1116            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
1117
1118            // (r == y) && (x == 1) ==> r = x * y
1119            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),
1120
1121          });
1122
1123  // Create a suppression factory for functionBinary
1124
1125}
1126
1127  // #define EQUALITY_MIN_MAX_SUPPRESS
1128
1129  // default is that it is not this function, overriden in the subclass
1130  @Pure
1131  public boolean isMinimum() {
1132    return false;
1133  }
1134
1135/**
1136 * Represents the invariant {@code x = Minimum(y, z)} over three double
1137 * scalars. 
1138 */
1139public static class MinimumDouble_xyz extends FunctionBinaryFloat {
1140  // We are Serializable, so we specify a version to allow changes to
1141  // method signatures without breaking serialization.  If you add or
1142  // remove fields, you should change this number to the current date.
1143  static final long serialVersionUID = 20031030L;
1144
1145  private static @Prototype MinimumDouble_xyz proto = new @Prototype MinimumDouble_xyz ();
1146
1147  /** Returns the prototype invariant for MinimumDouble_xyz */
1148  public static @Prototype MinimumDouble_xyz get_proto() {
1149    return proto;
1150  }
1151
1152  /** instantiate an invariant on the specified slice */
1153  @Override
1154  protected MinimumDouble_xyz instantiate_dyn(@Prototype MinimumDouble_xyz this, PptSlice slice) {
1155    return new MinimumDouble_xyz (slice);
1156  }
1157
1158  private MinimumDouble_xyz (PptSlice slice) {
1159    super(slice);
1160  }
1161
1162  public @Prototype MinimumDouble_xyz () {
1163    super();
1164  }
1165
1166  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};
1167
1168  @Override
1169  public String[] get_method_name(@GuardSatisfied MinimumDouble_xyz this) {
1170    return method_name;
1171  }
1172
1173  private static int function_id = -1;
1174
1175  @Override
1176  public int get_function_id() {
1177    return function_id;
1178  }
1179
1180  @Override
1181  public void set_function_id(int function_id) {
1182    assert MinimumDouble_xyz.function_id == -1;
1183    MinimumDouble_xyz.function_id = function_id;
1184  }
1185
1186  private static int var_order = 1;
1187
1188  @Override
1189  public int get_var_order(@GuardSatisfied MinimumDouble_xyz this) {
1190    return var_order;
1191  }
1192
1193  @Pure
1194  @Override
1195  public boolean is_symmetric() {
1196
1197      return true;
1198  }
1199
1200  @Override
1201
1202  public double func(double y, double z) {
1203
1204    return Math.min(y, z);
1205  }
1206
1207  @Override
1208  public InvariantStatus check_modified(double x, double y,
1209                                      double z, int count) {
1210    return check_ordered(x, y, z, count);
1211  }
1212
1213  @Override
1214  public InvariantStatus add_modified(double x, double y,
1215                                      double z, int count) {
1216    if (Debug.logDetail()) {
1217      log("result=%s, arg1=%s, arg2=%s", x, y, z);
1218    }
1219    return add_ordered(x, y, z, count);
1220  }
1221
1222  @Pure
1223  @Override
1224  public boolean isMinimum() {
1225    return true;
1226  }
1227
1228  /** Returns a list of non-instantiating suppressions for this invariant. */
1229  @Pure
1230  @Override
1231  public @Nullable NISuppressionSet get_ni_suppressions() {
1232    if (NIS.dkconfig_enabled && dkconfig_enabled) {
1233      return suppressions;
1234    } else {
1235      return null;
1236    }
1237  }
1238
1239  /** definition of this invariant (the suppressee) */
1240  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_xyz.class, 3);
1241
1242  // suppressor definitions (used below)
1243  private static NISuppressor result_eq_arg1 =
1244      new NISuppressor(0, 1, FloatEqual.class);
1245  private static NISuppressor result_eq_arg2 =
1246      new NISuppressor(0, 2, FloatEqual.class);
1247  private static NISuppressor arg1_eq_arg2 =
1248      new NISuppressor(1, 2, FloatEqual.class);
1249
1250  private static NISuppressor result_lt_arg1 =
1251      new NISuppressor(0, 1, FloatLessThan.class);
1252  private static NISuppressor result_lt_arg2 =
1253      new NISuppressor(0, 2, FloatLessThan.class);
1254  private static NISuppressor arg1_lt_arg2 =
1255      new NISuppressor(1, 2, FloatLessThan.class);
1256  private static NISuppressor arg2_lt_arg1 =
1257      new NISuppressor(2, 1, FloatLessThan.class);
1258
1259  private static NISuppressor result_le_arg1 =
1260      new NISuppressor(0, 1, FloatLessEqual.class);
1261  private static NISuppressor result_le_arg2 =
1262      new NISuppressor(0, 2, FloatLessEqual.class);
1263  private static NISuppressor arg1_le_arg2 =
1264      new NISuppressor(1, 2, FloatLessEqual.class);
1265  private static NISuppressor arg2_le_arg1 =
1266      new NISuppressor(2, 1, FloatLessEqual.class);
1267
1268  private static NISuppressor result_track0_arg1 =
1269      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
1270  private static NISuppressor result_track0_arg2 =
1271      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
1272  private static NISuppressor arg1_track0_arg2 =
1273      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
1274  private static NISuppressor arg1_track0_result =
1275      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
1276  private static NISuppressor arg2_track0_result =
1277      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
1278  private static NISuppressor arg2_track0_arg1 =
1279      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
1280
1281  private static NISuppressor result_eq_1 =
1282      new NISuppressor(0, RangeFloat.EqualOne.class);
1283  private static NISuppressor arg1_eq_1 =
1284      new NISuppressor(1, RangeFloat.EqualOne.class);
1285  private static NISuppressor arg2_eq_1 =
1286      new NISuppressor(2, RangeFloat.EqualOne.class);
1287
1288  private static NISuppressor result_eq_0 =
1289      new NISuppressor(0, RangeFloat.EqualZero.class);
1290  private static NISuppressor arg1_eq_0 =
1291      new NISuppressor(1, RangeFloat.EqualZero.class);
1292  private static NISuppressor arg2_eq_0 =
1293      new NISuppressor(2, RangeFloat.EqualZero.class);
1294
1295  private static NISuppressor result_ne_0 =
1296      new NISuppressor(0, NonZeroFloat.class);
1297  private static NISuppressor arg1_ne_0 =
1298      new NISuppressor(1, NonZeroFloat.class);
1299  private static NISuppressor arg2_ne_0 =
1300      new NISuppressor(2, NonZeroFloat.class);
1301
1302  private static NISuppressor result_ge_0 =
1303      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
1304  private static NISuppressor arg1_ge_0 =
1305      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
1306  private static NISuppressor arg2_ge_0 =
1307      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
1308
1309  private static NISuppressor result_ge_64 =
1310      new NISuppressor(0, RangeInt.GreaterEqual64.class);
1311  private static NISuppressor arg1_ge_64 =
1312      new NISuppressor(1, RangeInt.GreaterEqual64.class);
1313  private static NISuppressor arg2_ge_64 =
1314      new NISuppressor(2, RangeInt.GreaterEqual64.class);
1315
1316    private static NISuppressionSet suppressions =
1317      new NISuppressionSet(
1318          new NISuppression[] {
1319
1320            // (x == y) && (y <= z) ==> r = min(y, z)
1321            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),
1322
1323            // (x == z) && (z <= y) ==> r = min(y, z)
1324            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),
1325
1326          });
1327
1328  // Create a suppression factory for functionBinary
1329
1330}
1331
1332/**
1333 * Represents the invariant {@code y = Minimum(x, z)} over three double
1334 * scalars. 
1335 */
1336public static class MinimumDouble_yxz extends FunctionBinaryFloat {
1337  // We are Serializable, so we specify a version to allow changes to
1338  // method signatures without breaking serialization.  If you add or
1339  // remove fields, you should change this number to the current date.
1340  static final long serialVersionUID = 20031030L;
1341
1342  private static @Prototype MinimumDouble_yxz proto = new @Prototype MinimumDouble_yxz ();
1343
1344  /** Returns the prototype invariant for MinimumDouble_yxz */
1345  public static @Prototype MinimumDouble_yxz get_proto() {
1346    return proto;
1347  }
1348
1349  /** instantiate an invariant on the specified slice */
1350  @Override
1351  protected MinimumDouble_yxz instantiate_dyn(@Prototype MinimumDouble_yxz this, PptSlice slice) {
1352    return new MinimumDouble_yxz (slice);
1353  }
1354
1355  private MinimumDouble_yxz (PptSlice slice) {
1356    super(slice);
1357  }
1358
1359  public @Prototype MinimumDouble_yxz () {
1360    super();
1361  }
1362
1363  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};
1364
1365  @Override
1366  public String[] get_method_name(@GuardSatisfied MinimumDouble_yxz this) {
1367    return method_name;
1368  }
1369
1370  private static int function_id = -1;
1371
1372  @Override
1373  public int get_function_id() {
1374    return function_id;
1375  }
1376
1377  @Override
1378  public void set_function_id(int function_id) {
1379    assert MinimumDouble_yxz.function_id == -1;
1380    MinimumDouble_yxz.function_id = function_id;
1381  }
1382
1383  private static int var_order = 2;
1384
1385  @Override
1386  public int get_var_order(@GuardSatisfied MinimumDouble_yxz this) {
1387    return var_order;
1388  }
1389
1390  @Pure
1391  @Override
1392  public boolean is_symmetric() {
1393
1394      return true;
1395  }
1396
1397  @Override
1398
1399  public double func(double x, double z) {
1400
1401    return Math.min(x, z);
1402  }
1403
1404  @Override
1405  public InvariantStatus check_modified(double x, double y,
1406                                      double z, int count) {
1407    return check_ordered(y, x, z, count);
1408  }
1409
1410  @Override
1411  public InvariantStatus add_modified(double x, double y,
1412                                      double z, int count) {
1413    if (Debug.logDetail()) {
1414      log("result=%s, arg1=%s, arg2=%s", y, x, z);
1415    }
1416    return add_ordered(y, x, z, count);
1417  }
1418
1419  @Pure
1420  @Override
1421  public boolean isMinimum() {
1422    return true;
1423  }
1424
1425  /** Returns a list of non-instantiating suppressions for this invariant. */
1426  @Pure
1427  @Override
1428  public @Nullable NISuppressionSet get_ni_suppressions() {
1429    if (NIS.dkconfig_enabled && dkconfig_enabled) {
1430      return suppressions;
1431    } else {
1432      return null;
1433    }
1434  }
1435
1436  /** definition of this invariant (the suppressee) */
1437  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_yxz.class, 3);
1438
1439  // suppressor definitions (used below)
1440  private static NISuppressor result_eq_arg1 =
1441      new NISuppressor(1, 0, FloatEqual.class);
1442  private static NISuppressor result_eq_arg2 =
1443      new NISuppressor(1, 2, FloatEqual.class);
1444  private static NISuppressor arg1_eq_arg2 =
1445      new NISuppressor(0, 2, FloatEqual.class);
1446
1447  private static NISuppressor result_lt_arg1 =
1448      new NISuppressor(1, 0, FloatLessThan.class);
1449  private static NISuppressor result_lt_arg2 =
1450      new NISuppressor(1, 2, FloatLessThan.class);
1451  private static NISuppressor arg1_lt_arg2 =
1452      new NISuppressor(0, 2, FloatLessThan.class);
1453  private static NISuppressor arg2_lt_arg1 =
1454      new NISuppressor(2, 0, FloatLessThan.class);
1455
1456  private static NISuppressor result_le_arg1 =
1457      new NISuppressor(1, 0, FloatLessEqual.class);
1458  private static NISuppressor result_le_arg2 =
1459      new NISuppressor(1, 2, FloatLessEqual.class);
1460  private static NISuppressor arg1_le_arg2 =
1461      new NISuppressor(0, 2, FloatLessEqual.class);
1462  private static NISuppressor arg2_le_arg1 =
1463      new NISuppressor(2, 0, FloatLessEqual.class);
1464
1465  private static NISuppressor result_track0_arg1 =
1466      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
1467  private static NISuppressor result_track0_arg2 =
1468      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
1469  private static NISuppressor arg1_track0_arg2 =
1470      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
1471  private static NISuppressor arg1_track0_result =
1472      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
1473  private static NISuppressor arg2_track0_result =
1474      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
1475  private static NISuppressor arg2_track0_arg1 =
1476      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
1477
1478  private static NISuppressor result_eq_1 =
1479      new NISuppressor(1, RangeFloat.EqualOne.class);
1480  private static NISuppressor arg1_eq_1 =
1481      new NISuppressor(0, RangeFloat.EqualOne.class);
1482  private static NISuppressor arg2_eq_1 =
1483      new NISuppressor(2, RangeFloat.EqualOne.class);
1484
1485  private static NISuppressor result_eq_0 =
1486      new NISuppressor(1, RangeFloat.EqualZero.class);
1487  private static NISuppressor arg1_eq_0 =
1488      new NISuppressor(0, RangeFloat.EqualZero.class);
1489  private static NISuppressor arg2_eq_0 =
1490      new NISuppressor(2, RangeFloat.EqualZero.class);
1491
1492  private static NISuppressor result_ne_0 =
1493      new NISuppressor(1, NonZeroFloat.class);
1494  private static NISuppressor arg1_ne_0 =
1495      new NISuppressor(0, NonZeroFloat.class);
1496  private static NISuppressor arg2_ne_0 =
1497      new NISuppressor(2, NonZeroFloat.class);
1498
1499  private static NISuppressor result_ge_0 =
1500      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
1501  private static NISuppressor arg1_ge_0 =
1502      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
1503  private static NISuppressor arg2_ge_0 =
1504      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
1505
1506  private static NISuppressor result_ge_64 =
1507      new NISuppressor(1, RangeInt.GreaterEqual64.class);
1508  private static NISuppressor arg1_ge_64 =
1509      new NISuppressor(0, RangeInt.GreaterEqual64.class);
1510  private static NISuppressor arg2_ge_64 =
1511      new NISuppressor(2, RangeInt.GreaterEqual64.class);
1512
1513    private static NISuppressionSet suppressions =
1514      new NISuppressionSet(
1515          new NISuppression[] {
1516
1517            // (y == x) && (x <= z) ==> r = min(x, z)
1518            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),
1519
1520            // (y == z) && (z <= x) ==> r = min(x, z)
1521            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),
1522
1523          });
1524
1525  // Create a suppression factory for functionBinary
1526
1527}
1528
1529/**
1530 * Represents the invariant {@code z = Minimum(x, y)} over three double
1531 * scalars. 
1532 */
1533public static class MinimumDouble_zxy extends FunctionBinaryFloat {
1534  // We are Serializable, so we specify a version to allow changes to
1535  // method signatures without breaking serialization.  If you add or
1536  // remove fields, you should change this number to the current date.
1537  static final long serialVersionUID = 20031030L;
1538
1539  private static @Prototype MinimumDouble_zxy proto = new @Prototype MinimumDouble_zxy ();
1540
1541  /** Returns the prototype invariant for MinimumDouble_zxy */
1542  public static @Prototype MinimumDouble_zxy get_proto() {
1543    return proto;
1544  }
1545
1546  /** instantiate an invariant on the specified slice */
1547  @Override
1548  protected MinimumDouble_zxy instantiate_dyn(@Prototype MinimumDouble_zxy this, PptSlice slice) {
1549    return new MinimumDouble_zxy (slice);
1550  }
1551
1552  private MinimumDouble_zxy (PptSlice slice) {
1553    super(slice);
1554  }
1555
1556  public @Prototype MinimumDouble_zxy () {
1557    super();
1558  }
1559
1560  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};
1561
1562  @Override
1563  public String[] get_method_name(@GuardSatisfied MinimumDouble_zxy this) {
1564    return method_name;
1565  }
1566
1567  private static int function_id = -1;
1568
1569  @Override
1570  public int get_function_id() {
1571    return function_id;
1572  }
1573
1574  @Override
1575  public void set_function_id(int function_id) {
1576    assert MinimumDouble_zxy.function_id == -1;
1577    MinimumDouble_zxy.function_id = function_id;
1578  }
1579
1580  private static int var_order = 3;
1581
1582  @Override
1583  public int get_var_order(@GuardSatisfied MinimumDouble_zxy this) {
1584    return var_order;
1585  }
1586
1587  @Pure
1588  @Override
1589  public boolean is_symmetric() {
1590
1591      return true;
1592  }
1593
1594  @Override
1595
1596  public double func(double x, double y) {
1597
1598    return Math.min(x, y);
1599  }
1600
1601  @Override
1602  public InvariantStatus check_modified(double x, double y,
1603                                      double z, int count) {
1604    return check_ordered(z, x, y, count);
1605  }
1606
1607  @Override
1608  public InvariantStatus add_modified(double x, double y,
1609                                      double z, int count) {
1610    if (Debug.logDetail()) {
1611      log("result=%s, arg1=%s, arg2=%s", z, x, y);
1612    }
1613    return add_ordered(z, x, y, count);
1614  }
1615
1616  @Pure
1617  @Override
1618  public boolean isMinimum() {
1619    return true;
1620  }
1621
1622  /** Returns a list of non-instantiating suppressions for this invariant. */
1623  @Pure
1624  @Override
1625  public @Nullable NISuppressionSet get_ni_suppressions() {
1626    if (NIS.dkconfig_enabled && dkconfig_enabled) {
1627      return suppressions;
1628    } else {
1629      return null;
1630    }
1631  }
1632
1633  /** definition of this invariant (the suppressee) */
1634  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_zxy.class, 3);
1635
1636  // suppressor definitions (used below)
1637  private static NISuppressor result_eq_arg1 =
1638      new NISuppressor(2, 0, FloatEqual.class);
1639  private static NISuppressor result_eq_arg2 =
1640      new NISuppressor(2, 1, FloatEqual.class);
1641  private static NISuppressor arg1_eq_arg2 =
1642      new NISuppressor(0, 1, FloatEqual.class);
1643
1644  private static NISuppressor result_lt_arg1 =
1645      new NISuppressor(2, 0, FloatLessThan.class);
1646  private static NISuppressor result_lt_arg2 =
1647      new NISuppressor(2, 1, FloatLessThan.class);
1648  private static NISuppressor arg1_lt_arg2 =
1649      new NISuppressor(0, 1, FloatLessThan.class);
1650  private static NISuppressor arg2_lt_arg1 =
1651      new NISuppressor(1, 0, FloatLessThan.class);
1652
1653  private static NISuppressor result_le_arg1 =
1654      new NISuppressor(2, 0, FloatLessEqual.class);
1655  private static NISuppressor result_le_arg2 =
1656      new NISuppressor(2, 1, FloatLessEqual.class);
1657  private static NISuppressor arg1_le_arg2 =
1658      new NISuppressor(0, 1, FloatLessEqual.class);
1659  private static NISuppressor arg2_le_arg1 =
1660      new NISuppressor(1, 0, FloatLessEqual.class);
1661
1662  private static NISuppressor result_track0_arg1 =
1663      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
1664  private static NISuppressor result_track0_arg2 =
1665      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
1666  private static NISuppressor arg1_track0_arg2 =
1667      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
1668  private static NISuppressor arg1_track0_result =
1669      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
1670  private static NISuppressor arg2_track0_result =
1671      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
1672  private static NISuppressor arg2_track0_arg1 =
1673      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
1674
1675  private static NISuppressor result_eq_1 =
1676      new NISuppressor(2, RangeFloat.EqualOne.class);
1677  private static NISuppressor arg1_eq_1 =
1678      new NISuppressor(0, RangeFloat.EqualOne.class);
1679  private static NISuppressor arg2_eq_1 =
1680      new NISuppressor(1, RangeFloat.EqualOne.class);
1681
1682  private static NISuppressor result_eq_0 =
1683      new NISuppressor(2, RangeFloat.EqualZero.class);
1684  private static NISuppressor arg1_eq_0 =
1685      new NISuppressor(0, RangeFloat.EqualZero.class);
1686  private static NISuppressor arg2_eq_0 =
1687      new NISuppressor(1, RangeFloat.EqualZero.class);
1688
1689  private static NISuppressor result_ne_0 =
1690      new NISuppressor(2, NonZeroFloat.class);
1691  private static NISuppressor arg1_ne_0 =
1692      new NISuppressor(0, NonZeroFloat.class);
1693  private static NISuppressor arg2_ne_0 =
1694      new NISuppressor(1, NonZeroFloat.class);
1695
1696  private static NISuppressor result_ge_0 =
1697      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
1698  private static NISuppressor arg1_ge_0 =
1699      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
1700  private static NISuppressor arg2_ge_0 =
1701      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
1702
1703  private static NISuppressor result_ge_64 =
1704      new NISuppressor(2, RangeInt.GreaterEqual64.class);
1705  private static NISuppressor arg1_ge_64 =
1706      new NISuppressor(0, RangeInt.GreaterEqual64.class);
1707  private static NISuppressor arg2_ge_64 =
1708      new NISuppressor(1, RangeInt.GreaterEqual64.class);
1709
1710    private static NISuppressionSet suppressions =
1711      new NISuppressionSet(
1712          new NISuppression[] {
1713
1714            // (z == x) && (x <= y) ==> r = min(x, y)
1715            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),
1716
1717            // (z == y) && (y <= x) ==> r = min(x, y)
1718            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),
1719
1720          });
1721
1722  // Create a suppression factory for functionBinary
1723
1724}
1725
1726  // #define EQUALITY_MIN_MAX_SUPPRESS
1727
1728  // default is that it is not this function, overriden in the subclass
1729  @Pure
1730  public boolean isMaximum() {
1731    return false;
1732  }
1733
1734/**
1735 * Represents the invariant {@code x = Maximum(y, z)} over three double
1736 * scalars. 
1737 */
1738public static class MaximumDouble_xyz extends FunctionBinaryFloat {
1739  // We are Serializable, so we specify a version to allow changes to
1740  // method signatures without breaking serialization.  If you add or
1741  // remove fields, you should change this number to the current date.
1742  static final long serialVersionUID = 20031030L;
1743
1744  private static @Prototype MaximumDouble_xyz proto = new @Prototype MaximumDouble_xyz ();
1745
1746  /** Returns the prototype invariant for MaximumDouble_xyz */
1747  public static @Prototype MaximumDouble_xyz get_proto() {
1748    return proto;
1749  }
1750
1751  /** instantiate an invariant on the specified slice */
1752  @Override
1753  protected MaximumDouble_xyz instantiate_dyn(@Prototype MaximumDouble_xyz this, PptSlice slice) {
1754    return new MaximumDouble_xyz (slice);
1755  }
1756
1757  private MaximumDouble_xyz (PptSlice slice) {
1758    super(slice);
1759  }
1760
1761  public @Prototype MaximumDouble_xyz () {
1762    super();
1763  }
1764
1765  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};
1766
1767  @Override
1768  public String[] get_method_name(@GuardSatisfied MaximumDouble_xyz this) {
1769    return method_name;
1770  }
1771
1772  private static int function_id = -1;
1773
1774  @Override
1775  public int get_function_id() {
1776    return function_id;
1777  }
1778
1779  @Override
1780  public void set_function_id(int function_id) {
1781    assert MaximumDouble_xyz.function_id == -1;
1782    MaximumDouble_xyz.function_id = function_id;
1783  }
1784
1785  private static int var_order = 1;
1786
1787  @Override
1788  public int get_var_order(@GuardSatisfied MaximumDouble_xyz this) {
1789    return var_order;
1790  }
1791
1792  @Pure
1793  @Override
1794  public boolean is_symmetric() {
1795
1796      return true;
1797  }
1798
1799  @Override
1800
1801  public double func(double y, double z) {
1802
1803    return Math.max(y, z);
1804  }
1805
1806  @Override
1807  public InvariantStatus check_modified(double x, double y,
1808                                      double z, int count) {
1809    return check_ordered(x, y, z, count);
1810  }
1811
1812  @Override
1813  public InvariantStatus add_modified(double x, double y,
1814                                      double z, int count) {
1815    if (Debug.logDetail()) {
1816      log("result=%s, arg1=%s, arg2=%s", x, y, z);
1817    }
1818    return add_ordered(x, y, z, count);
1819  }
1820
1821  @Pure
1822  @Override
1823  public boolean isMaximum() {
1824    return true;
1825  }
1826
1827  /** Returns a list of non-instantiating suppressions for this invariant. */
1828  @Pure
1829  @Override
1830  public @Nullable NISuppressionSet get_ni_suppressions() {
1831    if (NIS.dkconfig_enabled && dkconfig_enabled) {
1832      return suppressions;
1833    } else {
1834      return null;
1835    }
1836  }
1837
1838  /** definition of this invariant (the suppressee) */
1839  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_xyz.class, 3);
1840
1841  // suppressor definitions (used below)
1842  private static NISuppressor result_eq_arg1 =
1843      new NISuppressor(0, 1, FloatEqual.class);
1844  private static NISuppressor result_eq_arg2 =
1845      new NISuppressor(0, 2, FloatEqual.class);
1846  private static NISuppressor arg1_eq_arg2 =
1847      new NISuppressor(1, 2, FloatEqual.class);
1848
1849  private static NISuppressor result_lt_arg1 =
1850      new NISuppressor(0, 1, FloatLessThan.class);
1851  private static NISuppressor result_lt_arg2 =
1852      new NISuppressor(0, 2, FloatLessThan.class);
1853  private static NISuppressor arg1_lt_arg2 =
1854      new NISuppressor(1, 2, FloatLessThan.class);
1855  private static NISuppressor arg2_lt_arg1 =
1856      new NISuppressor(2, 1, FloatLessThan.class);
1857
1858  private static NISuppressor result_le_arg1 =
1859      new NISuppressor(0, 1, FloatLessEqual.class);
1860  private static NISuppressor result_le_arg2 =
1861      new NISuppressor(0, 2, FloatLessEqual.class);
1862  private static NISuppressor arg1_le_arg2 =
1863      new NISuppressor(1, 2, FloatLessEqual.class);
1864  private static NISuppressor arg2_le_arg1 =
1865      new NISuppressor(2, 1, FloatLessEqual.class);
1866
1867  private static NISuppressor result_track0_arg1 =
1868      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
1869  private static NISuppressor result_track0_arg2 =
1870      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
1871  private static NISuppressor arg1_track0_arg2 =
1872      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
1873  private static NISuppressor arg1_track0_result =
1874      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
1875  private static NISuppressor arg2_track0_result =
1876      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
1877  private static NISuppressor arg2_track0_arg1 =
1878      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
1879
1880  private static NISuppressor result_eq_1 =
1881      new NISuppressor(0, RangeFloat.EqualOne.class);
1882  private static NISuppressor arg1_eq_1 =
1883      new NISuppressor(1, RangeFloat.EqualOne.class);
1884  private static NISuppressor arg2_eq_1 =
1885      new NISuppressor(2, RangeFloat.EqualOne.class);
1886
1887  private static NISuppressor result_eq_0 =
1888      new NISuppressor(0, RangeFloat.EqualZero.class);
1889  private static NISuppressor arg1_eq_0 =
1890      new NISuppressor(1, RangeFloat.EqualZero.class);
1891  private static NISuppressor arg2_eq_0 =
1892      new NISuppressor(2, RangeFloat.EqualZero.class);
1893
1894  private static NISuppressor result_ne_0 =
1895      new NISuppressor(0, NonZeroFloat.class);
1896  private static NISuppressor arg1_ne_0 =
1897      new NISuppressor(1, NonZeroFloat.class);
1898  private static NISuppressor arg2_ne_0 =
1899      new NISuppressor(2, NonZeroFloat.class);
1900
1901  private static NISuppressor result_ge_0 =
1902      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
1903  private static NISuppressor arg1_ge_0 =
1904      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
1905  private static NISuppressor arg2_ge_0 =
1906      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
1907
1908  private static NISuppressor result_ge_64 =
1909      new NISuppressor(0, RangeInt.GreaterEqual64.class);
1910  private static NISuppressor arg1_ge_64 =
1911      new NISuppressor(1, RangeInt.GreaterEqual64.class);
1912  private static NISuppressor arg2_ge_64 =
1913      new NISuppressor(2, RangeInt.GreaterEqual64.class);
1914
1915    private static NISuppressionSet suppressions =
1916      new NISuppressionSet(
1917          new NISuppression[] {
1918
1919            // (r == y) && (z <= y) ==> r = max(y, z)
1920            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),
1921
1922            // (r == z) && (y <= z) ==> r = max(y, z)
1923            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),
1924
1925          });
1926
1927  // Create a suppression factory for functionBinary
1928
1929}
1930
1931/**
1932 * Represents the invariant {@code y = Maximum(x, z)} over three double
1933 * scalars. 
1934 */
1935public static class MaximumDouble_yxz extends FunctionBinaryFloat {
1936  // We are Serializable, so we specify a version to allow changes to
1937  // method signatures without breaking serialization.  If you add or
1938  // remove fields, you should change this number to the current date.
1939  static final long serialVersionUID = 20031030L;
1940
1941  private static @Prototype MaximumDouble_yxz proto = new @Prototype MaximumDouble_yxz ();
1942
1943  /** Returns the prototype invariant for MaximumDouble_yxz */
1944  public static @Prototype MaximumDouble_yxz get_proto() {
1945    return proto;
1946  }
1947
1948  /** instantiate an invariant on the specified slice */
1949  @Override
1950  protected MaximumDouble_yxz instantiate_dyn(@Prototype MaximumDouble_yxz this, PptSlice slice) {
1951    return new MaximumDouble_yxz (slice);
1952  }
1953
1954  private MaximumDouble_yxz (PptSlice slice) {
1955    super(slice);
1956  }
1957
1958  public @Prototype MaximumDouble_yxz () {
1959    super();
1960  }
1961
1962  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};
1963
1964  @Override
1965  public String[] get_method_name(@GuardSatisfied MaximumDouble_yxz this) {
1966    return method_name;
1967  }
1968
1969  private static int function_id = -1;
1970
1971  @Override
1972  public int get_function_id() {
1973    return function_id;
1974  }
1975
1976  @Override
1977  public void set_function_id(int function_id) {
1978    assert MaximumDouble_yxz.function_id == -1;
1979    MaximumDouble_yxz.function_id = function_id;
1980  }
1981
1982  private static int var_order = 2;
1983
1984  @Override
1985  public int get_var_order(@GuardSatisfied MaximumDouble_yxz this) {
1986    return var_order;
1987  }
1988
1989  @Pure
1990  @Override
1991  public boolean is_symmetric() {
1992
1993      return true;
1994  }
1995
1996  @Override
1997
1998  public double func(double x, double z) {
1999
2000    return Math.max(x, z);
2001  }
2002
2003  @Override
2004  public InvariantStatus check_modified(double x, double y,
2005                                      double z, int count) {
2006    return check_ordered(y, x, z, count);
2007  }
2008
2009  @Override
2010  public InvariantStatus add_modified(double x, double y,
2011                                      double z, int count) {
2012    if (Debug.logDetail()) {
2013      log("result=%s, arg1=%s, arg2=%s", y, x, z);
2014    }
2015    return add_ordered(y, x, z, count);
2016  }
2017
2018  @Pure
2019  @Override
2020  public boolean isMaximum() {
2021    return true;
2022  }
2023
2024  /** Returns a list of non-instantiating suppressions for this invariant. */
2025  @Pure
2026  @Override
2027  public @Nullable NISuppressionSet get_ni_suppressions() {
2028    if (NIS.dkconfig_enabled && dkconfig_enabled) {
2029      return suppressions;
2030    } else {
2031      return null;
2032    }
2033  }
2034
2035  /** definition of this invariant (the suppressee) */
2036  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_yxz.class, 3);
2037
2038  // suppressor definitions (used below)
2039  private static NISuppressor result_eq_arg1 =
2040      new NISuppressor(1, 0, FloatEqual.class);
2041  private static NISuppressor result_eq_arg2 =
2042      new NISuppressor(1, 2, FloatEqual.class);
2043  private static NISuppressor arg1_eq_arg2 =
2044      new NISuppressor(0, 2, FloatEqual.class);
2045
2046  private static NISuppressor result_lt_arg1 =
2047      new NISuppressor(1, 0, FloatLessThan.class);
2048  private static NISuppressor result_lt_arg2 =
2049      new NISuppressor(1, 2, FloatLessThan.class);
2050  private static NISuppressor arg1_lt_arg2 =
2051      new NISuppressor(0, 2, FloatLessThan.class);
2052  private static NISuppressor arg2_lt_arg1 =
2053      new NISuppressor(2, 0, FloatLessThan.class);
2054
2055  private static NISuppressor result_le_arg1 =
2056      new NISuppressor(1, 0, FloatLessEqual.class);
2057  private static NISuppressor result_le_arg2 =
2058      new NISuppressor(1, 2, FloatLessEqual.class);
2059  private static NISuppressor arg1_le_arg2 =
2060      new NISuppressor(0, 2, FloatLessEqual.class);
2061  private static NISuppressor arg2_le_arg1 =
2062      new NISuppressor(2, 0, FloatLessEqual.class);
2063
2064  private static NISuppressor result_track0_arg1 =
2065      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
2066  private static NISuppressor result_track0_arg2 =
2067      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
2068  private static NISuppressor arg1_track0_arg2 =
2069      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
2070  private static NISuppressor arg1_track0_result =
2071      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
2072  private static NISuppressor arg2_track0_result =
2073      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
2074  private static NISuppressor arg2_track0_arg1 =
2075      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
2076
2077  private static NISuppressor result_eq_1 =
2078      new NISuppressor(1, RangeFloat.EqualOne.class);
2079  private static NISuppressor arg1_eq_1 =
2080      new NISuppressor(0, RangeFloat.EqualOne.class);
2081  private static NISuppressor arg2_eq_1 =
2082      new NISuppressor(2, RangeFloat.EqualOne.class);
2083
2084  private static NISuppressor result_eq_0 =
2085      new NISuppressor(1, RangeFloat.EqualZero.class);
2086  private static NISuppressor arg1_eq_0 =
2087      new NISuppressor(0, RangeFloat.EqualZero.class);
2088  private static NISuppressor arg2_eq_0 =
2089      new NISuppressor(2, RangeFloat.EqualZero.class);
2090
2091  private static NISuppressor result_ne_0 =
2092      new NISuppressor(1, NonZeroFloat.class);
2093  private static NISuppressor arg1_ne_0 =
2094      new NISuppressor(0, NonZeroFloat.class);
2095  private static NISuppressor arg2_ne_0 =
2096      new NISuppressor(2, NonZeroFloat.class);
2097
2098  private static NISuppressor result_ge_0 =
2099      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
2100  private static NISuppressor arg1_ge_0 =
2101      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
2102  private static NISuppressor arg2_ge_0 =
2103      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
2104
2105  private static NISuppressor result_ge_64 =
2106      new NISuppressor(1, RangeInt.GreaterEqual64.class);
2107  private static NISuppressor arg1_ge_64 =
2108      new NISuppressor(0, RangeInt.GreaterEqual64.class);
2109  private static NISuppressor arg2_ge_64 =
2110      new NISuppressor(2, RangeInt.GreaterEqual64.class);
2111
2112    private static NISuppressionSet suppressions =
2113      new NISuppressionSet(
2114          new NISuppression[] {
2115
2116            // (r == x) && (z <= x) ==> r = max(x, z)
2117            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),
2118
2119            // (r == z) && (x <= z) ==> r = max(x, z)
2120            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),
2121
2122          });
2123
2124  // Create a suppression factory for functionBinary
2125
2126}
2127
2128/**
2129 * Represents the invariant {@code z = Maximum(x, y)} over three double
2130 * scalars. 
2131 */
2132public static class MaximumDouble_zxy extends FunctionBinaryFloat {
2133  // We are Serializable, so we specify a version to allow changes to
2134  // method signatures without breaking serialization.  If you add or
2135  // remove fields, you should change this number to the current date.
2136  static final long serialVersionUID = 20031030L;
2137
2138  private static @Prototype MaximumDouble_zxy proto = new @Prototype MaximumDouble_zxy ();
2139
2140  /** Returns the prototype invariant for MaximumDouble_zxy */
2141  public static @Prototype MaximumDouble_zxy get_proto() {
2142    return proto;
2143  }
2144
2145  /** instantiate an invariant on the specified slice */
2146  @Override
2147  protected MaximumDouble_zxy instantiate_dyn(@Prototype MaximumDouble_zxy this, PptSlice slice) {
2148    return new MaximumDouble_zxy (slice);
2149  }
2150
2151  private MaximumDouble_zxy (PptSlice slice) {
2152    super(slice);
2153  }
2154
2155  public @Prototype MaximumDouble_zxy () {
2156    super();
2157  }
2158
2159  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};
2160
2161  @Override
2162  public String[] get_method_name(@GuardSatisfied MaximumDouble_zxy this) {
2163    return method_name;
2164  }
2165
2166  private static int function_id = -1;
2167
2168  @Override
2169  public int get_function_id() {
2170    return function_id;
2171  }
2172
2173  @Override
2174  public void set_function_id(int function_id) {
2175    assert MaximumDouble_zxy.function_id == -1;
2176    MaximumDouble_zxy.function_id = function_id;
2177  }
2178
2179  private static int var_order = 3;
2180
2181  @Override
2182  public int get_var_order(@GuardSatisfied MaximumDouble_zxy this) {
2183    return var_order;
2184  }
2185
2186  @Pure
2187  @Override
2188  public boolean is_symmetric() {
2189
2190      return true;
2191  }
2192
2193  @Override
2194
2195  public double func(double x, double y) {
2196
2197    return Math.max(x, y);
2198  }
2199
2200  @Override
2201  public InvariantStatus check_modified(double x, double y,
2202                                      double z, int count) {
2203    return check_ordered(z, x, y, count);
2204  }
2205
2206  @Override
2207  public InvariantStatus add_modified(double x, double y,
2208                                      double z, int count) {
2209    if (Debug.logDetail()) {
2210      log("result=%s, arg1=%s, arg2=%s", z, x, y);
2211    }
2212    return add_ordered(z, x, y, count);
2213  }
2214
2215  @Pure
2216  @Override
2217  public boolean isMaximum() {
2218    return true;
2219  }
2220
2221  /** Returns a list of non-instantiating suppressions for this invariant. */
2222  @Pure
2223  @Override
2224  public @Nullable NISuppressionSet get_ni_suppressions() {
2225    if (NIS.dkconfig_enabled && dkconfig_enabled) {
2226      return suppressions;
2227    } else {
2228      return null;
2229    }
2230  }
2231
2232  /** definition of this invariant (the suppressee) */
2233  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_zxy.class, 3);
2234
2235  // suppressor definitions (used below)
2236  private static NISuppressor result_eq_arg1 =
2237      new NISuppressor(2, 0, FloatEqual.class);
2238  private static NISuppressor result_eq_arg2 =
2239      new NISuppressor(2, 1, FloatEqual.class);
2240  private static NISuppressor arg1_eq_arg2 =
2241      new NISuppressor(0, 1, FloatEqual.class);
2242
2243  private static NISuppressor result_lt_arg1 =
2244      new NISuppressor(2, 0, FloatLessThan.class);
2245  private static NISuppressor result_lt_arg2 =
2246      new NISuppressor(2, 1, FloatLessThan.class);
2247  private static NISuppressor arg1_lt_arg2 =
2248      new NISuppressor(0, 1, FloatLessThan.class);
2249  private static NISuppressor arg2_lt_arg1 =
2250      new NISuppressor(1, 0, FloatLessThan.class);
2251
2252  private static NISuppressor result_le_arg1 =
2253      new NISuppressor(2, 0, FloatLessEqual.class);
2254  private static NISuppressor result_le_arg2 =
2255      new NISuppressor(2, 1, FloatLessEqual.class);
2256  private static NISuppressor arg1_le_arg2 =
2257      new NISuppressor(0, 1, FloatLessEqual.class);
2258  private static NISuppressor arg2_le_arg1 =
2259      new NISuppressor(1, 0, FloatLessEqual.class);
2260
2261  private static NISuppressor result_track0_arg1 =
2262      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
2263  private static NISuppressor result_track0_arg2 =
2264      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
2265  private static NISuppressor arg1_track0_arg2 =
2266      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
2267  private static NISuppressor arg1_track0_result =
2268      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
2269  private static NISuppressor arg2_track0_result =
2270      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
2271  private static NISuppressor arg2_track0_arg1 =
2272      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
2273
2274  private static NISuppressor result_eq_1 =
2275      new NISuppressor(2, RangeFloat.EqualOne.class);
2276  private static NISuppressor arg1_eq_1 =
2277      new NISuppressor(0, RangeFloat.EqualOne.class);
2278  private static NISuppressor arg2_eq_1 =
2279      new NISuppressor(1, RangeFloat.EqualOne.class);
2280
2281  private static NISuppressor result_eq_0 =
2282      new NISuppressor(2, RangeFloat.EqualZero.class);
2283  private static NISuppressor arg1_eq_0 =
2284      new NISuppressor(0, RangeFloat.EqualZero.class);
2285  private static NISuppressor arg2_eq_0 =
2286      new NISuppressor(1, RangeFloat.EqualZero.class);
2287
2288  private static NISuppressor result_ne_0 =
2289      new NISuppressor(2, NonZeroFloat.class);
2290  private static NISuppressor arg1_ne_0 =
2291      new NISuppressor(0, NonZeroFloat.class);
2292  private static NISuppressor arg2_ne_0 =
2293      new NISuppressor(1, NonZeroFloat.class);
2294
2295  private static NISuppressor result_ge_0 =
2296      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
2297  private static NISuppressor arg1_ge_0 =
2298      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
2299  private static NISuppressor arg2_ge_0 =
2300      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
2301
2302  private static NISuppressor result_ge_64 =
2303      new NISuppressor(2, RangeInt.GreaterEqual64.class);
2304  private static NISuppressor arg1_ge_64 =
2305      new NISuppressor(0, RangeInt.GreaterEqual64.class);
2306  private static NISuppressor arg2_ge_64 =
2307      new NISuppressor(1, RangeInt.GreaterEqual64.class);
2308
2309    private static NISuppressionSet suppressions =
2310      new NISuppressionSet(
2311          new NISuppression[] {
2312
2313            // (r == x) && (y <= x) ==> r = max(x, y)
2314            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),
2315
2316            // (r == y) && (x <= y) ==> r = max(x, y)
2317            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),
2318
2319          });
2320
2321  // Create a suppression factory for functionBinary
2322
2323}
2324
2325  // default is that it is not this function, overriden in the subclass
2326  @Pure
2327  public boolean isDivision() {
2328    return false;
2329  }
2330
2331/**
2332 * Represents the invariant {@code x = Division(y, z)} over three double
2333 * scalars. 
2334 */
2335public static class DivisionDouble_xyz extends FunctionBinaryFloat {
2336  // We are Serializable, so we specify a version to allow changes to
2337  // method signatures without breaking serialization.  If you add or
2338  // remove fields, you should change this number to the current date.
2339  static final long serialVersionUID = 20031030L;
2340
2341  private static @Prototype DivisionDouble_xyz proto = new @Prototype DivisionDouble_xyz ();
2342
2343  /** Returns the prototype invariant for DivisionDouble_xyz */
2344  public static @Prototype DivisionDouble_xyz get_proto() {
2345    return proto;
2346  }
2347
2348  /** instantiate an invariant on the specified slice */
2349  @Override
2350  protected DivisionDouble_xyz instantiate_dyn(@Prototype DivisionDouble_xyz this, PptSlice slice) {
2351    return new DivisionDouble_xyz (slice);
2352  }
2353
2354  private DivisionDouble_xyz (PptSlice slice) {
2355    super(slice);
2356  }
2357
2358  public @Prototype DivisionDouble_xyz () {
2359    super();
2360  }
2361
2362  private static String[] method_name = new String[] {"", " / ", ""};
2363
2364  @Override
2365  public String[] get_method_name(@GuardSatisfied DivisionDouble_xyz this) {
2366    return method_name;
2367  }
2368
2369  private static int function_id = -1;
2370
2371  @Override
2372  public int get_function_id() {
2373    return function_id;
2374  }
2375
2376  @Override
2377  public void set_function_id(int function_id) {
2378    assert DivisionDouble_xyz.function_id == -1;
2379    DivisionDouble_xyz.function_id = function_id;
2380  }
2381
2382  private static int var_order = 1;
2383
2384  @Override
2385  public int get_var_order(@GuardSatisfied DivisionDouble_xyz this) {
2386    return var_order;
2387  }
2388
2389  @Pure
2390  @Override
2391  public boolean is_symmetric() {
2392
2393      return false;
2394  }
2395
2396  @Override
2397
2398  public double func(double y, double z) {
2399
2400    return (y / z);
2401  }
2402
2403  @Override
2404  public InvariantStatus check_modified(double x, double y,
2405                                      double z, int count) {
2406    return check_ordered(x, y, z, count);
2407  }
2408
2409  @Override
2410  public InvariantStatus add_modified(double x, double y,
2411                                      double z, int count) {
2412    if (Debug.logDetail()) {
2413      log("result=%s, arg1=%s, arg2=%s", x, y, z);
2414    }
2415    return add_ordered(x, y, z, count);
2416  }
2417
2418  @Pure
2419  @Override
2420  public boolean isDivision() {
2421    return true;
2422  }
2423
2424  @Pure
2425  @Override
2426  public boolean isExact() {
2427    return true;
2428  }
2429
2430  /** Returns a list of non-instantiating suppressions for this invariant. */
2431  @Pure
2432  @Override
2433  public @Nullable NISuppressionSet get_ni_suppressions() {
2434    if (NIS.dkconfig_enabled && dkconfig_enabled) {
2435      return suppressions;
2436    } else {
2437      return null;
2438    }
2439  }
2440
2441  /** definition of this invariant (the suppressee) */
2442  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xyz.class, 3);
2443
2444  // suppressor definitions (used below)
2445  private static NISuppressor result_eq_arg1 =
2446      new NISuppressor(0, 1, FloatEqual.class);
2447  private static NISuppressor result_eq_arg2 =
2448      new NISuppressor(0, 2, FloatEqual.class);
2449  private static NISuppressor arg1_eq_arg2 =
2450      new NISuppressor(1, 2, FloatEqual.class);
2451
2452  private static NISuppressor result_lt_arg1 =
2453      new NISuppressor(0, 1, FloatLessThan.class);
2454  private static NISuppressor result_lt_arg2 =
2455      new NISuppressor(0, 2, FloatLessThan.class);
2456  private static NISuppressor arg1_lt_arg2 =
2457      new NISuppressor(1, 2, FloatLessThan.class);
2458  private static NISuppressor arg2_lt_arg1 =
2459      new NISuppressor(2, 1, FloatLessThan.class);
2460
2461  private static NISuppressor result_le_arg1 =
2462      new NISuppressor(0, 1, FloatLessEqual.class);
2463  private static NISuppressor result_le_arg2 =
2464      new NISuppressor(0, 2, FloatLessEqual.class);
2465  private static NISuppressor arg1_le_arg2 =
2466      new NISuppressor(1, 2, FloatLessEqual.class);
2467  private static NISuppressor arg2_le_arg1 =
2468      new NISuppressor(2, 1, FloatLessEqual.class);
2469
2470  private static NISuppressor result_track0_arg1 =
2471      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
2472  private static NISuppressor result_track0_arg2 =
2473      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
2474  private static NISuppressor arg1_track0_arg2 =
2475      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
2476  private static NISuppressor arg1_track0_result =
2477      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
2478  private static NISuppressor arg2_track0_result =
2479      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
2480  private static NISuppressor arg2_track0_arg1 =
2481      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
2482
2483  private static NISuppressor result_eq_1 =
2484      new NISuppressor(0, RangeFloat.EqualOne.class);
2485  private static NISuppressor arg1_eq_1 =
2486      new NISuppressor(1, RangeFloat.EqualOne.class);
2487  private static NISuppressor arg2_eq_1 =
2488      new NISuppressor(2, RangeFloat.EqualOne.class);
2489
2490  private static NISuppressor result_eq_0 =
2491      new NISuppressor(0, RangeFloat.EqualZero.class);
2492  private static NISuppressor arg1_eq_0 =
2493      new NISuppressor(1, RangeFloat.EqualZero.class);
2494  private static NISuppressor arg2_eq_0 =
2495      new NISuppressor(2, RangeFloat.EqualZero.class);
2496
2497  private static NISuppressor result_ne_0 =
2498      new NISuppressor(0, NonZeroFloat.class);
2499  private static NISuppressor arg1_ne_0 =
2500      new NISuppressor(1, NonZeroFloat.class);
2501  private static NISuppressor arg2_ne_0 =
2502      new NISuppressor(2, NonZeroFloat.class);
2503
2504  private static NISuppressor result_ge_0 =
2505      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
2506  private static NISuppressor arg1_ge_0 =
2507      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
2508  private static NISuppressor arg2_ge_0 =
2509      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
2510
2511  private static NISuppressor result_ge_64 =
2512      new NISuppressor(0, RangeInt.GreaterEqual64.class);
2513  private static NISuppressor arg1_ge_64 =
2514      new NISuppressor(1, RangeInt.GreaterEqual64.class);
2515  private static NISuppressor arg2_ge_64 =
2516      new NISuppressor(2, RangeInt.GreaterEqual64.class);
2517
2518    private static NISuppressionSet suppressions =
2519      new NISuppressionSet(
2520          new NISuppression[] {
2521
2522            // (y == z) && (z != 0) && (r == 1)
2523            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
2524
2525            // (r == y) && (z == 1) ==> r = y / z
2526            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
2527          });
2528
2529  // Create a suppression factory for functionBinary
2530
2531}
2532
2533/**
2534 * Represents the invariant {@code y = Division(x, z)} over three double
2535 * scalars. 
2536 */
2537public static class DivisionDouble_yxz extends FunctionBinaryFloat {
2538  // We are Serializable, so we specify a version to allow changes to
2539  // method signatures without breaking serialization.  If you add or
2540  // remove fields, you should change this number to the current date.
2541  static final long serialVersionUID = 20031030L;
2542
2543  private static @Prototype DivisionDouble_yxz proto = new @Prototype DivisionDouble_yxz ();
2544
2545  /** Returns the prototype invariant for DivisionDouble_yxz */
2546  public static @Prototype DivisionDouble_yxz get_proto() {
2547    return proto;
2548  }
2549
2550  /** instantiate an invariant on the specified slice */
2551  @Override
2552  protected DivisionDouble_yxz instantiate_dyn(@Prototype DivisionDouble_yxz this, PptSlice slice) {
2553    return new DivisionDouble_yxz (slice);
2554  }
2555
2556  private DivisionDouble_yxz (PptSlice slice) {
2557    super(slice);
2558  }
2559
2560  public @Prototype DivisionDouble_yxz () {
2561    super();
2562  }
2563
2564  private static String[] method_name = new String[] {"", " / ", ""};
2565
2566  @Override
2567  public String[] get_method_name(@GuardSatisfied DivisionDouble_yxz this) {
2568    return method_name;
2569  }
2570
2571  private static int function_id = -1;
2572
2573  @Override
2574  public int get_function_id() {
2575    return function_id;
2576  }
2577
2578  @Override
2579  public void set_function_id(int function_id) {
2580    assert DivisionDouble_yxz.function_id == -1;
2581    DivisionDouble_yxz.function_id = function_id;
2582  }
2583
2584  private static int var_order = 2;
2585
2586  @Override
2587  public int get_var_order(@GuardSatisfied DivisionDouble_yxz this) {
2588    return var_order;
2589  }
2590
2591  @Pure
2592  @Override
2593  public boolean is_symmetric() {
2594
2595      return false;
2596  }
2597
2598  @Override
2599
2600  public double func(double x, double z) {
2601
2602    return (x / z);
2603  }
2604
2605  @Override
2606  public InvariantStatus check_modified(double x, double y,
2607                                      double z, int count) {
2608    return check_ordered(y, x, z, count);
2609  }
2610
2611  @Override
2612  public InvariantStatus add_modified(double x, double y,
2613                                      double z, int count) {
2614    if (Debug.logDetail()) {
2615      log("result=%s, arg1=%s, arg2=%s", y, x, z);
2616    }
2617    return add_ordered(y, x, z, count);
2618  }
2619
2620  @Pure
2621  @Override
2622  public boolean isDivision() {
2623    return true;
2624  }
2625
2626  @Pure
2627  @Override
2628  public boolean isExact() {
2629    return true;
2630  }
2631
2632  /** Returns a list of non-instantiating suppressions for this invariant. */
2633  @Pure
2634  @Override
2635  public @Nullable NISuppressionSet get_ni_suppressions() {
2636    if (NIS.dkconfig_enabled && dkconfig_enabled) {
2637      return suppressions;
2638    } else {
2639      return null;
2640    }
2641  }
2642
2643  /** definition of this invariant (the suppressee) */
2644  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yxz.class, 3);
2645
2646  // suppressor definitions (used below)
2647  private static NISuppressor result_eq_arg1 =
2648      new NISuppressor(1, 0, FloatEqual.class);
2649  private static NISuppressor result_eq_arg2 =
2650      new NISuppressor(1, 2, FloatEqual.class);
2651  private static NISuppressor arg1_eq_arg2 =
2652      new NISuppressor(0, 2, FloatEqual.class);
2653
2654  private static NISuppressor result_lt_arg1 =
2655      new NISuppressor(1, 0, FloatLessThan.class);
2656  private static NISuppressor result_lt_arg2 =
2657      new NISuppressor(1, 2, FloatLessThan.class);
2658  private static NISuppressor arg1_lt_arg2 =
2659      new NISuppressor(0, 2, FloatLessThan.class);
2660  private static NISuppressor arg2_lt_arg1 =
2661      new NISuppressor(2, 0, FloatLessThan.class);
2662
2663  private static NISuppressor result_le_arg1 =
2664      new NISuppressor(1, 0, FloatLessEqual.class);
2665  private static NISuppressor result_le_arg2 =
2666      new NISuppressor(1, 2, FloatLessEqual.class);
2667  private static NISuppressor arg1_le_arg2 =
2668      new NISuppressor(0, 2, FloatLessEqual.class);
2669  private static NISuppressor arg2_le_arg1 =
2670      new NISuppressor(2, 0, FloatLessEqual.class);
2671
2672  private static NISuppressor result_track0_arg1 =
2673      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
2674  private static NISuppressor result_track0_arg2 =
2675      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
2676  private static NISuppressor arg1_track0_arg2 =
2677      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
2678  private static NISuppressor arg1_track0_result =
2679      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
2680  private static NISuppressor arg2_track0_result =
2681      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
2682  private static NISuppressor arg2_track0_arg1 =
2683      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
2684
2685  private static NISuppressor result_eq_1 =
2686      new NISuppressor(1, RangeFloat.EqualOne.class);
2687  private static NISuppressor arg1_eq_1 =
2688      new NISuppressor(0, RangeFloat.EqualOne.class);
2689  private static NISuppressor arg2_eq_1 =
2690      new NISuppressor(2, RangeFloat.EqualOne.class);
2691
2692  private static NISuppressor result_eq_0 =
2693      new NISuppressor(1, RangeFloat.EqualZero.class);
2694  private static NISuppressor arg1_eq_0 =
2695      new NISuppressor(0, RangeFloat.EqualZero.class);
2696  private static NISuppressor arg2_eq_0 =
2697      new NISuppressor(2, RangeFloat.EqualZero.class);
2698
2699  private static NISuppressor result_ne_0 =
2700      new NISuppressor(1, NonZeroFloat.class);
2701  private static NISuppressor arg1_ne_0 =
2702      new NISuppressor(0, NonZeroFloat.class);
2703  private static NISuppressor arg2_ne_0 =
2704      new NISuppressor(2, NonZeroFloat.class);
2705
2706  private static NISuppressor result_ge_0 =
2707      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
2708  private static NISuppressor arg1_ge_0 =
2709      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
2710  private static NISuppressor arg2_ge_0 =
2711      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
2712
2713  private static NISuppressor result_ge_64 =
2714      new NISuppressor(1, RangeInt.GreaterEqual64.class);
2715  private static NISuppressor arg1_ge_64 =
2716      new NISuppressor(0, RangeInt.GreaterEqual64.class);
2717  private static NISuppressor arg2_ge_64 =
2718      new NISuppressor(2, RangeInt.GreaterEqual64.class);
2719
2720    private static NISuppressionSet suppressions =
2721      new NISuppressionSet(
2722          new NISuppression[] {
2723
2724            // (x == z) && (z != 0) && (r == 1)
2725            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
2726
2727            // (r == x) && (z == 1) ==> r = x / z
2728            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
2729          });
2730
2731  // Create a suppression factory for functionBinary
2732
2733}
2734
2735/**
2736 * Represents the invariant {@code z = Division(x, y)} over three double
2737 * scalars. 
2738 */
2739public static class DivisionDouble_zxy extends FunctionBinaryFloat {
2740  // We are Serializable, so we specify a version to allow changes to
2741  // method signatures without breaking serialization.  If you add or
2742  // remove fields, you should change this number to the current date.
2743  static final long serialVersionUID = 20031030L;
2744
2745  private static @Prototype DivisionDouble_zxy proto = new @Prototype DivisionDouble_zxy ();
2746
2747  /** Returns the prototype invariant for DivisionDouble_zxy */
2748  public static @Prototype DivisionDouble_zxy get_proto() {
2749    return proto;
2750  }
2751
2752  /** instantiate an invariant on the specified slice */
2753  @Override
2754  protected DivisionDouble_zxy instantiate_dyn(@Prototype DivisionDouble_zxy this, PptSlice slice) {
2755    return new DivisionDouble_zxy (slice);
2756  }
2757
2758  private DivisionDouble_zxy (PptSlice slice) {
2759    super(slice);
2760  }
2761
2762  public @Prototype DivisionDouble_zxy () {
2763    super();
2764  }
2765
2766  private static String[] method_name = new String[] {"", " / ", ""};
2767
2768  @Override
2769  public String[] get_method_name(@GuardSatisfied DivisionDouble_zxy this) {
2770    return method_name;
2771  }
2772
2773  private static int function_id = -1;
2774
2775  @Override
2776  public int get_function_id() {
2777    return function_id;
2778  }
2779
2780  @Override
2781  public void set_function_id(int function_id) {
2782    assert DivisionDouble_zxy.function_id == -1;
2783    DivisionDouble_zxy.function_id = function_id;
2784  }
2785
2786  private static int var_order = 3;
2787
2788  @Override
2789  public int get_var_order(@GuardSatisfied DivisionDouble_zxy this) {
2790    return var_order;
2791  }
2792
2793  @Pure
2794  @Override
2795  public boolean is_symmetric() {
2796
2797      return false;
2798  }
2799
2800  @Override
2801
2802  public double func(double x, double y) {
2803
2804    return (x / y);
2805  }
2806
2807  @Override
2808  public InvariantStatus check_modified(double x, double y,
2809                                      double z, int count) {
2810    return check_ordered(z, x, y, count);
2811  }
2812
2813  @Override
2814  public InvariantStatus add_modified(double x, double y,
2815                                      double z, int count) {
2816    if (Debug.logDetail()) {
2817      log("result=%s, arg1=%s, arg2=%s", z, x, y);
2818    }
2819    return add_ordered(z, x, y, count);
2820  }
2821
2822  @Pure
2823  @Override
2824  public boolean isDivision() {
2825    return true;
2826  }
2827
2828  @Pure
2829  @Override
2830  public boolean isExact() {
2831    return true;
2832  }
2833
2834  /** Returns a list of non-instantiating suppressions for this invariant. */
2835  @Pure
2836  @Override
2837  public @Nullable NISuppressionSet get_ni_suppressions() {
2838    if (NIS.dkconfig_enabled && dkconfig_enabled) {
2839      return suppressions;
2840    } else {
2841      return null;
2842    }
2843  }
2844
2845  /** definition of this invariant (the suppressee) */
2846  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zxy.class, 3);
2847
2848  // suppressor definitions (used below)
2849  private static NISuppressor result_eq_arg1 =
2850      new NISuppressor(2, 0, FloatEqual.class);
2851  private static NISuppressor result_eq_arg2 =
2852      new NISuppressor(2, 1, FloatEqual.class);
2853  private static NISuppressor arg1_eq_arg2 =
2854      new NISuppressor(0, 1, FloatEqual.class);
2855
2856  private static NISuppressor result_lt_arg1 =
2857      new NISuppressor(2, 0, FloatLessThan.class);
2858  private static NISuppressor result_lt_arg2 =
2859      new NISuppressor(2, 1, FloatLessThan.class);
2860  private static NISuppressor arg1_lt_arg2 =
2861      new NISuppressor(0, 1, FloatLessThan.class);
2862  private static NISuppressor arg2_lt_arg1 =
2863      new NISuppressor(1, 0, FloatLessThan.class);
2864
2865  private static NISuppressor result_le_arg1 =
2866      new NISuppressor(2, 0, FloatLessEqual.class);
2867  private static NISuppressor result_le_arg2 =
2868      new NISuppressor(2, 1, FloatLessEqual.class);
2869  private static NISuppressor arg1_le_arg2 =
2870      new NISuppressor(0, 1, FloatLessEqual.class);
2871  private static NISuppressor arg2_le_arg1 =
2872      new NISuppressor(1, 0, FloatLessEqual.class);
2873
2874  private static NISuppressor result_track0_arg1 =
2875      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
2876  private static NISuppressor result_track0_arg2 =
2877      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
2878  private static NISuppressor arg1_track0_arg2 =
2879      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
2880  private static NISuppressor arg1_track0_result =
2881      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
2882  private static NISuppressor arg2_track0_result =
2883      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
2884  private static NISuppressor arg2_track0_arg1 =
2885      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
2886
2887  private static NISuppressor result_eq_1 =
2888      new NISuppressor(2, RangeFloat.EqualOne.class);
2889  private static NISuppressor arg1_eq_1 =
2890      new NISuppressor(0, RangeFloat.EqualOne.class);
2891  private static NISuppressor arg2_eq_1 =
2892      new NISuppressor(1, RangeFloat.EqualOne.class);
2893
2894  private static NISuppressor result_eq_0 =
2895      new NISuppressor(2, RangeFloat.EqualZero.class);
2896  private static NISuppressor arg1_eq_0 =
2897      new NISuppressor(0, RangeFloat.EqualZero.class);
2898  private static NISuppressor arg2_eq_0 =
2899      new NISuppressor(1, RangeFloat.EqualZero.class);
2900
2901  private static NISuppressor result_ne_0 =
2902      new NISuppressor(2, NonZeroFloat.class);
2903  private static NISuppressor arg1_ne_0 =
2904      new NISuppressor(0, NonZeroFloat.class);
2905  private static NISuppressor arg2_ne_0 =
2906      new NISuppressor(1, NonZeroFloat.class);
2907
2908  private static NISuppressor result_ge_0 =
2909      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
2910  private static NISuppressor arg1_ge_0 =
2911      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
2912  private static NISuppressor arg2_ge_0 =
2913      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
2914
2915  private static NISuppressor result_ge_64 =
2916      new NISuppressor(2, RangeInt.GreaterEqual64.class);
2917  private static NISuppressor arg1_ge_64 =
2918      new NISuppressor(0, RangeInt.GreaterEqual64.class);
2919  private static NISuppressor arg2_ge_64 =
2920      new NISuppressor(1, RangeInt.GreaterEqual64.class);
2921
2922    private static NISuppressionSet suppressions =
2923      new NISuppressionSet(
2924          new NISuppression[] {
2925
2926            // (x == y) && (y != 0) && (r == 1)
2927            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
2928
2929            // (r == x) && (y == 1) ==> r = x / y
2930            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
2931          });
2932
2933  // Create a suppression factory for functionBinary
2934
2935}
2936
2937/**
2938 * Represents the invariant {@code x = Division(z, y)} over three double
2939 * scalars. 
2940 */
2941public static class DivisionDouble_xzy extends FunctionBinaryFloat {
2942  // We are Serializable, so we specify a version to allow changes to
2943  // method signatures without breaking serialization.  If you add or
2944  // remove fields, you should change this number to the current date.
2945  static final long serialVersionUID = 20031030L;
2946
2947  private static @Prototype DivisionDouble_xzy proto = new @Prototype DivisionDouble_xzy ();
2948
2949  /** Returns the prototype invariant for DivisionDouble_xzy */
2950  public static @Prototype DivisionDouble_xzy get_proto() {
2951    return proto;
2952  }
2953
2954  /** instantiate an invariant on the specified slice */
2955  @Override
2956  protected DivisionDouble_xzy instantiate_dyn(@Prototype DivisionDouble_xzy this, PptSlice slice) {
2957    return new DivisionDouble_xzy (slice);
2958  }
2959
2960  private DivisionDouble_xzy (PptSlice slice) {
2961    super(slice);
2962  }
2963
2964  public @Prototype DivisionDouble_xzy () {
2965    super();
2966  }
2967
2968  private static String[] method_name = new String[] {"", " / ", ""};
2969
2970  @Override
2971  public String[] get_method_name(@GuardSatisfied DivisionDouble_xzy this) {
2972    return method_name;
2973  }
2974
2975  private static int function_id = -1;
2976
2977  @Override
2978  public int get_function_id() {
2979    return function_id;
2980  }
2981
2982  @Override
2983  public void set_function_id(int function_id) {
2984    assert DivisionDouble_xzy.function_id == -1;
2985    DivisionDouble_xzy.function_id = function_id;
2986  }
2987
2988  private static int var_order = 4;
2989
2990  @Override
2991  public int get_var_order(@GuardSatisfied DivisionDouble_xzy this) {
2992    return var_order;
2993  }
2994
2995  @Pure
2996  @Override
2997  public boolean is_symmetric() {
2998
2999      return false;
3000  }
3001
3002  @Override
3003
3004  public double func(double z, double y) {
3005
3006    return (z / y);
3007  }
3008
3009  @Override
3010  public InvariantStatus check_modified(double x, double y,
3011                                      double z, int count) {
3012    return check_ordered(x, z, y, count);
3013  }
3014
3015  @Override
3016  public InvariantStatus add_modified(double x, double y,
3017                                      double z, int count) {
3018    if (Debug.logDetail()) {
3019      log("result=%s, arg1=%s, arg2=%s", x, z, y);
3020    }
3021    return add_ordered(x, z, y, count);
3022  }
3023
3024  @Pure
3025  @Override
3026  public boolean isDivision() {
3027    return true;
3028  }
3029
3030  @Pure
3031  @Override
3032  public boolean isExact() {
3033    return true;
3034  }
3035
3036  /** Returns a list of non-instantiating suppressions for this invariant. */
3037  @Pure
3038  @Override
3039  public @Nullable NISuppressionSet get_ni_suppressions() {
3040    if (NIS.dkconfig_enabled && dkconfig_enabled) {
3041      return suppressions;
3042    } else {
3043      return null;
3044    }
3045  }
3046
3047  /** definition of this invariant (the suppressee) */
3048  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xzy.class, 3);
3049
3050  // suppressor definitions (used below)
3051  private static NISuppressor result_eq_arg1 =
3052      new NISuppressor(0, 2, FloatEqual.class);
3053  private static NISuppressor result_eq_arg2 =
3054      new NISuppressor(0, 1, FloatEqual.class);
3055  private static NISuppressor arg1_eq_arg2 =
3056      new NISuppressor(2, 1, FloatEqual.class);
3057
3058  private static NISuppressor result_lt_arg1 =
3059      new NISuppressor(0, 2, FloatLessThan.class);
3060  private static NISuppressor result_lt_arg2 =
3061      new NISuppressor(0, 1, FloatLessThan.class);
3062  private static NISuppressor arg1_lt_arg2 =
3063      new NISuppressor(2, 1, FloatLessThan.class);
3064  private static NISuppressor arg2_lt_arg1 =
3065      new NISuppressor(1, 2, FloatLessThan.class);
3066
3067  private static NISuppressor result_le_arg1 =
3068      new NISuppressor(0, 2, FloatLessEqual.class);
3069  private static NISuppressor result_le_arg2 =
3070      new NISuppressor(0, 1, FloatLessEqual.class);
3071  private static NISuppressor arg1_le_arg2 =
3072      new NISuppressor(2, 1, FloatLessEqual.class);
3073  private static NISuppressor arg2_le_arg1 =
3074      new NISuppressor(1, 2, FloatLessEqual.class);
3075
3076  private static NISuppressor result_track0_arg1 =
3077      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
3078  private static NISuppressor result_track0_arg2 =
3079      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
3080  private static NISuppressor arg1_track0_arg2 =
3081      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
3082  private static NISuppressor arg1_track0_result =
3083      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
3084  private static NISuppressor arg2_track0_result =
3085      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
3086  private static NISuppressor arg2_track0_arg1 =
3087      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
3088
3089  private static NISuppressor result_eq_1 =
3090      new NISuppressor(0, RangeFloat.EqualOne.class);
3091  private static NISuppressor arg1_eq_1 =
3092      new NISuppressor(2, RangeFloat.EqualOne.class);
3093  private static NISuppressor arg2_eq_1 =
3094      new NISuppressor(1, RangeFloat.EqualOne.class);
3095
3096  private static NISuppressor result_eq_0 =
3097      new NISuppressor(0, RangeFloat.EqualZero.class);
3098  private static NISuppressor arg1_eq_0 =
3099      new NISuppressor(2, RangeFloat.EqualZero.class);
3100  private static NISuppressor arg2_eq_0 =
3101      new NISuppressor(1, RangeFloat.EqualZero.class);
3102
3103  private static NISuppressor result_ne_0 =
3104      new NISuppressor(0, NonZeroFloat.class);
3105  private static NISuppressor arg1_ne_0 =
3106      new NISuppressor(2, NonZeroFloat.class);
3107  private static NISuppressor arg2_ne_0 =
3108      new NISuppressor(1, NonZeroFloat.class);
3109
3110  private static NISuppressor result_ge_0 =
3111      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
3112  private static NISuppressor arg1_ge_0 =
3113      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
3114  private static NISuppressor arg2_ge_0 =
3115      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
3116
3117  private static NISuppressor result_ge_64 =
3118      new NISuppressor(0, RangeInt.GreaterEqual64.class);
3119  private static NISuppressor arg1_ge_64 =
3120      new NISuppressor(2, RangeInt.GreaterEqual64.class);
3121  private static NISuppressor arg2_ge_64 =
3122      new NISuppressor(1, RangeInt.GreaterEqual64.class);
3123
3124    private static NISuppressionSet suppressions =
3125      new NISuppressionSet(
3126          new NISuppression[] {
3127
3128            // (z == y) && (y != 0) && (r == 1)
3129            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
3130
3131            // (r == z) && (y == 1) ==> r = z / y
3132            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
3133          });
3134
3135  // Create a suppression factory for functionBinary
3136
3137}
3138
3139/**
3140 * Represents the invariant {@code y = Division(z, x)} over three double
3141 * scalars. 
3142 */
3143public static class DivisionDouble_yzx extends FunctionBinaryFloat {
3144  // We are Serializable, so we specify a version to allow changes to
3145  // method signatures without breaking serialization.  If you add or
3146  // remove fields, you should change this number to the current date.
3147  static final long serialVersionUID = 20031030L;
3148
3149  private static @Prototype DivisionDouble_yzx proto = new @Prototype DivisionDouble_yzx ();
3150
3151  /** Returns the prototype invariant for DivisionDouble_yzx */
3152  public static @Prototype DivisionDouble_yzx get_proto() {
3153    return proto;
3154  }
3155
3156  /** instantiate an invariant on the specified slice */
3157  @Override
3158  protected DivisionDouble_yzx instantiate_dyn(@Prototype DivisionDouble_yzx this, PptSlice slice) {
3159    return new DivisionDouble_yzx (slice);
3160  }
3161
3162  private DivisionDouble_yzx (PptSlice slice) {
3163    super(slice);
3164  }
3165
3166  public @Prototype DivisionDouble_yzx () {
3167    super();
3168  }
3169
3170  private static String[] method_name = new String[] {"", " / ", ""};
3171
3172  @Override
3173  public String[] get_method_name(@GuardSatisfied DivisionDouble_yzx this) {
3174    return method_name;
3175  }
3176
3177  private static int function_id = -1;
3178
3179  @Override
3180  public int get_function_id() {
3181    return function_id;
3182  }
3183
3184  @Override
3185  public void set_function_id(int function_id) {
3186    assert DivisionDouble_yzx.function_id == -1;
3187    DivisionDouble_yzx.function_id = function_id;
3188  }
3189
3190  private static int var_order = 5;
3191
3192  @Override
3193  public int get_var_order(@GuardSatisfied DivisionDouble_yzx this) {
3194    return var_order;
3195  }
3196
3197  @Pure
3198  @Override
3199  public boolean is_symmetric() {
3200
3201      return false;
3202  }
3203
3204  @Override
3205
3206  public double func(double z, double x) {
3207
3208    return (z / x);
3209  }
3210
3211  @Override
3212  public InvariantStatus check_modified(double x, double y,
3213                                      double z, int count) {
3214    return check_ordered(y, z, x, count);
3215  }
3216
3217  @Override
3218  public InvariantStatus add_modified(double x, double y,
3219                                      double z, int count) {
3220    if (Debug.logDetail()) {
3221      log("result=%s, arg1=%s, arg2=%s", y, z, x);
3222    }
3223    return add_ordered(y, z, x, count);
3224  }
3225
3226  @Pure
3227  @Override
3228  public boolean isDivision() {
3229    return true;
3230  }
3231
3232  @Pure
3233  @Override
3234  public boolean isExact() {
3235    return true;
3236  }
3237
3238  /** Returns a list of non-instantiating suppressions for this invariant. */
3239  @Pure
3240  @Override
3241  public @Nullable NISuppressionSet get_ni_suppressions() {
3242    if (NIS.dkconfig_enabled && dkconfig_enabled) {
3243      return suppressions;
3244    } else {
3245      return null;
3246    }
3247  }
3248
3249  /** definition of this invariant (the suppressee) */
3250  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yzx.class, 3);
3251
3252  // suppressor definitions (used below)
3253  private static NISuppressor result_eq_arg1 =
3254      new NISuppressor(1, 2, FloatEqual.class);
3255  private static NISuppressor result_eq_arg2 =
3256      new NISuppressor(1, 0, FloatEqual.class);
3257  private static NISuppressor arg1_eq_arg2 =
3258      new NISuppressor(2, 0, FloatEqual.class);
3259
3260  private static NISuppressor result_lt_arg1 =
3261      new NISuppressor(1, 2, FloatLessThan.class);
3262  private static NISuppressor result_lt_arg2 =
3263      new NISuppressor(1, 0, FloatLessThan.class);
3264  private static NISuppressor arg1_lt_arg2 =
3265      new NISuppressor(2, 0, FloatLessThan.class);
3266  private static NISuppressor arg2_lt_arg1 =
3267      new NISuppressor(0, 2, FloatLessThan.class);
3268
3269  private static NISuppressor result_le_arg1 =
3270      new NISuppressor(1, 2, FloatLessEqual.class);
3271  private static NISuppressor result_le_arg2 =
3272      new NISuppressor(1, 0, FloatLessEqual.class);
3273  private static NISuppressor arg1_le_arg2 =
3274      new NISuppressor(2, 0, FloatLessEqual.class);
3275  private static NISuppressor arg2_le_arg1 =
3276      new NISuppressor(0, 2, FloatLessEqual.class);
3277
3278  private static NISuppressor result_track0_arg1 =
3279      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
3280  private static NISuppressor result_track0_arg2 =
3281      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
3282  private static NISuppressor arg1_track0_arg2 =
3283      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
3284  private static NISuppressor arg1_track0_result =
3285      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
3286  private static NISuppressor arg2_track0_result =
3287      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
3288  private static NISuppressor arg2_track0_arg1 =
3289      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
3290
3291  private static NISuppressor result_eq_1 =
3292      new NISuppressor(1, RangeFloat.EqualOne.class);
3293  private static NISuppressor arg1_eq_1 =
3294      new NISuppressor(2, RangeFloat.EqualOne.class);
3295  private static NISuppressor arg2_eq_1 =
3296      new NISuppressor(0, RangeFloat.EqualOne.class);
3297
3298  private static NISuppressor result_eq_0 =
3299      new NISuppressor(1, RangeFloat.EqualZero.class);
3300  private static NISuppressor arg1_eq_0 =
3301      new NISuppressor(2, RangeFloat.EqualZero.class);
3302  private static NISuppressor arg2_eq_0 =
3303      new NISuppressor(0, RangeFloat.EqualZero.class);
3304
3305  private static NISuppressor result_ne_0 =
3306      new NISuppressor(1, NonZeroFloat.class);
3307  private static NISuppressor arg1_ne_0 =
3308      new NISuppressor(2, NonZeroFloat.class);
3309  private static NISuppressor arg2_ne_0 =
3310      new NISuppressor(0, NonZeroFloat.class);
3311
3312  private static NISuppressor result_ge_0 =
3313      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
3314  private static NISuppressor arg1_ge_0 =
3315      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
3316  private static NISuppressor arg2_ge_0 =
3317      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
3318
3319  private static NISuppressor result_ge_64 =
3320      new NISuppressor(1, RangeInt.GreaterEqual64.class);
3321  private static NISuppressor arg1_ge_64 =
3322      new NISuppressor(2, RangeInt.GreaterEqual64.class);
3323  private static NISuppressor arg2_ge_64 =
3324      new NISuppressor(0, RangeInt.GreaterEqual64.class);
3325
3326    private static NISuppressionSet suppressions =
3327      new NISuppressionSet(
3328          new NISuppression[] {
3329
3330            // (z == x) && (x != 0) && (r == 1)
3331            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
3332
3333            // (r == z) && (x == 1) ==> r = z / x
3334            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
3335          });
3336
3337  // Create a suppression factory for functionBinary
3338
3339}
3340
3341/**
3342 * Represents the invariant {@code z = Division(y, x)} over three double
3343 * scalars. 
3344 */
3345public static class DivisionDouble_zyx extends FunctionBinaryFloat {
3346  // We are Serializable, so we specify a version to allow changes to
3347  // method signatures without breaking serialization.  If you add or
3348  // remove fields, you should change this number to the current date.
3349  static final long serialVersionUID = 20031030L;
3350
3351  private static @Prototype DivisionDouble_zyx proto = new @Prototype DivisionDouble_zyx ();
3352
3353  /** Returns the prototype invariant for DivisionDouble_zyx */
3354  public static @Prototype DivisionDouble_zyx get_proto() {
3355    return proto;
3356  }
3357
3358  /** instantiate an invariant on the specified slice */
3359  @Override
3360  protected DivisionDouble_zyx instantiate_dyn(@Prototype DivisionDouble_zyx this, PptSlice slice) {
3361    return new DivisionDouble_zyx (slice);
3362  }
3363
3364  private DivisionDouble_zyx (PptSlice slice) {
3365    super(slice);
3366  }
3367
3368  public @Prototype DivisionDouble_zyx () {
3369    super();
3370  }
3371
3372  private static String[] method_name = new String[] {"", " / ", ""};
3373
3374  @Override
3375  public String[] get_method_name(@GuardSatisfied DivisionDouble_zyx this) {
3376    return method_name;
3377  }
3378
3379  private static int function_id = -1;
3380
3381  @Override
3382  public int get_function_id() {
3383    return function_id;
3384  }
3385
3386  @Override
3387  public void set_function_id(int function_id) {
3388    assert DivisionDouble_zyx.function_id == -1;
3389    DivisionDouble_zyx.function_id = function_id;
3390  }
3391
3392  private static int var_order = 6;
3393
3394  @Override
3395  public int get_var_order(@GuardSatisfied DivisionDouble_zyx this) {
3396    return var_order;
3397  }
3398
3399  @Pure
3400  @Override
3401  public boolean is_symmetric() {
3402
3403      return false;
3404  }
3405
3406  @Override
3407
3408  public double func(double y, double x) {
3409
3410    return (y / x);
3411  }
3412
3413  @Override
3414  public InvariantStatus check_modified(double x, double y,
3415                                      double z, int count) {
3416    return check_ordered(z, y, x, count);
3417  }
3418
3419  @Override
3420  public InvariantStatus add_modified(double x, double y,
3421                                      double z, int count) {
3422    if (Debug.logDetail()) {
3423      log("result=%s, arg1=%s, arg2=%s", z, y, x);
3424    }
3425    return add_ordered(z, y, x, count);
3426  }
3427
3428  @Pure
3429  @Override
3430  public boolean isDivision() {
3431    return true;
3432  }
3433
3434  @Pure
3435  @Override
3436  public boolean isExact() {
3437    return true;
3438  }
3439
3440  /** Returns a list of non-instantiating suppressions for this invariant. */
3441  @Pure
3442  @Override
3443  public @Nullable NISuppressionSet get_ni_suppressions() {
3444    if (NIS.dkconfig_enabled && dkconfig_enabled) {
3445      return suppressions;
3446    } else {
3447      return null;
3448    }
3449  }
3450
3451  /** definition of this invariant (the suppressee) */
3452  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zyx.class, 3);
3453
3454  // suppressor definitions (used below)
3455  private static NISuppressor result_eq_arg1 =
3456      new NISuppressor(2, 1, FloatEqual.class);
3457  private static NISuppressor result_eq_arg2 =
3458      new NISuppressor(2, 0, FloatEqual.class);
3459  private static NISuppressor arg1_eq_arg2 =
3460      new NISuppressor(1, 0, FloatEqual.class);
3461
3462  private static NISuppressor result_lt_arg1 =
3463      new NISuppressor(2, 1, FloatLessThan.class);
3464  private static NISuppressor result_lt_arg2 =
3465      new NISuppressor(2, 0, FloatLessThan.class);
3466  private static NISuppressor arg1_lt_arg2 =
3467      new NISuppressor(1, 0, FloatLessThan.class);
3468  private static NISuppressor arg2_lt_arg1 =
3469      new NISuppressor(0, 1, FloatLessThan.class);
3470
3471  private static NISuppressor result_le_arg1 =
3472      new NISuppressor(2, 1, FloatLessEqual.class);
3473  private static NISuppressor result_le_arg2 =
3474      new NISuppressor(2, 0, FloatLessEqual.class);
3475  private static NISuppressor arg1_le_arg2 =
3476      new NISuppressor(1, 0, FloatLessEqual.class);
3477  private static NISuppressor arg2_le_arg1 =
3478      new NISuppressor(0, 1, FloatLessEqual.class);
3479
3480  private static NISuppressor result_track0_arg1 =
3481      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
3482  private static NISuppressor result_track0_arg2 =
3483      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
3484  private static NISuppressor arg1_track0_arg2 =
3485      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
3486  private static NISuppressor arg1_track0_result =
3487      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
3488  private static NISuppressor arg2_track0_result =
3489      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
3490  private static NISuppressor arg2_track0_arg1 =
3491      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
3492
3493  private static NISuppressor result_eq_1 =
3494      new NISuppressor(2, RangeFloat.EqualOne.class);
3495  private static NISuppressor arg1_eq_1 =
3496      new NISuppressor(1, RangeFloat.EqualOne.class);
3497  private static NISuppressor arg2_eq_1 =
3498      new NISuppressor(0, RangeFloat.EqualOne.class);
3499
3500  private static NISuppressor result_eq_0 =
3501      new NISuppressor(2, RangeFloat.EqualZero.class);
3502  private static NISuppressor arg1_eq_0 =
3503      new NISuppressor(1, RangeFloat.EqualZero.class);
3504  private static NISuppressor arg2_eq_0 =
3505      new NISuppressor(0, RangeFloat.EqualZero.class);
3506
3507  private static NISuppressor result_ne_0 =
3508      new NISuppressor(2, NonZeroFloat.class);
3509  private static NISuppressor arg1_ne_0 =
3510      new NISuppressor(1, NonZeroFloat.class);
3511  private static NISuppressor arg2_ne_0 =
3512      new NISuppressor(0, NonZeroFloat.class);
3513
3514  private static NISuppressor result_ge_0 =
3515      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
3516  private static NISuppressor arg1_ge_0 =
3517      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
3518  private static NISuppressor arg2_ge_0 =
3519      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
3520
3521  private static NISuppressor result_ge_64 =
3522      new NISuppressor(2, RangeInt.GreaterEqual64.class);
3523  private static NISuppressor arg1_ge_64 =
3524      new NISuppressor(1, RangeInt.GreaterEqual64.class);
3525  private static NISuppressor arg2_ge_64 =
3526      new NISuppressor(0, RangeInt.GreaterEqual64.class);
3527
3528    private static NISuppressionSet suppressions =
3529      new NISuppressionSet(
3530          new NISuppression[] {
3531
3532            // (y == x) && (x != 0) && (r == 1)
3533            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),
3534
3535            // (r == y) && (x == 1) ==> r = y / x
3536            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
3537          });
3538
3539  // Create a suppression factory for functionBinary
3540
3541}
3542
3543  // default is that it is not this function, overriden in the subclass
3544  @Pure
3545  public boolean isPower() {
3546    return false;
3547  }
3548
3549/**
3550 * Represents the invariant {@code x = Power(y, z)} over three double
3551 * scalars. 
3552 */
3553public static class PowerDouble_xyz extends FunctionBinaryFloat {
3554  // We are Serializable, so we specify a version to allow changes to
3555  // method signatures without breaking serialization.  If you add or
3556  // remove fields, you should change this number to the current date.
3557  static final long serialVersionUID = 20031030L;
3558
3559  private static @Prototype PowerDouble_xyz proto = new @Prototype PowerDouble_xyz ();
3560
3561  /** Returns the prototype invariant for PowerDouble_xyz */
3562  public static @Prototype PowerDouble_xyz get_proto() {
3563    return proto;
3564  }
3565
3566  /** instantiate an invariant on the specified slice */
3567  @Override
3568  protected PowerDouble_xyz instantiate_dyn(@Prototype PowerDouble_xyz this, PptSlice slice) {
3569    return new PowerDouble_xyz (slice);
3570  }
3571
3572  private PowerDouble_xyz (PptSlice slice) {
3573    super(slice);
3574  }
3575
3576  public @Prototype PowerDouble_xyz () {
3577    super();
3578  }
3579
3580  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
3581
3582  @Override
3583  public String[] get_method_name(@GuardSatisfied PowerDouble_xyz this) {
3584    return method_name;
3585  }
3586
3587  private static int function_id = -1;
3588
3589  @Override
3590  public int get_function_id() {
3591    return function_id;
3592  }
3593
3594  @Override
3595  public void set_function_id(int function_id) {
3596    assert PowerDouble_xyz.function_id == -1;
3597    PowerDouble_xyz.function_id = function_id;
3598  }
3599
3600  private static int var_order = 1;
3601
3602  @Override
3603  public int get_var_order(@GuardSatisfied PowerDouble_xyz this) {
3604    return var_order;
3605  }
3606
3607  @Pure
3608  @Override
3609  public boolean is_symmetric() {
3610
3611      return false;
3612  }
3613
3614  @Override
3615
3616  public double func(double y, double z) {
3617
3618    return Math.pow(y, z);
3619  }
3620
3621  @Override
3622  public InvariantStatus check_modified(double x, double y,
3623                                      double z, int count) {
3624    return check_ordered(x, y, z, count);
3625  }
3626
3627  @Override
3628  public InvariantStatus add_modified(double x, double y,
3629                                      double z, int count) {
3630    if (Debug.logDetail()) {
3631      log("result=%s, arg1=%s, arg2=%s", x, y, z);
3632    }
3633    return add_ordered(x, y, z, count);
3634  }
3635
3636  @Pure
3637  @Override
3638  public boolean isPower() {
3639    return true;
3640  }
3641
3642  @Pure
3643  @Override
3644  public boolean isExact() {
3645    return true;
3646  }
3647
3648  /** Returns a list of non-instantiating suppressions for this invariant. */
3649  @Pure
3650  @Override
3651  public @Nullable NISuppressionSet get_ni_suppressions() {
3652    if (NIS.dkconfig_enabled && dkconfig_enabled) {
3653      return suppressions;
3654    } else {
3655      return null;
3656    }
3657  }
3658
3659  /** definition of this invariant (the suppressee) */
3660  private static NISuppressee suppressee = new NISuppressee(PowerDouble_xyz.class, 3);
3661
3662  // suppressor definitions (used below)
3663  private static NISuppressor result_eq_arg1 =
3664      new NISuppressor(0, 1, FloatEqual.class);
3665  private static NISuppressor result_eq_arg2 =
3666      new NISuppressor(0, 2, FloatEqual.class);
3667  private static NISuppressor arg1_eq_arg2 =
3668      new NISuppressor(1, 2, FloatEqual.class);
3669
3670  private static NISuppressor result_lt_arg1 =
3671      new NISuppressor(0, 1, FloatLessThan.class);
3672  private static NISuppressor result_lt_arg2 =
3673      new NISuppressor(0, 2, FloatLessThan.class);
3674  private static NISuppressor arg1_lt_arg2 =
3675      new NISuppressor(1, 2, FloatLessThan.class);
3676  private static NISuppressor arg2_lt_arg1 =
3677      new NISuppressor(2, 1, FloatLessThan.class);
3678
3679  private static NISuppressor result_le_arg1 =
3680      new NISuppressor(0, 1, FloatLessEqual.class);
3681  private static NISuppressor result_le_arg2 =
3682      new NISuppressor(0, 2, FloatLessEqual.class);
3683  private static NISuppressor arg1_le_arg2 =
3684      new NISuppressor(1, 2, FloatLessEqual.class);
3685  private static NISuppressor arg2_le_arg1 =
3686      new NISuppressor(2, 1, FloatLessEqual.class);
3687
3688  private static NISuppressor result_track0_arg1 =
3689      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
3690  private static NISuppressor result_track0_arg2 =
3691      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
3692  private static NISuppressor arg1_track0_arg2 =
3693      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
3694  private static NISuppressor arg1_track0_result =
3695      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
3696  private static NISuppressor arg2_track0_result =
3697      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
3698  private static NISuppressor arg2_track0_arg1 =
3699      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
3700
3701  private static NISuppressor result_eq_1 =
3702      new NISuppressor(0, RangeFloat.EqualOne.class);
3703  private static NISuppressor arg1_eq_1 =
3704      new NISuppressor(1, RangeFloat.EqualOne.class);
3705  private static NISuppressor arg2_eq_1 =
3706      new NISuppressor(2, RangeFloat.EqualOne.class);
3707
3708  private static NISuppressor result_eq_0 =
3709      new NISuppressor(0, RangeFloat.EqualZero.class);
3710  private static NISuppressor arg1_eq_0 =
3711      new NISuppressor(1, RangeFloat.EqualZero.class);
3712  private static NISuppressor arg2_eq_0 =
3713      new NISuppressor(2, RangeFloat.EqualZero.class);
3714
3715  private static NISuppressor result_ne_0 =
3716      new NISuppressor(0, NonZeroFloat.class);
3717  private static NISuppressor arg1_ne_0 =
3718      new NISuppressor(1, NonZeroFloat.class);
3719  private static NISuppressor arg2_ne_0 =
3720      new NISuppressor(2, NonZeroFloat.class);
3721
3722  private static NISuppressor result_ge_0 =
3723      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
3724  private static NISuppressor arg1_ge_0 =
3725      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
3726  private static NISuppressor arg2_ge_0 =
3727      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
3728
3729  private static NISuppressor result_ge_64 =
3730      new NISuppressor(0, RangeInt.GreaterEqual64.class);
3731  private static NISuppressor arg1_ge_64 =
3732      new NISuppressor(1, RangeInt.GreaterEqual64.class);
3733  private static NISuppressor arg2_ge_64 =
3734      new NISuppressor(2, RangeInt.GreaterEqual64.class);
3735
3736    // Note that any suppression that doesn't limit z to valid exponents
3737    // (>= 0), must check for valid exponents as well (so that the invariant
3738    // is correctly destroyed on invalid exponents)
3739    //
3740    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
3741    // Another interesting artificat of pow is that for any even base, any
3742    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
3743    // (at least for integers)
3744
3745    private static NISuppressionSet suppressions =
3746      new NISuppressionSet(
3747          new NISuppression[] {
3748
3749            // (r == 1) && (z == 0) ==> r = pow (y, z)
3750            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
3751
3752            // (r == 1) && (y == 1) && (z >= 0)   ==> r = pow (y, z)
3753            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
3754
3755            // (r == 0) && (y == 0) && (z > 0)
3756            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
3757                              suppressee),
3758
3759            // (r == y) && (z == 1)    ==> r = pow (y, z)
3760            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
3761
3762          });
3763
3764  // Create a suppression factory for functionBinary
3765
3766}
3767
3768/**
3769 * Represents the invariant {@code y = Power(x, z)} over three double
3770 * scalars. 
3771 */
3772public static class PowerDouble_yxz extends FunctionBinaryFloat {
3773  // We are Serializable, so we specify a version to allow changes to
3774  // method signatures without breaking serialization.  If you add or
3775  // remove fields, you should change this number to the current date.
3776  static final long serialVersionUID = 20031030L;
3777
3778  private static @Prototype PowerDouble_yxz proto = new @Prototype PowerDouble_yxz ();
3779
3780  /** Returns the prototype invariant for PowerDouble_yxz */
3781  public static @Prototype PowerDouble_yxz get_proto() {
3782    return proto;
3783  }
3784
3785  /** instantiate an invariant on the specified slice */
3786  @Override
3787  protected PowerDouble_yxz instantiate_dyn(@Prototype PowerDouble_yxz this, PptSlice slice) {
3788    return new PowerDouble_yxz (slice);
3789  }
3790
3791  private PowerDouble_yxz (PptSlice slice) {
3792    super(slice);
3793  }
3794
3795  public @Prototype PowerDouble_yxz () {
3796    super();
3797  }
3798
3799  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
3800
3801  @Override
3802  public String[] get_method_name(@GuardSatisfied PowerDouble_yxz this) {
3803    return method_name;
3804  }
3805
3806  private static int function_id = -1;
3807
3808  @Override
3809  public int get_function_id() {
3810    return function_id;
3811  }
3812
3813  @Override
3814  public void set_function_id(int function_id) {
3815    assert PowerDouble_yxz.function_id == -1;
3816    PowerDouble_yxz.function_id = function_id;
3817  }
3818
3819  private static int var_order = 2;
3820
3821  @Override
3822  public int get_var_order(@GuardSatisfied PowerDouble_yxz this) {
3823    return var_order;
3824  }
3825
3826  @Pure
3827  @Override
3828  public boolean is_symmetric() {
3829
3830      return false;
3831  }
3832
3833  @Override
3834
3835  public double func(double x, double z) {
3836
3837    return Math.pow(x, z);
3838  }
3839
3840  @Override
3841  public InvariantStatus check_modified(double x, double y,
3842                                      double z, int count) {
3843    return check_ordered(y, x, z, count);
3844  }
3845
3846  @Override
3847  public InvariantStatus add_modified(double x, double y,
3848                                      double z, int count) {
3849    if (Debug.logDetail()) {
3850      log("result=%s, arg1=%s, arg2=%s", y, x, z);
3851    }
3852    return add_ordered(y, x, z, count);
3853  }
3854
3855  @Pure
3856  @Override
3857  public boolean isPower() {
3858    return true;
3859  }
3860
3861  @Pure
3862  @Override
3863  public boolean isExact() {
3864    return true;
3865  }
3866
3867  /** Returns a list of non-instantiating suppressions for this invariant. */
3868  @Pure
3869  @Override
3870  public @Nullable NISuppressionSet get_ni_suppressions() {
3871    if (NIS.dkconfig_enabled && dkconfig_enabled) {
3872      return suppressions;
3873    } else {
3874      return null;
3875    }
3876  }
3877
3878  /** definition of this invariant (the suppressee) */
3879  private static NISuppressee suppressee = new NISuppressee(PowerDouble_yxz.class, 3);
3880
3881  // suppressor definitions (used below)
3882  private static NISuppressor result_eq_arg1 =
3883      new NISuppressor(1, 0, FloatEqual.class);
3884  private static NISuppressor result_eq_arg2 =
3885      new NISuppressor(1, 2, FloatEqual.class);
3886  private static NISuppressor arg1_eq_arg2 =
3887      new NISuppressor(0, 2, FloatEqual.class);
3888
3889  private static NISuppressor result_lt_arg1 =
3890      new NISuppressor(1, 0, FloatLessThan.class);
3891  private static NISuppressor result_lt_arg2 =
3892      new NISuppressor(1, 2, FloatLessThan.class);
3893  private static NISuppressor arg1_lt_arg2 =
3894      new NISuppressor(0, 2, FloatLessThan.class);
3895  private static NISuppressor arg2_lt_arg1 =
3896      new NISuppressor(2, 0, FloatLessThan.class);
3897
3898  private static NISuppressor result_le_arg1 =
3899      new NISuppressor(1, 0, FloatLessEqual.class);
3900  private static NISuppressor result_le_arg2 =
3901      new NISuppressor(1, 2, FloatLessEqual.class);
3902  private static NISuppressor arg1_le_arg2 =
3903      new NISuppressor(0, 2, FloatLessEqual.class);
3904  private static NISuppressor arg2_le_arg1 =
3905      new NISuppressor(2, 0, FloatLessEqual.class);
3906
3907  private static NISuppressor result_track0_arg1 =
3908      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
3909  private static NISuppressor result_track0_arg2 =
3910      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
3911  private static NISuppressor arg1_track0_arg2 =
3912      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
3913  private static NISuppressor arg1_track0_result =
3914      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
3915  private static NISuppressor arg2_track0_result =
3916      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
3917  private static NISuppressor arg2_track0_arg1 =
3918      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
3919
3920  private static NISuppressor result_eq_1 =
3921      new NISuppressor(1, RangeFloat.EqualOne.class);
3922  private static NISuppressor arg1_eq_1 =
3923      new NISuppressor(0, RangeFloat.EqualOne.class);
3924  private static NISuppressor arg2_eq_1 =
3925      new NISuppressor(2, RangeFloat.EqualOne.class);
3926
3927  private static NISuppressor result_eq_0 =
3928      new NISuppressor(1, RangeFloat.EqualZero.class);
3929  private static NISuppressor arg1_eq_0 =
3930      new NISuppressor(0, RangeFloat.EqualZero.class);
3931  private static NISuppressor arg2_eq_0 =
3932      new NISuppressor(2, RangeFloat.EqualZero.class);
3933
3934  private static NISuppressor result_ne_0 =
3935      new NISuppressor(1, NonZeroFloat.class);
3936  private static NISuppressor arg1_ne_0 =
3937      new NISuppressor(0, NonZeroFloat.class);
3938  private static NISuppressor arg2_ne_0 =
3939      new NISuppressor(2, NonZeroFloat.class);
3940
3941  private static NISuppressor result_ge_0 =
3942      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
3943  private static NISuppressor arg1_ge_0 =
3944      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
3945  private static NISuppressor arg2_ge_0 =
3946      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
3947
3948  private static NISuppressor result_ge_64 =
3949      new NISuppressor(1, RangeInt.GreaterEqual64.class);
3950  private static NISuppressor arg1_ge_64 =
3951      new NISuppressor(0, RangeInt.GreaterEqual64.class);
3952  private static NISuppressor arg2_ge_64 =
3953      new NISuppressor(2, RangeInt.GreaterEqual64.class);
3954
3955    // Note that any suppression that doesn't limit z to valid exponents
3956    // (>= 0), must check for valid exponents as well (so that the invariant
3957    // is correctly destroyed on invalid exponents)
3958    //
3959    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
3960    // Another interesting artificat of pow is that for any even base, any
3961    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
3962    // (at least for integers)
3963
3964    private static NISuppressionSet suppressions =
3965      new NISuppressionSet(
3966          new NISuppression[] {
3967
3968            // (r == 1) && (z == 0) ==> r = pow (x, z)
3969            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
3970
3971            // (r == 1) && (x == 1) && (z >= 0)   ==> r = pow (x, z)
3972            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
3973
3974            // (r == 0) && (x == 0) && (z > 0)
3975            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
3976                              suppressee),
3977
3978            // (r == x) && (z == 1)    ==> r = pow (x, z)
3979            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
3980
3981          });
3982
3983  // Create a suppression factory for functionBinary
3984
3985}
3986
3987/**
3988 * Represents the invariant {@code z = Power(x, y)} over three double
3989 * scalars. 
3990 */
3991public static class PowerDouble_zxy extends FunctionBinaryFloat {
3992  // We are Serializable, so we specify a version to allow changes to
3993  // method signatures without breaking serialization.  If you add or
3994  // remove fields, you should change this number to the current date.
3995  static final long serialVersionUID = 20031030L;
3996
3997  private static @Prototype PowerDouble_zxy proto = new @Prototype PowerDouble_zxy ();
3998
3999  /** Returns the prototype invariant for PowerDouble_zxy */
4000  public static @Prototype PowerDouble_zxy get_proto() {
4001    return proto;
4002  }
4003
4004  /** instantiate an invariant on the specified slice */
4005  @Override
4006  protected PowerDouble_zxy instantiate_dyn(@Prototype PowerDouble_zxy this, PptSlice slice) {
4007    return new PowerDouble_zxy (slice);
4008  }
4009
4010  private PowerDouble_zxy (PptSlice slice) {
4011    super(slice);
4012  }
4013
4014  public @Prototype PowerDouble_zxy () {
4015    super();
4016  }
4017
4018  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
4019
4020  @Override
4021  public String[] get_method_name(@GuardSatisfied PowerDouble_zxy this) {
4022    return method_name;
4023  }
4024
4025  private static int function_id = -1;
4026
4027  @Override
4028  public int get_function_id() {
4029    return function_id;
4030  }
4031
4032  @Override
4033  public void set_function_id(int function_id) {
4034    assert PowerDouble_zxy.function_id == -1;
4035    PowerDouble_zxy.function_id = function_id;
4036  }
4037
4038  private static int var_order = 3;
4039
4040  @Override
4041  public int get_var_order(@GuardSatisfied PowerDouble_zxy this) {
4042    return var_order;
4043  }
4044
4045  @Pure
4046  @Override
4047  public boolean is_symmetric() {
4048
4049      return false;
4050  }
4051
4052  @Override
4053
4054  public double func(double x, double y) {
4055
4056    return Math.pow(x, y);
4057  }
4058
4059  @Override
4060  public InvariantStatus check_modified(double x, double y,
4061                                      double z, int count) {
4062    return check_ordered(z, x, y, count);
4063  }
4064
4065  @Override
4066  public InvariantStatus add_modified(double x, double y,
4067                                      double z, int count) {
4068    if (Debug.logDetail()) {
4069      log("result=%s, arg1=%s, arg2=%s", z, x, y);
4070    }
4071    return add_ordered(z, x, y, count);
4072  }
4073
4074  @Pure
4075  @Override
4076  public boolean isPower() {
4077    return true;
4078  }
4079
4080  @Pure
4081  @Override
4082  public boolean isExact() {
4083    return true;
4084  }
4085
4086  /** Returns a list of non-instantiating suppressions for this invariant. */
4087  @Pure
4088  @Override
4089  public @Nullable NISuppressionSet get_ni_suppressions() {
4090    if (NIS.dkconfig_enabled && dkconfig_enabled) {
4091      return suppressions;
4092    } else {
4093      return null;
4094    }
4095  }
4096
4097  /** definition of this invariant (the suppressee) */
4098  private static NISuppressee suppressee = new NISuppressee(PowerDouble_zxy.class, 3);
4099
4100  // suppressor definitions (used below)
4101  private static NISuppressor result_eq_arg1 =
4102      new NISuppressor(2, 0, FloatEqual.class);
4103  private static NISuppressor result_eq_arg2 =
4104      new NISuppressor(2, 1, FloatEqual.class);
4105  private static NISuppressor arg1_eq_arg2 =
4106      new NISuppressor(0, 1, FloatEqual.class);
4107
4108  private static NISuppressor result_lt_arg1 =
4109      new NISuppressor(2, 0, FloatLessThan.class);
4110  private static NISuppressor result_lt_arg2 =
4111      new NISuppressor(2, 1, FloatLessThan.class);
4112  private static NISuppressor arg1_lt_arg2 =
4113      new NISuppressor(0, 1, FloatLessThan.class);
4114  private static NISuppressor arg2_lt_arg1 =
4115      new NISuppressor(1, 0, FloatLessThan.class);
4116
4117  private static NISuppressor result_le_arg1 =
4118      new NISuppressor(2, 0, FloatLessEqual.class);
4119  private static NISuppressor result_le_arg2 =
4120      new NISuppressor(2, 1, FloatLessEqual.class);
4121  private static NISuppressor arg1_le_arg2 =
4122      new NISuppressor(0, 1, FloatLessEqual.class);
4123  private static NISuppressor arg2_le_arg1 =
4124      new NISuppressor(1, 0, FloatLessEqual.class);
4125
4126  private static NISuppressor result_track0_arg1 =
4127      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
4128  private static NISuppressor result_track0_arg2 =
4129      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
4130  private static NISuppressor arg1_track0_arg2 =
4131      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
4132  private static NISuppressor arg1_track0_result =
4133      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
4134  private static NISuppressor arg2_track0_result =
4135      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
4136  private static NISuppressor arg2_track0_arg1 =
4137      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
4138
4139  private static NISuppressor result_eq_1 =
4140      new NISuppressor(2, RangeFloat.EqualOne.class);
4141  private static NISuppressor arg1_eq_1 =
4142      new NISuppressor(0, RangeFloat.EqualOne.class);
4143  private static NISuppressor arg2_eq_1 =
4144      new NISuppressor(1, RangeFloat.EqualOne.class);
4145
4146  private static NISuppressor result_eq_0 =
4147      new NISuppressor(2, RangeFloat.EqualZero.class);
4148  private static NISuppressor arg1_eq_0 =
4149      new NISuppressor(0, RangeFloat.EqualZero.class);
4150  private static NISuppressor arg2_eq_0 =
4151      new NISuppressor(1, RangeFloat.EqualZero.class);
4152
4153  private static NISuppressor result_ne_0 =
4154      new NISuppressor(2, NonZeroFloat.class);
4155  private static NISuppressor arg1_ne_0 =
4156      new NISuppressor(0, NonZeroFloat.class);
4157  private static NISuppressor arg2_ne_0 =
4158      new NISuppressor(1, NonZeroFloat.class);
4159
4160  private static NISuppressor result_ge_0 =
4161      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
4162  private static NISuppressor arg1_ge_0 =
4163      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
4164  private static NISuppressor arg2_ge_0 =
4165      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
4166
4167  private static NISuppressor result_ge_64 =
4168      new NISuppressor(2, RangeInt.GreaterEqual64.class);
4169  private static NISuppressor arg1_ge_64 =
4170      new NISuppressor(0, RangeInt.GreaterEqual64.class);
4171  private static NISuppressor arg2_ge_64 =
4172      new NISuppressor(1, RangeInt.GreaterEqual64.class);
4173
4174    // Note that any suppression that doesn't limit y to valid exponents
4175    // (>= 0), must check for valid exponents as well (so that the invariant
4176    // is correctly destroyed on invalid exponents)
4177    //
4178    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
4179    // Another interesting artificat of pow is that for any even base, any
4180    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
4181    // (at least for integers)
4182
4183    private static NISuppressionSet suppressions =
4184      new NISuppressionSet(
4185          new NISuppression[] {
4186
4187            // (r == 1) && (y == 0) ==> r = pow (x, y)
4188            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
4189
4190            // (r == 1) && (x == 1) && (y >= 0)   ==> r = pow (x, y)
4191            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
4192
4193            // (r == 0) && (x == 0) && (y > 0)
4194            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
4195                              suppressee),
4196
4197            // (r == x) && (y == 1)    ==> r = pow (x, y)
4198            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
4199
4200          });
4201
4202  // Create a suppression factory for functionBinary
4203
4204}
4205
4206/**
4207 * Represents the invariant {@code x = Power(z, y)} over three double
4208 * scalars. 
4209 */
4210public static class PowerDouble_xzy extends FunctionBinaryFloat {
4211  // We are Serializable, so we specify a version to allow changes to
4212  // method signatures without breaking serialization.  If you add or
4213  // remove fields, you should change this number to the current date.
4214  static final long serialVersionUID = 20031030L;
4215
4216  private static @Prototype PowerDouble_xzy proto = new @Prototype PowerDouble_xzy ();
4217
4218  /** Returns the prototype invariant for PowerDouble_xzy */
4219  public static @Prototype PowerDouble_xzy get_proto() {
4220    return proto;
4221  }
4222
4223  /** instantiate an invariant on the specified slice */
4224  @Override
4225  protected PowerDouble_xzy instantiate_dyn(@Prototype PowerDouble_xzy this, PptSlice slice) {
4226    return new PowerDouble_xzy (slice);
4227  }
4228
4229  private PowerDouble_xzy (PptSlice slice) {
4230    super(slice);
4231  }
4232
4233  public @Prototype PowerDouble_xzy () {
4234    super();
4235  }
4236
4237  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
4238
4239  @Override
4240  public String[] get_method_name(@GuardSatisfied PowerDouble_xzy this) {
4241    return method_name;
4242  }
4243
4244  private static int function_id = -1;
4245
4246  @Override
4247  public int get_function_id() {
4248    return function_id;
4249  }
4250
4251  @Override
4252  public void set_function_id(int function_id) {
4253    assert PowerDouble_xzy.function_id == -1;
4254    PowerDouble_xzy.function_id = function_id;
4255  }
4256
4257  private static int var_order = 4;
4258
4259  @Override
4260  public int get_var_order(@GuardSatisfied PowerDouble_xzy this) {
4261    return var_order;
4262  }
4263
4264  @Pure
4265  @Override
4266  public boolean is_symmetric() {
4267
4268      return false;
4269  }
4270
4271  @Override
4272
4273  public double func(double z, double y) {
4274
4275    return Math.pow(z, y);
4276  }
4277
4278  @Override
4279  public InvariantStatus check_modified(double x, double y,
4280                                      double z, int count) {
4281    return check_ordered(x, z, y, count);
4282  }
4283
4284  @Override
4285  public InvariantStatus add_modified(double x, double y,
4286                                      double z, int count) {
4287    if (Debug.logDetail()) {
4288      log("result=%s, arg1=%s, arg2=%s", x, z, y);
4289    }
4290    return add_ordered(x, z, y, count);
4291  }
4292
4293  @Pure
4294  @Override
4295  public boolean isPower() {
4296    return true;
4297  }
4298
4299  @Pure
4300  @Override
4301  public boolean isExact() {
4302    return true;
4303  }
4304
4305  /** Returns a list of non-instantiating suppressions for this invariant. */
4306  @Pure
4307  @Override
4308  public @Nullable NISuppressionSet get_ni_suppressions() {
4309    if (NIS.dkconfig_enabled && dkconfig_enabled) {
4310      return suppressions;
4311    } else {
4312      return null;
4313    }
4314  }
4315
4316  /** definition of this invariant (the suppressee) */
4317  private static NISuppressee suppressee = new NISuppressee(PowerDouble_xzy.class, 3);
4318
4319  // suppressor definitions (used below)
4320  private static NISuppressor result_eq_arg1 =
4321      new NISuppressor(0, 2, FloatEqual.class);
4322  private static NISuppressor result_eq_arg2 =
4323      new NISuppressor(0, 1, FloatEqual.class);
4324  private static NISuppressor arg1_eq_arg2 =
4325      new NISuppressor(2, 1, FloatEqual.class);
4326
4327  private static NISuppressor result_lt_arg1 =
4328      new NISuppressor(0, 2, FloatLessThan.class);
4329  private static NISuppressor result_lt_arg2 =
4330      new NISuppressor(0, 1, FloatLessThan.class);
4331  private static NISuppressor arg1_lt_arg2 =
4332      new NISuppressor(2, 1, FloatLessThan.class);
4333  private static NISuppressor arg2_lt_arg1 =
4334      new NISuppressor(1, 2, FloatLessThan.class);
4335
4336  private static NISuppressor result_le_arg1 =
4337      new NISuppressor(0, 2, FloatLessEqual.class);
4338  private static NISuppressor result_le_arg2 =
4339      new NISuppressor(0, 1, FloatLessEqual.class);
4340  private static NISuppressor arg1_le_arg2 =
4341      new NISuppressor(2, 1, FloatLessEqual.class);
4342  private static NISuppressor arg2_le_arg1 =
4343      new NISuppressor(1, 2, FloatLessEqual.class);
4344
4345  private static NISuppressor result_track0_arg1 =
4346      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
4347  private static NISuppressor result_track0_arg2 =
4348      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
4349  private static NISuppressor arg1_track0_arg2 =
4350      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
4351  private static NISuppressor arg1_track0_result =
4352      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
4353  private static NISuppressor arg2_track0_result =
4354      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
4355  private static NISuppressor arg2_track0_arg1 =
4356      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
4357
4358  private static NISuppressor result_eq_1 =
4359      new NISuppressor(0, RangeFloat.EqualOne.class);
4360  private static NISuppressor arg1_eq_1 =
4361      new NISuppressor(2, RangeFloat.EqualOne.class);
4362  private static NISuppressor arg2_eq_1 =
4363      new NISuppressor(1, RangeFloat.EqualOne.class);
4364
4365  private static NISuppressor result_eq_0 =
4366      new NISuppressor(0, RangeFloat.EqualZero.class);
4367  private static NISuppressor arg1_eq_0 =
4368      new NISuppressor(2, RangeFloat.EqualZero.class);
4369  private static NISuppressor arg2_eq_0 =
4370      new NISuppressor(1, RangeFloat.EqualZero.class);
4371
4372  private static NISuppressor result_ne_0 =
4373      new NISuppressor(0, NonZeroFloat.class);
4374  private static NISuppressor arg1_ne_0 =
4375      new NISuppressor(2, NonZeroFloat.class);
4376  private static NISuppressor arg2_ne_0 =
4377      new NISuppressor(1, NonZeroFloat.class);
4378
4379  private static NISuppressor result_ge_0 =
4380      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
4381  private static NISuppressor arg1_ge_0 =
4382      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
4383  private static NISuppressor arg2_ge_0 =
4384      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
4385
4386  private static NISuppressor result_ge_64 =
4387      new NISuppressor(0, RangeInt.GreaterEqual64.class);
4388  private static NISuppressor arg1_ge_64 =
4389      new NISuppressor(2, RangeInt.GreaterEqual64.class);
4390  private static NISuppressor arg2_ge_64 =
4391      new NISuppressor(1, RangeInt.GreaterEqual64.class);
4392
4393    // Note that any suppression that doesn't limit y to valid exponents
4394    // (>= 0), must check for valid exponents as well (so that the invariant
4395    // is correctly destroyed on invalid exponents)
4396    //
4397    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
4398    // Another interesting artificat of pow is that for any even base, any
4399    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
4400    // (at least for integers)
4401
4402    private static NISuppressionSet suppressions =
4403      new NISuppressionSet(
4404          new NISuppression[] {
4405
4406            // (r == 1) && (y == 0) ==> r = pow (z, y)
4407            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
4408
4409            // (r == 1) && (z == 1) && (y >= 0)   ==> r = pow (z, y)
4410            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
4411
4412            // (r == 0) && (z == 0) && (y > 0)
4413            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
4414                              suppressee),
4415
4416            // (r == z) && (y == 1)    ==> r = pow (z, y)
4417            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
4418
4419          });
4420
4421  // Create a suppression factory for functionBinary
4422
4423}
4424
4425/**
4426 * Represents the invariant {@code y = Power(z, x)} over three double
4427 * scalars. 
4428 */
4429public static class PowerDouble_yzx extends FunctionBinaryFloat {
4430  // We are Serializable, so we specify a version to allow changes to
4431  // method signatures without breaking serialization.  If you add or
4432  // remove fields, you should change this number to the current date.
4433  static final long serialVersionUID = 20031030L;
4434
4435  private static @Prototype PowerDouble_yzx proto = new @Prototype PowerDouble_yzx ();
4436
4437  /** Returns the prototype invariant for PowerDouble_yzx */
4438  public static @Prototype PowerDouble_yzx get_proto() {
4439    return proto;
4440  }
4441
4442  /** instantiate an invariant on the specified slice */
4443  @Override
4444  protected PowerDouble_yzx instantiate_dyn(@Prototype PowerDouble_yzx this, PptSlice slice) {
4445    return new PowerDouble_yzx (slice);
4446  }
4447
4448  private PowerDouble_yzx (PptSlice slice) {
4449    super(slice);
4450  }
4451
4452  public @Prototype PowerDouble_yzx () {
4453    super();
4454  }
4455
4456  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
4457
4458  @Override
4459  public String[] get_method_name(@GuardSatisfied PowerDouble_yzx this) {
4460    return method_name;
4461  }
4462
4463  private static int function_id = -1;
4464
4465  @Override
4466  public int get_function_id() {
4467    return function_id;
4468  }
4469
4470  @Override
4471  public void set_function_id(int function_id) {
4472    assert PowerDouble_yzx.function_id == -1;
4473    PowerDouble_yzx.function_id = function_id;
4474  }
4475
4476  private static int var_order = 5;
4477
4478  @Override
4479  public int get_var_order(@GuardSatisfied PowerDouble_yzx this) {
4480    return var_order;
4481  }
4482
4483  @Pure
4484  @Override
4485  public boolean is_symmetric() {
4486
4487      return false;
4488  }
4489
4490  @Override
4491
4492  public double func(double z, double x) {
4493
4494    return Math.pow(z, x);
4495  }
4496
4497  @Override
4498  public InvariantStatus check_modified(double x, double y,
4499                                      double z, int count) {
4500    return check_ordered(y, z, x, count);
4501  }
4502
4503  @Override
4504  public InvariantStatus add_modified(double x, double y,
4505                                      double z, int count) {
4506    if (Debug.logDetail()) {
4507      log("result=%s, arg1=%s, arg2=%s", y, z, x);
4508    }
4509    return add_ordered(y, z, x, count);
4510  }
4511
4512  @Pure
4513  @Override
4514  public boolean isPower() {
4515    return true;
4516  }
4517
4518  @Pure
4519  @Override
4520  public boolean isExact() {
4521    return true;
4522  }
4523
4524  /** Returns a list of non-instantiating suppressions for this invariant. */
4525  @Pure
4526  @Override
4527  public @Nullable NISuppressionSet get_ni_suppressions() {
4528    if (NIS.dkconfig_enabled && dkconfig_enabled) {
4529      return suppressions;
4530    } else {
4531      return null;
4532    }
4533  }
4534
4535  /** definition of this invariant (the suppressee) */
4536  private static NISuppressee suppressee = new NISuppressee(PowerDouble_yzx.class, 3);
4537
4538  // suppressor definitions (used below)
4539  private static NISuppressor result_eq_arg1 =
4540      new NISuppressor(1, 2, FloatEqual.class);
4541  private static NISuppressor result_eq_arg2 =
4542      new NISuppressor(1, 0, FloatEqual.class);
4543  private static NISuppressor arg1_eq_arg2 =
4544      new NISuppressor(2, 0, FloatEqual.class);
4545
4546  private static NISuppressor result_lt_arg1 =
4547      new NISuppressor(1, 2, FloatLessThan.class);
4548  private static NISuppressor result_lt_arg2 =
4549      new NISuppressor(1, 0, FloatLessThan.class);
4550  private static NISuppressor arg1_lt_arg2 =
4551      new NISuppressor(2, 0, FloatLessThan.class);
4552  private static NISuppressor arg2_lt_arg1 =
4553      new NISuppressor(0, 2, FloatLessThan.class);
4554
4555  private static NISuppressor result_le_arg1 =
4556      new NISuppressor(1, 2, FloatLessEqual.class);
4557  private static NISuppressor result_le_arg2 =
4558      new NISuppressor(1, 0, FloatLessEqual.class);
4559  private static NISuppressor arg1_le_arg2 =
4560      new NISuppressor(2, 0, FloatLessEqual.class);
4561  private static NISuppressor arg2_le_arg1 =
4562      new NISuppressor(0, 2, FloatLessEqual.class);
4563
4564  private static NISuppressor result_track0_arg1 =
4565      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
4566  private static NISuppressor result_track0_arg2 =
4567      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
4568  private static NISuppressor arg1_track0_arg2 =
4569      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
4570  private static NISuppressor arg1_track0_result =
4571      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
4572  private static NISuppressor arg2_track0_result =
4573      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
4574  private static NISuppressor arg2_track0_arg1 =
4575      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
4576
4577  private static NISuppressor result_eq_1 =
4578      new NISuppressor(1, RangeFloat.EqualOne.class);
4579  private static NISuppressor arg1_eq_1 =
4580      new NISuppressor(2, RangeFloat.EqualOne.class);
4581  private static NISuppressor arg2_eq_1 =
4582      new NISuppressor(0, RangeFloat.EqualOne.class);
4583
4584  private static NISuppressor result_eq_0 =
4585      new NISuppressor(1, RangeFloat.EqualZero.class);
4586  private static NISuppressor arg1_eq_0 =
4587      new NISuppressor(2, RangeFloat.EqualZero.class);
4588  private static NISuppressor arg2_eq_0 =
4589      new NISuppressor(0, RangeFloat.EqualZero.class);
4590
4591  private static NISuppressor result_ne_0 =
4592      new NISuppressor(1, NonZeroFloat.class);
4593  private static NISuppressor arg1_ne_0 =
4594      new NISuppressor(2, NonZeroFloat.class);
4595  private static NISuppressor arg2_ne_0 =
4596      new NISuppressor(0, NonZeroFloat.class);
4597
4598  private static NISuppressor result_ge_0 =
4599      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
4600  private static NISuppressor arg1_ge_0 =
4601      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
4602  private static NISuppressor arg2_ge_0 =
4603      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
4604
4605  private static NISuppressor result_ge_64 =
4606      new NISuppressor(1, RangeInt.GreaterEqual64.class);
4607  private static NISuppressor arg1_ge_64 =
4608      new NISuppressor(2, RangeInt.GreaterEqual64.class);
4609  private static NISuppressor arg2_ge_64 =
4610      new NISuppressor(0, RangeInt.GreaterEqual64.class);
4611
4612    // Note that any suppression that doesn't limit x to valid exponents
4613    // (>= 0), must check for valid exponents as well (so that the invariant
4614    // is correctly destroyed on invalid exponents)
4615    //
4616    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
4617    // Another interesting artificat of pow is that for any even base, any
4618    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
4619    // (at least for integers)
4620
4621    private static NISuppressionSet suppressions =
4622      new NISuppressionSet(
4623          new NISuppression[] {
4624
4625            // (r == 1) && (x == 0) ==> r = pow (z, x)
4626            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
4627
4628            // (r == 1) && (z == 1) && (x >= 0)   ==> r = pow (z, x)
4629            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
4630
4631            // (r == 0) && (z == 0) && (x > 0)
4632            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
4633                              suppressee),
4634
4635            // (r == z) && (x == 1)    ==> r = pow (z, x)
4636            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
4637
4638          });
4639
4640  // Create a suppression factory for functionBinary
4641
4642}
4643
4644/**
4645 * Represents the invariant {@code z = Power(y, x)} over three double
4646 * scalars. 
4647 */
4648public static class PowerDouble_zyx extends FunctionBinaryFloat {
4649  // We are Serializable, so we specify a version to allow changes to
4650  // method signatures without breaking serialization.  If you add or
4651  // remove fields, you should change this number to the current date.
4652  static final long serialVersionUID = 20031030L;
4653
4654  private static @Prototype PowerDouble_zyx proto = new @Prototype PowerDouble_zyx ();
4655
4656  /** Returns the prototype invariant for PowerDouble_zyx */
4657  public static @Prototype PowerDouble_zyx get_proto() {
4658    return proto;
4659  }
4660
4661  /** instantiate an invariant on the specified slice */
4662  @Override
4663  protected PowerDouble_zyx instantiate_dyn(@Prototype PowerDouble_zyx this, PptSlice slice) {
4664    return new PowerDouble_zyx (slice);
4665  }
4666
4667  private PowerDouble_zyx (PptSlice slice) {
4668    super(slice);
4669  }
4670
4671  public @Prototype PowerDouble_zyx () {
4672    super();
4673  }
4674
4675  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};
4676
4677  @Override
4678  public String[] get_method_name(@GuardSatisfied PowerDouble_zyx this) {
4679    return method_name;
4680  }
4681
4682  private static int function_id = -1;
4683
4684  @Override
4685  public int get_function_id() {
4686    return function_id;
4687  }
4688
4689  @Override
4690  public void set_function_id(int function_id) {
4691    assert PowerDouble_zyx.function_id == -1;
4692    PowerDouble_zyx.function_id = function_id;
4693  }
4694
4695  private static int var_order = 6;
4696
4697  @Override
4698  public int get_var_order(@GuardSatisfied PowerDouble_zyx this) {
4699    return var_order;
4700  }
4701
4702  @Pure
4703  @Override
4704  public boolean is_symmetric() {
4705
4706      return false;
4707  }
4708
4709  @Override
4710
4711  public double func(double y, double x) {
4712
4713    return Math.pow(y, x);
4714  }
4715
4716  @Override
4717  public InvariantStatus check_modified(double x, double y,
4718                                      double z, int count) {
4719    return check_ordered(z, y, x, count);
4720  }
4721
4722  @Override
4723  public InvariantStatus add_modified(double x, double y,
4724                                      double z, int count) {
4725    if (Debug.logDetail()) {
4726      log("result=%s, arg1=%s, arg2=%s", z, y, x);
4727    }
4728    return add_ordered(z, y, x, count);
4729  }
4730
4731  @Pure
4732  @Override
4733  public boolean isPower() {
4734    return true;
4735  }
4736
4737  @Pure
4738  @Override
4739  public boolean isExact() {
4740    return true;
4741  }
4742
4743  /** Returns a list of non-instantiating suppressions for this invariant. */
4744  @Pure
4745  @Override
4746  public @Nullable NISuppressionSet get_ni_suppressions() {
4747    if (NIS.dkconfig_enabled && dkconfig_enabled) {
4748      return suppressions;
4749    } else {
4750      return null;
4751    }
4752  }
4753
4754  /** definition of this invariant (the suppressee) */
4755  private static NISuppressee suppressee = new NISuppressee(PowerDouble_zyx.class, 3);
4756
4757  // suppressor definitions (used below)
4758  private static NISuppressor result_eq_arg1 =
4759      new NISuppressor(2, 1, FloatEqual.class);
4760  private static NISuppressor result_eq_arg2 =
4761      new NISuppressor(2, 0, FloatEqual.class);
4762  private static NISuppressor arg1_eq_arg2 =
4763      new NISuppressor(1, 0, FloatEqual.class);
4764
4765  private static NISuppressor result_lt_arg1 =
4766      new NISuppressor(2, 1, FloatLessThan.class);
4767  private static NISuppressor result_lt_arg2 =
4768      new NISuppressor(2, 0, FloatLessThan.class);
4769  private static NISuppressor arg1_lt_arg2 =
4770      new NISuppressor(1, 0, FloatLessThan.class);
4771  private static NISuppressor arg2_lt_arg1 =
4772      new NISuppressor(0, 1, FloatLessThan.class);
4773
4774  private static NISuppressor result_le_arg1 =
4775      new NISuppressor(2, 1, FloatLessEqual.class);
4776  private static NISuppressor result_le_arg2 =
4777      new NISuppressor(2, 0, FloatLessEqual.class);
4778  private static NISuppressor arg1_le_arg2 =
4779      new NISuppressor(1, 0, FloatLessEqual.class);
4780  private static NISuppressor arg2_le_arg1 =
4781      new NISuppressor(0, 1, FloatLessEqual.class);
4782
4783  private static NISuppressor result_track0_arg1 =
4784      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
4785  private static NISuppressor result_track0_arg2 =
4786      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
4787  private static NISuppressor arg1_track0_arg2 =
4788      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
4789  private static NISuppressor arg1_track0_result =
4790      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
4791  private static NISuppressor arg2_track0_result =
4792      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
4793  private static NISuppressor arg2_track0_arg1 =
4794      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
4795
4796  private static NISuppressor result_eq_1 =
4797      new NISuppressor(2, RangeFloat.EqualOne.class);
4798  private static NISuppressor arg1_eq_1 =
4799      new NISuppressor(1, RangeFloat.EqualOne.class);
4800  private static NISuppressor arg2_eq_1 =
4801      new NISuppressor(0, RangeFloat.EqualOne.class);
4802
4803  private static NISuppressor result_eq_0 =
4804      new NISuppressor(2, RangeFloat.EqualZero.class);
4805  private static NISuppressor arg1_eq_0 =
4806      new NISuppressor(1, RangeFloat.EqualZero.class);
4807  private static NISuppressor arg2_eq_0 =
4808      new NISuppressor(0, RangeFloat.EqualZero.class);
4809
4810  private static NISuppressor result_ne_0 =
4811      new NISuppressor(2, NonZeroFloat.class);
4812  private static NISuppressor arg1_ne_0 =
4813      new NISuppressor(1, NonZeroFloat.class);
4814  private static NISuppressor arg2_ne_0 =
4815      new NISuppressor(0, NonZeroFloat.class);
4816
4817  private static NISuppressor result_ge_0 =
4818      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
4819  private static NISuppressor arg1_ge_0 =
4820      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
4821  private static NISuppressor arg2_ge_0 =
4822      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
4823
4824  private static NISuppressor result_ge_64 =
4825      new NISuppressor(2, RangeInt.GreaterEqual64.class);
4826  private static NISuppressor arg1_ge_64 =
4827      new NISuppressor(1, RangeInt.GreaterEqual64.class);
4828  private static NISuppressor arg2_ge_64 =
4829      new NISuppressor(0, RangeInt.GreaterEqual64.class);
4830
4831    // Note that any suppression that doesn't limit x to valid exponents
4832    // (>= 0), must check for valid exponents as well (so that the invariant
4833    // is correctly destroyed on invalid exponents)
4834    //
4835    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
4836    // Another interesting artificat of pow is that for any even base, any
4837    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
4838    // (at least for integers)
4839
4840    private static NISuppressionSet suppressions =
4841      new NISuppressionSet(
4842          new NISuppression[] {
4843
4844            // (r == 1) && (x == 0) ==> r = pow (y, x)
4845            new NISuppression(result_eq_1, arg2_eq_0, suppressee),
4846
4847            // (r == 1) && (y == 1) && (x >= 0)   ==> r = pow (y, x)
4848            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),
4849
4850            // (r == 0) && (y == 0) && (x > 0)
4851            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
4852                              suppressee),
4853
4854            // (r == y) && (x == 1)    ==> r = pow (y, x)
4855            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
4856
4857          });
4858
4859  // Create a suppression factory for functionBinary
4860
4861}
4862
4863}