javabdd-checkins Mailing List for JavaBDD (Page 2)
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins — CVS updates. High traffic.
You can subscribe to this list here.
| 2003 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(4) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2004 |
Jan
|
Feb
|
Mar
(6) |
Apr
(6) |
May
(4) |
Jun
(31) |
Jul
(64) |
Aug
(19) |
Sep
(28) |
Oct
(50) |
Nov
(25) |
Dec
|
| 2005 |
Jan
(44) |
Feb
(8) |
Mar
(2) |
Apr
(15) |
May
(48) |
Jun
(8) |
Jul
(7) |
Aug
|
Sep
(1) |
Oct
(3) |
Nov
|
Dec
|
| 2006 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(1) |
Jun
(2) |
Jul
(14) |
Aug
|
Sep
|
Oct
|
Nov
(6) |
Dec
(4) |
| 2007 |
Jan
|
Feb
|
Mar
(2) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
(1) |
Dec
|
| 2011 |
Jan
|
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
| 2019 |
Jan
|
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <joe...@us...> - 2006-07-17 15:54:29
|
Revision: 459 Author: joewhaley Date: 2006-07-17 08:54:24 -0700 (Mon, 17 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=459&view=rev Log Message: ----------- Remove unused field. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/JFactory.java Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 05:24:39 UTC (rev 458) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 15:54:24 UTC (rev 459) @@ -4920,8 +4920,6 @@ static final int BDD_REORDER_FREE = 0; static final int BDD_REORDER_FIXED = 1; - static long c1; - void bdd_reorder_done() { bddtree_del(vartree); bdd_operator_reset(); This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-07-17 05:24:43
|
Revision: 458 Author: joewhaley Date: 2006-07-16 22:24:39 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=458&view=rev Log Message: ----------- Add new CUDD to svn:ignore. Property Changed: ---------------- trunk/JavaBDD/ Property changes on: trunk/JavaBDD ___________________________________________________________________ Name: svn:ignore - buddy_jni.h cudd_jni.h cal_jni.h *.jar *.so *.dll *.jnilib *.ext *.lib *.o *.class buddy22 cudd-2.3.1 cudd-2.4.0 cal-2.1 target velocity.log + buddy_jni.h cudd_jni.h cal_jni.h *.jar *.so *.dll *.jnilib *.ext *.lib *.o *.class buddy22 cudd-2.3.1 cudd-2.4.0 cal-2.1 target velocity.log cudd-2.4.1 This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-07-17 05:20:09
|
Revision: 457 Author: joewhaley Date: 2006-07-16 22:20:06 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=457&view=rev Log Message: ----------- Upgraded to latest JavaBDD 2.0 and jwutil libraries. Added Paths: ----------- trunk/JavaBDD_tests/bdd/RangeTest.java Added: trunk/JavaBDD_tests/bdd/RangeTest.java =================================================================== --- trunk/JavaBDD_tests/bdd/RangeTest.java (rev 0) +++ trunk/JavaBDD_tests/bdd/RangeTest.java 2006-07-17 05:20:06 UTC (rev 457) @@ -0,0 +1,74 @@ +// RangeTest.java, created Jul 13, 2003 9:28:32 PM by John Whaley +// Copyright (C) 2003 John Whaley +// Licensed under the terms of the GNU LGPL; see COPYING for details. +package bdd; + +import java.util.Arrays; +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; +import net.sf.javabdd.BDD; +import net.sf.javabdd.BDDDomain; +import net.sf.javabdd.BDDFactory; + +/** + * RangeTest + * + * @author John Whaley + * @version $Id: RangeTest.java 2001 2004-10-16 03:03:56Z joewhaley $ + */ +public class RangeTest { + + public static void main(String[] args) throws IOException { + BDDFactory bdd = BDDFactory.init(1000000, 10000); + + BDDDomain[] domains = bdd.extDomain(new int[] { 10, 8 }); + int[] order = new int[bdd.varNum()]; + + BufferedReader in = new BufferedReader(new InputStreamReader(System.in)); + for (;;) { + buildRandomPermutation(order); + printPermutation(order); + bdd.setVarOrder(order); + System.out.print("Enter low: "); + int lo = Integer.parseInt(in.readLine()); + System.out.print("Enter high: "); + int hi = Integer.parseInt(in.readLine()); + for (int i=0; i<domains.length; ++i) { + BDD b = domains[i].varRange(lo, hi); + System.out.println(b.toStringWithDomains()+" = "+b.nodeCount()+" nodes"); + buildRandomPermutation(order); + printPermutation(order); + bdd.setVarOrder(order); + System.out.println(b.toStringWithDomains()+" = "+b.nodeCount()+" nodes"); + buildRandomPermutation(order); + printPermutation(order); + bdd.setVarOrder(order); + System.out.println(b.toStringWithDomains()+" = "+b.nodeCount()+" nodes"); + buildRandomPermutation(order); + printPermutation(order); + bdd.setVarOrder(order); + System.out.println(b.toStringWithDomains()+" = "+b.nodeCount()+" nodes"); + } + } + } + + static void printPermutation(int[] a) { + for (int i=0; i<a.length; ++i) { + System.out.print(a[i]+" "); + } + System.out.println(); + } + + static void buildRandomPermutation(int[] a) { + Arrays.fill(a, -1); + int n = 0; + java.util.Random r = new java.util.Random(); + while (n < a.length) { + int k = r.nextInt(a.length); + if (a[k] == -1) { + a[k] = n++; + } + } + } +} This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-07-17 05:20:01
|
Revision: 456 Author: joewhaley Date: 2006-07-16 22:19:54 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=456&view=rev Log Message: ----------- Upgraded to latest JavaBDD 2.0 and jwutil libraries. Modified Paths: -------------- trunk/JavaBDD/Makefile trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java Modified: trunk/JavaBDD/Makefile =================================================================== --- trunk/JavaBDD/Makefile 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/Makefile 2006-07-17 05:19:54 UTC (rev 456) @@ -12,7 +12,7 @@ BUDDY_SRC = buddy/src CUDD_SRC = cudd-2.4.1 CAL_SRC = cal-2.1 -VER = 1.0b2 +VER = 2.0 ifeq (${OS},Windows_NT) JDK_ROOT = $(firstword $(wildcard c:/j2sdk*)) Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-17 05:19:54 UTC (rev 456) @@ -646,95 +646,6 @@ } /** - * <p>Scans this BDD to find all occurrences of BDD variables and returns an - * array that contains the indices of the possible found BDD variables.</p> - * - * <p>Compare to bdd_scanset.</p> - * - * @return int[] containing indices of the possible found BDD variables - */ - public int[] scanSet() { - if (isOne() || isZero()) { - return null; - } - - int num = 0; - BDD n = this.id(); - do { - num++; - BDD n2 = n.high(); - n.free(); n = n2; - } while (!n.isZero() && !n.isOne()); - - int[] varset = new int[num]; - - num = 0; - n = this.id(); - do { - varset[num++] = n.var(); - BDD n2 = n.high(); - n.free(); n = n2; - } while (!n.isZero() && !n.isOne()); - - return varset; - } - - /** - * <p>Scans this BDD and copies the stored variables into a integer array of - * BDDDomain variable numbers. The numbers returned are guaranteed to be in - * ascending order.</p> - * - * <p>Compare to fdd_scanset.</p> - * - * @return int[] - */ - public int[] scanSetDomains() { - int[] fv; - int[] varset; - int fn; - int num, n, m, i; - - fv = this.scanSet(); - if (fv == null) - return null; - fn = fv.length; - - BDDFactory factory = getFactory(); - - for (n = 0, num = 0; n < factory.numberOfDomains(); n++) { - BDDDomain dom = factory.getDomain(n); - int[] ivar = dom.vars(); - boolean found = false; - for (m = 0; m < dom.varNum() && !found; m++) { - for (i = 0; i < fn && !found; i++) { - if (ivar[m] == fv[i]) { - num++; - found = true; - } - } - } - } - - varset = new int[num]; - - for (n = 0, num = 0; n < factory.numberOfDomains(); n++) { - BDDDomain dom = factory.getDomain(n); - int[] ivar = dom.vars(); - boolean found = false; - for (m = 0; m < dom.varNum() && !found; m++) { - for (i = 0; i < fn && !found; i++) { - if (ivar[m] == fv[i]) { - varset[num++] = n; - found = true; - } - } - } - } - - return varset; - } - - /** * <p>Finds one satisfying assignment of the domain <tt>d</tt> in this BDD * and returns that value.</p> * Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-17 05:19:54 UTC (rev 456) @@ -4,13 +4,13 @@ package net.sf.javabdd; import java.util.Arrays; +import java.util.BitSet; import java.util.Collection; import java.util.Iterator; import java.util.LinkedList; import java.util.List; import java.util.Map; import java.util.StringTokenizer; -import java.util.BitSet; import java.io.BufferedReader; import java.io.BufferedWriter; import java.io.FileReader; @@ -21,7 +21,6 @@ import java.lang.reflect.Modifier; import java.math.BigInteger; import java.security.AccessControlException; -import net.sf.javabdd.JFactory.BddTree; /** * <p>Interface for the creation and manipulation of BDDs.</p> Modified: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-17 05:19:54 UTC (rev 456) @@ -32,6 +32,58 @@ public abstract int[] toLevelArray(); /** + * <p>Scans this BDD and copies the stored variables into an array of BDDDomains. + * The domains returned are guaranteed to be in ascending order.</p> + * + * <p>Compare to fdd_scanset.</p> + * + * @return int[] + */ + public BDDDomain[] getDomains() { + int[] fv; + BDDDomain[] varset; + int fn; + int num, n, m, i; + + fv = this.toArray(); + fn = fv.length; + + BDDFactory factory = getFactory(); + + for (n = 0, num = 0; n < factory.numberOfDomains(); n++) { + BDDDomain dom = factory.getDomain(n); + int[] ivar = dom.vars(); + boolean found = false; + for (m = 0; m < dom.varNum() && !found; m++) { + for (i = 0; i < fn && !found; i++) { + if (ivar[m] == fv[i]) { + num++; + found = true; + } + } + } + } + + varset = new BDDDomain[num]; + + for (n = 0, num = 0; n < factory.numberOfDomains(); n++) { + BDDDomain dom = factory.getDomain(n); + int[] ivar = dom.vars(); + boolean found = false; + for (m = 0; m < dom.varNum() && !found; m++) { + for (i = 0; i < fn && !found; i++) { + if (ivar[m] == fv[i]) { + varset[num++] = dom; + found = true; + } + } + } + } + + return varset; + } + + /** * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet * and the given BDDVarSet. This constructs a new set; neither the current * nor the given BDDVarSet is modified.</p> Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-17 05:19:54 UTC (rev 456) @@ -11,7 +11,6 @@ import java.io.FileInputStream; import java.io.FileOutputStream; import java.io.IOException; -import java.math.BigInteger; /** * <p>An implementation of BDDFactory that relies on the BuDDy library through a Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 05:19:54 UTC (rev 456) @@ -16,8 +16,6 @@ import java.io.BufferedWriter; import java.io.IOException; import java.io.PrintStream; -import java.math.BigInteger; -import net.sf.javabdd.BDDFactory.BDDOp; /** * <p>This is a 100% Java implementation of the BDD factory. It is based on Modified: trunk/JavaBDD/net/sf/javabdd/MicroFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-17 05:19:54 UTC (rev 456) @@ -6008,14 +6008,6 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean) - */ - public void addVarBlock(BDD var, boolean fixed) { - int[] set = var.scanSet(); - bdd_addvarblock(set, fixed); - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean) */ public void addVarBlock(int first, int last, boolean fixed) { Modified: trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java 2006-07-17 03:45:54 UTC (rev 455) +++ trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java 2006-07-17 05:19:54 UTC (rev 456) @@ -1044,10 +1044,10 @@ } - private class TypedBDDVarSet extends BDDVarSet { + public class TypedBDDVarSet extends BDDVarSet { - BDDVarSet bdd; - Set dom; + final BDDVarSet bdd; + final Set dom; protected TypedBDDVarSet(BDDVarSet bdd, Set dom) { this.bdd = bdd; 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-17 03:45:51
|
Revision: 454 Author: joewhaley Date: 2006-07-16 20:45:42 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=454&view=rev Log Message: ----------- Some small bug fixes. Begin to consolidate code. Modified Paths: -------------- trunk/JavaBDD/Makefile trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDDomain.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/CALFactory.java trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java Added Paths: ----------- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java Modified: trunk/JavaBDD/Makefile =================================================================== --- trunk/JavaBDD/Makefile 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/Makefile 2006-07-17 03:45:42 UTC (rev 454) @@ -10,7 +10,7 @@ # BUDDY_SRC = buddy/src -CUDD_SRC = cudd-2.4.0 +CUDD_SRC = cudd-2.4.1 CAL_SRC = cal-2.1 VER = 1.0b2 @@ -19,6 +19,7 @@ CLASSPATH = .\;jdd.jar CC = gcc CFLAGS = -Wall -O2 -mno-cygwin $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) -DHAVE_SYS_RESOURCE_H=0 CAL_CFLAGS = $(CFLAGS) -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=1 -DHAVE_SYS_RESOURCE_H=0 -DHAVE_STDARG_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=0 OBJECT_OUTPUT_OPTION = -o$(space) LINK = dllwrap @@ -35,6 +36,7 @@ CAL_DLL_NAME = cal.dll ifeq (${CC},icl) # Intel Windows compiler CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND -DSMALL_NODES /O2 /Ob2 $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) -DHAVE_SYS_RESOURCE_H=0 CAL_CFLAGS = $(CFLAGS) -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=0 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=0 -DHAVE_SYS_RESOURCE_H=0 -DHAVE_STDARG_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=0 OBJECT_OUTPUT_OPTION = -Fo LINK = xilink @@ -43,6 +45,7 @@ endif ifeq (${CC},cl) # Microsoft Visual C++ compiler CFLAGS = -O2 $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) -DHAVE_SYS_RESOURCE_H=0 CAL_CFLAGS = $(CFLAGS) -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=0 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=0 -DHAVE_SYS_RESOURCE_H=0 -DHAVE_STDARG_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=0 OBJECT_OUTPUT_OPTION = -Fo LINK = cl @@ -55,6 +58,7 @@ CLASSPATH = .:jdd.jar CC = gcc CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -DSMALL_NODES -O2 -fomit-frame-pointer $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) CAL_CFLAGS = -O2 -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=1 -DHAVE_SYS_RESOURCE_H=1 -DHAVE_STDARG_H=1 -DHAVE_VARARGS_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=1 $(EXTRA_CFLAGS) OBJECT_OUTPUT_OPTION = -o$(space) LINK = $(CC) @@ -75,6 +79,7 @@ JDK_ROOT = $(firstword $(wildcard /usr/java/j*dk*)) CLASSPATH = .:jdd.jar CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -DSMALL_NODES -O2 -fomit-frame-pointer $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) CAL_CFLAGS = -O2 -DCLOCK_RESOLUTION=60 -DRLIMIT_DATA_DEFAULT=16777216 -DNDEBUG=1 -DSTDC_HEADERS=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_SYS_FILE_H=1 -DHAVE_SYS_STAT_H=1 -DHAVE_UNISTD_H=1 -DHAVE_ERRNO_H=1 -DHAVE_ASSERT_H=1 -DHAVE_SYS_WAIT_H=1 -DHAVE_PWD_H=1 -DHAVE_SYS_TYPES_H=1 -DHAVE_SYS_TIMES_H=1 -DHAVE_SYS_TIME_H=1 -DHAVE_SYS_RESOURCE_H=1 -DHAVE_STDARG_H=1 -DHAVE_VARARGS_H=1 -DSIZEOF_VOID_P=4 -DSIZEOF_INT=4 -DHAVE_IEEE_754=1 -DPAGE_SIZE=4096 -DLG_PAGE_SIZE=12 -DRETSIGTYPE=void -DHAVE_STRCOLL=1 -DHAVE_SYSCONF=1 -DHAVE_GETHOSTNAME=1 -DHAVE_STRCSPN=1 -DHAVE_STRERROR=1 -DHAVE_STRSPN=1 -DHAVE_STRSTR=1 -DHAVE_GETENV=1 -DHAVE_STRCHR=1 -DHAVE_GETRLIMIT=1 -DHAVE_GETRUSAGE=1 -DHAVE_VALLOC=1 $(EXTRA_CFLAGS) OBJECT_OUTPUT_OPTION = -o$(space) LINK = $(CC) @@ -91,13 +96,15 @@ CAL_DLL_NAME = libcal.so ifeq (${CC},icc) # Intel Linux compiler CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -DSMALL_NODES -O2 -Ob2 -ip $(EXTRA_CFLAGS) + CUDD_CFLAGS = $(CFLAGS) LINK = xild # Bug in icc link makes it ignore -static, so use xild # Include libirc for _intel_fast_memset LINKFLAGS = -static -shared /opt/intel_cc_80/lib/libirc.a endif ifeq (${CC},pathcc) # Pathscale compiler + # For 64-bit, eliminate -m32 and add -fPIC in CFLAGS. CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -DSMALL_NODES -m32 -O2 -fomit_frame_pointer $(EXTRA_CFLAGS) - # For 64-bit, eliminate -m32 and add -fPIC in CFLAGS. + CUDD_CFLAGS = $(CFLAGS) LINK = pathcc LINKFLAGS = -shared $(CFLAGS) endif @@ -135,15 +142,12 @@ CAL_CLASSFILE = net/sf/javabdd/CALFactory.class BUDDY_CLASSNAMES = net.sf.javabdd.BuDDyFactory \ net.sf.javabdd.BuDDyFactory\$$BuDDyBDD \ - net.sf.javabdd.BuDDyFactory\$$BuDDyBDDDomain \ net.sf.javabdd.BuDDyFactory\$$BuDDyBDDPairing CUDD_CLASSNAMES = net.sf.javabdd.CUDDFactory \ net.sf.javabdd.CUDDFactory\$$CUDDBDD \ - net.sf.javabdd.CUDDFactory\$$CUDDBDDDomain \ net.sf.javabdd.CUDDFactory\$$CUDDBDDPairing CAL_CLASSNAMES = net.sf.javabdd.CALFactory \ net.sf.javabdd.CALFactory\$$CALBDD \ - net.sf.javabdd.CALFactory\$$CALBDDDomain \ net.sf.javabdd.CALFactory\$$CALBDDPairing EXAMPLE_SOURCES = NQueens.java RubiksCube.java EXAMPLE_CLASSFILES = $(EXAMPLE_SOURCES:%.java=%.class) @@ -218,6 +222,9 @@ $(CAL_OBJS): %.o: %.c $(CC) $(CAL_CFLAGS) $(INCLUDES) -c $(OBJECT_OUTPUT_OPTION)$@ $< +$(CUDD_OBJS): %.o: %.c + $(CC) $(CUDD_CFLAGS) $(INCLUDES) -c $(OBJECT_OUTPUT_OPTION)$@ $< + .c.o: $(CC) $(CFLAGS) $(INCLUDES) -c $(OBJECT_OUTPUT_OPTION)$@ $< Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-17 03:45:42 UTC (rev 454) @@ -272,7 +272,9 @@ * @return the result of the relational product * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD relprod(BDD that, BDDVarSet var); + public BDD relprod(BDD that, BDDVarSet var) { + return applyEx(that, BDDFactory.and, var); + } /** * <p>Functional composition. Substitutes the variable var with the BDD that @@ -404,7 +406,7 @@ * * @return the variable support of this BDD */ - public abstract BDD support(); + public abstract BDDVarSet support(); /** * <p>Returns the result of applying the binary operator <tt>opr</tt> to the Modified: trunk/JavaBDD/net/sf/javabdd/BDDDomain.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-07-17 03:45:42 UTC (rev 454) @@ -315,29 +315,7 @@ } if (ivar.length == binsize) return binsize; - if (true) { - throw new BDDException("Can't add bits to domains, requested domain "+name+" upper limit "+range); - } - int[] new_ivar = new int[binsize]; - System.arraycopy(ivar, 0, new_ivar, 0, ivar.length); - BDDFactory factory = getFactory(); - for (int i = ivar.length; i < new_ivar.length; ++i) { - //System.out.println("Domain "+this+" Duplicating var#"+new_ivar[i-1]); - int newVar = factory.duplicateVar(new_ivar[i-1]); - factory.firstbddvar++; - new_ivar[i] = newVar; - //System.out.println("Domain "+this+" var#"+i+" = "+newVar); - } - this.ivar = new_ivar; - //System.out.println("Domain "+this+" old var = "+var); - this.var.free(); - BDDVarSet nvar = factory.emptySet(); - for (int i = 0; i < ivar.length; ++i) { - nvar.unionWith(ivar[i]); - } - this.var = nvar; - //System.out.println("Domain "+this+" new var = "+var); - return binsize; + throw new BDDException("Can't add bits to domains, requested domain "+name+" upper limit "+range); } /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -21,6 +21,7 @@ import java.lang.reflect.Modifier; import java.math.BigInteger; import java.security.AccessControlException; +import net.sf.javabdd.JFactory.BddTree; /** * <p>Interface for the creation and manipulation of BDDs.</p> @@ -987,14 +988,6 @@ */ public abstract void swapVar(int v1, int v2); - /** - * Duplicate a BDD variable. - * - * @param var var to duplicate - * @return index of new variable - */ - public abstract int duplicateVar(int var); - /**** VARIABLE BLOCKS ****/ /** @@ -1008,7 +1001,23 @@ * * <p>Compare to bdd_addvarblock.</p> */ - public abstract void addVarBlock(BDD var, boolean fixed); + public void addVarBlock(BDDVarSet var, boolean fixed) { + int[] v = var.toArray(); + int first, last; + if (v.length < 1) + throw new BDDException("Invalid parameter for addVarBlock"); + + first = last = v[0]; + + for (int n = 1; n < v.length; n++) { + if (v[n] < first) + first = v[n]; + if (v[n] > last) + last = v[n]; + } + + addVarBlock(first, last, fixed); + } // TODO: handle error code for addVarBlock. /** @@ -1317,7 +1326,11 @@ * <p>Implementors must implement this factory method to create BDDDomain * objects of the correct type.</p> */ - protected abstract BDDDomain createDomain(int a, BigInteger b); + protected BDDDomain createDomain(int a, BigInteger b) { + return new BDDDomain(a, b) { + public BDDFactory getFactory() { return BDDFactory.this; } + }; + } /** * <p>Creates a new finite domain block of the given size. Allocates @@ -1640,7 +1653,11 @@ * <p>Implementors must implement this factory method to create BDDBitVector * objects of the correct type.</p> */ - protected abstract BDDBitVector createBitVector(int a); + protected BDDBitVector createBitVector(int a) { + return new BDDBitVector(a) { + public BDDFactory getFactory() { return BDDFactory.this; } + }; + } /** * <p>Build a bit vector that is constant true or constant false.</p> Added: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java (rev 0) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-17 03:45:42 UTC (rev 454) @@ -0,0 +1,421 @@ +// BDDFactoryIntImpl.java, created Jul 16, 2006 2:59:55 PM by jwhaley +// Copyright (C) 2004-2006 John Whaley <jw...@al...> +// Licensed under the terms of the GNU LGPL; see COPYING for details. +package net.sf.javabdd; + +import java.util.Collection; +import java.util.Iterator; + +/** + * A shared superclass for BDD factories that refer to BDDs as ints. + * + * @author jwhaley + * @version $Id$ + */ +public abstract class BDDFactoryIntImpl extends BDDFactory { + + static final boolean USE_FINALIZER = false; + + protected abstract void addref_impl(int v); + protected abstract void delref_impl(int v); + protected abstract int zero_impl(); + protected abstract int one_impl(); + protected abstract int invalid_bdd_impl(); + protected abstract int var_impl(int v); + protected abstract int level_impl(int v); + protected abstract int low_impl(int v); + protected abstract int high_impl(int v); + protected abstract int ithVar_impl(int var); + protected abstract int nithVar_impl(int var); + + protected abstract int ite_impl(int v1, int v2, int v3); + protected abstract int apply_impl(int v1, int v2, BDDOp opr); + protected abstract int not_impl(int v1); + protected abstract int applyAll_impl(int v1, int v2, BDDOp opr, int v3); + protected abstract int applyEx_impl(int v1, int v2, BDDOp opr, int v3); + protected abstract int applyUni_impl(int v1, int v2, BDDOp opr, int v3); + protected abstract int compose_impl(int v1, int v2, int var); + protected abstract int constrain_impl(int v1, int v2); + protected abstract int restrict_impl(int v1, int v2); + protected abstract int simplify_impl(int v1, int v2); + protected abstract int support_impl(int v); + protected abstract int exist_impl(int v1, int v2); + protected abstract int forAll_impl(int v1, int v2); + protected abstract int unique_impl(int v1, int v2); + protected abstract int fullSatOne_impl(int v); + + protected abstract int replace_impl(int v, BDDPairing p); + protected abstract int veccompose_impl(int v, BDDPairing p); + + protected abstract int nodeCount_impl(int v); + protected abstract double pathCount_impl(int v); + protected abstract double satCount_impl(int v); + protected abstract int satOne_impl(int v); + protected abstract int satOne_impl2(int v1, int v2, boolean pol); + protected abstract int nodeCount_impl2(int[] v); + protected abstract int[] varProfile_impl(int v); + protected abstract void printTable_impl(int v); + + public class IntBDD extends BDD { + protected int v; + protected IntBDD(int v) { + this.v = v; + addref_impl(v); + } + public BDD apply(BDD that, BDDOp opr) { + return makeBDD(apply_impl(v, unwrap(that), opr)); + } + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { + return makeBDD(applyAll_impl(v, unwrap(that), opr, unwrap(var))); + } + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { + return makeBDD(applyEx_impl(v, unwrap(that), opr, unwrap(var))); + } + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { + return makeBDD(applyUni_impl(v, unwrap(that), opr, unwrap(var))); + } + public BDD applyWith(BDD that, BDDOp opr) { + int v2 = unwrap(that); + int v3 = apply_impl(v, v2, opr); + addref_impl(v3); + delref_impl(v); + if (this != that) + that.free(); + v = v3; + return this; + } + public BDD compose(BDD g, int var) { + return makeBDD(compose_impl(v, unwrap(g), var)); + } + public BDD constrain(BDD that) { + return makeBDD(constrain_impl(v, unwrap(that))); + } + public boolean equals(BDD that) { + return v == unwrap(that); + } + public BDD exist(BDDVarSet var) { + return makeBDD(exist_impl(v, unwrap(var))); + } + public BDD forAll(BDDVarSet var) { + return makeBDD(forAll_impl(v, unwrap(var))); + } + public void free() { + delref_impl(v); + v = invalid_bdd_impl(); + } + public BDD fullSatOne() { + return makeBDD(fullSatOne_impl(v)); + } + public BDDFactory getFactory() { + return BDDFactoryIntImpl.this; + } + public int hashCode() { + return v; + } + public BDD high() { + return makeBDD(high_impl(v)); + } + public BDD id() { + return makeBDD(v); + } + public boolean isOne() { + return v == one_impl(); + } + public boolean isZero() { + return v == zero_impl(); + } + public BDD ite(BDD thenBDD, BDD elseBDD) { + return makeBDD(ite_impl(v, unwrap(thenBDD), unwrap(elseBDD))); + } + public BDD low() { + return makeBDD(low_impl(v)); + } + public int level() { + return level_impl(v); + } + public int nodeCount() { + return nodeCount_impl(v); + } + public BDD not() { + return makeBDD(not_impl(v)); + } + public double pathCount() { + return pathCount_impl(v); + } + public BDD replace(BDDPairing pair) { + return makeBDD(replace_impl(v, pair)); + } + public BDD replaceWith(BDDPairing pair) { + int v3 = replace_impl(v, pair); + addref_impl(v3); + delref_impl(v); + v = v3; + return this; + } + public BDD restrict(BDD var) { + return makeBDD(restrict_impl(v, unwrap(var))); + } + public BDD restrictWith(BDD that) { + int v2 = unwrap(that); + int v3 = restrict_impl(v, v2); + addref_impl(v3); + delref_impl(v); + if (this != that) + that.free(); + v = v3; + return this; + } + public double satCount() { + return satCount_impl(v); + } + public BDD satOne() { + return makeBDD(satOne_impl(v)); + } + public BDD satOne(BDDVarSet var, boolean pol) { + return makeBDD(satOne_impl2(v, unwrap(var), pol)); + } + public BDD simplify(BDDVarSet d) { + return makeBDD(simplify_impl(v, unwrap(d))); + } + public BDDVarSet support() { + return makeBDDVarSet(support_impl(v)); + } + public BDD unique(BDDVarSet var) { + return makeBDD(unique_impl(v, unwrap(var))); + } + public int var() { + return var_impl(v); + } + public int[] varProfile() { + return varProfile_impl(v); + } + public BDD veccompose(BDDPairing pair) { + return makeBDD(veccompose_impl(v, pair)); + } + public BDDVarSet toVarSet() { + return makeBDDVarSet(v); + } + } + + public class IntBDDWithFinalizer extends IntBDD { + protected IntBDDWithFinalizer(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 IntBDD makeBDD(int v) { + if (USE_FINALIZER) + return new IntBDDWithFinalizer(v); + else + return new IntBDD(v); + } + + protected static final int unwrap(BDD b) { + return ((IntBDD) b).v; + } + + protected static final int[] unwrap(Collection/*<BDD>*/ c) { + int[] result = new int[c.size()]; + int k = -1; + for (Iterator i = c.iterator(); i.hasNext(); ) { + result[++k] = ((IntBDD) i.next()).v; + } + return result; + } + + public class IntBDDVarSet extends BDDVarSet { + int v; + private IntBDDVarSet(int v) { + this.v = v; + addref_impl(v); + } + public boolean equals(BDDVarSet that) { + return v == unwrap(that); + } + public void free() { + delref_impl(v); + v = invalid_bdd_impl(); + } + public BDDFactory getFactory() { + return BDDFactoryIntImpl.this; + } + public int hashCode() { + return v; + } + public BDDVarSet id() { + return makeBDDVarSet(v); + } + public BDDVarSet intersect(BDDVarSet b) { + return makeBDDVarSet(apply_impl(v, unwrap(b), or)); + } + public BDDVarSet intersectWith(BDDVarSet b) { + int v2 = unwrap(b); + int v3 = apply_impl(v, v2, or); + addref_impl(v3); + delref_impl(v); + if (this != b) + b.free(); + v = v3; + return this; + } + public boolean isEmpty() { + return v == one_impl(); + } + public int size() { + int result = 0; + for (int p = v; p != one_impl(); p = high_impl(p)) { + if (p == zero_impl()) + throw new BDDException("varset contains zero"); + ++result; + } + return result; + } + public int[] toArray() { + int[] result = new int[size()]; + int k = -1; + for (int p = v; p != one_impl(); p = high_impl(p)) { + result[++k] = var_impl(p); + } + return result; + } + public BDD toBDD() { + return makeBDD(v); + } + public int[] toLevelArray() { + int[] result = new int[size()]; + int k = -1; + for (int p = v; p != one_impl(); p = high_impl(p)) { + result[++k] = level_impl(p); + } + return result; + } + public BDDVarSet union(BDDVarSet b) { + return makeBDDVarSet(apply_impl(v, unwrap(b), and)); + } + public BDDVarSet union(int var) { + int v2 = ithVar_impl(var); + int v3 = apply_impl(v, v2, and); + delref_impl(v2); + return makeBDDVarSet(v3); + } + public BDDVarSet unionWith(BDDVarSet b) { + int v2 = unwrap(b); + int v3 = apply_impl(v, v2, and); + addref_impl(v3); + delref_impl(v); + if (this != b) + b.free(); + v = v3; + return this; + } + public BDDVarSet unionWith(int var) { + int v2 = ithVar_impl(var); + int v3 = apply_impl(v, v2, and); + addref_impl(v3); + delref_impl(v); + delref_impl(v2); + v = v3; + return this; + } + } + + public class IntBDDVarSetWithFinalizer extends IntBDDVarSet { + + protected IntBDDVarSetWithFinalizer(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(int v) { + if (USE_FINALIZER) + return new IntBDDVarSetWithFinalizer(v); + else + return new IntBDDVarSet(v); + } + + protected static final int unwrap(BDDVarSet b) { + return ((IntBDDVarSet) b).v; + } + + public class IntBDDBitVector extends BDDBitVector { + + protected IntBDDBitVector(int bitnum) { + super(bitnum); + } + + public BDDFactory getFactory() { + return BDDFactoryIntImpl.this; + } + + } + + public BDD ithVar(int var) { + return makeBDD(ithVar_impl(var)); + } + + public BDD nithVar(int var) { + return makeBDD(nithVar_impl(var)); + } + + public int nodeCount(Collection/*<BDD>*/ r) { + return nodeCount_impl2(unwrap(r)); + } + + public BDD one() { + return makeBDD(one_impl()); + } + + public BDDVarSet emptySet() { + return makeBDDVarSet(one_impl()); + } + + public void printTable(BDD b) { + printTable_impl(unwrap(b)); + } + + public BDD zero() { + return makeBDD(zero_impl()); + } + + protected int[] to_free = new int[8]; + protected int to_free_length = 0; + public void deferredFree(int v) { + synchronized(to_free) { + if (to_free_length == to_free.length) { + int[] t = new int[to_free.length * 2]; + System.arraycopy(to_free, 0, t, 0, to_free.length); + to_free = t; + } + to_free[to_free_length++] = v; + } + } + public void handleDeferredFree() { + synchronized(to_free) { + while (to_free_length > 0) { + delref_impl(to_free[--to_free_length]); + } + } + } +} Modified: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-17 03:45:42 UTC (rev 454) @@ -1,5 +1,5 @@ // BDDVarSet.java, created Jul 13, 2006 8:53:13 PM by jwhaley -// Copyright (C) 2004 John Whaley <jw...@al...> +// Copyright (C) 2004-2006 John Whaley <jw...@al...> // Licensed under the terms of the GNU LGPL; see COPYING for details. package net.sf.javabdd; Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -597,13 +597,6 @@ private static native void printStat0(); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createDomain(int, java.math.BigInteger) - */ - protected BDDDomain createDomain(int a, BigInteger b) { - return new BuDDyBDDDomain(a, b); - } - - /* (non-Javadoc) * An implementation of a BDD class, used by the BuDDy interface. */ private static class BuDDyBDD extends BDD { @@ -793,9 +786,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDD#support() */ - public BDD support() { + public BDDVarSet support() { int b = support0(_id); - return makeBDD(b); + return makeBDDVarSet(b); } private static native int support0(int b); @@ -1055,22 +1048,6 @@ } /* (non-Javadoc) - * An implementation of a BDDDomain, used by the BuDDy interface. - */ - private static class BuDDyBDDDomain extends BDDDomain { - - private BuDDyBDDDomain(int a, BigInteger b) { - super(a, b); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDDomain#getFactory() - */ - public BDDFactory getFactory() { return INSTANCE; } - - } - - /* (non-Javadoc) * An implementation of a BDDPairing, used by the BuDDy interface. */ private static class BuDDyBDDPairing extends BDDPairing { @@ -1150,29 +1127,6 @@ } - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createBitVector(int) - */ - protected BDDBitVector createBitVector(int a) { - return new BuDDyBDDBitVector(a); - } - - /* (non-Javadoc) - * An implementation of a BDDBitVector, used by the BuDDy interface. - */ - private static class BuDDyBDDBitVector extends BDDBitVector { - - private BuDDyBDDBitVector(int a) { - super(a); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDBitVector#getFactory() - */ - public BDDFactory getFactory() { return INSTANCE; } - - } - public static final String REVISION = "$Revision$"; /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/CALFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -594,9 +594,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDD#support() */ - public BDD support() { + public BDDVarSet support() { long b = support0(_ddnode_ptr); - return new CALBDD(b); + return new BDDVarSet.DefaultImpl(new CALBDD(b)); } private static native long support0(long b); Modified: trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -627,9 +627,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDD#support() */ - public BDD support() { + public BDDVarSet support() { long b = support0(_ddnode_ptr); - return new CUDDBDD(b); + return new BDDVarSet.DefaultImpl(new CUDDBDD(b)); } private static native long support0(long b); Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -219,9 +219,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDD#support() */ - public BDD support() { + public BDDVarSet support() { int x = _index; - return new bdd(bdd.support(x)); + return new BDDVarSet.DefaultImpl(new bdd(bdd.support(x))); } private int apply0(int x, int y, int z) { Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-16 21:50:14 UTC (rev 453) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 03:45:42 UTC (rev 454) @@ -17,6 +17,7 @@ import java.io.IOException; import java.io.PrintStream; import java.math.BigInteger; +import net.sf.javabdd.BDDFactory.BDDOp; /** * <p>This is a 100% Java implementation of the BDD factory. It is based on @@ -27,9 +28,13 @@ * @author John Whaley * @version $Id$ */ -public class JFactory extends BDDFactory { +public class JFactory extends BDDFactoryIntImpl { static final boolean VERIFY_ASSERTIONS = false; + public static boolean FLUSH_CACHE_ON_GC = true; + static final boolean CACHESTATS = false; + static final boolean SWAPCOUNT = false; + public static final String REVISION = "$Revision$"; public String getVersion() { @@ -47,402 +52,435 @@ return f; } - static final boolean USE_FINALIZER = false; - public static boolean FLUSH_CACHE_ON_GC = true; + public boolean ZDD = false; /** - * Private helper function to create BDD objects. + * Implementation of BDDPairing used by JFactory. */ - private bdd makeBDD(int id) { - bdd b; - if (USE_FINALIZER) { - b = new bddWithFinalizer(id); - if (false) { // can check for specific id's here. - System.out.println("Created "+System.identityHashCode(b)+" id "+id); - new Exception().printStackTrace(System.out); - } - } else { - b = new bdd(id); - } - return b; - } - - /** - * Private helper function to create BDD objects. - */ - private BDDVarSet makeBDDVarSet(int id) { - BDDVarSet b = new BDDVarSet.DefaultImpl(makeBDD(id)); - return b; - } - - /** - * Wrapper for the BDD index number used internally in the representation. - */ - private class bdd extends BDD { - int _index; + class bddPair extends BDDPairing { + int[] result; + int last; + int id; + bddPair next; - bdd(int index) { - this._index = index; - bdd_addref(_index); - } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#getFactory() + * @see net.sf.javabdd.BDDPairing#set(int, int) */ - public BDDFactory getFactory() { - return JFactory.this; + public void set(int oldvar, int newvar) { + bdd_setpair(this, oldvar, newvar); } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#toVarSet() + * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) */ - public BDDVarSet toVarSet() { - return makeBDDVarSet(_index); + public void set(int oldvar, BDD newvar) { + bdd_setbddpair(this, oldvar, unwrap(newvar)); } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isZero() + * @see net.sf.javabdd.BDDPairing#reset() */ - public boolean isZero() { - return _index == bddfalse; + public void reset() { + bdd_resetpair(this); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isOne() - */ - public boolean isOne() { - return _index == bddtrue; + + public String toString() { + StringBuffer sb = new StringBuffer(); + sb.append('{'); + boolean any = false; + for (int i = 0; i < result.length; ++i) { + if (result[i] != bdd_ithvar(bddlevel2var[i])) { + if (any) sb.append(", "); + any = true; + sb.append(bddlevel2var[i]); + sb.append('='); + BDD b = makeBDD(result[i]); + sb.append(b); + b.free(); + } + } + sb.append('}'); + return sb.toString(); } + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#makePair() + */ + public BDDPairing makePair() { + bddPair p = new bddPair(); + p.result = new int[bddvarnum]; + int n; + for (n = 0; n < bddvarnum; n++) + p.result[n] = bdd_ithvar(bddlevel2var[n]); - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#var() - */ - public int var() { - return bdd_var(_index); - } + p.id = update_pairsid(); + p.last = -1; - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#high() - */ - public BDD high() { - return makeBDD(HIGH(_index)); - } + bdd_register_pair(p); + return p; + } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#low() - */ - public BDD low() { - return makeBDD(LOW(_index)); - } + // Redirection functions. + + protected void addref_impl(int v) { bdd_addref(v); } + protected void delref_impl(int v) { bdd_delref(v); } + protected int zero_impl() { return BDDZERO; } + protected int one_impl() {return BDDONE; } + 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); } + protected int low_impl(int v) { return bdd_low(v); } + protected int high_impl(int v) { return bdd_high(v); } + protected int ithVar_impl(int var) { return bdd_ithvar(var); } + protected int nithVar_impl(int var) { return bdd_nithvar(var); } + + 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); } + protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appall(v1, v2, opr.id, v3); } + protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appex(v1, v2, opr.id, v3); } + protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appuni(v1, v2, opr.id, v3); } + protected int compose_impl(int v1, int v2, int var) { return bdd_compose(v1, v2, var); } + protected int constrain_impl(int v1, int v2) { return bdd_constrain(v1, v2); } + protected int restrict_impl(int v1, int v2) { return bdd_restrict(v1, v2); } + protected int simplify_impl(int v1, int v2) { return bdd_simplify(v1, v2); } + protected int support_impl(int v) { return bdd_support(v); } + protected int exist_impl(int v1, int v2) { return bdd_exist(v1, v2); } + protected int forAll_impl(int v1, int v2) { return bdd_forall(v1, v2); } + protected int unique_impl(int v1, int v2) { return bdd_unique(v1, v2); } + protected int fullSatOne_impl(int v) { return bdd_fullsatone(v); } + + protected int replace_impl(int v, BDDPairing p) { return bdd_replace(v, (bddPair)p); } + protected int veccompose_impl(int v, BDDPairing p) { return bdd_veccompose(v, (bddPair)p); } + + protected int nodeCount_impl(int v) { return bdd_nodecount(v); } + protected double pathCount_impl(int v) { return bdd_pathcount(v); } + protected double satCount_impl(int v) { return bdd_satcount(v); } + protected int satOne_impl(int v) { return bdd_satone(v); } + protected int satOne_impl2(int v1, int v2, boolean pol) { return bdd_satoneset(v1, v2, pol); } + protected int nodeCount_impl2(int[] v) { return bdd_anodecount(v); } + protected int[] varProfile_impl(int v) { return bdd_varprofile(v); } + protected void printTable_impl(int v) { bdd_fprinttable(System.out, v); } + + // More redirection functions. + + protected void initialize(int initnodesize, int cs) { bdd_init(initnodesize, cs); } + public void addVarBlock(int first, int last, boolean fixed) { bdd_intaddvarblock(first, last, fixed); } + public void varBlockAll() { bdd_varblockall(); } + public void clearVarBlocks() { bdd_clrvarblocks(); } + public void printOrder() { bdd_fprintorder(System.out); } + public int getNodeTableSize() { return bdd_getallocnum(); } + public int setNodeTableSize(int size) { return bdd_setallocnum(size); } + public int setCacheSize(int v) { return bdd_setcachesize(v); } + public boolean isZDD() { return ZDD; } + public boolean isInitialized() { return bddrunning; } + public void done() { bdd_done(); } + public void setError(int code) { bdderrorcond = code; } + public void clearError() { bdderrorcond = 0; } + public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); } + public double setMinFreeNodes(double x) { return bdd_setminfreenodes((int)(x * 100.)) / 100.; } + public int setMaxIncrease(int x) { return bdd_setmaxincrease(x); } + public double setIncreaseFactor(double x) { return bdd_setincreasefactor(x); } + public int getNodeNum() { return bdd_getnodenum(); } + public int getCacheSize() { return cachesize; } + public int reorderGain() { return bdd_reorder_gain(); } + public void printStat() { bdd_fprintstat(System.out); } + public double setCacheRatio(double x) { return bdd_setcacheratio((int)(x * 100)) / 100.; } + public int varNum() { return bdd_varnum(); } + public int setVarNum(int num) { return bdd_setvarnum(num); } + public void printAll() { bdd_fprintall(System.out); } + public BDD load(BufferedReader in, int[] translate) throws IOException { return makeBDD(bdd_load(in, translate)); } + public void save(BufferedWriter out, BDD b) throws IOException { bdd_save(out, unwrap(b)); } + public void setVarOrder(int[] neworder) { bdd_setvarorder(neworder); } + public int level2Var(int level) { return bddlevel2var[level]; } + public int var2Level(int var) { return bddvar2level[var]; } + public int getReorderTimes() { return bddreordertimes; } + public void disableReorder() { bdd_disable_reorder(); } + public void enableReorder() { bdd_enable_reorder(); } + public int reorderVerbose(int v) { return bdd_reorder_verbose(v); } + public void reorder(ReorderMethod m) { bdd_reorder(m.id); } + public void autoReorder(ReorderMethod method) { bdd_autoreorder(method.id); } + public void autoReorder(ReorderMethod method, int max) { bdd_autoreorder_times(method.id, max); } + public void swapVar(int v1, int v2) { bdd_swapvar(v1, v2); } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#id() - */ - public BDD id() { - return makeBDD(_index); + public ReorderMethod getReorderMethod() { + switch (bddreordermethod) { + case BDD_REORDER_NONE : + return REORDER_NONE; + case BDD_REORDER_WIN2 : + return REORDER_WIN2; + case BDD_REORDER_WIN2ITE : + return REORDER_WIN2ITE; + case BDD_REORDER_WIN3 : + return REORDER_WIN3; + case BDD_REORDER_WIN3ITE : + return REORDER_WIN3ITE; + case BDD_REORDER_SIFT : + return REORDER_SIFT; + case BDD_REORDER_SIFTITE : + return REORDER_SIFTITE; + case BDD_REORDER_RANDOM : + return REORDER_RANDOM; + default : + throw new BDDException(); } + } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#not() - */ - public BDD not() { - return makeBDD(bdd_not(_index)); - } + // Experimental functions. + + public void validateAll() { bdd_validate_all(); } + public void validateBDD(BDD b) { bdd_validate(unwrap(b)); } + + public JFactory cloneFactory() { + JFactory INSTANCE = new JFactory(); + if (applycache != null) + INSTANCE.applycache = this.applycache.copy(); + if (itecache != null) + INSTANCE.itecache = this.itecache.copy(); + if (quantcache != null) + INSTANCE.quantcache = this.quantcache.copy(); + INSTANCE.appexcache = this.appexcache.copy(); + if (replacecache != null) + INSTANCE.replacecache = this.replacecache.copy(); + if (misccache != null) + INSTANCE.misccache = this.misccache.copy(); + if (countcache != null) + INSTANCE.countcache = this.countcache.copy(); + // TODO: potential difference here (!) + INSTANCE.rng = new Random(); + INSTANCE.verbose = this.verbose; + INSTANCE.cachestats.copyFrom(this.cachestats); + + INSTANCE.bddrunning = this.bddrunning; + INSTANCE.bdderrorcond = this.bdderrorcond; + INSTANCE.bddnodesize = this.bddnodesize; + INSTANCE.bddmaxnodesize = this.bddmaxnodesize; + INSTANCE.bddmaxnodeincrease = this.bddmaxnodeincrease; + INSTANCE.bddfreepos = this.bddfreepos; + INSTANCE.bddfreenum = this.bddfreenum; + INSTANCE.bddproduced = this.bddproduced; + INSTANCE.bddvarnum = this.bddvarnum; - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD) - */ - public BDD ite(BDD thenBDD, BDD elseBDD) { - int x = _index; - int y = ((bdd) thenBDD)._index; - int z = ((bdd) elseBDD)._index; - return makeBDD(bdd_ite(x, y, z)); + INSTANCE.gbcollectnum = this.gbcollectnum; + INSTANCE.cachesize = this.cachesize; + INSTANCE.gbcclock = this.gbcclock; + INSTANCE.usednodes_nextreorder = this.usednodes_nextreorder; + + INSTANCE.bddrefstacktop = this.bddrefstacktop; + INSTANCE.bddresized = this.bddresized; + INSTANCE.minfreenodes = this.minfreenodes; + INSTANCE.bddnodes = new int[this.bddnodes.length]; + System.arraycopy(this.bddnodes, 0, INSTANCE.bddnodes, 0, this.bddnodes.length); + INSTANCE.bddrefstack = new int[this.bddrefstack.length]; + System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length); + INSTANCE.bddvar2level = new int[this.bddvar2level.length]; + System.arraycopy(this.bddvar2level, 0, INSTANCE.bddvar2level, 0, this.bddvar2level.length); + INSTANCE.bddlevel2var = new int[this.bddlevel2var.length]; + System.arraycopy(this.bddlevel2var, 0, INSTANCE.bddlevel2var, 0, this.bddlevel2var.length); + INSTANCE.bddvarset = new int[this.bddvarset.length]; + System.arraycopy(this.bddvarset, 0, INSTANCE.bddvarset, 0, this.bddvarset.length); + + INSTANCE.domain = new BDDDomain[this.domain.length]; + for (int i = 0; i < INSTANCE.domain.length; ++i) { + INSTANCE.domain[i] = INSTANCE.createDomain(i, this.domain[i].realsize); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) - */ - public BDD relprod(BDD that, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_relprod(x, y, z)); + return INSTANCE; + } + + /** + * Use this function to translate BDD's from a JavaFactory into its clone. + * This will only work immediately after cloneFactory() is called, and + * before any other BDD operations are performed. + * + * @param that BDD in old factory + * @return a BDD in the new factory + */ + public BDD copyNode(BDD that) { + return makeBDD(unwrap(that)); + } + + public void reverseAllDomains() { + reorder_init(); + for (int i = 0; i < fdvarnum; ++i) { + reverseDomain0(domain[i]); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int) - */ - public BDD compose(BDD g, int var) { - int x = _index; - int y = ((bdd) g)._index; - return makeBDD(bdd_compose(x, y, var)); + reorder_done(); + } + + public void reverseDomain(BDDDomain d) { + reorder_init(); + reverseDomain0(d); + reorder_done(); + } + + protected void reverseDomain0(BDDDomain d) { + int n = d.varNum(); + BddTree[] trees = new BddTree[n]; + int v = d.ivar[0]; + addVarBlock(v, v, true); + trees[0] = getBlock(vartree, v, v); + BddTree parent = getParent(trees[0]); + for (int i = 1; i < n; ++i) { + v = d.ivar[i]; + addVarBlock(v, v, true); + trees[i] = getBlock(vartree, v, v); + BddTree parent2 = getParent(trees[i]); + if (parent != parent2) { + throw new BDDException(); + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing) - */ - public BDD veccompose(BDDPairing pair) { - int x = _index; - return makeBDD(bdd_veccompose(x, ((bddPair) pair))); + for (int i = 0; i < n; ++i) { + for (int j = i + 1; j < n; ++j) { + blockdown(trees[i]); + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD) - */ - public BDD constrain(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - return makeBDD(bdd_constrain(x, y)); + BddTree newchild = trees[n-1]; + while (newchild.prev != null) newchild = newchild.prev; + if (parent == null) vartree = newchild; + else parent.nextlevel = newchild; + } + + public void setVarOrder(String ordering) { + List result = new LinkedList(); + int nDomains = numberOfDomains(); + StringTokenizer st = new StringTokenizer(ordering, "x_", true); + boolean[] done = new boolean[nDomains]; + List last = null; + for (int i=0; ; ++i) { + String s = st.nextToken(); + BDDDomain d; + for (int j=0; ; ++j) { + if (j == nDomains) + throw new BDDException("bad domain: "+s); + d = getDomain(j); + if (s.equals(d.getName())) break; + } + if (done[d.getIndex()]) + throw new BDDException("duplicate domain: "+s); + done[d.getIndex()] = true; + if (last != null) last.add(d); + if (st.hasMoreTokens()) { + s = st.nextToken(); + if (s.equals("x")) { + if (last == null) { + last = new LinkedList(); + last.add(d); + result.add(last); + } + } else if (s.equals("_")) { + if (last == null) { + result.add(d); + } + last = null; + } else { + throw new BDDException("bad token: "+s); + } + } else { + if (last == null) { + result.add(d); + } + break; + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) - */ - public BDD exist(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_exist(x, y)); + + for (int i=0; i<done.length; ++i) { + if (!done[i]) { + throw new BDDException("missing domain #"+i+": "+getDomain(i)); + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) - */ - public BDD forAll(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_forall(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) - */ - public BDD unique(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_unique(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD) - */ - public BDD restrict(BDD var) { - int x = _index; - int y = ((bdd) var)._index; - return makeBDD(bdd_restrict(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD) - */ - public BDD restrictWith(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - int a = bdd_restrict(x, y); - bdd_delref(x); - if (this != that) - that.free(); - bdd_addref(a); - this._index = a; - return this; - } - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) - */ - public BDD simplify(BDDVarSet d) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; - return makeBDD(bdd_simplify(x, y)); + setVarOrder(result); + } + + /** + * <p>Set the variable order to be the given list of domains.</p> + * + * @param domains domain order + */ + public void setVarOrder(List domains) { + BddTree[] my_vartree = new BddTree[fdvarnum]; + boolean[] interleaved = new boolean[fdvarnum]; + int k = 0; + for (Iterator i = domains.iterator(); i.hasNext(); ) { + Object o = i.next(); + Collection c; + if (o instanceof BDDDomain) c = Collections.singleton(o); + else c = (Collection) o; + for (Iterator j = c.iterator(); j.hasNext(); ) { + BDDDomain d = (BDDDomain) j.next(); + int low = d.ivar[0]; + int high = d.ivar[d.ivar.length-1]; + bdd_intaddvarblock(low, high, false); + BddTree b = getBlock(vartree, low, high); + my_vartree[k] = b; + interleaved[k] = j.hasNext(); + k++; + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#support() - */ - public BDD support() { - int x = _index; - return makeBDD(bdd_support(x)); + if (k <= 1) return; + BddTree parent = getParent(my_vartree[0]); + for (int i = 0; i < k; ++i) { + if (parent != getParent(my_vartree[i])) { + throw new BDDException("var block "+my_vartree[i].firstVar+".."+my_vartree[i].lastVar+" is in wrong place in tree"); + } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD apply(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - return makeBDD(bdd_apply(x, y, z)); + reorder_init(); + BddTree prev = null; boolean prev_interleaved = false; + for (int i = 0; i < k; ++i) { + BddTree t = my_vartree[i]; + while (t.prev != prev) { + blockdown(t.prev); + } + boolean inter = interleaved[i]; + if (prev_interleaved) { + blockinterleave(t.prev); + //++i; + prev = t.prev; + } else { + prev = t; + } + prev_interleaved = inter; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD applyWith(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = bdd_apply(x, y, z); - bdd_delref(x); - if (this != that) - that.free(); - bdd_addref(a); - this._index = a; - return this; + BddTree newchild = my_vartree[0]; + _assert(newchild.prev == null); + //while (newchild.prev != null) newchild = newchild.prev; + if (parent == null) vartree = newchild; + else parent.nextlevel = newchild; + reorder_done(); + } + + protected BddTree getParent(BddTree child) { + for (BddTree p = vartree; p != null; p = p.next) { + if (p == child) return null; + BddTree q = getParent(p, child); + if (q != null) return q; } - - /* (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) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_appall(x, y, z, a)); + throw new BDDException("Cannot find tree node "+child); + } + + protected BddTree getParent(BddTree parent, BddTree child) { + if (parent.nextlevel == null) return null; + for (BddTree p = parent.nextlevel; p != null; p = p.next) { + if (p == child) return parent; + BddTree q = getParent(p, child); + if (q != null) return q; } - - /* (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) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_appex(x, y, z, a)); - } - - /* (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) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return makeBDD(bdd_appuni(x, y, z, a)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne() - */ - public BDD satOne() { - int x = _index; - return makeBDD(bdd_satone(x)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#fullSatOne() - */ - public BDD fullSatOne() { - int x = _index; - return makeBDD(bdd_fullsatone(x)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) - */ - public BDD satOne(BDDVarSet var, boolean pol) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - int z = pol ? 1 : 0; - return makeBDD(bdd_satoneset(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) - */ - public BDD replace(BDDPairing pair) { - int x = _index; - return makeBDD(bdd_replace(x, ((bddPair) pair))); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing) - */ - public BDD replaceWith(BDDPairing pair) { - int x = _index; - int y = bdd_replace(x, ((bddPair) pair)); - bdd_delref(x); - bdd_addref(y); - _index = y; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#nodeCount() - */ - public int nodeCount() { - return bdd_nodecount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#pathCount() - */ - public double pathCount() { - return bdd_pathcount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount() - */ - public double satCount() { - return bdd_satcount(_index); - ... [truncated message content] |
|
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-16 21:50:09
|
Revision: 452 Author: joewhaley Date: 2006-07-16 14:50:02 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=452&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/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDDomain.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/CALFactory.java trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java trunk/JavaBDD/net/sf/javabdd/TryVarOrder.java trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java Added Paths: ----------- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-16 21:50:02 UTC (rev 452) @@ -18,15 +18,6 @@ * * <p>Use an implementation of BDDFactory to create BDD objects.</p> * - * <p>Some methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>, - * <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>, - * and <tt>satCount()</tt> take a 'set of variables' argument that is also of type BDD. - * Those BDDs must be a boolean function that represents the all-true minterm - * of the BDD variables of interest. They only serve to identify the set of - * variables of interest, however. For example, for a given BDDDomain, a BDD var set - * representing all BDD variables of that domain can be obtained - * by calling <tt>BDDDomain.set()</tt>.</p> - * * @see net.sf.javabdd.BDDFactory * @see net.sf.javabdd.BDDDomain#set() * @@ -57,6 +48,18 @@ public abstract boolean isOne(); /** + * <p>Converts this BDD to a new BDDVarSet.</p> + * + * <p>This BDD must be a boolean function that represents the all-true minterm + * of the BDD variables of interest.</p> + * + * @return the contents of this BDD as a new BDDVarSet + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(id()); + } + + /** * <p>Gets the variable labeling the BDD.</p> * * <p>Compare to bdd_var.</p> @@ -265,11 +268,11 @@ * <p>Compare to bdd_relprod.</p> * * @param that the BDD to 'and' with - * @param var the BDD to existentially quantify with + * @param var the BDDVarSet to existentially quantify with * @return the result of the relational product * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD relprod(BDD that, BDD var); + public abstract BDD relprod(BDD that, BDDVarSet var); /** * <p>Functional composition. Substitutes the variable var with the BDD that @@ -317,11 +320,11 @@ * * <p>Compare to bdd_exist.</p> * - * @param var BDD containing the variables to be existentially quantified + * @param var BDDVarSet containing the variables to be existentially quantified * @return the result of the existential quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD exist(BDD var); + public abstract BDD exist(BDDVarSet var); /** * <p>Universal quantification of variables. Removes all occurrences of this @@ -329,11 +332,11 @@ * * <p>Compare to bdd_forall.</p> * - * @param var BDD containing the variables to be universally quantified + * @param var BDDVarSet containing the variables to be universally quantified * @return the result of the universal quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD forAll(BDD var); + public abstract BDD forAll(BDDVarSet var); /** * <p>Unique quantification of variables. This type of quantification uses a @@ -342,11 +345,11 @@ * * <p>Compare to bdd_unique.</p> * - * @param var BDD containing the variables to be uniquely quantified + * @param var BDDVarSet containing the variables to be uniquely quantified * @return the result of the unique quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD unique(BDD var); + public abstract BDD unique(BDDVarSet var); /** * <p>Restrict a set of variables to constant values. Restricts the variables @@ -388,10 +391,10 @@ * * <p>Compare to bdd_simplify.</p> * - * @param d BDD containing the variables in the domain + * @param d BDDVarSet containing the variables in the domain * @return the result of the simplify operation */ - public abstract BDD simplify(BDD d); + public abstract BDD simplify(BDDVarSet d); /** * <p>Returns the variable support of this BDD. The support is all the @@ -436,11 +439,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs @@ -451,11 +454,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs @@ -466,11 +469,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one @@ -504,12 +507,12 @@ * * <p>Compare to bdd_satoneset.</p> * - * @param var BDD containing the set of variables that must be mentioned in the result + * @param var BDDVarSet containing the set of variables that must be mentioned in the result * @param pol the polarity of the result * @return one satisfying variable assignment * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD satOne(BDD var, boolean pol); + public abstract BDD satOne(BDDVarSet var, boolean pol); /** * <p>Finds all satisfying variable assignments.</p> @@ -557,7 +560,8 @@ useLevel = lev; if (r.isZero()) return; allsatProfile = new byte[f.varNum()]; - Arrays.fill(allsatProfile, (byte) -1); + if (!f.isZDD()) + Arrays.fill(allsatProfile, (byte) -1); loStack = new LinkedList(); hiStack = new LinkedList(); if (!r.isOne()) { @@ -808,7 +812,8 @@ * @param r BDD varset * @return array of levels */ - private static int[] varset2levels(BDD r) { + /* + private static int[] varset2levels(BDDVarSet r) { int size = 0; BDD p = r.id(); while (!p.isOne() && !p.isZero()) { @@ -830,6 +835,7 @@ p.free(); return result; } + */ /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns @@ -840,7 +846,7 @@ * @return an iteration of minterms * @see net.sf.javabdd.BDDDomain#set() */ - public BDDIterator iterator(final BDD var) { + public BDDIterator iterator(final BDDVarSet var) { return new BDDIterator(this, var); } @@ -872,32 +878,14 @@ * @param bdd BDD to iterate over * @param var variable set to mention in result */ - public BDDIterator(BDD bdd, BDD var) { + public BDDIterator(BDD bdd, BDDVarSet var) { initialBDD = bdd; f = bdd.getFactory(); i = new AllSatIterator(bdd, true); // init v[] - int n = 0; - BDD p = var.id(); - while (!p.isOne()) { - ++n; - BDD q = p.high(); - p.free(); - p = q; - } - p.free(); - v = new int[n]; - n = 0; - p = var.id(); - while (!p.isOne()) { - v[n++] = p.level(); - BDD q = p.high(); - p.free(); - p = q; - } - p.free(); + v = var.toLevelArray(); // init b[] - b = new boolean[n]; + b = new boolean[v.length]; gotoNext(); } @@ -1291,21 +1279,14 @@ * * @return the number of satisfying variable assignments */ - public double satCount(BDD varset) { + public double satCount(BDDVarSet varset) { BDDFactory factory = getFactory(); - double unused = factory.varNum(); - if (varset.isZero() || varset.isOne() || isZero()) /* empty set */ + if (varset.isEmpty() || isZero()) /* empty set */ return 0.; - BDD n = varset.id(); - do { - BDD n2 = n.high(); - n.free(); n = n2; - unused--; - } while (!n.isOne() && !n.isZero()); - n.free(); - + double unused = factory.varNum(); + unused -= varset.size(); unused = satCount() / Math.pow(2.0, unused); return unused >= 1.0 ? unused : 1.0; @@ -1330,7 +1311,7 @@ * * @return the logarithm of the number of satisfying variable assignments */ - public double logSatCount(BDD varset) { + public double logSatCount(BDDVarSet varset) { return Math.log(satCount(varset)); } Modified: trunk/JavaBDD/net/sf/javabdd/BDDDomain.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-07-16 21:50:02 UTC (rev 452) @@ -33,7 +33,7 @@ /* Variable indices for the variable set */ protected int[] ivar; /* The BDD variable set. Actually constructed in extDomain(), etc. */ - protected BDD var; + protected BDDVarSet var; /** * Default constructor. @@ -203,9 +203,9 @@ * * Compare to fdd_ithset. * - * @return BDD + * @return BDDVarSet */ - public BDD set() { + public BDDVarSet set() { return var.id(); } @@ -331,9 +331,9 @@ this.ivar = new_ivar; //System.out.println("Domain "+this+" old var = "+var); this.var.free(); - BDD nvar = factory.one(); + BDDVarSet nvar = factory.emptySet(); for (int i = 0; i < ivar.length; ++i) { - nvar.andWith(factory.ithVar(ivar[i])); + nvar.unionWith(ivar[i]); } this.var = nvar; //System.out.println("Domain "+this+" new var = "+var); @@ -375,7 +375,7 @@ * @see #ithVar(long) */ public BigInteger[] getVarIndices(BDD bdd, int max) { - BDD myvarset = set(); // can't use var here, must respect subclass a factory may provide + BDDVarSet myvarset = set(); // can't use var here, must respect subclass a factory may provide int n = (int) bdd.satCount(myvarset); if (max != -1 && n > max) n = max; Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -177,6 +177,11 @@ } /** + * <p>Returns true if this is a ZDD factory, false otherwise.</p> + */ + public boolean isZDD() { return false; } + + /** * <p>Get the constant false BDD.</p> * * <p>Compare to bdd_false.</p> @@ -191,6 +196,15 @@ public abstract BDD one(); /** + * <p>Get an empty BDDVarSet.</p> + * + * <p>Compare to bdd_true.</p> + */ + public BDDVarSet emptySet() { + return new BDDVarSet.DefaultImpl(one()); + } + + /** * <p>Build a cube from an array of variables.</p> * * <p>Compare to bdd_buildcube.</p> @@ -238,11 +252,11 @@ * * <p>Compare to bdd_makeset.</p> */ - public BDD makeSet(int[] varset) { - BDD res = one(); + public BDDVarSet makeSet(int[] varset) { + BDDVarSet res = emptySet(); int varnum = varset.length; - for (int v = varnum-1 ; v>=0 ; v--) { - res.andWith(ithVar(varset[v])); + for (int v = varnum-1; v >= 0; --v) { + res.unionWith(varset[v]); } return res; } @@ -711,17 +725,12 @@ root.free(); return 1; } - //Integer i = (Integer) visited.get(root); int i = root.hashCode(); - //if (i != null) { if (visited.get(i)) { root.free(); - //return i.intValue(); return i; } - //int v = visited.size() + 2; int v = i; - //visited.put(root, new Integer(v)); visited.set(i); BDD h = root.high(); @@ -735,7 +744,6 @@ int hi = save_rec(out, visited, h); - //out.write(v + " "); out.write(i + " "); out.write(rootvar + " "); out.write(lo + " "); @@ -1449,12 +1457,12 @@ * * <p>Compare to fdd_makeset.</p> */ - public BDD makeSet(BDDDomain[] v) { - BDD res = one(); + public BDDVarSet makeSet(BDDDomain[] v) { + BDDVarSet res = emptySet(); int n; for (n = 0; n < v.length; n++) { - res.andWith(v[n].set()); + res.unionWith(v[n].set()); } return res; Added: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java (rev 0) +++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-16 21:50:02 UTC (rev 452) @@ -0,0 +1,302 @@ +// BDDVarSet.java, created Jul 13, 2006 8:53:13 PM by jwhaley +// Copyright (C) 2004 John Whaley <jw...@al...> +// Licensed under the terms of the GNU LGPL; see COPYING for details. +package net.sf.javabdd; + +/** + * <p>Some BDD methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>, + * <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>, + * and <tt>satCount()</tt> take a BDDVarSet argument.</p> + * + * @author jwhaley + * @version $Id$ + */ +public abstract class BDDVarSet { + + /** + * <p>Returns the factory that created this BDDVarSet.</p> + * + * @return factory that created this BDDVarSet + */ + public abstract BDDFactory getFactory(); + + public abstract BDD toBDD(); + + public abstract BDDVarSet id(); + public abstract void free(); + + public abstract int size(); + public abstract boolean isEmpty(); + + public abstract int[] toArray(); + public abstract int[] toLevelArray(); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given BDDVarSet. This constructs a new set; neither the current + * nor the given BDDVarSet is modified.</p> + * + * @param b BDDVarSet to union with + * @return a new BDDVarSet that is the union of the two sets + */ + public abstract BDDVarSet union(BDDVarSet b); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given variable. This constructs a new set; the current BDDVarSet + * is not modified.</p> + * + * @param b variable to add to set + * @return a new BDDVarSet that includes the given variable + */ + public abstract BDDVarSet union(int var); + + /** + * <p>Modifies this BDDVarSet to include all of the vars in the given set. + * This modifies the current set in place and consumes the given set.</p> + * + * @param b BDDVarSet to union in + * @return this + */ + public abstract BDDVarSet unionWith(BDDVarSet b); + + /** + * <p>Modifies this BDDVarSet to include the given variable. This modifies + * the current set in place.</p> + * + * @param b variable to add to set + * @return this + */ + public abstract BDDVarSet unionWith(int var); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given BDDVarSet. This constructs a new set; neither the current + * nor the given BDDVarSet is modified.</p> + * + * @param b BDDVarSet to union with + * @return a new BDDVarSet that is the union of the two sets + */ + public abstract BDDVarSet intersect(BDDVarSet b); + + /** + * <p>Modifies this BDDVarSet to include all of the vars in the given set. + * This modifies the current set in place and consumes the given set.</p> + * + * @param b BDDVarSet to union in + * @return this + */ + public abstract BDDVarSet intersectWith(BDDVarSet b); + + /* (non-Javadoc) + * @see java.lang.Object#hashCode() + */ + public abstract int hashCode(); + + /** + * Returns true if the sets are equal. + * + * @param that other set + * @return true if the sets are equal + */ + public abstract boolean equals(BDDVarSet that); + + /* (non-Javadoc) + * @see java.lang.Object#equals(java.lang.Object) + */ + public final boolean equals(Object o) { + if (o instanceof BDDVarSet) + return equals((BDDVarSet) o); + return false; + } + + /** + * Default implementation of BDDVarSet based on BDDs. + * + * @author jwhaley + * @version $Id$ + */ + public static class DefaultImpl extends BDDVarSet { + + /** + * BDD representation of the set of variables. + * Treated like a linked list of variables. + */ + protected BDD b; + + /** + * Construct a BDDVarSet backed by the given BDD. + * Ownership of the given BDD is transferred to this BDDVarSet, + * so you should not touch it after construction! + * + * @param b BDD to use in constructing BDDVarSet + */ + public DefaultImpl(BDD b) { + this.b = b; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#free() + */ + public void free() { + if (b != null) { + b.free(); + b = null; + } + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#getFactory() + */ + public BDDFactory getFactory() { + return b.getFactory(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#id() + */ + public BDDVarSet id() { + return new DefaultImpl(b.id()); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#intersect(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet intersect(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + return new DefaultImpl(b.or(i.b)); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#intersectWith(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet intersectWith(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + b.orWith(i.b); i.b = null; + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#isEmpty() + */ + public boolean isEmpty() { + return b.isOne(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#size() + */ + public int size() { + int result = 0; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + ++result; + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toArray() + */ + public int[] toArray() { + int[] result = new int[size()]; + int i = -1; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + result[++i] = r.var(); + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toBDD() + */ + public BDD toBDD() { + return b.id(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toLevelArray() + */ + public int[] toLevelArray() { + int[] result = new int[size()]; + int i = -1; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + result[++i] = r.level(); + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#union(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet union(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + return new DefaultImpl(b.and(i.b)); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#union(int) + */ + public BDDVarSet union(int var) { + BDD ith = b.getFactory().ithVar(var); + DefaultImpl j = new DefaultImpl(b.and(ith)); + ith.free(); + return j; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#unionWith(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet unionWith(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + b.andWith(i.b); i.b = null; + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#unionWith(int) + */ + public BDDVarSet unionWith(int var) { + b.andWith(b.getFactory().ithVar(var)); + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#hashCode() + */ + public int hashCode() { + return b.hashCode(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#equals(net.sf.javabdd.BDDVarSet) + */ + public boolean equals(BDDVarSet s) { + if (s instanceof DefaultImpl) + return equals((DefaultImpl) s); + return false; + } + + public boolean equals(DefaultImpl s) { + return b.equals(s.b); + } + } + +} Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -127,6 +127,10 @@ return b; } + private static BDDVarSet.DefaultImpl makeBDDVarSet(int id) { + return new BDDVarSet.DefaultImpl(makeBDD(id)); + } + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#zero() */ @@ -176,9 +180,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#makeSet(int[]) */ - public BDD makeSet(int[] v) { + public BDDVarSet makeSet(int[] v) { int id = makeSet0(v); - return makeBDD(id); + return makeBDDVarSet(id); } private static native int makeSet0(int[] var); @@ -690,11 +694,11 @@ private static native int ite0(int b, int c, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = relprod0(_id, c._id, d._id); return makeBDD(b); } @@ -721,30 +725,30 @@ private static native int constrain0(int b, int c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD exist(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = exist0(_id, c._id); return makeBDD(b); } private static native int exist0(int b, int var); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD forAll(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = forAll0(_id, c._id); return makeBDD(b); } private static native int forAll0(int b, int var); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD unique(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = unique0(_id, c._id); return makeBDD(b); } @@ -777,10 +781,10 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { - BuDDyBDD c = (BuDDyBDD) d; + public BDD simplify(BDDVarSet d) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) d).b; int b = simplify0(_id, c._id); return makeBDD(b); } @@ -822,33 +826,33 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyAll0(_id, c._id, opr.id, d._id); return makeBDD(b); } private static native int applyAll0(int b, int c, int opr, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyEx0(_id, c._id, opr.id, d._id); return makeBDD(b); } private static native int applyEx0(int b, int c, int opr, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyUni0(_id, c._id, opr.id, d._id); return makeBDD(b); } @@ -873,10 +877,10 @@ private static native int fullSatOne0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD satOne(BDDVarSet var, boolean pol) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = satOne1(_id, c._id, pol?1:0); return makeBDD(b); } @@ -923,10 +927,10 @@ private static native double satCount0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#satCount(net.sf.javabdd.BDDVarSet) */ - public double satCount(BDD varset) { - BuDDyBDD c = (BuDDyBDD) varset; + public double satCount(BDDVarSet varset) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) varset).b; return satCount1(_id, c._id); } private static native double satCount1(int b, int c); @@ -940,10 +944,10 @@ private static native double logSatCount0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#logSatCount(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#logSatCount(net.sf.javabdd.BDDVarSet) */ - public double logSatCount(BDD varset) { - BuDDyBDD c = (BuDDyBDD) varset; + public double logSatCount(BDDVarSet varset) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) varset).b; return logSatCount1(_id, c._id); } private static native double logSatCount1(int b, int c); @@ -1016,6 +1020,13 @@ return this._id; } + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return makeBDDVarSet(this._id); + } + } private static class BuDDyBDDWithFinalizer extends BuDDyBDD { Modified: trunk/JavaBDD/net/sf/javabdd/CALFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -505,11 +505,11 @@ private static native long ite0(long b, long c, long d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { CALBDD c = (CALBDD) that; - CALBDD d = (CALBDD) var; + CALBDD d = (CALBDD) ((BDDVarSet.DefaultImpl) var).b; long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr); return new CALBDD(b); } @@ -534,25 +534,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -584,9 +584,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -627,25 +627,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -668,9 +668,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -787,6 +787,10 @@ return (int) this._ddnode_ptr; } + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new CALBDD(this._ddnode_ptr)); + } + } /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -534,11 +534,11 @@ private static native long ite0(long b, long c, long d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { CUDDBDD c = (CUDDBDD) that; - CUDDBDD d = (CUDDBDD) var; + CUDDBDD d = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr); return new CUDDBDD(b); } @@ -563,29 +563,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { - CUDDBDD c = (CUDDBDD) var; + public BDD exist(BDDVarSet var) { + CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = exist0(_ddnode_ptr, c._ddnode_ptr); return new CUDDBDD(b); } private static native long exist0(long b, long c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { - CUDDBDD c = (CUDDBDD) var; + public BDD forAll(BDDVarSet var) { + CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = forAll0(_ddnode_ptr, c._ddnode_ptr); return new CUDDBDD(b); } private static native long forAll0(long b, long c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -617,9 +617,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -660,25 +660,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -701,9 +701,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -819,6 +819,13 @@ return (int) this._ddnode_ptr; } + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new CUDDBDD(this._ddnode_ptr)); + } + } /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java 2006-07-16 21:50:02 UTC (rev 452) @@ -24,7 +24,7 @@ boolean newbdd = true; BDD b1 = null; BDD b2 = null; - BDD b3 = null; + BDDVarSet b3 = null; String filename0 = "fbo.bi"; String filename1 = "fbo.1"; @@ -59,7 +59,7 @@ this.DELAY_TIME = delayTime; } - public void init(BDD b1, BDD b2, BDD dom, BDDFactory.BDDOp op) throws IOException { + public void init(BDD b1, BDD b2, BDDVarSet dom, BDDFactory.BDDOp op) throws IOException { this.op = op; f0 = File.createTempFile("fbo", "a"); filename0 = f0.getAbsolutePath(); @@ -77,7 +77,7 @@ writeBDDConfig(b1.getFactory(), filename0); b1.getFactory().save(filename1, b1); b2.getFactory().save(filename2, b2); - dom.getFactory().save(filename3, dom); + dom.getFactory().save(filename3, dom.toBDD()); //System.out.println("done."); } @@ -167,7 +167,7 @@ if (newbdd) { b1 = bdd.load(filename1); b2 = bdd.load(filename2); - b3 = bdd.load(filename3); + b3 = bdd.load(filename3).toVarSet(); newbdd = false; } long t = System.currentTimeMillis(); Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -6,6 +6,7 @@ import java.util.Collection; import java.math.BigInteger; + /** * JDDFactory * @@ -119,12 +120,12 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; - int z = ((bdd) var)._index; + int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.relProd(x, y, z)); } @@ -155,29 +156,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.exists(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.forall(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return null; // todo. } @@ -207,11 +208,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { int x = _index; - int y = ((bdd) d)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; return new bdd(bdd.simplify(x, y)); } @@ -267,13 +268,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; // todo: combine. int r = apply0(x, y, z); bdd.ref(r); @@ -283,13 +284,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; // todo: combine. int r = apply0(x, y, z); bdd.ref(r); @@ -299,13 +300,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; throw new BDDException(); // todo. } @@ -399,9 +400,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -419,6 +420,13 @@ public int[] varProfile() { throw new BDDException(); } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new bdd(_index)); + } } Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -68,6 +68,14 @@ } /** + * Private helper function to create BDD objects. + */ + private BDDVarSet makeBDDVarSet(int id) { + BDDVarSet b = new BDDVarSet.DefaultImpl(makeBDD(id)); + return b; + } + + /** * Wrapper for the BDD index number used internally in the representation. */ private class bdd extends BDD { @@ -86,6 +94,13 @@ } /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return makeBDDVarSet(_index); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDD#isZero() */ public boolean isZero() { @@ -145,12 +160,12 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; - int z = ((bdd) var)._index; + int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_relprod(x, y, z)); } @@ -181,29 +196,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_exist(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_forall(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_unique(x, y)); } @@ -232,11 +247,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { int x = _index; - int y = ((bdd) d)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; return makeBDD(bdd_simplify(x, y)); } @@ -275,35 +290,35 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appall(x, y, z, a)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appex(x, y, z, a)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @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, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appuni(x, y, z, a)); } @@ -324,11 +339,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; int z = pol ? 1 : 0; return makeBDD(bdd_satoneset(x, y, z)); } @@ -649,37 +664,27 @@ static final int BDD_MEMORY = (-1); /* Out of memory */ static final int BDD_VAR = (-2); /* Unknown variable */ - static final int BDD_RANGE = (-3); - /* Variable value out of range (not in domain) */ - static final int BDD_DEREF = (-4); - /* Removing external reference to unknown node */ - static final int BDD_RUNNING = (-5); - /* Called bdd_init() twice whithout bdd_done() */ + static final int BDD_RANGE = (-3); /* Variable value out of range (not in domain) */ + static final int BDD_DEREF = (-4); /* Removing external reference to unknown node */ + static final int BDD_RUNNING = (-5); /* Called bdd_init() twice without bdd_done() */ static final int BDD_FILE = (-6); /* Some file operation failed */ static final int BDD_FORMAT = (-7); /* Incorrect file format */ - static final int BDD_ORDER = (-8); - /* Vars. not in order for vector based functions */ + static final int BDD_ORDER = (-8); /* Vars. not in order for vector based functions */ static final int BDD_BREAK = (-9); /* User called break */ - static final int BDD_VARNUM = (-10); - /* Different number of vars. for vector pair */ - static final int BDD_NODES = (-11); - /* Tried to set max. number of nodes to be fewer */ - /* than there already has been allocated */ + static final int BDD_VARNUM = (-10); /* Different number of vars. for vector pair */ + static final int BDD_NODES = (-11); /* Tried to set max. number of nodes to be fewer */ + /* than there already has been allocated */ static final int BDD_OP = (-12); /* Unknown operator */ static final int BDD_VARSET = (-13); /* Illegal variable set */ static final int BDD_VARBLK = (-14); /* Bad variable block operation */ - static final int BDD_DECVNUM = (-15); - /* Trying to decrease the number of variables */ - static final int BDD_REPLACE = (-16); - /* Replacing to already existing variables */ - static final int BDD_NODENUM = (-17); - /* Number of nodes reached user defined maximum */ + static final int BDD_DECVNUM = (-15); /* Trying to decrease the number of variables */ + static final int BDD_REPLACE = (-16); /* Replacing to already existing variables */ + static final int BDD_NODENUM = (-17); /* Number of nodes reached user defined maximum */ static final int BDD_ILLBDD = (-18); /* Illegal bdd argument */ static final int BDD_SIZE = (-19); /* Illegal size argument */ static final int BVEC_SIZE = (-20); /* Mismatch in bitvector size */ - static final int BVEC_SHIFT = (-21); - /* Illegal shift-left/right parameter */ + static final int BVEC_SHIFT = (-21); /* Illegal shift-left/right parameter */ static final int BVEC_DIVZERO = (-22); /* Division by zero */ static final int BDD_ERRNUM = 24; @@ -729,6 +734,11 @@ } /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#isZDD() + */ + public boolean isZDD() { return ZDD; } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#zero() */ public BDD zero() { @@ -742,6 +752,10 @@ return makeBDD(bddtrue); } + public BDDVarSet emptySet() { + return makeBDDVarSet(bddtrue); + } + int bdd_ithvar(int var) { if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); @@ -900,7 +914,7 @@ if (firstReorder == 0) bdd_disable_reorder(); - res = not_rec(r); + res = ZDD ? znot_rec(r) : not_rec(r); if (firstReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { @@ -948,6 +962,36 @@ 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; firstReorder = 1; @@ -965,7 +1009,7 @@ if (firstReorder == 0) ... [truncated message content] |
|
From: <joe...@us...> - 2006-06-06 23:38:32
|
Revision: 451 Author: joewhaley Date: 2006-06-06 16:38:30 -0700 (Tue, 06 Jun 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=451&view=rev Log Message: ----------- Added svn:ignore properties. Property Changed: ---------------- trunk/JavaBDD/ trunk/JavaBDD/net/sf/javabdd/ Property changes on: trunk/JavaBDD ___________________________________________________________________ Name: svn:ignore - buddy_jni.h cudd_jni.h cal_jni.h *.jar *.dll *.jnilib *.ext *.lib *.o *.class buddy22 cudd-2.3.1 cudd-2.4.0 cal-2.1 target velocity.log + buddy_jni.h cudd_jni.h cal_jni.h *.jar *.so *.dll *.jnilib *.ext *.lib *.o *.class buddy22 cudd-2.3.1 cudd-2.4.0 cal-2.1 target velocity.log Property changes on: trunk/JavaBDD/net/sf/javabdd ___________________________________________________________________ Name: svn:ignore + *.class This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-06-06 23:26:16
|
Revision: 450 Author: joewhaley Date: 2006-06-06 16:26:14 -0700 (Tue, 06 Jun 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=450&view=rev Log Message: ----------- Remove incorrect 'buddy' module import. Use the version in JavaBDD/buddy. Removed Paths: ------------- trunk/buddy/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: John W. <joe...@us...> - 2006-05-21 06:01:15
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs6.sourceforge.net:/tmp/cvs-serv29658 Modified Files: project.xml Log Message: Naughty sourceforge changed the CVS root. Index: project.xml =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/project.xml,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** project.xml 5 May 2005 21:41:55 -0000 1.18 --- project.xml 21 May 2006 06:01:10 -0000 1.19 *************** *** 46,52 **** <distributionDirectory>/home/groups/j/ja/javabdd/</distributionDirectory> <repository> ! <connection>scm:cvs:pserver:ano...@cv...:/cvsroot/javabdd:JavaBDD</connection> ! <developerConnection>scm:cvs:ext:joe...@cv...:/cvsroot/javabdd:JavaBDD</developerConnection> ! <url>http://cvs.sourceforge.net/viewcvs.py/javabdd/</url> </repository> <versions> --- 46,52 ---- <distributionDirectory>/home/groups/j/ja/javabdd/</distributionDirectory> <repository> ! <connection>scm:cvs:pserver:ano...@ja...:/cvsroot/javabdd:JavaBDD</connection> ! <developerConnection>scm:cvs:ext:joe...@ja...:/cvsroot/javabdd:JavaBDD</developerConnection> ! <url>http://javabdd.cvs.sourceforge.net/javabdd/</url> </repository> <versions> |
|
From: John W. <joe...@us...> - 2005-10-13 05:59:59
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24428/net/sf/javabdd Modified Files: FindBestOrder.java Log Message: Added parameterized waiting factors. Index: FindBestOrder.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/FindBestOrder.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** FindBestOrder.java 16 Oct 2004 02:58:57 -0000 1.1 --- FindBestOrder.java 13 Oct 2005 05:59:47 -0000 1.2 *************** *** 32,36 **** String filename3 = "fbo.3"; ! long DELAY_TIME = 30000; BDDFactory.BDDOp op; --- 32,40 ---- String filename3 = "fbo.3"; ! /** How long to delay for loading, in ms. */ ! long DELAY_TIME = Long.parseLong(System.getProperty("fbo.delaytime", "30000")); ! ! /** Factor how long to wait beyond the best time. */ ! float FACTOR = Float.parseFloat(System.getProperty("fbo.waitfactor", "1.1")); BDDFactory.BDDOp op; *************** *** 109,113 **** t.start(); try { ! long waitTime = bestTotalTime + DELAY_TIME; if (waitTime < 0L) waitTime = Long.MAX_VALUE; t.join(waitTime); --- 113,117 ---- t.start(); try { ! long waitTime = (long)(bestTotalTime*FACTOR) + DELAY_TIME; if (waitTime < 0L) waitTime = Long.MAX_VALUE; t.join(waitTime); |
|
From: John W. <joe...@us...> - 2005-10-13 05:37:19
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv19940/net/sf/javabdd Modified Files: TryVarOrder.java Log Message: Added parameterized waiting factors. Index: TryVarOrder.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TryVarOrder.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** TryVarOrder.java 19 Oct 2004 04:34:48 -0000 1.2 --- TryVarOrder.java 13 Oct 2005 05:37:07 -0000 1.3 *************** *** 240,244 **** /** How long to delay for loading, in ms. */ ! long DELAY_TIME = 20000; /** Best calc time so far. */ --- 240,247 ---- /** How long to delay for loading, in ms. */ ! long DELAY_TIME = Long.parseLong(System.getProperty("fbo.delaytime", "20000")); ! ! /** Factor how long to wait beyond the best time. */ ! float FACTOR = Float.parseFloat(System.getProperty("fbo.waitfactor", "1.1")); /** Best calc time so far. */ *************** *** 355,363 **** TryThread t = new TryThread(reverse, varOrder); t.start(); - boolean stopped; try { t.join(DELAY_TIME); if (t.initTime >= 0L) { ! t.join(bestCalcTime); } } catch (InterruptedException x) { --- 358,365 ---- TryThread t = new TryThread(reverse, varOrder); t.start(); try { t.join(DELAY_TIME); if (t.initTime >= 0L) { ! t.join((long)(bestCalcTime*FACTOR)); } } catch (InterruptedException x) { *************** *** 416,420 **** computeTime = doIt(); free(); ! System.out.println("Ordering: "+varOrderToTry+" time: "+time); } catch (Exception x) { System.err.println("Exception occurred while trying order: "+x.getLocalizedMessage()); --- 418,422 ---- computeTime = doIt(); free(); ! System.out.println("Ordering: "+varOrderToTry+" init: "+initTime+" compute: "+computeTime); } catch (Exception x) { System.err.println("Exception occurred while trying order: "+x.getLocalizedMessage()); |
|
From: John W. <joe...@us...> - 2005-10-12 10:27:21
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv461/net/sf/javabdd Modified Files: BDDFactory.java Log Message: Added support in makeVarOrdering for when some variables are not in BDDDomains. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.17 retrieving revision 1.18 diff -C2 -d -r1.17 -r1.18 *** BDDFactory.java 27 Sep 2005 22:56:19 -0000 1.17 --- BDDFactory.java 12 Oct 2005 10:27:08 -0000 1.18 *************** *** 6,10 **** import java.util.Arrays; import java.util.Collection; - import java.util.HashMap; import java.util.Iterator; import java.util.LinkedList; --- 6,9 ---- *************** *** 1576,1582 **** throw new BDDException("missing domain #"+i+": "+getDomain(i)); } - doms[i] = getDomain(i); } int[] test = new int[varorder.length]; System.arraycopy(varorder, 0, test, 0, varorder.length); --- 1575,1585 ---- throw new BDDException("missing domain #"+i+": "+getDomain(i)); } } + while (bitIndex < varorder.length) { + varorder[bitIndex] = bitIndex; + ++bitIndex; + } + int[] test = new int[varorder.length]; System.arraycopy(varorder, 0, test, 0, varorder.length); |
|
From: John W. <joe...@us...> - 2005-09-27 22:56:29
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17374/net/sf/javabdd Modified Files: JFactory.java BDDFactory.java Log Message: Added support for variable translation during load. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.16 retrieving revision 1.17 diff -C2 -d -r1.16 -r1.17 *** BDDFactory.java 11 Jul 2005 22:48:52 -0000 1.16 --- BDDFactory.java 27 Sep 2005 22:56:19 -0000 1.17 *************** *** 486,489 **** --- 486,503 ---- */ public BDD load(BufferedReader ifile) throws IOException { + return load(ifile, null); + } + + /** + * <p>Loads a BDD from the given input, translating BDD variables according + * to the given map.</p> + * + * <p>Compare to bdd_load.</p> + * + * @param ifile reader + * @param translate variable translation map + * @return BDD + */ + public BDD load(BufferedReader ifile, int[] translate) throws IOException { tokenizer = null; *************** *** 520,523 **** --- 534,539 ---- int key = Integer.parseInt(readNext(ifile)); int var = Integer.parseInt(readNext(ifile)); + if (translate != null) + var = translate[var]; int lowi = Integer.parseInt(readNext(ifile)); int highi = Integer.parseInt(readNext(ifile)); Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.27 retrieving revision 1.28 diff -C2 -d -r1.27 -r1.28 *** JFactory.java 21 May 2005 08:47:09 -0000 1.27 --- JFactory.java 27 Sep 2005 22:56:18 -0000 1.28 *************** *** 4940,4945 **** * @see net.sf.javabdd.BDDFactory#load(java.io.BufferedReader) */ ! public BDD load(BufferedReader in) throws IOException { ! int result = bdd_load(in); return makeBDD(result); } --- 4940,4945 ---- * @see net.sf.javabdd.BDDFactory#load(java.io.BufferedReader) */ ! public BDD load(BufferedReader in, int[] translate) throws IOException { ! int result = bdd_load(in, translate); return makeBDD(result); } *************** *** 6126,6130 **** LoadHash[] lh_table; ! int bdd_load(BufferedReader ifile) throws IOException { int n, vnum, tmproot; int root; --- 6126,6130 ---- LoadHash[] lh_table; ! int bdd_load(BufferedReader ifile, int[] translate) throws IOException { int n, vnum, tmproot; int root; *************** *** 6158,6162 **** lh_freepos = 0; ! tmproot = bdd_loaddata(ifile); for (n = 0; n < lh_nodenum; n++) --- 6158,6162 ---- lh_freepos = 0; ! tmproot = bdd_loaddata(ifile, translate); for (n = 0; n < lh_nodenum; n++) *************** *** 6179,6183 **** } ! int bdd_loaddata(BufferedReader ifile) throws IOException { int key, var, low, high, root = 0, n; --- 6179,6183 ---- } ! int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException { int key, var, low, high, root = 0, n; *************** *** 6185,6188 **** --- 6185,6190 ---- key = Integer.parseInt(readNext(ifile)); var = Integer.parseInt(readNext(ifile)); + if (translate != null) + var = translate[var]; low = Integer.parseInt(readNext(ifile)); high = Integer.parseInt(readNext(ifile)); |
|
From: John W. <joe...@us...> - 2005-07-22 19:44:00
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23063 Modified Files: cudd_jni.c Log Message: Fix stupid warning. Index: cudd_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v retrieving revision 1.15 retrieving revision 1.16 diff -C2 -d -r1.15 -r1.16 *** cudd_jni.c 22 Jul 2005 19:36:30 -0000 1.15 --- cudd_jni.c 22 Jul 2005 19:43:52 -0000 1.16 *************** *** 183,187 **** (*env)->ThrowNew(env, cls, "invalid number of variables"); (*env)->DeleteLocalRef(env, cls); ! return; } p = pair_list; --- 183,187 ---- (*env)->ThrowNew(env, cls, "invalid number of variables"); (*env)->DeleteLocalRef(env, cls); ! return 0; } p = pair_list; |
|
From: John W. <joe...@us...> - 2005-07-22 19:37:26
|
Update of /cvsroot/javabdd/JavaBDD_tests/regression In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20793/regression Added Files: R4.java Log Message: Regression test for allsat(). --- NEW FILE: R4.java --- // R4.java, created Jul 22, 2005 11:36:30 AM by joewhaley // Copyright (C) 2005 John Whaley <jw...@al...> // Licensed under the terms of the GNU LGPL; see COPYING for details. package regression; import junit.framework.Assert; import net.sf.javabdd.BDD; import net.sf.javabdd.BDDFactory; import bdd.BDDTestCase; /** * allsat bug * * @author John Whaley * @version $Id: R4.java,v 1.1 2005/07/22 19:37:11 joewhaley Exp $ */ public class R4 extends BDDTestCase { public static void main(String[] args) { junit.textui.TestRunner.run(R4.class); } public void testR4() { Assert.assertTrue(hasNext()); while (hasNext()) { BDDFactory f = nextFactory(); f.setVarNum(2); BDD bdd1 = f.ithVar(0); BDD.AllSatIterator i = bdd1.allsat(); Assert.assertTrue(i.hasNext()); byte[] b = (byte[]) i.next(); Assert.assertTrue(!i.hasNext()); Assert.assertEquals(b.length, 2); Assert.assertEquals(b[0], 1); Assert.assertEquals(b[1], -1); bdd1.free(); } } } |
|
From: John W. <joe...@us...> - 2005-07-22 19:36:42
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20511 Modified Files: cudd_jni.c Log Message: Added more fixes, error checking to setVarNum(). Index: cudd_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v retrieving revision 1.14 retrieving revision 1.15 diff -C2 -d -r1.14 -r1.15 *** cudd_jni.c 22 Jul 2005 19:11:50 -0000 1.14 --- cudd_jni.c 22 Jul 2005 19:36:30 -0000 1.15 *************** *** 131,134 **** --- 131,135 ---- int bdds; DdManager* m; + int varnum = Cudd_ReadSize(manager); while (pair_list) { *************** *** 165,169 **** (JNIEnv *env, jclass cl) { ! return varnum; } --- 166,170 ---- (JNIEnv *env, jclass cl) { ! return Cudd_ReadSize(manager); } *************** *** 177,181 **** { jint old = Cudd_ReadSize(manager); ! CuddPairing *p = pair_list; while (p) { int n; --- 178,189 ---- { jint old = Cudd_ReadSize(manager); ! CuddPairing *p; ! if (x < 1 || x < old || x > CUDD_MAXINDEX) { ! jclass cls = (*env)->FindClass(env, "java/lang/IllegalArgumentException"); ! (*env)->ThrowNew(env, cls, "invalid number of variables"); ! (*env)->DeleteLocalRef(env, cls); ! return; ! } ! p = pair_list; while (p) { int n; *************** *** 247,262 **** (JNIEnv *env, jclass cl, jintArray arr) { ! int *a; ! jint size = (*env)->GetArrayLength(env, arr); ! if (size != varnum) { ! jclass cls = (*env)->FindClass(env, "java/lang/IllegalArgumentException"); ! (*env)->ThrowNew(env, cls, "array size != number of vars"); ! (*env)->DeleteLocalRef(env, cls); ! return; ! } ! a = (int*) (*env)->GetPrimitiveArrayCritical(env, arr, NULL); ! if (a == NULL) return; ! Cudd_ShuffleHeap(manager, a); ! (*env)->ReleasePrimitiveArrayCritical(env, arr, a, JNI_ABORT); } --- 255,271 ---- (JNIEnv *env, jclass cl, jintArray arr) { ! int *a; ! int varnum = Cudd_ReadSize(manager); ! jint size = (*env)->GetArrayLength(env, arr); ! if (size != varnum) { ! jclass cls = (*env)->FindClass(env, "java/lang/IllegalArgumentException"); ! (*env)->ThrowNew(env, cls, "array size != number of vars"); ! (*env)->DeleteLocalRef(env, cls); ! return; ! } ! a = (int*) (*env)->GetPrimitiveArrayCritical(env, arr, NULL); ! if (a == NULL) return; ! Cudd_ShuffleHeap(manager, a); ! (*env)->ReleasePrimitiveArrayCritical(env, arr, a, JNI_ABORT); } |
|
From: John W. <joe...@us...> - 2005-07-22 19:11:59
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv13875 Modified Files: cudd_jni.c Log Message: Fixes to CUDD to correctly get and set number of variables. Index: cudd_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** cudd_jni.c 29 Jun 2005 08:00:44 -0000 1.13 --- cudd_jni.c 22 Jul 2005 19:11:50 -0000 1.14 *************** *** 34,38 **** static DdManager *manager; static jlong bdd_one, bdd_zero; - static int varcount, varnum; #define INVALID_BDD 0L --- 34,37 ---- *************** *** 177,181 **** (JNIEnv *env, jclass cl, jint x) { ! jint old = varnum; CuddPairing *p = pair_list; while (p) { --- 176,180 ---- (JNIEnv *env, jclass cl, jint x) { ! jint old = Cudd_ReadSize(manager); CuddPairing *p = pair_list; while (p) { *************** *** 194,198 **** p = p->next; } ! varnum = varcount = x; return old; } --- 193,199 ---- p = p->next; } ! while (Cudd_ReadSize(manager) < x) { ! Cudd_bddNewVar(manager); ! } return old; } *************** *** 683,686 **** --- 684,688 ---- { DdNode* d; + int varcount = Cudd_ReadSize(manager); d = (DdNode*) (intptr_cast_type) a; return Cudd_CountMinterm(manager, d, varcount); *************** *** 748,751 **** --- 750,754 ---- int n; int *arr; + int varnum = Cudd_ReadSize(manager); arr = (int*) malloc(sizeof(int)*varnum); if (arr == NULL) return INVALID_BDD; *************** *** 776,779 **** --- 779,783 ---- { int n; + int varnum = Cudd_ReadSize(manager); CuddPairing* r = (CuddPairing*) malloc(sizeof(CuddPairing)); if (r == NULL) return 0; *************** *** 838,841 **** --- 842,846 ---- int n; CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; + int varnum = Cudd_ReadSize(manager); for (n=0 ; n<varnum ; n++) { int var; *************** *** 859,862 **** --- 864,868 ---- CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; CuddPairing** ptr; + int varnum = Cudd_ReadSize(manager); for (n=0 ; n<varnum ; n++) { Cudd_RecursiveDeref(manager, r->table[n]); |
|
From: Christopher U. <cu...@us...> - 2005-07-12 01:35:38
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30215/net/sf/javabdd Modified Files: BDDDomain.java Log Message: domain resizing doesn't really work. throw an exception when it would be needed. Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDDomain.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** BDDDomain.java 21 May 2005 10:15:07 -0000 1.9 --- BDDDomain.java 12 Jul 2005 01:35:30 -0000 1.10 *************** *** 316,319 **** --- 316,322 ---- if (ivar.length == binsize) return binsize; + if (true) { + throw new BDDException("Can't add bits to domains, requested domain "+name+" upper limit "+range); + } int[] new_ivar = new int[binsize]; System.arraycopy(ivar, 0, new_ivar, 0, ivar.length); |
|
From: Christopher U. <cu...@us...> - 2005-07-12 01:34:09
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29471 Modified Files: buddy_jni.c Log Message: change #if to if() to accomodate cygwin gcc 3.4.4's obnoxious definition of CLOCKS_PER_SEC as "(clock_t) 1000". Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.33 retrieving revision 1.34 diff -C2 -d -r1.33 -r1.34 *** buddy_jni.c 21 May 2005 08:43:21 -0000 1.33 --- buddy_jni.c 12 Jul 2005 01:34:00 -0000 1.34 *************** *** 149,157 **** if (fid) { long t = s->time; ! #if CLOCKS_PER_SEC < 1000 ! t = t * 1000 / CLOCKS_PER_SEC; ! #else ! t /= (CLOCKS_PER_SEC/1000); ! #endif (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } --- 149,158 ---- if (fid) { long t = s->time; ! if (CLOCKS_PER_SEC < 1000) { ! t = t * 1000 / CLOCKS_PER_SEC; ! } ! else { ! t /= (CLOCKS_PER_SEC/1000); ! } (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } *************** *** 159,167 **** if (fid) { long t = s->sumtime; ! #if CLOCKS_PER_SEC < 1000 ! t = t * 1000 / CLOCKS_PER_SEC; ! #else ! t /= (CLOCKS_PER_SEC/1000); ! #endif (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } --- 160,169 ---- if (fid) { long t = s->sumtime; ! if (CLOCKS_PER_SEC < 1000) { ! t = t * 1000 / CLOCKS_PER_SEC; ! } ! else { ! t /= (CLOCKS_PER_SEC/1000); ! } (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } |
|
From: CS343 s. <cs...@us...> - 2005-07-11 22:49:04
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4325 Modified Files: BDDFactory.java Log Message: modified save and save_rec to use node hashcode & bitset instead of node object & map, to save memory. previous implementation kept as save_rec_original. note: this is incompatible with the CUDD factory, which should use the original implementation instead. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/BDDFactory.java,v retrieving revision 1.15 retrieving revision 1.16 diff -C2 -d -r1.15 -r1.16 *** BDDFactory.java 24 May 2005 18:24:38 -0000 1.15 --- BDDFactory.java 11 Jul 2005 22:48:52 -0000 1.16 *************** *** 12,15 **** --- 12,16 ---- import java.util.Map; import java.util.StringTokenizer; + import java.util.BitSet; import java.io.BufferedReader; import java.io.BufferedWriter; *************** *** 639,649 **** out.write("\n"); ! Map visited = new HashMap(); ! save_rec(out, visited, r); ! for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) { ! BDD b = (BDD) it.next(); ! if (b != r) b.free(); ! } } --- 640,651 ---- out.write("\n"); ! //Map visited = new HashMap(); ! BitSet visited = new BitSet(getNodeTableSize()); ! save_rec(out, visited, r.id()); ! //for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) { ! // BDD b = (BDD) it.next(); ! // if (b != r) b.free(); ! //} } *************** *** 651,655 **** * Helper function for save(). */ ! protected int save_rec(BufferedWriter out, Map visited, BDD root) throws IOException { if (root.isZero()) { root.free(); --- 653,657 ---- * Helper function for save(). */ ! protected int save_rec_original(BufferedWriter out, Map visited, BDD root) throws IOException { if (root.isZero()) { root.free(); *************** *** 669,676 **** BDD l = root.low(); ! int lo = save_rec(out, visited, l); BDD h = root.high(); ! int hi = save_rec(out, visited, h); out.write(v + " "); --- 671,678 ---- BDD l = root.low(); ! int lo = save_rec_original(out, visited, l); BDD h = root.high(); ! int hi = save_rec_original(out, visited, h); out.write(v + " "); *************** *** 681,684 **** --- 683,732 ---- return v; } + + + /** + * Helper function for save(). + */ + protected int save_rec(BufferedWriter out, BitSet visited, BDD root) throws IOException { + if (root.isZero()) { + root.free(); + return 0; + } + if (root.isOne()) { + root.free(); + return 1; + } + //Integer i = (Integer) visited.get(root); + int i = root.hashCode(); + //if (i != null) { + if (visited.get(i)) { + root.free(); + //return i.intValue(); + return i; + } + //int v = visited.size() + 2; + int v = i; + //visited.put(root, new Integer(v)); + visited.set(i); + + BDD h = root.high(); + + BDD l = root.low(); + + int rootvar = root.var(); + root.free(); + + int lo = save_rec(out, visited, l); + + int hi = save_rec(out, visited, h); + + //out.write(v + " "); + out.write(i + " "); + out.write(rootvar + " "); + out.write(lo + " "); + out.write(hi + "\n"); + + return v; + } // TODO: bdd_blockfile_hook |
|
From: John W. <joe...@us...> - 2005-06-29 08:02:03
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3633/bdd Modified Files: BDDTestCase.java Log Message: Also test CUDD factory by default. Index: BDDTestCase.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BDDTestCase.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** BDDTestCase.java 21 May 2005 02:46:19 -0000 1.7 --- BDDTestCase.java 29 Jun 2005 08:01:54 -0000 1.8 *************** *** 24,28 **** "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.MicroFactory", ! //"net.sf.javabdd.CUDDFactory", //"net.sf.javabdd.CALFactory", //"net.sf.javabdd.JDDFactory", --- 24,28 ---- "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.MicroFactory", ! "net.sf.javabdd.CUDDFactory", //"net.sf.javabdd.CALFactory", //"net.sf.javabdd.JDDFactory", |
|
From: John W. <joe...@us...> - 2005-06-29 08:01:37
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3494/bdd Modified Files: BasicTests.java Log Message: Added replace test. Removed ensureCapacity tests. Index: BasicTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BasicTests.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** BasicTests.java 29 Apr 2005 06:44:03 -0000 1.5 --- BasicTests.java 29 Jun 2005 08:01:29 -0000 1.6 *************** *** 17,20 **** --- 17,21 ---- import net.sf.javabdd.BDDException; import net.sf.javabdd.BDDFactory; + import net.sf.javabdd.BDDPairing; /** *************** *** 396,400 **** } ! public void testEnsureCapacity() { reset(); Assert.assertTrue(hasNext()); --- 397,440 ---- } ! public void testReplace() { ! reset(); ! Assert.assertTrue(hasNext()); ! while (hasNext()) { ! BDDFactory bdd = nextFactory(); ! if (bdd.varNum() < 5) bdd.setVarNum(5); ! BDDPairing p1 = bdd.makePair(0, 1); ! BDDPairing p2 = bdd.makePair(); ! p2.set(1, 2); ! BDDPairing p3 = bdd.makePair(); ! p3.set(new int[] { 0, 1 }, new int[] { 1, 0 }); ! BDD a, b, c, d, e, f; ! a = bdd.ithVar(0); ! b = bdd.ithVar(1); ! c = bdd.ithVar(2); ! d = bdd.zero(); ! e = bdd.one(); ! a.replaceWith(p1); ! Assert.assertEquals(a, b); ! a.replaceWith(p2); ! Assert.assertEquals(a, c); ! if (bdd.varNum() < 25) bdd.setVarNum(25); ! b.andWith(bdd.nithVar(0)); ! f = b.replace(p3); ! f.andWith(bdd.ithVar(0)); ! Assert.assertTrue(!f.isZero()); ! f.andWith(bdd.ithVar(1)); ! Assert.assertTrue(f.isZero()); ! d.replaceWith(p3); ! Assert.assertTrue(d.isZero()); ! e.replaceWith(p3); ! Assert.assertTrue(e.isOne()); ! a.free(); b.free(); c.free(); d.free(); e.free(); f.free(); ! p1.reset(); ! p2.reset(); ! p3.reset(); ! } ! } ! ! void tEnsureCapacity() { reset(); Assert.assertTrue(hasNext()); *************** *** 433,437 **** } ! public void testEnsureCapacity2() throws IOException { reset(); Assert.assertTrue(hasNext()); --- 473,477 ---- } ! void tEnsureCapacity2() throws IOException { reset(); Assert.assertTrue(hasNext()); *************** *** 439,443 **** BDDFactory bdd = nextFactory(); System.out.println("Factory "+bdd); - int n = bdd.numberOfDomains(); long[] domainSizes = new long[] { 127, 17, 31, 4, 256, 87, 42, 666, 3405, 18 }; while (bdd.numberOfDomains() < domainSizes.length) { --- 479,482 ---- |
|
From: John W. <joe...@us...> - 2005-06-29 08:00:54
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3183 Modified Files: cudd_jni.c Log Message: Fixed implementation of CUDD pairing. Also added getCacheSize() Index: cudd_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** cudd_jni.c 16 Oct 2004 02:58:57 -0000 1.12 --- cudd_jni.c 29 Jun 2005 08:00:44 -0000 1.13 *************** *** 60,63 **** --- 60,70 ---- } + typedef struct CuddPairing { + DdNode** table; + struct CuddPairing *next; + } CuddPairing; + + static CuddPairing *pair_list; + /* * Class: net_sf_javabdd_CUDDFactory *************** *** 91,94 **** --- 98,103 ---- Cudd_Ref((DdNode *)(intptr_cast_type) bdd_zero); + pair_list = NULL; + one_fid = (*env)->GetStaticFieldID(env, cl, "one", "J"); zero_fid = (*env)->GetStaticFieldID(env, cl, "zero", "J"); *************** *** 124,132 **** DdManager* m; Cudd_Deref((DdNode *)(intptr_cast_type) bdd_one); Cudd_Deref((DdNode *)(intptr_cast_type) bdd_zero); fprintf(stderr, "Garbage collections: %d Time spent: %ldms\n", ! Cudd_ReadGarbageCollections(manager), Cudd_ReadGarbageCollectionTime(manager)); bdds = Cudd_CheckZeroRef(manager); --- 133,153 ---- DdManager* m; + while (pair_list) { + CuddPairing *p; + int n; + for (n=0 ; n<varnum ; n++) { + Cudd_RecursiveDeref(manager, pair_list->table[n]); + } + free(pair_list->table); + p = pair_list->next; + free(pair_list); + pair_list = p; + } + Cudd_Deref((DdNode *)(intptr_cast_type) bdd_one); Cudd_Deref((DdNode *)(intptr_cast_type) bdd_zero); fprintf(stderr, "Garbage collections: %d Time spent: %ldms\n", ! Cudd_ReadGarbageCollections(manager), Cudd_ReadGarbageCollectionTime(manager)); bdds = Cudd_CheckZeroRef(manager); *************** *** 134,138 **** m = manager; manager = NULL; // race condition with delRef ! Cudd_Quit(m); } --- 155,159 ---- m = manager; manager = NULL; // race condition with delRef ! Cudd_Quit(m); } *************** *** 157,160 **** --- 178,197 ---- { jint old = varnum; + CuddPairing *p = pair_list; + while (p) { + int n; + DdNode** t = (DdNode**) malloc(sizeof(DdNode*)*x); + if (t == NULL) return 0; + memcpy(t, p->table, sizeof(DdNode*)*old); + for (n=old ; n<x ; n++) { + int var = n; + //int var = Cudd_ReadInvPerm(manager, n); // level2var + t[n] = Cudd_bddIthVar(manager, var); + Cudd_Ref(t[n]); + } + free(p->table); + p->table = t; + p = p->next; + } varnum = varcount = x; return old; *************** *** 185,190 **** (JNIEnv *env, jclass cl, jint level) { ! //return manager->invperm[level]; ! return (jint) Cudd_ReadInvPerm(manager, level); } --- 222,227 ---- (JNIEnv *env, jclass cl, jint level) { ! //return manager->invperm[level]; ! return (jint) Cudd_ReadInvPerm(manager, level); } *************** *** 197,202 **** (JNIEnv *env, jclass cl, jint v) { ! //return (jint) cuddI(manager, v); ! return (jint) Cudd_ReadPerm(manager, v); } --- 234,239 ---- (JNIEnv *env, jclass cl, jint v) { ! //return (jint) cuddI(manager, v); ! return (jint) Cudd_ReadPerm(manager, v); } *************** *** 245,248 **** --- 282,296 ---- } + /* + * Class: net_sf_javabdd_CUDDFactory + * Method: getCacheSize0 + * Signature: ()I + */ + JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_getCacheSize0 + (JNIEnv *env, jclass cl) + { + return Cudd_ReadCacheSlots(manager); + } + /* class net_sf_javabdd_CUDDFactory_CUDDBDD */ *************** *** 529,542 **** if (F == zero || ! F == one) { ! return f; } ! index = F->index; high = cuddT(F); low = cuddE(F); if (Cudd_IsComplement(f)) { ! high = Cudd_Not(high); ! low = Cudd_Not(low); } if (low == (DdNode*)(intptr_cast_type)bdd_zero) { --- 577,590 ---- if (F == zero || ! F == one) { ! return f; } ! index = F->index; high = cuddT(F); low = cuddE(F); if (Cudd_IsComplement(f)) { ! high = Cudd_Not(high); ! low = Cudd_Not(low); } if (low == (DdNode*)(intptr_cast_type)bdd_zero) { *************** *** 544,548 **** if (res == NULL) { return NULL; ! } cuddRef(res); if (Cudd_IsComplement(res)) { --- 592,596 ---- if (res == NULL) { return NULL; ! } cuddRef(res); if (Cudd_IsComplement(res)) { *************** *** 675,685 **** (JNIEnv *env, jclass cl, jlong a, jlong b) { ! DdNode* d; ! DdNode** e; ! DdNode* f; jlong result; d = (DdNode*) (intptr_cast_type) a; ! e = (DdNode**) (intptr_cast_type) b; ! f = Cudd_bddVectorCompose(manager, d, e); result = (jlong) (intptr_cast_type) f; return result; --- 723,733 ---- (JNIEnv *env, jclass cl, jlong a, jlong b) { ! DdNode* d; ! CuddPairing* e; ! DdNode* f; jlong result; d = (DdNode*) (intptr_cast_type) a; ! e = (CuddPairing*) (intptr_cast_type) b; ! f = Cudd_bddVectorCompose(manager, d, e->table); result = (jlong) (intptr_cast_type) f; return result; *************** *** 694,714 **** (JNIEnv *env, jclass cl, jlong a, jlong b) { ! DdNode* d; ! DdNode** e; ! DdNode* f; jlong result; ! int n; ! int *arr; ! arr = (int*) malloc(sizeof(int)*varnum); ! if (arr == NULL) return INVALID_BDD; d = (DdNode*) (intptr_cast_type) a; ! e = (DdNode**) (intptr_cast_type) b; ! for (n=0; n<varnum; ++n) { ! DdNode* node = e[n]; ! int var = Cudd_Regular(node)->index; ! int level = var; ! //int level = Cudd_ReadPerm(manager, var); ! arr[n] = level; ! } f = Cudd_bddPermute(manager, d, arr); free(arr); --- 742,762 ---- (JNIEnv *env, jclass cl, jlong a, jlong b) { ! DdNode* d; ! CuddPairing* e; ! DdNode* f; jlong result; ! int n; ! int *arr; ! arr = (int*) malloc(sizeof(int)*varnum); ! if (arr == NULL) return INVALID_BDD; d = (DdNode*) (intptr_cast_type) a; ! e = (CuddPairing*) (intptr_cast_type) b; ! for (n=0; n<varnum; ++n) { ! DdNode* node = e->table[n]; ! int var = Cudd_Regular(node)->index; ! int level = var; ! //int level = Cudd_ReadPerm(manager, var); ! arr[n] = level; ! } f = Cudd_bddPermute(manager, d, arr); free(arr); *************** *** 727,740 **** (JNIEnv *env, jclass cl) { ! int n; ! DdNode **r = (DdNode**) malloc(sizeof(DdNode*)*varnum); ! if (r == NULL) return 0; ! for (n=0 ; n<varnum ; n++) { ! int var = n; ! //int var = Cudd_ReadInvPerm(manager, n); // level2var ! r[n] = Cudd_bddIthVar(manager, var); ! Cudd_Ref(r[n]); ! } ! return (jlong) (intptr_cast_type) r; } --- 775,795 ---- (JNIEnv *env, jclass cl) { ! int n; ! CuddPairing* r = (CuddPairing*) malloc(sizeof(CuddPairing)); ! if (r == NULL) return 0; ! r->table = (DdNode**) malloc(sizeof(DdNode*)*varnum); ! if (r->table == NULL) { ! free(r); ! return 0; ! } ! for (n=0 ; n<varnum ; n++) { ! int var = n; ! //int var = Cudd_ReadInvPerm(manager, n); // level2var ! r->table[n] = Cudd_bddIthVar(manager, var); ! Cudd_Ref(r->table[n]); ! } ! r->next = pair_list; ! pair_list = r; ! return (jlong) (intptr_cast_type) r; } *************** *** 747,757 **** (JNIEnv *env, jclass cl, jlong p, jint var, jint b) { ! DdNode **r = (DdNode**) (intptr_cast_type) p; ! int level1 = var; ! //int level1 = Cudd_ReadPerm(manager, var); ! //int level2 = Cudd_ReadPerm(manager, b); ! Cudd_RecursiveDeref(manager, r[level1]); ! r[level1] = Cudd_bddIthVar(manager, b); ! Cudd_Ref(r[level1]); } --- 802,812 ---- (JNIEnv *env, jclass cl, jlong p, jint var, jint b) { ! CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; ! int level1 = var; ! //int level1 = Cudd_ReadPerm(manager, var); ! //int level2 = Cudd_ReadPerm(manager, b); ! Cudd_RecursiveDeref(manager, r->table[level1]); ! r->table[level1] = Cudd_bddIthVar(manager, b); ! Cudd_Ref(r->table[level1]); } *************** *** 764,774 **** (JNIEnv *env, jclass cl, jlong p, jint var, jlong b) { ! DdNode **r = (DdNode**) (intptr_cast_type) p; ! DdNode *d = (DdNode*) (intptr_cast_type) b; ! int level1 = var; ! //int level1 = Cudd_ReadPerm(manager, var); ! Cudd_RecursiveDeref(manager, r[level1]); ! r[level1] = d; ! Cudd_Ref(r[level1]); } --- 819,829 ---- (JNIEnv *env, jclass cl, jlong p, jint var, jlong b) { ! CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; ! DdNode *d = (DdNode*) (intptr_cast_type) b; ! int level1 = var; ! //int level1 = Cudd_ReadPerm(manager, var); ! Cudd_RecursiveDeref(manager, r->table[level1]); ! r->table[level1] = d; ! Cudd_Ref(r->table[level1]); } *************** *** 781,794 **** (JNIEnv *env, jclass cl, jlong p) { ! int n; ! DdNode **r = (DdNode**) (intptr_cast_type) p; ! for (n=0 ; n<varnum ; n++) { ! int var; ! Cudd_RecursiveDeref(manager, r[n]); ! var = n; ! //int var = Cudd_ReadInvPerm(manager, n); // level2var ! r[n] = Cudd_bddIthVar(manager, var); ! Cudd_Ref(r[n]); ! } } --- 836,849 ---- (JNIEnv *env, jclass cl, jlong p) { ! int n; ! CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; ! for (n=0 ; n<varnum ; n++) { ! int var; ! Cudd_RecursiveDeref(manager, r->table[n]); ! var = n; ! //int var = Cudd_ReadInvPerm(manager, n); // level2var ! r->table[n] = Cudd_bddIthVar(manager, var); ! Cudd_Ref(r->table[n]); ! } } *************** *** 801,809 **** (JNIEnv *env, jclass cl, jlong p) { ! int n; ! DdNode **r = (DdNode**) (intptr_cast_type) p; ! for (n=0 ; n<varnum ; n++) { ! Cudd_RecursiveDeref(manager, r[n]); ! } ! free(r); } --- 856,870 ---- (JNIEnv *env, jclass cl, jlong p) { ! int n; ! CuddPairing* r = (CuddPairing*) (intptr_cast_type) p; ! CuddPairing** ptr; ! for (n=0 ; n<varnum ; n++) { ! Cudd_RecursiveDeref(manager, r->table[n]); ! } ! ptr = &pair_list; ! while (*ptr != r) ! ptr = &(*ptr)->next; ! *ptr = r->next; ! free(r->table); ! free(r); } |
