// ***** This file is automatically generated from LinearTernary.java.jpp

package daikon.inv.ternary.threeScalar;

import daikon.*;
import daikon.inv.*        ;
import daikon.inv.DiscardCode;
import daikon.inv.DiscardInfo;
import daikon.inv.binary.twoScalar.*;
import daikon.inv.unary.scalar.*;
import daikon.suppress.NIS;
import java.util.*;
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.checkerframework.framework.qual.Unused;
import typequals.prototype.qual.NonPrototype;
import typequals.prototype.qual.Prototype;

/**
 * Represents a Linear invariant over three long scalars {@code x},
 * {@code y}, and {@code z}, of the form
 * {@code ax + by + cz + d = 0}.
 * The constants {@code a}, {@code b}, {@code c}, and
 * {@code d} are mutually relatively prime, and the constant
 * {@code a} is always positive.
 */

@SuppressWarnings("UnnecessaryParentheses")  // generated code, parens are sometimes necessary
public class LinearTernary extends ThreeScalar {
  static final long serialVersionUID = 20030822L;

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /** Boolean. True iff LinearTernary invariants should be considered. */
  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;

  public static final boolean debugLinearTernary = false;
  // public static final boolean debugLinearTernary = true;

  @Unused(when=Prototype.class)
  public LinearTernaryCore core;

  @SuppressWarnings("nullness") // circular initialization
  protected LinearTernary(PptSlice ppt) {
    super(ppt);
    core = new LinearTernaryCore(this);
  }

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

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

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

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

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

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

    // make sure the variables are integral
    if (!vis[0].file_rep_type.isIntegral()
        || !vis[1].file_rep_type.isIntegral()
        || !vis[2].file_rep_type.isIntegral())
      return false;

    // Don't create if any of the variables are constant.
    // DynamicConstants will create this from LinearBinary
    // and the constant value if/when all of its variables are non-constant
    PptTopLevel parent = vis[0].ppt;
    if (NIS.dkconfig_enabled && (parent.is_constant(vis[0])
                                 || parent.is_constant(vis[1])
                                 || parent.is_constant(vis[2])))
      return false;

    /*
    // JHP: This code is removed because these sorts of static checks
    // can't be reliably performed with equality sets (just because
    // the leaders are obvious subsets, does not imply that all members
    // are.  Eventually this should be moved to isObviousStatically()

    VarInfo x = ppt.var_infos[0];
    VarInfo y = ppt.var_infos[1];
    VarInfo z = ppt.var_infos[2];

    if (((x.derived instanceof SequenceLength)
         && (((SequenceLength) x.derived).shift != 0))
        || ((y.derived instanceof SequenceLength)
            && (((SequenceLength) y.derived).shift != 0))
        || ((z.derived instanceof SequenceLength)
            && (((SequenceLength) z.derived).shift != 0))) {
      // Do not instantiate z-1 = ax + by + c.  Instead, choose a different c.
      Global.implied_noninstantiated_invariants += 1;
      return null;
    }

    VarInfo x_summand = null;
    VarInfo y_summand = null;
    VarInfo z_summand = null;
    if (x.derived instanceof SequenceSum) {
      x_summand = ((SequenceSum) x.derived).base;
    }
    if (y.derived instanceof SequenceSum) {
      y_summand = ((SequenceSum) y.derived).base;
    }
    if (z.derived instanceof SequenceSum) {
    z_summand = ((SequenceSum) z.derived).base;
    }

    if ((x_summand != null) && (y_summand != null) && (z_summand != null)) {
      // all 3 of x, y, and z are "sum(...)"
      // avoid sum(a[0..i]) + sum(a[i..]) = sum(a[])

      if (debugLinearTernary) {
        System.out.println(ppt.varNames() + " 3 summands: " + x_summand.name + " " + y_summand.name + " " + z_summand.name);
      }

      VarInfo x_seq = x_summand.isDerivedSubSequenceOf();
      VarInfo y_seq = y_summand.isDerivedSubSequenceOf();
      VarInfo z_seq = z_summand.isDerivedSubSequenceOf();
      if (x_seq == null) x_seq = x_summand;
      if (y_seq == null) y_seq = y_summand;
      if (z_seq == null) z_seq = z_summand;
      VarInfo seq = x_seq;

      if (debugLinearTernary) {
        System.out.println(ppt.varNames() + " 3 sequences: " + x_seq.name + " " + y_seq.name + " " + z_seq.name);
      }

      if (((seq == x_summand) || (seq == y_summand) || (seq == z_summand))
          && (x_seq == y_seq) && (x_seq == z_seq)) {
        assert y_seq == z_seq;
        if (debugLinearTernary) {
          System.out.println(ppt.varNames() + " 3 sequences match");
        }

        SequenceScalarSubsequence part1 = null;
        SequenceScalarSubsequence part2 = null;
        for (int i = 0; i < 3; i++) {
          VarInfo vi = ppt.var_infos[i];
          VarInfo summand = ((SequenceSum) vi.derived).base;
          if (debugLinearTernary) {
            System.out.println("considering: " + summand.name + " " + vi.name);
          }
          if (summand.derived instanceof SequenceScalarSubsequence) {
            SequenceScalarSubsequence sss = (SequenceScalarSubsequence) summand.derived;
            if (sss.from_start) {
              part1 = sss;
            } else {
              part2 = sss;
            }
          } else {
            if (debugLinearTernary) {
              System.out.println("Not subseq: " + summand.name + " " + vi.name);
            }
          }
        }
        if (debugLinearTernary) {
          System.out.println(ppt.varNames() + " part1=" + part1 + ", part2=" + part2 + ", seq=" + seq.name);
        }
        if ((part1 != null) && (part2 != null)) {
          // now part1, and part2 are set
          if ((part1.sclvar() == part2.sclvar())
              && (part1.index_shift + 1 == part2.index_shift)) {
            if (debugLinearTernary) {
              System.out.println("LinearTernary suppressed: " + ppt.varNames());
            }
            Global.implied_noninstantiated_invariants += 1;
            return null;
          }
        }
      }
    } else if ((x_summand != null) && (y_summand != null)
               || ((x_summand != null) && (z_summand != null))
               || ((y_summand != null) && (z_summand != null))) {
      // two of x, y, and z are "sum(...)"
      // avoid sum(a[0..i-1]) + a[i] = sum(a[0..i])

      // if (debugLinearTernary) {
      //   System.out.println(ppt.varNames() + " 2 summands: " + x_summand + " " + y_summand + " " + z_summand);
      // }

      // The intention is that parta is a[0..i], partb is a[0..i-1], and
      // notpart is a[i].
      VarInfo parta;
      VarInfo partb;
      VarInfo notpart;

      if (x_summand != null) {
        parta = x;
        if (y_summand != null) {
          partb = y;
          notpart = z;
        } else {
          partb = z;
          notpart = y;
        }
      } else {
        notpart = x;
        parta = y;
        partb = z;
      }
      parta = ((SequenceSum) parta.derived).base;
      partb = ((SequenceSum) partb.derived).base;
      VarInfo seq = null;
      VarInfo eltindex = null;
      if (notpart.derived instanceof SequenceScalarSubscript) {
        SequenceScalarSubscript sss = (SequenceScalarSubscript) notpart.derived;
        seq = sss.seqvar();
        eltindex = sss.sclvar();
      }
      if ((seq != null)
          && (seq == parta.isDerivedSubSequenceOf())
          && (seq == partb.isDerivedSubSequenceOf())) {
        // For now, don't deal with case where one variable is the entire
        // sequence.
        if (!((parta == seq) || (partb == seq))) {
          SequenceScalarSubsequence a_sss = (SequenceScalarSubsequence) parta.derived;
          SequenceScalarSubsequence b_sss = (SequenceScalarSubsequence) partb.derived;
          if ((a_sss.sclvar() == eltindex)
              && (b_sss.sclvar() == eltindex)) {
            if ((a_sss.from_start
                 && b_sss.from_start
                 && (((a_sss.index_shift == -1) && (b_sss.index_shift == 0))
                     || ((a_sss.index_shift == 0) && (b_sss.index_shift == -1))))
                || ((!a_sss.from_start)
                    && (!b_sss.from_start)
                    && (((a_sss.index_shift == 0) && (b_sss.index_shift == 1))
                        || ((a_sss.index_shift == 1) && (b_sss.index_shift == 0))))) {
            Global.implied_noninstantiated_invariants += 1;
            return null;
            }
          }
        }
      }
    }
    */

    return true;
  }

  @Override
  public LinearTernary instantiate_dyn(@Prototype LinearTernary this, PptSlice slice) {
    return new LinearTernary(slice);
  }

  @SideEffectFree
  @Override
  public LinearTernary clone(@GuardSatisfied LinearTernary this) {
    LinearTernary result = (LinearTernary) super.clone();
    result.core = core.clone();
    result.core.wrapper = result;
    return result;
  }

  @Override
  protected Invariant resurrect_done(int[] permutation) {
    core.permute(permutation);
    return this;
  }

  @Override
  public String repr(@GuardSatisfied LinearTernary this) {
    return "LinearTernary" + varNames() + ": falsified=" + falsified
      + "; " + core.repr();
  }

  @SideEffectFree
  @Override
  public String format_using(@GuardSatisfied LinearTernary this, OutputFormat format) {
    return core.format_using(format, var1().name_using(format),
                        var2().name_using(format), var3().name_using(format));
  }

  // public String format_reversed() {
  //   return core.format_reversed(var1().name.name(), var2().name.name(), var3().name.name());
  // }

  @Pure
  @Override
  public boolean isActive() {
    return core.isActive();
  }

  public InvariantStatus setup(LinearBinary lb, VarInfo con_var,
                                long con_val) {
    return core.setup(lb, con_var, con_val);
  }

  public InvariantStatus setup(OneOfScalar oo, VarInfo v1, long con1,
                                VarInfo v2, long con2) {
    return core.setup(oo, v1, con1, v2, con2);
  }

  @Override
  public InvariantStatus check_modified(long x, long y, long z, int count) {
    return clone().add_modified(x, y, z, count);
  }

  @Override
  public InvariantStatus add_modified(long x, long y, long z, int count) {
    return core.add_modified(x, y, z, count);
  }

  @Override
  public boolean enoughSamples(@GuardSatisfied LinearTernary this) {
    return core.enoughSamples();
  }

  @Override
  protected double computeConfidence() {
    return core.computeConfidence();
  }

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

  @Pure
  @Override
  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    if (core.a == 0 || core.b == 0 || core.c == 0) {
      return new DiscardInfo(this, DiscardCode.obvious, "If a coefficient is 0, a LinearBinary should"
                             + " exist over the other two variables");
    }

    return null;
  }

  @Pure
  @Override
  public boolean isSameFormula(Invariant other) {
    return core.isSameFormula(((LinearTernary) other).core);
  }

  @Pure
  @Override
  public boolean isExclusiveFormula(Invariant other) {
    if (other instanceof LinearTernary) {
      return core.isExclusiveFormula(((LinearTernary) other).core);
    }
    return false;
  }

  // Look up a previously instantiated invariant.
  public static @Nullable LinearTernary find(PptSlice ppt) {
    assert ppt.arity() == 3;
    for (Invariant inv : ppt.invs) {
      if (inv instanceof LinearTernary) {
        return (LinearTernary) inv;
      }
    }
    return null;
  }

  // Returns a vector of LinearTernary objects.
  // This ought to produce an iterator instead.
  public static List<LinearTernary> findAll(VarInfo vi) {
    List<LinearTernary> result = new ArrayList<>();
    for (PptSlice view : vi.ppt.views_iterable()) {
      if ((view.arity() == 3) && view.usesVar(vi)) {
        LinearTernary lt = LinearTernary.find(view);
        if (lt != null) {
          result.add(lt);
        }
      }
    }
    return result;
  }

  @Override
  public boolean mergeFormulasOk() {
    return core.mergeFormulasOk();
  }

  /**
   * Merge the invariants in invs to form a new invariant. Each must be a LinearTernary invariant. The
   * work is done by the LinearTernary core
   *
   * @param invs list of invariants to merge. They should all be permuted to match the variable
   *     order in parent_ppt.
   * @param parent_ppt slice that will contain the new invariant
   */
  @Override
  public @Nullable LinearTernary merge(List<Invariant> invs, PptSlice parent_ppt) {

    // Create a matching list of cores
    List<LinearTernaryCore> cores = new ArrayList<>();
    for (Invariant inv : invs) {
      cores.add(((LinearTernary) inv).core);
    }

    // Merge the cores and build a new invariant containing the merged core
    LinearTernary result = new LinearTernary(parent_ppt);
    LinearTernaryCore newcore = core.merge(cores, result);
    if (newcore == null) {
      return null;
    }
    result.core = newcore;
    return result;
  }
}
