public int setCacheSize(int newcachesize) { int old = cachesize; BddCache_resize(applycache, newcachesize); BddCache_resize(itecache, newcachesize); BddCache_resize(quantcache, newcachesize); BddCache_resize(appexcache, newcachesize); BddCache_resize(replacecache, newcachesize); BddCache_resize(misccache, newcachesize); BddCache_resize(countcache, newcachesize); return old; }
public int setCacheSize(int v) { return bdd_setcachesize(v); }
    public int setCacheSize(int newcachesize) {        int old = cachesize;        BddCache_resize(applycache, newcachesize);        BddCache_resize(itecache, newcachesize);        BddCache_resize(quantcache, newcachesize);        BddCache_resize(appexcache, newcachesize);        BddCache_resize(replacecache, newcachesize);        BddCache_resize(misccache, newcachesize);        BddCache_resize(countcache, newcachesize);        return old;    }