[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.19,1.20 BDDDomain.java,1.6,1.7 MicroFactor

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20956/net/sf/javabdd

Modified Files:
	JFactory.java BDDDomain.java MicroFactory.java BDDFactory.java 
Log Message:
Updates to duplicateVar.  Seems to actually work now.

Index: BDDFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** BDDFactory.java	14 Apr 2005 23:58:41 -0000	1.8
--- BDDFactory.java	17 Apr 2005 10:21:47 -0000	1.9
***************
*** 268,271 ****
--- 268,274 ----
          int nodes = getNodeTableSize();
          int cache = getCacheSize();
+         domain = null;
+         fdvarnum = 0;
+         firstbddvar = 0;
          done();
          initialize(nodes, cache);

Index: BDDDomain.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v
retrieving revision 1.6
retrieving revision 1.7
diff -C2 -d -r1.6 -r1.7
*** BDDDomain.java	14 Apr 2005 23:58:41 -0000	1.6
--- BDDDomain.java	17 Apr 2005 10:21:46 -0000	1.7
***************
*** 320,328 ****
--- 320,331 ----
          BDDFactory factory = getFactory();
          for (int i = ivar.length; i < new_ivar.length; ++i) {
+             //System.out.println("Domain "+this+" Duplicating var#"+new_ivar[i-1]);
              int newVar = factory.duplicateVar(new_ivar[i-1]);
              factory.firstbddvar++;
              new_ivar[i] = newVar;
+             //System.out.println("Domain "+this+" var#"+i+" = "+newVar);
          }
          this.ivar = new_ivar;
+         //System.out.println("Domain "+this+" old var = "+var);
          this.var.free();
          BDD nvar = factory.one();
***************
*** 331,334 ****
--- 334,338 ----
          }
          this.var = nvar;
+         //System.out.println("Domain "+this+" new var = "+var);
          return binsize;
      }

Index: JFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v
retrieving revision 1.19
retrieving revision 1.20
diff -C2 -d -r1.19 -r1.20
*** JFactory.java	14 Apr 2005 23:58:41 -0000	1.19
--- JFactory.java	17 Apr 2005 10:21:46 -0000	1.20
***************
*** 4470,4473 ****
--- 4470,4475 ----
          bddrefstack = null;
          bddvarset = null;
+         bddvar2level = null;
+         bddlevel2var = null;
  
          bdd_operator_done();
***************
*** 4610,4614 ****
          bdd_setvarnum(bddvarnum+1);
          // Actually duplicate the var in all BDDs.
!         insert_level(lev, true, 0);
          // Fix up bddvar2level
          for (int i = 0; i < bddvarnum; ++i) {
--- 4612,4617 ----
          bdd_setvarnum(bddvarnum+1);
          // Actually duplicate the var in all BDDs.
!         insert_level(lev);
!         dup_level(lev, 0);
          // Fix up bddvar2level
          for (int i = 0; i < bddvarnum; ++i) {
***************
*** 4629,4633 ****
  
              SETMAXREF(bddvarset[bdv * 2]);
!             SETMAXREF(bddvarset[bdv * 2] + 1);
          }
          // Fix up pairs
--- 4632,4636 ----
  
              SETMAXREF(bddvarset[bdv * 2]);
!             SETMAXREF(bddvarset[bdv * 2 + 1]);
          }
          // Fix up pairs
***************
*** 4707,4711 ****
  
              SETMAXREF(bddvarset[bddvarnum * 2]);
!             SETMAXREF(bddvarset[bddvarnum * 2] + 1);
              bddlevel2var[bddvarnum] = bddvarnum;
              bddvar2level[bddvarnum] = bddvarnum;
--- 4710,4714 ----
  
              SETMAXREF(bddvarset[bddvarnum * 2]);
!             SETMAXREF(bddvarset[bddvarnum * 2 + 1]);
              bddlevel2var[bddvarnum] = bddvarnum;
              bddvar2level[bddvarnum] = bddvarnum;
***************
*** 5465,5496 ****
      }
  
!     void insert_level(int levToInsert, boolean dupLevel, int val) {
          for (int n = 2; n < bddnodesize; n++) {
              if (LOW(n) == INVALID_BDD) continue;
              int lev = LEVEL(n);
!             if (lev < levToInsert || lev == bddvarnum-1) {
                  // Stays the same.
                  continue;
              }
              int lo, hi, newLev;
!             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.
--- 5468,5538 ----
      }
  
!     void insert_level(int levToInsert) {
          for (int n = 2; n < bddnodesize; n++) {
              if (LOW(n) == INVALID_BDD) continue;
              int lev = LEVEL(n);
!             if (lev <= levToInsert || lev == bddvarnum-1) {
                  // Stays the same.
                  continue;
              }
              int lo, hi, newLev;
!             lo = LOW(n);
!             hi = HIGH(n);
!             // Need to increase level by one.
!             newLev = lev+1;
!             
!             // Find this node in its hash chain.
!             int hash = NODEHASH(lev, lo, hi);
!             int r = HASH(hash), r2 = 0;
!             while (r != n && r != 0) {
!                 r2 = r;
!                 r = NEXT(r);
!             }
!             if (r == 0) {
!                 // Cannot find node in the hash chain ?!
!                 throw new InternalError();
!             }
!             // Remove from this hash chain.
!             int 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);
!         }
!     }
! 
!     void dup_level(int levToInsert, int val) {
!         for (int n = 2; n < bddnodesize; n++) {
!             if (LOW(n) == INVALID_BDD) continue;
!             int lev = LEVEL(n);
!             if (lev != levToInsert || lev == bddvarnum-1) {
!                 // Stays the same.
!                 continue;
              }
+             int lo, hi, newLev;
+             lo = LOW(n);
+             hi = HIGH(n);
+             // Duplicate this node.
+             _assert(LEVEL(lo) > levToInsert + 1);
+             _assert(LEVEL(hi) > levToInsert + 1);
+             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 ? lo : 0, val<=0 ? 0 : lo);
+             n_high = bdd_makenode(levToInsert+1, val==0 ? hi : 0, val==0 ? 0 : hi);
+             bdd_delref(n);
+             //System.out.println("Lev = "+lev+" old low = "+lo+" old high = "+hi+" new low = "+n_low+" ("+new bdd(n_low)+") new high = "+n_high+" ("+new bdd(n_high)+")");
+             newLev = lev;
+             SETLOW(n, n_low);
+             SETHIGH(n, n_high);
              
              // Find this node in its hash chain.
***************
*** 5522,5526 ****
          }
      }
!     
      int mark_roots() {
          boolean[] dep = new boolean[bddvarnum];
--- 5564,5568 ----
          }
      }
! 
      int mark_roots() {
          boolean[] dep = new boolean[bddvarnum];
***************
*** 6016,6019 ****
--- 6058,6062 ----
          bdd_unmark(r);
  
+         out.flush();
          return;
      }

Index: MicroFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** MicroFactory.java	8 Apr 2005 05:27:52 -0000	1.8
--- MicroFactory.java	17 Apr 2005 10:21:46 -0000	1.9
***************
*** 4955,4969 ****
          int newVar = bddvarnum;
          int lev = bddvar2level[var];
          bdd_setvarnum(bddvarnum+1);
!         insert_level(lev, true, 0);
!         for (int i = 0; i < bddvar2level.length; ++i) {
              if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum)
                  ++bddvar2level[i];
          }
          bddvar2level[newVar] = lev+1;
          for (int i = bddvarnum-2; i > lev; --i) {
              bddlevel2var[i+1] = bddlevel2var[i];
          }
          bddlevel2var[lev+1] = newVar;
          
          bdd_enable_reorder();
--- 4955,4995 ----
          int newVar = bddvarnum;
          int lev = bddvar2level[var];
+         // Increase the size of the various data structures.
          bdd_setvarnum(bddvarnum+1);
!         // Actually duplicate the var in all BDDs.
!         insert_level(lev);
!         dup_level(lev, 0);
!         // Fix up bddvar2level
!         for (int i = 0; i < bddvarnum; ++i) {
              if (bddvar2level[i] > lev && bddvar2level[i] < bddvarnum)
                  ++bddvar2level[i];
          }
          bddvar2level[newVar] = lev+1;
+         // Fix up bddlevel2var
          for (int i = bddvarnum-2; i > lev; --i) {
              bddlevel2var[i+1] = bddlevel2var[i];
          }
          bddlevel2var[lev+1] = newVar;
+         // Fix up bddvarset
+         for (int 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]);
+         }
+         // Fix up pairs
+         for (bddPair pair = pairs; pair != null; pair = pair.next) {
+             bdd_delref(pair.result[bddvarnum-1]);
+             for (int 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);
+             //System.out.println("Pair "+pair);
+         }
          
          bdd_enable_reorder();
***************
*** 5028,5032 ****
  
              SETMAXREF(bddvarset[bddvarnum * 2]);
!             SETMAXREF(bddvarset[bddvarnum * 2] + 1);
              bddlevel2var[bddvarnum] = bddvarnum;
              bddvar2level[bddvarnum] = bddvarnum;
--- 5054,5058 ----
  
              SETMAXREF(bddvarset[bddvarnum * 2]);
!             SETMAXREF(bddvarset[bddvarnum * 2 + 1]);
              bddlevel2var[bddvarnum] = bddvarnum;
              bddvar2level[bddvarnum] = bddvarnum;
***************
*** 5779,5810 ****
      }
  
!     void insert_level(int levToInsert, boolean dupLevel, int val) {
          for (int n = 2; n < bddnodesize; n++) {
              if (LOW(n) == INVALID_BDD) continue;
              int lev = LEVEL(n);
!             if (lev < levToInsert || lev == bddvarnum-1) {
                  // Stays the same.
                  continue;
              }
              int lo, hi, newLev;
!             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.
--- 5805,5874 ----
      }
  
!     void insert_level(int levToInsert) {
          for (int n = 2; n < bddnodesize; n++) {
              if (LOW(n) == INVALID_BDD) continue;
              int lev = LEVEL(n);
!             if (lev <= levToInsert || lev == bddvarnum-1) {
                  // Stays the same.
                  continue;
              }
              int lo, hi, newLev;
!             lo = LOW(n);
!             hi = HIGH(n);
!             // Need to increase level by one.
!             newLev = lev+1;
!             
!             // Find this node in its hash chain.
!             int hash = NODEHASH(lev, lo, hi);
!             int r = HASH(hash), r2 = 0;
!             while (r != n && r != 0) {
!                 r2 = r;
!                 r = NEXT(r);
!             }
!             if (r == 0) {
!                 // Cannot find node in the hash chain ?!
!                 throw new InternalError();
!             }
!             // Remove from this hash chain.
!             int 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);
!         }
!     }
! 
!     void dup_level(int levToInsert, int val) {
!         for (int n = 2; n < bddnodesize; n++) {
!             if (LOW(n) == INVALID_BDD) continue;
!             int lev = LEVEL(n);
!             if (lev != levToInsert || lev == bddvarnum-1) {
!                 // Stays the same.
!                 continue;
              }
+             int lo, hi, newLev;
+             lo = LOW(n);
+             hi = HIGH(n);
+             // Duplicate this node.
+             _assert(LEVEL(lo) > levToInsert + 1);
+             _assert(LEVEL(hi) > levToInsert + 1);
+             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 ? 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);
              
              // Find this node in its hash chain.

[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.19,1.20 BDDDomain.java,1.6,1.7 MicroFactor

[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.19,1.20 BDDDomain.java,1.6,1.7 MicroFactory.java,1.8,1.9 BDDFactory.java,1.8,1.9