[Javabdd-checkins] JavaBDD/buddy/src kernel.h,1.3,1.4 reorder.c,1.6,1.7
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] JavaBDD/buddy/src kernel.h,1.3,1.4 reorder.c,1.6,1.7
|
From: John W. <joe...@us...> - 2005-01-31 10:05:10
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23333/buddy/src Modified Files: kernel.h reorder.c Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** kernel.h 1 Oct 2004 02:17:20 -0000 1.3 --- kernel.h 31 Jan 2005 10:04:59 -0000 1.4 *************** *** 57,61 **** if (!bddrunning) return bdd_error(BDD_RUNNING);\ else if ((r) < 0 || (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\ ! else if (r >= 2 && LOW(r) == -1) return bdd_error(BDD_ILLBDD)\ /* Sanity check argument and return eventually the argument 'a' */ --- 57,61 ---- if (!bddrunning) return bdd_error(BDD_RUNNING);\ else if ((r) < 0 || (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\ ! else if (r >= 2 && LOW(r) == INVALID_BDD) return bdd_error(BDD_ILLBDD)\ /* Sanity check argument and return eventually the argument 'a' */ *************** *** 64,68 **** else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return (a); }\ ! else if (r >= 2 && LOW(r) == -1)\ { bdd_error(BDD_ILLBDD); return (a); } --- 64,68 ---- else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return (a); }\ ! else if (r >= 2 && LOW(r) == INVALID_BDD)\ { bdd_error(BDD_ILLBDD); return (a); } *************** *** 71,77 **** else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return; }\ ! else if (r >= 2 && LOW(r) == -1)\ { bdd_error(BDD_ILLBDD); return; } /*=== SEMI-INTERNAL TYPES ==============================================*/ --- 71,217 ---- else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return; }\ ! else if (r >= 2 && LOW(r) == INVALID_BDD)\ { bdd_error(BDD_ILLBDD); return; } + #if defined(SMALL_NODES) + + /*=== SEMI-INTERNAL TYPES ==============================================*/ + + typedef struct s_BddNode /* Node table entry */ + { + unsigned int hash_lref; + unsigned int next_href_mark; + unsigned int low_llev; + unsigned int high_hlev; + } BddNode; + + /*=== KERNEL DEFINITIONS ===============================================*/ + + #define NODE_MASK 0x07FFFFFF + #define LEV_LMASK 0xF8000000 + #define LEV_HMASK 0xF8000000 + + #define REF_LMASK 0xF8000000 + #define REF_HMASK 0xF0000000 + #define REF_LINC 0x08000000 + #define REF_HINC 0x10000000 + #define MARK_MASK 0x08000000 + #define HASH_MASK 0x07FFFFFF + #define NEXT_MASK 0x07FFFFFF + + #define NODE_BITS 27 + #define LEV_LPOS 27 + #define LEV_LBITS 5 + #define LEV_HPOS 27 + #define LEV_HBITS 5 + #define REF_LPOS 27 + #define REF_LBITS 5 + #define REF_HPOS 28 + #define REF_HBITS 4 + + #define INVALID_BDD NODE_MASK + #define MAXVAR ((1 << (LEV_LBITS + LEV_HBITS)) - 1) + #define MAX_PAIRSID MAXVAR + #define MAXREF ((1 << (REF_LBITS + REF_HBITS)) - 1) + + /* Reference counting */ + #define LREF(n) (bddnodes[n].hash_lref & REF_LMASK) + #define LREFp(n) (n->hash_lref & REF_LMASK) + #define HREF(n) (bddnodes[n].next_href_mark & REF_HMASK) + #define HREFp(n) (n->next_href_mark & REF_HMASK) + #define REF(n) ((bddnodes[n].hash_lref >> REF_LPOS) | \ + ((bddnodes[n].next_href_mark & REF_HMASK) >> (REF_HPOS-REF_LBITS))) + #define REFp(n) (((n)->hash_lref >> REF_LPOS) | \ + (((n)->next_href_mark & REF_HMASK) >> (REF_HPOS-REF_LBITS))) + + #define DECREF(n) { \ + if (LREF(n)!=REF_LMASK || HREF(n)!=REF_HMASK) { \ + if (LREF(n)==0) bddnodes[n].next_href_mark -= REF_HINC; \ + bddnodes[n].hash_lref -= REF_LINC; \ + } } + #define INCREF(n) { \ + if (LREF(n)!=REF_LMASK) bddnodes[n].hash_lref += REF_LINC; \ + else if (HREF(n)!=REF_HMASK) { \ + bddnodes[n].hash_lref += REF_LINC; \ + bddnodes[n].next_href_mark += REF_HINC; \ + } } + #define DECREFp(n) { \ + if (LREFp(n)!=REF_LMASK || HREFp(n)!=REF_HMASK) { \ + if (LREFp(n)==0) (n)->next_href_mark -= REF_HINC; \ + (n)->hash_lref -= REF_LINC; \ + } } + #define INCREFp(n) { \ + if (LREFp(n)!=REF_LMASK) (n)->hash_lref += REF_LINC; \ + else if (HREFp(n)!=REF_HMASK) { \ + (n)->hash_lref += REF_LINC; \ + (n)->next_href_mark += REF_HINC; \ + } } + #define HASREF(n) (LREF(n) != 0 || HREF(n) != 0) + + /* Marking BDD nodes */ + + #define MARKHIDE NEXT_MASK + #define SETMARK(n) (bddnodes[n].next_href_mark |= MARK_MASK) + #define UNMARK(n) (bddnodes[n].next_href_mark &= ~MARK_MASK) + #define MARKED(n) (bddnodes[n].next_href_mark & MARK_MASK) + #define SETMARKp(p) ((p)->next_href_mark |= MARK_MASK) + #define UNMARKp(p) ((p)->next_href_mark &= ~MARK_MASK) + #define MARKEDp(p) ((p)->next_href_mark & MARK_MASK) + + #define LOW(a) (bddnodes[a].low_llev & NODE_MASK) + #define HIGH(a) (bddnodes[a].high_hlev & NODE_MASK) + #define LOWp(p) ((p)->low_llev & NODE_MASK) + #define HIGHp(p) ((p)->high_hlev & NODE_MASK) + #define SETLOW(a,n) (bddnodes[a].low_llev = (n) | (bddnodes[a].low_llev & ~NODE_MASK)) + #define SETLOWp(p,n) ((p)->low_llev = (n) | ((p)->low_llev & ~NODE_MASK)) + #define SETLOWpz(p,n) ((p)->low_llev = (n)) + #define SETHIGH(a,n) (bddnodes[a].high_hlev = (n) | (bddnodes[a].high_hlev & ~NODE_MASK)) + #define SETHIGHp(p,n) ((p)->high_hlev = (n) | ((p)->high_hlev & ~NODE_MASK)) + #define HASH(a) (bddnodes[a].hash_lref & HASH_MASK) + #define HASHp(p) ((p)->hash_lref & HASH_MASK) + #define SETHASH(a,n) (bddnodes[a].hash_lref = (n) | (bddnodes[a].hash_lref & ~HASH_MASK)) + #define SETHASHp(p,n) ((p)->hash_lref = (n) | ((p)->hash_lref & ~HASH_MASK)) + #define NEXT(a) (bddnodes[a].next_href_mark & NEXT_MASK) + #define NEXTp(p) ((p)->next_href_mark & NEXT_MASK) + #define SETNEXT(a,n) (bddnodes[a].next_href_mark = (n) | (bddnodes[a].next_href_mark & ~NEXT_MASK)) + #define SETNEXTp(p,n) ((p)->next_href_mark = (n) | ((p)->next_href_mark & ~NEXT_MASK)) + #define SETNEXTpz(p,n) ((p)->next_href_mark = (n)) + #define CLRREF(n) { bddnodes[n].hash_lref &= ~REF_LMASK; bddnodes[n].next_href_mark &= ~REF_HMASK; } + #define CLRREFp(p) { (p)->hash_lref &= ~REF_LMASK; (p)->next_href_mark &= ~REF_HMASK; } + #define SETMAXREF(n) { bddnodes[n].hash_lref |= REF_LMASK; bddnodes[n].next_href_mark |= REF_HMASK; } + #define SETMAXREFp(p) { (p)->hash_lref |= REF_LMASK; (p)->next_href_mark |= REF_HMASK; } + #define LEVEL(n) ((bddnodes[n].low_llev >> LEV_LPOS) | \ + ((bddnodes[n].high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define LEVELp(p) (((p)->low_llev >> LEV_LPOS) | \ + (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define SETLEVEL(n,v) { \ + bddnodes[n].low_llev = ((v) << LEV_LPOS) | (bddnodes[n].low_llev & NODE_MASK); \ + bddnodes[n].high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | (bddnodes[n].high_hlev & NODE_MASK); \ + } + #define SETLEVELp(p,v) { \ + (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & NODE_MASK); \ + (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & NODE_MASK); \ + } + #define CLRLEVELREF(n) { \ + bddnodes[n].hash_lref &= ~REF_LMASK; \ + bddnodes[n].next_href_mark &= ~REF_HMASK; \ + bddnodes[n].low_llev &= ~LEV_LMASK; \ + bddnodes[n].high_hlev &= ~LEV_HMASK; \ + } + + #define INIT_NODE(n) { \ + bddnodes[n].hash_lref = 0; \ + bddnodes[n].next_href_mark = (n)+1; \ + bddnodes[n].low_llev = INVALID_BDD; \ + bddnodes[n].high_hlev = 0; \ + } + + #define CREATE_NODE(n, lev, lo, hi, nxt) { \ + bddnodes[n].next_href_mark = nxt; \ + bddnodes[n].low_llev = lo | ((lev) << LEV_LPOS); \ + bddnodes[n].high_hlev = hi | (((lev) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK); \ + } + + #else // SMALL_NODES /*=== SEMI-INTERNAL TYPES ==============================================*/ *************** *** 91,127 **** } BddNode; - - /*=== KERNEL VARIABLES =================================================*/ - - #ifdef CPLUSPLUS - extern "C" { - #endif - - extern int bddrunning; /* Flag - package initialized */ - extern int bdderrorcond; /* Some error condition was met */ - extern int bddnodesize; /* Number of allocated nodes */ - extern int bddmaxnodesize; /* Maximum allowed number of nodes */ - extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ - extern BddNode* bddnodes; /* All of the bdd nodes */ - extern int bddvarnum; /* Number of defined BDD variables */ - extern int* bddrefstack; /* Internal node reference stack */ - extern int* bddrefstacktop; /* Internal node reference stack top */ - extern int* bddvar2level; - extern int* bddlevel2var; - extern jmp_buf bddexception; - extern int bddreorderdisabled; - extern int bddresized; - extern bddCacheStat bddcachestats; - - #ifdef CPLUSPLUS - } - #endif - - /*=== KERNEL DEFINITIONS ===============================================*/ #define MAXVAR 0x1FFFFF #define MAXREF 0x3FF ! #define SRAND48SEED 0xbeef /* Reference counting */ --- 231,239 ---- } BddNode; /*=== KERNEL DEFINITIONS ===============================================*/ #define MAXVAR 0x1FFFFF #define MAXREF 0x3FF ! #define INVALID_BDD -1 /* Reference counting */ *************** *** 132,136 **** #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++ --- 244,248 ---- #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou++ #define HASREF(n) (REF(n) > 0) ! #else // USE_BITFIELDS #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++ *************** *** 138,142 **** #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ #define HASREF(n) (REF(n) > 0) ! #endif /* Marking BDD nodes */ --- 250,254 ---- #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ #define HASREF(n) (REF(n) > 0) ! #endif // USE_BITFIELDS /* Marking BDD nodes */ *************** *** 152,156 **** #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 */ --- 264,268 ---- #define UNMARKp(p) (LEVELp(p) &= MARKOFF1) #define MARKEDp(p) (LEVELp(p) & MARKON1) ! #else // USE_BITFIELDS #define MARKON2 0x80000000 /* Bit used to mark a node (1) */ #define MARKOFF2 0x7FFFFFFF /* - unmark */ *************** *** 162,188 **** #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif ! ! ! /* Hashfunctions */ ! ! #define PAIR(a,b) ((unsigned int)((((unsigned int)a)+((unsigned int)b))*(((unsigned int)a)+((unsigned int)b)+((unsigned int)1))/((unsigned int)2)+((unsigned int)a))) ! #define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b)))) ! - /* Inspection of BDD nodes */ - #define ISCONST(a) ((a) < 2) - #define ISNONCONST(a) ((a) >= 2) - #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) --- 274,304 ---- #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif // USE_BITFIELDS #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) + #define SETLOW(a,n) (bddnodes[a].low = (n)) + #define SETLOWp(p,n) ((p)->low = (n)) + #define SETLOWpz(p,n) ((p)->low = (n)) + #define SETHIGH(a,n) (bddnodes[a].high = (n)) + #define SETHIGHp(p,n) ((p)->high = (n)) + #define NEXT(a) (bddnodes[a].next) + #define NEXTp(p) ((p)->next) + #define SETNEXT(a,n) (bddnodes[a].next = (n)) + #define SETNEXTp(p,n) ((p)->next = (n)) + #define SETNEXTpz(p,n) ((p)->next = (n)) + #define HASH(a) (bddnodes[a].hash) + #define HASHp(p) ((p)->hash) + #define SETHASH(a,n) (bddnodes[a].hash = (n)) + #define SETHASHp(p,n) ((p)->hash = (n)) #if defined(USE_BITFIELDS) #define REF(n) (bddnodes[n].refcou) #define REFp(n) ((n)->refcou) ! #define CLRREF(n) (bddnodes[n].refcou = 0) ! #define CLRREFp(p) ((p)->refcou = 0) ! #define SETMAXREF(n) (bddnodes[n].refcou = MAXREF) ! #define SETMAXREFp(p) ((p)->refcou |= MAXREF) #define LEVEL(n) (bddnodes[n].level) #define LEVELp(p) ((p)->level) *************** *** 190,198 **** #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) --- 306,317 ---- #define SETLEVELp(p,v) (LEVELp(p) = (v)) #define CLRLEVELREF(n) (bddnodes[n].refcou = bddnodes[n].level = 0) ! #define SETLEVELREF(n,v) { bddnodes[n].refcou = 0; bddnodes[n].level = v; } ! #else // USE_BITFIELDS #define REF(n) (bddnodes[n].refcou_and_level & MAXREF) #define REFp(n) ((n)->refcou_and_level & MAXREF) ! #define CLRREF(n) (bddnodes[n].refcou_and_level &= ~MAXREF) ! #define CLRREFp(p) ((p)->refcou_and_level &= ~MAXREF) ! #define SETMAXREF(n) (bddnodes[n].refcou_and_level |= MAXREF) ! #define SETMAXREFp(p) ((p)->refcou_and_level |= MAXREF) #define LEVEL(n) (bddnodes[n].refcou_and_level >> 10) #define LEVELp(p) ((p)->refcou_and_level >> 10) *************** *** 200,204 **** #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 */ --- 319,354 ---- #define SETLEVELp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) #define CLRLEVELREF(n) (bddnodes[n].refcou_and_level = 0) ! #define SETLEVELREF(n,v) (bddnodes[n].refcou_and_level = v << 10) ! #endif // USE_BITFIELDS ! ! #define INIT_NODE(n) { \ ! CLRLEVELREF(n); \ ! SETLOW(n, INVALID_BDD); \ ! SETHASH(n, 0); \ ! SETNEXT(n, n+1); \ ! } ! ! #define CREATE_NODE(n,lev,lo,hi,nxt) { \ ! SETLEVELREF(n, lev); \ ! SETLOW(n, lo); \ ! SETHIGH(n, hi); \ ! SETNEXT(n, nxt); \ ! } ! ! #endif // SMALL_NODES ! ! /* Hashfunctions */ ! ! #define PAIR(a,b) ((unsigned int)((((unsigned int)a)+((unsigned int)b))*(((unsigned int)a)+((unsigned int)b)+((unsigned int)1))/((unsigned int)2)+((unsigned int)a))) ! #define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b)))) ! ! ! /* Inspection of BDD nodes */ ! #define ISCONST(a) ((a) < 2) ! #define ISNONCONST(a) ((a) >= 2) ! #define ISONE(a) ((a) == 1) ! #define ISZERO(a) ((a) == 0) ! ! #define SRAND48SEED 0xbeef /* Stacking for garbage collector */ *************** *** 234,237 **** --- 384,413 ---- + /*=== KERNEL VARIABLES =================================================*/ + + #ifdef CPLUSPLUS + extern "C" { + #endif + + extern int bddrunning; /* Flag - package initialized */ + extern int bdderrorcond; /* Some error condition was met */ + extern int bddnodesize; /* Number of allocated nodes */ + extern int bddmaxnodesize; /* Maximum allowed number of nodes */ + extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ + extern BddNode* bddnodes; /* All of the bdd nodes */ + extern int bddvarnum; /* Number of defined BDD variables */ + extern int* bddrefstack; /* Internal node reference stack */ + extern int* bddrefstacktop; /* Internal node reference stack top */ + extern int* bddvar2level; + extern int* bddlevel2var; + extern jmp_buf bddexception; + extern int bddreorderdisabled; + extern int bddresized; + extern bddCacheStat bddcachestats; + + #ifdef CPLUSPLUS + } + #endif + /*=== KERNEL PROTOTYPES ================================================*/ Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** reorder.c 29 Jan 2005 11:33:58 -0000 1.6 --- reorder.c 31 Jan 2005 10:04:59 -0000 1.7 *************** *** 53,56 **** --- 53,66 ---- /* Change macros to reflect the above idea */ + #if defined(SMALL_NODES) + #define VAR(n) ((bddnodes[n].low_llev >> LEV_LPOS) | \ + ((bddnodes[n].high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define VARp(p) (((p)->low_llev >> LEV_LPOS) | \ + (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define SETVARp(p,v) { \ + (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & ~NODE_MASK); \ + (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & ~NODE_MASK); \ + } + #else #if defined(USE_BITFIELDS) #define VAR(n) (bddnodes[n].level) *************** *** 62,65 **** --- 72,76 ---- #define SETVARp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) #endif + #endif /* Avoid these - they are misleading! */ *************** *** 880,888 **** /* 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) --- 891,896 ---- /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ ! int v = bddlevel2var[VAR(n)]; ! SETVARp(&bddnodes[n], v); if (REF(n) > 0) *************** *** 919,927 **** /* Make sure the hash field is empty. This saves a loop in the initial GBC */ ! node->hash = 0; } ! bddnodes[0].hash = 0; ! bddnodes[1].hash = 0; free(dep); --- 927,935 ---- /* Make sure the hash field is empty. This saves a loop in the initial GBC */ ! SETHASHp(node, 0); } ! SETHASH(0, 0); ! SETHASH(1, 0); free(dep); *************** *** 952,963 **** hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = n; bddfreenum++; --- 960,971 ---- hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = n; bddfreenum++; *************** *** 1002,1006 **** for (n=bddnodesize-1 ; n>=0 ; n--) ! bddnodes[n].hash = 0; for (n=bddnodesize-1 ; n>=2 ; n--) --- 1010,1014 ---- for (n=bddnodesize-1 ; n>=0 ; n--) ! SETHASH(n, 0); for (n=bddnodesize-1 ; n>=2 ; n--) *************** *** 1013,1022 **** hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! node->next = bddfreepos; bddfreepos = n; } --- 1021,1030 ---- hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETNEXTp(node, bddfreepos); bddfreepos = n; } *************** *** 1052,1056 **** /* Try to find an existing node of this kind */ hash = NODEHASH(var, low, high); ! res = bddnodes[hash].hash; while(res != 0) --- 1060,1064 ---- /* Try to find an existing node of this kind */ hash = NODEHASH(var, low, high); ! res = HASH(hash); while(res != 0) *************** *** 1064,1068 **** return res; } ! res = bddnodes[res].next; #ifdef CACHESTATS --- 1072,1076 ---- return res; } ! res = NEXT(res); #ifdef CACHESTATS *************** *** 1100,1104 **** /* Build new node */ res = bddfreepos; ! bddfreepos = bddnodes[bddfreepos].next; levels[var].nodenum++; bddproduced++; --- 1108,1112 ---- /* Build new node */ res = bddfreepos; ! bddfreepos = NEXT(bddfreepos); levels[var].nodenum++; bddproduced++; *************** *** 1107,1119 **** node = &bddnodes[res]; SETVARp(node, var); ! LOWp(node) = low; ! HIGHp(node) = high; /* Insert node in hash chain */ ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = res; /* Make sure it is reference counted */ ! SETREFp(node, 1); INCREF(LOWp(node)); INCREF(HIGHp(node)); --- 1115,1128 ---- node = &bddnodes[res]; SETVARp(node, var); ! SETLOWp(node, low); ! SETHIGHp(node, high); /* Insert node in hash chain */ ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, res); /* Make sure it is reference counted */ ! CLRREFp(node); // <-- is this necessary? ! INCREFp(node); INCREF(LOWp(node)); INCREF(HIGHp(node)); *************** *** 1142,1158 **** int r; ! r = bddnodes[n + vl0].hash; ! bddnodes[n + vl0].hash = 0; while (r != 0) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) { /* Node does not depend on next var, let it stay in the chain */ ! node->next = bddnodes[n+vl0].hash; ! bddnodes[n+vl0].hash = r; levels[var0].nodenum++; } --- 1151,1167 ---- int r; ! r = HASH(n + vl0); ! SETHASH(n + vl0, 0); while (r != 0) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) { /* Node does not depend on next var, let it stay in the chain */ ! SETNEXTp(node, HASH(n+vl0)); ! SETHASH(n+vl0, r); levels[var0].nodenum++; } *************** *** 1160,1164 **** { /* Node depends on next var - save it for later procesing */ ! node->next = toBeProcessed; toBeProcessed = r; #ifdef SWAPCOUNT --- 1169,1173 ---- { /* Node depends on next var - save it for later procesing */ ! SETNEXTp(node, toBeProcessed); toBeProcessed = r; #ifdef SWAPCOUNT *************** *** 1188,1192 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int f0 = LOWp(node); int f1 = HIGHp(node); --- 1197,1201 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int f0 = LOWp(node); int f1 = HIGHp(node); *************** *** 1226,1231 **** /* Update in-place */ SETVARp(node, var1); ! LOWp(node) = f0; ! HIGHp(node) = f1; levels[var1].nodenum++; --- 1235,1240 ---- /* Update in-place */ SETVARp(node, var1); ! SETLOWp(node, f0); ! SETHIGHp(node, f1); levels[var1].nodenum++; *************** *** 1233,1238 **** /* Rehash the node since it got new childs */ hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = toBeProcessed; toBeProcessed = next; --- 1242,1247 ---- /* Rehash the node since it got new childs */ hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, toBeProcessed); toBeProcessed = next; *************** *** 1255,1270 **** { int hash = n+vl1; ! int r = bddnodes[hash].hash; ! bddnodes[hash].hash = 0; while (r) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (REFp(node) > 0) { ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = r; } else --- 1264,1279 ---- { int hash = n+vl1; ! int r = HASH(hash); ! SETHASH(hash, 0); while (r) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (REFp(node) > 0) { ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, r); } else *************** *** 1273,1278 **** DECREF(HIGHp(node)); ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = r; levels[var1].nodenum--; --- 1282,1287 ---- DECREF(HIGHp(node)); ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = r; levels[var1].nodenum--; *************** *** 1297,1301 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int f0 = LOWp(node); int f1 = HIGHp(node); --- 1306,1310 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int f0 = LOWp(node); int f1 = HIGHp(node); *************** *** 1334,1340 **** /* Update in-place */ ! VARp(node) = var1; ! LOWp(node) = f0; ! HIGHp(node) = f1; levels[var1].nodenum++; --- 1343,1349 ---- /* Update in-place */ ! SETVARp(node, var1); ! SETLOWp(node, f0); ! SETHIGHp(node, f1); levels[var1].nodenum++; *************** *** 1357,1371 **** { int hash = n+vl1; ! int r = bddnodes[hash].hash; ! bddnodes[hash].hash = 0; while (r) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (REFp(node) > 0) { ! node->next = toBeProcessed; toBeProcessed = r; } --- 1366,1380 ---- { int hash = n+vl1; ! int r = HASH(hash); ! SETHASH(hash, 0); while (r) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (REFp(node) > 0) { ! SETNEXTp(node, toBeProcessed); toBeProcessed = r; } *************** *** 1375,1380 **** DECREF(HIGHp(node)); ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = r; levels[var1].nodenum--; --- 1384,1389 ---- DECREF(HIGHp(node)); ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = r; levels[var1].nodenum--; *************** *** 1399,1407 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = toBeProcessed; toBeProcessed = next; --- 1408,1416 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, toBeProcessed); toBeProcessed = next; *************** *** 1439,1443 **** { assert(VAR(r) == v); ! r = bddnodes[r].next; cou++; vcou++; --- 1448,1452 ---- { assert(VAR(r) == v); ! r = NEXT(r); cou++; vcou++; *************** *** 1700,1725 **** 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 } - #if 0 - for (n=0 ; n<bddvarnum ; n++) - printf("%3d\n", bddlevel2var[n]); - printf("\n"); - #endif - - #if 0 - for (n=0 ; n<bddvarnum ; n++) - printf("%3d: %4d nodes , %4d entries\n", n, levels[n].nodenum, - levels[n].size); - #endif free(extroots); free(levels); --- 1709,1719 ---- UNMARK(n); else ! CLRREF(n); /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ ! { int v = bddvar2level[VAR(n)]; SETVARp(&bddnodes[n], v); } } free(extroots); free(levels); |
