@Test public void testAdd() { BDDFactory factory = BDDUtils.bddFactory(10); BDDInteger x = BDDInteger.makeFromIndex(factory, 5, 0, false); assertTrue(x.hasVariablesOnly()); BDDInteger constant1 = BDDInteger.makeFromValue(factory, 5, 1); assertFalse(constant1.hasVariablesOnly()); BDDInteger xPlus1 = x.add(constant1); assertFalse(xPlus1.hasVariablesOnly()); assertTrue(x.value(0).equals(xPlus1.value(1))); assertTrue(x.value(1).equals(xPlus1.value(2))); assertTrue(x.value(31).equals(xPlus1.value(0))); assertThat(x.getValuesSatisfying(x.value(3L), 100), contains(3L)); assertThat(xPlus1.getValuesSatisfying(xPlus1.value(3L), 100), contains(3L)); BDDInteger y = BDDInteger.makeFromIndex(factory, 5, 5, false); BDD[] bv1 = xPlus1.getBitvec(); BDD[] bv2 = y.getBitvec(); BDD yEqXPlus1 = factory.one(); for (int i = 0; i < bv2.length; i++) { yEqXPlus1 = yEqXPlus1.and(bv2[i].biimp(bv1[i])); } assertThat(y.getValuesSatisfying(yEqXPlus1.and(x.value(1)), 5), contains(2L)); assertThat(y.getValuesSatisfying(yEqXPlus1.and(x.value(10)), 5), contains(11L)); assertThat(y.getValuesSatisfying(yEqXPlus1.and(x.value(31)), 5), contains(0L)); assertThat(x.getValuesSatisfying(yEqXPlus1.and(y.value(0)), 5), contains(31L)); assertThat(x.getValuesSatisfying(yEqXPlus1.and(y.value(10)), 5), contains(9L)); assertThat(x.getValuesSatisfying(yEqXPlus1.and(y.value(31)), 5), contains(30L)); }
public BDDInteger add(BDDInteger other) { BDD[] as = _bitvec; BDD[] bs = other._bitvec; checkArgument(as.length > 0, "Cannot add BDDIntegers of length 0"); checkArgument(as.length == bs.length, "Cannot add BDDIntegers of different length"); BDD carry = _factory.zero(); BDDInteger sum = new BDDInteger(_factory, as.length); BDD[] cs = sum._bitvec; for (int i = cs.length - 1; i > 0; --i) { cs[i] = as[i].xor(bs[i]).xor(carry); carry = as[i].and(bs[i]).or(carry.and(as[i].or(bs[i]))); } cs[0] = as[0].xor(bs[0]).xor(carry); sum._hasVariablesOnly = false; return sum; }
BDDInteger { public BDDInteger add(BDDInteger other) { BDD[] as = _bitvec; BDD[] bs = other._bitvec; checkArgument(as.length > 0, "Cannot add BDDIntegers of length 0"); checkArgument(as.length == bs.length, "Cannot add BDDIntegers of different length"); BDD carry = _factory.zero(); BDDInteger sum = new BDDInteger(_factory, as.length); BDD[] cs = sum._bitvec; for (int i = cs.length - 1; i > 0; --i) { cs[i] = as[i].xor(bs[i]).xor(carry); carry = as[i].and(bs[i]).or(carry.and(as[i].or(bs[i]))); } cs[0] = as[0].xor(bs[0]).xor(carry); sum._hasVariablesOnly = false; return sum; } }
BDDInteger { public BDDInteger add(BDDInteger other) { BDD[] as = _bitvec; BDD[] bs = other._bitvec; checkArgument(as.length > 0, "Cannot add BDDIntegers of length 0"); checkArgument(as.length == bs.length, "Cannot add BDDIntegers of different length"); BDD carry = _factory.zero(); BDDInteger sum = new BDDInteger(_factory, as.length); BDD[] cs = sum._bitvec; for (int i = cs.length - 1; i > 0; --i) { cs[i] = as[i].xor(bs[i]).xor(carry); carry = as[i].and(bs[i]).or(carry.and(as[i].or(bs[i]))); } cs[0] = as[0].xor(bs[0]).xor(carry); sum._hasVariablesOnly = false; return sum; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); }
BDDInteger { public BDDInteger add(BDDInteger other) { BDD[] as = _bitvec; BDD[] bs = other._bitvec; checkArgument(as.length > 0, "Cannot add BDDIntegers of length 0"); checkArgument(as.length == bs.length, "Cannot add BDDIntegers of different length"); BDD carry = _factory.zero(); BDDInteger sum = new BDDInteger(_factory, as.length); BDD[] cs = sum._bitvec; for (int i = cs.length - 1; i > 0; --i) { cs[i] = as[i].xor(bs[i]).xor(carry); carry = as[i].and(bs[i]).or(carry.and(as[i].or(bs[i]))); } cs[0] = as[0].xor(bs[0]).xor(carry); sum._hasVariablesOnly = false; return sum; } 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 BDDInteger add(BDDInteger other) { BDD[] as = _bitvec; BDD[] bs = other._bitvec; checkArgument(as.length > 0, "Cannot add BDDIntegers of length 0"); checkArgument(as.length == bs.length, "Cannot add BDDIntegers of different length"); BDD carry = _factory.zero(); BDDInteger sum = new BDDInteger(_factory, as.length); BDD[] cs = sum._bitvec; for (int i = cs.length - 1; i > 0; --i) { cs[i] = as[i].xor(bs[i]).xor(carry); carry = as[i].and(bs[i]).or(carry.and(as[i].or(bs[i]))); } cs[0] = as[0].xor(bs[0]).xor(carry); sum._hasVariablesOnly = false; return sum; } 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();  }