// ***** This file is automatically generated from FunctionBinary.java.jpp
// ***** (and files it recursively includes).

package daikon.inv.ternary.threeScalar;

import daikon.*;
import daikon.derive.unary.*;
import daikon.inv.*;
import daikon.inv.binary.twoScalar.*;
import daikon.inv.unary.scalar.*;
import daikon.suppress.*;
import java.lang.reflect.*;
import java.util.*;
import java.util.logging.Logger;
import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.plumelib.util.ArraysPlume;
import org.plumelib.util.MathPlume;
import typequals.prototype.qual.NonPrototype;
import typequals.prototype.qual.Prototype;

/**
 * Base class for each of the FunctionBinaryFloat functions and permutatons. Most of the work is done
 * here. The subclasses basically define the function and return information describing the function
 * and permutation to these methods.
 */
@SuppressWarnings("UnusedVariable")  // generated code, complex rules for when var is used
public abstract class FunctionBinaryFloat extends ThreeFloat {
  static final long serialVersionUID = 20031030L;

  /** Boolean. True if FunctionBinaryFloat invariants should be considered. */
  public static boolean dkconfig_enabled = false;

  public static Logger debug =
    Logger.getLogger("daikon.inv.ternary.threeScalar.#CLASSNAME");

  static final int[][] var_indices;
  static {
    var_indices = new int[7][];
    var_indices[1] = new int[] { 0, 1, 2 };
    var_indices[2] = new int[] { 1, 0, 2 };
    var_indices[3] = new int[] { 2, 0, 1 };
    var_indices[4] = new int[] { 0, 2, 1 };
    var_indices[5] = new int[] { 1, 2, 0 };
    var_indices[6] = new int[] { 2, 1, 0 };
  }

  protected FunctionBinaryFloat(PptSlice ppt) {
    super(ppt);
  }

  protected @Prototype FunctionBinaryFloat() {
    super();
  }

  @Override
  public boolean enabled() {
    return dkconfig_enabled;
  }

  @Override
  public boolean instantiate_ok(VarInfo[] vis) {

    if (!valid_types(vis)) {
      return false;
    }

    // Make sure that each variable is integral (not boolean or hashcode)
    if (!vis[0].file_rep_type.isFloat()
        || !vis[1].file_rep_type.isFloat()
        || !vis[2].file_rep_type.isFloat())
      return false;

    return true;
  }

  // check_modified relies on func having no side effects.
  abstract double func(double arg1, double arg2);
  @Pure
  abstract boolean is_symmetric();
  abstract String[] get_method_name(@GuardSatisfied FunctionBinaryFloat this);
  abstract int get_var_order(@GuardSatisfied FunctionBinaryFloat this);
  abstract void set_function_id(int function_id);
  abstract int get_function_id();

  /**
   * Map from function name (eg, MultiplyLong, MinimumFloat) to an array of instances (one for each
   * valid permutation) for that function.
   */
  private static Map<String,@Prototype FunctionBinaryFloat[]> functions = new LinkedHashMap<>();

  /**
   * A list indexed by function number to an array of instances (one for each valid permutation) for
   * that function. The array is the same one as is stored in the functions Map. This provides a
   * faster access mechanism once we have the function id (which are calculated the first time
   * through).
   */
  private static List<@Prototype FunctionBinaryFloat[]> func_list = new ArrayList<>();

  private static void build_func_list() {

    // Reflection seems to confuse clover
    // CLOVER:OFF

    // Build the map of functions to array of instances for that function
    debug.fine("Processing FunctionBinaryFloat");
    functions = new LinkedHashMap<>();
    @SuppressWarnings("unchecked")
    Class<@Prototype FunctionBinaryFloat>[] subclasses = (Class<@Prototype FunctionBinaryFloat>[]) FunctionBinaryFloat.class.getDeclaredClasses();
    for (int ii = 0; ii < subclasses.length; ii++) {
      Class<@Prototype FunctionBinaryFloat> subc = subclasses[ii];
      String function = subc.getName();
      if (function.indexOf("CLOVER") >= 0) {
        continue;
      }
      function = function.replaceFirst(".*FunctionBinary\\$", "");
      function = function.replaceFirst("_.*", "");
      if (function.equals("SubClass")) {
        continue;
      }
      @Prototype FunctionBinaryFloat[] fb_arr = functions.get(function);
      if (fb_arr == null) {
        fb_arr = new @Prototype FunctionBinaryFloat[7];
        functions.put(function, fb_arr);
        func_list.add(fb_arr);
      }
      int func_id = func_list.indexOf(fb_arr);
      @SuppressWarnings({"nonprototype"})
      @Prototype FunctionBinaryFloat fb;
      try {
        Constructor<@Prototype FunctionBinaryFloat> con = subc.getDeclaredConstructor(new Class<?>[] {});
        fb = con.newInstance(new Object[] {});
      }  catch (Exception e) {
        throw new Error(" can't create instance for " + subc.getName()
                        + ": '" + e + "' ii = " + ii);
      }
      assert fb_arr[fb.get_var_order()] == null;
      fb_arr[fb.get_var_order()] = fb;
      fb.set_function_id(func_id);
      debug.fine("Adding " + function + " " + fb.getClass().getName()
                  + " " + fb.get_var_order() + " " + fb.get_function_id());
    }
    // CLOVER:ON
  }

  /** Returns a list of all of the FunctionBinaryFloat prototype invariants. */
  public static List<@Prototype Invariant> get_proto_all() {

    List<@Prototype Invariant> result = new ArrayList<>();

    // If this is the first call
    if (functions.isEmpty()) {
      build_func_list();
    }

    // Get the proto invariant for all of the subclasses and return them
    for (@Prototype FunctionBinaryFloat[] fb_arr : func_list) {
      for (int jj = 1; jj < fb_arr.length; jj++) {
        @Prototype FunctionBinaryFloat fb = fb_arr[jj];
        if (fb != null) {
          result.add(fb);
        }
      }
    }
    return result;
  }

  /** Permuted result var. */
  public VarInfo resultVar() {
    return ppt.var_infos[var_indices[get_var_order()][0]];
  }

  /** Permuted arg1 var. */
  public VarInfo argVar1() {
    return ppt.var_infos[var_indices[get_var_order()][1]];
  }

  /** Permuted arg2 var. */
  public VarInfo argVar2() {
    return ppt.var_infos[var_indices[get_var_order()][2]];
  }

  /**
   * Apply the specified sample to the function, returning the result. The caller is responsible
   * for permuting the arguments.
   */
  public InvariantStatus check_ordered(double result, double arg1,
                                      double arg2, int count) {
    // This implementation relies on func having no side effects.
    try {
      if (!Global.fuzzy.eq(result, func(arg1, arg2))) {
        return InvariantStatus.FALSIFIED;
      }
    } catch (Exception e) {
        return InvariantStatus.FALSIFIED;
    }
    return InvariantStatus.NO_CHANGE;
  }

  /**
   * Apply the specified sample to the function, returning the result. The caller is responsible
   * for permuting the arguments.
   */
  public InvariantStatus add_ordered(double result, double arg1,
                                      double arg2, int count) {
    return check_ordered(result, arg1, arg2, count);
  }

  /**
   * Reorganize our already-seen state as if the variables had shifted order underneath us
   * (re-arrangement given by the permutation). We accomplish this by returning the class that
   * corresponds to the new permutation.
   */
  @Override
  protected Invariant resurrect_done(int[] permutation) {

    assert permutation.length == 3;
    assert ArraysPlume.fnIsPermutation(permutation);

    int[] new_order = new int[3];
    int[] old_order = var_indices[get_var_order()];

    // "permutation" is a permutation on the var_info array. old_order
    // was the permutation that took the formatted invariant to the
    // var_info array, so old_order^-1 is the permutation from the
    // var_info array to the old formatted invariant. We want to find
    // a new_order so that when we first do "permutation", then
    // apply the new permutation from the var_info array to the
    // formatted invariant, we get the same formatted invariant.
    // What we want, then. is:
    //    new_order^-1 o permutation = old_order^-1
    // rearranging, this is equivalent to
    //    new_order = permutation o old_order
    new_order[0] = permutation[old_order[0]];
    new_order[1] = permutation[old_order[1]];
    new_order[2] = permutation[old_order[2]];

    // Force symmetric functions into a canonical form so that
    // we can match them when necessary and they always print the same.
    // For example, order of 0, 1, 2 and 0, 2, 1 represent the same
    // invariant for a symmetric function.  This forces them to always
    // be represented as 0, 1, 2
    if (is_symmetric()) {
      if (new_order[2] < new_order[1]) {
        int tmp = new_order[2];
        new_order[2] = new_order[1];
        new_order[1] = tmp;
      }
    }

    // Look for the new order in the list of possible orders
    int var_order = -1;
    for (int i = 0; i < var_indices.length; i++) {
      if (Arrays.equals(new_order, var_indices[i])) {
        var_order = i;
        break;
      }
    }
    assert var_order != -1;

    // If the var order hasn't changed, we don't need to do anything
    if (var_order == get_var_order()) {
      return this;
    }

    // Find the class that corresponds to the new order
    if (functions.isEmpty()) {
      build_func_list();
    }
    int func_id = get_function_id();
    @Prototype FunctionBinaryFloat[] fb_arr = func_list.get(func_id);
    assert fb_arr != null;
    for (int ii = 0; ii < fb_arr.length; ii++) {
      if ((fb_arr[ii] != null) && (fb_arr[ii].get_var_order() == var_order)) {
        return fb_arr[ii].instantiate_dyn(ppt);
      }
    }

    throw new Error("Could not find new ordering");
  }

  @Override
  public String repr(@GuardSatisfied FunctionBinaryFloat this) {
    return format();
  }

  @SideEffectFree
  @Override
  public String format_using(@GuardSatisfied FunctionBinaryFloat this, OutputFormat format) {
    if (format == OutputFormat.SIMPLIFY) {
      return format_simplify();
    }
    if (format == OutputFormat.CSHARPCONTRACT) {
      return format_csharp_contract();
    }

    int var_order = get_var_order();
    String[] methodname = get_method_name();

    VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]];
    VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]];
    VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]];

    String argresult_name = argresultvi.name_using(format);
    String arg1_name = arg1vi.name_using(format);
    String arg2_name = arg2vi.name_using(format);

    if (format == OutputFormat.DAIKON) {
      return argresult_name + " == (" + methodname[0] + arg1_name
        + methodname[1] + arg2_name + methodname[2] + ")";
    }

    if (format.isJavaFamily()) {
      if (methodname[1].equals(" || ") || methodname[1].equals(" && ")) {
        return "(" +  argresult_name + " != 0) == ((" + methodname[0] + arg1_name + " != 0)"
          + methodname[1] + "(" + arg2_name + methodname[2] + " != 0))";
      } else {
        return argresult_name + " == (" + methodname[0] + arg1_name
          + methodname[1] + arg2_name + methodname[2] + ")";
      }
    }

    return format_unimplemented(format);
  }

  public String format_simplify(@GuardSatisfied FunctionBinaryFloat this) {
    int var_order = get_var_order();
    String[] methodname = get_method_name();
    VarInfo[] vis = ppt.var_infos;

    String result = vis[var_indices[var_order][0]].simplifyFixedupName();
    String arg1 = vis[var_indices[var_order][1]].simplifyFixedupName();
    String arg2 = vis[var_indices[var_order][2]].simplifyFixedupName();
    String func = null;
    if (methodname[1].equals(" * ")) {
      func = "*";
    } else if (methodname[1].equals(" | ")) {
      func = "|java-bitwise-or|";
    } else if (methodname[1].equals(" || ")) {
      func = "|java-logical-or|";
    } else if (methodname[1].equals(", ")) {
      if (methodname[0].equals("java.lang.Math.min(")) {
        func = "min";
      } else if (methodname[0].equals("java.lang.Math.max(")) {
        func = "max";
      } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) {
        func = "gcd";
      } else if (methodname[0].equals("java.lang.Math.pow(")) {
        func = "pow";
      } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) {
        func = "|java-logical-xor|";
      }
    } else {
      assert methodname[0].equals("");
      assert methodname[2].equals("");
      func = "|java-" + methodname[1].trim() + "|";
    }
    if (func == null) {
      return "format_simplify_contract() doesn't know function " + methodname[0] + "-"
        + methodname[1] + "-" + methodname[2];
    }
    return "(EQ " + result + " (" + func + " " + arg1 + " " + arg2 + "))";
  }

  public String format_csharp_contract(@GuardSatisfied FunctionBinaryFloat this) {
    int var_order = get_var_order();
    String[] methodname = get_method_name();

    VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]];
    VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]];
    VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]];
    String result = argresultvi.csharp_name();
    String arg1 = arg1vi.csharp_name();
    String arg2 = arg2vi.csharp_name();
    String operator = null;

    if (methodname[1].equals(" * ")) {
      operator = "*";
    } else if (methodname[1].equals(" | ")) {
      operator = "|";
    } else if (methodname[1].equals(" & ")) {
      operator = "&";
    } else if (methodname[1].equals(" / ")) {
      operator = "/";
    } else if (methodname[1].equals(" ^ ")) {
      operator = "^";
    } else if (methodname[1].equals(" % ")) {
      operator = "%";
    } else if (methodname[1].equals(" && ")) {
      operator = "&&";
    } else if (methodname[1].equals(" || ")) {
      operator = "||";
    } else if (methodname[1].equals(" >> ")) {
      operator = ">>";
    } else if (methodname[1].equals(" >>> ")) {
      return result + " == " + arg1 + ".UnsignedRightShift(" + arg2 + ")";
      //return result + " == CSharpDaikonLib.Extensions.UnsignedRightShift(" + arg1 + ", " + arg2 + ")";
    } else if (methodname[1].equals(" << ")) {
      operator = "<<";
    }

    if (operator != null) {
      return result + " == (" + arg1 + " " + operator + " " + arg2 + ")";
    }

    String func = null;
    if (methodname[1].equals(", ")) {
      if (methodname[0].equals("java.lang.Math.min(")) {
        func = "Math.Min";
      } else if (methodname[0].equals("java.lang.Math.max(")) {
        func = "Math.Max";
      } else if (methodname[0].equals("org.plumelib.util.MathPlume.gcd(")) {
        return result + " == CSharpDaikonLib.Extensions.GCD(" + arg1 + ", " + arg2 + ")";
      } else if (methodname[0].equals("java.lang.Math.pow(")) {
        return result + " == " + arg1 + ".Pow(" + arg2 + ")";
      } else if (methodname[0].equals("org.plumelib.util.MathPlume.logicalXor(")) {
        return result + " == (" + arg1 + " ^ " + arg2 + ")";
      }
    } else {
      assert methodname[0].equals("");
      assert methodname[2].equals("");
      func = "|" + methodname[1].trim() + "|";
    }

    if (func == null) {
      return "format_csharp_contract() doesn't know function " + methodname[0] + "-" + methodname[1] + "-" + methodname[2];
    }
    return result + " == " + func + "(" + arg1 + ", " + arg2 + ")";
  }

  // If our classes match, we must match
  @Pure
  @Override
  public boolean isSameFormula(Invariant other) {
    return true;
  }
  @Override
  public double computeConfidence() {
    if (logOn()) {
      VarInfo v1 = ppt.var_infos[0];
      VarInfo v2 = ppt.var_infos[1];
      VarInfo v3 = ppt.var_infos[2];
      log("computeConfidence(%s: num_values = %s, num_values(%s)=%s, num_values(%s)=%s, num_values(%s)=%s",
          format(), ppt.num_values(),
          v1.name(), ppt.parent.num_values(v1),
          v2.name(), ppt.parent.num_values(v2),
          v3.name(), ppt.parent.num_values(v3));
    }
    return Invariant.conf_is_ge(ppt.num_values(), 5);
  }

  /** If the arg is a sequence size, return the sequence; otherwise return null. */
  private @Nullable VarInfo sized_sequence(VarInfo size) {
    if (size.derived instanceof SequenceLength) {
      return ((SequenceLength)size.derived).base;
    }
    return null;
  }

  @Pure
  @Override
  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {

    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    // Discard if any two of the three variables are the sizes of the
    // same arrays.
    VarInfo arr1 = sized_sequence(vis[0]);
    VarInfo arr2 = sized_sequence(vis[1]);
    VarInfo arr3 = sized_sequence(vis[2]);
    if (((arr1 != null) && (arr1 == arr2))
        || ((arr1 != null) && (arr1 == arr3))
        || ((arr2 != null) && (arr2 == arr3))) {
      return new DiscardInfo(this, DiscardCode.obvious,
                    "two are sizes of same array:  "
                    + vis[0].name() + " "
                    + vis[1].name() + " "
                    + vis[2].name());
    }

    return null;
  }

  // default is that it is not this function, overridden in the subclass
  @Pure
  public boolean isMultiply() {
    return false;
  }

/**
 * Represents the invariant {@code x = Multiply(y, z)} over three double
 * scalars. 
 */
public static class MultiplyDouble_xyz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MultiplyDouble_xyz proto = new @Prototype MultiplyDouble_xyz ();

  /** Returns the prototype invariant for MultiplyDouble_xyz */
  public static @Prototype MultiplyDouble_xyz get_proto() {
    return proto;
  }

  @Override
  protected MultiplyDouble_xyz instantiate_dyn(@Prototype MultiplyDouble_xyz this, PptSlice slice) {
    return new MultiplyDouble_xyz (slice);
  }

  private MultiplyDouble_xyz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MultiplyDouble_xyz () {
    super();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied MultiplyDouble_xyz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MultiplyDouble_xyz.function_id == -1;
    MultiplyDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  @Override
  public int get_var_order(@GuardSatisfied MultiplyDouble_xyz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double y, double z) {

    return y * z;
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, y, z);
    }
    return add_ordered(x, y, z, count);
  }

  @Pure
  @Override
  public boolean isMultiply() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 0) && (y == 0) ==> r = y * z
            new NISuppression(result_eq_0, arg1_eq_0, suppressee),

            // (r == 0) && (z == 0) ==> r = y * z
            new NISuppression(result_eq_0, arg2_eq_0, suppressee),

            // (r == y) && (z == 1) ==> r = y * z
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

            // (r == z) && (y == 1) ==> r = y * z
            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Multiply(x, z)} over three double
 * scalars. 
 */
public static class MultiplyDouble_yxz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MultiplyDouble_yxz proto = new @Prototype MultiplyDouble_yxz ();

  /** Returns the prototype invariant for MultiplyDouble_yxz */
  public static @Prototype MultiplyDouble_yxz get_proto() {
    return proto;
  }

  @Override
  protected MultiplyDouble_yxz instantiate_dyn(@Prototype MultiplyDouble_yxz this, PptSlice slice) {
    return new MultiplyDouble_yxz (slice);
  }

  private MultiplyDouble_yxz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MultiplyDouble_yxz () {
    super();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied MultiplyDouble_yxz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MultiplyDouble_yxz.function_id == -1;
    MultiplyDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  @Override
  public int get_var_order(@GuardSatisfied MultiplyDouble_yxz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double z) {

    return x * z;
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, x, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, x, z);
    }
    return add_ordered(y, x, z, count);
  }

  @Pure
  @Override
  public boolean isMultiply() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 0) && (x == 0) ==> r = x * z
            new NISuppression(result_eq_0, arg1_eq_0, suppressee),

            // (r == 0) && (z == 0) ==> r = x * z
            new NISuppression(result_eq_0, arg2_eq_0, suppressee),

            // (r == x) && (z == 1) ==> r = x * z
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

            // (r == z) && (x == 1) ==> r = x * z
            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Multiply(x, y)} over three double
 * scalars. 
 */
public static class MultiplyDouble_zxy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MultiplyDouble_zxy proto = new @Prototype MultiplyDouble_zxy ();

  /** Returns the prototype invariant for MultiplyDouble_zxy */
  public static @Prototype MultiplyDouble_zxy get_proto() {
    return proto;
  }

  @Override
  protected MultiplyDouble_zxy instantiate_dyn(@Prototype MultiplyDouble_zxy this, PptSlice slice) {
    return new MultiplyDouble_zxy (slice);
  }

  private MultiplyDouble_zxy (PptSlice slice) {
    super(slice);
  }

  public @Prototype MultiplyDouble_zxy () {
    super();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied MultiplyDouble_zxy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MultiplyDouble_zxy.function_id == -1;
    MultiplyDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  @Override
  public int get_var_order(@GuardSatisfied MultiplyDouble_zxy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double y) {

    return x * y;
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, x, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, x, y);
    }
    return add_ordered(z, x, y, count);
  }

  @Pure
  @Override
  public boolean isMultiply() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MultiplyDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 0) && (x == 0) ==> r = x * y
            new NISuppression(result_eq_0, arg1_eq_0, suppressee),

            // (r == 0) && (y == 0) ==> r = x * y
            new NISuppression(result_eq_0, arg2_eq_0, suppressee),

            // (r == x) && (y == 1) ==> r = x * y
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

            // (r == y) && (x == 1) ==> r = x * y
            new NISuppression(result_eq_arg2, arg1_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

  // #define EQUALITY_MIN_MAX_SUPPRESS

  // default is that it is not this function, overridden in the subclass
  @Pure
  public boolean isMinimum() {
    return false;
  }

/**
 * Represents the invariant {@code x = Minimum(y, z)} over three double
 * scalars. 
 */
public static class MinimumDouble_xyz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MinimumDouble_xyz proto = new @Prototype MinimumDouble_xyz ();

  /** Returns the prototype invariant for MinimumDouble_xyz */
  public static @Prototype MinimumDouble_xyz get_proto() {
    return proto;
  }

  @Override
  protected MinimumDouble_xyz instantiate_dyn(@Prototype MinimumDouble_xyz this, PptSlice slice) {
    return new MinimumDouble_xyz (slice);
  }

  private MinimumDouble_xyz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MinimumDouble_xyz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MinimumDouble_xyz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MinimumDouble_xyz.function_id == -1;
    MinimumDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  @Override
  public int get_var_order(@GuardSatisfied MinimumDouble_xyz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double y, double z) {

    return Math.min(y, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, y, z);
    }
    return add_ordered(x, y, z, count);
  }

  @Pure
  @Override
  public boolean isMinimum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (x == y) && (y <= z) ==> r = min(y, z)
            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),

            // (x == z) && (z <= y) ==> r = min(y, z)
            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Minimum(x, z)} over three double
 * scalars. 
 */
public static class MinimumDouble_yxz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MinimumDouble_yxz proto = new @Prototype MinimumDouble_yxz ();

  /** Returns the prototype invariant for MinimumDouble_yxz */
  public static @Prototype MinimumDouble_yxz get_proto() {
    return proto;
  }

  @Override
  protected MinimumDouble_yxz instantiate_dyn(@Prototype MinimumDouble_yxz this, PptSlice slice) {
    return new MinimumDouble_yxz (slice);
  }

  private MinimumDouble_yxz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MinimumDouble_yxz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MinimumDouble_yxz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MinimumDouble_yxz.function_id == -1;
    MinimumDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  @Override
  public int get_var_order(@GuardSatisfied MinimumDouble_yxz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double z) {

    return Math.min(x, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, x, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, x, z);
    }
    return add_ordered(y, x, z, count);
  }

  @Pure
  @Override
  public boolean isMinimum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (y == x) && (x <= z) ==> r = min(x, z)
            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),

            // (y == z) && (z <= x) ==> r = min(x, z)
            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Minimum(x, y)} over three double
 * scalars. 
 */
public static class MinimumDouble_zxy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MinimumDouble_zxy proto = new @Prototype MinimumDouble_zxy ();

  /** Returns the prototype invariant for MinimumDouble_zxy */
  public static @Prototype MinimumDouble_zxy get_proto() {
    return proto;
  }

  @Override
  protected MinimumDouble_zxy instantiate_dyn(@Prototype MinimumDouble_zxy this, PptSlice slice) {
    return new MinimumDouble_zxy (slice);
  }

  private MinimumDouble_zxy (PptSlice slice) {
    super(slice);
  }

  public @Prototype MinimumDouble_zxy () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MinimumDouble_zxy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MinimumDouble_zxy.function_id == -1;
    MinimumDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  @Override
  public int get_var_order(@GuardSatisfied MinimumDouble_zxy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double y) {

    return Math.min(x, y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, x, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, x, y);
    }
    return add_ordered(z, x, y, count);
  }

  @Pure
  @Override
  public boolean isMinimum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MinimumDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (z == x) && (x <= y) ==> r = min(x, y)
            new NISuppression(result_eq_arg1, arg1_le_arg2, suppressee),

            // (z == y) && (y <= x) ==> r = min(x, y)
            new NISuppression(result_eq_arg2, arg2_le_arg1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

  // #define EQUALITY_MIN_MAX_SUPPRESS

  // default is that it is not this function, overridden in the subclass
  @Pure
  public boolean isMaximum() {
    return false;
  }

/**
 * Represents the invariant {@code x = Maximum(y, z)} over three double
 * scalars. 
 */
public static class MaximumDouble_xyz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MaximumDouble_xyz proto = new @Prototype MaximumDouble_xyz ();

  /** Returns the prototype invariant for MaximumDouble_xyz */
  public static @Prototype MaximumDouble_xyz get_proto() {
    return proto;
  }

  @Override
  protected MaximumDouble_xyz instantiate_dyn(@Prototype MaximumDouble_xyz this, PptSlice slice) {
    return new MaximumDouble_xyz (slice);
  }

  private MaximumDouble_xyz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MaximumDouble_xyz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MaximumDouble_xyz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MaximumDouble_xyz.function_id == -1;
    MaximumDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  @Override
  public int get_var_order(@GuardSatisfied MaximumDouble_xyz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double y, double z) {

    return Math.max(y, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, y, z);
    }
    return add_ordered(x, y, z, count);
  }

  @Pure
  @Override
  public boolean isMaximum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == y) && (z <= y) ==> r = max(y, z)
            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),

            // (r == z) && (y <= z) ==> r = max(y, z)
            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Maximum(x, z)} over three double
 * scalars. 
 */
public static class MaximumDouble_yxz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MaximumDouble_yxz proto = new @Prototype MaximumDouble_yxz ();

  /** Returns the prototype invariant for MaximumDouble_yxz */
  public static @Prototype MaximumDouble_yxz get_proto() {
    return proto;
  }

  @Override
  protected MaximumDouble_yxz instantiate_dyn(@Prototype MaximumDouble_yxz this, PptSlice slice) {
    return new MaximumDouble_yxz (slice);
  }

  private MaximumDouble_yxz (PptSlice slice) {
    super(slice);
  }

  public @Prototype MaximumDouble_yxz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MaximumDouble_yxz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MaximumDouble_yxz.function_id == -1;
    MaximumDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  @Override
  public int get_var_order(@GuardSatisfied MaximumDouble_yxz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double z) {

    return Math.max(x, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, x, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, x, z);
    }
    return add_ordered(y, x, z, count);
  }

  @Pure
  @Override
  public boolean isMaximum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == x) && (z <= x) ==> r = max(x, z)
            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),

            // (r == z) && (x <= z) ==> r = max(x, z)
            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Maximum(x, y)} over three double
 * scalars. 
 */
public static class MaximumDouble_zxy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype MaximumDouble_zxy proto = new @Prototype MaximumDouble_zxy ();

  /** Returns the prototype invariant for MaximumDouble_zxy */
  public static @Prototype MaximumDouble_zxy get_proto() {
    return proto;
  }

  @Override
  protected MaximumDouble_zxy instantiate_dyn(@Prototype MaximumDouble_zxy this, PptSlice slice) {
    return new MaximumDouble_zxy (slice);
  }

  private MaximumDouble_zxy (PptSlice slice) {
    super(slice);
  }

  public @Prototype MaximumDouble_zxy () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied MaximumDouble_zxy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert MaximumDouble_zxy.function_id == -1;
    MaximumDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  @Override
  public int get_var_order(@GuardSatisfied MaximumDouble_zxy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return true;
  }

  @Override

  public double func(double x, double y) {

    return Math.max(x, y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, x, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, x, y);
    }
    return add_ordered(z, x, y, count);
  }

  @Pure
  @Override
  public boolean isMaximum() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(MaximumDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == x) && (y <= x) ==> r = max(x, y)
            new NISuppression(result_eq_arg1, arg2_le_arg1, suppressee),

            // (r == y) && (x <= y) ==> r = max(x, y)
            new NISuppression(result_eq_arg2, arg1_le_arg2, suppressee),

          });

  // Create a suppression factory for functionBinary

}

  // default is that it is not this function, overridden in the subclass
  @Pure
  public boolean isDivision() {
    return false;
  }

/**
 * Represents the invariant {@code x = Division(y, z)} over three double
 * scalars. 
 */
public static class DivisionDouble_xyz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_xyz proto = new @Prototype DivisionDouble_xyz ();

  /** Returns the prototype invariant for DivisionDouble_xyz */
  public static @Prototype DivisionDouble_xyz get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_xyz instantiate_dyn(@Prototype DivisionDouble_xyz this, PptSlice slice) {
    return new DivisionDouble_xyz (slice);
  }

  private DivisionDouble_xyz (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_xyz () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_xyz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_xyz.function_id == -1;
    DivisionDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_xyz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double y, double z) {

    return (y / z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, y, z);
    }
    return add_ordered(x, y, z, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (y == z) && (z != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == y) && (z == 1) ==> r = y / z
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Division(x, z)} over three double
 * scalars. 
 */
public static class DivisionDouble_yxz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_yxz proto = new @Prototype DivisionDouble_yxz ();

  /** Returns the prototype invariant for DivisionDouble_yxz */
  public static @Prototype DivisionDouble_yxz get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_yxz instantiate_dyn(@Prototype DivisionDouble_yxz this, PptSlice slice) {
    return new DivisionDouble_yxz (slice);
  }

  private DivisionDouble_yxz (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_yxz () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_yxz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_yxz.function_id == -1;
    DivisionDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_yxz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double x, double z) {

    return (x / z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, x, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, x, z);
    }
    return add_ordered(y, x, z, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (x == z) && (z != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == x) && (z == 1) ==> r = x / z
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Division(x, y)} over three double
 * scalars. 
 */
public static class DivisionDouble_zxy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_zxy proto = new @Prototype DivisionDouble_zxy ();

  /** Returns the prototype invariant for DivisionDouble_zxy */
  public static @Prototype DivisionDouble_zxy get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_zxy instantiate_dyn(@Prototype DivisionDouble_zxy this, PptSlice slice) {
    return new DivisionDouble_zxy (slice);
  }

  private DivisionDouble_zxy (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_zxy () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_zxy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_zxy.function_id == -1;
    DivisionDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_zxy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double x, double y) {

    return (x / y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, x, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, x, y);
    }
    return add_ordered(z, x, y, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (x == y) && (y != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == x) && (y == 1) ==> r = x / y
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code x = Division(z, y)} over three double
 * scalars. 
 */
public static class DivisionDouble_xzy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_xzy proto = new @Prototype DivisionDouble_xzy ();

  /** Returns the prototype invariant for DivisionDouble_xzy */
  public static @Prototype DivisionDouble_xzy get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_xzy instantiate_dyn(@Prototype DivisionDouble_xzy this, PptSlice slice) {
    return new DivisionDouble_xzy (slice);
  }

  private DivisionDouble_xzy (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_xzy () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_xzy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_xzy.function_id == -1;
    DivisionDouble_xzy.function_id = function_id;
  }

  private static int var_order = 4;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_xzy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double z, double y) {

    return (z / y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, z, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, z, y);
    }
    return add_ordered(x, z, y, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_xzy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (z == y) && (y != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == z) && (y == 1) ==> r = z / y
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Division(z, x)} over three double
 * scalars. 
 */
public static class DivisionDouble_yzx extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_yzx proto = new @Prototype DivisionDouble_yzx ();

  /** Returns the prototype invariant for DivisionDouble_yzx */
  public static @Prototype DivisionDouble_yzx get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_yzx instantiate_dyn(@Prototype DivisionDouble_yzx this, PptSlice slice) {
    return new DivisionDouble_yzx (slice);
  }

  private DivisionDouble_yzx (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_yzx () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_yzx this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_yzx.function_id == -1;
    DivisionDouble_yzx.function_id = function_id;
  }

  private static int var_order = 5;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_yzx this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double z, double x) {

    return (z / x);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, z, x, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, z, x);
    }
    return add_ordered(y, z, x, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_yzx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(2, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(0, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(0, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (z == x) && (x != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == z) && (x == 1) ==> r = z / x
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Division(y, x)} over three double
 * scalars. 
 */
public static class DivisionDouble_zyx extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype DivisionDouble_zyx proto = new @Prototype DivisionDouble_zyx ();

  /** Returns the prototype invariant for DivisionDouble_zyx */
  public static @Prototype DivisionDouble_zyx get_proto() {
    return proto;
  }

  @Override
  protected DivisionDouble_zyx instantiate_dyn(@Prototype DivisionDouble_zyx this, PptSlice slice) {
    return new DivisionDouble_zyx (slice);
  }

  private DivisionDouble_zyx (PptSlice slice) {
    super(slice);
  }

  public @Prototype DivisionDouble_zyx () {
    super();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  @Override
  public String[] get_method_name(@GuardSatisfied DivisionDouble_zyx this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert DivisionDouble_zyx.function_id == -1;
    DivisionDouble_zyx.function_id = function_id;
  }

  private static int var_order = 6;

  @Override
  public int get_var_order(@GuardSatisfied DivisionDouble_zyx this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double y, double x) {

    return (y / x);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, y, x, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, y, x);
    }
    return add_ordered(z, y, x, count);
  }

  @Pure
  @Override
  public boolean isDivision() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(DivisionDouble_zyx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (y == x) && (x != 0) && (r == 1)
            new NISuppression(arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

            // (r == y) && (x == 1) ==> r = y / x
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),
          });

  // Create a suppression factory for functionBinary

}

  // default is that it is not this function, overridden in the subclass
  @Pure
  public boolean isPower() {
    return false;
  }

/**
 * Represents the invariant {@code x = Power(y, z)} over three double
 * scalars. 
 */
public static class PowerDouble_xyz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_xyz proto = new @Prototype PowerDouble_xyz ();

  /** Returns the prototype invariant for PowerDouble_xyz */
  public static @Prototype PowerDouble_xyz get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_xyz instantiate_dyn(@Prototype PowerDouble_xyz this, PptSlice slice) {
    return new PowerDouble_xyz (slice);
  }

  private PowerDouble_xyz (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_xyz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_xyz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_xyz.function_id == -1;
    PowerDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_xyz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double y, double z) {

    return Math.pow(y, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, y, z);
    }
    return add_ordered(x, y, z, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit z to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (z == 0) ==> r = pow (y, z)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (y == 1) && (z >= 0)   ==> r = pow (y, z)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (y == 0) && (z > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == y) && (z == 1)    ==> r = pow (y, z)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Power(x, z)} over three double
 * scalars. 
 */
public static class PowerDouble_yxz extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_yxz proto = new @Prototype PowerDouble_yxz ();

  /** Returns the prototype invariant for PowerDouble_yxz */
  public static @Prototype PowerDouble_yxz get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_yxz instantiate_dyn(@Prototype PowerDouble_yxz this, PptSlice slice) {
    return new PowerDouble_yxz (slice);
  }

  private PowerDouble_yxz (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_yxz () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_yxz this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_yxz.function_id == -1;
    PowerDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_yxz this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double x, double z) {

    return Math.pow(x, z);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, x, z, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, x, z);
    }
    return add_ordered(y, x, z, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit z to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (z == 0) ==> r = pow (x, z)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (x == 1) && (z >= 0)   ==> r = pow (x, z)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (x == 0) && (z > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == x) && (z == 1)    ==> r = pow (x, z)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Power(x, y)} over three double
 * scalars. 
 */
public static class PowerDouble_zxy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_zxy proto = new @Prototype PowerDouble_zxy ();

  /** Returns the prototype invariant for PowerDouble_zxy */
  public static @Prototype PowerDouble_zxy get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_zxy instantiate_dyn(@Prototype PowerDouble_zxy this, PptSlice slice) {
    return new PowerDouble_zxy (slice);
  }

  private PowerDouble_zxy (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_zxy () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_zxy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_zxy.function_id == -1;
    PowerDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_zxy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double x, double y) {

    return Math.pow(x, y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, x, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, x, y);
    }
    return add_ordered(z, x, y, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit y to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (y == 0) ==> r = pow (x, y)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (x == 1) && (y >= 0)   ==> r = pow (x, y)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (x == 0) && (y > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == x) && (y == 1)    ==> r = pow (x, y)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code x = Power(z, y)} over three double
 * scalars. 
 */
public static class PowerDouble_xzy extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_xzy proto = new @Prototype PowerDouble_xzy ();

  /** Returns the prototype invariant for PowerDouble_xzy */
  public static @Prototype PowerDouble_xzy get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_xzy instantiate_dyn(@Prototype PowerDouble_xzy this, PptSlice slice) {
    return new PowerDouble_xzy (slice);
  }

  private PowerDouble_xzy (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_xzy () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_xzy this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_xzy.function_id == -1;
    PowerDouble_xzy.function_id = function_id;
  }

  private static int var_order = 4;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_xzy this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double z, double y) {

    return Math.pow(z, y);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(x, z, y, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", x, z, y);
    }
    return add_ordered(x, z, y, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_xzy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(0, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(0, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(2, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(0, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(0, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(1, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(0, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(0, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(1, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit y to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (y == 0) ==> r = pow (z, y)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (z == 1) && (y >= 0)   ==> r = pow (z, y)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (z == 0) && (y > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == z) && (y == 1)    ==> r = pow (z, y)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code y = Power(z, x)} over three double
 * scalars. 
 */
public static class PowerDouble_yzx extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_yzx proto = new @Prototype PowerDouble_yzx ();

  /** Returns the prototype invariant for PowerDouble_yzx */
  public static @Prototype PowerDouble_yzx get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_yzx instantiate_dyn(@Prototype PowerDouble_yzx this, PptSlice slice) {
    return new PowerDouble_yzx (slice);
  }

  private PowerDouble_yzx (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_yzx () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_yzx this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_yzx.function_id == -1;
    PowerDouble_yzx.function_id = function_id;
  }

  private static int var_order = 5;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_yzx this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double z, double x) {

    return Math.pow(z, x);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(y, z, x, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", y, z, x);
    }
    return add_ordered(y, z, x, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_yzx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(1, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(1, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(2, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(1, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(0, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(1, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(0, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit x to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (x == 0) ==> r = pow (z, x)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (z == 1) && (x >= 0)   ==> r = pow (z, x)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (z == 0) && (x > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == z) && (x == 1)    ==> r = pow (z, x)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant {@code z = Power(y, x)} over three double
 * scalars. 
 */
public static class PowerDouble_zyx extends FunctionBinaryFloat {
  static final long serialVersionUID = 20031030L;

  private static @Prototype PowerDouble_zyx proto = new @Prototype PowerDouble_zyx ();

  /** Returns the prototype invariant for PowerDouble_zyx */
  public static @Prototype PowerDouble_zyx get_proto() {
    return proto;
  }

  @Override
  protected PowerDouble_zyx instantiate_dyn(@Prototype PowerDouble_zyx this, PptSlice slice) {
    return new PowerDouble_zyx (slice);
  }

  private PowerDouble_zyx (PptSlice slice) {
    super(slice);
  }

  public @Prototype PowerDouble_zyx () {
    super();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  @Override
  public String[] get_method_name(@GuardSatisfied PowerDouble_zyx this) {
    return method_name;
  }

  private static int function_id = -1;

  @Override
  public int get_function_id() {
    return function_id;
  }

  @Override
  public void set_function_id(int function_id) {
    assert PowerDouble_zyx.function_id == -1;
    PowerDouble_zyx.function_id = function_id;
  }

  private static int var_order = 6;

  @Override
  public int get_var_order(@GuardSatisfied PowerDouble_zyx this) {
    return var_order;
  }

  @Pure
  @Override
  public boolean is_symmetric() {

      return false;
  }

  @Override

  public double func(double y, double x) {

    return Math.pow(y, x);
  }

  @Override
  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return check_ordered(z, y, x, count);
  }

  @Override
  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail()) {
      log("result=%s, arg1=%s, arg2=%s", z, y, x);
    }
    return add_ordered(z, y, x, count);
  }

  @Pure
  @Override
  public boolean isPower() {
    return true;
  }

  @Pure
  @Override
  public boolean isExact() {
    return true;
  }

  /** Returns a list of non-instantiating suppressions for this invariant. */
  @Pure
  @Override
  public @Nullable NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled) {
      return suppressions;
    } else {
      return null;
    }
  }

  /** definition of this invariant (the suppressee) */
  private static NISuppressee suppressee = new NISuppressee(PowerDouble_zyx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1 =
      new NISuppressor(2, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2 =
      new NISuppressor(2, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2 =
      new NISuppressor(1, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1 =
      new NISuppressor(2, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2 =
      new NISuppressor(2, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2 =
      new NISuppressor(1, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1 =
      new NISuppressor(0, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1 =
      new NISuppressor(2, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2 =
      new NISuppressor(2, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2 =
      new NISuppressor(1, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1 =
      new NISuppressor(0, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1 =
      new NISuppressor(2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2 =
      new NISuppressor(2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2 =
      new NISuppressor(1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result =
      new NISuppressor(1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result =
      new NISuppressor(0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1 =
      new NISuppressor(0, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1 =
      new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1 =
      new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1 =
      new NISuppressor(0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0 =
      new NISuppressor(2, RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0 =
      new NISuppressor(1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0 =
      new NISuppressor(0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0 =
      new NISuppressor(2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0 =
      new NISuppressor(1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0 =
      new NISuppressor(0, NonZeroFloat.class);

  private static NISuppressor result_ge_0 =
      new NISuppressor(2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0 =
      new NISuppressor(1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0 =
      new NISuppressor(0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64 =
      new NISuppressor(2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64 =
      new NISuppressor(1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64 =
      new NISuppressor(0, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit x to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions =
      new NISuppressionSet(
          new NISuppression[] {

            // (r == 1) && (x == 0) ==> r = pow (y, x)
            new NISuppression(result_eq_1, arg2_eq_0, suppressee),

            // (r == 1) && (y == 1) && (x >= 0)   ==> r = pow (y, x)
            new NISuppression(result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

            // (r == 0) && (y == 0) && (x > 0)
            new NISuppression(result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                              suppressee),

            // (r == y) && (x == 1)    ==> r = pow (y, x)
            new NISuppression(result_eq_arg1, arg2_eq_1, suppressee),

          });

  // Create a suppression factory for functionBinary

}

}
