[Javabdd-checkins] SF.net SVN: javabdd: [470] trunk/JavaBDD/net/sf/javabdd

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

Revision: 470
          http://svn.sourceforge.net/javabdd/?rev=470&view=rev
Author:   joewhaley
Date:     2006-11-30 01:22:42 -0800 (Thu, 30 Nov 2006)

Log Message:
-----------
Implement ZDD iterators.

Modified Paths:
--------------
    trunk/JavaBDD/net/sf/javabdd/BDD.java
    trunk/JavaBDD/net/sf/javabdd/JFactory.java

Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDD.java	2006-11-29 08:07:31 UTC (rev 469)
+++ trunk/JavaBDD/net/sf/javabdd/BDD.java	2006-11-30 09:22:42 UTC (rev 470)
@@ -598,10 +598,25 @@
                 BDD rn = lo_empty ? r.high() : r.low();
                 int v = rn.isOne()||rn.isZero() ? f.varNum() - 1 : rn.level() - 1;
                 for ( ; v > LEVEL_r; --v) {
-                    allsatProfile[useLevel?v:f.level2Var(v)] = -1;
+                    allsatProfile[useLevel?v:f.level2Var(v)] = f.isZDD()?(byte)0:(byte)-1;
                 }
                 if (!lo_empty) {
-                    hiStack.addLast(r);
+                    if (f.isZDD()) {
+                        // Check for dont-care bits in ZDD.
+                        BDD rh = r.high();
+                        boolean isDontCare = rn.equals(rh);
+                        rh.free();
+                        if (isDontCare) {
+                            // low child == high child, this is a dont-care bit.
+                            allsatProfile[useLevel?v:f.level2Var(v)] = -1;
+                            r.free();
+                        } else {
+                            hiStack.addLast(r);
+                        }
+                    } else {
+                        // BDD.
+                        hiStack.addLast(r);
+                    }
                 } else {
                     r.free();
                 }
@@ -965,7 +980,7 @@
                 throw new NoSuchElementException();
             }
             //if (lastReturned != null) lastReturned.free();
-            lastReturned = f.one();
+            lastReturned = f.universe();
             //for (int i = 0; i < v.length; ++i) {
             for (int i = v.length-1; i >= 0; --i) {
                 int li = v[i];

Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java	2006-11-29 08:07:31 UTC (rev 469)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java	2006-11-30 09:22:42 UTC (rev 470)
@@ -2978,37 +2978,42 @@
             return r;
 
         if (LEVEL(r) < LEVEL(var)) {
+            // r is not in the set
             if (ISZERO(LOW(r))) {
                 int res = satoneset_rec(HIGH(r), var);
-                int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+                int m = makenode_impl(LEVEL(r), BDDZERO, res);
                 PUSHREF(m);
                 return m;
             } else {
                 int res = satoneset_rec(LOW(r), var);
-                int m = bdd_makenode(LEVEL(r), res, BDDZERO);
+                int m = makenode_impl(LEVEL(r), res, (ZDD && LOW(r) == HIGH(r))?res:BDDZERO);
                 PUSHREF(m);
                 return m;
             }
         } else if (LEVEL(var) < LEVEL(r)) {
             int res = satoneset_rec(r, HIGH(var));
-            if (satPolarity) {
-                int m = bdd_makenode(LEVEL(var), BDDZERO, res);
+            if (!ZDD && satPolarity) {
+                int m = makenode_impl(LEVEL(var), BDDZERO, res);
                 PUSHREF(m);
                 return m;
             } else {
-                int m = bdd_makenode(LEVEL(var), res, BDDZERO);
+                int m = makenode_impl(LEVEL(var), res, BDDZERO);
                 PUSHREF(m);
                 return m;
             }
         } else /* LEVEL(r) == LEVEL(var) */ {
             if (ISZERO(LOW(r))) {
                 int res = satoneset_rec(HIGH(r), HIGH(var));
-                int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+                int m = makenode_impl(LEVEL(r), BDDZERO, res);
                 PUSHREF(m);
                 return m;
             } else {
                 int res = satoneset_rec(LOW(r), HIGH(var));
-                int m = bdd_makenode(LEVEL(r), res, BDDZERO);
+                int m;
+                if (ZDD && satPolarity && LOW(r) == HIGH(r))
+                    m = zdd_makenode(LEVEL(r), BDDZERO, res);
+                else
+                    m = makenode_impl(LEVEL(r), res, BDDZERO);
                 PUSHREF(m);
                 return m;
             }
@@ -3030,7 +3035,7 @@
         res = fullsatone_rec(r);
 
         for (v = LEVEL(r) - 1; v >= 0; v--) {
-            res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+            res = PUSHREF(makenode_impl(v, res, 0));
         }
 
         bdd_enable_reorder();
@@ -3048,19 +3053,19 @@
             int v;
 
             for (v = LEVEL(LOW(r)) - 1; v > LEVEL(r); v--) {
-                res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+                res = PUSHREF(makenode_impl(v, res, 0));
             }
 
-            return PUSHREF(ZDD?zdd_makenode(LEVEL(r), res, 0):bdd_makenode(LEVEL(r), res, 0));
+            return PUSHREF(makenode_impl(LEVEL(r), res, 0));
         } else {
             int res = fullsatone_rec(HIGH(r));
             int v;
 
             for (v = LEVEL(HIGH(r)) - 1; v > LEVEL(r); v--) {
-                res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+                res = PUSHREF(makenode_impl(v, res, 0));
             }
 
-            return PUSHREF(ZDD?zdd_makenode(LEVEL(r), 0, res):bdd_makenode(LEVEL(r), 0, res));
+            return PUSHREF(makenode_impl(LEVEL(r), 0, res));
         }
     }
 


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.