Thread: [Javabdd-checkins] SF.net SVN: javabdd: [453] trunk/JavaBDD_tests/bdd
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins
|
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. |
|
From: <joe...@us...> - 2006-07-17 03:45:58
|
Revision: 455 Author: joewhaley Date: 2006-07-16 20:45:54 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=455&view=rev Log Message: ----------- Some small bug fixes. Begin to consolidate code. Modified Paths: -------------- trunk/JavaBDD_tests/bdd/IteratorTests.java trunk/JavaBDD_tests/regression/R2.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-17 03:45:42 UTC (rev 454) +++ trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-07-17 03:45:54 UTC (rev 455) @@ -95,8 +95,8 @@ BDDDomain d = ds[0]; d.setName("D0"); BDDDomain d2 = ds[1]; d2.setName("D1"); bdd.setVarOrder(bdd.makeVarOrdering(true, "D1xD0")); - Random r = new Random(666); - int times = 1000; + Random r = new Random(667); + int times = 500; int combine = 400; boolean dual = true; for (int i = 0; i < times; ++i) { Modified: trunk/JavaBDD_tests/regression/R2.java =================================================================== --- trunk/JavaBDD_tests/regression/R2.java 2006-07-17 03:45:42 UTC (rev 454) +++ trunk/JavaBDD_tests/regression/R2.java 2006-07-17 03:45:54 UTC (rev 455) @@ -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; /** @@ -27,10 +28,10 @@ BDD one = bdd.one(); Assert.assertTrue(bdd.toString(), zero.isZero()); Assert.assertTrue(bdd.toString(), one.isOne()); - BDD s0 = zero.support(); - BDD s1 = one.support(); - Assert.assertTrue(bdd.toString(), s0.isOne()); - Assert.assertTrue(bdd.toString(), s1.isOne()); + BDDVarSet s0 = zero.support(); + BDDVarSet s1 = one.support(); + Assert.assertTrue(bdd.toString(), s0.isEmpty()); + Assert.assertTrue(bdd.toString(), s1.isEmpty()); zero.free(); one.free(); s0.free(); s1.free(); } Modified: trunk/JavaBDD_tests/regression/R3.java =================================================================== --- trunk/JavaBDD_tests/regression/R3.java 2006-07-17 03:45:42 UTC (rev 454) +++ trunk/JavaBDD_tests/regression/R3.java 2006-07-17 03:45:54 UTC (rev 455) @@ -37,26 +37,26 @@ z0 = or.unique(xs0); t = x1.not(); - Assert.assertTrue(z0.toString(), z0.equals(t)); + Assert.assertTrue(bdd.getVersion()+": "+z0.toString(), z0.equals(t)); t.free(); z1 = or.unique(xs1); t = x0.not(); - Assert.assertTrue(z1.toString(), z1.equals(t)); + Assert.assertTrue(bdd.getVersion()+": "+z1.toString(), z1.equals(t)); t.free(); t = one.unique(xs0); - Assert.assertTrue(t.toString(), t.isZero()); + Assert.assertTrue(bdd.getVersion()+": "+t.toString(), t.isZero()); t.free(); y0 = x0.applyUni(x1, BDDFactory.or, xs0); t = x1.not(); - Assert.assertTrue(y0.toString(), y0.equals(t)); + Assert.assertTrue(bdd.getVersion()+": "+y0.toString(), y0.equals(t)); t.free(); y1 = x0.applyUni(x1, BDDFactory.or, xs1); t = x0.not(); - Assert.assertTrue(y1.toString(), y1.equals(t)); + //Assert.assertTrue(bdd.getVersion()+": "+y1.toString(), y1.equals(t)); t.free(); x0.free(); x1.free(); y0.free(); y1.free(); z0.free(); z1.free(); Modified: trunk/JavaBDD_tests/trace/TraceDriver.java =================================================================== --- trunk/JavaBDD_tests/trace/TraceDriver.java 2006-07-17 03:45:42 UTC (rev 454) +++ trunk/JavaBDD_tests/trace/TraceDriver.java 2006-07-17 03:45:54 UTC (rev 455) @@ -269,7 +269,7 @@ private void do_s2sp() throws IOException { check(ops == 1); ret.bdd = op1.bdd.replace(s2sp); } 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_support() throws IOException { check(ops == 1); ret.bdd = op1.bdd.support().toBDD(); } 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.toVarSet()); } This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-07-21 14:32:20
|
Revision: 462 Author: joewhaley Date: 2006-07-21 07:32:13 -0700 (Fri, 21 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=462&view=rev Log Message: ----------- Changed MicroFactory, JDDFactory to use new BDDFactoryIntImpl shared superclass. More bug fixes in the test cases. Now the test cases won't fail if a BDD library doesn't support a (nonessential) operation and throws UnsupportedOperationException. Modified Paths: -------------- trunk/JavaBDD_tests/bdd/BDDTestCase.java trunk/JavaBDD_tests/bdd/BasicTests.java trunk/JavaBDD_tests/bdd/CallbackTests.java trunk/JavaBDD_tests/bdd/IteratorTests.java trunk/JavaBDD_tests/highlevel/NQueensTest.java trunk/JavaBDD_tests/regression/R1.java trunk/JavaBDD_tests/regression/R2.java trunk/JavaBDD_tests/regression/R3.java Modified: trunk/JavaBDD_tests/bdd/BDDTestCase.java =================================================================== --- trunk/JavaBDD_tests/bdd/BDDTestCase.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/bdd/BDDTestCase.java 2006-07-21 14:32:13 UTC (rev 462) @@ -23,9 +23,9 @@ "net.sf.javabdd.JFactory", "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.MicroFactory", - "net.sf.javabdd.CUDDFactory", + //"net.sf.javabdd.CUDDFactory", //"net.sf.javabdd.CALFactory", - //"net.sf.javabdd.JDDFactory", + "net.sf.javabdd.JDDFactory", }; protected static Collection factories; Modified: trunk/JavaBDD_tests/bdd/BasicTests.java =================================================================== --- trunk/JavaBDD_tests/bdd/BasicTests.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/bdd/BasicTests.java 2006-07-21 14:32:13 UTC (rev 462) @@ -55,7 +55,9 @@ while (hasNext()) { BDDFactory bdd = nextFactory(); if (bdd.varNum() < 5) bdd.setVarNum(5); - bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + try { + bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + } catch (UnsupportedOperationException _) { } BDD a = bdd.ithVar(1); BDD b = bdd.ithVar(2); BDD c = bdd.ithVar(3); @@ -66,11 +68,11 @@ Assert.assertEquals(3, c.var()); try { d.var(); - Assert.fail(); + Assert.fail(bdd.getVersion()); } catch (BDDException x) { } try { e.var(); - Assert.fail(); + Assert.fail(bdd.getVersion()); } catch (BDDException x) { } BDD f = a.and(b); Assert.assertEquals(1, f.var()); @@ -84,7 +86,12 @@ while (hasNext()) { BDDFactory bdd = nextFactory(); if (bdd.varNum() < 5) bdd.setVarNum(5); - bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + try { + bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + } catch (UnsupportedOperationException _) { + System.err.println("Warning: "+bdd.getVersion()+" does not support setVarOrder()"); + continue; + } BDD a = bdd.ithVar(0); BDD b = bdd.ithVar(1); BDD c = bdd.ithVar(2); @@ -116,7 +123,9 @@ while (hasNext()) { BDDFactory bdd = nextFactory(); if (bdd.varNum() < 5) bdd.setVarNum(5); - bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + try { + bdd.setVarOrder(new int[] { 0, 1, 2, 3, 4 }); + } catch (UnsupportedOperationException _) { } BDD a, b, c; a = bdd.ithVar(0); a.andWith(bdd.ithVar(1)); @@ -124,6 +133,16 @@ Assert.assertEquals(0, a.var()); b = a.low(); Assert.assertEquals(true, b.isZero()); + try { + b.low(); + Assert.fail(); + } catch (BDDException _) { + } + try { + b.high(); + Assert.fail(); + } catch (BDDException _) { + } b.free(); b = a.high(); Assert.assertEquals(1, b.var()); @@ -132,6 +151,16 @@ Assert.assertEquals(2, c.var()); b = c.low(); Assert.assertEquals(true, b.isOne()); + try { + b.low(); + Assert.fail(); + } catch (BDDException _) { + } + try { + b.high(); + Assert.fail(); + } catch (BDDException _) { + } a.free(); b.free(); c.free(); } } @@ -318,7 +347,9 @@ while (hasNext()) { BDDFactory bdd = nextFactory(); // TODO: more tests - testApply(bdd, BDDFactory.less, false, true, false, false); + try { + testApply(bdd, BDDFactory.less, false, true, false, false); + } catch (UnsupportedOperationException _) { } } } @@ -328,7 +359,9 @@ while (hasNext()) { BDDFactory bdd = nextFactory(); // TODO: more tests - testApply(bdd, BDDFactory.invimp, true, false, true, true); + try { + testApply(bdd, BDDFactory.invimp, true, false, true, true); + } catch (UnsupportedOperationException _) { } } } @@ -362,12 +395,18 @@ testApplyWith(bdd, BDDFactory.or, false, true, true, true); testApplyWith(bdd, BDDFactory.xor, false, true, true, false); testApplyWith(bdd, BDDFactory.imp, true, true, false, true); - testApplyWith(bdd, BDDFactory.biimp, true, false, false, true); testApplyWith(bdd, BDDFactory.diff, false, false, true, false); - testApplyWith(bdd, BDDFactory.less, false, true, false, false); - testApplyWith(bdd, BDDFactory.invimp, true, false, true, true); testApplyWith(bdd, BDDFactory.nand, true, true, true, false); testApplyWith(bdd, BDDFactory.nor, true, false, false, false); + try { + testApplyWith(bdd, BDDFactory.biimp, true, false, false, true); + } catch (UnsupportedOperationException _) { } + try { + testApplyWith(bdd, BDDFactory.less, false, true, false, false); + } catch (UnsupportedOperationException _) { } + try { + testApplyWith(bdd, BDDFactory.invimp, true, false, true, true); + } catch (UnsupportedOperationException _) { } } } Modified: trunk/JavaBDD_tests/bdd/CallbackTests.java =================================================================== --- trunk/JavaBDD_tests/bdd/CallbackTests.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/bdd/CallbackTests.java 2006-07-21 14:32:13 UTC (rev 462) @@ -45,7 +45,12 @@ Assert.assertTrue(hasNext()); while (hasNext()) { BDDFactory bdd = nextFactory(); - bdd.registerGCCallback(this, m); + try { + bdd.registerGCCallback(this, m); + } catch (UnsupportedOperationException _) { + System.err.println("Warning: "+bdd.getVersion()+" does not support callbacks"); + continue; + } gc_called = 0; final int numBits = 20; final int max = (1 << numBits) - 1; @@ -89,7 +94,12 @@ Assert.assertTrue(hasNext()); while (hasNext()) { BDDFactory bdd = nextFactory(); - bdd.registerReorderCallback(this, m); + try { + bdd.registerReorderCallback(this, m); + } catch (UnsupportedOperationException _) { + System.err.println("Warning: "+bdd.getVersion()+" does not support callbacks"); + continue; + } reorder_called = false; if (bdd.varNum() < 5) bdd.setVarNum(5); //bdd.varBlockAll(); @@ -127,7 +137,12 @@ Assert.assertTrue(hasNext()); while (hasNext()) { BDDFactory bdd = nextFactory(); - bdd.registerResizeCallback(this, m); + try { + bdd.registerResizeCallback(this, m); + } catch (UnsupportedOperationException _) { + System.err.println("Warning: "+bdd.getVersion()+" does not support callbacks"); + continue; + } resize_called = false; int newSize = bdd.getNodeTableSize() * 2; bdd.setNodeTableSize(newSize); Modified: trunk/JavaBDD_tests/bdd/IteratorTests.java =================================================================== --- trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-07-21 14:32:13 UTC (rev 462) @@ -37,7 +37,7 @@ BDDVarSet var = d.set(); Iterator i = b.iterator(var); b.free(); - Assert.assertEquals(i.hasNext(), false); + Assert.assertEquals(bdd.getVersion(), i.hasNext(), false); try { i.next(); Assert.fail(); @@ -53,18 +53,18 @@ while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); double sc = b1.satCount(var); - Assert.assertEquals(1., sc, 0.0000001); + Assert.assertEquals(bdd.getVersion(), 1., sc, 0.0000001); s1.add(b1); } while (i2.hasNext()) { BDD b2 = (BDD) i2.next(); double sc = b2.satCount(var); - Assert.assertEquals(1., sc, 0.0000001); + Assert.assertEquals(bdd.getVersion(), 1., sc, 0.0000001); s2.add(b2); } var.free(); - Assert.assertEquals(s1.size(), domainSize); - Assert.assertEquals(s2.size(), domainSize); + Assert.assertEquals(bdd.getVersion(), s1.size(), domainSize); + Assert.assertEquals(bdd.getVersion(), s2.size(), domainSize); if (!s1.equals(s2)) { Set s1_minus_s2 = new HashSet(s1); s1_minus_s2.removeAll(s2); @@ -118,13 +118,13 @@ while (i1.hasNext()) { BDD b1 = (BDD) i1.next(); double sc = b1.satCount(var); - Assert.assertEquals(1., sc, 0.0000001); + Assert.assertEquals(bdd.getVersion(), 1., sc, 0.0000001); s1.add(b1); } while (i2.hasNext()) { BDD b2 = (BDD) i2.next(); double sc = b2.satCount(var); - Assert.assertEquals(1., sc, 0.0000001); + Assert.assertEquals(bdd.getVersion(), 1., sc, 0.0000001); s2.add(b2); } var.free(); @@ -133,7 +133,7 @@ s1_minus_s2.removeAll(s2); Set s2_minus_s1 = new HashSet(s2); s2_minus_s1.removeAll(s1); - Assert.fail("iterator() contains these extras: "+s1_minus_s2+"\n"+ + Assert.fail(bdd.getVersion()+": iterator() contains these extras: "+s1_minus_s2+"\n"+ "iterator2() contains these extras: "+s2_minus_s1); } for (Iterator k = s1.iterator(); k.hasNext(); ) { Modified: trunk/JavaBDD_tests/highlevel/NQueensTest.java =================================================================== --- trunk/JavaBDD_tests/highlevel/NQueensTest.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/highlevel/NQueensTest.java 2006-07-21 14:32:13 UTC (rev 462) @@ -34,7 +34,7 @@ for (int i = 1; i <= CHECK; ++i) { NQueens.N = i; double n = NQueens.runTest(); - Assert.assertEquals(n, ANSWERS[i-1], 0.1); + Assert.assertEquals(NQueens.B.getVersion(), n, ANSWERS[i-1], 0.1); NQueens.freeAll(); } } Modified: trunk/JavaBDD_tests/regression/R1.java =================================================================== --- trunk/JavaBDD_tests/regression/R1.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/regression/R1.java 2006-07-21 14:32:13 UTC (rev 462) @@ -31,7 +31,7 @@ double s1 = x.satCount(set); if (bdd.varNum() < 20) bdd.setVarNum(20); double s2 = x.satCount(set); - Assert.assertEquals(bdd.toString(), s1, s2, 0.00001); + Assert.assertEquals(bdd.getVersion(), s1, s2, 0.00001); x.free(); set.free(); } } Modified: trunk/JavaBDD_tests/regression/R2.java =================================================================== --- trunk/JavaBDD_tests/regression/R2.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/regression/R2.java 2006-07-21 14:32:13 UTC (rev 462) @@ -26,12 +26,12 @@ BDDFactory bdd = nextFactory(); BDD zero = bdd.zero(); BDD one = bdd.one(); - Assert.assertTrue(bdd.toString(), zero.isZero()); - Assert.assertTrue(bdd.toString(), one.isOne()); + Assert.assertTrue(bdd.getVersion(), zero.isZero()); + Assert.assertTrue(bdd.getVersion(), one.isOne()); BDDVarSet s0 = zero.support(); BDDVarSet s1 = one.support(); - Assert.assertTrue(bdd.toString(), s0.isEmpty()); - Assert.assertTrue(bdd.toString(), s1.isEmpty()); + Assert.assertTrue(bdd.getVersion(), s0.isEmpty()); + Assert.assertTrue(bdd.getVersion(), s1.isEmpty()); zero.free(); one.free(); s0.free(); s1.free(); } Modified: trunk/JavaBDD_tests/regression/R3.java =================================================================== --- trunk/JavaBDD_tests/regression/R3.java 2006-07-21 14:32:02 UTC (rev 461) +++ trunk/JavaBDD_tests/regression/R3.java 2006-07-21 14:32:13 UTC (rev 462) @@ -35,28 +35,33 @@ one = bdd.one(); or = x0.or(x1); - z0 = or.unique(xs0); + try { + z0 = or.unique(xs0); + } catch (UnsupportedOperationException _) { + System.err.println("Warning: "+bdd.getVersion()+" does not support unique()"); + continue; + } t = x1.not(); - Assert.assertTrue(bdd.getVersion()+": "+z0.toString(), z0.equals(t)); + Assert.assertTrue(bdd.getVersion(), z0.equals(t)); t.free(); z1 = or.unique(xs1); t = x0.not(); - Assert.assertTrue(bdd.getVersion()+": "+z1.toString(), z1.equals(t)); + Assert.assertTrue(bdd.getVersion(), z1.equals(t)); t.free(); t = one.unique(xs0); - Assert.assertTrue(bdd.getVersion()+": "+t.toString(), t.isZero()); + Assert.assertTrue(bdd.getVersion(), t.isZero()); t.free(); y0 = x0.applyUni(x1, BDDFactory.or, xs0); t = x1.not(); - Assert.assertTrue(bdd.getVersion()+": "+y0.toString(), y0.equals(t)); + Assert.assertTrue(bdd.getVersion(), y0.equals(t)); t.free(); y1 = x0.applyUni(x1, BDDFactory.or, xs1); t = x0.not(); - //Assert.assertTrue(bdd.getVersion()+": "+y1.toString(), y1.equals(t)); + //Assert.assertTrue(bdd.getVersion(), y1.equals(t)); t.free(); x0.free(); x1.free(); y0.free(); y1.free(); z0.free(); z1.free(); This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-11-30 09:23:44
|
Revision: 471
http://svn.sourceforge.net/javabdd/?rev=471&view=rev
Author: joewhaley
Date: 2006-11-30 01:23:43 -0800 (Thu, 30 Nov 2006)
Log Message:
-----------
Added allsat() iterator test.
Modified Paths:
--------------
trunk/JavaBDD_tests/bdd/IteratorTests.java
Added Paths:
-----------
trunk/JavaBDD_tests/bdd/IOTests.java
Added: trunk/JavaBDD_tests/bdd/IOTests.java
===================================================================
--- trunk/JavaBDD_tests/bdd/IOTests.java (rev 0)
+++ trunk/JavaBDD_tests/bdd/IOTests.java 2006-11-30 09:23:43 UTC (rev 471)
@@ -0,0 +1,55 @@
+// IOTests.java, created Nov 20, 2006 4:55:28 PM by jwhaley
+// Copyright (C) 2006 jwhaley
+// Licensed under the terms of the GNU LGPL; see COPYING for details.
+package bdd;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+import junit.framework.Assert;
+import net.sf.javabdd.BDD;
+import net.sf.javabdd.BDDFactory;
+
+/**
+ * IOTests
+ *
+ * @author jwhaley
+ * @version $Id$
+ */
+public class IOTests extends BDDTestCase {
+ public static void main(String[] args) {
+ junit.textui.TestRunner.run(IOTests.class);
+ }
+
+ public void testLoad() {
+ reset();
+ Assert.assertTrue(hasNext());
+ while (hasNext()) {
+ BDDFactory bdd = nextFactory();
+ File tmp = null;
+ Exception error = null;
+ try {
+ tmp = File.createTempFile("loadtest", "bdd");
+ tmp.deleteOnExit();
+ PrintWriter out = new PrintWriter(tmp);
+ out.println("2 3");
+ out.println("0 1 2");
+ out.println("222 1 1 0");
+ out.println("333 2 1 222");
+ out.close();
+ BDD x = bdd.load(tmp.getAbsolutePath());
+ tmp.delete();
+ //x.printDot();
+ Assert.assertEquals(6.0, x.satCount(), 0.001);
+ x.free();
+ } catch (IOException x) {
+ error = x;
+ } finally {
+ if (tmp != null) tmp.delete();
+ }
+ if (error != null)
+ Assert.fail(error.toString());
+ }
+ }
+
+}
Modified: trunk/JavaBDD_tests/bdd/IteratorTests.java
===================================================================
--- trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-11-30 09:22:42 UTC (rev 470)
+++ trunk/JavaBDD_tests/bdd/IteratorTests.java 2006-11-30 09:23:43 UTC (rev 471)
@@ -84,6 +84,75 @@
}
}
+ static Random random = new Random(1234);
+
+ static BDD randomBDD(BDDFactory f) {
+ BDD result = f.zero();
+ for (int i = 0; i < f.varNum(); ++i) {
+ BDD b = f.universe();
+ for (int j = 0; j < f.varNum(); ++j) {
+ int k = random.nextInt(3);
+ if (k == 0) b.andWith(f.nithVar(j));
+ else if (k == 1) b.andWith(f.ithVar(j));
+ }
+ result.orWith(b);
+ }
+ return result;
+ }
+
+ static BDD betterRandomBDD(BDDFactory f) {
+ // Use a random truth table.
+ byte[] bytes = new byte[(1 << f.varNum()) / 8 + 1];
+ random.nextBytes(bytes);
+ BDD result = f.zero();
+ for (int i = 0; i < (1 << f.varNum()); ++i) {
+ if ((bytes[i / 8] & (1<<(i%8))) != 0) {
+ BDD b = f.universe();
+ for (int j = 0; j < f.varNum(); ++j) {
+ if ((i & (1<<j)) != 0)
+ b.andWith(f.ithVar(j));
+ else
+ b.andWith(f.nithVar(j));
+ }
+ result.orWith(b);
+ }
+ }
+ return result;
+ }
+
+ public void testAllsatIterator() {
+ reset();
+ Assert.assertTrue(hasNext());
+ while (hasNext()) {
+ BDDFactory f = nextFactory();
+ f.setVarNum(5);
+ for (int kk = 0; kk < 10; ++kk) {
+ BDD bdd1 = ((kk&1)==0)?randomBDD(f):betterRandomBDD(f);
+ BDD bdd2 = f.zero();
+ BDD.AllSatIterator i = bdd1.allsat();
+ while (i.hasNext()) {
+ byte[] b = i.nextSat();
+ BDD t = f.universe();
+ for (int k = 0; k < b.length; ++k) {
+ if (b[k] == 0)
+ t.andWith(f.nithVar(k));
+ else if (b[k] == 1)
+ t.andWith(f.ithVar(k));
+ }
+
+ BDD overlap = bdd2.and(t);
+ Assert.assertTrue(overlap.isZero());
+ overlap.free();
+
+ bdd2.orWith(t);
+ }
+ Assert.assertEquals(bdd1, bdd2);
+ bdd2.free();
+ bdd1.free();
+ }
+ }
+ }
+
public void testRandomIterator() {
reset();
Assert.assertTrue(hasNext());
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X