bdd_operator_init(cs);
bdd_operator_init(cachesize);
    protected void initialize(int initnodesize, int cs) {        int n;        if (bddrunning)            throw new JavaBDDException(BDD_RUNNING);        bddnodesize = bdd_prime_gte(initnodesize);        bddnodes = new int[bddnodesize*__node_size];        bddresized = false;        for (n = 0; n < bddnodesize; n++) {            SETLOW(n, INVALID_BDD);            SETNEXT(n, n+1);        }        SETNEXT(bddnodesize-1, 0);        SETMAXREF(0);        SETMAXREF(1);        SETLOW(0, 0); SETHIGH(0, 0);        SETLOW(1, 1); SETHIGH(1, 1);        bdd_operator_init(cs);        bddfreepos = 2;        bddfreenum = bddnodesize - 2;        bddrunning = true;        bddvarnum = 0;        gbcollectnum = 0;        gbcclock = 0;        cachesize = cs;        usednodes_nextreorder = bddnodesize;        bddmaxnodeincrease = DEFAULTMAXNODEINC;        bdderrorcond = 0;        bdd_pairs_init();        bdd_reorder_init();        return;    }