[Javabdd-checkins] JavaBDD/net/sf/javabdd BDDFactory.java,1.15,1.16

[CS343 s. <cs...@us...>]

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

Modified Files:
	BDDFactory.java 
Log Message:
modified save and save_rec to use node hashcode & bitset instead of node object & map, to save memory.
previous implementation kept as save_rec_original.
note: this is incompatible with the CUDD factory, which should use the original implementation instead.



Index: BDDFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v
retrieving revision 1.15
retrieving revision 1.16
diff -C2 -d -r1.15 -r1.16
*** BDDFactory.java	24 May 2005 18:24:38 -0000	1.15
--- BDDFactory.java	11 Jul 2005 22:48:52 -0000	1.16
***************
*** 12,15 ****
--- 12,16 ----
  import java.util.Map;
  import java.util.StringTokenizer;
+ import java.util.BitSet;
  import java.io.BufferedReader;
  import java.io.BufferedWriter;
***************
*** 639,649 ****
          out.write("\n");
  
!         Map visited = new HashMap();
!         save_rec(out, visited, r);
          
!         for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) {
!             BDD b = (BDD) it.next();
!             if (b != r) b.free();
!         }
      }
  
--- 640,651 ----
          out.write("\n");
  
!         //Map visited = new HashMap();
!         BitSet visited = new BitSet(getNodeTableSize());
!         save_rec(out, visited, r.id());
          
!         //for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) {
!         //    BDD b = (BDD) it.next();
!         //    if (b != r) b.free();
!         //}
      }
  
***************
*** 651,655 ****
       * Helper function for save().
       */
!     protected int save_rec(BufferedWriter out, Map visited, BDD root) throws IOException {
          if (root.isZero()) {
              root.free();
--- 653,657 ----
       * Helper function for save().
       */
!     protected int save_rec_original(BufferedWriter out, Map visited, BDD root) throws IOException {
          if (root.isZero()) {
              root.free();
***************
*** 669,676 ****
          
          BDD l = root.low();
!         int lo = save_rec(out, visited, l);
          
          BDD h = root.high();
!         int hi = save_rec(out, visited, h);
  
          out.write(v + " ");
--- 671,678 ----
          
          BDD l = root.low();
!         int lo = save_rec_original(out, visited, l);
          
          BDD h = root.high();
!         int hi = save_rec_original(out, visited, h);
  
          out.write(v + " ");
***************
*** 681,684 ****
--- 683,732 ----
          return v;
      }
+ 
+ 
+     /**
+      * Helper function for save().
+      */
+     protected int save_rec(BufferedWriter out, BitSet visited, BDD root) throws IOException {
+         if (root.isZero()) {
+             root.free();
+             return 0;
+         }
+         if (root.isOne()) {
+             root.free();
+             return 1;
+         }
+         //Integer i = (Integer) visited.get(root);
+         int i = root.hashCode();
+         //if (i != null) {
+         if (visited.get(i)) {
+             root.free();
+             //return i.intValue();
+             return i;
+         }
+         //int v = visited.size() + 2;
+         int v = i;
+         //visited.put(root, new Integer(v));
+         visited.set(i);
+         
+         BDD h = root.high();
+ 
+         BDD l = root.low();
+ 
+         int rootvar = root.var();
+         root.free();
+ 
+         int lo = save_rec(out, visited, l);
+         
+         int hi = save_rec(out, visited, h);
+ 
+         //out.write(v + " ");
+         out.write(i + " ");
+         out.write(rootvar + " ");
+         out.write(lo + " ");
+         out.write(hi + "\n");
+         
+         return v;
+     }
      
      // TODO: bdd_blockfile_hook