[Javabdd-checkins] JavaBDD/buddy/src bddop.c,1.9,1.10

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

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

Modified Files:
	bddop.c 
Log Message:
Added correct support for unique() and appuni().

Index: bddop.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v
retrieving revision 1.9
retrieving revision 1.10
diff -C2 -d -r1.9 -r1.10
*** bddop.c	31 Jan 2005 10:02:43 -0000	1.9
--- bddop.c	31 Jan 2005 12:03:34 -0000	1.10
***************
*** 134,139 ****
--- 134,141 ----
  static int    simplify_rec(BDD, BDD);
  static int    quant_rec(int);
+ static int    unique_rec(int, int);
  static int    appquant_rec(int, int);
  static int    appquant_rec0(int, int);
+ static int    appuni_rec(int, int, int);
  static int    restrict_rec(int);
  static BDD    constrain_rec(BDD, BDD);
***************
*** 2158,2164 ****
     if (setjmp(bddexception) == 0)
     {
-       if (varset2vartable(var) < 0)
- 	 RETURN_BDD(bddfalse);
- 
        INITREF;
        quantid = (var << 3) | CACHEID_UNIQUE;
--- 2160,2163 ----
***************
*** 2167,2171 ****
        if (!firstReorder)
  	 bdd_disable_reorder();
!       res = quant_rec(r);
        if (!firstReorder)
  	 bdd_enable_reorder();
--- 2166,2170 ----
        if (!firstReorder)
  	 bdd_disable_reorder();
!       res = unique_rec(r, var);
        if (!firstReorder)
  	 bdd_enable_reorder();
***************
*** 2223,2226 ****
--- 2222,2267 ----
  }
  
+ static int unique_rec(int r, int q) {
+     BddCacheData3 *entry;
+     int res;
+     int LEVEL_r, LEVEL_q;
+ 
+     LEVEL_r = LEVEL(r);
+     LEVEL_q = LEVEL(q);
+     if (LEVEL_r > LEVEL_q) {
+         // Skipped a quantified node, answer is zero.
+         return BDDZERO;
+     }
+         
+     if (r < 2 || q < 2)
+         return r;
+         
+     entry = BddCache_lookup(&quantcache, QUANTHASH(r));
+     if (entry->a == r  &&  entry->b == quantid) {
+ #ifdef CACHESTATS
+         bddcachestats.opHit++;
+ #endif
+         return entry->res;
+     }
+ #ifdef CACHESTATS
+     bddcachestats.opMiss++;
+ #endif
+     if (LEVEL_r == LEVEL_q) {
+         PUSHREF(unique_rec(LOW(r), HIGH(q)));
+         PUSHREF(unique_rec(HIGH(r), HIGH(q)));
+         res = apply_rec(READREF(2), READREF(1));
+     } else {
+         PUSHREF(unique_rec(LOW(r), q));
+         PUSHREF(unique_rec(HIGH(r), q));
+         res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+     }
+     POPREF(2);
+ 
+     entry->a = r;
+     entry->b = quantid;
+     entry->res = res;
+     return res;
+ }
+ 
  
  /*=== APPLY & QUANTIFY =================================================*/
***************
*** 2422,2432 ****
       if (quantcache.table == NULL && BddCache3_init(&quantcache,cachesize) < 0)
         return bdd_error(BDD_MEMORY);
  
   again:
     if (setjmp(bddexception) == 0)
     {
-       if (varset2vartable(var) < 0)
- 	 RETURN_BDD(bddfalse);
- 
        INITREF;
        applyop = bddop_xor;
--- 2463,2472 ----
       if (quantcache.table == NULL && BddCache3_init(&quantcache,cachesize) < 0)
         return bdd_error(BDD_MEMORY);
+      if (appexcache.table == NULL && BddCache4_init(&appexcache,cachesize) < 0)
+        return bdd_error(BDD_MEMORY);
  
   again:
     if (setjmp(bddexception) == 0)
     {
        INITREF;
        applyop = bddop_xor;
***************
*** 2437,2441 ****
        if (!firstReorder)
  	 bdd_disable_reorder();
!       res = appquant_rec(l, r);
        if (!firstReorder)
  	 bdd_enable_reorder();
--- 2477,2481 ----
        if (!firstReorder)
  	 bdd_disable_reorder();
!       res = appuni_rec(l, r, var);
        if (!firstReorder)
  	 bdd_enable_reorder();
***************
*** 2588,2591 ****
--- 2628,2712 ----
  }
  
+ static int appuni_rec(int l, int r, int var) {
+     BddCacheData4 *entry;
+     int res;
+ 
+     int LEVEL_l, LEVEL_r, LEVEL_var;
+     LEVEL_l = LEVEL(l);
+     LEVEL_r = LEVEL(r);
+     LEVEL_var = LEVEL(var);
+ 
+     if (LEVEL_l > LEVEL_var && LEVEL_r > LEVEL_var) {
+         // Skipped a quantified node, answer is zero.
+         return BDDZERO;
+     }
+ 
+     if (ISCONST(l) && ISCONST(r))
+         res = oprres[appexop][(l << 1) | r];
+     else if (ISCONST(var)) {
+         int oldop = applyop;
+         applyop = appexop;
+         res = apply_rec(l, r);
+         applyop = oldop;
+     } else {
+         int lev;
+         entry = BddCache_lookup(&appexcache, APPEXHASH(l,r,appexop));
+         if (entry->a == l  &&  entry->b == r  &&  entry->r.c == appexid) {
+ #ifdef CACHESTATS
+             bddcachestats.opHit++;
+ #endif
+             return entry->r.res;
+         }
+ #ifdef CACHESTATS
+         bddcachestats.opMiss++;
+ #endif
+ 
+         if (LEVEL_l == LEVEL_r) {
+             if (LEVEL_l == LEVEL_var) {
+                 lev = -1;
+                 var = HIGH(var);
+             } else {
+                 lev = LEVEL_l;
+             }
+             PUSHREF(appuni_rec(LOW(l), LOW(r), var));
+             PUSHREF(appuni_rec(HIGH(l), HIGH(r), var));
+             lev = LEVEL_l;
+         } else if (LEVEL_l < LEVEL_r) {
+             if (LEVEL_l == LEVEL_var) {
+                 lev = -1;
+                 var = HIGH(var);
+             } else {
+                 lev = LEVEL_l;
+             }
+             PUSHREF(appuni_rec(LOW(l), r, var));
+             PUSHREF(appuni_rec(HIGH(l), r, var));
+         } else {
+             if (LEVEL_r == LEVEL_var) {
+                 lev = -1;
+                 var = HIGH(var);
+             } else {
+                 lev = LEVEL_r;
+             }
+             PUSHREF(appuni_rec(l, LOW(r), var));
+             PUSHREF(appuni_rec(l, HIGH(r), var));
+         }
+         if (lev == -1) {
+             int r2 = READREF(2), r1 = READREF(1);
+             res = apply_rec(r2, r1);
+         } else {
+             res = bdd_makenode(lev, READREF(2), READREF(1));
+         }
+ 
+         POPREF(2);
+ 
+         entry->a = l;
+         entry->b = r;
+         entry->r.c = appexid;
+         entry->r.res = res;
+         }
+ 
+     return res;
+ }
+ 
  #if defined(SPECIALIZE_RELPROD)
  /* Special version of appex for common case of relprod. */