[Javabdd-checkins] SF.net SVN: javabdd: [454] trunk/JavaBDD
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [454] trunk/JavaBDD
|
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] |
