[Javabdd-checkins] SF.net SVN: javabdd: [472] trunk/JavaBDD/net/sf/javabdd
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [472] trunk/JavaBDD/net/sf/javabdd
|
From: <joe...@us...> - 2006-12-03 10:32:29
|
Revision: 472
http://svn.sourceforge.net/javabdd/?rev=472&view=rev
Author: joewhaley
Date: 2006-12-03 02:32:26 -0800 (Sun, 03 Dec 2006)
Log Message:
-----------
For ZDD: Fixed toString() and an embarrassing bug in ithVar/setvarnum.
Updated TestBDDFactory to work with ZDDs and newer APIs.
Modified Paths:
--------------
trunk/JavaBDD/net/sf/javabdd/BDD.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -546,6 +546,11 @@
protected byte[] allsatProfile;
protected final boolean useLevel;
+ protected AllSatIterator(BDDFactory factory, boolean level) {
+ f = factory;
+ useLevel = level;
+ }
+
/**
* Constructs a satisfying-assignment iterator on the given BDD.
* next() returns a byte array indexed by BDD variable number.
@@ -1289,6 +1294,8 @@
public String toString() {
BDDFactory f = this.getFactory();
int[] set = new int[f.varNum()];
+ if (f.isZDD())
+ Arrays.fill(set, 1);
StringBuffer sb = new StringBuffer();
bdd_printset_rec(f, sb, this, set);
return sb.toString();
@@ -1316,17 +1323,34 @@
}
sb.append('>');
} else {
- set[f.var2Level(r.var())] = 1;
- BDD rl = r.low();
- bdd_printset_rec(f, sb, rl, set);
- rl.free();
-
- set[f.var2Level(r.var())] = 2;
- BDD rh = r.high();
- bdd_printset_rec(f, sb, rh, set);
- rh.free();
-
- set[f.var2Level(r.var())] = 0;
+ if (f.isZDD()) {
+ if (r.low().equals(r.high())) {
+ set[f.var2Level(r.var())] = 0;
+ } else {
+ BDD rl = r.low();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 2;
+ }
+ BDD rl = r.high();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 1;
+ } else {
+ set[f.var2Level(r.var())] = 1;
+ BDD rl = r.low();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 2;
+ BDD rh = r.high();
+ bdd_printset_rec(f, sb, rh, set);
+ rh.free();
+
+ set[f.var2Level(r.var())] = 0;
+ }
}
}
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -2943,12 +2943,12 @@
if (ISZERO(LOW(r))) {
int res = satone_rec(HIGH(r));
- int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+ int m = makenode_impl(LEVEL(r), BDDZERO, res);
PUSHREF(m);
return m;
} else {
int res = satone_rec(LOW(r));
- 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;
}
@@ -5003,13 +5003,22 @@
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);
+ int res2 = zdd_makenode(k, (k == bddvarnum)?0:res, res);
+ INCREF(res2);
+ DECREF(res);
+ res = res2;
+
+ int res_not2 = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not);
+ INCREF(res_not2);
+ DECREF(res_not);
+ res_not = res_not2;
+
+ if (bdv == bddvarnum) {
+ int univ2 = zdd_makenode(k, univ, univ);
+ INCREF(univ2);
+ DECREF(univ);
+ univ = univ2;
+ }
}
bddvarset[bddvarnum * 2] = res;
bddvarset[bddvarnum * 2 + 1] = res_not;
@@ -5040,7 +5049,7 @@
bdd_operator_varresize();
if (ZDD) {
- System.out.println("Changed number of ZDD variables, all existing ZDDs are now invalid.");
+ System.out.println("Changed number of ZDD variables to "+num+", all existing ZDDs are now invalid.");
// Need to rebuild varsets for existing domains.
for (int n = 0; n < fdvarnum; n++) {
domain[n].var.free();
Modified: trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -11,9 +11,11 @@
import java.math.BigInteger;
/**
- * <p>This BDD factory is used to test other BDD factories. It is a wrapper around
- * two BDD factories, and all operations are performed on both factories. It
- * throws an exception if the results from the two implementations do not match.</p>
+ * <p>
+ * This BDD factory is used to test other BDD factories. It is a wrapper around
+ * two BDD factories, and all operations are performed on both factories. It
+ * throws an exception if the results from the two implementations do not match.
+ * </p>
*
* @see net.sf.javabdd.BDDFactory
*
@@ -21,11 +23,11 @@
* @version $Id$
*/
public class TestBDDFactory extends BDDFactory {
-
BDDFactory f1, f2;
public TestBDDFactory(BDDFactory a, BDDFactory b) {
- f1 = a; f2 = b;
+ f1 = a;
+ f2 = b;
}
public static BDDFactory init(int nodenum, int cachesize) {
@@ -41,36 +43,34 @@
throw new InternalError(s);
}
}
-
+
public static final void assertSame(BDD b1, BDD b2, String s) {
if (!b1.toString().equals(b2.toString())) {
//if (b1.nodeCount() != b2.nodeCount()) {
- System.out.println("b1 = "+b1.nodeCount());
- System.out.println("b2 = "+b2.nodeCount());
- System.out.println("b1 = "+b1.toString());
- System.out.println("b2 = "+b2.toString());
+ System.out.println("b1 = " + b1.nodeCount());
+ System.out.println("b2 = " + b2.nodeCount());
+ System.out.println("b1 = " + b1.toString());
+ System.out.println("b2 = " + b2.toString());
throw new InternalError(s);
}
}
public static final void assertSame(boolean b, BDD b1, BDD b2, String s) {
if (!b) {
- System.err.println("b1 = "+b1);
- System.err.println("b2 = "+b2);
+ System.err.println("b1 = " + b1);
+ System.err.println("b2 = " + b2);
throw new InternalError(s);
}
}
-
+
public static final void assertSame(BDDVarSet b1, BDDVarSet b2, String s) {
assertSame(b1.toBDD(), b2.toBDD(), s);
}
-
+
public static final void assertSame(boolean b, BDDVarSet b1, BDDVarSet b2, String s) {
assertSame(b, b1.toBDD(), b2.toBDD(), s);
}
-
private class TestBDD extends BDD {
-
BDD b1, b2;
TestBDD(BDD a, BDD b) {
@@ -79,21 +79,27 @@
assertSame(a, b, "constructor");
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#toVarSet()
*/
public BDDVarSet toVarSet() {
return new TestBDDVarSet(b1.toVarSet(), b2.toVarSet());
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#isZero()
*/
public boolean isZero() {
@@ -103,7 +109,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#isOne()
*/
public boolean isOne() {
@@ -113,7 +121,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#var()
*/
public int var() {
@@ -123,7 +133,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#high()
*/
public BDD high() {
@@ -132,7 +144,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#low()
*/
public BDD low() {
@@ -141,7 +155,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#id()
*/
public BDD id() {
@@ -150,7 +166,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#not()
*/
public BDD not() {
@@ -159,133 +177,158 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD)
*/
public BDD ite(BDD thenBDD, BDD elseBDD) {
- BDD c1 = ((TestBDD)thenBDD).b1;
- BDD c2 = ((TestBDD)thenBDD).b2;
- BDD d1 = ((TestBDD)elseBDD).b1;
- BDD d2 = ((TestBDD)elseBDD).b2;
+ BDD c1 = ((TestBDD) thenBDD).b1;
+ BDD c2 = ((TestBDD) thenBDD).b2;
+ BDD d1 = ((TestBDD) elseBDD).b1;
+ BDD d2 = ((TestBDD) elseBDD).b2;
BDD r1 = b1.ite(c1, d1);
BDD r2 = b2.ite(c2, d2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDVarSet)
*/
public BDD relprod(BDD that, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet d1 = ((TestBDDVarSet)var).b1;
- BDDVarSet d2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet d1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet d2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.relprod(c1, d1);
BDD r2 = b2.relprod(c2, d2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int)
*/
public BDD compose(BDD g, int var) {
- BDD c1 = ((TestBDD)g).b1;
- BDD c2 = ((TestBDD)g).b2;
+ BDD c1 = ((TestBDD) g).b1;
+ BDD c2 = ((TestBDD) g).b2;
BDD r1 = b1.compose(c1, var);
BDD r2 = b2.compose(c2, var);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing)
*/
public BDD veccompose(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
BDD r1 = b1.veccompose(c1);
BDD r2 = b2.veccompose(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD)
*/
public BDD constrain(BDD that) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
BDD r1 = b1.constrain(c1);
BDD r2 = b2.constrain(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet)
*/
public BDD exist(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.exist(c1);
BDD r2 = b2.exist(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD)
*/
public BDD forAll(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.forAll(c1);
BDD r2 = b2.forAll(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD)
*/
public BDD unique(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.unique(c1);
BDD r2 = b2.unique(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD)
*/
public BDD restrict(BDD var) {
- BDD c1 = ((TestBDD)var).b1;
- BDD c2 = ((TestBDD)var).b2;
+ BDD c1 = ((TestBDD) var).b1;
+ BDD c2 = ((TestBDD) var).b2;
BDD r1 = b1.restrict(c1);
BDD r2 = b2.restrict(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD)
*/
public BDD restrictWith(BDD var) {
- BDD c1 = ((TestBDD)var).b1;
- BDD c2 = ((TestBDD)var).b2;
+ BDD c1 = ((TestBDD) var).b1;
+ BDD c2 = ((TestBDD) var).b2;
b1.restrictWith(c1);
b2.restrictWith(c2);
assertSame(b1, b2, "restrict");
return this;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet)
*/
public BDD simplify(BDDVarSet d) {
- BDDVarSet c1 = ((TestBDDVarSet)d).b1;
- BDDVarSet c2 = ((TestBDDVarSet)d).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) d).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) d).b2;
BDD r1 = b1.simplify(c1);
BDD r2 = b2.simplify(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#support()
*/
public BDDVarSet support() {
@@ -294,69 +337,86 @@
return new TestBDDVarSet(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp)
*/
public BDD apply(BDD that, BDDOp opr) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
BDD r1 = b1.apply(c1, opr);
BDD r2 = b2.apply(c2, opr);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp)
*/
public BDD applyWith(BDD that, BDDOp opr) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
b1.applyWith(c1, opr);
b2.applyWith(c2, opr);
- assertSame(b1, b2, "applyWith "+opr);
+ assertSame(b1, b2, "applyWith " + opr);
return this;
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyAll(c1, opr, e1);
BDD r2 = b2.applyAll(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyEx(c1, opr, e1);
BDD r2 = b2.applyEx(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyUni(c1, opr, e1);
BDD r2 = b2.applyUni(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satOne()
*/
public BDD satOne() {
@@ -365,7 +425,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#fullSatOne()
*/
public BDD fullSatOne() {
@@ -374,41 +436,49 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean)
*/
public BDD satOne(BDDVarSet var, boolean pol) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.satOne(c1, pol);
BDD r2 = b2.satOne(c2, pol);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing)
*/
public BDD replace(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
BDD r1 = b1.replace(c1);
BDD r2 = b2.replace(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing)
*/
public BDD replaceWith(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
b1.replaceWith(c1);
b2.replaceWith(c2);
assertSame(b1, b2, "replaceWith");
return this;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#printDot()
*/
public void printDot() {
@@ -416,17 +486,81 @@
b1.printDot();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#toString()
+ */
+ public String toString() {
+ // String already checked.
+ return b1.toString();
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#toStringWithDomains(net.sf.javabdd.BDD.BDDToString)
+ */
+ public String toStringWithDomains(BDDToString ts) {
+ String s1 = b1.toStringWithDomains(ts);
+ String s2 = b2.toStringWithDomains(ts);
+ assertSame(s1.equals(s2), "toStringWithDomains");
+ return s1;
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#allsat()
+ */
+ public AllSatIterator allsat() {
+ return new AllSatIterator(TestBDDFactory.this, false) {
+ AllSatIterator i1 = b1.allsat();
+ AllSatIterator i2 = b2.allsat();
+
+ public boolean hasNext() {
+ boolean r1 = i1.hasNext();
+ boolean r2 = i2.hasNext();
+ assertSame(r1 == r2, b1, b2, "allsat.hasNext");
+ return r1;
+ }
+
+ public byte[] nextSat() {
+ byte[] r1 = i1.nextSat();
+ byte[] r2 = i2.nextSat();
+ assertSame(Arrays.equals(r1, r2), b1, b2, "allsat.nextSat");
+ return r1;
+ }
+ };
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#scanAllVar()
+ */
+ public BigInteger[] scanAllVar() {
+ BigInteger[] r1 = b1.scanAllVar();
+ BigInteger[] r2 = b2.scanAllVar();
+ assertSame(Arrays.equals(r1, r2), b1, b2, "scanAllVar");
+ return r1;
+ }
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#nodeCount()
*/
public int nodeCount() {
int r1 = b1.nodeCount();
int r2 = b2.nodeCount();
- assertSame(r1 == r2, b1, b2, "nodeCount");
+ if (false) assertSame(r1 == r2, b1, b2, "nodeCount");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#pathCount()
*/
public double pathCount() {
@@ -436,7 +570,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satCount()
*/
public double satCount() {
@@ -446,32 +582,35 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#varProfile()
*/
public int[] varProfile() {
int[] r1 = b1.varProfile();
int[] r2 = b2.varProfile();
- assertSame(r1.length == r2.length, "varProfile");
- for (int i=0; i<r1.length; ++i) {
- assertSame(r1[i] == r2[i], "varProfile");
- }
+ assertSame(Arrays.equals(r1, r2), "varProfile");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD)
*/
public boolean equals(BDD that) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
boolean r1 = b1.equals(c1);
boolean r2 = b2.equals(c2);
assertSame(r1 == r2, b1, b2, "equals");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#hashCode()
*/
public int hashCode() {
@@ -480,7 +619,9 @@
return b2.hashCode();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#free()
*/
public void free() {
@@ -488,9 +629,7 @@
b2.free();
}
}
-
private class TestBDDVarSet extends BDDVarSet {
-
BDDVarSet b1, b2;
TestBDDVarSet(BDDVarSet a, BDDVarSet b) {
@@ -513,7 +652,7 @@
BDD r2 = b2.toBDD();
return new TestBDD(r1, r2);
}
-
+
public BDDVarSet id() {
BDDVarSet r1 = b1.id();
BDDVarSet r2 = b2.id();
@@ -521,16 +660,16 @@
}
public BDDVarSet intersect(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
BDDVarSet r1 = b1.intersect(c1);
BDDVarSet r2 = b2.intersect(c2);
return new TestBDDVarSet(r1, r2);
}
public BDDVarSet intersectWith(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
b1.intersectWith(c1);
b2.intersectWith(c2);
assertSame(b1, b2, "intersectWith");
@@ -566,8 +705,8 @@
}
public BDDVarSet union(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
BDDVarSet r1 = b1.union(c1);
BDDVarSet r2 = b2.union(c2);
return new TestBDDVarSet(r1, r2);
@@ -580,8 +719,8 @@
}
public BDDVarSet unionWith(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
b1.unionWith(c1);
b2.unionWith(c2);
assertSame(b1, b2, "unionWith");
@@ -594,45 +733,62 @@
assertSame(b1, b2, "unionWith");
return this;
}
-
+
public int hashCode() {
// TODO Compare!
b1.hashCode();
return b2.hashCode();
}
-
+
public boolean equals(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
boolean r1 = b1.equals(c1);
boolean r2 = b2.equals(c2);
assertSame(r1 == r2, b1, b2, "equals");
return r1;
}
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#zero()
*/
public BDD zero() {
return new TestBDD(f1.zero(), f2.zero());
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#one()
*/
public BDD one() {
return new TestBDD(f1.one(), f2.one());
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDDFactory#universe()
+ */
+ public BDD universe() {
+ return new TestBDD(f1.universe(), f2.universe());
+ }
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#emptySet()
*/
public BDDVarSet emptySet() {
return new TestBDDVarSet(f1.emptySet(), f2.emptySet());
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#initialize(int, int)
*/
protected void initialize(int nodenum, int cachesize) {
@@ -640,7 +796,9 @@
f2.initialize(nodenum, cachesize);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#isInitialized()
*/
public boolean isInitialized() {
@@ -650,7 +808,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#done()
*/
public void done() {
@@ -658,23 +818,29 @@
f2.done();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setError(int)
*/
public void setError(int code) {
f1.setError(code);
f2.setError(code);
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#clearError()
*/
public void clearError() {
f1.clearError();
f2.clearError();
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int)
*/
public int setMaxNodeNum(int size) {
@@ -684,7 +850,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double)
*/
public double setMinFreeNodes(double x) {
@@ -694,17 +862,21 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double)
*/
public double setIncreaseFactor(double x) {
double r1 = f1.setIncreaseFactor(x);
double r2 = f2.setIncreaseFactor(x);
- assertSame(r1 == r2, "setIncreaseFactor");
+ if (false) assertSame(r1 == r2, "setIncreaseFactor");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMaxIncrease(int)
*/
public int setMaxIncrease(int x) {
@@ -714,7 +886,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setCacheRatio(double)
*/
public double setCacheRatio(double x) {
@@ -724,17 +898,21 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setNodeTableSize(int)
*/
public int setNodeTableSize(int size) {
int r1 = f1.setNodeTableSize(size);
int r2 = f2.setNodeTableSize(size);
- assertSame(r1 == r2, "setNodeTableSize");
+ if (false) assertSame(r1 == r2, "setNodeTableSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setCacheSize(int)
*/
public int setCacheSize(int size) {
@@ -743,8 +921,10 @@
assertSame(r1 == r2, "setCacheSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#varNum()
*/
public int varNum() {
@@ -754,31 +934,39 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setVarNum(int)
*/
public int setVarNum(int num) {
int r1 = f1.setVarNum(num);
int r2 = f2.setVarNum(num);
- //assertSame(r1 == r2, "setVarNum");
+ // assertSame(r1 == r2, "setVarNum");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#ithVar(int)
*/
public BDD ithVar(int var) {
return new TestBDD(f1.ithVar(var), f2.ithVar(var));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#nithVar(int)
*/
public BDD nithVar(int var) {
return new TestBDD(f1.nithVar(var), f2.nithVar(var));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printAll()
*/
public void printAll() {
@@ -786,32 +974,40 @@
f1.printAll();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD)
*/
public void printTable(BDD b) {
// TODO Compare!
- BDD b1 = ((TestBDD)b).b1;
+ BDD b1 = ((TestBDD) b).b1;
f1.printTable(b1);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#load(java.lang.String)
*/
public BDD load(String filename) throws IOException {
return new TestBDD(f1.load(filename), f2.load(filename));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#save(java.lang.String, net.sf.javabdd.BDD)
*/
public void save(String filename, BDD var) throws IOException {
// TODO Compare!
- BDD b1 = ((TestBDD)var).b1;
+ BDD b1 = ((TestBDD) var).b1;
f1.save(filename, b1);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#level2Var(int)
*/
public int level2Var(int level) {
@@ -821,7 +1017,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#var2Level(int)
*/
public int var2Level(int var) {
@@ -831,7 +1029,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod)
*/
public void reorder(ReorderMethod m) {
@@ -839,7 +1039,9 @@
f2.reorder(m);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod)
*/
public void autoReorder(ReorderMethod method) {
@@ -847,15 +1049,20 @@
f2.autoReorder(method);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod,
+ * int)
*/
public void autoReorder(ReorderMethod method, int max) {
f1.autoReorder(method, max);
f2.autoReorder(method, max);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getReorderMethod()
*/
public ReorderMethod getReorderMethod() {
@@ -865,7 +1072,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getReorderTimes()
*/
public int getReorderTimes() {
@@ -875,7 +1084,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#disableReorder()
*/
public void disableReorder() {
@@ -883,7 +1094,9 @@
f2.disableReorder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#enableReorder()
*/
public void enableReorder() {
@@ -891,7 +1104,9 @@
f2.enableReorder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorderVerbose(int)
*/
public int reorderVerbose(int v) {
@@ -901,7 +1116,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
*/
public void setVarOrder(int[] neworder) {
@@ -909,7 +1126,9 @@
f2.setVarOrder(neworder);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean)
*/
public void addVarBlock(int first, int last, boolean fixed) {
@@ -917,7 +1136,9 @@
f2.addVarBlock(first, last, fixed);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#varBlockAll()
*/
public void varBlockAll() {
@@ -925,7 +1146,9 @@
f2.varBlockAll();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#clearVarBlocks()
*/
public void clearVarBlocks() {
@@ -933,7 +1156,9 @@
f2.clearVarBlocks();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printOrder()
*/
public void printOrder() {
@@ -941,14 +1166,16 @@
f1.printOrder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection)
*/
public int nodeCount(Collection r) {
LinkedList a1 = new LinkedList();
LinkedList a2 = new LinkedList();
- for (Iterator i=r.iterator(); i.hasNext();) {
- TestBDD b = (TestBDD)i.next();
+ for (Iterator i = r.iterator(); i.hasNext();) {
+ TestBDD b = (TestBDD) i.next();
a1.add(b.b1);
a2.add(b.b2);
}
@@ -958,7 +1185,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getNodeTableSize()
*/
public int getNodeTableSize() {
@@ -968,7 +1197,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getNodeNum()
*/
public int getNodeNum() {
@@ -978,7 +1209,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getCacheSize()
*/
public int getCacheSize() {
@@ -987,8 +1220,10 @@
assertSame(r1 == r2, "getCacheSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorderGain()
*/
public int reorderGain() {
@@ -998,7 +1233,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printStat()
*/
public void printStat() {
@@ -1006,7 +1243,9 @@
f1.printStat();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#makePair()
*/
public BDDPairing makePair() {
@@ -1015,7 +1254,9 @@
return new TestBDDPairing(p1, p2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#swapVar(int, int)
*/
public void swapVar(int v1, int v2) {
@@ -1023,30 +1264,34 @@
f2.swapVar(v1, v2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger)
*/
protected BDDDomain createDomain(int a, BigInteger b) {
return new TestBDDDomain(a, b);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#createBitVector(int)
*/
protected BDDBitVector createBitVector(int a) {
return new TestBDDBitVector(a);
}
-
private static class TestBDDPairing extends BDDPairing {
-
BDDPairing b1, b2;
-
+
TestBDDPairing(BDDPairing p1, BDDPairing p2) {
this.b1 = p1;
this.b2 = p2;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#set(int, int)
*/
public void set(int oldvar, int newvar) {
@@ -1054,7 +1299,9 @@
b2.set(oldvar, newvar);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
*/
public void set(int oldvar, BDD newvar) {
@@ -1062,53 +1309,53 @@
b2.set(oldvar, newvar);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#reset()
*/
public void reset() {
b1.reset();
b2.reset();
}
-
}
-
private class TestBDDDomain extends BDDDomain {
-
private TestBDDDomain(int a, BigInteger b) {
super(a, b);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDDomain#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
-
}
-
private class TestBDDBitVector extends BDDBitVector {
-
TestBDDBitVector(int a) {
super(a);
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDBitVector#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
-
}
-
public static final String REVISION = "$Revision$";
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getVersion()
*/
public String getVersion() {
- return "TestBDD "+REVISION.substring(11, REVISION.length()-2)+
- " of ("+f1.getVersion()+","+f2.getVersion()+")";
+ return "TestBDD " + REVISION.substring(11, REVISION.length() - 2)
+ + " of (" + f1.getVersion() + "," + f2.getVersion() + ")";
}
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
