[Javabdd-checkins] JavaBDD/org/sf/javabdd JFactory.java,1.8,1.9

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

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

Modified Files:
	JFactory.java 
Log Message:
Special-case and, or, relprod operations.

Index: JFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JFactory.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -C2 -d -r1.8 -r1.9
*** JFactory.java	9 Aug 2004 21:31:11 -0000	1.8
--- JFactory.java	15 Sep 2004 00:02:07 -0000	1.9
***************
*** 1161,1165 ****
                  if (firstReorder == 0)
                      bdd_disable_reorder();
!                 res = apply_rec(l, r);
                  if (firstReorder == 0)
                      bdd_enable_reorder();
--- 1161,1169 ----
                  if (firstReorder == 0)
                      bdd_disable_reorder();
!                 switch (op) {
!                     case bddop_and: res = and_rec(l, r); break;
!                     case bddop_or: res = or_rec(l, r); break;
!                     default: res = apply_rec(l, r); break;
!                 }
                  if (firstReorder == 0)
                      bdd_enable_reorder();
***************
*** 1183,1207 ****
          int res;
  
          switch (applyop) {
-             case bddop_and :
-                 if (l == r)
-                     return l;
-                 if (ISZERO(l) || ISZERO(r))
-                     return 0;
-                 if (ISONE(l))
-                     return r;
-                 if (ISONE(r))
-                     return l;
-                 break;
-             case bddop_or :
-                 if (l == r)
-                     return l;
-                 if (ISONE(l) || ISONE(r))
-                     return 1;
-                 if (ISZERO(l))
-                     return r;
-                 if (ISZERO(r))
-                     return l;
-                 break;
              case bddop_xor :
                  if (l == r)
--- 1187,1193 ----
          int res;
  
+         if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or);
+         
          switch (applyop) {
              case bddop_xor :
                  if (l == r)
***************
*** 1268,1271 ****
--- 1254,1349 ----
      }
  
+     int and_rec(int l, int r) {
+         BddCacheDataI entry;
+         int res;
+ 
+         if (l == r)
+             return l;
+         if (ISZERO(l) || ISZERO(r))
+             return 0;
+         if (ISONE(l))
+             return r;
+         if (ISONE(r))
+             return l;
+         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
+ 
+         if (entry.a == l && entry.b == r && entry.c == bddop_and) {
+             if (CACHESTATS)
+                 bddcachestats.opHit++;
+             return entry.res;
+         }
+         if (CACHESTATS)
+             bddcachestats.opMiss++;
+ 
+         if (LEVEL(l) == LEVEL(r)) {
+             PUSHREF(and_rec(LOW(l), LOW(r)));
+             PUSHREF(and_rec(HIGH(l), HIGH(r)));
+             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
+         } else if (LEVEL(l) < LEVEL(r)) {
+             PUSHREF(and_rec(LOW(l), r));
+             PUSHREF(and_rec(HIGH(l), r));
+             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
+         } else {
+             PUSHREF(and_rec(l, LOW(r)));
+             PUSHREF(and_rec(l, HIGH(r)));
+             res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+         }
+ 
+         POPREF(2);
+ 
+         entry.a = l;
+         entry.b = r;
+         entry.c = bddop_and;
+         entry.res = res;
+ 
+         return res;
+     }
+     
+     int or_rec(int l, int r) {
+         BddCacheDataI entry;
+         int res;
+ 
+         if (l == r)
+             return l;
+         if (ISONE(l) || ISONE(r))
+             return 1;
+         if (ISZERO(l))
+             return r;
+         if (ISZERO(r))
+             return l;
+         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or));
+ 
+         if (entry.a == l && entry.b == r && entry.c == bddop_or) {
+             if (CACHESTATS)
+                 bddcachestats.opHit++;
+             return entry.res;
+         }
+         if (CACHESTATS)
+             bddcachestats.opMiss++;
+ 
+         if (LEVEL(l) == LEVEL(r)) {
+             PUSHREF(or_rec(LOW(l), LOW(r)));
+             PUSHREF(or_rec(HIGH(l), HIGH(r)));
+             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
+         } else if (LEVEL(l) < LEVEL(r)) {
+             PUSHREF(or_rec(LOW(l), r));
+             PUSHREF(or_rec(HIGH(l), r));
+             res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
+         } else {
+             PUSHREF(or_rec(l, LOW(r)));
+             PUSHREF(or_rec(l, HIGH(r)));
+             res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+         }
+ 
+         POPREF(2);
+ 
+         entry.a = l;
+         entry.b = r;
+         entry.c = bddop_or;
+         entry.res = res;
+ 
+         return res;
+     }
+ 
      int relprod_rec(int l, int r) {
          BddCacheDataI entry;
***************
*** 1284,1293 ****
          int LEVEL_r = LEVEL(r);
          if (LEVEL_l > quantlast && LEVEL_r > quantlast) {
!             int oldop = applyop;
!             applyop = appexop;
!             res = apply_rec(l, r);
!             applyop = oldop;
          } else {
!             entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop));
              if (entry.a == l && entry.b == r && entry.c == appexid) {
                  if (CACHESTATS)
--- 1362,1370 ----
          int LEVEL_r = LEVEL(r);
          if (LEVEL_l > quantlast && LEVEL_r > quantlast) {
!             applyop = bddop_and;
!             res = and_rec(l, r);
!             applyop = bddop_or;
          } else {
!             entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
              if (entry.a == l && entry.b == r && entry.c == appexid) {
                  if (CACHESTATS)
***************
*** 1302,1306 ****
                  PUSHREF(relprod_rec(HIGH(l), HIGH(r)));
                  if (INVARSET(LEVEL_l))
!                     res = apply_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
--- 1379,1383 ----
                  PUSHREF(relprod_rec(HIGH(l), HIGH(r)));
                  if (INVARSET(LEVEL_l))
!                     res = or_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
***************
*** 1309,1313 ****
                  PUSHREF(relprod_rec(HIGH(l), r));
                  if (INVARSET(LEVEL_l))
!                     res = apply_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
--- 1386,1390 ----
                  PUSHREF(relprod_rec(HIGH(l), r));
                  if (INVARSET(LEVEL_l))
!                     res = or_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
***************
*** 1316,1320 ****
                  PUSHREF(relprod_rec(l, HIGH(r)));
                  if (INVARSET(LEVEL_r))
!                     res = apply_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
--- 1393,1397 ----
                  PUSHREF(relprod_rec(l, HIGH(r)));
                  if (INVARSET(LEVEL_r))
!                     res = or_rec(READREF(2), READREF(1));
                  else
                      res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
***************
*** 1365,1369 ****
                  if (firstReorder == 0)
                      bdd_disable_reorder();
!                 res = opr == -1 ? relprod_rec(l, r) : appquant_rec(l, r);
                  if (firstReorder == 0)
                      bdd_enable_reorder();
--- 1442,1446 ----
                  if (firstReorder == 0)
                      bdd_disable_reorder();
!                 res = opr == bddop_and ? relprod_rec(l, r) : appquant_rec(l, r);
                  if (firstReorder == 0)
                      bdd_enable_reorder();
***************
*** 1439,1453 ****
          int res;
  
          switch (appexop) {
-             case bddop_and :
-                 if (l == 0 || r == 0)
-                     return 0;
-                 if (l == r)
-                     return quant_rec(l);
-                 if (l == 1)
-                     return quant_rec(r);
-                 if (r == 1)
-                     return quant_rec(l);
-                 break;
              case bddop_or :
                  if (l == 1 || r == 1)
--- 1516,1522 ----
          int res;
  
+         if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and);
+         
          switch (appexop) {
              case bddop_or :
                  if (l == 1 || r == 1)
***************
*** 1483,1487 ****
              int oldop = applyop;
              applyop = appexop;
!             res = apply_rec(l, r);
              applyop = oldop;
          } else {
--- 1552,1560 ----
              int oldop = applyop;
              applyop = appexop;
!             switch (applyop) {
!             case bddop_and: res = and_rec(l, r); break;
!             case bddop_or: res = or_rec(l, r); break;
!             default: res = apply_rec(l, r); break;
!             }
              applyop = oldop;
          } else {
***************
*** 1495,1519 ****
                  bddcachestats.opMiss++;
  
              if (LEVEL(l) == LEVEL(r)) {
                  PUSHREF(appquant_rec(LOW(l), LOW(r)));
                  PUSHREF(appquant_rec(HIGH(l), HIGH(r)));
!                 if (INVARSET(LEVEL(l)))
!                     res = apply_rec(READREF(2), READREF(1));
!                 else
!                     res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
              } else if (LEVEL(l) < LEVEL(r)) {
                  PUSHREF(appquant_rec(LOW(l), r));
                  PUSHREF(appquant_rec(HIGH(l), r));
!                 if (INVARSET(LEVEL(l)))
!                     res = apply_rec(READREF(2), READREF(1));
!                 else
!                     res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
              } else {
                  PUSHREF(appquant_rec(l, LOW(r)));
                  PUSHREF(appquant_rec(l, HIGH(r)));
!                 if (INVARSET(LEVEL(r)))
!                     res = apply_rec(READREF(2), READREF(1));
!                 else
!                     res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
              }
  
--- 1568,1594 ----
                  bddcachestats.opMiss++;
  
+             int lev;
              if (LEVEL(l) == LEVEL(r)) {
                  PUSHREF(appquant_rec(LOW(l), LOW(r)));
                  PUSHREF(appquant_rec(HIGH(l), HIGH(r)));
!                 lev = LEVEL(l);
              } else if (LEVEL(l) < LEVEL(r)) {
                  PUSHREF(appquant_rec(LOW(l), r));
                  PUSHREF(appquant_rec(HIGH(l), r));
!                 lev = LEVEL(l);
              } else {
                  PUSHREF(appquant_rec(l, LOW(r)));
                  PUSHREF(appquant_rec(l, HIGH(r)));
!                 lev = LEVEL(r);
!             }
!             if (INVARSET(lev)) {
!                 int r2 = READREF(2), r1 = READREF(1);
!                 switch (applyop) {
!                 case bddop_and: res = and_rec(r2, r1); break;
!                 case bddop_or: res = or_rec(r2, r1); break;
!                 default: res = apply_rec(r2, r1); break;
!                 }
!             } else {
!                 res = bdd_makenode(lev, READREF(2), READREF(1));
              }
  
***************
*** 1548,1555 ****
          PUSHREF(quant_rec(HIGH(r)));
  
!         if (INVARSET(LEVEL(r)))
!             res = apply_rec(READREF(2), READREF(1));
!         else
              res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
  
          POPREF(2);
--- 1623,1636 ----
          PUSHREF(quant_rec(HIGH(r)));
  
!         if (INVARSET(LEVEL(r))) {
!             int r2 = READREF(2), r1 = READREF(1);
!             switch (applyop) {
!             case bddop_and: res = and_rec(r2, r1); break;
!             case bddop_or: res = or_rec(r2, r1); break;
!             default: res = apply_rec(r2, r1); break;
!             }
!         } else {
              res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+         }
  
          POPREF(2);
***************
*** 2053,2057 ****
              POPREF(2);
          } else /* LEVEL(d) < LEVEL(f) */ {
!             PUSHREF(apply_rec(LOW(d), HIGH(d))); /* Exist quant */
              res = simplify_rec(f, READREF(1));
              POPREF(1);
--- 2134,2138 ----
              POPREF(2);
          } else /* LEVEL(d) < LEVEL(f) */ {
!             PUSHREF(or_rec(LOW(d), HIGH(d))); /* Exist quant */
              res = simplify_rec(f, READREF(1));
              POPREF(1);