[Javabdd-checkins] JavaBDD/net/sf/javabdd MicroFactory.java,1.1,1.2

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-serv620/net/sf/javabdd

Modified Files:
	MicroFactory.java 
Log Message:
Bug fixes to make it actually work.

Index: MicroFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -C2 -d -r1.1 -r1.2
*** MicroFactory.java	30 Jan 2005 14:42:22 -0000	1.1
--- MicroFactory.java	31 Jan 2005 00:07:11 -0000	1.2
***************
*** 37,41 ****
      static final boolean USE_FINALIZER = false;
      static final boolean CACHESTATS = false;
!     public static boolean FLUSH_CACHE_ON_GC = false;

      private MicroFactory() { }
--- 37,41 ----
      static final boolean USE_FINALIZER = false;
      static final boolean CACHESTATS = false;
!     public static boolean FLUSH_CACHE_ON_GC = true;

      private MicroFactory() { }
***************
*** 61,65 ****
      static final int offset__llev = 2;
      static final int offset__hlev = 3;
!     static final int offset__mark = 0;

      static final int NODE_MASK  = 0x07FFFFFF;
--- 61,65 ----
      static final int offset__llev = 2;
      static final int offset__hlev = 3;
!     static final int offset__mark = 1;

      static final int NODE_MASK  = 0x07FFFFFF;
***************
*** 122,129 ****
              if (a == 0) {
                  if (b == 0) return;
!                 table[node*__node_size + offset__high] -= REF_HINC;
              } else if (b == REF_HMASK) return;
          }
!         table[node*__node_size + offset__low] -= REF_LINC;
      }

--- 122,129 ----
              if (a == 0) {
                  if (b == 0) return;
!                 table[node*__node_size + offset__href] -= REF_HINC;
              } else if (b == REF_HMASK) return;
          }
!         table[node*__node_size + offset__lref] -= REF_LINC;
      }

***************
*** 137,141 ****
          int a = table[node*__node_size + offset__llev] & LEV_LMASK;
          int b = table[node*__node_size + offset__hlev] & LEV_HMASK;
!         return a >>> LEV_LPOS | b >>> (LEV_HPOS-LEV_LBITS);
      }

--- 137,142 ----
          int a = table[node*__node_size + offset__llev] & LEV_LMASK;
          int b = table[node*__node_size + offset__hlev] & LEV_HMASK;
!         int lev = a >>> LEV_LPOS | b >>> (LEV_HPOS-LEV_LBITS);
!         return lev;
      }

***************
*** 207,211 ****

      private final void INIT_NODE(int r, int lev, int lo, int hi, int next) {
!         table[r*__node_size + offset__hash] = 0;
          table[r*__node_size + offset__next] = next;
          table[r*__node_size + offset__low] = lo | (lev << LEV_LPOS);
--- 208,212 ----

      private final void INIT_NODE(int r, int lev, int lo, int hi, int next) {
!         //table[r*__node_size + offset__hash] = 0;
          table[r*__node_size + offset__next] = next;
          table[r*__node_size + offset__low] = lo | (lev << LEV_LPOS);
***************
*** 644,648 ****
          final OpCache1 copy() {
              OpCache1 that = new OpCache1(this.table.length);
!             System.arraycopy(this.table, 0, that.table, 0, this.table.length);
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
--- 645,652 ----
          final OpCache1 copy() {
              OpCache1 that = new OpCache1(this.table.length);
!             for (int i = 0; i < this.table.length; ++i) {
!                 that.table[i].a = this.table[i].a;
!                 that.table[i].res = this.table[i].res;
!             }
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
***************
*** 683,687 ****
          final OpCache2 copy() {
              OpCache2 that = new OpCache2(this.table.length);
!             System.arraycopy(this.table, 0, that.table, 0, this.table.length);
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
--- 687,695 ----
          final OpCache2 copy() {
              OpCache2 that = new OpCache2(this.table.length);
!             for (int i = 0; i < this.table.length; ++i) {
!                 that.table[i].a = this.table[i].a;
!                 that.table[i].b = this.table[i].b;
!                 that.table[i].res = this.table[i].res;
!             }
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
***************
*** 723,727 ****
          final OpCache3 copy() {
              OpCache3 that = new OpCache3(this.table.length);
!             System.arraycopy(this.table, 0, that.table, 0, this.table.length);
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
--- 731,780 ----
          final OpCache3 copy() {
              OpCache3 that = new OpCache3(this.table.length);
!             for (int i = 0; i < this.table.length; ++i) {
!                 that.table[i].a = this.table[i].a;
!                 that.table[i].b = this.table[i].b;
!                 that.table[i].c = this.table[i].c;
!                 that.table[i].res = this.table[i].res;
!             }
!             that.cacheHit = this.cacheHit;
!             that.cacheMiss = this.cacheMiss;
!             return that;
!         }
!     }
!     
!     private class OpCacheD {
!         OpCacheDEntry table[];
!         int cacheHit;
!         int cacheMiss;
!         OpCacheD(int size) { alloc(size); }
!         final void alloc(int size) {
!             table = new OpCacheDEntry[size];
!             for (int i = 0; i < table.length; ++i) {
!                 table[i] = new OpCacheDEntry();
!             }
!         }
!         final OpCacheDEntry lookup(int hash) {
!             return (OpCacheDEntry) table[Math.abs(hash % table.length)];
!         }
!         final void reset() {
!             for (int i = 0; i < table.length; ++i) {
!                 table[i].a = -1;
!             }
!         }
!         final void clean() {
!             for (int i = 0; i < table.length; ++i) {
!                 int a = table[i].a;
!                 if (a == -1) continue;
!                 if (LOW(a & NODE_MASK) == INVALID_BDD) {
!                     table[i].a = -1;
!                 }
!             }
!         }
!         final OpCacheD copy() {
!             OpCacheD that = new OpCacheD(this.table.length);
!             for (int i = 0; i < this.table.length; ++i) {
!                 that.table[i].a = this.table[i].a;
!                 that.table[i].res = this.table[i].res;
!             }
              that.cacheHit = this.cacheHit;
              that.cacheMiss = this.cacheMiss;
***************
*** 841,844 ****
--- 894,921 ----

      }
+ 
+     private static class OpCacheDEntry {
+         int a;
+         double res;
+         
+         final double get_sid(int node, int id) {
+             if (VERIFY_ASSERTIONS) {
+                 _assert(node == (node & NODE_MASK));
+                 _assert(id == (id & ~NODE_MASK));
+             }
+             int k = node | id;
+             if (a != k) return -1;
+             return res;
+         }
+         
+         final void set_sid(int node, int id, double r) {
+             if (VERIFY_ASSERTIONS) {
+                 _assert(node == (node & NODE_MASK));
+                 _assert(id == (id & ~NODE_MASK));
+             }
+             a = node | id;
+             res = r;
+         }
+     }

      private static class JavaBDDException extends BDDException {
***************
*** 859,863 ****
      int bddmaxnodesize; /* Maximum allowed number of nodes */
      int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */
-     int[] bddnodes; /* All of the bdd nodes */
      int bddfreepos; /* First free node */
      int bddfreenum; /* Number of free nodes */
--- 936,939 ----
***************
*** 2802,2824 ****
          CHECK(r);

!         miscid = CACHEID_PATHCOU;

!         if (countcache == null) countcache = new OpCache2(cachesize);

          return bdd_pathcount_rec(r);
      }

!     float bdd_pathcount_rec(int r) {
!         OpCache2Entry entry;
!         float size;

          if (ISZERO(r)) return 0f;
          if (ISONE(r)) return 1f;

-         int res;
          entry = countcache.lookup(PATHCOUHASH(r));
!         if ((res = entry.get(r, miscid)) != -1) {
              if (CACHESTATS) countcache.cacheHit++;
!             return Float.intBitsToFloat(res);
          }
          if (CACHESTATS) countcache.cacheMiss++;
--- 2878,2899 ----
          CHECK(r);

!         miscid = CACHEID_PATHCOU << NODE_BITS;

!         if (countcache == null) countcache = new OpCacheD(cachesize);

          return bdd_pathcount_rec(r);
      }

!     double bdd_pathcount_rec(int r) {
!         OpCacheDEntry entry;
!         double size;

          if (ISZERO(r)) return 0f;
          if (ISONE(r)) return 1f;

          entry = countcache.lookup(PATHCOUHASH(r));
!         if ((size = entry.get_sid(r, miscid)) >= 0) {
              if (CACHESTATS) countcache.cacheHit++;
!             return size;
          }
          if (CACHESTATS) countcache.cacheMiss++;
***************
*** 2826,2830 ****
          size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));

!         entry.set(r, miscid, Float.floatToIntBits(size));

          return size;
--- 2901,2905 ----
          size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));

!         entry.set_sid(r, miscid, size);

          return size;
***************
*** 2892,2898 ****
          CHECK(r);

!         if (countcache == null) countcache = new OpCache2(cachesize);

!         miscid = CACHEID_SATCOU;
          size = Math.pow(2.0, (double) LEVEL(r));

--- 2967,2973 ----
          CHECK(r);

!         if (countcache == null) countcache = new OpCacheD(cachesize);

!         miscid = CACHEID_SATCOU << NODE_BITS;
          size = Math.pow(2.0, (double) LEVEL(r));

***************
*** 2915,2929 ****
      }

!     float satcount_rec(int r) {
!         OpCache2Entry entry;
!         float size, s;

          if (ISCONST(r)) return r;

-         int res;
          entry = countcache.lookup(SATCOUHASH(r));
!         if ((res = entry.get(r, miscid)) != -1) {
              if (CACHESTATS) countcache.cacheHit++;
!             return Float.intBitsToFloat(res);
          }

--- 2990,3003 ----
      }

!     double satcount_rec(int r) {
!         OpCacheDEntry entry;
!         double size, s;

          if (ISCONST(r)) return r;

          entry = countcache.lookup(SATCOUHASH(r));
!         if ((size = entry.get_sid(r, miscid)) >= 0) {
              if (CACHESTATS) countcache.cacheHit++;
!             return size;
          }

***************
*** 2941,2945 ****
          size += s * satcount_rec(HIGH_r);

!         entry.set(r, miscid, Float.floatToIntBits(size));

          return size;
--- 3015,3019 ----
          size += s * satcount_rec(HIGH_r);

!         entry.set_sid(r, miscid, size);

          return size;
***************
*** 3185,3190 ****
          int n;
          newnodes = new int[bddnodesize*__node_size];
!         System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length);
!         bddnodes = newnodes;

          if (doRehash)
--- 3259,3264 ----
          int n;
          newnodes = new int[bddnodesize*__node_size];
!         System.arraycopy(table, 0, newnodes, 0, table.length);
!         table = newnodes;

          if (doRehash)
***************
*** 3218,3223 ****

          bddnodesize = bdd_prime_gte(initnodesize);

!         bddnodes = new int[bddnodesize*__node_size];

          bddresized = false;
--- 3292,3298 ----

          bddnodesize = bdd_prime_gte(initnodesize);
+         cachesize = bdd_prime_gte(cs);

!         table = new int[bddnodesize*__node_size];

          bddresized = false;
***************
*** 3234,3238 ****
          SETLOW(1, 1); SETHIGH(1, 1);

!         bdd_operator_init(cs);

          bddfreepos = 2;
--- 3309,3313 ----
          SETLOW(1, 1); SETHIGH(1, 1);

!         bdd_operator_init(cachesize);

          bddfreepos = 2;
***************
*** 3242,3246 ****
          gbcollectnum = 0;
          gbcclock = 0;
-         cachesize = cs;
          usednodes_nextreorder = bddnodesize;
          bddmaxnodeincrease = DEFAULTMAXNODEINC;
--- 3317,3320 ----
***************
*** 3250,3255 ****
          bdd_pairs_init();
          bdd_reorder_init();
- 
-         return;
      }

--- 3324,3327 ----
***************
*** 3319,3324 ****
      OpCache3 appexcache;   /* appex(), appall(), appuni(), constrain(), compose() */
      OpCache3 itecache;     /* ite() */
-     OpCache2 countcache;   /* satcount() */
      OpCache2 misccache;    /* other functions */

      void bdd_operator_init(int cachesize) {
--- 3391,3396 ----
      OpCache3 appexcache;   /* appex(), appall(), appuni(), constrain(), compose() */
      OpCache3 itecache;     /* ite() */
      OpCache2 misccache;    /* other functions */
+     OpCacheD countcache;   /* satcount(), pathcount() */

      void bdd_operator_init(int cachesize) {
***************
*** 3347,3375 ****

      void bdd_operator_reset() {
!         singlecache.reset();
!         replacecache.reset();
!         andcache.reset();
!         orcache.reset();
!         applycache.reset();
!         relprodcache.reset();
!         quantcache.reset();
!         appexcache.reset();
!         itecache.reset();
!         countcache.reset();
!         misccache.reset();
      }

      void bdd_operator_clean() {
!         singlecache.clean();
!         replacecache.clean();
!         andcache.clean();
!         orcache.clean();
!         applycache.clean();
!         relprodcache.clean();
!         quantcache.clean();
!         appexcache.clean();
!         itecache.clean();
!         countcache.clean();
!         misccache.clean();
      }

--- 3419,3469 ----

      void bdd_operator_reset() {
!         if (singlecache != null)
!             singlecache.reset();
!         if (replacecache != null)
!             replacecache.reset();
!         if (andcache != null)
!             andcache.reset();
!         if (orcache != null)
!             orcache.reset();
!         if (applycache != null)
!             applycache.reset();
!         if (relprodcache != null)
!             relprodcache.reset();
!         if (quantcache != null)
!             quantcache.reset();
!         if (appexcache != null)
!             appexcache.reset();
!         if (itecache != null)
!             itecache.reset();
!         if (countcache != null)
!             countcache.reset();
!         if (misccache != null)
!             misccache.reset();
      }

      void bdd_operator_clean() {
!         if (singlecache != null)
!             singlecache.clean();
!         if (replacecache != null)
!             replacecache.clean();
!         if (andcache != null)
!             andcache.clean();
!         if (orcache != null)
!             orcache.clean();
!         if (applycache != null)
!             applycache.clean();
!         if (relprodcache != null)
!             relprodcache.clean();
!         if (quantcache != null)
!             quantcache.clean();
!         if (appexcache != null)
!             appexcache.clean();
!         if (itecache != null)
!             itecache.clean();
!         if (countcache != null)
!             countcache.clean();
!         if (misccache != null)
!             misccache.clean();
      }

***************
*** 3377,3381 ****
          quantvarset = new int[bddvarnum];
          quantvarsetID = 0;
!         countcache.reset();
      }

--- 3471,3475 ----
          quantvarset = new int[bddvarnum];
          quantvarsetID = 0;
!         if (countcache != null) countcache.reset();
      }

***************
*** 4313,4317 ****
          bdd_pairs_done();

!         bddnodes = null;
          bddrefstack = null;
          bddvarset = null;
--- 4407,4411 ----
          bdd_pairs_done();

!         table = null;
          bddrefstack = null;
          bddvarset = null;
***************
*** 5258,5262 ****
          for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
              /* This is where we go from .level to .var! */
!             SETVARr(n, bddlevel2var[LEVEL(n)]);

              if (HASREF(n)) {
--- 5352,5358 ----
          for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
              /* This is where we go from .level to .var! */
!             int lev = LEVEL(n);
!             int var = bddlevel2var[lev];
!             SETVARr(n, var);

              if (HASREF(n)) {
***************
*** 6198,6203 ****
          INSTANCE.bddresized = this.bddresized;
          INSTANCE.minfreenodes = this.minfreenodes;
!         INSTANCE.bddnodes = new int[this.bddnodes.length];
!         System.arraycopy(this.bddnodes, 0, INSTANCE.bddnodes, 0, this.bddnodes.length);
          INSTANCE.bddrefstack = new int[this.bddrefstack.length];
          System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length);
--- 6294,6299 ----
          INSTANCE.bddresized = this.bddresized;
          INSTANCE.minfreenodes = this.minfreenodes;
!         INSTANCE.table = new int[this.table.length];
!         System.arraycopy(this.table, 0, INSTANCE.table, 0, this.table.length);
          INSTANCE.bddrefstack = new int[this.bddrefstack.length];
          System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length);