package org.checkerframework.checker.index.upperbound;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import javax.annotation.processing.ProcessingEnvironment;
import javax.lang.model.element.AnnotationMirror;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.LTOMLengthOf;
import org.checkerframework.checker.index.qual.SubstringIndexFor;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.Pair;
import org.plumelib.util.CollectionsPlume;

/**
 * Abstraction for Upper Bound annotations. This abstract class has 4 subclasses, each of which is a
 * nested class: {@link LessThanLengthOf}, {@link UpperBoundUnknownQualifier}, {@code
 * UpperBoundBottomQualifier}, and {@code PolyQualifier}.
 *
 * <p>{@link LTLengthOf} is modeled by {@link LessThanLengthOf}. {@link LTEqLengthOf} is equivalent
 * to @{@link LessThanLengthOf} with an offset of -1. {@link LTOMLengthOf} is equivalent to @{@link
 * LessThanLengthOf} with an offset of 1.
 */
public abstract class UBQualifier {

  /**
   * Create a UBQualifier from the given annotation.
   *
   * @param am the annotation to turn into a UBQualifier
   * @param ubChecker used to obtain the fields of {@code am}
   * @return a UBQualifier that represents the same information as the given annotation
   */
  public static UBQualifier createUBQualifier(AnnotationMirror am, UpperBoundChecker ubChecker) {
    return createUBQualifier(am, null, ubChecker);
  }

  /**
   * Create a UBQualifier from the given annotation, with an extra offset.
   *
   * @param am the annotation to turn into a UBQualifier
   * @param offset the extra offset; may be null
   * @param ubChecker used to obtain the fields of {@code am}
   * @return a UBQualifier that represents the same information as the given annotation (plus an
   *     optional offset)
   */
  public static UBQualifier createUBQualifier(
      AnnotationMirror am, String offset, UpperBoundChecker ubChecker) {
    switch (AnnotationUtils.annotationName(am)) {
      case "org.checkerframework.checker.index.qual.UpperBoundUnknown":
        return UpperBoundUnknownQualifier.UNKNOWN;
      case "org.checkerframework.checker.index.qual.UpperBoundBottom":
        return UpperBoundBottomQualifier.BOTTOM;
      case "org.checkerframework.checker.index.qual.UpperBoundLiteral":
        int intValue =
            AnnotationUtils.getElementValueInt(am, ubChecker.upperBoundLiteralValueElement);
        return UpperBoundLiteralQualifier.create(intValue);
      case "org.checkerframework.checker.index.qual.LTLengthOf":
        return parseLTLengthOf(am, offset, ubChecker);
      case "org.checkerframework.checker.index.qual.SubstringIndexFor":
        return parseSubstringIndexFor(am, offset, ubChecker);
      case "org.checkerframework.checker.index.qual.LTEqLengthOf":
        return parseLTEqLengthOf(am, offset, ubChecker);
      case "org.checkerframework.checker.index.qual.LTOMLengthOf":
        return parseLTOMLengthOf(am, offset, ubChecker);
      case "org.checkerframework.checker.index.qual.PolyUpperBound":
        // TODO:  Ignores offset.  Should we check that offset is not set?
        return PolyQualifier.POLY;
      default:
        throw new BugInCF("createUBQualifier(%s, %s, ...)", am, offset);
    }
  }

  /** A cache for the {@link #nCopiesEmptyStringCache} method. */
  private static List<List<String>> nCopiesEmptyStringCache = new ArrayList<>(10);

  static {
    nCopiesEmptyStringCache.add(Collections.emptyList());
    nCopiesEmptyStringCache.add(Collections.singletonList(""));
    nCopiesEmptyStringCache.add(Collections.nCopies(2, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(3, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(4, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(5, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(6, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(7, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(8, ""));
    nCopiesEmptyStringCache.add(Collections.nCopies(9, ""));
  }

  /**
   * Equivalent to {@code Collections.nCopies(n, "")}.
   *
   * @param n the length of the list
   * @return an immutable list of {@code n} copies of {@code ""}
   */
  private static List<String> nCopiesEmptyString(int n) {
    if (n < 10) {
      return nCopiesEmptyStringCache.get(n);
    } else {
      return Collections.nCopies(n, "");
    }
  }

  /**
   * Create a UBQualifier from a @LTLengthOf annotation.
   *
   * @param ltLengthOfAnno a @LTLengthOf annotation
   * @param extraOffset the extra offset
   * @param ubChecker used to obtain the fields of {@code am}
   * @return a UBQualifier created from the @LTLengthOf annotation
   */
  private static UBQualifier parseLTLengthOf(
      AnnotationMirror ltLengthOfAnno, String extraOffset, UpperBoundChecker ubChecker) {
    List<String> sequences =
        AnnotationUtils.getElementValueArray(
            ltLengthOfAnno, ubChecker.ltLengthOfValueElement, String.class);
    List<String> offsets =
        AnnotationUtils.getElementValueArray(
            ltLengthOfAnno,
            ubChecker.ltLengthOfOffsetElement,
            String.class,
            nCopiesEmptyString(sequences.size()));
    return createUBQualifier(sequences, offsets, extraOffset);
  }

  /**
   * Create a UBQualifier from a @SubstringIndexFor annotation.
   *
   * @param substringIndexForAnno a @SubstringIndexFor annotation
   * @param extraOffset the extra offset
   * @param ubChecker used for obtaining arguments/elements from {@code substringIndexForAnno}
   * @return a UBQualifier created from the @SubstringIndexFor annotation
   */
  private static UBQualifier parseSubstringIndexFor(
      AnnotationMirror substringIndexForAnno, String extraOffset, UpperBoundChecker ubChecker) {
    List<String> sequences =
        AnnotationUtils.getElementValueArray(
            substringIndexForAnno, ubChecker.substringIndexForValueElement, String.class);
    List<String> offsets =
        AnnotationUtils.getElementValueArray(
            substringIndexForAnno, ubChecker.substringIndexForOffsetElement, String.class);
    if (offsets.isEmpty()) {
      offsets = nCopiesEmptyString(sequences.size());
    }
    return createUBQualifier(sequences, offsets, extraOffset);
  }

  /**
   * Create a UBQualifier from a @LTEqLengthOf annotation.
   *
   * @param am a @LTEqLengthOf annotation
   * @param extraOffset the extra offset
   * @param ubChecker used for obtaining fields from {@code am}
   * @return a UBQualifier created from the @LTEqLengthOf annotation
   */
  private static UBQualifier parseLTEqLengthOf(
      AnnotationMirror am, String extraOffset, UpperBoundChecker ubChecker) {
    List<String> sequences =
        AnnotationUtils.getElementValueArray(am, ubChecker.ltEqLengthOfValueElement, String.class);
    if (sequences.isEmpty()) {
      // How did this AnnotationMirror even get made?  It seems invalid.
      return UpperBoundUnknownQualifier.UNKNOWN;
    }
    List<String> offset = Collections.nCopies(sequences.size(), "-1");
    return createUBQualifier(sequences, offset, extraOffset);
  }

  /**
   * Create a UBQualifier from a @LTOMLengthOf annotation.
   *
   * @param am a @LTOMLengthOf annotation
   * @param extraOffset offset to add to each element of offsets; may be null
   * @param ubChecker used for obtaining fields from {@code am}
   * @return a UBQualifier created from the @LTOMLengthOf annotation
   */
  private static UBQualifier parseLTOMLengthOf(
      AnnotationMirror am, String extraOffset, UpperBoundChecker ubChecker) {
    List<String> sequences =
        AnnotationUtils.getElementValueArray(am, ubChecker.ltOMLengthOfValueElement, String.class);
    List<String> offset = Collections.nCopies(sequences.size(), "1");
    return createUBQualifier(sequences, offset, extraOffset);
  }

  public static UBQualifier createUBQualifier(String sequence, String offset) {
    return createUBQualifier(
        Collections.singletonList(sequence), Collections.singletonList(offset));
  }

  /**
   * Create an upper bound qualifier.
   *
   * @param type the type from which to obtain an annotation
   * @param top the top annotation in a hierarchy; the annotation in this hierarchy will be used
   * @param ubChecker used to obtain the fields of {@code am}
   * @return a new upper bound qualifier
   */
  public static UBQualifier createUBQualifier(
      AnnotatedTypeMirror type, AnnotationMirror top, UpperBoundChecker ubChecker) {
    return createUBQualifier(type.getEffectiveAnnotationInHierarchy(top), ubChecker);
  }

  /**
   * Creates an {@link UBQualifier} from the given sequences and offsets. The list of sequences may
   * not be empty. If the offsets list is empty, then an offset of 0 is used for each sequence. If
   * the offsets list is not empty, then it must be the same size as sequence.
   *
   * @param sequences non-empty list of sequences
   * @param offsets list of offset, if empty, an offset of 0 is used
   * @return an {@link UBQualifier} for the sequences with the given offsets
   */
  public static UBQualifier createUBQualifier(List<String> sequences, List<String> offsets) {
    return createUBQualifier(sequences, offsets, null);
  }

  /**
   * Creates an {@link UBQualifier} from the given sequences and offsets, with the given additional
   * offset. The list of sequences may not be empty. If the offsets list is empty, then an offset of
   * 0 is used for each sequence. If the offsets list is not empty, then it must be the same size as
   * sequence.
   *
   * @param sequences non-empty list of sequences
   * @param offsets list of offset, if empty, an offset of 0 is used
   * @param extraOffset offset to add to each element of offsets; may be null
   * @return an {@link UBQualifier} for the sequences with the given offsets
   */
  public static UBQualifier createUBQualifier(
      List<String> sequences, List<String> offsets, String extraOffset) {
    assert !sequences.isEmpty();

    OffsetEquation extraEq;
    if (extraOffset == null) {
      extraEq = OffsetEquation.ZERO;
    } else {
      extraEq = OffsetEquation.createOffsetFromJavaExpression(extraOffset);
      if (extraEq.hasError()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
    }

    return new LessThanLengthOf(sequences, offsets, extraEq);
  }

  /**
   * Add the node as an offset to a copy of this qualifier. If this qualifier is UNKNOWN or BOTTOM,
   * then UNKNOWN is returned. Otherwise, see {@link LessThanLengthOf#plusOffset(int)} for an
   * explanation of how node is added as an offset.
   *
   * @param node a Node
   * @param factory an AnnotatedTypeFactory
   * @return a copy of this qualifier with node added as an offset
   */
  public UBQualifier plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) {
    return UpperBoundUnknownQualifier.UNKNOWN;
  }

  public UBQualifier plusOffset(int value) {
    return UpperBoundUnknownQualifier.UNKNOWN;
  }

  public UBQualifier minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) {
    return UpperBoundUnknownQualifier.UNKNOWN;
  }

  public UBQualifier minusOffset(int value) {
    return UpperBoundUnknownQualifier.UNKNOWN;
  }

  public boolean isLessThanLengthQualifier() {
    return false;
  }

  /**
   * Returns true if this UBQualifier represents a literal integer.
   *
   * @return true if this UBQualifier represents a literal integer
   */
  public boolean isLiteral() {
    return false;
  }

  /**
   * Returns true if this UBQualifier is the top type.
   *
   * @return true if this UBQualifier is the top type
   */
  public boolean isUnknown() {
    return false;
  }

  /**
   * Returns true if this UBQualifier is the bottom type.
   *
   * @return true if this UBQualifier is the bottom type
   */
  public boolean isBottom() {
    return false;
  }

  /**
   * Return true if this is UBQualifier.PolyQualifier.
   *
   * @return true if this is UBQualifier.PolyQualifier
   */
  @Pure
  public boolean isPoly() {
    return false;
  }

  public abstract boolean isSubtype(UBQualifier superType);

  public abstract UBQualifier lub(UBQualifier other);

  public UBQualifier widenUpperBound(UBQualifier obj) {
    return lub(obj);
  }

  public abstract UBQualifier glb(UBQualifier other);

  /**
   * Is the value with this qualifier less than the length of sequence?
   *
   * @param sequence a String sequence
   * @return whether or not the value with this qualifier is less than the length of sequence
   */
  public boolean isLessThanLengthOf(String sequence) {
    return false;
  }

  /**
   * Is the value with this qualifier less than the length of any of the sequences?
   *
   * @param sequences list of sequences
   * @return whether or not the value with this qualifier is less than the length of any of the
   *     sequences
   */
  public boolean isLessThanLengthOfAny(List<String> sequences) {
    return false;
  }

  /**
   * Returns whether or not this qualifier has sequence with the specified offset.
   *
   * @param sequence sequence expression
   * @param offset the offset being looked for
   * @return whether or not this qualifier has sequence with the specified offset
   */
  public boolean hasSequenceWithOffset(String sequence, int offset) {
    return false;
  }

  /**
   * Returns whether or not this qualifier has sequence with the specified offset.
   *
   * @param sequence sequence expression
   * @param offset the offset being looked for
   * @return whether or not this qualifier has sequence with the specified offset
   */
  public boolean hasSequenceWithOffset(String sequence, String offset) {
    return false;
  }

  /**
   * Is the value with this qualifier less than or equal to the length of sequence?
   *
   * @param sequence a String sequence
   * @return whether or not the value with this qualifier is less than or equal to the length of
   *     sequence
   */
  public boolean isLessThanOrEqualTo(String sequence) {
    return false;
  }

  /** The less-than-length-of qualifier (@LTLengthOf). */
  public static class LessThanLengthOf extends UBQualifier {

    // There are two representations for sequences and offsets.
    // In source code, they are represented by two parallel arrays, as in
    //   @LTLengthOf(value = {"a", "b", "a", "c"}, offset = {"-1", "x", "y", "0"}).
    // In this implementation, they are represented by a single map; the above would be
    //   { "a" : {"-1", "y"}, "b" : {"x"}, "c" : {"0"} }
    // Code in this class transforms from one representation to the other.

    /** Maps from sequence name to offset. */
    private final Map<String, Set<OffsetEquation>> map;

    /**
     * Returns a copy of the map.
     *
     * @return a copy of the map
     */
    private Map<String, Set<OffsetEquation>> copyMap() {
      Map<String, Set<OffsetEquation>> result = new HashMap<>(CollectionsPlume.mapCapacity(map));
      for (String sequenceName : map.keySet()) {
        Set<OffsetEquation> oldEquations = map.get(sequenceName);
        Set<OffsetEquation> newEquations =
            new HashSet<>(CollectionsPlume.mapCapacity(oldEquations));
        for (OffsetEquation offsetEquation : oldEquations) {
          newEquations.add(new OffsetEquation(offsetEquation));
        }
        result.put(sequenceName, newEquations);
      }
      return result;
    }

    /**
     * Returns true if the given integer literal is a subtype of this. The literal is a subtype of
     * this if, for every offset expression, {@code literal + offset <= -1}.
     *
     * @param i an integer
     * @return true if the given integer literal is a subtype of this
     */
    /*package-protected*/ boolean literalIsSubtype(int i) {
      for (Map.Entry<String, Set<OffsetEquation>> entry : map.entrySet()) {
        for (OffsetEquation equation : entry.getValue()) {
          if (!equation.isInt()) {
            return false;
          }
          int offset = equation.getInt();
          if (i + offset > -1) {
            return false;
          }
        }
      }
      return true;
    }

    /**
     * Convert the parallel array representation to the map representation.
     *
     * @param sequences non-empty list of sequences
     * @param offsets list of offset, if empty, an offset of 0 is used
     * @param extraEq offset to add to each element of offsets; may be null
     * @return the map representation of a {@link UBQualifier}, or null if there is an error
     */
    private static @Nullable Map<String, Set<OffsetEquation>> sequencesAndOffsetsToMap(
        List<String> sequences, List<String> offsets, OffsetEquation extraEq) {

      Map<String, Set<OffsetEquation>> map = new HashMap<>(CollectionsPlume.mapCapacity(sequences));
      if (offsets.isEmpty()) {
        for (String sequence : sequences) {
          // Not `Collections.singleton(extraEq)` because the values get modified
          Set<OffsetEquation> thisSet = new HashSet<>(1);
          thisSet.add(extraEq);
          map.put(sequence, thisSet);
        }
      } else {
        assert sequences.size() == offsets.size();
        for (int i = 0; i < sequences.size(); i++) {
          String sequence = sequences.get(i);
          String offset = offsets.get(i);
          Set<OffsetEquation> set = map.computeIfAbsent(sequence, __ -> new HashSet<>());
          OffsetEquation eq = OffsetEquation.createOffsetFromJavaExpression(offset);
          if (eq.hasError()) {
            return null;
          }
          eq = eq.copyAdd('+', extraEq);
          set.add(eq);
        }
      }
      return map;
    }

    /** A triple that is the return type of {@link #mapToSequencesAndOffsets}. */
    private static class SequencesOffsetsAndClass {
      /** List of sequences. */
      public final List<String> sequences;
      /** List of offsets. */
      public final List<String> offsets;
      /** The class of the annotation to be built. */
      public final Class<? extends Annotation> annoClass;

      /**
       * Creates a new SequencesOffsetsAndClass.
       *
       * @param sequences list of sequences
       * @param offsets list of offsets
       * @param annoClass the class of the annotation to be built
       */
      public SequencesOffsetsAndClass(
          List<String> sequences, List<String> offsets, Class<? extends Annotation> annoClass) {

        this.sequences = sequences;
        this.offsets = offsets;
        this.annoClass = annoClass;
      }
    }

    /**
     * Given the map representation, returns parallel-arrays representation.
     *
     * @param map the internal representation of LessThanLengthOf
     * @param buildSubstringIndexAnnotation if true, the annoClass in the result is
     *     ubstringIndexFor.class
     * @return the external representation
     */
    private static SequencesOffsetsAndClass mapToSequencesAndOffsets(
        Map<String, Set<OffsetEquation>> map, boolean buildSubstringIndexAnnotation) {
      List<String> sortedSequences = new ArrayList<>(map.keySet());
      Collections.sort(sortedSequences);
      List<String> sequences = new ArrayList<>();
      List<String> offsets = new ArrayList<>();
      boolean isLTEq = true;
      boolean isLTOM = true;
      for (String sequence : sortedSequences) {
        // The offsets for this sequence.
        List<String> thisOffsets = new ArrayList<>();
        for (OffsetEquation eq : map.get(sequence)) {
          isLTEq = isLTEq && eq.equals(OffsetEquation.NEG_1);
          isLTOM = isLTOM && eq.equals(OffsetEquation.ONE);
          thisOffsets.add(eq.toString());
        }
        Collections.sort(thisOffsets);
        for (String offset : thisOffsets) {
          sequences.add(sequence);
          offsets.add(offset);
        }
      }
      Class<? extends Annotation> annoClass;
      if (buildSubstringIndexAnnotation) {
        annoClass = SubstringIndexFor.class;
      } else if (isLTEq) {
        annoClass = LTEqLengthOf.class;
      } else if (isLTOM) {
        annoClass = LTOMLengthOf.class;
      } else {
        annoClass = LTLengthOf.class;
      }
      return new SequencesOffsetsAndClass(sequences, offsets, annoClass);
    }

    // End of code for manipulating the representation

    /**
     * Create a new LessThanLengthOf, from the internal representation.
     *
     * @param map a map from sequence name to offse
     */
    private LessThanLengthOf(Map<String, Set<OffsetEquation>> map) {
      assert !map.isEmpty();
      this.map = map;
    }

    /**
     * Create a new LessThanLengthOf from the parallel array representation.
     *
     * @param sequences non-empty list of sequences
     * @param offsets list of offset, if empty, an offset of 0 is used
     * @param extraEq offset to add to each element of offsets; may be null
     */
    private LessThanLengthOf(List<String> sequences, List<String> offsets, OffsetEquation extraEq) {
      this(sequencesAndOffsetsToMap(sequences, offsets, extraEq));
    }

    @Override
    public boolean hasSequenceWithOffset(String sequence, int offset) {
      Set<OffsetEquation> offsets = map.get(sequence);
      if (offsets == null) {
        return false;
      }
      return offsets.contains(OffsetEquation.createOffsetForInt(offset));
    }

    @Override
    public boolean hasSequenceWithOffset(String sequence, String offset) {
      Set<OffsetEquation> offsets = map.get(sequence);
      if (offsets == null) {
        return false;
      }
      OffsetEquation target = OffsetEquation.createOffsetFromJavaExpression(offset);
      return offsets.contains(target);
    }

    /**
     * Is a value with this type less than or equal to the length of sequence?
     *
     * @param sequence a String sequence
     * @return true if a value with this type is less than or equal to the length of sequence
     */
    @Override
    public boolean isLessThanOrEqualTo(String sequence) {
      return isLessThanLengthOf(sequence) || hasSequenceWithOffset(sequence, -1);
    }

    /**
     * Is a value with this type less than the length of any of the sequences?
     *
     * @param sequences list of sequences
     * @return true if a value with this type is less than the length of any of the sequences
     */
    @Override
    public boolean isLessThanLengthOfAny(List<String> sequences) {
      for (String sequence : sequences) {
        if (isLessThanLengthOf(sequence)) {
          return true;
        }
      }
      return false;
    }
    /**
     * Is a value with this type less than the length of the sequence?
     *
     * @param sequence a String sequence
     * @return true if a value with this type is less than the length of the sequence
     */
    @Override
    public boolean isLessThanLengthOf(String sequence) {
      Set<OffsetEquation> offsets = map.get(sequence);
      if (offsets == null) {
        return false;
      }
      if (offsets.isEmpty()) {
        return true;
      }
      for (OffsetEquation offset : offsets) {
        if (offset.isNonNegative()) {
          return true;
        }
      }
      return false;
    }

    /**
     * Returns the AnnotationMirror that represents this qualifier. If possible, AnnotationMirrors
     * using @{@link LTEqLengthOf} or @{@link LTOMLengthOf} are returned. Otherwise, @{@link
     * LTLengthOf} is used.
     *
     * <p>The returned annotation is canonicalized by sorting its arguments by sequence and then
     * offset. This is so that {@link AnnotationUtils#areSame(AnnotationMirror, AnnotationMirror)}
     * returns true for equivalent annotations.
     *
     * @param env a processing environment used to build the returned annotation
     * @return the AnnotationMirror that represents this qualifier
     */
    public AnnotationMirror convertToAnnotation(ProcessingEnvironment env) {
      return convertToAnnotation(env, false);
    }

    /**
     * Returns the @{@link SubstringIndexFor} AnnotationMirror from the Substring Index hierarchy
     * that imposes the same upper bounds on the annotated expression as this qualifier. However,
     * the upper bounds represented by this qualifier do not apply to the value -1 which is always
     * allowed by the returned annotation.
     *
     * @param env a processing environment used to build the returned annotation
     * @return the AnnotationMirror from the Substring Index hierarchy that represents the same
     *     upper bounds as this qualifier
     */
    public AnnotationMirror convertToSubstringIndexAnnotation(ProcessingEnvironment env) {
      return convertToAnnotation(env, true);
    }

    /**
     * Helper method called by {@link #convertToAnnotation} and {@link
     * convertToSubstringIndexAnnotation} that does the real work.
     *
     * @param env a processing environment used to build the returned annotation
     * @param buildSubstringIndexAnnotation if true, act like {@link
     *     #convertToSubstringIndexAnnotation} and return a @{@link SubstringIndexFor} annotation;
     *     if false, act like {@link #convertToAnnotation}
     * @return the AnnotationMirror that represents the same upper bounds as this qualifier
     */
    private AnnotationMirror convertToAnnotation(
        ProcessingEnvironment env, boolean buildSubstringIndexAnnotation) {
      SequencesOffsetsAndClass soc = mapToSequencesAndOffsets(map, buildSubstringIndexAnnotation);
      List<String> sequences = soc.sequences;
      List<String> offsets = soc.offsets;
      Class<? extends Annotation> annoClass = soc.annoClass;

      AnnotationBuilder builder = new AnnotationBuilder(env, annoClass);
      if (annoClass == SubstringIndexFor.class) {
        builder.setValue("value", sequences);
        builder.setValue("offset", offsets);
      } else if (annoClass == LTEqLengthOf.class) {
        builder.setValue("value", sequences);
      } else if (annoClass == LTOMLengthOf.class) {
        builder.setValue("value", sequences);
      } else if (annoClass == LTLengthOf.class) {
        builder.setValue("value", sequences);
        builder.setValue("offset", offsets);
      } else {
        throw new BugInCF("What annoClass? " + annoClass);
      }
      return builder.build();
    }

    @Override
    public boolean equals(@Nullable Object o) {
      if (this == o) {
        return true;
      }
      if (o == null || getClass() != o.getClass()) {
        return false;
      }

      LessThanLengthOf qualifier = (LessThanLengthOf) o;
      if (containsSame(map.keySet(), qualifier.map.keySet())) {
        for (Map.Entry<String, Set<OffsetEquation>> entry : map.entrySet()) {
          Set<OffsetEquation> otherOffset = qualifier.map.get(entry.getKey());
          Set<OffsetEquation> thisOffset = entry.getValue();
          if (!containsSame(otherOffset, thisOffset)) {
            return false;
          }
        }
        return true;
      }
      return false;
    }

    private static <T> boolean containsSame(Set<T> set1, Set<T> set2) {
      return set1.containsAll(set2) && set2.containsAll(set1);
    }

    @Override
    public int hashCode() {
      return map.hashCode();
    }

    @Override
    public boolean isLessThanLengthQualifier() {
      return true;
    }

    /**
     * If superType is Unknown, return true. If superType is Bottom, return false.
     *
     * <p>Otherwise, return true if this qualifier contains all the sequences in superType, AND for
     * each of the offsets for each sequence in superType, there is an offset in this qualifier for
     * the sequence that is greater than or equal to the super offset.
     *
     * @param superType other qualifier
     * @return whether this qualifier is a subtype of superType
     */
    @Override
    public boolean isSubtype(UBQualifier superType) {
      if (superType.isUnknown()) {
        return true;
      } else if (superType.isBottom()) {
        return false;
      } else if (superType.isLiteral()) {
        return false;
      }

      LessThanLengthOf superTypeLTL = (LessThanLengthOf) superType;

      if (!map.keySet().containsAll(superTypeLTL.map.keySet())) {
        return false;
      }
      for (Map.Entry<String, Set<OffsetEquation>> entry : superTypeLTL.map.entrySet()) {
        String sequence = entry.getKey();
        Set<OffsetEquation> superOffsets = entry.getValue();
        Set<OffsetEquation> subOffsets = map.get(sequence);

        if (!isSubtypeOffset(subOffsets, superOffsets)) {
          return false;
        }
      }

      return true;
    }

    /**
     * One set of offsets is a subtype of another if for every superOffsets, at least one suboffset
     * is greater than or equal to the superOffset.
     */
    private boolean isSubtypeOffset(
        Set<OffsetEquation> subOffsets, Set<OffsetEquation> superOffsets) {
      for (OffsetEquation superOffset : superOffsets) {
        boolean oneIsSubtype = false;
        for (OffsetEquation subOffset : subOffsets) {
          if (superOffset.lessThanOrEqual(subOffset)) {
            oneIsSubtype = true;
            break;
          }
        }
        if (!oneIsSubtype) {
          return false;
        }
      }
      return true;
    }

    /**
     * If other is Unknown, return Unknown. If other is Bottom, return this.
     *
     * <p>Otherwise lub is computed as follows:
     *
     * <p>1. Create the intersection of the sets of arrays for this and other.
     *
     * <p>2. For each sequence in the intersection, get the offsets for this and other. If any
     * offset in this is a less than or equal to an offset in other, then that offset is an offset
     * for the sequence in lub. If any offset in other is a less than or equal to an offset in this,
     * then that offset is an offset for the sequence in lub.
     *
     * @param other to lub with this
     * @return the lub
     */
    @Override
    public UBQualifier lub(UBQualifier other) {
      if (other.isUnknown()) {
        return other;
      } else if (other.isBottom()) {
        return this;
      } else if (other.isLiteral()) {
        return other.lub(this);
      }
      LessThanLengthOf otherLtl = (LessThanLengthOf) other;

      Set<String> sequences = new HashSet<>(map.keySet());
      sequences.retainAll(otherLtl.map.keySet());

      Map<String, Set<OffsetEquation>> lubMap =
          new HashMap<>(CollectionsPlume.mapCapacity(sequences));
      for (String sequence : sequences) {
        Set<OffsetEquation> offsets1 = map.get(sequence);
        Set<OffsetEquation> offsets2 = otherLtl.map.get(sequence);
        Set<OffsetEquation> lub = new HashSet<>(offsets1.size() + offsets2.size());
        for (OffsetEquation offset1 : offsets1) {
          for (OffsetEquation offset2 : offsets2) {
            if (offset2.lessThanOrEqual(offset1)) {
              lub.add(offset2);
            } else if (offset1.lessThanOrEqual(offset2)) {
              lub.add(offset1);
            }
          }
        }
        if (!lub.isEmpty()) {
          lubMap.put(sequence, lub);
        }
      }
      if (lubMap.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
      return new LessThanLengthOf(lubMap);
    }

    @Override
    public UBQualifier widenUpperBound(UBQualifier obj) {
      UBQualifier lub = lub(obj);
      if (!lub.isLessThanLengthQualifier() || !obj.isLessThanLengthQualifier()) {
        return lub;
      }
      Map<String, Set<OffsetEquation>> lubMap = ((LessThanLengthOf) lub).map;
      widenLub((LessThanLengthOf) obj, lubMap);
      if (lubMap.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
      return new LessThanLengthOf(lubMap);
    }

    /**
     *
     *
     * <pre>@LTLengthOf("a") int i = ...;
     * while (expr) {
     *   i++;
     * }</pre>
     *
     * <p>Dataflow never stops analyzing the above loop, because the type of i always changes after
     * each analysis of the loop:
     *
     * <p>1. @LTLengthOf(value="a', offset="-1")
     *
     * <p>2. @LTLengthOf(value="a', offset="-2")
     *
     * <p>3. @LTLengthOf(value="a', offset="-3")
     *
     * <p>In order to prevent this, if both types passed to lub include all the same sequences with
     * the same non-constant value offsets and if the constant value offsets are different then
     * remove that sequence-offset pair from lub.
     *
     * <p>For example:
     *
     * <p>LUB @LTLengthOf(value={"a", "b"}, offset={"0", "0") and @LTLengthOf(value={"a", "b"},
     * offset={"-20", "0") is @LTLengthOf("b")
     *
     * <p>This widened lub should only be used in order to break dataflow analysis loops.
     */
    private void widenLub(LessThanLengthOf other, Map<String, Set<OffsetEquation>> lubMap) {
      if (!containsSame(this.map.keySet(), lubMap.keySet())
          || !containsSame(other.map.keySet(), lubMap.keySet())) {
        return;
      }
      List<Pair<String, OffsetEquation>> remove = new ArrayList<>();
      for (Map.Entry<String, Set<OffsetEquation>> entry : lubMap.entrySet()) {
        String sequence = entry.getKey();
        Set<OffsetEquation> lubOffsets = entry.getValue();
        Set<OffsetEquation> thisOffsets = this.map.get(sequence);
        Set<OffsetEquation> otherOffsets = other.map.get(sequence);
        if (lubOffsets.size() != thisOffsets.size() || lubOffsets.size() != otherOffsets.size()) {
          return;
        }
        for (OffsetEquation lubEq : lubOffsets) {
          if (lubEq.isInt()) {
            int thisInt = OffsetEquation.getIntOffsetEquation(thisOffsets).getInt();
            int otherInt = OffsetEquation.getIntOffsetEquation(otherOffsets).getInt();
            if (thisInt != otherInt) {
              remove.add(Pair.of(sequence, lubEq));
            }
          } else if (thisOffsets.contains(lubEq) && otherOffsets.contains(lubEq)) {
            //  continue;
          } else {
            return;
          }
        }
      }
      for (Pair<String, OffsetEquation> pair : remove) {
        Set<OffsetEquation> offsets = lubMap.get(pair.first);
        offsets.remove(pair.second);
        if (offsets.isEmpty()) {
          lubMap.remove(pair.first);
        }
      }
    }

    @Override
    public UBQualifier glb(UBQualifier other) {
      if (other.isUnknown()) {
        return this;
      } else if (other.isBottom()) {
        return other;
      } else if (other.isLiteral()) {
        return other.glb(this);
      }
      LessThanLengthOf otherLtl = (LessThanLengthOf) other;

      Set<String> sequences = new HashSet<>(map.keySet());
      sequences.addAll(otherLtl.map.keySet());

      Map<String, Set<OffsetEquation>> glbMap = new HashMap<>(sequences.size());
      for (String sequence : sequences) {
        Set<OffsetEquation> glb = map.get(sequence);
        Set<OffsetEquation> otherglb = otherLtl.map.get(sequence);
        if (glb == null) {
          glb = otherglb;
        } else if (otherglb != null) {
          glb.addAll(otherglb);
        }
        glbMap.put(sequence, removeSmallerInts(glb));
      }
      return new LessThanLengthOf(glbMap);
    }

    /**
     * Returns a copy of the argument, but it contains just one offset equation that is an int value
     * -- the largest one in the argument. Any non-int offset equations appear in the result. Does
     * not side effect its argument.
     *
     * @param offsets a set of offset equations
     * @return a copy of the argument with just one int value (the largest in the input) and
     *     arbitrarily many non-ints
     */
    private Set<OffsetEquation> removeSmallerInts(Set<OffsetEquation> offsets) {
      Set<OffsetEquation> newOff = new HashSet<>(offsets.size());
      OffsetEquation literal = null;
      for (OffsetEquation eq : offsets) {
        if (eq.isInt()) {
          if (literal == null) {
            literal = eq;
          } else {
            literal = literal.lessThanOrEqual(eq) ? eq : literal;
          }
        } else {
          newOff.add(eq);
        }
      }
      if (literal != null) {
        newOff.add(literal);
      }
      return newOff;
    }

    /**
     * Adds node as an offset to a copy of this qualifier. This is done by creating an offset
     * equation for node and then adding that equation to every offset equation in a copy of this
     * object.
     *
     * @param node a Node
     * @param factory an AnnotatedTypeFactory
     * @return a copy of this qualifier with node add as an offset
     */
    @Override
    public UBQualifier plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) {
      return plusOrMinusOffset(node, factory, '+');
    }

    /**
     * Adds node as a negative offset to a copy of this qualifier. This is done by creating a
     * negative offset equation for node and then adding that equation to every offset equation in a
     * copy of this object.
     *
     * @param node a Node
     * @param factory an AnnotatedTypeFactory
     * @return a copy of this qualifier with node add as an offset
     */
    @Override
    public UBQualifier minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) {
      return plusOrMinusOffset(node, factory, '-');
    }

    /**
     * Adds node as a positive or negative offset to a copy of this qualifier. This is done by
     * creating an offset equation for node and then adding or subtracting that equation to every
     * offset equation in a copy of this object.
     *
     * @param node a Node
     * @param factory an AnnotatedTypeFactory
     * @param op either '-' or '+'
     * @return a copy of this qualifier with node add as an offset
     */
    private UBQualifier plusOrMinusOffset(
        Node node, UpperBoundAnnotatedTypeFactory factory, char op) {
      assert op == '-' || op == '+';

      // Try treating the offset as both an OffsetEquation and as a value.
      // Use whichever is not null, or glb the two.

      OffsetEquation newOffset = OffsetEquation.createOffsetFromNode(node, factory, op);
      LessThanLengthOf nodeOffsetQualifier = null;
      if (!newOffset.hasError()) {
        UBQualifier nodeOffsetQualifierMaybe = addOffset(newOffset);
        if (!(nodeOffsetQualifierMaybe instanceof UpperBoundUnknownQualifier)) {
          nodeOffsetQualifier = (LessThanLengthOf) nodeOffsetQualifierMaybe;
        }
      }

      OffsetEquation valueOffset =
          OffsetEquation.createOffsetFromNodesValue(
              node, factory.getValueAnnotatedTypeFactory(), op);
      LessThanLengthOf valueOffsetQualifier = null;
      if (valueOffset != null && !valueOffset.hasError()) {
        UBQualifier valueOffsetQualifierMaybe = addOffset(valueOffset);
        if (!(valueOffsetQualifierMaybe instanceof UpperBoundUnknownQualifier)) {
          valueOffsetQualifier = (LessThanLengthOf) valueOffsetQualifierMaybe;
        }
      }

      if (valueOffsetQualifier == null) {
        if (nodeOffsetQualifier == null) {
          return UpperBoundUnknownQualifier.UNKNOWN;
        } else {
          return nodeOffsetQualifier;
        }
      } else {
        if (nodeOffsetQualifier == null) {
          return valueOffsetQualifier;
        } else {
          return nodeOffsetQualifier.glb(valueOffsetQualifier);
        }
      }
    }

    /**
     * Adds value as an offset to a copy of this qualifier. This is done by adding value to every
     * offset equation in a copy of this object.
     *
     * @param value int value to add
     * @return a copy of this qualifier with value add as an offset
     */
    @Override
    public UBQualifier plusOffset(int value) {
      OffsetEquation newOffset = OffsetEquation.createOffsetForInt(value);
      return addOffset(newOffset);
    }

    /**
     * Adds the negation of value as an offset to a copy of this qualifier. This is done by adding
     * the negation of {@code value} to every offset equation in a copy of this object.
     *
     * @param value int value to add
     * @return a copy of this qualifier with value add as an offset
     */
    @Override
    public UBQualifier minusOffset(int value) {
      OffsetEquation newOffset = OffsetEquation.createOffsetForInt(-value);
      return addOffset(newOffset);
    }

    /**
     * Returns a copy of this qualifier with sequence-offset pairs where in the original the offset
     * contains an access of an sequence length in {@code sequences}. The sequence length access has
     * been removed from the offset. If the original qualifier has no sequence length offsets, then
     * UNKNOWN is returned.
     *
     * @param sequences access of the length of these sequences are removed
     * @return a copy of this qualifier with some offsets removed
     */
    public UBQualifier removeSequenceLengthAccess(final List<String> sequences) {
      if (sequences.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
      OffsetEquationFunction removeSequenceLengthsFunc =
          new OffsetEquationFunction() {
            @Override
            public OffsetEquation compute(OffsetEquation eq) {
              return eq.removeSequenceLengths(sequences);
            }
          };
      return computeNewOffsets(removeSequenceLengthsFunc);
    }
    /**
     * Returns a copy of this qualifier with sequence-offset pairs where in the original the offset
     * contains an access of an sequence length in {@code sequences}. The sequence length access has
     * been removed from the offset. If the offset also has -1 then -1 is also removed.
     *
     * @param sequences access of the length of these sequences are removed
     * @return a copy of this qualifier with some offsets removed
     */
    public UBQualifier removeSequenceLengthAccessAndNeg1(final List<String> sequences) {
      if (sequences.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
      OffsetEquationFunction removeSequenceLenFunc =
          new OffsetEquationFunction() {
            @Override
            public OffsetEquation compute(OffsetEquation eq) {
              OffsetEquation newEq = eq.removeSequenceLengths(sequences);
              if (newEq == null) {
                return null;
              }
              if (newEq.getInt() == -1) {
                return newEq.copyAdd('+', OffsetEquation.ONE);
              }
              return newEq;
            }
          };
      return computeNewOffsets(removeSequenceLenFunc);
    }

    private UBQualifier addOffset(final OffsetEquation newOffset) {
      OffsetEquationFunction addOffsetFunc =
          new OffsetEquationFunction() {
            @Override
            public OffsetEquation compute(OffsetEquation eq) {
              return eq.copyAdd('+', newOffset);
            }
          };
      return computeNewOffsets(addOffsetFunc);
    }

    /**
     * If divisor == 1, return this object.
     *
     * <p>If divisor greater than 1, then return a copy of this object keeping only sequences and
     * offsets where the offset is less than or equal to zero.
     *
     * <p>Otherwise, return UNKNOWN.
     *
     * @param divisor number to divide by
     * @return the result of dividing a value with this qualifier by divisor
     */
    public UBQualifier divide(int divisor) {
      if (divisor == 1) {
        return this;
      } else if (divisor > 1) {
        OffsetEquationFunction divideFunc =
            new OffsetEquationFunction() {
              @Override
              public OffsetEquation compute(OffsetEquation eq) {
                if (eq.isNegativeOrZero()) {
                  return eq;
                }
                return null;
              }
            };
        return computeNewOffsets(divideFunc);
      }
      return UpperBoundUnknownQualifier.UNKNOWN;
    }

    public boolean isValuePlusOffsetLessThanMinLen(String sequence, long value, int minlen) {
      Set<OffsetEquation> offsets = map.get(sequence);
      if (offsets == null) {
        return false;
      }
      for (OffsetEquation offset : offsets) {
        if (offset.isInt()) {
          // This expression must not overflow
          return (long) minlen - offset.getInt() > value;
        }
      }
      return false;
    }

    /**
     * Checks whether replacing sequence with replacementSequence in this qualifier creates
     * replacementSequence entry in other.
     */
    public boolean isValidReplacement(
        String sequence, String replacementSequence, LessThanLengthOf other) {
      Set<OffsetEquation> offsets = map.get(sequence);
      if (offsets == null) {
        return false;
      }
      Set<OffsetEquation> otherOffsets = other.map.get(replacementSequence);
      if (otherOffsets == null) {
        return false;
      }
      return containsSame(offsets, otherOffsets);
    }

    @Override
    public String toString() {
      return "LessThanLengthOf{" + "map=" + map + '}';
    }

    public Iterable<? extends String> getSequences() {
      return map.keySet();
    }

    /**
     * Generates a new UBQualifer without the given (sequence, offset) pair. Other occurrences of
     * the sequence and the offset may remain in the result, but not together.
     *
     * @param sequence a Java expression representing a string
     * @param offset an integral offset
     * @return a new UBQualifer without the given sequence and offset
     */
    public UBQualifier removeOffset(String sequence, int offset) {
      OffsetEquation offsetEq = OffsetEquation.createOffsetForInt(offset);
      Map<String, Set<OffsetEquation>> newMap = copyMap();
      Set<OffsetEquation> equations = newMap.get(sequence);
      if (equations != null) {
        equations.remove(offsetEq);
        if (equations.isEmpty()) {
          newMap.remove(sequence);
        }
      }

      if (newMap.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      } else {
        return new LessThanLengthOf(newMap);
      }
    }

    /** Functional interface that operates on {@link OffsetEquation}s. */
    interface OffsetEquationFunction {
      /**
       * Returns the result of the computation or null if the passed equation should be removed.
       *
       * @param eq current offset equation
       * @return the result of the computation or null if the passed equation should be removed
       */
      OffsetEquation compute(OffsetEquation eq);
    }

    /**
     * Returns a new qualifier that is a copy of this qualifier with the OffsetEquationFunction
     * applied to each offset.
     *
     * <p>If the {@link OffsetEquationFunction} returns null, it's not added as an offset. If after
     * all functions have been applied, an sequence has no offsets, then that sequence is not added
     * to the returned qualifier. If no sequences are added to the returned qualifier, then UNKNOWN
     * is returned.
     *
     * @param f function to apply
     * @return a new qualifier that is a copy of this qualifier with the OffsetEquationFunction
     *     applied to each offset
     */
    private UBQualifier computeNewOffsets(OffsetEquationFunction f) {
      Map<String, Set<OffsetEquation>> newMap = new HashMap<>(map.size());
      for (Map.Entry<String, Set<OffsetEquation>> entry : map.entrySet()) {
        Set<OffsetEquation> offsets = new HashSet<>(entry.getValue().size());
        for (OffsetEquation eq : entry.getValue()) {
          OffsetEquation newEq = f.compute(eq);
          if (newEq != null) {
            offsets.add(newEq);
          }
        }
        if (!offsets.isEmpty()) {
          newMap.put(entry.getKey(), offsets);
        }
      }
      if (newMap.isEmpty()) {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
      return new LessThanLengthOf(newMap);
    }
  }

  /** Represents an integer value that is known at compile time. */
  public static class UpperBoundLiteralQualifier extends UBQualifier {

    /** Represents the value -1. */
    public static UpperBoundLiteralQualifier NEGATIVEONE = new UpperBoundLiteralQualifier(-1);
    /** Represents the value 0. */
    public static UpperBoundLiteralQualifier ZERO = new UpperBoundLiteralQualifier(0);
    /** Represents the value 1. */
    public static UpperBoundLiteralQualifier ONE = new UpperBoundLiteralQualifier(1);

    /**
     * Creates a new UpperBoundLiteralQualifier, without using cached values.
     *
     * @param value the integer value
     */
    private UpperBoundLiteralQualifier(int value) {
      this.value = value;
    }

    /**
     * Creates an UpperBoundLiteralQualifier.
     *
     * @param value the integer value
     * @return an UpperBoundLiteralQualifier
     */
    public static UpperBoundLiteralQualifier create(int value) {
      switch (value) {
        case -1:
          return NEGATIVEONE;
        case 0:
          return ZERO;
        case 1:
          return ONE;
        default:
          return new UpperBoundLiteralQualifier(value);
      }
    }

    /** The integer value. */
    int value;

    /**
     * Returns the integer value.
     *
     * @return the integer value
     */
    int getValue() {
      return value;
    }

    @Override
    public boolean isLiteral() {
      return true;
    }

    @Override
    public boolean isSubtype(UBQualifier superType) {
      if (superType.isUnknown()) {
        return true;
      } else if (superType.isBottom()) {
        return false;
      } else if (superType.isLiteral()) {
        int otherValue = ((UpperBoundLiteralQualifier) superType).value;
        return value == otherValue;
      }

      LessThanLengthOf superTypeLTL = (LessThanLengthOf) superType;
      return superTypeLTL.literalIsSubtype(value);
    }

    @Override
    public UBQualifier lub(UBQualifier other) {
      if (isSubtype(other)) {
        return other;
      } else {
        return UpperBoundUnknownQualifier.UNKNOWN;
      }
    }

    @Override
    public UBQualifier glb(UBQualifier other) {
      if (isSubtype(other)) {
        return this;
      } else {
        return UpperBoundBottomQualifier.BOTTOM;
      }
    }

    @Override
    public String toString() {
      return "Literal(" + value + ")";
    }
  }

  /** The top type qualifier. */
  public static class UpperBoundUnknownQualifier extends UBQualifier {
    /** The canonical representative. */
    static final UBQualifier UNKNOWN = new UpperBoundUnknownQualifier();

    /** This class is a singleton. */
    private UpperBoundUnknownQualifier() {}

    @Override
    public boolean isSubtype(UBQualifier superType) {
      return superType.isUnknown();
    }

    @Override
    public boolean isUnknown() {
      return true;
    }

    @Override
    public UBQualifier lub(UBQualifier other) {
      return this;
    }

    @Override
    public UBQualifier glb(UBQualifier other) {
      return other;
    }

    @Override
    public String toString() {
      return "UNKNOWN";
    }
  }

  private static class UpperBoundBottomQualifier extends UBQualifier {
    static final UBQualifier BOTTOM = new UpperBoundBottomQualifier();

    @Override
    public boolean isBottom() {
      return true;
    }

    @Override
    public boolean isSubtype(UBQualifier superType) {
      return true;
    }

    @Override
    public UBQualifier lub(UBQualifier other) {
      return other;
    }

    @Override
    public UBQualifier glb(UBQualifier other) {
      return this;
    }

    @Override
    public String toString() {
      return "BOTTOM";
    }
  }

  private static class PolyQualifier extends UBQualifier {
    static final UBQualifier POLY = new PolyQualifier();

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

    @Override
    public boolean isSubtype(UBQualifier superType) {
      return superType.isUnknown() || superType.isPoly();
    }

    @Override
    public UBQualifier lub(UBQualifier other) {
      if (other.isPoly() || other.isBottom()) {
        return this;
      }
      return UpperBoundUnknownQualifier.UNKNOWN;
    }

    @Override
    public UBQualifier glb(UBQualifier other) {
      if (other.isPoly() || other.isUnknown()) {
        return this;
      }
      return UpperBoundBottomQualifier.BOTTOM;
    }
  }
}