class BDDInteger {

  public BDD range(long a, long b) {
    checkArgument(a <= b, "range is not ordered correctly");
    checkArgument(a >= 0, "value is negative");
    checkArgument(b < (1L << _bitvec.length), "value %s is out of range", b);

    if (a == b) {
      return value(a);
    }

    long bitOfFirstDifference = Long.highestOneBit(a ^ b);
    int sizeOfDifferentSuffix = Long.numberOfTrailingZeros(bitOfFirstDifference) + 1;
    BDD geqA = geqN(a, sizeOfDifferentSuffix);
    BDD leqB = leqN(b, sizeOfDifferentSuffix);

    BDD between = geqA.and(leqB);
    long currentVal = a >> sizeOfDifferentSuffix;
    for (int i = sizeOfDifferentSuffix; i < _bitvec.length; ++i) {
      BDD bit = _bitvec[_bitvec.length - i - 1];
      if ((currentVal & 1) != 0) {
        between = bit.and(between);
      } else {
        between = bit.less(between); // "not i and x" rewritten "i less x"
      }
      currentVal >>= 1;
    }
    return between;
  }

  private  BDDInteger(BDDFactory factory, int length);
  public  BDDInteger(BDDInteger other);

}