class BDDInteger {

  public Long satAssignmentToLong(BDD satAssignment) {
    checkArgument(satAssignment.isAssignment(), "not a satisfying assignment");

    if (_hasVariablesOnly) {
      // Shortcut for performance.
      return satAssignmentToLong(satAssignment.minAssignmentBits());
    }

    if (_bitvec.length > Long.SIZE) {
      throw new IllegalArgumentException(
          "Can't get a representative of a BDDInteger with more than Long.SIZE bits");
    }

    long value = 0;
    for (int i = 0; i < _bitvec.length; i++) {
      BDD bitBDD = _bitvec[_bitvec.length - i - 1];
      // a.diff(b) is a.and(b.not()). When the input is only a partial assignment (like satOne),
      // this biases towards lexicographically smaller solutions: set a 1 only if you can't set 0.
      if (!satAssignment.diffSat(bitBDD)) {
        value |= 1L << i;
      }
    }
    return value;
  }

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

}