class 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);
  public  BDDInteger(BDDInteger other);

}