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