[Javabdd-checkins] SF.net SVN: javabdd: [468] trunk/JavaBDD
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [468] trunk/JavaBDD
|
From: <joe...@us...> - 2006-11-29 08:07:15
|
Revision: 468
http://svn.sourceforge.net/javabdd/?rev=468&view=rev
Author: joewhaley
Date: 2006-11-29 00:07:13 -0800 (Wed, 29 Nov 2006)
Log Message:
-----------
Improved ZDD support. load(), support(), quant methods now work.
Modified Paths:
--------------
trunk/JavaBDD/NQueens.java
trunk/JavaBDD/RubiksCube.java
trunk/JavaBDD/net/sf/javabdd/BDDDomain.java
trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
Modified: trunk/JavaBDD/NQueens.java
===================================================================
--- trunk/JavaBDD/NQueens.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/NQueens.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -58,7 +58,7 @@
}
if (B.varNum() < N * N) B.setVarNum(N * N);
- queen = B.one();
+ queen = B.universe();
int i, j;
@@ -108,7 +108,7 @@
}
static void build(int i, int j) {
- BDD a = B.one(), b = B.one(), c = B.one(), d = B.one();
+ BDD a = B.universe(), b = B.universe(), c = B.universe(), d = B.universe();
int k, l;
/* No one in the same column */
Modified: trunk/JavaBDD/RubiksCube.java
===================================================================
--- trunk/JavaBDD/RubiksCube.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/RubiksCube.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -159,7 +159,7 @@
}
static BDD buildInitial() {
- BDD b = bdd.one();
+ BDD b = bdd.universe();
for (int k=0; k<4; ++k) {
for (int i=0; i<n; ++i) {
b.andWith(bdd.getDomain(k*n + i).ithVar(k));
Modified: trunk/JavaBDD/net/sf/javabdd/BDDDomain.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -94,7 +94,7 @@
/* Encode V<=X-1. V is the variables in 'var' and X is the domain size */
BigInteger val = size().subtract(BigInteger.ONE);
- BDD d = factory.one();
+ BDD d = factory.universe();
int[] ivar = vars();
for (int n = 0; n < this.varNum(); n++) {
if (val.testBit(0))
@@ -128,7 +128,7 @@
BDDFactory bdd = getFactory();
if (value == 0L) {
- BDD result = bdd.one();
+ BDD result = bdd.universe();
int n;
for (n = 0; n < bits; n++) {
BDD b = bdd.ithVar(this.ivar[n]);
@@ -182,7 +182,7 @@
}
BDDFactory factory = getFactory();
- BDD e = factory.one();
+ BDD e = factory.universe();
int[] this_ivar = this.vars();
int[] that_ivar = that.vars();
@@ -226,7 +226,7 @@
}
BDDFactory factory = getFactory();
- BDD v = factory.one();
+ BDD v = factory.universe();
int[] ivar = this.vars();
for (int n = 0; n < ivar.length; n++) {
if (val.testBit(0))
@@ -257,7 +257,7 @@
BDD result = factory.zero();
int[] ivar = this.vars();
while (lo.compareTo(hi) <= 0) {
- BDD v = factory.one();
+ BDD v = factory.universe();
for (int n = ivar.length - 1; ; n--) {
if (lo.testBit(n)) {
v.andWith(factory.ithVar(ivar[n]));
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -84,6 +84,11 @@
return TestBDDFactory.init(nodenum, cachesize);
if (bddpackage.equals("typed"))
return TypedBDDFactory.init(nodenum, cachesize);
+ if (bddpackage.equals("zdd")) {
+ BDDFactory bdd = JFactory.init(nodenum, cachesize);
+ ((JFactory)bdd).ZDD = true;
+ return bdd;
+ }
} catch (LinkageError e) {
System.out.println("Could not load BDD package "+bddpackage+": "+e.getLocalizedMessage());
}
@@ -218,7 +223,7 @@
* <p>Compare to bdd_buildcube.</p>
*/
public BDD buildCube(int value, List/*<BDD>*/ variables) {
- BDD result = one();
+ BDD result = universe();
Iterator i = variables.iterator();
int z = 0;
while (i.hasNext()) {
@@ -240,7 +245,7 @@
* <p>Compare to bdd_ibuildcube./p>
*/
public BDD buildCube(int value, int[] variables) {
- BDD result = one();
+ BDD result = universe();
for (int z = 0; z < variables.length; z++, value >>= 1) {
BDD v;
if ((value & 0x1) != 0)
@@ -529,7 +534,7 @@
// Check for constant true / false
if (lh_nodenum == 0 && vnum == 0) {
int r = Integer.parseInt(readNext(ifile));
- return r == 0 ? zero() : one();
+ return r == 0 ? zero() : universe();
}
// Not actually used.
@@ -631,7 +636,7 @@
protected BDD loadhash_get(LoadHash[] lh_table, int lh_nodenum, int key) {
if (key < 0) return null;
if (key == 0) return zero();
- if (key == 1) return one();
+ if (key == 1) return universe();
int hash = lh_table[key % lh_nodenum].first;
@@ -1423,6 +1428,14 @@
}
}
+ if (isZDD()) {
+ // Need to rebuild varsets for existing domains.
+ for (n = 0; n < fdvarnum; n++) {
+ domain[n].var.free();
+ domain[n].var =
+ makeSet(domain[n].ivar);
+ }
+ }
for (n = 0; n < num; n++) {
domain[n + fdvarnum].var =
makeSet(domain[n + fdvarnum].ivar);
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -446,7 +446,7 @@
}
protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) {
- if (true || isZDD()) {
+ if (isZDD()) {
if (USE_FINALIZER)
return new IntZDDVarSetWithFinalizer(v);
else
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -67,7 +67,7 @@
});
}
- boolean ZDD = true;
+ boolean ZDD = false;
/**
* Implementation of BDDPairing used by JFactory.
@@ -1561,14 +1561,11 @@
return l;
if (ISZERO(l) || ISZERO(r))
return 0;
- if (ISONE(l))
- return r;
- if (ISONE(r))
- return l;
if (LEVEL(l) < LEVEL(r))
return zand_rec(LOW(l), r);
else if (LEVEL(l) > LEVEL(r))
return zand_rec(l, LOW(r));
+ _assert(!ISCONST(l) && !ISCONST(r));
entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
@@ -1811,6 +1808,14 @@
if (var < 2) /* Empty set */
return bdd_apply(l, r, opr);
+ if (ZDD) {
+ // TODO: A real ZDD implementation.
+ int x = bdd_addref(bdd_apply(l, r, opr));
+ int y = bdd_exist(x, var);
+ bdd_delref(x);
+ return y;
+ }
+
if (applycache == null) applycache = BddCacheI_init(cachesize);
if (appexcache == null) appexcache = BddCacheI_init(cachesize);
if (quantcache == null) quantcache = BddCacheI_init(cachesize);
@@ -2144,14 +2149,12 @@
if (INVARSET(LEVEL(r))) {
int r2 = READREF(2), r1 = READREF(1);
switch (applyop) {
- case bddop_and: res = ZDD ? zand_rec(r2, r1) : and_rec(r2, r1); break;
- case bddop_or: res = ZDD ? zor_rec(r2, r1) : or_rec(r2, r1); break;
+ 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 = ZDD
- ? zdd_makenode(LEVEL(r), READREF(2), READREF(1))
- : bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+ res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
}
POPREF(2);
@@ -2163,6 +2166,45 @@
return res;
}
+ int zquant_rec(int r) {
+ BddCacheDataI entry;
+ int res;
+
+ if (r < 2 || LEVEL(r) > quantlast)
+ return r;
+
+ entry = BddCache_lookupI(quantcache, QUANTHASH(r));
+ if (entry.a == r && entry.c == quantid) {
+ if (CACHESTATS)
+ cachestats.opHit++;
+ return entry.res;
+ }
+ if (CACHESTATS)
+ cachestats.opMiss++;
+
+ PUSHREF(zquant_rec(LOW(r)));
+ PUSHREF(zquant_rec(HIGH(r)));
+
+ if (INVARSET(LEVEL(r))) {
+ int r2 = READREF(2), r1 = READREF(1);
+ switch (applyop) {
+ case bddop_and: res = zand_rec(r2, r1); break;
+ case bddop_or: res = zor_rec(r2, r1); break;
+ default: throw new BDDException();
+ }
+ } else {
+ res = zdd_makenode(LEVEL(r), READREF(2), READREF(1));
+ }
+
+ POPREF(2);
+
+ entry.a = r;
+ entry.c = quantid;
+ entry.res = res;
+
+ return res;
+ }
+
int bdd_constrain(int f, int c) {
int res;
int numReorder = 1;
@@ -2706,7 +2748,10 @@
supportMin = LEVEL(r);
supportMax = supportMin;
- support_rec(r, supportSet);
+ if (ZDD)
+ zsupport_rec(r, 0, supportSet);
+ else
+ support_rec(r, supportSet);
bdd_unmark(r);
bdd_disable_reorder();
@@ -2715,7 +2760,7 @@
if (supportSet[n] == supportID) {
int tmp;
bdd_addref(res);
- tmp = bdd_makenode(n, 0, res);
+ tmp = makenode_impl(n, 0, res);
bdd_delref(res);
res = tmp;
}
@@ -2727,6 +2772,8 @@
void support_rec(int r, int[] support) {
+ _assert(!ZDD);
+
if (r < 2)
return;
@@ -2744,6 +2791,41 @@
support_rec(HIGH(r), support);
}
+ void zsupport_rec(int r, int lev, int[] support) {
+
+ _assert(ZDD);
+
+ if (!ISZERO(r)) {
+ while (lev != LEVEL(r)) {
+ if (lev > supportMax)
+ supportMax = lev;
+ support[lev++] = supportID;
+ }
+ }
+
+ if (r < 2)
+ return;
+
+ if (MARKED(r) || LOW(r) == INVALID_BDD)
+ return;
+
+ if (LOW(r) == HIGH(r)) {
+ SETMARK(r);
+ zsupport_rec(LOW(r), LEVEL(r)+1, support);
+ return;
+ }
+
+ support[LEVEL(r)] = supportID;
+
+ if (LEVEL(r) > supportMax)
+ supportMax = LEVEL(r);
+
+ SETMARK(r);
+
+ zsupport_rec(LOW(r), LEVEL(r)+1, support);
+ zsupport_rec(HIGH(r), LEVEL(r)+1, support);
+ }
+
int bdd_appall(int l, int r, int opr, int var) {
int res;
int numReorder = 1;
@@ -4952,6 +5034,15 @@
bdd_pairs_resize(oldbddvarnum, bddvarnum);
bdd_operator_varresize();
+ if (ZDD) {
+ System.out.println("Changed number of ZDD variables, all existing ZDDs are now invalid.");
+ // Need to rebuild varsets for existing domains.
+ for (int n = 0; n < fdvarnum; n++) {
+ domain[n].var.free();
+ domain[n].var = makeSet(domain[n].ivar);
+ }
+ }
+
bdd_enable_reorder();
return 0;
@@ -5888,7 +5979,6 @@
int next;
}
- // TODO: revisit for zdd
int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException {
int key, var, low, high, root = 0, n;
@@ -5908,6 +5998,12 @@
if (low < 0 || high < 0 || var < 0)
return bdd_error(BDD_FORMAT);
+ if (ZDD) {
+ // The terminal "1" in BDD means universal set.
+ if (low == 1) low = univ;
+ if (high == 1) high = univ;
+ }
+
root = bdd_addref(bdd_ite(bdd_ithvar(var), high, low));
loadhash_add(key, root);
@@ -5962,6 +6058,7 @@
return;
}
+ // TODO: revisit for ZDD
void bdd_save_rec(BufferedWriter out, int root) throws IOException {
if (root < 2)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
