[Javabdd-checkins] JavaBDD/buddy/src kernel.h,1.4,1.5 kernel.c,1.9,1.10 pairs.c,1.3,1.4
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] JavaBDD/buddy/src kernel.h,1.4,1.5 kernel.c,1.9,1.10 pairs.c,1.3,1.4
|
From: John W. <joe...@us...> - 2005-04-17 10:21:45
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20708/buddy/src Modified Files: kernel.h kernel.c pairs.c Log Message: Updates to duplicateVar. Seems to actually work now. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** kernel.h 31 Jan 2005 10:04:59 -0000 1.4 --- kernel.h 17 Apr 2005 10:21:27 -0000 1.5 *************** *** 450,453 **** --- 450,455 ---- extern void bdd_cpp_init(void); + extern void fixup_pairs(int,int); + #ifdef CPLUSPLUS } Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** kernel.c 8 Apr 2005 05:28:05 -0000 1.9 --- kernel.c 17 Apr 2005 10:21:27 -0000 1.10 *************** *** 1659,1701 **** } ! static void insert_level(int levToInsert, int dupLevel, int val) ! { ! int n, lev; for (n = 2; n < bddnodesize; n++) { ! int lo, hi, newLev, hash, r, r2, NEXT_r; if (LOW(n) == INVALID_BDD) continue; lev = LEVEL(n); ! if (lev < levToInsert || lev == bddvarnum-1) { ! // Stays the same. continue; } ! if (dupLevel && lev == levToInsert) { ! // Duplicate this node. ! int n_low, n_high; ! bdd_addref(n); ! // 0 = var is zero, 1 = var is one, -1 = var equals other ! n_low = bdd_makenode(levToInsert+1, val<=0 ? LOW(n) : 0, val<=0 ? 0 : LOW(n)); ! n_high = bdd_makenode(levToInsert+1, val==0 ? HIGH(n) : 0, val==0 ? 0 : HIGH(n)); ! bdd_delref(n); ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); } else { ! // Need to increase level by one. ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; } ! ! // Find this node in its hash chain. hash = NODEHASH(lev, lo, hi); ! r = HASH(hash), r2 = 0; ! while (r != n) { r2 = r; r = NEXT(r); } - // Remove from this hash chain. NEXT_r = NEXT(r); if (r2 == 0) { --- 1659,1723 ---- } ! static void insert_level(int levToInsert) { ! int n; for (n = 2; n < bddnodesize; n++) { ! int lev, lo, hi, newLev, hash, r, r2, NEXT_r; if (LOW(n) == INVALID_BDD) continue; lev = LEVEL(n); ! if (lev <= levToInsert || lev == bddvarnum-1) { continue; } ! lo = LOW(n); ! hi = HIGH(n); ! newLev = lev+1; ! hash = NODEHASH(lev, lo, hi); ! r = HASH(hash); ! r2 = 0; ! while (r != n && r != 0) { ! r2 = r; ! r = NEXT(r); ! } ! NEXT_r = NEXT(r); ! if (r2 == 0) { ! SETHASH(hash, NEXT_r); } else { ! SETNEXT(r2, NEXT_r); } ! SETLEVEL(n, newLev); ! lo = LOW(n); hi = HIGH(n); ! hash = NODEHASH(newLev, lo, hi); ! r = HASH(hash); ! SETHASH(hash, n); ! SETNEXT(n, r); ! } ! } ! ! static void dup_level(int levToInsert, int val) { ! int n; ! for (n = 2; n < bddnodesize; n++) { ! int lev, lo, hi, newLev; ! int n_low, n_high; ! int hash, r, r2, NEXT_r; ! if (LOW(n) == INVALID_BDD) continue; ! lev = LEVEL(n); ! if (lev != levToInsert || lev == bddvarnum-1) { ! continue; ! } ! lo = LOW(n); ! hi = HIGH(n); ! bdd_addref(n); ! n_low = bdd_makenode(levToInsert+1, val<=0 ? lo : 0, val<=0 ? 0 : lo); ! n_high = bdd_makenode(levToInsert+1, val==0 ? hi : 0, val==0 ? 0 : hi); ! bdd_delref(n); ! newLev = lev; ! SETLOW(n, n_low); ! SETHIGH(n, n_high); hash = NODEHASH(lev, lo, hi); ! r = HASH(hash); ! r2 = 0; ! while (r != n && r != 0) { r2 = r; r = NEXT(r); } NEXT_r = NEXT(r); if (r2 == 0) { *************** *** 1704,1711 **** SETNEXT(r2, NEXT_r); } - // Set level of this node. SETLEVEL(n, newLev); lo = LOW(n); hi = HIGH(n); - // Add to new hash chain. hash = NODEHASH(newLev, lo, hi); r = HASH(hash); --- 1726,1731 ---- *************** *** 1716,1732 **** int bdd_duplicatevar(int var) { ! int newVar, lev, i; if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); return bddfalse; } - bdd_disable_reorder(); - newVar = bddvarnum; lev = bddvar2level[var]; bdd_setvarnum(bddvarnum+1); ! insert_level(lev, 1, 0); ! for (i = 0; i <= bddvarnum; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; --- 1736,1751 ---- int bdd_duplicatevar(int var) { ! int newVar, lev, i, bdv; if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); return bddfalse; } bdd_disable_reorder(); newVar = bddvarnum; lev = bddvar2level[var]; bdd_setvarnum(bddvarnum+1); ! insert_level(lev); ! dup_level(lev, 0); ! for (i = 0; i < bddvarnum; ++i) { if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum) ++bddvar2level[i]; *************** *** 1737,1743 **** } bddlevel2var[lev+1] = newVar; ! bdd_enable_reorder(); - return newVar; } --- 1756,1768 ---- } bddlevel2var[lev+1] = newVar; ! for (bdv = 0; bdv < bddvarnum; bdv++) { ! bddvarset[bdv * 2] = PUSHREF(bdd_makenode(bddvar2level[bdv], 0, 1)); ! bddvarset[bdv * 2 + 1] = bdd_makenode(bddvar2level[bdv], 1, 0); ! POPREF(1); ! SETMAXREF(bddvarset[bdv * 2]); ! SETMAXREF(bddvarset[bdv * 2 + 1]); ! } ! fixup_pairs(lev, newVar); bdd_enable_reorder(); return newVar; } Index: pairs.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/pairs.c,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** pairs.c 30 Jan 2005 14:43:02 -0000 1.3 --- pairs.c 17 Apr 2005 10:21:27 -0000 1.4 *************** *** 360,363 **** --- 360,379 ---- } + void fixup_pairs(int lev, int newVar) + { + bddPair* pair; + for (pair = pairs; pair != NULL; pair = pair->next) { + int i; + bdd_delref(pair->result[bddvarnum-1]); + for (i = bddvarnum-1; i > lev+1; --i) { + pair->result[i] = pair->result[i-1]; + if (i != LEVEL(pair->result[i]) && i > pair->last) { + pair->last = i; + } + } + pair->result[lev+1] = bdd_ithvar(newVar); + } + } + /* EOF */ |
