PUSHREF(res); PUSHREF(res_not); PUSHREF(univ); res = zdd_makenode(k, (k == bddvarnum)?0:res, res); res_not = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not); if (bdv == bddvarnum) univ = zdd_makenode(k, univ, univ); POPREF(3);
int res2 = zdd_makenode(k, (k == bddvarnum)?0:res, res); INCREF(res2); DECREF(res); res = res2;  int res_not2 = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not); INCREF(res_not2); DECREF(res_not); res_not = res_not2;  if (bdv == bddvarnum) { int univ2 = zdd_makenode(k, univ, univ); INCREF(univ2); DECREF(univ); univ = univ2; }
    int bdd_setvarnum(int num) {        int bdv;        int oldbddvarnum = bddvarnum;        if (num < 1 || num > MAXVAR) {            bdd_error(BDD_RANGE);            return bddfalse;        }        if (num < bddvarnum)            return bdd_error(BDD_DECVNUM);        if (num == bddvarnum)            return 0;        bdd_disable_reorder();        if (bddvarset == null) {            bddvarset = new int[num * 2];            bddlevel2var = new int[num + 1];            bddvar2level = new int[num + 1];        } else {            int[] bddvarset2 = new int[num * 2];            System.arraycopy(bddvarset, 0, bddvarset2, 0, bddvarset.length);            bddvarset = bddvarset2;            int[] bddlevel2var2 = new int[num + 1];            System.arraycopy(                bddlevel2var,                0,                bddlevel2var2,                0,                bddlevel2var.length);            bddlevel2var = bddlevel2var2;            int[] bddvar2level2 = new int[num + 1];            System.arraycopy(                bddvar2level,                0,                bddvar2level2,                0,                bddvar2level.length);            bddvar2level = bddvar2level2;        }        if (bddrefstack != null)            free(bddrefstack);        bddrefstack = new int[num * 2 + 1];        bddrefstacktop = 0;        if (ZDD)            bddvarnum = 0; // need to recreate all of them for ZDD                univ = 1;        for (bdv = bddvarnum; bddvarnum < num; bddvarnum++) {            if (ZDD) {                int res = 1, res_not = 1;                for (int k = num-1; k >= 0; --k) {                    PUSHREF(res);                    PUSHREF(res_not);                    PUSHREF(univ);                    res = zdd_makenode(k, (k == bddvarnum)?0:res, res);                    res_not = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not);                    if (bdv == bddvarnum) univ = zdd_makenode(k, univ, univ);                    POPREF(3);                }                bddvarset[bddvarnum * 2] = res;                bddvarset[bddvarnum * 2 + 1] = res_not;                SETMAXREF(univ);            } else {                bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1));                bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0);                POPREF(1);            }            if (bdderrorcond != 0) {                bddvarnum = bdv;                return -bdderrorcond;            }                        SETMAXREF(bddvarset[bddvarnum * 2]);            SETMAXREF(bddvarset[bddvarnum * 2 + 1]);            bddlevel2var[bddvarnum] = bddvarnum;            bddvar2level[bddvarnum] = bddvarnum;        }        SETLEVELANDMARK(0, num);        SETLEVELANDMARK(1, num);        bddvar2level[num] = num;        bddlevel2var[num] = num;        bdd_pairs_resize(oldbddvarnum, bddvarnum);        bdd_operator_varresize();        if (ZDD) {            System.out.println("Changed number of ZDD variables, all existing ZDDs are now invalid.");            // Need to rebuild varsets for existing domains.            for (int n = 0; n < fdvarnum; n++) {                domain[n].var.free();                domain[n].var = makeSet(domain[n].ivar);            }        }                bdd_enable_reorder();        return 0;    }