Menu
▾
▴
[Javabdd-checkins] JavaBDD/buddy/src bddop.c,1.3,1.4 kernel.h,1.2,1.3 kernel.c,1.2,1.3 reorder.c,1.2,1.3 bddio.c,1.2,1.3
|
From: John W. <joe...@us...> - 2004-10-01 02:17:34
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22244/buddy/src Modified Files: bddop.c kernel.h kernel.c reorder.c bddio.c Log Message: Implement bitfields directly, because the compiler does a poor job at it. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** kernel.h 29 Sep 2004 10:03:50 -0000 1.2 --- kernel.h 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 79,84 **** --- 79,88 ---- typedef struct s_BddNode /* Node table entry */ { + #if defined(USE_BITFIELDS) unsigned int refcou : 10; unsigned int level : 22; + #else + unsigned int refcou_and_level; + #endif int low; int high; *************** *** 122,141 **** /* Reference counting */ ! #define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou-- ! #define INCREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou++ ! #define DECREFp(n) if (n->refcou!=MAXREF && n->refcou>0) n->refcou-- ! #define INCREFp(n) if (n->refcou<MAXREF) n->refcou++ ! #define HASREF(n) (bddnodes[n].refcou > 0) /* Marking BDD nodes */ ! #define MARKON 0x200000 /* Bit used to mark a node (1) */ ! #define MARKOFF 0x1FFFFF /* - unmark */ #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (bddnodes[n].level |= MARKON) ! #define UNMARK(n) (bddnodes[n].level &= MARKOFF) ! #define MARKED(n) (bddnodes[n].level & MARKON) ! #define SETMARKp(p) (node->level |= MARKON) ! #define UNMARKp(p) (node->level &= MARKOFF) ! #define MARKEDp(p) (node->level & MARKON) /* Hashfunctions */ --- 126,167 ---- /* Reference counting */ ! #if defined(USE_BITFIELDS) ! #define DECREF(n) if (REF(n)!=MAXREF && REF(n)>0) bddnodes[n].refcou-- ! #define INCREF(n) if (REF(n)<MAXREF) bddnodes[n].refcou++ ! #define DECREFp(n) if (REFp(n)!=MAXREF && REFp(n)>0) n->refcou-- ! #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou++ ! #define HASREF(n) (REF(n) > 0) ! #else ! #define DECREF(n) if (REF(n)!=MAXREF && REF(n)>0) bddnodes[n].refcou_and_level-- ! #define INCREF(n) if (REF(n)<MAXREF) bddnodes[n].refcou_and_level++ ! #define DECREFp(n) if (REFp(n)!=MAXREF && REFp(n)>0) n->refcou_and_level-- ! #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ ! #define HASREF(n) (REF(n) > 0) ! #endif /* Marking BDD nodes */ ! ! #if defined(USE_BITFIELDS) ! #define MARKON1 0x200000 /* Bit used to mark a node (1) */ ! #define MARKOFF1 0x1FFFFF /* - unmark */ #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (LEVEL(n) |= MARKON1) ! #define UNMARK(n) (LEVEL(n) &= MARKOFF1) ! #define MARKED(n) (LEVEL(n) & MARKON1) ! #define SETMARKp(p) (LEVELp(p) |= MARKON1) ! #define UNMARKp(p) (LEVELp(p) &= MARKOFF1) ! #define MARKEDp(p) (LEVELp(p) & MARKON1) ! #else ! #define MARKON2 0x80000000 /* Bit used to mark a node (1) */ ! #define MARKOFF2 0x7FFFFFFF /* - unmark */ ! #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (bddnodes[n].refcou_and_level |= MARKON2) ! #define UNMARK(n) (bddnodes[n].refcou_and_level &= MARKOFF2) ! #define MARKED(n) (bddnodes[n].refcou_and_level & MARKON2) ! #define SETMARKp(p) ((p)->refcou_and_level |= MARKON2) ! #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) ! #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif ! /* Hashfunctions */ *************** *** 150,159 **** #define ISONE(a) ((a) == 1) #define ISZERO(a) ((a) == 0) - #define LEVEL(a) (bddnodes[a].level) #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) - #define LEVELp(p) ((p)->level) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) /* Stacking for garbage collector */ --- 176,204 ---- #define ISONE(a) ((a) == 1) #define ISZERO(a) ((a) == 0) #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) + #if defined(USE_BITFIELDS) + #define REF(n) (bddnodes[n].refcou) + #define REFp(n) ((n)->refcou) + #define SETREF(n,v) (bddnodes[n].refcou = (v)) + #define SETREFp(n,v) ((n)->refcou = (v)) + #define LEVEL(n) (bddnodes[n].level) + #define LEVELp(p) ((p)->level) + #define SETLEVEL(n,v) (LEVEL(n) = (v)) + #define SETLEVELp(p,v) (LEVELp(p) = (v)) + #define CLRLEVELREF(n) (bddnodes[n].refcou = bddnodes[n].level = 0) + #else + #define REF(n) (bddnodes[n].refcou_and_level & MAXREF) + #define REFp(n) ((n)->refcou_and_level & MAXREF) + #define SETREF(n,v) (bddnodes[n].refcou_and_level = (bddnodes[n].refcou_and_level & ~MAXREF) | (v)) + #define SETREFp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & ~MAXREF) | (v)) + #define LEVEL(n) (bddnodes[n].refcou_and_level >> 10) + #define LEVELp(p) ((p)->refcou_and_level >> 10) + #define SETLEVEL(n,v) (bddnodes[n].refcou_and_level = (bddnodes[n].refcou_and_level & MAXREF) | (v << 10)) + #define SETLEVELp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) + #define CLRLEVELREF(n) (bddnodes[n].refcou_and_level = 0) + #endif /* Stacking for garbage collector */ *************** *** 181,188 **** #define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) ) ! ! #ifdef _MSC_VER #define srand48(x) srand(x) #define lrand48(x) rand(x) #endif --- 226,234 ---- #define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) ) ! /* Compatibility with Windows */ ! #if defined(_MSC_VER) || defined(WIN32) #define srand48(x) srand(x) #define lrand48(x) rand(x) + #define alloca(x) _alloca(x) #endif Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** kernel.c 29 Sep 2004 10:00:50 -0000 1.2 --- kernel.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 217,229 **** for (n=0 ; n<bddnodesize ; n++) { ! bddnodes[n].refcou = 0; LOW(n) = -1; bddnodes[n].hash = 0; - LEVEL(n) = 0; bddnodes[n].next = n+1; } bddnodes[bddnodesize-1].next = 0; ! bddnodes[0].refcou = bddnodes[1].refcou = MAXREF; LOW(0) = HIGH(0) = 0; LOW(1) = HIGH(1) = 1; --- 217,229 ---- for (n=0 ; n<bddnodesize ; n++) { ! CLRLEVELREF(n); LOW(n) = -1; bddnodes[n].hash = 0; bddnodes[n].next = n+1; } bddnodes[bddnodesize-1].next = 0; ! SETREF(0, MAXREF); ! SETREF(1, MAXREF); LOW(0) = HIGH(0) = 0; LOW(1) = HIGH(1) = 1; *************** *** 398,409 **** } ! bddnodes[bddvarset[bddvarnum*2]].refcou = MAXREF; ! bddnodes[bddvarset[bddvarnum*2+1]].refcou = MAXREF; bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; } ! LEVEL(0) = num; ! LEVEL(1) = num; bddvar2level[num] = num; bddlevel2var[num] = num; --- 398,409 ---- } ! SETREF(bddvarset[bddvarnum*2], MAXREF); ! SETREF(bddvarset[bddvarnum*2+1], MAXREF); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; } ! SETLEVEL(0, num); ! SETLEVEL(1, num); bddvar2level[num] = num; bddlevel2var[num] = num; *************** *** 1139,1143 **** for (n=0 ; n<bddnodesize ; n++) { ! if (bddnodes[n].refcou > 0) bdd_mark(n); bddnodes[n].hash = 0; --- 1139,1143 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (REF(n) > 0) bdd_mark(n); bddnodes[n].hash = 0; *************** *** 1151,1159 **** register BddNode *node = &bddnodes[n]; ! if ((LEVELp(node) & MARKON) && LOWp(node) != -1) { register unsigned int hash; ! LEVELp(node) &= MARKOFF; hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); node->next = bddnodes[hash].hash; --- 1151,1159 ---- register BddNode *node = &bddnodes[n]; ! if (MARKEDp(node) && LOWp(node) != -1) { register unsigned int hash; ! UNMARKp(node); hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); node->next = bddnodes[hash].hash; *************** *** 1261,1268 **** node = &bddnodes[i]; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; ! LEVELp(node) |= MARKON; bdd_mark(LOWp(node)); --- 1261,1268 ---- node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == -1) return; ! SETMARKp(node); bdd_mark(LOWp(node)); *************** *** 1278,1282 **** return; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; --- 1278,1282 ---- return; ! if (MARKEDp(node) || LOWp(node) == -1) return; *************** *** 1284,1288 **** return; ! LEVELp(node) |= MARKON; bdd_mark_upto(LOWp(node), level); --- 1284,1288 ---- return; ! SETMARKp(node); bdd_mark_upto(LOWp(node), level); *************** *** 1335,1342 **** return; ! if (!(LEVELp(node) & MARKON)) return; ! LEVELp(node) &= MARKOFF; if (LEVELp(node) > level) --- 1335,1342 ---- return; ! if (!MARKEDp(node)) return; ! UNMARKp(node); if (LEVELp(node) > level) *************** *** 1428,1432 **** node = &bddnodes[res]; ! LEVELp(node) = level; LOWp(node) = low; HIGHp(node) = high; --- 1428,1432 ---- node = &bddnodes[res]; ! SETLEVELp(node, level); LOWp(node) = low; HIGHp(node) = high; *************** *** 1478,1484 **** for (n=oldsize ; n<bddnodesize ; n++) { ! bddnodes[n].refcou = 0; bddnodes[n].hash = 0; - LEVEL(n) = 0; LOW(n) = -1; bddnodes[n].next = n+1; --- 1478,1483 ---- for (n=oldsize ; n<bddnodesize ; n++) { ! CLRLEVELREF(n); bddnodes[n].hash = 0; LOW(n) = -1; bddnodes[n].next = n+1; Index: bddio.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddio.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** bddio.c 29 Sep 2004 10:00:49 -0000 1.2 --- bddio.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 133,137 **** if (LOW(n) != -1) { ! fprintf(ofile, "[%5d - %2d] ", n, bddnodes[n].refcou); if (filehandler) filehandler(ofile, bddlevel2var[LEVEL(n)]); --- 133,137 ---- if (LOW(n) != -1) { ! fprintf(ofile, "[%5d - %2d] ", n, REF(n)); if (filehandler) filehandler(ofile, bddlevel2var[LEVEL(n)]); *************** *** 185,193 **** for (n=0 ; n<bddnodesize ; n++) { ! if (LEVEL(n) & MARKON) { node = &bddnodes[n]; ! LEVELp(node) &= MARKOFF; fprintf(ofile, "[%5d] ", n); --- 185,193 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (MARKED(n)) { node = &bddnodes[n]; ! UNMARKp(node); fprintf(ofile, "[%5d] ", n); *************** *** 441,447 **** return 0; ! if (LEVELp(node) & MARKON) return 0; ! LEVELp(node) |= MARKON; if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) --- 441,447 ---- return 0; ! if (MARKEDp(node)) return 0; ! SETMARKp(node); if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** reorder.c 29 Sep 2004 10:00:50 -0000 1.2 --- reorder.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 53,62 **** /* Change macros to reflect the above idea */ #define VAR(n) (bddnodes[n].level) ! #define VARp(p) (p->level) /* Avoid these - they are misleading! */ #undef LEVEL #undef LEVELp --- 53,71 ---- /* Change macros to reflect the above idea */ + #if defined(USE_BITFIELDS) #define VAR(n) (bddnodes[n].level) ! #define VARp(p) ((p)->level) ! #define SETVARp(p,v) (VARp(p) = (v)) ! #else ! #define VAR(n) (bddnodes[n].refcou_and_level >> 10) ! #define VARp(p) ((p)->refcou_and_level >> 10) ! #define SETVARp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) ! #endif /* Avoid these - they are misleading! */ #undef LEVEL #undef LEVELp + #undef SETLEVEL + #undef SETLEVELp *************** *** 813,817 **** return; ! if (bddnodes[r].refcou == 0) { bddfreenum--; --- 822,826 ---- return; ! if (REF(r) == 0) { bddfreenum--; *************** *** 871,877 **** /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ bddnodes[n].level = bddlevel2var[bddnodes[n].level]; ! if (bddnodes[n].refcou > 0) { SETMARK(n); --- 880,890 ---- /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ + #if defined(USE_BITFIELDS) bddnodes[n].level = bddlevel2var[bddnodes[n].level]; + #else + bddnodes[n].refcou_and_level = (bddlevel2var[bddnodes[n].refcou_and_level >> 10] << 10) | REF(n); + #endif ! if (REF(n) > 0) { SETMARK(n); *************** *** 934,938 **** register BddNode *node = &bddnodes[n]; ! if (node->refcou > 0) { register unsigned int hash; --- 947,951 ---- register BddNode *node = &bddnodes[n]; ! if (REFp(node) > 0) { register unsigned int hash; *************** *** 995,999 **** register BddNode *node = &bddnodes[n]; ! if (node->refcou > 0) { register unsigned int hash; --- 1008,1012 ---- register BddNode *node = &bddnodes[n]; ! if (REFp(node) > 0) { register unsigned int hash; *************** *** 1093,1097 **** node = &bddnodes[res]; ! VARp(node) = var; LOWp(node) = low; HIGHp(node) = high; --- 1106,1110 ---- node = &bddnodes[res]; ! SETVARp(node, var); LOWp(node) = low; HIGHp(node) = high; *************** *** 1102,1106 **** /* Make sure it is reference counted */ ! node->refcou = 1; INCREF(LOWp(node)); INCREF(HIGHp(node)); --- 1115,1119 ---- /* Make sure it is reference counted */ ! SETREFp(node, 1); INCREF(LOWp(node)); INCREF(HIGHp(node)); *************** *** 1212,1216 **** /* Update in-place */ ! VARp(node) = var1; LOWp(node) = f0; HIGHp(node) = f1; --- 1225,1229 ---- /* Update in-place */ ! SETVARp(node, var1); LOWp(node) = f0; HIGHp(node) = f1; *************** *** 1250,1254 **** int next = node->next; ! if (node->refcou > 0) { node->next = bddnodes[hash].hash; --- 1263,1267 ---- int next = node->next; ! if (REFp(node) > 0) { node->next = bddnodes[hash].hash; *************** *** 1352,1356 **** int next = node->next; ! if (node->refcou > 0) { node->next = toBeProcessed; --- 1365,1369 ---- int next = node->next; ! if (REFp(node) > 0) { node->next = toBeProcessed; *************** *** 1437,1441 **** for (n=2 ; n<bddnodesize ; n++) { ! if (bddnodes[n].refcou > 0) { assert(LEVEL(n) < LEVEL(LOW(n))); --- 1450,1454 ---- for (n=2 ; n<bddnodesize ; n++) { ! if (REF(n) > 0) { assert(LEVEL(n) < LEVEL(LOW(n))); *************** *** 1689,1697 **** UNMARK(n); else ! bddnodes[n].refcou = 0; /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ bddnodes[n].level = bddvar2level[bddnodes[n].level]; } --- 1702,1714 ---- UNMARK(n); else ! SETREF(n, 0); /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ + #if defined(USE_BITFIELDS) bddnodes[n].level = bddvar2level[bddnodes[n].level]; + #else + bddnodes[n].refcou_and_level = (bddvar2level[bddnodes[n].refcou_and_level >> 10] << 10) | REF(n); + #endif } Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** bddop.c 30 Sep 2004 03:21:38 -0000 1.3 --- bddop.c 1 Oct 2004 02:17:20 -0000 1.4 *************** *** 774,777 **** --- 774,779 ---- return l; + _mm_prefetch(&bddnodes[l], 0); + entry = BddCache_lookup(&andcache, ANDHASH(l,r)); *************** *** 2712,2716 **** node = &bddnodes[r]; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; --- 2714,2718 ---- node = &bddnodes[r]; ! if (MARKEDp(node) || LOWp(node) == -1) return; *************** *** 2720,2724 **** supportMax = LEVELp(node); ! LEVELp(node) |= MARKON; support_rec(LOWp(node), support); --- 2722,2726 ---- supportMax = LEVELp(node); ! SETMARKp(node); support_rec(LOWp(node), support); *************** *** 3341,3349 **** node = &bddnodes[r]; ! if (LEVELp(node) & MARKON) return; varprofile[bddlevel2var[LEVELp(node)]]++; ! LEVELp(node) |= MARKON; varprofile_rec(LOWp(node)); --- 3343,3351 ---- node = &bddnodes[r]; ! if (MARKEDp(node)) return; varprofile[bddlevel2var[LEVELp(node)]]++; ! SETMARKp(node); varprofile_rec(LOWp(node)); |
