[Javabdd-checkins] SF.net SVN: javabdd: [453] trunk/JavaBDD_tests/bdd
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [453] trunk/JavaBDD_tests/bdd
|
From: <joe...@us...> - 2006-07-16 21:50:19
|
Revision: 453 Author: joewhaley Date: 2006-07-16 14:50:14 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=453&view=rev Log Message: ----------- Update to add a new type, BDDVarSet. This replaces the use of raw BDDs for variable sets. Library users will have to update their code (sorry!) Also added preliminary (untested) code for ZDD support. Modified Paths: -------------- trunk/JavaBDD_tests/bdd/IteratorTests.java trunk/JavaBDD_tests/regression/R1.java trunk/JavaBDD_tests/regression/R3.java trunk/JavaBDD_tests/trace/TraceDriver.java Modified: trunk/JavaBDD_tests/bdd/IteratorTests.java =================================================================== --- trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-07-16 21:50:02 UTC (rev 452) +++ trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-07-16 21:50:14 UTC (rev 453) @@ -12,6 +12,7 @@ import net.sf.javabdd.BDD; import net.sf.javabdd.BDDDomain; import net.sf.javabdd.BDDFactory; +import net.sf.javabdd.BDDVarSet; /** * IteratorTests @@ -33,7 +34,7 @@ BDDDomain[] ds = bdd.extDomain(new int[] { domainSize }); BDDDomain d = ds[0]; BDD b = bdd.zero(); - BDD var = d.set(); + BDDVarSet var = d.set(); Iterator i = b.iterator(var); b.free(); Assert.assertEquals(i.hasNext(), false); @@ -107,8 +108,8 @@ if (dual) c.andWith(d2.ithVar(r.nextInt(domainSize))); b.orWith(c); } - BDD var = d.set(); - if (dual) var.andWith(d2.set()); + BDDVarSet var = d.set(); + if (dual) var.unionWith(d2.set()); Iterator i1 = b.iterator(var); Iterator i2 = new MyBDDIterator(b, var); b.free(); @@ -155,10 +156,10 @@ BDD orig; BDD b = null; - BDD myVar; + BDDVarSet myVar; BDD last = null; - MyBDDIterator(BDD dis, BDD var) { + MyBDDIterator(BDD dis, BDDVarSet var) { orig = dis; if (!dis.isZero()) { b = dis.id(); Modified: trunk/JavaBDD_tests/regression/R1.java =================================================================== --- trunk/JavaBDD_tests/regression/R1.java 2006-07-16 21:50:02 UTC (rev 452) +++ trunk/JavaBDD_tests/regression/R1.java 2006-07-16 21:50:14 UTC (rev 453) @@ -7,6 +7,7 @@ import net.sf.javabdd.BDD; import net.sf.javabdd.BDDDomain; import net.sf.javabdd.BDDFactory; +import net.sf.javabdd.BDDVarSet; import bdd.BDDTestCase; /** @@ -26,7 +27,7 @@ BDDFactory bdd = nextFactory(); BDDDomain d = bdd.extDomain(new int[] { 16 })[0]; BDD x = d.ithVar(6).orWith(d.ithVar(13)); - BDD set = d.set(); + BDDVarSet set = d.set(); double s1 = x.satCount(set); if (bdd.varNum() < 20) bdd.setVarNum(20); double s2 = x.satCount(set); Modified: trunk/JavaBDD_tests/regression/R3.java =================================================================== --- trunk/JavaBDD_tests/regression/R3.java 2006-07-16 21:50:02 UTC (rev 452) +++ trunk/JavaBDD_tests/regression/R3.java 2006-07-16 21:50:14 UTC (rev 453) @@ -6,6 +6,7 @@ import junit.framework.Assert; import net.sf.javabdd.BDD; import net.sf.javabdd.BDDFactory; +import net.sf.javabdd.BDDVarSet; import bdd.BDDTestCase; /** @@ -25,37 +26,41 @@ BDDFactory bdd = nextFactory(); BDD x0,x1,y0,y1,z0,z1,t,or,one; + BDDVarSet xs0,xs1; bdd.setVarNum(5); x0 = bdd.ithVar(0); x1 = bdd.ithVar(1); + xs0 = x0.toVarSet(); + xs1 = x1.toVarSet(); one = bdd.one(); or = x0.or(x1); - z0 = or.unique(x0); + z0 = or.unique(xs0); t = x1.not(); Assert.assertTrue(z0.toString(), z0.equals(t)); t.free(); - z1 = or.unique(x1); + z1 = or.unique(xs1); t = x0.not(); Assert.assertTrue(z1.toString(), z1.equals(t)); t.free(); - t = one.unique(x0); + t = one.unique(xs0); Assert.assertTrue(t.toString(), t.isZero()); t.free(); - y0 = x0.applyUni(x1, BDDFactory.or, x0); + y0 = x0.applyUni(x1, BDDFactory.or, xs0); t = x1.not(); Assert.assertTrue(y0.toString(), y0.equals(t)); t.free(); - y1 = x0.applyUni(x1, BDDFactory.or, x1); + y1 = x0.applyUni(x1, BDDFactory.or, xs1); t = x0.not(); Assert.assertTrue(y1.toString(), y1.equals(t)); t.free(); x0.free(); x1.free(); y0.free(); y1.free(); z0.free(); z1.free(); + xs0.free(); xs1.free(); or.free(); one.free(); } Modified: trunk/JavaBDD_tests/trace/TraceDriver.java =================================================================== --- trunk/JavaBDD_tests/trace/TraceDriver.java 2006-07-16 21:50:02 UTC (rev 452) +++ trunk/JavaBDD_tests/trace/TraceDriver.java 2006-07-16 21:50:14 UTC (rev 453) @@ -270,11 +270,11 @@ private void do_sp2s() throws IOException { check(ops == 1); ret.bdd = op1.bdd.replace(sp2s); } private void do_support() throws IOException { check(ops == 1); ret.bdd = op1.bdd.support(); } - private void do_exists() throws IOException { check(ops == 2); ret.bdd = op2.bdd.exist(op1.bdd); } + private void do_exists() throws IOException { check(ops == 2); ret.bdd = op2.bdd.exist(op1.bdd.toVarSet()); } - private void do_forall() throws IOException { check(ops == 2); ret.bdd = op2.bdd.forAll(op1.bdd); } + private void do_forall() throws IOException { check(ops == 2); ret.bdd = op2.bdd.forAll(op1.bdd.toVarSet()); } private void do_restrict() throws IOException { check(ops == 2); ret.bdd = op1.bdd.restrict(op2.bdd); } - private void do_relprod() throws IOException { check(ops == 3); ret.bdd = op2.bdd.relprod(op3.bdd, op1.bdd); } + private void do_relprod() throws IOException { check(ops == 3); ret.bdd = op2.bdd.relprod(op3.bdd, op1.bdd.toVarSet()); } This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
