public BDD buildAdd(BDDDomain that, int bits, long value) { if (bits > this.varNum() || bits > that.varNum()) throw new BDDException("Number of bits requested ("+bits+") is larger than domain sizes "+this.varNum()+","+that.varNum());  BDDFactory bdd = getFactory();  if (value == 0L) { BDD result = bdd.one(); int n; for (n = 0; n < bits; n++) { BDD b = bdd.ithVar(this.ivar[n]); b.biimpWith(bdd.ithVar(that.ivar[n])); result.andWith(b); } for ( ; n < Math.max(this.varNum(), that.varNum()); n++) { BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one(); b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one()); result.andWith(b); } return result; }  int[] vars = new int[bits]; System.arraycopy(this.ivar, 0, vars, 0, vars.length); BDDBitVector y = bdd.buildVector(vars); BDDBitVector v = bdd.constantVector(bits, value); BDDBitVector z = y.add(v);  int[] thatvars = new int[bits]; System.arraycopy(that.ivar, 0, thatvars, 0, thatvars.length); BDDBitVector x = bdd.buildVector(thatvars); BDD result = bdd.one(); int n; for (n = 0; n < x.size(); n++) { BDD b = x.bitvec[n].biimp(z.bitvec[n]); result.andWith(b); } for ( ; n < Math.max(this.varNum(), that.varNum()); n++) { BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one(); b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one()); result.andWith(b); } x.free(); y.free(); z.free(); v.free(); return result;
public BDD buildAdd(BDDDomain that, long value) { if (this.varNum() != that.varNum()) throw new BDDException(); return buildAdd(that, this.varNum(), value);
    public BDD buildAdd(BDDDomain that, int bits, long value) {        if (bits > this.varNum() ||            bits > that.varNum())            throw new BDDException("Number of bits requested ("+bits+") is larger than domain sizes "+this.varNum()+","+that.varNum());                BDDFactory bdd = getFactory();                if (value == 0L) {            BDD result = bdd.one();            int n;            for (n = 0; n < bits; n++) {                BDD b = bdd.ithVar(this.ivar[n]);                b.biimpWith(bdd.ithVar(that.ivar[n]));                result.andWith(b);            }            for ( ; n < Math.max(this.varNum(), that.varNum()); n++) {                BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one();                b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one());                result.andWith(b);            }            return result;        }        int[] vars = new int[bits];        System.arraycopy(this.ivar, 0, vars, 0, vars.length);        BDDBitVector y = bdd.buildVector(vars);        BDDBitVector v = bdd.constantVector(bits, value);        BDDBitVector z = y.add(v);                int[] thatvars = new int[bits];        System.arraycopy(that.ivar, 0, thatvars, 0, thatvars.length);        BDDBitVector x = bdd.buildVector(thatvars);        BDD result = bdd.one();        int n;        for (n = 0; n < x.size(); n++) {            BDD b = x.bitvec[n].biimp(z.bitvec[n]);            result.andWith(b);        }        for ( ; n < Math.max(this.varNum(), that.varNum()); n++) {            BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one();            b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one());            result.andWith(b);        }        x.free(); y.free(); z.free(); v.free();        return result;    }