@Test public void testRange() { BDDFactory factory = BDDUtils.bddFactory(10); BDDInteger x = BDDInteger.makeFromIndex(factory, 5, 0, false); for (int a = 0; a < 32; ++a) { for (int b = a; b < 32; ++b) { BDD range = x.range(a, b); BDD rangeEquiv = x.geq(a).and(x.leq(b)); assertThat(range, equalTo(rangeEquiv)); } } }
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); } currentVal >>= 1; } return between; }
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); } currentVal >>= 1; } return between; } }
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); } currentVal >>= 1; } return between; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); }
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); } currentVal >>= 1; } return between; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); boolean hasVariablesOnly(); int size(); static BDDInteger makeFromIndex(
      BDDFactory factory, int length, int start, boolean reverse); Optional<Long> getValueSatisfying(BDD bdd); Long satAssignmentToLong(BDD satAssignment); Long satAssignmentToLong(BitSet bits); List<Long> getValuesSatisfying(BDD bdd, int max); static BDDInteger makeFromValue(BDDFactory factory, int length, long value); BDDInteger ite(BDD b, BDDInteger other); BDD value(long val); BDD leq(long val); BDD geq(long val); BDD range(long a, long b); void setValue(long val); void setValue(BDDInteger other); BDDInteger add(BDDInteger other); BDDInteger sub(BDDInteger var1); BDD[] getBitvec(); @Nonnull BDD getVars(); BDDFactory getFactory(); @Override boolean equals(Object o); @Override int hashCode(); }
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); } currentVal >>= 1; } return between; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); boolean hasVariablesOnly(); int size(); static BDDInteger makeFromIndex(
      BDDFactory factory, int length, int start, boolean reverse); Optional<Long> getValueSatisfying(BDD bdd); Long satAssignmentToLong(BDD satAssignment); Long satAssignmentToLong(BitSet bits); List<Long> getValuesSatisfying(BDD bdd, int max); static BDDInteger makeFromValue(BDDFactory factory, int length, long value); BDDInteger ite(BDD b, BDDInteger other); BDD value(long val); BDD leq(long val); BDD geq(long val); BDD range(long a, long b); void setValue(long val); void setValue(BDDInteger other); BDDInteger add(BDDInteger other); BDDInteger sub(BDDInteger var1); BDD[] getBitvec(); @Nonnull BDD getVars(); BDDFactory getFactory(); @Override boolean equals(Object o); @Override int hashCode();  }