[Javabdd-checkins] JavaBDD/buddy/src kernel.c,1.8,1.9 bdd.h,1.4,1.5 reorder.c,1.8,1.9

[John W. <joe...@us...>]

Update of /cvsroot/javabdd/JavaBDD/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15852/buddy/src

Modified Files:
	kernel.c bdd.h reorder.c 
Log Message:
Support for dynamic resizing domains.

Index: kernel.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** kernel.c	15 Mar 2005 09:22:24 -0000	1.8
--- kernel.c	8 Apr 2005 05:28:05 -0000	1.9
***************
*** 1378,1382 ****
  int bdd_makenode(unsigned int level, int low, int high)
  {
-    register BddNode *node;
     register unsigned int hash;
     register int res;
--- 1378,1381 ----
***************
*** 1528,1532 ****
     int oldsize = bddnodesize;
     int newsize;
-    int n;
  
     if (bddnodesize >= bddmaxnodesize  &&  bddmaxnodesize > 0)
--- 1527,1530 ----
***************
*** 1661,1664 ****
--- 1659,1745 ----
  }
  
+ 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) {
+             SETHASH(hash, NEXT_r);
+         } else {
+             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);
+         SETHASH(hash, n);
+         SETNEXT(n, r);
+     }
+ }
+ 
+ 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];
+     }
+     bddvar2level[newVar] = lev+1;
+     for (i = bddvarnum-2; i > lev; --i) {
+         bddlevel2var[i+1] = bddlevel2var[i];
+     }
+     bddlevel2var[lev+1] = newVar;
+     
+     bdd_enable_reorder();
+     
+     return newVar;
+ }
  
  /* EOF */

Index: reorder.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** reorder.c	31 Jan 2005 12:04:16 -0000	1.8
--- reorder.c	8 Apr 2005 05:28:05 -0000	1.9
***************
*** 1665,1669 ****
  }
  
- 
  static int reorder_init(void)
  {
--- 1665,1668 ----

Index: bdd.h
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bdd.h,v
retrieving revision 1.4
retrieving revision 1.5
diff -C2 -d -r1.4 -r1.5
*** bdd.h	17 Nov 2004 23:05:02 -0000	1.4
--- bdd.h	8 Apr 2005 05:28:05 -0000	1.5
***************
*** 235,238 ****
--- 235,239 ----
  extern int      bdd_setmaxincrease(int);
  extern int      bdd_setminfreenodes(int);
+ extern double   bdd_setincreasefactor(double);
  extern int      bdd_getnodenum(void);
  extern int      bdd_setallocnum(int);
***************
*** 262,265 ****
--- 263,267 ----
  extern BDD      bdd_delref(BDD);
  extern void     bdd_gbc(void);
+ extern int      bdd_duplicatevar(int);
  extern int      bdd_scanset(BDD, int**, int*);
  extern BDD      bdd_makeset(int *, int);