Thread: [Javabdd-checkins] SF.net SVN: javabdd: [451] trunk/JavaBDD
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins
|
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-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-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-21 16:55:31
|
Revision: 463 Author: joewhaley Date: 2006-07-21 09:55:23 -0700 (Fri, 21 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=463&view=rev Log Message: ----------- Update BuDDyFactory to also use common superclass BDDFactoryIntImpl. Modified Paths: -------------- trunk/JavaBDD/Makefile trunk/JavaBDD/buddy_jni.c trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java Modified: trunk/JavaBDD/Makefile =================================================================== --- trunk/JavaBDD/Makefile 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/Makefile 2006-07-21 16:55:23 UTC (rev 463) @@ -141,8 +141,7 @@ CUDD_CLASSFILE = net/sf/javabdd/CUDDFactory.class CAL_CLASSFILE = net/sf/javabdd/CALFactory.class BUDDY_CLASSNAMES = net.sf.javabdd.BuDDyFactory \ - net.sf.javabdd.BuDDyFactory\$$BuDDyBDD \ - net.sf.javabdd.BuDDyFactory\$$BuDDyBDDPairing + net.sf.javabdd.BuDDyFactory\$$BuDDyPairing CUDD_CLASSNAMES = net.sf.javabdd.CUDDFactory \ net.sf.javabdd.CUDDFactory\$$CUDDBDD \ net.sf.javabdd.CUDDFactory\$$CUDDBDDPairing Modified: trunk/JavaBDD/buddy_jni.c =================================================================== --- trunk/JavaBDD/buddy_jni.c 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/buddy_jni.c 2006-07-21 16:55:23 UTC (rev 463) @@ -984,10 +984,10 @@ /* * Class: net_sf_javabdd_BuDDyFactory - * Method: nodeCount0 + * Method: nodeCount1 * Signature: ([I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_nodeCount0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_nodeCount1 (JNIEnv *env, jclass cl, jintArray arr) { jint *a; @@ -1116,11 +1116,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: var0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_var0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_var0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1134,11 +1134,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: high0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_high0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_high0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1152,11 +1152,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: low0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_low0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_low0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1169,11 +1169,11 @@ return result;} /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: not0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_not0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_not0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1187,11 +1187,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: ite0 * Signature: (III)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_ite0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_ite0 (JNIEnv *env, jclass cl, jint b, jint c, jint d) { int result; @@ -1205,11 +1205,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: relprod0 * Signature: (III)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_relprod0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_relprod0 (JNIEnv *env, jclass cl, jint b, jint c, jint d) { int result; @@ -1223,11 +1223,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: compose0 * Signature: (III)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_compose0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_compose0 (JNIEnv *env, jclass cl, jint b, jint c, jint v) { int result; @@ -1241,11 +1241,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: constrain0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_constrain0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_constrain0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1259,11 +1259,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: exist0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_exist0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_exist0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1277,11 +1277,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: forAll0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_forAll0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_forAll0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1295,11 +1295,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: unique0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_unique0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_unique0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1313,11 +1313,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: restrict0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_restrict0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_restrict0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1331,11 +1331,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: simplify0 * Signature: (II)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_simplify0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_simplify0 (JNIEnv *env, jclass cl, jint b, jint c) { int result; @@ -1349,11 +1349,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: support0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_support0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_support0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1367,11 +1367,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: apply0 * Signature: (III)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_apply0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_apply0 (JNIEnv *env, jclass cl, jint b, jint c, jint operation) { int result; @@ -1385,11 +1385,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: applyAll0 * Signature: (IIII)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_applyAll0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_applyAll0 (JNIEnv *env, jclass cl, jint b, jint c, jint operation, jint d) { int result; @@ -1403,11 +1403,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: applyEx0 * Signature: (IIII)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_applyEx0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_applyEx0 (JNIEnv *env, jclass cl, jint b, jint c, jint operation, jint d) { int result; @@ -1421,11 +1421,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: applyUni0 * Signature: (IIII)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_applyUni0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_applyUni0 (JNIEnv *env, jclass cl, jint b, jint c, jint operation, jint d) { int result; @@ -1439,11 +1439,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: satOne0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_satOne0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_satOne0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1457,11 +1457,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: fullSatOne0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_fullSatOne0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_fullSatOne0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1475,11 +1475,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: satOne1 * Signature: (III)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_satOne1 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_satOne1 (JNIEnv *env, jclass cl, jint b, jint c, jint d) { int result; @@ -1493,11 +1493,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: printSet0 * Signature: (I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_printSet0 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_printSet0 (JNIEnv *env, jclass cl, jint b) { jnienv = env; @@ -1510,11 +1510,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: printDot0 * Signature: (I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_printDot0 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_printDot0 (JNIEnv *env, jclass cl, jint b) { jnienv = env; @@ -1527,11 +1527,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: nodeCount0 * Signature: (I)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_nodeCount0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_nodeCount0 (JNIEnv *env, jclass cl, jint b) { int result; @@ -1545,11 +1545,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: pathCount0 * Signature: (I)D */ -JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_pathCount0 +JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_pathCount0 (JNIEnv *env, jclass cl, jint b) { double result; @@ -1563,11 +1563,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: satCount0 * Signature: (I)D */ -JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_satCount0 +JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_satCount0 (JNIEnv *env, jclass cl, jint b) { double result; @@ -1581,11 +1581,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: satCount1 * Signature: (II)D */ -JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_satCount1 +JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_satCount1 (JNIEnv *env, jclass cl, jint b, jint c) { double result; @@ -1599,11 +1599,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: logSatCount0 * Signature: (I)D */ -JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_logSatCount0 +JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_logSatCount0 (JNIEnv *env, jclass cl, jint b) { double result; @@ -1617,11 +1617,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: logSatCount1 * Signature: (II)D */ -JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_logSatCount1 +JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_BuDDyFactory_logSatCount1 (JNIEnv *env, jclass cl, jint b, jint c) { double result; @@ -1635,11 +1635,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: varProfile0 * Signature: (I)[I */ -JNIEXPORT jintArray JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_varProfile0 +JNIEXPORT jintArray JNICALL Java_net_sf_javabdd_BuDDyFactory_varProfile0 (JNIEnv *env, jclass cl, jint b) { jintArray result; @@ -1664,11 +1664,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: addRef * Signature: (I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_addRef +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_addRef (JNIEnv *env, jclass cl, jint b) { jnienv = env; @@ -1680,11 +1680,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD + * Class: net_sf_javabdd_BuDDyFactory * Method: delRef * Signature: (I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_delRef +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_delRef (JNIEnv *env, jclass cl, jint b) { jnienv = env; @@ -1702,7 +1702,7 @@ * Method: veccompose0 * Signature: (IJ)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_veccompose0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_veccompose0 (JNIEnv *env, jclass cl, jint b, jlong pair) { int result; @@ -1722,7 +1722,7 @@ * Method: replace0 * Signature: (IJ)I */ -JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDD_replace0 +JNIEXPORT jint JNICALL Java_net_sf_javabdd_BuDDyFactory_replace0 (JNIEnv *env, jclass cl, jint b, jlong pair) { int result; @@ -1737,14 +1737,14 @@ return result; } -/* class net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing */ +/* class net_sf_javabdd_BuDDyFactory_BuDDyPairing */ /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: set0 * Signature: (JII)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_set0 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_set0 (JNIEnv *env, jclass cl, jlong pair, jint i, jint j) { bddPair* p; @@ -1758,11 +1758,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: set1 * Signature: (J[I[I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_set1 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_set1 (JNIEnv *env, jclass cl, jlong pair, jintArray arr1, jintArray arr2) { jint size1, size2; @@ -1795,11 +1795,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: set2 * Signature: (JII)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_set2 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_set2 (JNIEnv *env, jclass cl, jlong pair, jint b, jint c) { bddPair* p; @@ -1813,11 +1813,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: set3 * Signature: (J[I[I)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_set3 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_set3 (JNIEnv *env, jclass cl, jlong pair, jintArray arr1, jintArray arr2) { jint size1, size2; @@ -1850,11 +1850,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: reset0 * Signature: (J)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_reset0 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_reset0 (JNIEnv *env, jclass cl, jlong pair) { bddPair* p; @@ -1868,11 +1868,11 @@ } /* - * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing + * Class: net_sf_javabdd_BuDDyFactory_BuDDyPairing * Method: free0 * Signature: (J)V */ -JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_free0 +JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyPairing_free0 (JNIEnv *env, jclass cl, jlong pair) { bddPair* p; Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-21 16:55:23 UTC (rev 463) @@ -399,6 +399,19 @@ return makeBDD(zero_impl()); } + public void done() { + if (USE_FINALIZER) { + System.gc(); + System.runFinalization(); + handleDeferredFree(); + } + } + + protected void finalize() throws Throwable { + super.finalize(); + this.done(); + } + protected /*bdd*/int[] to_free = new /*bdd*/int[8]; protected /*bdd*/int to_free_length = 0; public void deferredFree(int v) { Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-21 16:55:23 UTC (rev 463) @@ -4,9 +4,6 @@ package net.sf.javabdd; import java.util.Arrays; -import java.util.Collection; -import java.util.Iterator; -import java.util.List; import java.io.File; import java.io.FileInputStream; import java.io.FileOutputStream; @@ -26,8 +23,8 @@ * you are _completely_ sure that all BDD objects that reference the old * factory have been freed.</p> * - * <p>If you really need multiple BDD factories, consider using the JavaFactory - * class for the additional BDD factories --- JavaFactory can have multiple + * <p>If you really need multiple BDD factories, consider using the JFactory + * class for the additional BDD factories --- JFactory can have multiple * factory instances active at a time.</p> * * @see net.sf.javabdd.BDDFactory @@ -35,14 +32,10 @@ * @author John Whaley * @version $Id$ */ -public class BuDDyFactory extends BDDFactory { +public class BuDDyFactory extends BDDFactoryIntImpl { public static BDDFactory init(int nodenum, int cachesize) { - BuDDyFactory f; - if (USE_FINALIZER) - f = new BuDDyFactoryWithFinalizer(); - else - f = new BuDDyFactory(); + BuDDyFactory f = new BuDDyFactory(); f.initialize(nodenum, cachesize); return f; } @@ -98,93 +91,128 @@ private BuDDyFactory() {} - private static final boolean USE_FINALIZER = false; + /** An invalid id, for use in invalidating BDDs. */ + static final int INVALID_BDD = -1; - private static class BuDDyFactoryWithFinalizer extends BuDDyFactory { - - /** - * @see java.lang.Object#finalize() - */ - protected void finalize() throws Throwable { - super.finalize(); - this.done(); - } - - } + // Redirection functions. - private static BuDDyBDD makeBDD(int id) { - BuDDyBDD b; - if (USE_FINALIZER) { - b = new BuDDyBDDWithFinalizer(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 BuDDyBDD(id); - } - return b; - } + protected void addref_impl(int v) { addRef(v); } + private static native void addRef(int b); + protected void delref_impl(int v) { delRef(v); } + private static native void delRef(int b); + protected int zero_impl() { return 0; } + protected int one_impl() { return 1; } + protected int invalid_bdd_impl() { return INVALID_BDD; } + protected int var_impl(int v) { return var0(v); } + private static native int var0(int b); + protected int level_impl(int v) { return var2Level0(var0(v)); } + protected int low_impl(int v) { return low0(v); } + private static native int low0(int b); + protected int high_impl(int v) { return high0(v); } + private static native int high0(int b); + protected int ithVar_impl(int var) { return ithVar0(var); } + private static native int ithVar0(int var); + protected int nithVar_impl(int var) { return nithVar0(var); } + private static native int nithVar0(int var); - private static BDDVarSet.DefaultImpl makeBDDVarSet(int id) { - return new BDDVarSet.DefaultImpl(makeBDD(id)); - } + protected int ite_impl(int v1, int v2, int v3) { return ite0(v1, v2, v3); } + private static native int ite0(int b, int c, int d); + protected int apply_impl(int v1, int v2, BDDOp opr) { return apply0(v1, v2, opr.id); } + private static native int apply0(int b, int c, int opr); + protected int not_impl(int v1) { return not0(v1); } + private static native int not0(int b); + protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return applyAll0(v1, v2, opr.id, v3); } + private static native int applyAll0(int b, int c, int opr, int d); + protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return applyEx0(v1, v2, opr.id, v3); } + private static native int applyEx0(int b, int c, int opr, int d); + protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return applyUni0(v1, v2, opr.id, v3); } + private static native int applyUni0(int b, int c, int opr, int d); + protected int compose_impl(int v1, int v2, int var) { return compose0(v1, v2, var); } + private static native int compose0(int b, int c, int var); + protected int constrain_impl(int v1, int v2) { return constrain0(v1, v2); } + private static native int constrain0(int b, int c); + protected int restrict_impl(int v1, int v2) { return restrict0(v1, v2); } + private static native int restrict0(int b, int var); + protected int simplify_impl(int v1, int v2) { return simplify0(v1, v2); } + private static native int simplify0(int b, int d); + protected int support_impl(int v) { return support0(v); } + private static native int support0(int b); + protected int exist_impl(int v1, int v2) { return exist0(v1, v2); } + private static native int exist0(int b, int var); + protected int forAll_impl(int v1, int v2) { return forAll0(v1, v2); } + private static native int forAll0(int b, int var); + protected int unique_impl(int v1, int v2) { return unique0(v1, v2); } + private static native int unique0(int b, int var); + protected int fullSatOne_impl(int v) { return fullSatOne0(v); } + private static native int fullSatOne0(int b); - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#zero() - */ - public BDD zero() { return makeBDD(0); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#one() - */ - public BDD one() { return makeBDD(1); } + protected int replace_impl(int v, BDDPairing p) { return replace0(v, unwrap(p)); } + private static native int replace0(int b, long p); + protected int veccompose_impl(int v, BDDPairing p) { return veccompose0(v, unwrap(p)); } + private static native int veccompose0(int b, long p); - /** - * Converts collection of BuDDyBDD's into an int array, for passing to - * native code. - * - * @param c collection of BuDDyBDD's - * @return int array of indices - */ - private static int[] toBuDDyArray(Collection c) { - int[] a = new int[c.size()]; - int k = 0; - for (Iterator i = c.iterator(); k < a.length; ++k) { - BuDDyBDD b = (BuDDyBDD) i.next(); - a[k] = b._id; - } - return a; - } + protected int nodeCount_impl(int v) { return nodeCount0(v); } + private static native int nodeCount0(int b); + protected double pathCount_impl(int v) { return pathCount0(v); } + private static native double pathCount0(int b); + protected double satCount_impl(int v) { return satCount0(v); } + private static native double satCount0(int b); + protected int satOne_impl(int v) { return satOne0(v); } + private static native int satOne0(int b); + protected int satOne_impl2(int v1, int v2, boolean pol) { return satOne1(v1, v2, pol?1:0); } + private static native int satOne1(int b, int c, int d); + protected int nodeCount_impl2(int[] v) { return nodeCount1(v); } + private static native int nodeCount1(int[] a); + protected int[] varProfile_impl(int v) { return varProfile0(v); } + private static native int[] varProfile0(int b); + protected void printTable_impl(int v) { printTable0(v); } + private static native void printTable0(int b); - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#buildCube(int, java.util.List) - */ - public BDD buildCube(int value, List var) { - int[] a = toBuDDyArray(var); - int id = buildCube0(value, a); - return makeBDD(id); - } - private static native int buildCube0(int value, int[] var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#buildCube(int, int[]) - */ - public BDD buildCube(int value, int[] var) { - int id = buildCube1(value, var); - return makeBDD(id); - } - private static native int buildCube1(int value, int[] var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#makeSet(int[]) - */ - public BDDVarSet makeSet(int[] v) { - int id = makeSet0(v); - return makeBDDVarSet(id); - } - private static native int makeSet0(int[] var); + // More redirection functions. + public void addVarBlock(int first, int last, boolean fixed) { addVarBlock1(first, last, fixed); } + private static native void addVarBlock1(int first, int last, boolean fixed); + public void varBlockAll() { varBlockAll0(); } + private static native void varBlockAll0(); + public void clearVarBlocks() { clearVarBlocks0(); } + private static native void clearVarBlocks0(); + public void printOrder() { printOrder0(); } + private static native void printOrder0(); + public int getNodeTableSize() { return getAllocNum0(); } + private static native int getAllocNum0(); + public int getNodeNum() { return getNodeNum0(); } + private static native int getNodeNum0(); + public int getCacheSize() { return getCacheSize0(); } + private static native int getCacheSize0(); + public int reorderGain() { return reorderGain0(); } + private static native int reorderGain0(); + public void printStat() { printStat0(); } + private static native void printStat0(); + public void printAll() { printAll0(); } + private static native void printAll0(); + public void setVarOrder(int[] neworder) { setVarOrder0(neworder); } + private static native void setVarOrder0(int[] neworder); + public int level2Var(int level) { return level2Var0(level); } + private static native int level2Var0(int level); + public int var2Level(int var) { return var2Level0(var); } + private static native int var2Level0(int var); + public int getReorderTimes() { return getReorderTimes0(); } + private static native int getReorderTimes0(); + public void disableReorder() { disableReorder0(); } + private static native void disableReorder0(); + public void enableReorder() { enableReorder0(); } + private static native void enableReorder0(); + public int reorderVerbose(int v) { return reorderVerbose0(v); } + private static native int reorderVerbose0(int v); + public void reorder(ReorderMethod m) { reorder0(m.id); } + private static native void reorder0(int method); + public void autoReorder(ReorderMethod method) { autoReorder0(method.id); } + private static native void autoReorder0(int method); + public void autoReorder(ReorderMethod method, int max) { autoReorder1(method.id, max); } + private static native void autoReorder1(int method, int max); + public void swapVar(int v1, int v2) { swapVar0(v1, v2); } + private static native void swapVar0(int v1, int v2); + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#initialize(int, int) */ @@ -208,27 +236,13 @@ * @see net.sf.javabdd.BDDFactory#done() */ public void done() { - if (USE_FINALIZER) { - System.gc(); - System.runFinalization(); - } + super.done(); INSTANCE = null; done0(); } private static native void done0(); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reset() - */ - public void reset() { - if (USE_FINALIZER) { - System.gc(); - System.runFinalization(); - } - super.reset(); - } - - /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#setError(int) */ public void setError(int code) { @@ -317,78 +331,19 @@ private static native int setVarNum0(int num); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#duplicateVar(int) - */ - public int duplicateVar(int var) { - return duplicateVar0(var); - } - private static native int duplicateVar0(int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#extVarNum(int) - */ - public int extVarNum(int num) { - return extVarNum0(num); - } - private static native int extVarNum0(int num); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#ithVar(int) - */ - public BDD ithVar(int var) { - int id = ithVar0(var); - return makeBDD(id); - } - private static native int ithVar0(int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nithVar(int) - */ - public BDD nithVar(int var) { - int id = nithVar0(var); - return makeBDD(id); - } - private static native int nithVar0(int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#swapVar(int, int) - */ - public void swapVar(int v1, int v2) { - swapVar0(v1, v2); - } - private static native void swapVar0(int v1, int v2); - - /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#makePair() */ public BDDPairing makePair() { long ptr = makePair0(); if (USE_FINALIZER) { - return new BuDDyBDDPairingWithFinalizer(ptr); + return new BuDDyPairingWithFinalizer(ptr); } else { - return new BuDDyBDDPairing(ptr); + return new BuDDyPairing(ptr); } } private static native long makePair0(); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printAll() - */ - public void printAll() { - printAll0(); - } - private static native void printAll0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD) - */ - public void printTable(BDD b) { - BuDDyBDD bb = (BuDDyBDD) b; - printTable0(bb._id); - } - private static native void printTable0(int b); - - /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#load(java.lang.String) */ public BDD load(String filename) { @@ -401,52 +356,11 @@ * @see net.sf.javabdd.BDDFactory#save(java.lang.String, net.sf.javabdd.BDD) */ public void save(String filename, BDD b) { - BuDDyBDD bb = (BuDDyBDD) b; - save0(filename, bb._id); + save0(filename, unwrap(b)); } private static native void save0(String filename, int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#level2Var(int) - */ - public int level2Var(int level) { - return level2Var0(level); - } - private static native int level2Var0(int level); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#var2Level(int) - */ - public int var2Level(int var) { - return var2Level0(var); - } - private static native int var2Level0(int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void reorder(BDDFactory.ReorderMethod method) { - reorder0(method.id); - } - private static native void reorder0(int method); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void autoReorder(BDDFactory.ReorderMethod method) { - autoReorder0(method.id); - } - private static native void autoReorder0(int method); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int) - */ - public void autoReorder(BDDFactory.ReorderMethod method, int max) { - autoReorder1(method.id, max); - } - private static native void autoReorder1(int method, int max); - - /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#getReorderMethod() */ public BDDFactory.ReorderMethod getReorderMethod() { @@ -465,595 +379,18 @@ } private static native int getReorderMethod0(); - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getReorderTimes() - */ - public int getReorderTimes() { - return getReorderTimes0(); + static long unwrap(BDDPairing p) { + return ((BuDDyPairing)p)._ptr; } - private static native int getReorderTimes0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#disableReorder() - */ - public void disableReorder() { - disableReorder0(); - } - private static native void disableReorder0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#enableReorder() - */ - public void enableReorder() { - enableReorder0(); - } - private static native void enableReorder0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderVerbose(int) - */ - public int reorderVerbose(int v) { - return reorderVerbose0(v); - } - private static native int reorderVerbose0(int v); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setVarOrder(int[]) - */ - public void setVarOrder(int[] neworder) { - setVarOrder0(neworder); - } - private static native void setVarOrder0(int[] neworder); /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean) - */ - public void addVarBlock(BDD var, boolean fixed) { - BuDDyBDD bb = (BuDDyBDD) var; - addVarBlock0(bb._id, fixed); - } - private static native void addVarBlock0(int var, boolean fixed); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean) - */ - public void addVarBlock(int first, int last, boolean fixed) { - addVarBlock1(first, last, fixed); - } - private static native void addVarBlock1(int first, int last, boolean fixed); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#varBlockAll() - */ - public void varBlockAll() { - varBlockAll0(); - } - private static native void varBlockAll0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#clearVarBlocks() - */ - public void clearVarBlocks() { - clearVarBlocks0(); - } - private static native void clearVarBlocks0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printOrder() - */ - public void printOrder() { - printOrder0(); - } - private static native void printOrder0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection) - */ - public int nodeCount(Collection r) { - int[] a = toBuDDyArray(r); - return nodeCount0(a); - } - private static native int nodeCount0(int[] a); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeTableSize() - */ - public int getNodeTableSize() { - return getAllocNum0(); - } - private static native int getAllocNum0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getCacheSize() - */ - public int getCacheSize() { - return getCacheSize0(); - } - private static native int getCacheSize0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeNum() - */ - public int getNodeNum() { - return getNodeNum0(); - } - private static native int getNodeNum0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderGain() - */ - public int reorderGain() { - return reorderGain0(); - } - private static native int reorderGain0(); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printStat() - */ - public void printStat() { - printStat0(); - } - private static native void printStat0(); - - /* (non-Javadoc) - * An implementation of a BDD class, used by the BuDDy interface. - */ - private static class BuDDyBDD extends BDD { - - /** The value used by the BDD library. */ - protected int _id; - - /** An invalid id, for use in invalidating BDDs. */ - static final int INVALID_BDD = -1; - - protected BuDDyBDD(int id) { - _id = id; - addRef(_id); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#getFactory() - */ - public BDDFactory getFactory() { - return INSTANCE; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isZero() - */ - public boolean isZero() { - return _id == 0; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isOne() - */ - public boolean isOne() { - return _id == 1; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#var() - */ - public int var() { - return var0(_id); - } - private static native int var0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#high() - */ - public BDD high() { - int b = high0(_id); - return makeBDD(b); - } - private static native int high0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#low() - */ - public BDD low() { - int b = low0(_id); - return makeBDD(b); - } - private static native int low0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#id() - */ - public BDD id() { - return makeBDD(_id); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#not() - */ - public BDD not() { - int b = not0(_id); - return makeBDD(b); - } - private static native int not0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD) - */ - public BDD ite(BDD thenBDD, BDD elseBDD) { - BuDDyBDD c = (BuDDyBDD) thenBDD; - BuDDyBDD d = (BuDDyBDD) elseBDD; - int b = ite0(_id, c._id, d._id); - return makeBDD(b); - } - 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.BDDVarSet) - */ - public BDD relprod(BDD that, BDDVarSet var) { - BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; - int b = relprod0(_id, c._id, d._id); - return makeBDD(b); - } - private static native int relprod0(int b, int c, int d); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int) - */ - public BDD compose(BDD that, int var) { - BuDDyBDD c = (BuDDyBDD) that; - int b = compose0(_id, c._id, var); - return makeBDD(b); - } - private static native int compose0(int b, int c, int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD) - */ - public BDD constrain(BDD that) { - BuDDyBDD c = (BuDDyBDD) that; - int b = constrain0(_id, c._id); - return makeBDD(b); - } - private static native int constrain0(int b, int c); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) - */ - 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.BDDVarSet) - */ - 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.BDDVarSet) - */ - public BDD unique(BDDVarSet var) { - BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; - int b = unique0(_id, c._id); - return makeBDD(b); - } - private static native int unique0(int b, int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD) - */ - public BDD restrict(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; - int b = restrict0(_id, c._id); - return makeBDD(b); - } - private static native int restrict0(int b, int var); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD) - */ - public BDD restrictWith(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; - int b = restrict0(_id, c._id); - addRef(b); - delRef(_id); - if (this != c) { - delRef(c._id); - c._id = INVALID_BDD; - } - _id = b; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) - */ - public BDD simplify(BDDVarSet d) { - BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) d).b; - int b = simplify0(_id, c._id); - return makeBDD(b); - } - private static native int simplify0(int b, int d); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#support() - */ - public BDDVarSet support() { - int b = support0(_id); - return makeBDDVarSet(b); - } - private static native int support0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD apply(BDD that, BDDFactory.BDDOp opr) { - BuDDyBDD c = (BuDDyBDD) that; - int b = apply0(_id, c._id, opr.id); - return makeBDD(b); - } - private static native int apply0(int b, int c, int opr); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD applyWith(BDD that, BDDFactory.BDDOp opr) { - BuDDyBDD c = (BuDDyBDD) that; - int b = apply0(_id, c._id, opr.id); - addRef(b); - delRef(_id); - if (this != c) { - delRef(c._id); - c._id = INVALID_BDD; - } - _id = b; - return this; - } - - /* (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, BDDFactory.BDDOp opr, BDDVarSet var) { - BuDDyBDD c = (BuDDyBDD) that; - 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.BDDVarSet) - */ - public BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { - BuDDyBDD c = (BuDDyBDD) that; - 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.BDDVarSet) - */ - public BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { - BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; - int b = applyUni0(_id, c._id, opr.id, d._id); - return makeBDD(b); - } - private static native int applyUni0(int b, int c, int opr, int d); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne() - */ - public BDD satOne() { - int b = satOne0(_id); - return makeBDD(b); - } - private static native int satOne0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#fullSatOne() - */ - public BDD fullSatOne() { - int b = fullSatOne0(_id); - return makeBDD(b); - } - private static native int fullSatOne0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) - */ - 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); - } - private static native int satOne1(int b, int c, int d); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#printSet() - */ - public void printSet() { - printSet0(_id); - } - private static native void printSet0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#printDot() - */ - public void printDot() { - printDot0(_id); - } - private static native void printDot0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#nodeCount() - */ - public int nodeCount() { - return nodeCount0(_id); - } - private static native int nodeCount0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#pathCount() - */ - public double pathCount() { - return pathCount0(_id); - } - private static native double pathCount0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount() - */ - public double satCount() { - return satCount0(_id); - } - private static native double satCount0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount(net.sf.javabdd.BDDVarSet) - */ - 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); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#logSatCount() - */ - public double logSatCount() { - return logSatCount0(_id); - } - private static native double logSatCount0(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#logSatCount(net.sf.javabdd.BDDVarSet) - */ - 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); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#varProfile() - */ - public int[] varProfile() { - return varProfile0(_id); - } - private static native int[] varProfile0(int b); - - private static native void addRef(int b); - - private static native void delRef(int b); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#free() - */ - public void free() { - if (INSTANCE != null) { - delRef(_id); - } - _id = INVALID_BDD; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing) - */ - public BDD veccompose(BDDPairing pair) { - BuDDyBDDPairing p = (BuDDyBDDPairing) pair; - int b = veccompose0(_id, p._ptr); - return makeBDD(b); - } - private static native int veccompose0(int b, long p); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) - */ - public BDD replace(BDDPairing pair) { - BuDDyBDDPairing p = (BuDDyBDDPairing) pair; - int b = replace0(_id, p._ptr); - return makeBDD(b); - } - private static native int replace0(int b, long p); - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing) - */ - public BDD replaceWith(BDDPairing pair) { - BuDDyBDDPairing p = (BuDDyBDDPairing) pair; - int b = replace0(_id, p._ptr); - addRef(b); - delRef(_id); - _id = b; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD) - */ - public boolean equals(BDD that) { - return this._id == ((BuDDyBDD) that)._id; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#hashCode() - */ - public int hashCode() { - return this._id; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#toVarSet() - */ - public BDDVarSet toVarSet() { - return makeBDDVarSet(this._id); - } - - } - - private static class BuDDyBDDWithFinalizer extends BuDDyBDD { - - protected BuDDyBDDWithFinalizer(int id) { - super(id); - } - - /* Finalizer runs in different thread, and BuDDy is not thread-safe. - * Also, the existence of any finalize() method hurts performance - * considerably. - */ - /* (non-Javadoc) - * @see java.lang.Object#finalize() - */ - protected void finalize() throws Throwable { - super.finalize(); - if (_id >= 0) { - System.out.println("BDD not freed! "+System.identityHashCode(this)+" _id "+_id+" nodes: "+nodeCount()); - } - //this.free(); - } - static { - //System.runFinalizersOnExit(true); - } - } - - /* (non-Javadoc) * An implementation of a BDDPairing, used by the BuDDy interface. */ - private static class BuDDyBDDPairing extends BDDPairing { + private static class BuDDyPairing extends BDDPairing { private long _ptr; - private BuDDyBDDPairing(long ptr) { + private BuDDyPairing(long ptr) { this._ptr = ptr; } @@ -1077,8 +414,7 @@ * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) */ public void set(int oldvar, BDD newvar) { - BuDDyBDD c = (BuDDyBDD) newvar; - set2(_ptr, oldvar, c._id); + set2(_ptr, oldvar, unwrap(newvar)); } private static native void set2(long p, int oldvar, int newbdd); @@ -1086,8 +422,7 @@ * @see net.sf.javabdd.BDDPairing#set(int[], net.sf.javabdd.BDD[]) */ public void set(int[] oldvar, BDD[] newvar) { - int[] a = toBuDDyArray(Arrays.asList(newvar)); - set3(_ptr, oldvar, a); + set3(_ptr, oldvar, unwrap(Arrays.asList(newvar))); } private static native void set3(long p, int[] oldvar, int[] newbdds); @@ -1110,9 +445,9 @@ } - private static class BuDDyBDDPairingWithFinalizer extends BuDDyBDDPairing { + private static class BuDDyPairingWithFinalizer extends BuDDyPairing { - private BuDDyBDDPairingWithFinalizer(long ptr) { + private BuDDyPairingWithFinalizer(long ptr) { super(ptr); } Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-21 16:55:23 UTC (rev 463) @@ -208,7 +208,7 @@ return 0; } public boolean isInitialized() { return true; } - public void done() { bdd.cleanup(); bdd = null; } + public void done() { super.done(); bdd.cleanup(); bdd = null; } public void setError(int code) { // todo: implement this } Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-21 16:55:23 UTC (rev 463) @@ -188,7 +188,7 @@ 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 done() { super.done(); bdd_done(); } public void setError(int code) { bdderrorcond = code; } public void clearError() { bdderrorcond = 0; } public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); } @@ -3075,6 +3075,9 @@ gbc_handler(true, gcstats); } + // Handle nodes that were marked as free by finalizer. + handleDeferredFree(); + for (r = 0; r < bddrefstacktop; r++) bdd_mark(bddrefstack[r]); Modified: trunk/JavaBDD/net/sf/javabdd/MicroFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-21 14:32:13 UTC (rev 462) +++ trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-21 16:55:23 UTC (rev 463) @@ -188,7 +188,7 @@ public int setNodeTableSize(int size) { return bdd_setallocnum(size); } public int setCacheSize(int v) { return bdd_setcachesize(v); } public boolean isInitialized() { return bddrunning; } - public void done() { bdd_done(); } + public void done() { super.done(); bdd_done(); } public void setError(int code) { bdderrorcond = code; } public void clearError() { bdderrorcond = 0; } public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); } @@ -3217,6 +3217,9 @@ gcstats.num = gbcollectnum; gbc_handler(true, gcstats); + // Handle nodes that were marked as free by finalizer. + handleDeferredFree(); + for (r = 0; r < bddrefstacktop; r++) bdd_mark(bddrefstack[r]); This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-11-29 08:07:15
|
Revision: 468
http://svn.sourceforge.net/javabdd/?rev=468&view=rev
Author: joewhaley
Date: 2006-11-29 00:07:13 -0800 (Wed, 29 Nov 2006)
Log Message:
-----------
Improved ZDD support. load(), support(), quant methods now work.
Modified Paths:
--------------
trunk/JavaBDD/NQueens.java
trunk/JavaBDD/RubiksCube.java
trunk/JavaBDD/net/sf/javabdd/BDDDomain.java
trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
Modified: trunk/JavaBDD/NQueens.java
===================================================================
--- trunk/JavaBDD/NQueens.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/NQueens.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -58,7 +58,7 @@
}
if (B.varNum() < N * N) B.setVarNum(N * N);
- queen = B.one();
+ queen = B.universe();
int i, j;
@@ -108,7 +108,7 @@
}
static void build(int i, int j) {
- BDD a = B.one(), b = B.one(), c = B.one(), d = B.one();
+ BDD a = B.universe(), b = B.universe(), c = B.universe(), d = B.universe();
int k, l;
/* No one in the same column */
Modified: trunk/JavaBDD/RubiksCube.java
===================================================================
--- trunk/JavaBDD/RubiksCube.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/RubiksCube.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -159,7 +159,7 @@
}
static BDD buildInitial() {
- BDD b = bdd.one();
+ BDD b = bdd.universe();
for (int k=0; k<4; ++k) {
for (int i=0; i<n; ++i) {
b.andWith(bdd.getDomain(k*n + i).ithVar(k));
Modified: trunk/JavaBDD/net/sf/javabdd/BDDDomain.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -94,7 +94,7 @@
/* Encode V<=X-1. V is the variables in 'var' and X is the domain size */
BigInteger val = size().subtract(BigInteger.ONE);
- BDD d = factory.one();
+ BDD d = factory.universe();
int[] ivar = vars();
for (int n = 0; n < this.varNum(); n++) {
if (val.testBit(0))
@@ -128,7 +128,7 @@
BDDFactory bdd = getFactory();
if (value == 0L) {
- BDD result = bdd.one();
+ BDD result = bdd.universe();
int n;
for (n = 0; n < bits; n++) {
BDD b = bdd.ithVar(this.ivar[n]);
@@ -182,7 +182,7 @@
}
BDDFactory factory = getFactory();
- BDD e = factory.one();
+ BDD e = factory.universe();
int[] this_ivar = this.vars();
int[] that_ivar = that.vars();
@@ -226,7 +226,7 @@
}
BDDFactory factory = getFactory();
- BDD v = factory.one();
+ BDD v = factory.universe();
int[] ivar = this.vars();
for (int n = 0; n < ivar.length; n++) {
if (val.testBit(0))
@@ -257,7 +257,7 @@
BDD result = factory.zero();
int[] ivar = this.vars();
while (lo.compareTo(hi) <= 0) {
- BDD v = factory.one();
+ BDD v = factory.universe();
for (int n = ivar.length - 1; ; n--) {
if (lo.testBit(n)) {
v.andWith(factory.ithVar(ivar[n]));
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -84,6 +84,11 @@
return TestBDDFactory.init(nodenum, cachesize);
if (bddpackage.equals("typed"))
return TypedBDDFactory.init(nodenum, cachesize);
+ if (bddpackage.equals("zdd")) {
+ BDDFactory bdd = JFactory.init(nodenum, cachesize);
+ ((JFactory)bdd).ZDD = true;
+ return bdd;
+ }
} catch (LinkageError e) {
System.out.println("Could not load BDD package "+bddpackage+": "+e.getLocalizedMessage());
}
@@ -218,7 +223,7 @@
* <p>Compare to bdd_buildcube.</p>
*/
public BDD buildCube(int value, List/*<BDD>*/ variables) {
- BDD result = one();
+ BDD result = universe();
Iterator i = variables.iterator();
int z = 0;
while (i.hasNext()) {
@@ -240,7 +245,7 @@
* <p>Compare to bdd_ibuildcube./p>
*/
public BDD buildCube(int value, int[] variables) {
- BDD result = one();
+ BDD result = universe();
for (int z = 0; z < variables.length; z++, value >>= 1) {
BDD v;
if ((value & 0x1) != 0)
@@ -529,7 +534,7 @@
// Check for constant true / false
if (lh_nodenum == 0 && vnum == 0) {
int r = Integer.parseInt(readNext(ifile));
- return r == 0 ? zero() : one();
+ return r == 0 ? zero() : universe();
}
// Not actually used.
@@ -631,7 +636,7 @@
protected BDD loadhash_get(LoadHash[] lh_table, int lh_nodenum, int key) {
if (key < 0) return null;
if (key == 0) return zero();
- if (key == 1) return one();
+ if (key == 1) return universe();
int hash = lh_table[key % lh_nodenum].first;
@@ -1423,6 +1428,14 @@
}
}
+ if (isZDD()) {
+ // Need to rebuild varsets for existing domains.
+ for (n = 0; n < fdvarnum; n++) {
+ domain[n].var.free();
+ domain[n].var =
+ makeSet(domain[n].ivar);
+ }
+ }
for (n = 0; n < num; n++) {
domain[n + fdvarnum].var =
makeSet(domain[n + fdvarnum].ivar);
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -446,7 +446,7 @@
}
protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) {
- if (true || isZDD()) {
+ if (isZDD()) {
if (USE_FINALIZER)
return new IntZDDVarSetWithFinalizer(v);
else
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-13 07:25:37 UTC (rev 467)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-29 08:07:13 UTC (rev 468)
@@ -67,7 +67,7 @@
});
}
- boolean ZDD = true;
+ boolean ZDD = false;
/**
* Implementation of BDDPairing used by JFactory.
@@ -1561,14 +1561,11 @@
return l;
if (ISZERO(l) || ISZERO(r))
return 0;
- if (ISONE(l))
- return r;
- if (ISONE(r))
- return l;
if (LEVEL(l) < LEVEL(r))
return zand_rec(LOW(l), r);
else if (LEVEL(l) > LEVEL(r))
return zand_rec(l, LOW(r));
+ _assert(!ISCONST(l) && !ISCONST(r));
entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
@@ -1811,6 +1808,14 @@
if (var < 2) /* Empty set */
return bdd_apply(l, r, opr);
+ if (ZDD) {
+ // TODO: A real ZDD implementation.
+ int x = bdd_addref(bdd_apply(l, r, opr));
+ int y = bdd_exist(x, var);
+ bdd_delref(x);
+ return y;
+ }
+
if (applycache == null) applycache = BddCacheI_init(cachesize);
if (appexcache == null) appexcache = BddCacheI_init(cachesize);
if (quantcache == null) quantcache = BddCacheI_init(cachesize);
@@ -2144,14 +2149,12 @@
if (INVARSET(LEVEL(r))) {
int r2 = READREF(2), r1 = READREF(1);
switch (applyop) {
- case bddop_and: res = ZDD ? zand_rec(r2, r1) : and_rec(r2, r1); break;
- case bddop_or: res = ZDD ? zor_rec(r2, r1) : or_rec(r2, r1); break;
+ case bddop_and: res = and_rec(r2, r1); break;
+ case bddop_or: res = or_rec(r2, r1); break;
default: res = apply_rec(r2, r1); break;
}
} else {
- res = ZDD
- ? zdd_makenode(LEVEL(r), READREF(2), READREF(1))
- : bdd_makenode(LEVEL(r), READREF(2), READREF(1));
+ res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
}
POPREF(2);
@@ -2163,6 +2166,45 @@
return res;
}
+ int zquant_rec(int r) {
+ BddCacheDataI entry;
+ int res;
+
+ if (r < 2 || LEVEL(r) > quantlast)
+ return r;
+
+ entry = BddCache_lookupI(quantcache, QUANTHASH(r));
+ if (entry.a == r && entry.c == quantid) {
+ if (CACHESTATS)
+ cachestats.opHit++;
+ return entry.res;
+ }
+ if (CACHESTATS)
+ cachestats.opMiss++;
+
+ PUSHREF(zquant_rec(LOW(r)));
+ PUSHREF(zquant_rec(HIGH(r)));
+
+ if (INVARSET(LEVEL(r))) {
+ int r2 = READREF(2), r1 = READREF(1);
+ switch (applyop) {
+ case bddop_and: res = zand_rec(r2, r1); break;
+ case bddop_or: res = zor_rec(r2, r1); break;
+ default: throw new BDDException();
+ }
+ } else {
+ res = zdd_makenode(LEVEL(r), READREF(2), READREF(1));
+ }
+
+ POPREF(2);
+
+ entry.a = r;
+ entry.c = quantid;
+ entry.res = res;
+
+ return res;
+ }
+
int bdd_constrain(int f, int c) {
int res;
int numReorder = 1;
@@ -2706,7 +2748,10 @@
supportMin = LEVEL(r);
supportMax = supportMin;
- support_rec(r, supportSet);
+ if (ZDD)
+ zsupport_rec(r, 0, supportSet);
+ else
+ support_rec(r, supportSet);
bdd_unmark(r);
bdd_disable_reorder();
@@ -2715,7 +2760,7 @@
if (supportSet[n] == supportID) {
int tmp;
bdd_addref(res);
- tmp = bdd_makenode(n, 0, res);
+ tmp = makenode_impl(n, 0, res);
bdd_delref(res);
res = tmp;
}
@@ -2727,6 +2772,8 @@
void support_rec(int r, int[] support) {
+ _assert(!ZDD);
+
if (r < 2)
return;
@@ -2744,6 +2791,41 @@
support_rec(HIGH(r), support);
}
+ void zsupport_rec(int r, int lev, int[] support) {
+
+ _assert(ZDD);
+
+ if (!ISZERO(r)) {
+ while (lev != LEVEL(r)) {
+ if (lev > supportMax)
+ supportMax = lev;
+ support[lev++] = supportID;
+ }
+ }
+
+ if (r < 2)
+ return;
+
+ if (MARKED(r) || LOW(r) == INVALID_BDD)
+ return;
+
+ if (LOW(r) == HIGH(r)) {
+ SETMARK(r);
+ zsupport_rec(LOW(r), LEVEL(r)+1, support);
+ return;
+ }
+
+ support[LEVEL(r)] = supportID;
+
+ if (LEVEL(r) > supportMax)
+ supportMax = LEVEL(r);
+
+ SETMARK(r);
+
+ zsupport_rec(LOW(r), LEVEL(r)+1, support);
+ zsupport_rec(HIGH(r), LEVEL(r)+1, support);
+ }
+
int bdd_appall(int l, int r, int opr, int var) {
int res;
int numReorder = 1;
@@ -4952,6 +5034,15 @@
bdd_pairs_resize(oldbddvarnum, bddvarnum);
bdd_operator_varresize();
+ if (ZDD) {
+ System.out.println("Changed number of ZDD variables, all existing ZDDs are now invalid.");
+ // Need to rebuild varsets for existing domains.
+ for (int n = 0; n < fdvarnum; n++) {
+ domain[n].var.free();
+ domain[n].var = makeSet(domain[n].ivar);
+ }
+ }
+
bdd_enable_reorder();
return 0;
@@ -5888,7 +5979,6 @@
int next;
}
- // TODO: revisit for zdd
int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException {
int key, var, low, high, root = 0, n;
@@ -5908,6 +5998,12 @@
if (low < 0 || high < 0 || var < 0)
return bdd_error(BDD_FORMAT);
+ if (ZDD) {
+ // The terminal "1" in BDD means universal set.
+ if (low == 1) low = univ;
+ if (high == 1) high = univ;
+ }
+
root = bdd_addref(bdd_ite(bdd_ithvar(var), high, low));
loadhash_add(key, root);
@@ -5962,6 +6058,7 @@
return;
}
+ // TODO: revisit for ZDD
void bdd_save_rec(BufferedWriter out, int root) throws IOException {
if (root < 2)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <joe...@us...> - 2007-03-06 06:08:41
|
Revision: 476
http://svn.sourceforge.net/javabdd/?rev=476&view=rev
Author: joewhaley
Date: 2007-03-05 22:08:40 -0800 (Mon, 05 Mar 2007)
Log Message:
-----------
Added new UberMicroFactory.
Fixed setCacheRatio().
Added Intel compiler flag to optimize for Core 2 Duo processors.
Other small cleanups.
Modified Paths:
--------------
trunk/JavaBDD/Makefile
trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
Added Paths:
-----------
trunk/JavaBDD/net/sf/javabdd/BitString.java
trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java
Modified: trunk/JavaBDD/Makefile
===================================================================
--- trunk/JavaBDD/Makefile 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/Makefile 2007-03-06 06:08:40 UTC (rev 476)
@@ -35,7 +35,7 @@
CUDD_DLL_NAME = cudd.dll
CAL_DLL_NAME = cal.dll
ifeq (${CC},icl) # Intel Windows compiler
- CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND -DSMALL_NODES /O2 /Ob2 $(EXTRA_CFLAGS)
+ CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND -DSMALL_NODES /O2 /Ob2 /QxT $(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
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -76,7 +76,9 @@
return CALFactory.init(nodenum, cachesize);
if (bddpackage.equals("j") || bddpackage.equals("java"))
return JFactory.init(nodenum, cachesize);
- if (bddpackage.equals("u") || bddpackage.equals("micro"))
+ if (bddpackage.equals("u"))
+ return UberMicroFactory.init(nodenum, cachesize);
+ if (bddpackage.equals("micro"))
return MicroFactory.init(nodenum, cachesize);
if (bddpackage.equals("jdd"))
return JDDFactory.init(nodenum, cachesize);
@@ -1278,6 +1280,12 @@
sb.append("Unique Chain: ");
sb.append(uniqueChain);
sb.append(newLine);
+ sb.append("=> Ave. chain = ");
+ if (uniqueAccess > 0)
+ sb.append(((float) uniqueChain) / ((float) uniqueAccess));
+ else
+ sb.append((float)0);
+ sb.append(newLine);
sb.append("Unique Hit: ");
sb.append(uniqueHit);
sb.append(newLine);
@@ -1830,7 +1838,11 @@
}
protected static void bdd_default_gbchandler(boolean pre, GCStats s) {
- if (!pre) {
+ if (pre) {
+ if (s.freenodes != 0)
+ System.err.println("Starting GC cycle #"+(s.num+1)+
+ ": "+s.nodes+" nodes / "+s.freenodes+" free");
+ } else {
System.err.println(s.toString());
}
}
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -209,12 +209,10 @@
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);
+ if (false && v != invalid_bdd_impl()) {
+ System.out.println("BDD not freed! "+System.identityHashCode(this));
}
+ deferredFree(v);
}
}
@@ -347,12 +345,10 @@
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);
+ if (false && v != invalid_bdd_impl()) {
+ System.out.println("BDD not freed! "+System.identityHashCode(this));
}
+ deferredFree(v);
}
}
@@ -524,6 +520,8 @@
protected /*bdd*/int[] to_free = new /*bdd*/int[8];
protected /*bdd*/int to_free_length = 0;
public void deferredFree(int v) {
+ if (v == invalid_bdd_impl())
+ return;
synchronized(to_free) {
if (to_free_length == to_free.length) {
/*bdd*/int[] t = new /*bdd*/int[to_free.length * 2];
Modified: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -34,7 +34,16 @@
public abstract int[] toLevelArray();
public String toString() {
- return Arrays.toString(toArray());
+ //return Arrays.toString(toArray());
+ int[] a = toArray();
+ StringBuffer sb = new StringBuffer(a.length * 4 + 2);
+ sb.append('[');
+ for (int i = 0; i < a.length; ++i) {
+ if (i != 0) sb.append(',');
+ sb.append(a[i]);
+ }
+ sb.append(']');
+ return sb.toString();
}
/**
Added: trunk/JavaBDD/net/sf/javabdd/BitString.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BitString.java (rev 0)
+++ trunk/JavaBDD/net/sf/javabdd/BitString.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -0,0 +1,805 @@
+// BitString.java, created Wed May 16 17:26:33 2001 by joewhaley
+// Copyright (C) 2001-3 John Whaley <jw...@al...>
+// Licensed under the terms of the GNU LGPL; see COPYING for details.
+package net.sf.javabdd;
+
+import java.util.Iterator;
+
+/**
+ * <code>BitString</code> implements a vector of bits much like <code>java.util.BitSet</code>,
+ * except that this implementation actually works. Also, <code>BitString</code>
+ * has some groovy features which <code>BitSet</code> doesn't; mostly related to
+ * efficient iteration over <code>true</code> and <code>false</code> components.
+ * <p>
+ * Each component of the <code>BitString</code> has a boolean value.
+ * The bits of a <code>BitString</code> are indexed by non-negative
+ * integers (that means they are zero-based, of course). Individual
+ * indexed bits can be examined, set, or cleared. One
+ * <code>BitString</code> may be used to modify the contents of another
+ * <code>BitString</code> through logical AND, logical inclusive OR,
+ * and logical exclusive OR operations.
+ * <p>
+ * By default, all bits in the set initially have the value
+ * <code>false</code>.
+ * <p>
+ * Every bit set has a current size, which is the number of bits of
+ * space currently in use by the bit set. Note that the size is related
+ * to the implementation of a bit set, so it may change with implementation.
+ * The length of a bit set related to the logical length of a bit set
+ * and is defined independently of implementation.
+ *
+ * @author John Whaley <jw...@al...>
+ * @version $Id: BitString.java 2279 2005-05-28 10:24:54Z joewhaley $
+ */
+public final class BitString implements Cloneable, java.io.Serializable {
+
+ /**
+ * Version ID for serialization.
+ */
+ private static final long serialVersionUID = 3257570590025265971L;
+
+ /* There are 2^BITS_PER_UNIT bits in each unit (int) */
+ private static final int BITS_PER_UNIT = 5;
+ private static final int MASK = (1 << BITS_PER_UNIT) - 1;
+ private int[] bits;
+
+ /**
+ * Convert bitIndex to a subscript into the bits[] array.
+ */
+ private static int subscript(int bitIndex) {
+ return bitIndex >> BITS_PER_UNIT;
+ }
+
+ /**
+ * Creates an empty string with the specified size.
+ * @param nbits the size of the string
+ */
+ public BitString(int nbits) {
+ /* subscript(nbits + MASK) is the length of the array needed to hold
+ * nbits. Can also be written 1+subscript(nbits-1). */
+ bits = new int[subscript(nbits + MASK)];
+ }
+
+ /**
+ * Returns the first index in the bit string which is set, or
+ * -1 if there is no such index.
+ */
+ public int firstSet() {
+ return firstSet(-1);
+ }
+
+ /**
+ * Returns the first index greater than <code>where</code> in the
+ * bit string which is set, or -1 if there is no such index.
+ * @param where the starting point for the search. May be negative.
+ */
+ public int firstSet(int where) {
+ // convert exclusive starting point to inclusive starting point
+ where = (where < -1) ? 0 : (where + 1);
+ // search in first unit is masked.
+ int mask = (~0) << (where & MASK);
+ // search through units
+ for (int i = subscript(where); i < bits.length; i++, mask = ~0) {
+ int unit = bits[i] & mask;
+ if (unit != 0) return (i << BITS_PER_UNIT) + (bsf(unit) - 1);
+ }
+ return -1;
+ }
+
+ /**
+ * Utility function to return the number of 1 bits in the given integer
+ * value.
+ *
+ * @param b value to check
+ * @return byte number of one bits
+ */
+ public static final byte popcount(int b) {
+ int t, x;
+ x = b;
+ x = x - ((x >> 1) & 0x55555555);
+ t = ((x >> 2) & 0x33333333);
+ x = (x & 0x33333333) + t;
+ x = (x + (x >> 4)) & 0x0F0F0F0F;
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ return (byte) x;
+ }
+
+ /**
+ * Utility function to return the number of 1 bits in the given long value.
+ *
+ * @param b value to check
+ * @return byte number of one bits
+ */
+ public static final byte popcount(long b) {
+ long t, x;
+ x = b;
+ x = x - ((x >> 1) & 0x5555555555555555L);
+ t = ((x >> 2) & 0x3333333333333333L);
+ x = (x & 0x3333333333333333L) + t;
+ x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0FL;
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ x = x + (x >> 32);
+ return (byte) x;
+ }
+
+ /**
+ * Utility function to return the index of the first (lowest-order) one bit
+ * in the given integer. Returns zero if the given number is zero.
+ *
+ * @param b value to check
+ * @return byte index of first one bit, or zero if the number is zero
+ */
+ public static final int bsf(int b) {
+ int t = ~(b | -b);
+ return popcount(t);
+ }
+
+ /**
+ * Utility function to return the index of the last one bit in the given
+ * integer. Returns zero if the given number is zero.
+ *
+ * @param v value to check
+ * @return byte index of first one bit, or zero if the number is zero
+ */
+ public static final int bsr(int v) {
+ if ((v & 0xFFFF0000) != 0) {
+ if ((v & 0xFF000000) != 0)
+ return 24 + bytemsb[(v >> 24) & 0xFF];
+ else
+ return 16 + bytemsb[v >> 16];
+ }
+ if ((v & 0x0000FF00) != 0)
+ return 8 + bytemsb[v >> 8];
+ else
+ return bytemsb[v];
+ }
+
+ /** Highest bit set in a byte. */
+ private static final byte bytemsb[] = {0, 1, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8 /* 256 */};
+
+ /**
+ * Returns the last index less than <code>where</code> in the
+ * bit string which is set, or -1 if there is no such index.
+ * @param where the starting point for the search.
+ */
+ public int lastSet(int where) {
+ // convert exclusive starting point to inclusive starting point
+ if (--where < 0) return -1;
+ int start = (bits.length - 1), mask = ~0;
+ if (subscript(where) < bits.length) {
+ // search in first unit is masked.
+ start = subscript(where);
+ mask = (~0) >>> (MASK - (where & mask));
+ }
+ // search through units
+ for (int i = start; i >= 0; i--, mask = ~0) {
+ int unit = bits[i] & mask;
+ if (unit != 0) return (i << BITS_PER_UNIT) + (bsr(unit) - 1);
+ }
+ return -1;
+ }
+
+ /**
+ * Returns the last index in the bit string which is set, or
+ * -1 if there is no such index.
+ */
+ public int lastSet() {
+ return lastSet(size());
+ }
+
+ /**
+ * Sets all bits.
+ */
+ public void setAll() {
+ int i = bits.length;
+ while (i-- > 0) {
+ bits[i] = ~0;
+ }
+ }
+
+ /**
+ * Sets all bits up to and including the given bit.
+ * @param bit the bit to be set up to (zero-based)
+ */
+ public void setUpTo(int bit) {
+ int where = subscript(bit);
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where] |= ((1 << ((bit + 1) & MASK)) - 1);
+ while (where-- > 0) {
+ bits[where] = ~0;
+ }
+ }
+
+ public void setRange(int lo, int hi) {
+ int where1 = subscript(lo);
+ int where2 = subscript(hi);
+ if (where1 == where2) {
+ for ( ; lo <= hi; ++lo)
+ bits[where1] |= (1 << (lo & MASK));
+ } else {
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where2] |= ((1 << ((hi + 1) & MASK)) - 1);
+ while (--where2 > where1) {
+ bits[where2] = ~0;
+ }
+ bits[where1] |= -(1 << (lo & MASK));
+ }
+ }
+
+ /**
+ * Sets a bit.
+ * @param bit the bit to be set (zero-based)
+ */
+ public void set(int bit) {
+ bits[subscript(bit)] |= (1 << (bit & MASK));
+ }
+
+ /**
+ * Clears all bits.
+ */
+ public void clearAll() {
+ int i = bits.length;
+ while (i-- > 0) {
+ bits[i] = 0;
+ }
+ }
+
+ /**
+ * Clears all bits up to and including the given bit.
+ * @param bit the bit to be set up to (zero-based)
+ */
+ public void clearUpTo(int bit) {
+ int where = subscript(bit);
+ /* preaddition of 1 to bit is a clever hack to avoid long arithmetic */
+ bits[where] &= ~((1 << ((bit + 1) & MASK)) - 1);
+ while (where-- > 0) {
+ bits[where] = 0;
+ }
+ }
+
+ /**
+ * Clears a bit.
+ * @param bit the bit to be cleared (zero-based)
+ */
+ public void clear(int bit) {
+ bits[subscript(bit)] &= ~(1 << (bit & MASK));
+ }
+
+ /**
+ * Gets a bit.
+ * @param bit the bit to be gotten (zero-based)
+ */
+ public boolean get(int bit) {
+ int n = subscript(bit);
+ return ((bits[n] & (1 << (bit & MASK))) != 0);
+ }
+
+ /**
+ * Logically ANDs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ANDed with
+ */
+ public boolean and(BitString set) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ int n = bits.length;
+ boolean changed = false;
+ for (int i = n; i-- > 0;) {
+ int old = bits[i];
+ bits[i] &= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically ORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ORed with
+ */
+ public boolean or(BitString set) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ int setLength = set.bits.length;
+ boolean changed = false;
+ for (int i = setLength; i-- > 0;) {
+ int old = bits[i];
+ bits[i] |= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically ORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be ORed with
+ */
+ public boolean or_upTo(BitString set, int bit) {
+ if (this == set) { // should help alias analysis
+ return false;
+ }
+ boolean result;
+ int where = subscript(bit);
+ int old = bits[where];
+ bits[where] |= (set.bits[where] & ((1 << ((bit + 1) & MASK)) - 1));
+ result = (bits[where] != old);
+ while (where-- > 0) {
+ old = bits[where];
+ bits[where] |= set.bits[where];
+ result |= (bits[where] != old);
+ }
+ return result;
+ }
+
+ /**
+ * Logically XORs this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to be XORed with
+ */
+ public boolean xor(BitString set) {
+ int setLength = set.bits.length;
+ boolean changed = false;
+ for (int i = setLength; i-- > 0;) {
+ int old = bits[i];
+ bits[i] ^= set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Logically subtracts this bit set with the specified set of bits.
+ * Returns <code>true</code> if <code>this</code> was modified in
+ * response to the operation.
+ * @param set the bit set to subtract
+ */
+ public boolean minus(BitString set) {
+ int n = bits.length;
+ boolean changed = false;
+ for (int i = n; i-- > 0;) {
+ int old = bits[i];
+ bits[i] &= ~set.bits[i];
+ changed |= (old != bits[i]);
+ }
+ return changed;
+ }
+
+ /**
+ * Check if the intersection of the two sets is empty
+ * @param other the set to check intersection with
+ */
+ public boolean intersectionEmpty(BitString other) {
+ int n = bits.length;
+ for (int i = n; i-- > 0;) {
+ if ((bits[i] & other.bits[i]) != 0) return false;
+ }
+ return true;
+ }
+
+ /**
+ * Check if this set contains all bits of the given set.
+ * @param other the set to check containment with
+ */
+ public boolean contains(BitString other) {
+ int n = bits.length;
+ for (int i = n; i-- > 0;) {
+ if ((bits[i] & other.bits[i]) != other.bits[i]) return false;
+ }
+ return true;
+ }
+
+ private static void shld(int[] bits, int i1, int i2, int amt) {
+ //Assert._assert(amt >= 0 && amt < BITS_PER_UNIT);
+ bits[i1] = (bits[i1] << amt) | ((bits[i2] << (BITS_PER_UNIT - amt)) >> (BITS_PER_UNIT - amt));
+ }
+
+ /**
+ * Performs a left-shift operation.
+ * @param amt number of bits to shift, can be negative
+ */
+ public void shl(int amt) {
+ final int div = amt >> BITS_PER_UNIT;
+ final int mod = amt & MASK;
+ final int size = bits.length;
+ if (amt < 0) {
+ shr(-amt); return;
+ }
+ // big moves
+ if (div > 0) {
+ System.arraycopy(bits, 0, bits, div, size - div);
+ for (int i = 0; i < div; ++i)
+ bits[i] = 0;
+ /*
+ int i;
+ for (i = size - 1; i >= div; --i) {
+ bits[i] = bits[i - div];
+ }
+ for (; i >= 0; --i) {
+ bits[i] = 0;
+ }
+ */
+ }
+ // small moves
+ if (mod > 0) {
+ int i;
+ for (i = size - 1; i > div; --i) {
+ shld(bits, i, i - 1, mod);
+ }
+ bits[i] <<= mod;
+ }
+ }
+
+ private static void shrd(int[] bits, int i1, int i2, int amt) {
+ //Assert._assert(amt >= 0 && amt < BITS_PER_UNIT);
+ bits[i1] = (bits[i1] >>> amt) | ((bits[i2] >>> (BITS_PER_UNIT - amt)) << (BITS_PER_UNIT - amt));
+ }
+
+ /**
+ * Performs a right-shift operation.
+ * @param amt number of bits to shift
+ */
+ public void shr(int amt) {
+ final int div = amt >> BITS_PER_UNIT;
+ final int mod = amt & MASK;
+ final int size = bits.length;
+ // big moves
+ if (div > 0) {
+ System.arraycopy(bits, div, bits, 0, size - div);
+ for (int i = size-div; i < size; ++i)
+ bits[i] = 0;
+ /*
+ int i;
+ for (i = 0; i < size - div; ++i) {
+ bits[i] = bits[i + div];
+ }
+ for (; i < size; ++i) {
+ bits[i] = 0;
+ }
+ */
+ }
+ // small moves
+ if (mod > 0) {
+ int i;
+ for (i = 0; i < size - div - 1; ++i) {
+ shrd(bits, i, i + 1, mod);
+ }
+ bits[i] >>>= mod;
+ }
+ }
+
+ /**
+ * Copies the values of the bits in the specified set into this set.
+ * @param set the bit set to copy the bits from
+ */
+ public void copyBits(BitString set) {
+ System.arraycopy(set.bits, 0, bits, 0, Math.min(bits.length, set.bits.length));
+ }
+
+ /**
+ * Returns a hash code value for this bit string whose value depends
+ * only on which bits have been set within this <code>BitString</code>.
+ */
+ public int hashCode() {
+ int h = 1234;
+ for (int i = bits.length; --i >= 0;) {
+ h ^= bits[i] * (i + 1);
+ }
+ return h;
+ }
+
+ /**
+ * Returns the "logical size" of this <code>BitString</code>: the
+ * index of the highest set bit in the <code>BitString</code> plus
+ * one. Returns zero if the <code>BitString</code> contains no
+ * set bits.
+ */
+ public int length() {
+ return lastSet() + 1;
+ }
+
+ /**
+ * Returns the number of bits of space actually in use by this
+ * <code>BitString</code> to represent bit values.
+ * The maximum element in the set is the size - 1st element.
+ * The minimum element in the set is the zero'th element.
+ */
+ public int size() {
+ return bits.length << BITS_PER_UNIT;
+ }
+
+ /**
+ * Compares this object against the specified object.
+ * @param obj the object to compare with
+ * @return true if the contents of the bitsets are the same; false otherwise.
+ */
+ public boolean equals(Object obj) {
+ BitString set;
+ if (obj == null) return false;
+ if (this == obj) return true; //should help alias analysis
+ try {
+ set = (BitString) obj;
+ } catch (ClassCastException e) {
+ return false;
+ }
+ if (length() != set.length()) return false;
+ int n = bits.length - 1;
+ while (n >= 0 && bits[n] == 0) n--;
+ // now n has the first non-zero entry
+ for (int i = n; i >= 0; i--) {
+ if (bits[i] != set.bits[i]) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ /**
+ * Returns whether this <code>BitString</code> is all zeroes.
+ * @return true if it is all zeroes.
+ */
+ public boolean isZero() {
+ int setLength = bits.length;
+ for (int i = setLength; i-- > 0;) {
+ if (bits[i] != 0) return false;
+ }
+ return true;
+ }
+
+ /**
+ * Returns the number of ones in this <code>BitString</code>.
+ * @return number of bits set.
+ */
+ public int numberOfOnes() {
+ int setLength = bits.length;
+ int number = 0;
+ for (int i = setLength; i-- > 0;) {
+ number += popcount(bits[i]);
+ }
+ return number;
+ }
+
+ /**
+ * Returns the number of ones in this <code>BitString</code> up to a given index.
+ * @return number of bits set.
+ */
+ public int numberOfOnes(int where) {
+ int setLength = subscript(where);
+ int number = 0;
+ for (int i = setLength; i-- > 0;) {
+ number += popcount(bits[i]);
+ }
+ number += popcount(bits[setLength] & ((1 << ((where + 1) & MASK)) - 1));
+ return number;
+ }
+
+ /**
+ * Clones the BitString.
+ */
+ public Object clone() {
+ BitString result = null;
+ try {
+ result = (BitString) super.clone();
+ } catch (CloneNotSupportedException e) {
+ // this shouldn't happen, since we are Cloneable
+ throw new InternalError();
+ }
+ result.bits = new int[bits.length];
+ System.arraycopy(bits, 0, result.bits, 0, result.bits.length);
+ return result;
+ }
+
+ /**
+ * Converts the BitString to a String.
+ */
+ public String toString() {
+ StringBuffer buffer = new StringBuffer();
+ boolean needSeparator = false;
+ buffer.append('{');
+ for (ForwardBitStringIterator i=iterator(); i.hasNext(); ) {
+ int x = i.nextIndex();
+ if (needSeparator) {
+ buffer.append(", ");
+ } else {
+ needSeparator = true;
+ }
+ buffer.append(x);
+ }
+ buffer.append('}');
+ return buffer.toString();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in forward order.
+ */
+ public ForwardBitStringIterator iterator() {
+ return new ForwardBitStringIterator();
+ }
+
+ public ForwardBitStringZeroIterator zeroIterator() {
+ return new ForwardBitStringZeroIterator();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in backward order.
+ */
+ public BackwardBitStringIterator backwardsIterator() {
+ return new BackwardBitStringIterator();
+ }
+
+ /**
+ * Returns an iterator that iterates through the bits in backward order,
+ * starting at the given index.
+ */
+ public BackwardBitStringIterator backwardsIterator(int i) {
+ return new BackwardBitStringIterator(i);
+ }
+
+ /**
+ * Abstract bit string iterator class.
+ */
+ public abstract static class BitStringIterator implements Iterator {
+
+ /**
+ * Returns the index of the next bit set.
+ */
+ public abstract int nextIndex();
+
+ /**
+ * @see java.util.Iterator#next()
+ */
+ public final Object next() {
+ return new Integer(nextIndex());
+ }
+
+ public void remove() {
+ throw new UnsupportedOperationException("Unmodifiable Iterator");
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in forward order.
+ */
+ public class ForwardBitStringIterator extends BitStringIterator {
+ private int j, k, t;
+
+ ForwardBitStringIterator() {
+ j = 0;
+ k = 0;
+ t = bits[0];
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == bits.length - 1) return false;
+ t = bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == bits.length - 1) throw new java.util.NoSuchElementException();
+ t = bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ int t2 = (t ^ (-t));
+ int index = 31 - popcount(t2);
+ t &= t2;
+ return k + index;
+ /*
+ int t2 = ~(t | (-t));
+ int index = popcount(t2);
+ t &= ~(t2 + 1);
+ return k + index;
+ */
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in forward order.
+ */
+ public class ForwardBitStringZeroIterator extends BitStringIterator {
+ private int j, k, t;
+
+ ForwardBitStringZeroIterator() {
+ j = 0;
+ k = 0;
+ t = ~bits[0];
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == bits.length - 1) return false;
+ t = ~bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == bits.length - 1) throw new java.util.NoSuchElementException();
+ t = ~bits[++j];
+ k += 1 << BITS_PER_UNIT;
+ }
+ int t2 = (t ^ (-t));
+ int index = 31 - popcount(t2);
+ t &= t2;
+ return k + index;
+ }
+
+ }
+
+ /**
+ * Iterator for iterating through a bit string in backward order.
+ */
+ public class BackwardBitStringIterator extends BitStringIterator {
+ private int j, k, t;
+
+ BackwardBitStringIterator(int i) {
+ j = subscript(i);
+ t = bits[j];
+ t &= (1 << ((i + 1) & MASK)) - 1;
+ k = j << BITS_PER_UNIT;
+ }
+
+ BackwardBitStringIterator() {
+ j = bits.length - 1;
+ t = bits[j];
+ k = j << BITS_PER_UNIT;
+ }
+
+ /**
+ * @see java.util.Iterator#hasNext()
+ */
+ public boolean hasNext() {
+ while (t == 0) {
+ if (j == 0) {
+ return false;
+ }
+ t = bits[--j];
+ k -= 1 << BITS_PER_UNIT;
+ }
+ return true;
+ }
+
+ /**
+ * @see jwutil.math.BitString.BitStringIterator#nextIndex()
+ */
+ public int nextIndex() {
+ while (t == 0) {
+ if (j == 0) throw new java.util.NoSuchElementException();
+ t = bits[--j];
+ k -= 1 << BITS_PER_UNIT;
+ }
+ int index = bsr(t) - 1;
+ t &= ~(1 << index);
+ return k + index;
+ }
+
+ }
+}
Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -295,7 +295,7 @@
* @see net.sf.javabdd.BDDFactory#setCacheRatio(int)
*/
public double setCacheRatio(double x) {
- return setCacheRatio0((int)(x * 100.)) / 100.;
+ return setCacheRatio0((int)x);
}
private static native int setCacheRatio0(int x);
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-05 10:59:01 UTC (rev 475)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -214,7 +214,7 @@
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 double setCacheRatio(double x) { return bdd_setcacheratio((int)x); }
public int varNum() { return bdd_varnum(); }
public int setVarNum(int num) { return bdd_setvarnum(num); }
public void printAll() { bdd_fprintall(System.out); }
@@ -1431,7 +1431,7 @@
}
checkresize();
- if (true) bdd_validate(res);
+ if (false) bdd_validate(res);
return res;
}
@@ -2574,7 +2574,7 @@
}
checkresize();
- if (true) bdd_validate(res);
+ if (false) bdd_validate(res);
return res;
}
@@ -5331,21 +5331,28 @@
resizedInMakenode = false;
if (imatrixDepends(iactmtx, var, bddlevel2var[level + 1])) {
+ // This var depends on the next one.
+ // (ie there is some BDD with both this var and the next one)
+
+ // Rehash this level and return a list of nodes that depend on the
+ // next level.
int toBeProcessed = reorder_downSimple(var);
levelData l = levels[var];
if (l.nodenum < (l.size) / 3
|| l.nodenum >= (l.size * 3) / 2
&& l.size < l.maxsize) {
+ // Hash table for this level is too big or too small, resize it.
reorder_swapResize(toBeProcessed, var);
reorder_localGbcResize(toBeProcessed, var);
} else {
+ // Swap the variable and do a GC pass on this level.
reorder_swap(toBeProcessed, var);
reorder_localGbc(var);
}
}
- /* Swap the var<->level tables */
+ // Swap the var<->level tables
n = bddlevel2var[level];
bddlevel2var[level] = bddlevel2var[level + 1];
bddlevel2var[level + 1] = n;
@@ -5439,13 +5446,17 @@
int reorder_downSimple(int var0) {
int toBeProcessed = 0;
+
+ // Next variable to swap with.
int var1 = bddlevel2var[bddvar2level[var0] + 1];
+
+ // Hash table range for source variable.
int vl0 = levels[var0].start;
int size0 = levels[var0].size;
int n;
+ // Rehash this level and recalculate the number of nodes.
levels[var0].nodenum = 0;
-
for (n = 0; n < size0; n++) {
int r;
@@ -5455,26 +5466,17 @@
while (r != 0) {
int next = NEXT(r);
-/***
- if (LOW(r) == -1) {
- System.out.println(r+": LOW="+LOW(r));
- }
- if (HIGH(r) == -1) {
- System.out.println(r+": HIGH="+HIGH(r));
- }
-***/
if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
- /* Node does not depend on next var, let it stay in the chain */
+ // Node does not depend on next var, put it in the chain
SETNEXT(r, HASH(n + vl0));
SETHASH(n + vl0, r);
levels[var0].nodenum++;
} else {
- /* Node depends on next var - save it for later procesing */
+ // Node depends on next var - save it for later processing
SETNEXT(r, toBeProcessed);
toBeProcessed = r;
if (SWAPCOUNT)
cachestats.swapCount++;
-
}
r = next;
@@ -5493,7 +5495,7 @@
int f1 = HIGH(toBeProcessed);
int f00, f01, f10, f11;
- /* Find the cofactors for the new nodes */
+ // Find the cofactors for the new nodes
if (VARr(f0) == var1) {
f00 = LOW(f0);
f01 = HIGH(f0);
@@ -5520,14 +5522,14 @@
DECREF(LOW(toBeProcessed));
DECREF(HIGH(toBeProcessed));
- /* Update in-place */
+ // Update in-place
SETVARr(toBeProcessed, var1);
SETLOW(toBeProcessed, f0);
SETHIGH(toBeProcessed, f1);
levels[var1].nodenum++;
- /* Do not rehash yet since we are going to resize the hash table */
+ // Do not rehash yet since we are going to resize the hash table
toBeProcessed = next;
}
@@ -5595,13 +5597,15 @@
void reorder_swap(int toBeProcessed, int var0) {
int var1 = bddlevel2var[bddvar2level[var0] + 1];
+ // toBeProcessed is a linked list of nodes that depend on the next level.
+
while (toBeProcessed != 0) {
int next = NEXT(toBeProcessed);
int f0 = LOW(toBeProcessed);
int f1 = HIGH(toBeProcessed);
int f00, f01, f10, f11, hash;
- /* Find the cofactors for the new nodes */
+ // Find the cofactors for the new nodes
if (VARr(f0) == var1) {
f00 = LOW(f0);
f01 = HIGH(f0);
@@ -5620,22 +5624,25 @@
//node = bddnodes[toBeProcessed]; /* Might change in makenode */
/* We know that the refcou of the grandchilds of this node
- * is greater than one (these are f00...f11), so there is
- * no need to do a recursive refcou decrease. It is also
- * possible for the node.low/high nodes to come alive again,
- * so deref. of the childs is delayed until the local GBC. */
+ * is greater than one (these are f00...f11), so there is
+ * no need to do a recursive refcou decrease. It is also
+ * possible for the node.low/high nodes to come alive again,
+ * so deref. of the childs is delayed until the local GBC. */
DECREF(LOW(toBeProcessed));
DECREF(HIGH(toBeProcessed));
- /* Update in-place */
+ // Update in-place
+ // NOTE: This node may be a duplicate. However, we add this to the start
+ // of the list so we will always encounter this one first. The refcount
+ // of the node we duplicated will go to zero.
SETVARr(toBeProcessed, var1);
SETLOW(toBeProcessed, f0);
SETHIGH(toBeProcessed, f1);
levels[var1].nodenum++;
- /* Rehash the node since it got new childs */
+ // Rehash the node since it has new children
hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
SETNEXT(toBeProcessed, HASH(hash));
SETHASH(hash, toBeProcessed);
@@ -5658,7 +5665,7 @@
cachestats.uniqueAccess++;
/* Note: We know that low,high has a refcou greater than zero, so
- there is no need to add reference *recursively* */
+ there is no need to add reference *recursively* */
if (ZDD) {
/* check whether high child is zero */
@@ -5701,9 +5708,9 @@
return 0;
/* Try to allocate more nodes - call noderesize without
- * enabling rehashing.
+ * enabling rehashing.
* Note: if ever rehashing is allowed here, then remember to
- * update local variable "hash" */
+ * update local variable "hash" */
bdd_noderesize(false);
resizedInMakenode = true;
@@ -5740,12 +5747,18 @@
}
int reorder_init() {
+ // This method does the following:
+ // - Calculate interaction matrix "iactmtx"
+ // - Calculates the number of nodes with each variable.
+ // - Mutates each node to store the var instead of the level.
+ // - Sets refcounts for all links, including internal ones.
+
int n;
reorder_handler(true, reorderstats);
+ // Split the hash table into a separate region for each variable.
levels = new levelData[bddvarnum];
-
for (n = 0; n < bddvarnum; n++) {
levels[n] = new levelData();
levels[n].start = -1;
@@ -5753,15 +5766,15 @@
levels[n].nodenum = 0;
}
- /* First mark and recursive refcou. all roots and childs. Also do some
- * setup here for both setLevellookup and reorder_gbc */
+ // First mark and recursive refcou. all roots and childs. Also do some
+ // setup here for both setLevellookup and reorder_gbc
if (mark_roots() < 0)
return -1;
- /* Initialize the hash tables */
+ // Initialize the hash tables
reorder_setLevellookup();
- /* Garbage collect and rehash to new scheme */
+ // Garbage collect and rehash to new scheme
reorder_gbc();
return 0;
@@ -5786,14 +5799,19 @@
iactmtx = imatrixNew(bddvarnum);
+ // Loop to compute dependences and node refcounts.
for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
if (MARKED(n)) {
+ // Node has an external reference.
UNMARK(n);
extroots[extrootsize++] = n;
+ // Calculate the set of variables in this BDD.
+ // Also sets refcounts on internal nodes.
for (int i = 0; i < bddvarnum; ++i)
dep[i] = false;
+
dep[VARr(n)] = true;
levels[VARr(n)].nodenum++;
@@ -5835,12 +5853,15 @@
return;
if (!HASREF(r) || MARKED(r)) {
+ // We haven't processed the node yet.
+ // Processed nodes have a refcount and are unmarked.
+
bddfreenum--;
- /* Detect variable dependencies for the interaction matrix */
+ // Detect variable dependencies for the interaction matrix
dep[VARr(r) & ~MARK_MASK] = true;
- /* Make sure the nodenum field is updated. Used in the initial GBC */
+ // Make sure the nodenum field is updated. Used in the initial GBC
levels[VARr(r) & ~MARK_MASK].nodenum++;
addref_rec(LOW(r), dep);
@@ -5848,8 +5869,8 @@
} else {
int n;
- /* Update (from previously found) variable dependencies
- * for the interaction matrix */
+ // Update (from previously found) variable dependencies
+ // for the interaction matrix
for (n = 0; n < bddvarnum; n++)
dep[n]
|= imatrixDepends(iactmtx, VARr(r) & ~MARK_MASK, n);
@@ -5913,7 +5934,7 @@
CLEARREF(n);
/* This is where we go from .var to .level again!
- * - Do NOT use the LEVEL macro here. */
+ * - Do NOT use the LEVEL macro here. */
SETLEVELANDMARK(n, bddvar2level[LEVELANDMARK(n)]);
}
Added: trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java (rev 0)
+++ trunk/JavaBDD/net/sf/javabdd/UberMicroFactory.java 2007-03-06 06:08:40 UTC (rev 476)
@@ -0,0 +1,6763 @@
+// UberMicroFactory.java, created Jan 29, 2005 8:24:17 PM by joewhaley
+// Copyright (C) 2005 John Whaley <jw...@al...>
+// Licensed under the terms of the GNU LGPL; see COPYING for details.
+package net.sf.javabdd;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedList;
+import java.util.Random;
+import java.util.Set;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+import java.io.IOException;
+import java.io.PrintStream;
+
+/**
+ * <p>BDD factory where each node only takes 16 bytes.
+ * This is accomplished by tightly packing the bits, eliminating
+ * the refcount, splitting out the unique table and limiting the
+ * maximum number of BDD variables to 2^11 = 2048.</p>
+ *
+ * <p>This BDD factory is not only more memory efficient than
+ * JFactory, it also seems to perform better, probably due to
+ * better memory locality. It performs cache-aware BDD node
+ * placement.</p>
+ *
+ * @author jwhaley
+ * @version $Id: UberMicroFactory.java 465 2006-07-26 16:42:44Z joewhaley $
+ */
+public class UberMicroFactory extends BDDFactoryIntImpl {
+
+ public static boolean FLUSH_CACHE_ON_GC = true;
+
+ static final boolean VERIFY_ASSERTIONS = true;
+ static final boolean ORDER_CACHE = false;
+ static final int CACHESTATS = 0;
+ static final boolean SWAPCOUNT = false;
+
+ public static final String REVISION = "$Revision: 465 $";
+
+ public String getVersion() {
+ return "UberMicroFactory "+REVISION.substring(11, REVISION.length()-2);
+ }
+
+ private UberMicroFactory() { }
+
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDFactory#init(int, int)
+ */
+ public static BDDFactory init(int nodenum, int cachesize) {
+ BDDFactory f = new UberMicroFactory();
+ f.initialize(nodenum, cachesize);
+ if (CACHESTATS > 0) addShutdownHook(f);
+ return f;
+ }
+
+ static void addShutdownHook(final BDDFactory f) {
+ Runtime.getRuntime().addShutdownHook(new Thread() {
+ public void run() {
+ System.out.println(f.getCacheStats().toString());
+ }
+ });
+ }
+
+ protected IntBDD makeBDD(/*bdd*/int v) {
+ return new Micro5BDD(v);
+ }
+
+ static final boolean USE_WEAK_REFS = false;
+
+ Collection externalRefBDDs, externalRefVarSets;
+
+ class Micro5BDD extends BDDFactoryIntImpl.IntBDD {
+ Micro5BDD(int v) {
+ super(v);
+ if (VERIFY_ASSERTIONS) {
+ if (v == INVALID_BDD)
+ bdd_error(BDD_BREAK); /* distinctive */
+ if (v >= bddnodesize)
+ bdd_error(BDD_ILLBDD);
+ if (bddnodes[v] == 0)
+ bdd_error(BDD_ILLBDD);
+ }
+ if (USE_WEAK_REFS)
+ externalRefBDDs.add(new java.lang.ref.WeakReference(this));
+ else
+ externalRefBDDs.add(this);
+ }
+ }
+
+ protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) {
+ return new Micro5VarSet(v);
+ }
+
+ public class Micro5VarSet extends IntBDDVarSet {
+ Micro5VarSet(int v) {
+ super(v);
+ if (VERIFY_ASSERTIONS) {
+ if (v == INVALID_BDD)
+ bdd_error(BDD_BREAK); /* distinctive */
+ if (v >= bddnodesize)
+ bdd_error(BDD_ILLBDD);
+ if (bddnodes[v] == 0)
+ bdd_error(BDD_ILLBDD);
+ }
+ if (USE_WEAK_REFS)
+ externalRefVarSets.add(new java.lang.ref.WeakReference(this));
+ else
+ externalRefVarSets.add(this);
+ }
+ }
+
+ public void handleDeferredFree() {
+ to_free_length = 0;
+ }
+
+ /**
+ * Implementation of BDDPairing used by JFactory.
+ */
+ class bddPair extends BDDPairing {
+ int[] result;
+ int last;
+ int id;
+ bddPair next;
+
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#set(int, int)
+ */
+ public void set(int oldvar, int newvar) {
+ bdd_setpair(this, oldvar, newvar);
+ }
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
+ */
+ public void set(int oldvar, BDD newvar) {
+ bdd_setbddpair(this, oldvar, unwrap(newvar));
+ }
+ /* (non-Javadoc)
+ * @see net.sf.javabdd.BDDPairing#reset()
+ */
+ public void reset() {
+ bdd_resetpair(this);
+ }
+
+ 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]);
+
+ p.id = update_pairsid();
+ p.last = -1;
+
+ bdd_register_pair(p);
+ return p;
+ }
+
+ // Redirection functions.
+
+ protected void addref_impl(int v) { }
+ protected void delref_impl(int 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 makenode_impl(int lev, int lo, int hi) { return bdd_makenode(lev, lo, hi); }
+ 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 isInitialized() { return bddrunning; }
+ public void done() { super.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); }
+ 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); }
+
+ 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();
+ }
+ }
+
+ // Experimental functions.
+
+ public void validateAll() { bdd_validate_all(); }
+ public void validateLive() { bdd_validate_live(); }
+ public void validateBDD(BDD b) { bdd_validate(unwrap(b)); }
+
+
+ /***** IMPLEMENTATION BELOW *****/
+
+ long[] bddnodes;
+
+ static final int LEV_BITS = 11;
+ static final int NODE_BITS = 26;
+ static final int LOW_SHIFT = 12;
+ static final int HIGH_SHIFT = 38;
+ static final int LEV_SHIFT = 1;
+ static final int MARK_MASK = 0x001;
+ static final int LEV_MASK = 0xffe;
+ static final long LO_MASK = 0x0000003ffffff000L;
+ static final long HI_MASK = 0xffffffc000000000L;
+ static final long LOHILEV_MASK = LO_MASK | HI_MASK | LEV_MASK;
+
+ static final int INVALID_BDD = -1;
+ static final int MAXVAR = (1 << LEV_BITS) - 1;
+ static final int MAX_PAIRSID = MAXVAR;
+ static final int NODE_MASK = (1 << NODE_BITS) - 1;
+
+ private final int LEVEL(int node) {
+ return ((int)bddnodes[node] & LEV_MASK) >> LEV_SHIFT;
+ }
+
+ private final void SETLEVEL(int node, int val) {
+ if (VERIFY_ASSERTIONS)
+ _assert(val >= 0 && val <= MAXVAR);
+ long a = bddnodes[node] & ~LEV_MASK;
+ a |= val << LEV_SHIFT;
+ bddnodes[node] = a;
+ }
+
+ private final void SETMARK(int n) {
+ bddnodes[n] |= MARK_MASK;
+ }
+
+ private final void UNMARK(int n) {
+ if (VERIFY_ASSERTIONS) _assert(n > 1);
+ bddnodes[n] &= ~MARK_MASK;
+ }
+
+ private final boolean MARKED(int n) {
+ return ((int)bddnodes[n] & MARK_MASK) != 0;
+ }
+
+ private final int LOW(int r) {
+ return (int)(bddnodes[r] >> LOW_SHIFT) & NODE_MASK;
+ }
+
+ private final void SETLOW(int r, int v) {
+ if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
+ long a = bddnodes[r] & ~LO_MASK;
+ a |= (long)v << LOW_SHIFT;
+ bddnodes[r] = a;
+ }
+
+ private final int HIGH(int r) {
+ return (int)(bddnodes[r] >> HIGH_SHIFT) & NODE_MASK;
+ }
+
+ private final void SETHIGH(int r, int v) {
+ if (VERIFY_ASSERTIONS) _assert(v >= 0 && v <= NODE_MASK);
+ long a = bddnodes[r] & ~HI_MASK;
+ a |= (long)v << HIGH_SHIFT;
+ bddnodes[r] = a;
+ }
+
+ private static final long MAKE_NODE(int lev, int lo, int hi) {
+ long a = lev << LEV_SHIFT;
+ a |= (long)lo << LOW_SHIFT;
+ a |= (long)hi << HIGH_SHIFT;
+ return a;
+ }
+
+ private final int VARr(int node) {
+ return ((int)bddnodes[node] & LEV_MASK) >> LEV_SHIFT;
+ }
+
+ private final void SETVARr(int node, int val) {
+ if (VERIFY_ASSERTIONS)
+ _assert(val >= 0 && val <= MAXVAR);
+ long a = bddnodes[node] & ~LEV_MASK;
+ a |= val << LEV_SHIFT;
+ bddnodes[node] = a;
+ }
+
+ static final int BUCKET_SIZE = 8;
+
+ class freelist {
+ BitString fullbuckets;
+
+ void reset() {
+ if (VERIFY_ASSERTIONS) _assert((bddnodesize & -BUCKET_SIZE) == bddnodesize);
+ int b = bddnodesize / BUCKET_SIZE;
+ if (fullbuckets == null || b != fullbuckets.size())
+ fullbuckets = new BitString(b);
+ last_bucket = 0;
+ }
+
+ void resize() {
+ if (fullbuckets == null) {
+ reset();
+ } else {
+ if (VERIFY_ASSERTIONS) _assert((bddnodesize & -BUCKET_SIZE) == bddnodesize);
+ int b = bddnodesize / BUCKET_SIZE;
+ if (b !...
[truncated message content] |
|
From: <joe...@us...> - 2007-06-15 22:22:54
|
Revision: 478
http://svn.sourceforge.net/javabdd/?rev=478&view=rev
Author: joewhaley
Date: 2007-06-15 15:22:53 -0700 (Fri, 15 Jun 2007)
Log Message:
-----------
Added Google Analytics.
Modified Paths:
--------------
trunk/JavaBDD/project.properties
trunk/JavaBDD/xdocs/navigation.xml
Modified: trunk/JavaBDD/project.properties
===================================================================
--- trunk/JavaBDD/project.properties 2007-03-06 07:31:44 UTC (rev 477)
+++ trunk/JavaBDD/project.properties 2007-06-15 22:22:53 UTC (rev 478)
@@ -2,8 +2,10 @@
# Where to find source code, used by tasklist plugin.
#maven.src.dir = .
-maven.compile.source = 1.3
-maven.compile.target = 1.3
+#maven.compile.source = 1.3
+#maven.compile.target = 1.3
+maven.compile.source = 1.5
+maven.compile.target = 1.5
# The string to look for in TODO tags, used by tasklist plugin.
#maven.tasklist.taskTag = TODO
Modified: trunk/JavaBDD/xdocs/navigation.xml
===================================================================
--- trunk/JavaBDD/xdocs/navigation.xml 2007-03-06 07:31:44 UTC (rev 477)
+++ trunk/JavaBDD/xdocs/navigation.xml 2007-06-15 22:22:53 UTC (rev 478)
@@ -35,5 +35,13 @@
<item name="JavaBDD Source code"
href="http://prdownloads.sourceforge.net/javabdd/javabdd_src_1.0b2.tar.gz"/>
</menu>
+ <footer>
+<script src="http://www.google-analytics.com/urchin.js" type="text/javascript">
+</script>
+<script type="text/javascript">
+_uacct = "UA-72567-3";
+urchinTracker();
+</script>
+ </footer>
</body>
</project>
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X