[Javabdd-checkins] SF.net SVN: javabdd: [465] trunk/JavaBDD/net/sf/javabdd
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [465] trunk/JavaBDD/net/sf/javabdd
|
From: <joe...@us...> - 2006-07-26 17:46:44
|
Revision: 465 Author: joewhaley Date: 2006-07-26 09:42:44 -0700 (Wed, 26 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=465&view=rev Log Message: ----------- Improved ZDD support. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-26 16:42:44 UTC (rev 465) @@ -48,6 +48,14 @@ public abstract boolean isOne(); /** + * <p>Returns true if this BDD is the universe BDD. + * The universal BDD differs from the one BDD in ZDD mode.</p> + * + * @return true if this BDD is the universe BDD + */ + public boolean isUniverse() { return isOne(); } + + /** * <p>Converts this BDD to a new BDDVarSet.</p> * * <p>This BDD must be a boolean function that represents the all-true minterm Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -196,6 +196,14 @@ public abstract BDD one(); /** + * <p>Get the constant universe BDD. + * (The universe BDD differs from the one BDD in ZDD mode.)</p> + * + * <p>Compare to bdd_true.</p> + */ + public BDD universe() { return one(); } + + /** * <p>Get an empty BDDVarSet.</p> * * <p>Compare to bdd_true.</p> Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-26 16:42:44 UTC (rev 465) @@ -20,6 +20,7 @@ protected abstract void delref_impl(/*bdd*/int v); protected abstract /*bdd*/int zero_impl(); protected abstract /*bdd*/int one_impl(); + protected /*bdd*/int universe_impl() { return one_impl(); } protected abstract /*bdd*/int invalid_bdd_impl(); protected abstract int var_impl(/*bdd*/int v); protected abstract int level_impl(/*bdd*/int v); @@ -28,6 +29,7 @@ protected abstract /*bdd*/int ithVar_impl(int var); protected abstract /*bdd*/int nithVar_impl(int var); + protected abstract /*bdd*/int makenode_impl(int lev, /*bdd*/int lo, /*bdd*/int hi); protected abstract /*bdd*/int ite_impl(/*bdd*/int v1, /*bdd*/int v2, /*bdd*/int v3); protected abstract /*bdd*/int apply_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr); protected abstract /*bdd*/int not_impl(/*bdd*/int v1); @@ -121,6 +123,9 @@ public boolean isOne() { return v == one_impl(); } + public boolean isUniverse() { + return v == universe_impl(); + } public boolean isZero() { return v == zero_impl(); } @@ -236,7 +241,7 @@ public class IntBDDVarSet extends BDDVarSet { /*bdd*/int v; - private IntBDDVarSet(/*bdd*/int v) { + protected IntBDDVarSet(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -256,12 +261,15 @@ public BDDVarSet id() { return makeBDDVarSet(v); } + protected int do_intersect(int v1, int v2) { + return apply_impl(v1, v2, or); + } public BDDVarSet intersect(BDDVarSet b) { - return makeBDDVarSet(apply_impl(v, unwrap(b), or)); + return makeBDDVarSet(do_intersect(v, unwrap(b))); } public BDDVarSet intersectWith(BDDVarSet b) { /*bdd*/int v2 = unwrap(b); - /*bdd*/int v3 = apply_impl(v, v2, or); + /*bdd*/int v3 = do_intersect(v, v2); addref_impl(v3); delref_impl(v); if (this != b) @@ -300,18 +308,21 @@ } return result; } + protected int do_unionvar(int v, int var) { + return apply_impl(v, ithVar_impl(var), and); + } + protected int do_union(int v1, int v2) { + return apply_impl(v1, v2, and); + } public BDDVarSet union(BDDVarSet b) { - return makeBDDVarSet(apply_impl(v, unwrap(b), and)); + return makeBDDVarSet(do_union(v, unwrap(b))); } public BDDVarSet union(int var) { - /*bdd*/int v2 = ithVar_impl(var); - /*bdd*/int v3 = apply_impl(v, v2, and); - delref_impl(v2); - return makeBDDVarSet(v3); + return makeBDDVarSet(do_unionvar(v, var)); } public BDDVarSet unionWith(BDDVarSet b) { /*bdd*/int v2 = unwrap(b); - /*bdd*/int v3 = apply_impl(v, v2, and); + /*bdd*/int v3 = do_union(v, v2); addref_impl(v3); delref_impl(v); if (this != b) @@ -320,11 +331,9 @@ return this; } public BDDVarSet unionWith(int var) { - /*bdd*/int v2 = ithVar_impl(var); - /*bdd*/int v3 = apply_impl(v, v2, and); + /*bdd*/int v3 = do_unionvar(v, var); addref_impl(v3); delref_impl(v); - delref_impl(v2); v = v3; return this; } @@ -348,11 +357,106 @@ } + public class IntZDDVarSet extends IntBDDVarSet { + protected IntZDDVarSet(/*bdd*/int v) { + super(v); + } + protected int do_intersect(int v1, int v2) { + if (v1 == one_impl()) return v2; + if (v2 == one_impl()) return v1; + int l1, l2; + l1 = level_impl(v1); + l2 = level_impl(v2); + for (;;) { + if (v1 == v2) + return v1; + if (l1 < l2) { + v1 = high_impl(v1); + if (v1 == one_impl()) return v2; + l1 = level_impl(v1); + } else if (l1 > l2) { + v2 = high_impl(v2); + if (v2 == one_impl()) return v1; + l2 = level_impl(v2); + } else { + int k = do_intersect(high_impl(v1), high_impl(v2)); + addref_impl(k); + int result = makenode_impl(l1, zero_impl(), k); + delref_impl(k); + return result; + } + } + } + protected int do_union(int v1, int v2) { + if (v1 == v2) return v1; + if (v1 == one_impl()) return v2; + if (v2 == one_impl()) return v1; + int l1, l2; + l1 = level_impl(v1); + l2 = level_impl(v2); + int vv1 = v1, vv2 = v2, lev = l1; + if (l1 <= l2) + vv1 = high_impl(v1); + if (l1 >= l2) { + vv2 = high_impl(v2); + lev = l2; + } + int k = do_union(vv1, vv2); + addref_impl(k); + int result = makenode_impl(lev, zero_impl(), k); + delref_impl(k); + return result; + } + protected int do_unionvar(int v, int var) { + return do_unionlevel(v, var2Level(var)); + } + private int do_unionlevel(int v, int lev) { + if (v == one_impl()) + return makenode_impl(lev, zero_impl(), one_impl()); + int l = level_impl(v); + if (l == lev) { + return v; + } else if (l > lev) { + return makenode_impl(lev, zero_impl(), v); + } else { + int k = do_unionlevel(high_impl(v), lev); + addref_impl(k); + int result = makenode_impl(lev, zero_impl(), k); + return result; + } + } + } + + public class IntZDDVarSetWithFinalizer extends IntZDDVarSet { + + protected IntZDDVarSetWithFinalizer(int v) { + super(v); + } + + protected void finalize() throws Throwable { + super.finalize(); + if (USE_FINALIZER) { + if (false && v != invalid_bdd_impl()) { + System.out.println("BDD not freed! "+System.identityHashCode(this)); + } + deferredFree(v); + } + } + + } + protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) { - if (USE_FINALIZER) - return new IntBDDVarSetWithFinalizer(v); - else - return new IntBDDVarSet(v); + if (true || isZDD()) { + if (USE_FINALIZER) + return new IntZDDVarSetWithFinalizer(v); + else + return new IntZDDVarSet(v); + } else { + if (USE_FINALIZER) + return new IntBDDVarSetWithFinalizer(v); + else + return new IntBDDVarSet(v); + } } protected static final /*bdd*/int unwrap(BDDVarSet b) { @@ -387,6 +491,10 @@ return makeBDD(one_impl()); } + public BDD universe() { + return makeBDD(universe_impl()); + } + public BDDVarSet emptySet() { return makeBDDVarSet(one_impl()); } Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -115,6 +115,7 @@ protected int nithVar_impl(int var) { return nithVar0(var); } private static native int nithVar0(int var); + protected int makenode_impl(int lev, int lo, int hi) { return ite0(ithVar_impl(level2Var0(lev)), hi, lo); } protected int ite_impl(int v1, int v2, int v3) { return ite0(v1, v2, v3); } private static native int ite0(int b, int c, int d); protected int apply_impl(int v1, int v2, BDDOp opr) { return apply0(v1, v2, opr.id); } Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -62,6 +62,7 @@ throw new BDDException(); return bdd.not(vars[var]); } + protected int makenode_impl(int lev, int lo, int hi) { return bdd.mk(lev, lo, hi); } protected int ite_impl(int v1, int v2, int v3) { return bdd.ite(v1, v2, v3); } protected int apply_impl(int x, int y, BDDOp opr) { int r; Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -37,7 +37,7 @@ */ public static boolean FLUSH_CACHE_ON_GC = true; - static final boolean VERIFY_ASSERTIONS = false; + static final boolean VERIFY_ASSERTIONS = true; static final boolean CACHESTATS = false; static final boolean SWAPCOUNT = false; @@ -67,7 +67,7 @@ }); } - boolean ZDD = false; + boolean ZDD = true; /** * Implementation of BDDPairing used by JFactory. @@ -102,6 +102,7 @@ sb.append('{'); boolean any = false; for (int i = 0; i < result.length; ++i) { + // TODO: revisit for zdd if (result[i] != bdd_ithvar(bddlevel2var[i])) { if (any) sb.append(", "); any = true; @@ -124,6 +125,7 @@ bddPair p = new bddPair(); p.result = new int[bddvarnum]; int n; + // TODO: revisit for zdd for (n = 0; n < bddvarnum; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); @@ -140,6 +142,7 @@ protected void delref_impl(int v) { bdd_delref(v); } protected int zero_impl() { return BDDZERO; } protected int one_impl() { return BDDONE; } + protected int universe_impl() { return univ; } protected int invalid_bdd_impl() { return INVALID_BDD; } protected int var_impl(int v) { return bdd_var(v); } protected int level_impl(int v) { return LEVEL(v); } @@ -148,6 +151,12 @@ protected int ithVar_impl(int var) { return bdd_ithvar(var); } protected int nithVar_impl(int var) { return bdd_nithvar(var); } + protected int makenode_impl(int lev, int lo, int hi) { + if (ZDD) + return zdd_makenode(lev, lo, hi); + else + return bdd_makenode(lev, lo, hi); + } protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); } protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); } protected int not_impl(int v1) { return bdd_not(v1); } @@ -456,7 +465,7 @@ prev_interleaved = inter; } BddTree newchild = my_vartree[0]; - _assert(newchild.prev == null); + if (VERIFY_ASSERTIONS) _assert(newchild.prev == null); //while (newchild.prev != null) newchild = newchild.prev; if (parent == null) vartree = newchild; else parent.nextlevel = newchild; @@ -492,8 +501,6 @@ return null; } - - /***** IMPLEMENTATION BELOW *****/ static final int REF_MASK = 0xFFC00000; @@ -710,6 +717,7 @@ /*=== PRIVATE KERNEL VARIABLES =========================================*/ int[] bddvarset; /* Set of defined BDD variables */ + int univ = 1; /* Universal set (used for ZDD) */ int gbcollectnum; /* Number of garbage collections */ int cachesize; /* Size of the operator caches */ long gbcclock; /* Clock ticks used in GBC */ @@ -941,8 +949,10 @@ again : for (;;) { try { INITREF(); + if (numReorder == 0) bdd_disable_reorder(); - res = ZDD ? znot_rec(r) : not_rec(r); + if (ZDD) res = zdiff_rec(univ, r); + else res = not_rec(r); if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); @@ -985,36 +995,6 @@ return res; } - int znot_rec(int r) { - BddCacheDataI entry; - int res; - - if (ISZERO(r)) - return bddtrue; - if (ISONE(r)) - return bddfalse; - - entry = BddCache_lookupI(applycache, NOTHASH(r)); - - if (entry.a == r && entry.c == bddop_not) { - if (CACHESTATS) - cachestats.opHit++; - return entry.res; - } - if (CACHESTATS) - cachestats.opMiss++; - - PUSHREF(znot_rec(LOW(r))); - res = bdd_makenode(LEVEL(r), READREF(1), HIGH(r)); - POPREF(1); - - entry.a = r; - entry.c = bddop_not; - entry.res = res; - - return res; - } - int bdd_ite(int f, int g, int h) { int res; int numReorder = 1; @@ -1136,7 +1116,7 @@ if (ISONE(g) && ISZERO(h)) return f; if (ISZERO(g) && ISONE(h)) - return znot_rec(f); + return zdiff_rec(univ, f); int v = Math.min(LEVEL(g), LEVEL(h)); if (LEVEL(f) < v) @@ -1155,43 +1135,43 @@ if (LEVEL(f) == LEVEL(h)) { PUSHREF(zite_rec(LOW(f), LOW(g), LOW(h))); PUSHREF(zite_rec(HIGH(f), HIGH(g), HIGH(h))); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else if (LEVEL(f) < LEVEL(h)) { PUSHREF(zite_rec(LOW(f), LOW(g), h)); PUSHREF(zite_rec(HIGH(f), HIGH(g), 0)); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else /* f > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } else if (LEVEL(f) < LEVEL(g)) { if (LEVEL(f) == LEVEL(h)) { PUSHREF(zite_rec(LOW(f), g, LOW(h))); PUSHREF(zite_rec(HIGH(f), 0, HIGH(h))); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else if (LEVEL(f) < LEVEL(h)) { res = zite_rec(LOW(f), g, h); } else /* f > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } else /* f > g */ { if (LEVEL(g) == LEVEL(h)) { PUSHREF(zite_rec(f, LOW(g), LOW(h))); - res = bdd_makenode(LEVEL(g), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(g), HIGH(h), READREF(1)); POPREF(1); } else if (LEVEL(g) < LEVEL(h)) { PUSHREF(zite_rec(f, LOW(g), h)); - res = bdd_makenode(LEVEL(g), 0, READREF(1)); + res = zdd_makenode(LEVEL(g), 0, READREF(1)); POPREF(1); } else /* g > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } @@ -1253,11 +1233,18 @@ PUSHREF(replace_rec(LOW(r))); PUSHREF(replace_rec(HIGH(r))); - res = - bdd_correctify( - LEVEL(replacepair[LEVEL(r)]), - READREF(2), - READREF(1)); + if (ZDD) + res = + zdd_correctify( + LEVEL(replacepair[LEVEL(r)]), + READREF(2), + READREF(1)); + else + res = + bdd_correctify( + LEVEL(replacepair[LEVEL(r)]), + READREF(2), + READREF(1)); POPREF(2); entry.a = r; @@ -1296,6 +1283,36 @@ return res; /* FIXME: cache ? */ } + int zdd_correctify(int level, int l, int r) { + // TODO: This function is wrong. Need to figure out how to do replace in ZDD. + int res; + + if (level < LEVEL(l) && level < LEVEL(r)) + return zdd_makenode(level, l, r); + + if (level == LEVEL(l) || level == LEVEL(r)) { + bdd_error(BDD_REPLACE); + return 0; + } + + if (LEVEL(l) == LEVEL(r)) { + PUSHREF(zdd_correctify(level, LOW(l), LOW(r))); + PUSHREF(zdd_correctify(level, HIGH(l), HIGH(r))); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else if (LEVEL(l) < LEVEL(r)) { + PUSHREF(zdd_correctify(level, LOW(l), r)); + PUSHREF(zdd_correctify(level, HIGH(l), r)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else { + PUSHREF(zdd_correctify(level, l, LOW(r))); + PUSHREF(zdd_correctify(level, l, HIGH(r))); + res = zdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } + POPREF(2); + + return res; /* FIXME: cache ? */ + } + int bdd_apply(int l, int r, int op) { int res; int numReorder = 1; @@ -1483,7 +1500,7 @@ PUSHREF(zand_rec(LOW(l), LOW(r))); PUSHREF(zand_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); @@ -1547,8 +1564,8 @@ if (l == r) return l; - if (ISONE(l) || ISONE(r)) - return 1; + //if (ISONE(l) || ISONE(r)) + // return 1; if (ISZERO(l)) return r; if (ISZERO(r)) @@ -1566,15 +1583,15 @@ if (LEVEL(l) == LEVEL(r)) { PUSHREF(zor_rec(LOW(l), LOW(r))); PUSHREF(zor_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); } else { if (LEVEL(l) < LEVEL(r)) { PUSHREF(zor_rec(LOW(l), r)); - res = bdd_makenode(LEVEL(l), READREF(1), HIGH(l)); + res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l)); } else { PUSHREF(zor_rec(l, LOW(r))); - res = bdd_makenode(LEVEL(r), READREF(1), HIGH(r)); + res = zdd_makenode(LEVEL(r), READREF(1), HIGH(r)); } POPREF(1); } @@ -1591,16 +1608,16 @@ BddCacheDataI entry; int res; - if (ISZERO(l) || ISONE(r) || l == r) + if (ISZERO(l) /*|| ISONE(r)*/ || l == r) return 0; if (ISZERO(r)) return l; if (LEVEL(l) > LEVEL(r)) return zdiff_rec(l, LOW(r)); - entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and)); + entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_diff)); - if (entry.a == l && entry.b == r && entry.c == bddop_and) { + if (entry.a == l && entry.b == r && entry.c == bddop_diff) { if (CACHESTATS) cachestats.opHit++; return entry.res; @@ -1611,11 +1628,11 @@ if (LEVEL(l) == LEVEL(r)) { PUSHREF(zdiff_rec(LOW(l), LOW(r))); PUSHREF(zdiff_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); } else { PUSHREF(zdiff_rec(LOW(l), r)); - res = bdd_makenode(LEVEL(l), READREF(1), HIGH(l)); + res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l)); POPREF(1); } @@ -2050,7 +2067,9 @@ default: res = apply_rec(r2, r1); break; } } else { - res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + res = ZDD + ? zdd_makenode(LEVEL(r), READREF(2), READREF(1)) + : bdd_makenode(LEVEL(r), READREF(2), READREF(1)); } POPREF(2); @@ -3207,22 +3226,36 @@ } int bdd_makenode(int level, int low, int high) { - int hash2; - int res; + if (VERIFY_ASSERTIONS) _assert(!ZDD); + + if (CACHESTATS) + cachestats.uniqueAccess++; + // check whether children are equal + if (low == high) + return low; + + return makenode(level, low, high); + } + + int zdd_makenode(int level, int low, int high) { + if (VERIFY_ASSERTIONS) _assert(ZDD); + if (CACHESTATS) cachestats.uniqueAccess++; + + // check whether high child is zero + if (high == 0) + return low; + + return makenode(level, low, high); + } + + // Don't call directly - call bdd_makenode or zdd_makenode instead. + private int makenode(int level, int low, int high) { + int hash2; + int res; - if (ZDD) { - /* check whether high child is zero */ - if (high == 0) - return low; - } else { - /* check whether childs are equal */ - if (low == high) - return low; - } - /* Try to find an existing node of this kind */ hash2 = NODEHASH(level, low, high); res = HASH(hash2); @@ -3715,6 +3748,7 @@ bdd_error(BDD_VAR); bdd_delref(pair.result[bddvar2level[oldvar]]); + // TODO: revisit for zdd pair.result[bddvar2level[oldvar]] = bdd_ithvar(newvar); pair.id = update_pairsid(); @@ -3748,6 +3782,7 @@ void bdd_resetpair(bddPair p) { int n; + // TODO: revisit for zdd for (n = 0; n < bddvarnum; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); p.last = 0; @@ -3826,6 +3861,7 @@ System.arraycopy(p.result, 0, new_result, 0, oldsize); p.result = new_result; + // TODO: revisit for zdd for (n = oldsize; n < newsize; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); } @@ -4757,16 +4793,36 @@ bddrefstack = new int[num * 2 + 1]; bddrefstacktop = 0; + if (ZDD) + bddvarnum = 0; // need to recreate all of them for ZDD + + univ = 1; for (bdv = bddvarnum; bddvarnum < num; bddvarnum++) { - bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1)); - bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0); - POPREF(1); + if (ZDD) { + int res = 1, res_not = 1; + for (int k = num-1; k >= 0; --k) { + PUSHREF(res); + PUSHREF(res_not); + PUSHREF(univ); + res = zdd_makenode(k, (k == bddvarnum)?0:res, res); + res_not = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not); + if (bdv == bddvarnum) univ = zdd_makenode(k, univ, univ); + POPREF(3); + } + bddvarset[bddvarnum * 2] = res; + bddvarset[bddvarnum * 2 + 1] = res_not; + SETMAXREF(univ); + } else { + bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1)); + bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0); + POPREF(1); + } if (bdderrorcond != 0) { bddvarnum = bdv; return -bdderrorcond; } - + SETMAXREF(bddvarset[bddvarnum * 2]); SETMAXREF(bddvarset[bddvarnum * 2 + 1]); bddlevel2var[bddvarnum] = bddvarnum; @@ -5717,6 +5773,7 @@ int next; } + // TODO: revisit for zdd int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException { int key, var, low, high, root = 0, n; Modified: trunk/JavaBDD/net/sf/javabdd/MicroFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -149,6 +149,7 @@ protected int ithVar_impl(int var) { return bdd_ithvar(var); } protected int nithVar_impl(int var) { return bdd_nithvar(var); } + protected int makenode_impl(int lev, int lo, int hi) { return bdd_makenode(lev, lo, hi); } protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); } protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); } protected int not_impl(int v1) { return bdd_not(v1); } This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
