buddy/src/reorder.c

89 static levelData *levels; /* Indexed by variable! */
113 #define NODEHASH(var,l,h) ((PAIR((l),(h))%levels[var].size)+levels[var].start)
654 	 p[n].val -= levels[v].nodenum;
823       levels[VAR(r) & MARKHIDE].nodenum++;
898 	 levels[VARp(node)].nodenum++;
963       levels[n].maxsize = bddnodesize / bddvarnum;
964       levels[n].start = n * levels[n].maxsize;
965       levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4);
967       levels[n].maxsize = bddnodesize / bddvarnum;
968       levels[n].start = n * levels[n].maxsize;
969       levels[n].size = levels[n].maxsize;
972       if (levels[n].size >= 4)
973 	 levels[n].size = bdd_prime_lte(levels[n].size);
976       printf("L%3d: start %d, size %d, nodes %d\n", n, levels[n].start,
977 	     levels[n].size, levels[n].nodenum);
1090    levels[var].nodenum++;
1121    int vl0 = levels[var0].start;
1122    int size0 = levels[var0].size;
1125    levels[var0].nodenum = 0;
1144 	    levels[var0].nodenum++;
1218       levels[var1].nodenum++;
1237    int vl1 = levels[var1].start;
1238    int size1 = levels[var1].size;
1265 	    levels[var1].nodenum--;
1327       levels[var1].nodenum++;
1339    int vl1 = levels[var1].start;
1340    int size1 = levels[var1].size;
1367 	    levels[var1].nodenum--;
1376    if (levels[var1].nodenum < levels[var1].size)
1377       levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size/2);
1379       levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size*2);
1381    if (levels[var1].size >= 4)
1382       levels[var1].size = bdd_prime_lte(levels[var1].size);
1421       for (n=0 ; n<levels[v].size ; n++)
1423 	 r = bddnodes[n+levels[v].start].hash;
1434       assert(vcou == levels[v].nodenum);
1466       levelData *l = &levels[var];
1647    if ((levels=NEW(levelData,bddvarnum)) == NULL)
1652       levels[n].start = -1;
1653       levels[n].size = 0;
1654       levels[n].nodenum = 0;
1698       printf("%3d: %4d nodes , %4d entries\n", n, levels[n].nodenum,
1699 	     levels[n].size);
1702    free(levels);
2225 	   from {\tt bdd\_addvarblock}. The block levels depends on the