You can subscribe to this list here.
2003 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(4) |
---|---|---|---|---|---|---|---|---|---|---|---|---|
2004 |
Jan
|
Feb
|
Mar
(6) |
Apr
(6) |
May
(4) |
Jun
(31) |
Jul
(64) |
Aug
(19) |
Sep
(28) |
Oct
(50) |
Nov
(25) |
Dec
|
2005 |
Jan
(44) |
Feb
(8) |
Mar
(2) |
Apr
(15) |
May
(48) |
Jun
(8) |
Jul
(7) |
Aug
|
Sep
(1) |
Oct
(3) |
Nov
|
Dec
|
2006 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(1) |
Jun
(2) |
Jul
(14) |
Aug
|
Sep
|
Oct
|
Nov
(6) |
Dec
(4) |
2007 |
Jan
|
Feb
|
Mar
(2) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
(1) |
Dec
|
2011 |
Jan
|
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
2019 |
Jan
|
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: John W. <joe...@us...> - 2004-10-16 04:34:36
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17686 Modified Files: Makefile Log Message: Renamed org.sf.javabdd to net.sf.javabdd Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.32 retrieving revision 1.33 diff -C2 -d -r1.32 -r1.33 *** Makefile 12 Oct 2004 20:42:52 -0000 1.32 --- Makefile 16 Oct 2004 02:59:52 -0000 1.33 *************** *** 82,116 **** # The java source code ! JAVA_SOURCES = org/sf/javabdd/BDD.java \ ! org/sf/javabdd/BDDBitVector.java \ ! org/sf/javabdd/BDDDomain.java \ ! org/sf/javabdd/BDDException.java \ ! org/sf/javabdd/BDDFactory.java \ ! org/sf/javabdd/BDDPairing.java \ ! org/sf/javabdd/BuDDyFactory.java \ ! org/sf/javabdd/CALFactory.java \ ! org/sf/javabdd/CUDDFactory.java \ ! org/sf/javabdd/FindBestOrder.java \ ! org/sf/javabdd/JFactory.java \ ! org/sf/javabdd/JDDFactory.java \ ! org/sf/javabdd/TestBDDFactory.java \ ! org/sf/javabdd/TypedBDDFactory.java ! JAVA_CLASSFILES = org/sf/javabdd/*.class ! JAVA_PACKAGES = org.sf.javabdd ! BUDDY_CLASSFILE = org/sf/javabdd/BuDDyFactory.class ! CUDD_CLASSFILE = org/sf/javabdd/CUDDFactory.class ! CAL_CLASSFILE = org/sf/javabdd/CALFactory.class ! BUDDY_CLASSNAMES = org.sf.javabdd.BuDDyFactory \ ! org.sf.javabdd.BuDDyFactory\$$BuDDyBDD \ ! org.sf.javabdd.BuDDyFactory\$$BuDDyBDDDomain \ ! org.sf.javabdd.BuDDyFactory\$$BuDDyBDDPairing ! CUDD_CLASSNAMES = org.sf.javabdd.CUDDFactory \ ! org.sf.javabdd.CUDDFactory\$$CUDDBDD \ ! org.sf.javabdd.CUDDFactory\$$CUDDBDDDomain \ ! org.sf.javabdd.CUDDFactory\$$CUDDBDDPairing ! CAL_CLASSNAMES = org.sf.javabdd.CALFactory \ ! org.sf.javabdd.CALFactory\$$CALBDD \ ! org.sf.javabdd.CALFactory\$$CALBDDDomain \ ! org.sf.javabdd.CALFactory\$$CALBDDPairing EXAMPLE_SOURCES = NQueens.java RubiksCube.java EXAMPLE_CLASSFILES = $(EXAMPLE_SOURCES:%.java=%.class) --- 82,116 ---- # The java source code ! JAVA_SOURCES = net/sf/javabdd/BDD.java \ ! net/sf/javabdd/BDDBitVector.java \ ! net/sf/javabdd/BDDDomain.java \ ! net/sf/javabdd/BDDException.java \ ! net/sf/javabdd/BDDFactory.java \ ! net/sf/javabdd/BDDPairing.java \ ! net/sf/javabdd/BuDDyFactory.java \ ! net/sf/javabdd/CALFactory.java \ ! net/sf/javabdd/CUDDFactory.java \ ! net/sf/javabdd/FindBestOrder.java \ ! net/sf/javabdd/JFactory.java \ ! net/sf/javabdd/JDDFactory.java \ ! net/sf/javabdd/TestBDDFactory.java \ ! net/sf/javabdd/TypedBDDFactory.java ! JAVA_CLASSFILES = net/sf/javabdd/*.class ! JAVA_PACKAGES = net.sf.javabdd ! BUDDY_CLASSFILE = net/sf/javabdd/BuDDyFactory.class ! 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\$$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) |
From: John W. <joe...@us...> - 2004-10-16 04:31:37
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4310/bdd Modified Files: BDDTestCase.java Log Message: Renamed org.sf.javabdd to net.sf.javabdd Index: BDDTestCase.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BDDTestCase.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** BDDTestCase.java 28 Jul 2004 10:20:53 -0000 1.1 --- BDDTestCase.java 16 Oct 2004 04:31:27 -0000 1.2 *************** *** 8,12 **** import java.lang.reflect.Method; import junit.framework.TestCase; ! import org.sf.javabdd.BDDFactory; /** --- 8,12 ---- import java.lang.reflect.Method; import junit.framework.TestCase; ! import net.sf.javabdd.BDDFactory; /** *************** *** 20,28 **** static volatile Collection factories; static final String[] factoryNames = { ! "org.sf.javabdd.BuDDyFactory", ! "org.sf.javabdd.CUDDFactory", ! "org.sf.javabdd.CALFactory", ! "org.sf.javabdd.JFactory", ! //"org.sf.javabdd.JDDFactory", }; --- 20,28 ---- static volatile Collection factories; static final String[] factoryNames = { ! "net.sf.javabdd.BuDDyFactory", ! "net.sf.javabdd.CUDDFactory", ! "net.sf.javabdd.CALFactory", ! "net.sf.javabdd.JFactory", ! //"net.sf.javabdd.JDDFactory", }; |
From: John W. <joe...@us...> - 2004-10-16 04:31:37
|
Update of /cvsroot/javabdd/JavaBDD_tests/regression In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4310/regression Modified Files: R2.java R1.java Log Message: Renamed org.sf.javabdd to net.sf.javabdd Index: R1.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/regression/R1.java,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** R1.java 28 Jul 2004 10:20:53 -0000 1.3 --- R1.java 16 Oct 2004 04:31:28 -0000 1.4 *************** *** 5,11 **** import junit.framework.Assert; ! import org.sf.javabdd.BDD; ! import org.sf.javabdd.BDDDomain; ! import org.sf.javabdd.BDDFactory; import bdd.BDDTestCase; --- 5,11 ---- import junit.framework.Assert; ! import net.sf.javabdd.BDD; ! import net.sf.javabdd.BDDDomain; ! import net.sf.javabdd.BDDFactory; import bdd.BDDTestCase; Index: R2.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/regression/R2.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** R2.java 28 Jul 2004 10:20:53 -0000 1.2 --- R2.java 16 Oct 2004 04:31:28 -0000 1.3 *************** *** 5,10 **** import junit.framework.Assert; ! import org.sf.javabdd.BDD; ! import org.sf.javabdd.BDDFactory; import bdd.BDDTestCase; --- 5,10 ---- import junit.framework.Assert; ! import net.sf.javabdd.BDD; ! import net.sf.javabdd.BDDFactory; import bdd.BDDTestCase; |
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv761/org/sf/javabdd Removed Files: TryVarOrder.java BDDException.java BuDDyFactory.java FindBestOrder.java HijackingClassLoader.java TestBDDFactory.java BDDDomain.java CALFactory.java JFactory.java BDDFactory.java BDDPairing.java BDD.java BDDBitVector.java TypedBDDFactory.java JDDFactory.java CUDDFactory.java Log Message: Renamed org.sf.javabdd to net.sf.javabdd --- BuDDyFactory.java DELETED --- --- BDDDomain.java DELETED --- --- JFactory.java DELETED --- --- TypedBDDFactory.java DELETED --- --- JDDFactory.java DELETED --- --- BDDException.java DELETED --- --- BDDFactory.java DELETED --- --- FindBestOrder.java DELETED --- --- CUDDFactory.java DELETED --- --- BDD.java DELETED --- --- TestBDDFactory.java DELETED --- --- BDDPairing.java DELETED --- --- HijackingClassLoader.java DELETED --- --- TryVarOrder.java DELETED --- --- CALFactory.java DELETED --- --- BDDBitVector.java DELETED --- |
From: John W. <joe...@us...> - 2004-10-16 02:59:13
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17474 Modified Files: buddy_jni.c project.xml javabdd.jardesc cudd_jni.c cal_jni.c NQueens.java RubiksCube.java Log Message: Renamed org.sf.javabdd to net.sf.javabdd Index: cal_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cal_jni.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** cal_jni.c 28 Jul 2004 11:38:08 -0000 1.2 --- cal_jni.c 16 Oct 2004 02:58:57 -0000 1.3 *************** *** 48,56 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: registerNatives * Signature: ()V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_registerNatives (JNIEnv *env, jclass cl) { --- 48,56 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: registerNatives * Signature: ()V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_registerNatives (JNIEnv *env, jclass cl) { *************** *** 58,66 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: initialize0 * Signature: (II)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_initialize0 (JNIEnv *env, jclass cl, jint numSlots, jint cacheSize) { --- 58,66 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: initialize0 * Signature: (II)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_initialize0 (JNIEnv *env, jclass cl, jint numSlots, jint cacheSize) { *************** *** 97,105 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: isInitialized0 * Signature: ()Z */ ! JNIEXPORT jboolean JNICALL Java_org_sf_javabdd_CALFactory_isInitialized0 (JNIEnv *env, jclass cl) { --- 97,105 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: isInitialized0 * Signature: ()Z */ ! JNIEXPORT jboolean JNICALL Java_net_sf_javabdd_CALFactory_isInitialized0 (JNIEnv *env, jclass cl) { *************** *** 108,116 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: done0 * Signature: ()V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_done0 (JNIEnv *env, jclass cl) { --- 108,116 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: done0 * Signature: ()V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_done0 (JNIEnv *env, jclass cl) { *************** *** 132,140 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: varNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_varNum0 (JNIEnv *env, jclass cl) { --- 132,140 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: varNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_varNum0 (JNIEnv *env, jclass cl) { *************** *** 143,151 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: setVarNum0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_setVarNum0 (JNIEnv *env, jclass cl, jint x) { --- 143,151 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: setVarNum0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_setVarNum0 (JNIEnv *env, jclass cl, jint x) { *************** *** 159,167 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: ithVar0 * Signature: (I)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_ithVar0 (JNIEnv *env, jclass cl, jint i) { --- 159,167 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: ithVar0 * Signature: (I)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_ithVar0 (JNIEnv *env, jclass cl, jint i) { *************** *** 174,182 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: level2Var0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_level2Var0 (JNIEnv *env, jclass cl, jint level) { --- 174,182 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: level2Var0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_level2Var0 (JNIEnv *env, jclass cl, jint level) { *************** *** 192,200 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: var2Level0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_var2Level0 (JNIEnv *env, jclass cl, jint v) { --- 192,200 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: var2Level0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_var2Level0 (JNIEnv *env, jclass cl, jint v) { *************** *** 205,213 **** /* ! * Class: org_sf_javabdd_CALFactory * Method: setVarOrder0 * Signature: ([I)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_setVarOrder0 (JNIEnv *env, jclass cl, jintArray arr) { --- 205,213 ---- /* ! * Class: net_sf_javabdd_CALFactory * Method: setVarOrder0 * Signature: ([I)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_setVarOrder0 (JNIEnv *env, jclass cl, jintArray arr) { *************** *** 227,238 **** } ! /* class org_sf_javabdd_CALFactory_CALBDD */ /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: var0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_var0 (JNIEnv *env, jclass cl, jlong b) { --- 227,238 ---- } ! /* class net_sf_javabdd_CALFactory_CALBDD */ /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: var0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_var0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 243,251 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: high0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_high0 (JNIEnv *env, jclass cl, jlong b) { --- 243,251 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: high0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_high0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 263,271 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: low0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_low0 (JNIEnv *env, jclass cl, jlong b) { --- 263,271 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: low0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_low0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 283,291 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: not0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_not0 (JNIEnv *env, jclass cl, jlong b) { --- 283,291 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: not0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_not0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 299,307 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: ite0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_ite0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { --- 299,307 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: ite0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_ite0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { *************** *** 320,328 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: relprod0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_relprod0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { --- 320,328 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: relprod0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_relprod0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { *************** *** 343,351 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: restrict0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_restrict0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 343,351 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: restrict0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_restrict0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 362,370 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: support0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_support0 (JNIEnv *env, jclass cl, jlong a) { --- 362,370 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: support0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_support0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 379,387 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: apply0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_apply0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint oper) { --- 379,387 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: apply0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_apply0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint oper) { *************** *** 444,452 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: satOne0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_satOne0 (JNIEnv *env, jclass cl, jlong a) { --- 444,452 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: satOne0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_satOne0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 461,469 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: nodeCount0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_nodeCount0 (JNIEnv *env, jclass cl, jlong a) { --- 461,469 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: nodeCount0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_nodeCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 474,482 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: pathCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_pathCount0 (JNIEnv *env, jclass cl, jlong a) { --- 474,482 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: pathCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_pathCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 489,497 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: satCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_satCount0 (JNIEnv *env, jclass cl, jlong a) { --- 489,497 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: satCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_satCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 505,513 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: addRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_addRef (JNIEnv *env, jclass cl, jlong a) { --- 505,513 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: addRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_addRef (JNIEnv *env, jclass cl, jlong a) { *************** *** 518,526 **** /* ! * Class: org_sf_javabdd_CALFactory_CALBDD * Method: delRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CALFactory_00024CALBDD_delRef (JNIEnv *env, jclass cl, jlong a) { --- 518,526 ---- /* ! * Class: net_sf_javabdd_CALFactory_CALBDD * Method: delRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CALFactory_00024CALBDD_delRef (JNIEnv *env, jclass cl, jlong a) { Index: project.xml =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/project.xml,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** project.xml 2 Aug 2004 23:21:47 -0000 1.12 --- project.xml 16 Oct 2004 02:58:57 -0000 1.13 *************** *** 12,16 **** </organization> <inceptionYear>2003</inceptionYear> ! <package>org.sf.javabdd</package> <shortDescription>Java Binary Decision Diagram library</shortDescription> --- 12,16 ---- </organization> <inceptionYear>2003</inceptionYear> ! <package>net.sf.javabdd</package> <shortDescription>Java Binary Decision Diagram library</shortDescription> Index: cudd_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v retrieving revision 1.11 retrieving revision 1.12 diff -C2 -d -r1.11 -r1.12 *** cudd_jni.c 21 Jun 2004 17:42:18 -0000 1.11 --- cudd_jni.c 16 Oct 2004 02:58:57 -0000 1.12 *************** *** 51,59 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: registerNatives * Signature: ()V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_registerNatives (JNIEnv *env, jclass cl) { --- 51,59 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: registerNatives * Signature: ()V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_registerNatives (JNIEnv *env, jclass cl) { *************** *** 61,69 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: initialize0 * Signature: (II)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_initialize0 (JNIEnv *env, jclass cl, jint numSlots, jint cacheSize) { --- 61,69 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: initialize0 * Signature: (II)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_initialize0 (JNIEnv *env, jclass cl, jint numSlots, jint cacheSize) { *************** *** 103,111 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: isInitialized0 * Signature: ()Z */ ! JNIEXPORT jboolean JNICALL Java_org_sf_javabdd_CUDDFactory_isInitialized0 (JNIEnv *env, jclass cl) { --- 103,111 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: isInitialized0 * Signature: ()Z */ ! JNIEXPORT jboolean JNICALL Java_net_sf_javabdd_CUDDFactory_isInitialized0 (JNIEnv *env, jclass cl) { *************** *** 114,122 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: done0 * Signature: ()V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_done0 (JNIEnv *env, jclass cl) { --- 114,122 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: done0 * Signature: ()V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_done0 (JNIEnv *env, jclass cl) { *************** *** 138,146 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: varNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_varNum0 (JNIEnv *env, jclass cl) { --- 138,146 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: varNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_varNum0 (JNIEnv *env, jclass cl) { *************** *** 149,157 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: setVarNum0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_setVarNum0 (JNIEnv *env, jclass cl, jint x) { --- 149,157 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: setVarNum0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_setVarNum0 (JNIEnv *env, jclass cl, jint x) { *************** *** 162,170 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: ithVar0 * Signature: (I)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_ithVar0 (JNIEnv *env, jclass cl, jint i) { --- 162,170 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: ithVar0 * Signature: (I)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_ithVar0 (JNIEnv *env, jclass cl, jint i) { *************** *** 178,186 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: level2Var0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_level2Var0 (JNIEnv *env, jclass cl, jint level) { --- 178,186 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: level2Var0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_level2Var0 (JNIEnv *env, jclass cl, jint level) { *************** *** 190,198 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: var2Level0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_var2Level0 (JNIEnv *env, jclass cl, jint v) { --- 190,198 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: var2Level0 * Signature: (I)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_var2Level0 (JNIEnv *env, jclass cl, jint v) { *************** *** 202,210 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: setVarOrder0 * Signature: ([I)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_setVarOrder0 (JNIEnv *env, jclass cl, jintArray arr) { --- 202,210 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: setVarOrder0 * Signature: ([I)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_setVarOrder0 (JNIEnv *env, jclass cl, jintArray arr) { *************** *** 224,232 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: getAllocNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_getAllocNum0 (JNIEnv *env, jclass cl) { --- 224,232 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: getAllocNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_getAllocNum0 (JNIEnv *env, jclass cl) { *************** *** 235,243 **** /* ! * Class: org_sf_javabdd_CUDDFactory * Method: getNodeNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_getNodeNum0 (JNIEnv *env, jclass cl) { --- 235,243 ---- /* ! * Class: net_sf_javabdd_CUDDFactory * Method: getNodeNum0 * Signature: ()I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_getNodeNum0 (JNIEnv *env, jclass cl) { *************** *** 245,256 **** } ! /* class org_sf_javabdd_CUDDFactory_CUDDBDD */ /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: var0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_var0 (JNIEnv *env, jclass cl, jlong b) { --- 245,256 ---- } ! /* class net_sf_javabdd_CUDDFactory_CUDDBDD */ /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: var0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_var0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 261,269 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: high0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_high0 (JNIEnv *env, jclass cl, jlong b) { --- 261,269 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: high0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_high0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 282,290 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: low0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_low0 (JNIEnv *env, jclass cl, jlong b) { --- 282,290 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: low0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_low0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 303,311 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: not0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_not0 (JNIEnv *env, jclass cl, jlong b) { --- 303,311 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: not0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_not0 (JNIEnv *env, jclass cl, jlong b) { *************** *** 319,327 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: ite0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_ite0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { --- 319,327 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: ite0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_ite0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { *************** *** 340,348 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: relprod0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_relprod0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { --- 340,348 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: relprod0 * Signature: (JJJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_relprod0 (JNIEnv *env, jclass cl, jlong a, jlong b, jlong c) { *************** *** 361,369 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: compose0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_compose0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint i) { --- 361,369 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: compose0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_compose0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint i) { *************** *** 380,388 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: exist0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_exist0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 380,388 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: exist0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_exist0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 399,407 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: forAll0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_forAll0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 399,407 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: forAll0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_forAll0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 418,426 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: restrict0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_restrict0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 418,426 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: restrict0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_restrict0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 437,445 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: support0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_support0 (JNIEnv *env, jclass cl, jlong a) { --- 437,445 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: support0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_support0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 454,462 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: apply0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_apply0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint oper) { --- 454,462 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: apply0 * Signature: (JJI)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_apply0 (JNIEnv *env, jclass cl, jlong a, jlong b, jint oper) { *************** *** 578,586 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: satOne0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_satOne0 (JNIEnv *env, jclass cl, jlong a) { --- 578,586 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: satOne0 * Signature: (J)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_satOne0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 601,609 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: nodeCount0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_nodeCount0 (JNIEnv *env, jclass cl, jlong a) { --- 601,609 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: nodeCount0 * Signature: (J)I */ ! JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_nodeCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 614,622 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: pathCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_pathCount0 (JNIEnv *env, jclass cl, jlong a) { --- 614,622 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: pathCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_pathCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 627,635 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: satCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_satCount0 (JNIEnv *env, jclass cl, jlong a) { --- 627,635 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: satCount0 * Signature: (J)D */ ! JNIEXPORT jdouble JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_satCount0 (JNIEnv *env, jclass cl, jlong a) { *************** *** 640,648 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: addRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_addRef (JNIEnv *env, jclass cl, jlong a) { --- 640,648 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: addRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_addRef (JNIEnv *env, jclass cl, jlong a) { *************** *** 653,661 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: delRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_delRef (JNIEnv *env, jclass cl, jlong a) { --- 653,661 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: delRef * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_delRef (JNIEnv *env, jclass cl, jlong a) { *************** *** 668,676 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: veccompose0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_veccompose0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 668,676 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: veccompose0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_veccompose0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 687,695 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDD * Method: replace0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDD_replace0 (JNIEnv *env, jclass cl, jlong a, jlong b) { --- 687,695 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDD * Method: replace0 * Signature: (JJ)J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDD_replace0 (JNIEnv *env, jclass cl, jlong a, jlong b) { *************** *** 717,728 **** } ! /* class org_sf_javabdd_CUDDFactory_CUDDBDDPairing */ /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: alloc * Signature: ()J */ ! JNIEXPORT jlong JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_alloc (JNIEnv *env, jclass cl) { --- 717,728 ---- } ! /* class net_sf_javabdd_CUDDFactory_CUDDBDDPairing */ /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: alloc * Signature: ()J */ ! JNIEXPORT jlong JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_alloc (JNIEnv *env, jclass cl) { *************** *** 740,748 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: set0 * Signature: (JII)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_set0 (JNIEnv *env, jclass cl, jlong p, jint var, jint b) { --- 740,748 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: set0 * Signature: (JII)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_set0 (JNIEnv *env, jclass cl, jlong p, jint var, jint b) { *************** *** 757,765 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: set2 * Signature: (JIJ)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_set2 (JNIEnv *env, jclass cl, jlong p, jint var, jlong b) { --- 757,765 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: set2 * Signature: (JIJ)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_set2 (JNIEnv *env, jclass cl, jlong p, jint var, jlong b) { *************** *** 774,782 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: reset0 * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_reset0 (JNIEnv *env, jclass cl, jlong p) { --- 774,782 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: reset0 * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_reset0 (JNIEnv *env, jclass cl, jlong p) { *************** *** 794,802 **** /* ! * Class: org_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: free0 * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_free0 (JNIEnv *env, jclass cl, jlong p) { --- 794,802 ---- /* ! * Class: net_sf_javabdd_CUDDFactory_CUDDBDDPairing * Method: free0 * Signature: (J)V */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_00024CUDDBDDPairing_free0 (JNIEnv *env, jclass cl, jlong p) { Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.20 retrieving revision 1.21 diff -C2 -d -r1.20 -r1.21 *** buddy_jni.c 12 Oct 2004 20:43:42 -0000 1.20 --- buddy_jni.c 16 Oct 2004 02:58:57 -0000 1.21 *************** *** 74,78 **** case BVEC_SIZE: /* Mismatch in bitvector size */ case BVEC_DIVZERO: /* Division by zero */ ! clsname = "org/sf/javabdd/BDDException"; break; case BDD_FILE: /* Some file operation failed */ --- 74,78 ---- case BVEC_SIZE: /* Mismatch in bitvector size */ case BVEC_DIVZERO: /* Division by zero */ ! clsname = "net/sf/javabdd/BDDException"; break; [...1958 lines suppressed...] ! /* ! * Class: org_sf_javabdd_BuDDyFactory_BuDDyBDDPairing ! * Method: free0 ! * Signature: (J)V ! */ ! JNIEXPORT void JNICALL Java_org_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_free0 (JNIEnv *env, jclass cl, jlong pair) { --- 1634,1643 ---- } ! /* ! * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDDPairing ! * Method: free0 ! * Signature: (J)V ! */ ! JNIEXPORT void JNICALL Java_net_sf_javabdd_BuDDyFactory_00024BuDDyBDDPairing_free0 (JNIEnv *env, jclass cl, jlong pair) { Index: NQueens.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/NQueens.java,v retrieving revision 1.14 retrieving revision 1.15 diff -C2 -d -r1.14 -r1.15 *** NQueens.java 28 Jul 2004 09:19:29 -0000 1.14 --- NQueens.java 16 Oct 2004 02:58:57 -0000 1.15 *************** *** 1,3 **** ! import org.sf.javabdd.*; /** --- 1,3 ---- ! import net.sf.javabdd.*; /** Index: RubiksCube.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/RubiksCube.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** RubiksCube.java 31 Oct 2003 07:56:17 -0000 1.4 --- RubiksCube.java 16 Oct 2004 02:58:57 -0000 1.5 *************** *** 1,5 **** ! /* ! * Created on Sep 10, 2003 ! */ import java.util.ArrayList; --- 1,5 ---- ! // RubiksCube.java, created Jan 29, 2003 9:50:57 PM by jwhaley ! // Copyright (C) 2003 John Whaley ! // Licensed under the terms of the GNU LGPL; see COPYING for details. import java.util.ArrayList; *************** *** 9,18 **** import java.util.List; ! import org.sf.javabdd.BDD; ! import org.sf.javabdd.BDDDomain; ! import org.sf.javabdd.BDDFactory; ! import org.sf.javabdd.BDDPairing; /** * @author jwhaley */ --- 9,20 ---- import java.util.List; ! import net.sf.javabdd.BDD; ! import net.sf.javabdd.BDDDomain; ! import net.sf.javabdd.BDDFactory; ! import net.sf.javabdd.BDDPairing; /** + * RubiksCube + * * @author jwhaley */ *************** *** 221,225 **** static void p(BDD b, int d) { BDDDomain dom = bdd.getDomain(d); ! int v = (int) b.scanVar(dom); String s = Integer.toString(v); s = " ".substring(s.length())+s; --- 223,227 ---- static void p(BDD b, int d) { BDDDomain dom = bdd.getDomain(d); ! int v = b.scanVar(dom).intValue(); String s = Integer.toString(v); s = " ".substring(s.length())+s; Index: javabdd.jardesc =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/javabdd.jardesc,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** javabdd.jardesc 27 Aug 2004 01:02:35 -0000 1.4 --- javabdd.jardesc 16 Oct 2004 02:58:57 -0000 1.5 *************** *** 10,14 **** </manifest> <selectedElements exportClassFiles="true" exportJavaFiles="false" exportOutputFolder="false"> ! <javaElement handleIdentifier="=JavaBDD/<org.sf.javabdd"/> <javaElement handleIdentifier="=JavaBDD/<"/> </selectedElements> --- 10,14 ---- </manifest> <selectedElements exportClassFiles="true" exportJavaFiles="false" exportOutputFolder="false"> ! <javaElement handleIdentifier="=JavaBDD/<net.sf.javabdd"/> <javaElement handleIdentifier="=JavaBDD/<"/> </selectedElements> |
From: John W. <joe...@us...> - 2004-10-16 02:58:44
|
Update of /cvsroot/javabdd/JavaBDD/net In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17359/net Log Message: Directory /cvsroot/javabdd/JavaBDD/net added to the repository |
From: John W. <joe...@us...> - 2004-10-16 02:58:43
|
Update of /cvsroot/javabdd/JavaBDD/net/sf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17359/net/sf Log Message: Directory /cvsroot/javabdd/JavaBDD/net/sf added to the repository |
From: John W. <joe...@us...> - 2004-10-16 02:58:43
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17359/net/sf/javabdd Log Message: Directory /cvsroot/javabdd/JavaBDD/net/sf/javabdd added to the repository |
From: John W. <joe...@us...> - 2004-10-14 23:04:39
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2782/org/sf/javabdd Modified Files: TryVarOrder.java Log Message: Fix compilation problem. Also migrate to setError() version. Index: TryVarOrder.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TryVarOrder.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** TryVarOrder.java 29 Sep 2004 06:23:30 -0000 1.2 --- TryVarOrder.java 14 Oct 2004 23:04:30 -0000 1.3 *************** *** 27,31 **** static ClassLoader makeClassLoader() { ! return HijackingClassLoader.makeClassLoader(); } --- 27,32 ---- static ClassLoader makeClassLoader() { ! //return HijackingClassLoader.makeClassLoader(); ! return ClassLoader.getSystemClassLoader(); } *************** *** 84,87 **** --- 85,99 ---- } + void setBDDError(int code) { + Class c = bdd.getClass(); + try { + Method m = c.getMethod("setError", new Class[] { int.class }); + m.invoke(bdd, new Object[] { Integer.valueOf(code) }); + } catch (Exception x) { + System.err.println("Exception occurred while setting error for BDD factory: "+x.getLocalizedMessage()); + x.printStackTrace(); + } + } + /** * Make a domain in the BDD factory. *************** *** 352,357 **** } if (t.isAlive()) { ! t.stop(); ! Thread.yield(); // Help ThreadDeath exception to propagate. System.out.print("Free memory: "+Runtime.getRuntime().freeMemory()); destroyBDDFactory(); --- 364,372 ---- } if (t.isAlive()) { ! setBDDError(1); ! try { ! t.join(); ! } catch (InterruptedException x) { ! } System.out.print("Free memory: "+Runtime.getRuntime().freeMemory()); destroyBDDFactory(); |
From: John W. <joe...@us...> - 2004-10-14 23:03:18
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2350/buddy/src Modified Files: bddop.c Log Message: Small cleanups. Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** bddop.c 2 Oct 2004 08:13:34 -0000 1.6 --- bddop.c 14 Oct 2004 23:03:00 -0000 1.7 *************** *** 853,859 **** while (s_top != s_ptr) { ! int hash, lev; BDD l1, r1, res1; BddCacheData3 *entry; outer: r1 = *(--s_ptr); --- 853,860 ---- while (s_top != s_ptr) { ! int lev; BDD l1, r1, res1; BddCacheData3 *entry; + int entryNum; outer: r1 = *(--s_ptr); *************** *** 876,880 **** #endif ! entry = BddCache_lookup(&andcache, ANDHASH(l1,r1)); if (entry->a == l1 && entry->b == r1) { #ifdef CACHESTATS --- 877,882 ---- #endif ! entryNum = ANDHASH(l1,r1) % andcache.tablesize; ! entry = &andcache.table[entryNum]; if (entry->a == l1 && entry->b == r1) { #ifdef CACHESTATS *************** *** 888,892 **** *s_ptr++ = l1; *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - andcache.table); if (LEVEL(l1) == LEVEL(r1)) { *s_ptr++ = LEVEL(l1); --- 890,894 ---- *s_ptr++ = l1; *s_ptr++ = r1; ! *s_ptr++ = entryNum; if (LEVEL(l1) == LEVEL(r1)) { *s_ptr++ = LEVEL(l1); *************** *** 926,933 **** goto outer; } ! hash = *(--s_ptr); r1 = *(--s_ptr); l1 = *(--s_ptr); ! entry = &andcache.table[hash]; res1 = bdd_makenode(lev, READREF(2), READREF(1)); POPREF(2); --- 928,935 ---- goto outer; } ! entryNum = *(--s_ptr); r1 = *(--s_ptr); l1 = *(--s_ptr); ! entry = &andcache.table[entryNum]; res1 = bdd_makenode(lev, READREF(2), READREF(1)); POPREF(2); *************** *** 2664,2667 **** --- 2666,2670 ---- } + /* An iterative version of relprod. */ static int relprod_itr(int l0, int r0) { *************** *** 2669,2679 **** int* s_top; int* s_ptr; s_top = s_ptr = alloca(bddvarnum * sizeof(int) * 9); *s_ptr++ = l0; *s_ptr++ = r0; while (s_top != s_ptr) { ! int hash, lev, l1, r1, res1; BddCacheData4 *entry; outer: r1 = *(--s_ptr); --- 2672,2693 ---- int* s_top; int* s_ptr; + #if defined(USE_ALLOCA) s_top = s_ptr = alloca(bddvarnum * sizeof(int) * 9); + #else + if (gstack_size < bddvarnum) { + if (gstack != NULL) free(gstack); + if ((gstack=NEW(int,bddvarnum*9)) == NULL) + bdd_error(BDD_MEMORY); + gstack_size = bddvarnum; + } + s_top = s_ptr = gstack; + #endif *s_ptr++ = l0; *s_ptr++ = r0; while (s_top != s_ptr) { ! int lev, l1, r1, res1; BddCacheData4 *entry; + int entryNum; outer: r1 = *(--s_ptr); *************** *** 2707,2711 **** applyop = bddop_or; } else { ! entry = BddCache_lookup(&appexcache, APPEXHASH(l1,r1,bddop_and)); if (entry->a == l1 && entry->b == r1 && entry->r.c == appexid) { #ifdef CACHESTATS --- 2721,2726 ---- applyop = bddop_or; } else { ! entryNum = APPEXHASH(l1,r1,bddop_and) % appexcache.tablesize; ! entry = &appexcache.table[entryNum]; if (entry->a == l1 && entry->b == r1 && entry->r.c == appexid) { #ifdef CACHESTATS *************** *** 2719,2723 **** *s_ptr++ = l1; *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - appexcache.table); if (LEVEL(l1) == LEVEL(r1)) { *s_ptr++ = LEVEL(l1); --- 2734,2738 ---- *s_ptr++ = l1; *s_ptr++ = r1; ! *s_ptr++ = entryNum; if (LEVEL(l1) == LEVEL(r1)) { *s_ptr++ = LEVEL(l1); *************** *** 2758,2765 **** goto outer; } ! hash = *(--s_ptr); ! r1 = *(--s_ptr); ! l1 = *(--s_ptr); ! entry = &appexcache.table[hash]; if (INVARSET(lev)) { #if defined(SPECIALIZE_OR) --- 2773,2780 ---- goto outer; } ! entryNum = *(--s_ptr); ! r1 = *(--s_ptr); ! l1 = *(--s_ptr); ! entry = &appexcache.table[entryNum]; if (INVARSET(lev)) { #if defined(SPECIALIZE_OR) |
From: John W. <joe...@us...> - 2004-10-14 22:58:21
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv727/org/sf/javabdd Modified Files: BuDDyFactory.java Log Message: Added Javadoc. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.37 retrieving revision 1.38 diff -C2 -d -r1.37 -r1.38 *** BuDDyFactory.java 14 Oct 2004 19:47:36 -0000 1.37 --- BuDDyFactory.java 14 Oct 2004 22:58:05 -0000 1.38 *************** *** 90,95 **** * native code. * ! * @param c ! * @return */ private static int[] toBuDDyArray(Collection c) { --- 90,95 ---- * native code. * ! * @param c collection of BuDDyBDD's ! * @return int array of indices */ private static int[] toBuDDyArray(Collection c) { |
From: John W. <joe...@us...> - 2004-10-14 19:48:00
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20226/org/sf/javabdd Modified Files: JFactory.java CALFactory.java BuDDyFactory.java BDDFactory.java BDD.java TypedBDDFactory.java TestBDDFactory.java JDDFactory.java CUDDFactory.java BDDDomain.java Log Message: Updates to prepare for release. BDDDomains now use BigIntegers. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDD.java,v retrieving revision 1.37 retrieving revision 1.38 diff -C2 -d -r1.37 -r1.38 *** BDD.java 12 Oct 2004 20:40:17 -0000 1.37 --- BDD.java 14 Oct 2004 19:47:36 -0000 1.38 *************** *** 1,2 **** --- 1,5 ---- + // BDD.java, created Jan 29, 2003 9:50:57 PM by jwhaley + // Copyright (C) 2003 John Whaley + // Licensed under the terms of the GNU LGPL; see COPYING for details. package org.sf.javabdd; *************** *** 352,360 **** * in var, and constant false if they are included in their negative form.</p> * * <p>Compare to bdd_restrict.</p> * * @param var BDD containing the variables to be restricted * @return the result of the restrict operation ! * @see org.sf.javabdd.BDDDomain#set() */ public abstract BDD restrict(BDD var); --- 355,366 ---- * in var, and constant false if they are included in their negative form.</p> * + * <p><i>Note that this is quite different than Coudert and Madre's restrict + * function.</i></p> + * * <p>Compare to bdd_restrict.</p> * * @param var BDD containing the variables to be restricted * @return the result of the restrict operation ! * @see org.sf.javabdd.BDD#simplify(BDD) */ public abstract BDD restrict(BDD var); *************** *** 366,369 **** --- 372,378 ---- * their negative form. The "that" BDD is consumed, and can no longer be used.</p> * + * <p><i>Note that this is quite different than Coudert and Madre's restrict + * function.</i></p> + * * <p>Compare to bdd_restrict and bdd_delref.</p> * *************** *** 397,401 **** /** ! * <p>Returns the result of applying the binary operator opr to the two BDDs.</p> * * <p>Compare to bdd_apply.</p> --- 406,411 ---- /** ! * <p>Returns the result of applying the binary operator <tt>opr</tt> to the ! * two BDDs.</p> * * <p>Compare to bdd_apply.</p> *************** *** 408,414 **** /** ! * <p>Makes this BDD be the result of the binary operator opr of two BDDs. The ! * "that" BDD is consumed, and can no longer be used. Attempting to use the ! * passed in BDD again will result in an exception being thrown.</p> * * <p>Compare to bdd_apply and bdd_delref.</p> --- 418,424 ---- /** ! * <p>Makes this BDD be the result of the binary operator <tt>opr</tt> of two ! * BDDs. The "that" BDD is consumed, and can no longer be used. Attempting ! * to use the passed in BDD again will result in an exception being thrown.</p> * * <p>Compare to bdd_apply and bdd_delref.</p> *************** *** 420,425 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs a universal ! * quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appall.</p> --- 430,436 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs a ! * universal quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appall.</p> *************** *** 434,439 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs an ! * existential quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appex.</p> --- 445,451 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs ! * an existential quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appex.</p> *************** *** 448,453 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs a unique ! * quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appuni.</p> --- 460,466 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs ! * a unique quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appuni.</p> *************** *** 463,467 **** /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one ! * variable at each levels. The new BDD implies this BDD and is not false * unless this BDD is false.</p> * --- 476,480 ---- /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one ! * variable at each level. The new BDD implies this BDD and is not false * unless this BDD is false.</p> * *************** *** 485,493 **** /** * <p>Finds one satisfying variable assignment. Finds a minterm in this BDD. ! * The var argument is a set of variables that must be mentioned in the ! * result. The polarity of these variables in the result -- in case they ! * are undefined in this BDD, are defined by the pol parameter. If pol is ! * the false BDD then all variables will be in negative form, and otherwise ! * they will be in positive form.</p> * * <p>Compare to bdd_satoneset.</p> --- 498,506 ---- /** * <p>Finds one satisfying variable assignment. Finds a minterm in this BDD. ! * The <tt>var</tt> argument is a set of variables that must be mentioned in ! * the result. The polarity of these variables in the result - in case they ! * are undefined in this BDD - are defined by the <tt>pol</tt> parameter. ! * If <tt>pol</tt> is false, then all variables will be in negative form. ! * Otherwise they will be in positive form.</p> * * <p>Compare to bdd_satoneset.</p> *************** *** 496,501 **** * @param pol the polarity of the result * @return one satisfying variable assignment */ ! public abstract BDD satOne(BDD var, BDD pol); /** --- 509,515 ---- * @param pol the polarity of the result * @return one satisfying variable assignment + * @see org.sf.javabdd.BDDDomain#set() */ ! public abstract BDD satOne(BDD var, boolean pol); /** *************** *** 544,548 **** /** * <p>Scans this BDD and copies the stored variables into a integer array of ! * variable numbers. The numbers returned are guaranteed to be in * ascending order.</p> * --- 558,562 ---- /** * <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> * *************** *** 598,603 **** /** ! * <p>Finds one satisfying assignment of the domain d in this BDD and returns ! * that value.</p> * * <p>Compare to fdd_scanvar.</p> --- 612,617 ---- /** ! * <p>Finds one satisfying assignment of the domain <tt>d</tt> in this BDD ! * and returns that value.</p> * * <p>Compare to fdd_scanvar.</p> *************** *** 615,621 **** /** ! * <p>Finds one satisfying assignment in this BDD of all the defined FDD ! * variables. Each value is stored in an array which is returned. The size ! * of this array is exactly the number of FDD variables defined.</p> * * <p>Compare to fdd_scanallvar.</p> --- 629,635 ---- /** ! * <p>Finds one satisfying assignment in this BDD of all the defined ! * BDDDomain's. Each value is stored in an array which is returned. The size ! * of this array is exactly the number of BDDDomain's defined.</p> * * <p>Compare to fdd_scanallvar.</p> *************** *** 671,674 **** --- 685,694 ---- } + /** + * Utility function to convert from a BDD varset to an array of levels. + * + * @param r BDD varset + * @return array of levels + */ static int[] varset2levels(BDD r) { int size = 0; *************** *** 696,703 **** /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The var argument is the set of variables that ! * will be mentioned in the result.</p> * * @return an iteration of minterms */ public BDDIterator iterator(final BDD var) { --- 716,725 ---- /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The <tt>var</tt> argument is the set of variables ! * that will be mentioned in the result.</p> * + * @param var set of variables to mention in result * @return an iteration of minterms + * @see org.sf.javabdd.BDDDomain#set() */ public BDDIterator iterator(final BDD var) { *************** *** 705,715 **** } public static class BDDIterator implements Iterator { ! BDDFactory factory; ! int[] levels; ! boolean[] values; ! BDD[] nodes = null; ! boolean more = false; public BDDIterator(BDD dis, BDD var){ factory = dis.getFactory(); --- 727,751 ---- } + /** + * <p>BDDIterator is used to iterate through the satisfying assignments of a BDD. + * It includes the ability to check if bits are dont-cares and skip them.</p> + * + * @author jwhaley + * @version $Id$ + */ public static class BDDIterator implements Iterator { ! protected BDDFactory factory; ! protected int[] levels; ! protected boolean[] values; ! protected BDD[] nodes = null; ! protected boolean more = false; + /** + * <p>Construct a new BDDIterator on the given BDD. The <tt>var</tt> + * argument is the set of variables that will be mentioned in the result.</p> + * + * @param dis BDD to iterate over + * @param var variable set to mention in result + */ public BDDIterator(BDD dis, BDD var){ factory = dis.getFactory(); *************** *** 723,727 **** } ! void fillInSatisfyingAssignment(BDD node, int i) { while (!node.isOne() && !node.isZero()) { int v = node.level(); --- 759,763 ---- } ! protected void fillInSatisfyingAssignment(BDD node, int i) { while (!node.isOne() && !node.isZero()) { int v = node.level(); *************** *** 754,758 **** } ! boolean findNextSatisfyingAssignment() { int i = nodes.length - 1; for (;;) { --- 790,794 ---- } ! protected boolean findNextSatisfyingAssignment() { int i = nodes.length - 1; for (;;) { *************** *** 783,787 **** } ! void increment() { more = false; boolean carry = true; --- 819,823 ---- } ! protected void increment() { more = false; boolean carry = true; *************** *** 798,802 **** } ! BDD buildAndIncrement() { more = false; BDD b = factory.one(); --- 834,838 ---- } ! protected BDD buildAndIncrement() { more = false; BDD b = factory.one(); *************** *** 819,823 **** } ! void free() { for (int i = levels.length - 1; i >= 0; --i) { if (nodes[i] != null) { --- 855,859 ---- } ! protected void free() { for (int i = levels.length - 1; i >= 0; --i) { if (nodes[i] != null) { *************** *** 829,832 **** --- 865,871 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ public Object next() { BDD b; *************** *** 845,856 **** --- 884,909 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ public boolean hasNext() { return nodes != null; } + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ public void remove() { throw new UnsupportedOperationException(); } + /** + * <p>Returns true if the given BDD variable number is a dont-care. + * <tt>var</tt> must be a variable in the iteration set.</p> + * + * @param var variable number to check + * @return if the given variable is a dont-care + * @throws BDDException if var is not in the iteration set + */ public boolean isDontCare(int var) { if (nodes == null) return false; *************** *** 864,867 **** --- 917,928 ---- } + /** + * <p>Returns true if the BDD variables in the given BDD domain are + * all dont-care's.<p> + * + * @param d domain to check + * @return if the variables are all dont-cares + * @throws BDDException if d is not in the iteration set + */ public boolean isDontCare(BDDDomain d) { if (nodes == null) return false; *************** *** 873,877 **** } ! void fastForward0(int var) { if (levels == null) throw new BDDException(); --- 934,938 ---- } ! protected void fastForward0(int var) { if (levels == null) throw new BDDException(); *************** *** 885,888 **** --- 946,954 ---- } + /** + * Fast-forward the iteration such that the given variable number is true. + * + * @param var number of variable + */ public void fastForward(int var) { fastForward0(var); *************** *** 890,893 **** --- 956,965 ---- } + /** + * Assuming <tt>d</tt> is a dont-care, skip to the end of the iteration for + * <tt>d</tt> + * + * @param d BDD domain to fast-forward past + */ public void skipDontCare(BDDDomain d) { int[] vars = d.vars(); *************** *** 901,907 **** /** ! * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The var argument is a set of variables that ! * must be mentioned in the result.</p> * * @return an iteration of minterms --- 973,978 ---- /** ! * <p>This is another version of iterator() that supports the remove() operation. ! * It is much slower than the other one.</p> * * @return an iteration of minterms *************** *** 911,915 **** BDD b = null; - BDD zero; BDD myVar; BDD last = null; --- 982,985 ---- *************** *** 917,925 **** if (!isZero()) { b = id(); - zero = getFactory().zero(); myVar = var.id(); } } public void remove() { if (last != null) { --- 987,997 ---- if (!isZero()) { b = id(); myVar = var.id(); } } + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ public void remove() { if (last != null) { *************** *** 931,947 **** } public boolean hasNext() { return b != null; } public Object next() { if (b == null) throw new NoSuchElementException(); ! BDD c = b.satOne(myVar, zero); b.applyWith(c.id(), BDDFactory.diff); if (b.isZero()) { myVar.free(); myVar = null; b.free(); b = null; - zero.free(); zero = null; } return last = c; --- 1003,1024 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ public boolean hasNext() { return b != null; } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ public Object next() { if (b == null) throw new NoSuchElementException(); ! BDD c = b.satOne(myVar, false); b.applyWith(c.id(), BDDFactory.diff); if (b.isZero()) { myVar.free(); myVar = null; b.free(); b = null; } return last = c; *************** *** 1020,1024 **** } ! int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map) { Integer ri = ((Integer) map.get(this)); if (ri == null) { --- 1097,1101 ---- } ! protected int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map) { Integer ri = ((Integer) map.get(this)); if (ri == null) { *************** *** 1351,1362 **** if (val == 2) { pos |= 1L; - //System.out.print('1'); - } else if (val == 1) { - //System.out.print('0'); - } else { - //System.out.print('x'); } } - //System.out.println(); if (!hasDontCare) { sb.append(ts.elementName(n, pos)); --- 1428,1433 ---- *************** *** 1386,1405 **** } - static boolean[] fdddec2bin(BDDFactory bdd, int var, long val) { - boolean[] res; - int n = 0; - - res = new boolean[bdd.getDomain(var).varNum()]; - - while (val > 0) { - if ((val & 0x1) != 0) - res[n] = true; - val >>= 1; - n++; - } - - return res; - } - /** * <p>BDDToString is used to specify the printing behavior of BDDs with domains. --- 1457,1460 ---- Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** TestBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.13 --- TestBDDFactory.java 14 Oct 2004 19:47:36 -0000 1.14 *************** *** 360,370 **** * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { BDD c1 = ((TestBDD)var).b1; BDD c2 = ((TestBDD)var).b2; ! BDD d1 = ((TestBDD)pol).b1; ! BDD d2 = ((TestBDD)pol).b2; ! BDD r1 = b1.satOne(c1, d1); ! BDD r2 = b2.satOne(c2, d2); return new TestBDD(r1, r2); } --- 360,368 ---- * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, boolean pol) { BDD c1 = ((TestBDD)var).b1; BDD c2 = ((TestBDD)var).b2; ! BDD r1 = b1.satOne(c1, pol); ! BDD r2 = b2.satOne(c2, pol); return new TestBDD(r1, r2); } Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDDomain.java,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** BDDDomain.java 9 Aug 2004 21:48:42 -0000 1.18 --- BDDDomain.java 14 Oct 2004 19:47:36 -0000 1.19 *************** *** 2,5 **** --- 2,6 ---- import java.util.Iterator; + import java.math.BigInteger; /** *************** *** 26,30 **** /* The specified domain (0...N-1) */ ! protected long realsize; /* Variable indices for the variable set */ protected int[] ivar; --- 27,31 ---- /* The specified domain (0...N-1) */ ! protected BigInteger realsize; /* Variable indices for the variable set */ protected int[] ivar; *************** *** 32,38 **** protected BDD var; protected BDDDomain(int index, long range) { ! long calcsize = 2L; ! if (range <= 0L || range > Long.MAX_VALUE/2) throw new BDDException(); this.name = Integer.toString(index); --- 33,47 ---- protected BDD var; + /** + * Default constructor. + * + * @param index index of this domain + * @param range size of this domain + */ protected BDDDomain(int index, long range) { ! } ! protected BDDDomain(int index, BigInteger range) { ! BigInteger calcsize = BigInteger.valueOf(2L); ! if (range.signum() <= 0) throw new BDDException(); this.name = Integer.toString(index); *************** *** 40,46 **** this.realsize = range; int binsize = 1; ! while (calcsize < range) { binsize++; ! calcsize <<= 1; } this.ivar = new int[binsize]; --- 49,55 ---- this.realsize = range; int binsize = 1; ! while (calcsize.compareTo(range) < 0) { binsize++; ! calcsize = calcsize.shiftLeft(1); } this.ivar = new int[binsize]; *************** *** 74,82 **** /** ! * Returns what corresponds to a disjunction of all possible values of this * domain. This is more efficient than doing ithVar(0) OR ithVar(1) ... ! * explicitly for all values in the domain. * ! * Compare to fdd_domain. */ public BDD domain() { --- 83,91 ---- /** ! * <p>Returns what corresponds to a disjunction of all possible values of this * domain. This is more efficient than doing ithVar(0) OR ithVar(1) ... ! * explicitly for all values in the domain.</p> * ! * <p>Compare to fdd_domain.</p> */ public BDD domain() { *************** *** 84,96 **** /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */ ! long val = size() - 1L; BDD d = factory.one(); int[] ivar = vars(); for (int n = 0; n < this.varNum(); n++) { ! if ((val & 0x1L) != 0L) d.orWith(factory.nithVar(ivar[n])); else d.andWith(factory.nithVar(ivar[n])); ! val >>= 1; } return d; --- 93,105 ---- /* 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(); int[] ivar = vars(); for (int n = 0; n < this.varNum(); n++) { ! if (val.testBit(0)) d.orWith(factory.nithVar(ivar[n])); else d.andWith(factory.nithVar(ivar[n])); ! val = val.shiftRight(1); } return d; *************** *** 102,106 **** * Compare to fdd_domainsize. */ ! public long size() { return this.realsize; } --- 111,115 ---- * Compare to fdd_domainsize. */ ! public BigInteger size() { return this.realsize; } *************** *** 209,216 **** */ public BDD ithVar(int val) { ! return ithVar((long) val); } public BDD ithVar(long val) { ! if (val < 0L || val >= this.size()) { throw new BDDException(val+" is out of range"); } --- 218,228 ---- */ public BDD ithVar(int val) { ! return ithVar(BigInteger.valueOf(val)); } public BDD ithVar(long val) { ! return ithVar(BigInteger.valueOf(val)); ! } ! public BDD ithVar(BigInteger val) { ! if (val.signum() < 0 || val.compareTo(size()) >= 0) { throw new BDDException(val+" is out of range"); } *************** *** 220,228 **** int[] ivar = this.vars(); for (int n = 0; n < ivar.length; n++) { ! if ((val & 0x1L) != 0L) v.andWith(factory.ithVar(ivar[n])); else v.andWith(factory.nithVar(ivar[n])); ! val >>= 1; } --- 232,240 ---- int[] ivar = this.vars(); for (int n = 0; n < ivar.length; n++) { ! if (val.testBit(0)) v.andWith(factory.ithVar(ivar[n])); else v.andWith(factory.nithVar(ivar[n])); ! val = val.shiftRight(1); } *************** *** 236,241 **** * @return BDD */ ! public BDD varRange(long lo, long hi) { ! if (lo < 0L || hi >= this.size() || lo > hi) { throw new BDDException("range <"+lo+", "+hi+"> is invalid"); } --- 248,253 ---- * @return BDD */ ! public BDD varRange(BigInteger lo, BigInteger hi) { ! if (lo.signum() < 0 || hi.compareTo(size()) >= 0 || lo.compareTo(hi) > 0) { throw new BDDException("range <"+lo+", "+hi+"> is invalid"); } *************** *** 244,263 **** BDD result = factory.zero(); int[] ivar = this.vars(); ! while (lo <= hi) { ! long bitmask = 1L << (ivar.length - 1); BDD v = factory.one(); for (int n = ivar.length - 1; ; n--) { ! long bit = lo & bitmask; ! if (bit != 0L) { v.andWith(factory.ithVar(ivar[n])); } else { v.andWith(factory.nithVar(ivar[n])); } ! long mask = bitmask - 1L; ! if ((lo & mask) == 0L && (lo | mask) <= hi) { ! lo = (lo | mask) + 1L; break; } - bitmask >>= 1; } result.orWith(v); --- 256,272 ---- BDD result = factory.zero(); int[] ivar = this.vars(); ! while (lo.compareTo(hi) <= 0) { BDD v = factory.one(); for (int n = ivar.length - 1; ; n--) { ! if (lo.testBit(n)) { v.andWith(factory.ithVar(ivar[n])); } else { v.andWith(factory.nithVar(ivar[n])); } ! BigInteger mask = BigInteger.ONE.shiftLeft(n).subtract(BigInteger.ONE); ! if (!lo.testBit(n) && lo.or(mask).compareTo(hi) <= 0) { ! lo = lo.or(mask).add(BigInteger.ONE); break; } } result.orWith(v); Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JFactory.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** JFactory.java 12 Oct 2004 20:41:33 -0000 1.10 --- JFactory.java 14 Oct 2004 19:47:36 -0000 1.11 *************** *** 16,19 **** --- 16,20 ---- import java.io.IOException; import java.io.PrintStream; + import java.math.BigInteger; /** *************** *** 302,311 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { int x = _index; int y = ((bdd) var)._index; ! int z = ((bdd) pol)._index; return new bdd(bdd_satoneset(x, y, z)); } --- 303,312 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { int x = _index; int y = ((bdd) var)._index; ! int z = pol ? 1 : 0; return new bdd(bdd_satoneset(x, y, z)); } *************** *** 5935,5938 **** --- 5936,5942 ---- */ protected BDDDomain createDomain(int a, long b) { + return createDomain(a, BigInteger.valueOf(b)); + } + protected BDDDomain createDomain(int a, BigInteger b) { return new bddDomain(a, b); } *************** *** 5940,5944 **** class bddDomain extends BDDDomain { ! bddDomain(int a, long b) { super(a, b); } --- 5944,5948 ---- class bddDomain extends BDDDomain { ! bddDomain(int a, BigInteger b) { super(a, b); } Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDFactory.java,v retrieving revision 1.29 retrieving revision 1.30 diff -C2 -d -r1.29 -r1.30 *** BDDFactory.java 12 Oct 2004 20:37:19 -0000 1.29 --- BDDFactory.java 14 Oct 2004 19:47:36 -0000 1.30 *************** *** 903,907 **** d = domain[fdvarnum]; ! d.realsize = d1.realsize * d2.realsize; d.ivar = new int[d1.varNum() + d2.varNum()]; --- 903,907 ---- d = domain[fdvarnum]; ! d.realsize = d1.realsize.multiply(d2.realsize); d.ivar = new int[d1.varNum() + d2.varNum()]; Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.20 retrieving revision 1.21 diff -C2 -d -r1.20 -r1.21 *** TypedBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.20 --- TypedBDDFactory.java 14 Oct 2004 19:47:36 -0000 1.21 *************** *** 4,9 **** package org.sf.javabdd; - import java.io.IOException; - import java.io.PrintStream; import java.util.Collection; import java.util.Comparator; --- 4,7 ---- *************** *** 15,18 **** --- 13,19 ---- import java.util.TreeMap; import java.util.TreeSet; + import java.io.IOException; + import java.io.PrintStream; + import java.math.BigInteger; /** *************** *** 865,873 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { TypedBDD bdd1 = (TypedBDD) var; - TypedBDD bdd2 = (TypedBDD) pol; Set newDom = makeSet(); newDom.addAll(dom); --- 866,873 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { TypedBDD bdd1 = (TypedBDD) var; Set newDom = makeSet(); newDom.addAll(dom); *************** *** 878,882 **** } newDom.addAll(bdd1.dom); ! return new TypedBDD(bdd.satOne(bdd1.bdd, bdd2.bdd), newDom); } --- 878,882 ---- } newDom.addAll(bdd1.dom); ! return new TypedBDD(bdd.satOne(bdd1.bdd, pol), newDom); } *************** *** 1092,1096 **** * @see org.sf.javabdd.BDDDomain#varRange(long, long) */ ! public BDD varRange(long lo, long hi) { BDD v = domain.varRange(lo, hi); Set s = makeSet(); --- 1092,1096 ---- * @see org.sf.javabdd.BDDDomain#varRange(long, long) */ ! public BDD varRange(BigInteger lo, BigInteger hi) { BDD v = domain.varRange(lo, hi); Set s = makeSet(); Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** JDDFactory.java 12 Oct 2004 20:41:33 -0000 1.7 --- JDDFactory.java 14 Oct 2004 19:47:36 -0000 1.8 *************** *** 399,406 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { ! throw new BDDException(); } --- 399,407 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { ! // TODO Implement this. ! throw new UnsupportedOperationException(); } Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.36 retrieving revision 1.37 diff -C2 -d -r1.36 -r1.37 *** BuDDyFactory.java 12 Oct 2004 20:41:33 -0000 1.36 --- BuDDyFactory.java 14 Oct 2004 19:47:36 -0000 1.37 *************** *** 764,773 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { BuDDyBDD c = (BuDDyBDD) var; ! BuDDyBDD d = (BuDDyBDD) pol; ! int b = satOne1(_id, c._id, d._id); return makeBDD(b); } --- 764,772 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { BuDDyBDD c = (BuDDyBDD) var; ! int b = satOne1(_id, c._id, pol?1:0); return makeBDD(b); } Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CUDDFactory.java,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** CUDDFactory.java 12 Oct 2004 20:41:33 -0000 1.18 --- CUDDFactory.java 14 Oct 2004 19:47:36 -0000 1.19 *************** *** 658,664 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { // TODO Implement this. throw new UnsupportedOperationException(); --- 658,664 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CALFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** CALFactory.java 12 Oct 2004 20:41:33 -0000 1.6 --- CALFactory.java 14 Oct 2004 19:47:36 -0000 1.7 *************** *** 654,660 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { // TODO Implement this. throw new UnsupportedOperationException(); --- 654,660 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); |
From: John W. <joe...@us...> - 2004-10-12 20:44:02
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1066 Modified Files: buddy_jni.c Log Message: Added support for setError, etc. Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.19 retrieving revision 1.20 diff -C2 -d -r1.19 -r1.20 *** buddy_jni.c 22 Jul 2004 22:00:53 -0000 1.19 --- buddy_jni.c 12 Oct 2004 20:43:42 -0000 1.20 *************** *** 232,235 **** --- 232,265 ---- } + extern int bdderrorcond; + + /* + * Class: org_sf_javabdd_BuDDyFactory + * Method: setError0 + * Signature: (I)V + */ + JNIEXPORT void JNICALL Java_org_sf_javabdd_BuDDyFactory_setError0 + (JNIEnv *env, jclass cl, jint code) + { + #if defined(TRACE_BUDDYLIB) + printf("bdd_setError(%d)\n", code); + #endif + bdderrorcond = code; + } + + /* + * Class: org_sf_javabdd_BuDDyFactory + * Method: clearError0 + * Signature: ()V + */ + JNIEXPORT void JNICALL Java_org_sf_javabdd_BuDDyFactory_clearError0 + (JNIEnv *env, jclass cl) + { + #if defined(TRACE_BUDDYLIB) + printf("bdd_clearError()\n"); + #endif + bdderrorcond = 0; + } + /* * Class: org_sf_javabdd_BuDDyFactory |
From: John W. <joe...@us...> - 2004-10-12 20:43:01
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv802 Modified Files: Makefile Log Message: Change intel compiler flags. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.31 retrieving revision 1.32 diff -C2 -d -r1.31 -r1.32 *** Makefile 2 Oct 2004 08:10:06 -0000 1.31 --- Makefile 12 Oct 2004 20:42:52 -0000 1.32 *************** *** 34,38 **** CAL_DLL_NAME = cal.dll ifeq (${CC},icl) # Intel Windows compiler ! CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND /fast $(EXTRA_CFLAGS) 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 --- 34,38 ---- CAL_DLL_NAME = cal.dll ifeq (${CC},icl) # Intel Windows compiler ! CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND /O2 /Ob2 $(EXTRA_CFLAGS) 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 |
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv567/org/sf/javabdd Modified Files: BuDDyFactory.java CALFactory.java CUDDFactory.java JDDFactory.java JFactory.java TestBDDFactory.java TypedBDDFactory.java Log Message: Added support for setError, etc. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.35 retrieving revision 1.36 diff -C2 -d -r1.35 -r1.36 *** BuDDyFactory.java 14 Sep 2004 23:53:30 -0000 1.35 --- BuDDyFactory.java 12 Oct 2004 20:41:33 -0000 1.36 *************** *** 161,164 **** --- 161,180 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + setError0(code); + } + private static native void setError0(int code); + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + clearError0(); + } + private static native void clearError0(); + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JFactory.java,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** JFactory.java 15 Sep 2004 00:02:07 -0000 1.9 --- JFactory.java 12 Oct 2004 20:41:33 -0000 1.10 *************** *** 4246,4249 **** --- 4246,4263 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + bdderrorcond = code; + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + bdderrorcond = 0; + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.19 retrieving revision 1.20 diff -C2 -d -r1.19 -r1.20 *** TypedBDDFactory.java 12 Aug 2004 21:18:27 -0000 1.19 --- TypedBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.20 *************** *** 84,87 **** --- 84,101 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + factory.setError(code); + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + factory.clearError(); + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** JDDFactory.java 15 Sep 2004 03:03:39 -0000 1.6 --- JDDFactory.java 12 Oct 2004 20:41:33 -0000 1.7 *************** *** 537,540 **** --- 537,554 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + // TODO Implement this. + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + // TODO Implement this. + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CUDDFactory.java,v retrieving revision 1.17 retrieving revision 1.18 diff -C2 -d -r1.17 -r1.18 *** CUDDFactory.java 2 Aug 2004 20:20:53 -0000 1.17 --- CUDDFactory.java 12 Oct 2004 20:41:33 -0000 1.18 *************** *** 112,115 **** --- 112,129 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + // TODO Implement this. + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + // TODO Implement this. + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** TestBDDFactory.java 15 Sep 2004 03:02:53 -0000 1.12 --- TestBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.13 *************** *** 533,536 **** --- 533,552 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + f1.setError(code); + f2.setError(code); + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + f1.clearError(); + f2.clearError(); + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CALFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** CALFactory.java 2 Aug 2004 20:20:53 -0000 1.5 --- CALFactory.java 12 Oct 2004 20:41:33 -0000 1.6 *************** *** 112,115 **** --- 112,129 ---- /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#setError(int) + */ + public void setError(int code) { + // TODO Implement this. + } + + /* (non-Javadoc) + * @see org.sf.javabdd.BDDFactory#clearError() + */ + public void clearError() { + // TODO Implement this. + } + + /* (non-Javadoc) * @see org.sf.javabdd.BDDFactory#setMaxNodeNum(int) */ |
From: John W. <joe...@us...> - 2004-10-12 20:40:29
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32721/org/sf/javabdd Modified Files: BDD.java Log Message: Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDD.java,v retrieving revision 1.36 retrieving revision 1.37 diff -C2 -d -r1.36 -r1.37 *** BDD.java 12 Aug 2004 23:26:03 -0000 1.36 --- BDD.java 12 Oct 2004 20:40:17 -0000 1.37 *************** *** 1141,1145 **** * occurred in the BDD.</p> * ! * <p>Compare to bdd_varprofile.</p> */ public abstract int[] varProfile(); --- 1141,1146 ---- * occurred in the BDD.</p> * ! * <p>Compare to bdd_varprofile.</p> ! */ public abstract int[] varProfile(); |
From: John W. <joe...@us...> - 2004-10-12 20:37:28
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32141/org/sf/javabdd Modified Files: BDDFactory.java Log Message: Added setError, etc. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDFactory.java,v retrieving revision 1.28 retrieving revision 1.29 diff -C2 -d -r1.28 -r1.29 *** BDDFactory.java 15 Sep 2004 19:35:25 -0000 1.28 --- BDDFactory.java 12 Oct 2004 20:37:19 -0000 1.29 *************** *** 26,30 **** public abstract class BDDFactory { ! /** Initializes a BDD factory with the given initial node table size * and operation cache size. Tries to use the "buddy" native library; * if it fails, it falls back to the "java" library. --- 26,31 ---- public abstract class BDDFactory { ! /** ! * Initializes a BDD factory with the given initial node table size * and operation cache size. Tries to use the "buddy" native library; * if it fails, it falls back to the "java" library. *************** *** 39,43 **** } ! /** Initializes a BDD factory of the given type with the given initial * node table size and operation cache size. The type is a string that * can be "buddy", "cudd", "cal", "j", "java", "jdd", "test", "typed", or --- 40,45 ---- } ! /** ! * Initializes a BDD factory of the given type with the given initial * node table size and operation cache size. The type is a string that * can be "buddy", "cudd", "cal", "j", "java", "jdd", "test", "typed", or *************** *** 241,245 **** --- 243,258 ---- public abstract void done(); + /** + * Sets the error condition. This will cause the BDD package to throw an + * exception at the next garbage collection. + * + * @param code the error code to set + */ + public abstract void setError(int code); + /** + * Clears any outstanding error condition. + */ + public abstract void clearError(); /**** CACHE/TABLE PARAMETERS ****/ *************** *** 635,642 **** * instance the current number of variables is 3 and neworder contains * [1; 0; 2] then the new variable order is v1<v0<v2. ! * * @param neworder */ public abstract void setVarOrder(int[] neworder); - /**** VARIABLE BLOCKS ****/ --- 648,656 ---- * instance the current number of variables is 3 and neworder contains * [1; 0; 2] then the new variable order is v1<v0<v2. ! * ! * @param neworder new variable order ! */ public abstract void setVarOrder(int[] neworder); /**** VARIABLE BLOCKS ****/ |
From: John W. <joe...@us...> - 2004-10-12 20:34:24
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31557/buddy/src Modified Files: prime.h Log Message: Fixed define check for Windows. Index: prime.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/prime.h,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** prime.h 29 Sep 2004 10:04:34 -0000 1.2 --- prime.h 12 Oct 2004 20:34:06 -0000 1.3 *************** *** 42,46 **** unsigned int bdd_prime_lte(unsigned int src); ! #ifdef _MSC_VER #define srand48(x) srand(x) #define lrand48(x) rand(x) --- 42,46 ---- unsigned int bdd_prime_lte(unsigned int src); ! #if defined(_MSC_VER) || defined(WIN32) #define srand48(x) srand(x) #define lrand48(x) rand(x) |
From: John W. <joe...@us...> - 2004-10-02 08:15:10
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv10960/buddy/src Modified Files: bddop.c Log Message: Turn off prefetching by default. Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** bddop.c 1 Oct 2004 04:03:23 -0000 1.5 --- bddop.c 2 Oct 2004 08:13:34 -0000 1.6 *************** *** 643,648 **** --- 643,652 ---- if (andcache.table == NULL && BddCache3_init(&andcache,cachesize) < 0) return bdd_error(BDD_MEMORY); + #if defined(AND_ITR) + return and_itr(l, r); + #else return and_rec(l, r); #endif + #endif #if defined(SPECIALIZE_OR) case bddop_or: *************** *** 775,782 **** --- 779,790 ---- return l; + #if PREFETCH > 0 /* Prefetch nodes to get some concurrency between cache lookup and node table lookup. */ _mm_prefetch(&bddnodes[l], 0); + #if PREFETCH > 1 _mm_prefetch(&bddnodes[r], 0); + #endif + #endif entry = BddCache_lookup(&andcache, ANDHASH(l,r)); *************** *** 822,825 **** --- 830,836 ---- } + static int* gstack; + static int gstack_size; + static BDD and_itr(BDD l0, BDD r0) { *************** *** 827,831 **** --- 838,852 ---- int* s_top; int* s_ptr; + #if defined(USE_ALLOCA) s_top = s_ptr = alloca(bddvarnum * sizeof(int) * 9); + #else + if (gstack_size < bddvarnum) { + if (gstack != NULL) free(gstack); + if ((gstack=NEW(int,bddvarnum*9)) == NULL) + bdd_error(BDD_MEMORY); + gstack_size = bddvarnum; + } + s_top = s_ptr = gstack; + #endif *s_ptr++ = l0; *s_ptr++ = r0; *************** *** 846,853 **** --- 867,878 ---- } else { + #if PREFETCH > 0 /* Prefetch nodes to get some concurrency between cache lookup and node table lookup. */ _mm_prefetch(&bddnodes[l1], 0); + #if PREFETCH > 1 _mm_prefetch(&bddnodes[r1], 0); + #endif + #endif entry = BddCache_lookup(&andcache, ANDHASH(l1,r1)); *************** *** 941,948 **** --- 966,977 ---- return l; + #if PREFETCH > 0 /* Prefetch nodes to get some concurrency between cache lookup and node table lookup. */ _mm_prefetch(&bddnodes[l], 0); + #if PREFETCH > 1 _mm_prefetch(&bddnodes[r], 0); + #endif + #endif entry = BddCache_lookup(&orcache, ORHASH(l,r)); *************** *** 2425,2429 **** --- 2454,2462 ---- return bdd_error(BDD_MEMORY); #endif + #if defined(RELPROD_ITR) + return relprod_itr(l, r); + #else return relprod_rec(l, r); + #endif } #endif *************** *** 2556,2563 **** --- 2589,2598 ---- return quant_rec(r); + #if PREFETCH > 2 /* Prefetch LOW(l) to get some concurrency between cache lookup and node table lookup. LOW(l) is not that expensive because we need to load LEVEL(l) right after this anyway. */ _mm_prefetch(&bddnodes[LOW(l)], 0); + #endif if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) *************** *** 2565,2569 **** applyop = bddop_and; #if defined(SPECIALIZE_AND) ! res = and_rec(l,r); #else res = apply_rec(l,r); --- 2600,2608 ---- applyop = bddop_and; #if defined(SPECIALIZE_AND) ! #if defined(AND_ITR) ! res = and_itr(l, r); ! #else ! res = and_rec(l, r); ! #endif #else res = apply_rec(l,r); *************** *** 2648,2660 **** } else { /* Prefetch LOW(l1) to get some concurrency between cache lookup and node table lookup. LOW(l1) is not that expensive because we need to load LEVEL(l1) right after this anyway. */ _mm_prefetch(&bddnodes[LOW(l1)], 0); if (LEVEL(l1) > quantlast && LEVEL(r1) > quantlast) { applyop = bddop_and; #if defined(SPECIALIZE_AND) ! res1 = and_rec(l1,r1); #else res1 = apply_rec(l1,r1); --- 2687,2705 ---- } else { + #if PREFETCH > 2 /* Prefetch LOW(l1) to get some concurrency between cache lookup and node table lookup. LOW(l1) is not that expensive because we need to load LEVEL(l1) right after this anyway. */ _mm_prefetch(&bddnodes[LOW(l1)], 0); + #endif if (LEVEL(l1) > quantlast && LEVEL(r1) > quantlast) { applyop = bddop_and; #if defined(SPECIALIZE_AND) ! #if defined(AND_ITR) ! res1 = and_itr(l1, r1); ! #else ! res1 = and_rec(l1, r1); ! #endif #else res1 = apply_rec(l1,r1); |
From: John W. <joe...@us...> - 2004-10-02 08:11:55
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv10426 Modified Files: Makefile Log Message: update opt_report rule Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.30 retrieving revision 1.31 diff -C2 -d -r1.30 -r1.31 *** Makefile 30 Sep 2004 03:26:14 -0000 1.30 --- Makefile 2 Oct 2004 08:10:06 -0000 1.31 *************** *** 230,234 **** opt_report: ! icl -Qopt_report -Qopt_report_phase all $(INCLUDES) $(CFLAGS) $(DLL_OUTPUT_OPTION)buddy.dll $(BUDDY_SRCS) -LD /link /libpath:$(JDK_ROOT)/lib test: $(EXAMPLE_CLASSFILES) --- 230,234 ---- opt_report: ! icl -fast -Qopt_report_fileOPTREPORT.txt -Qopt_report_phase all -Qopt_report_levelmax -Qvec_report3 -Qpar_report3 $(INCLUDES) $(CFLAGS) /obuddy.dll $(BUDDY_SRCS) -LD /link /libpath:$(JDK_ROOT)/lib test: $(EXAMPLE_CLASSFILES) |
From: John W. <joe...@us...> - 2004-10-01 04:03:53
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7897/buddy/src Modified Files: bddop.c Log Message: For whatever reason, the recursive functions are quite a bit faster than the iterative ones !? using and_itr, relprod_itr : 248s using and_rec, relprod_itr : 238s using and_rec, relprod_rec : 233s Also introduced a few more prefetch instructions. Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** bddop.c 1 Oct 2004 02:17:20 -0000 1.4 --- bddop.c 1 Oct 2004 04:03:23 -0000 1.5 *************** *** 159,162 **** --- 159,163 ---- #if defined(SPECIALIZE_AND) static BDD and_rec(BDD, BDD); + static BDD and_itr(BDD, BDD); #endif #if defined(SPECIALIZE_RELPROD) *************** *** 774,778 **** --- 775,782 ---- return l; + /* Prefetch nodes to get some concurrency between cache lookup + and node table lookup. */ _mm_prefetch(&bddnodes[l], 0); + _mm_prefetch(&bddnodes[r], 0); entry = BddCache_lookup(&andcache, ANDHASH(l,r)); *************** *** 817,820 **** --- 821,926 ---- return res; } + + static BDD and_itr(BDD l0, BDD r0) + { + BDD res; + int* s_top; + int* s_ptr; + s_top = s_ptr = alloca(bddvarnum * sizeof(int) * 9); + *s_ptr++ = l0; + *s_ptr++ = r0; + + while (s_top != s_ptr) { + int hash, lev; + BDD l1, r1, res1; + BddCacheData3 *entry; + outer: + r1 = *(--s_ptr); + l1 = *(--s_ptr); + if (l1 == r1 || ISONE(r1)) { + res1 = l1; + } else if (ISZERO(l1) || ISZERO(r1)) { + res1 = 0; + } else if (ISONE(l1)) { + res1 = r1; + } else { + + /* Prefetch nodes to get some concurrency between cache lookup + and node table lookup. */ + _mm_prefetch(&bddnodes[l1], 0); + _mm_prefetch(&bddnodes[r1], 0); + + entry = BddCache_lookup(&andcache, ANDHASH(l1,r1)); + if (entry->a == l1 && entry->b == r1) { + #ifdef CACHESTATS + bddcachestats.opHit++; + #endif + res1 = entry->res; + } else { + #ifdef CACHESTATS + bddcachestats.opMiss++; + #endif + *s_ptr++ = l1; + *s_ptr++ = r1; + *s_ptr++ = (int)(entry - andcache.table); + if (LEVEL(l1) == LEVEL(r1)) { + *s_ptr++ = LEVEL(l1); + *s_ptr++ = HIGH(l1); + *s_ptr++ = HIGH(r1); + *s_ptr++ = -1; + *s_ptr++ = LOW(l1); + *s_ptr++ = LOW(r1); + continue; + } else if (LEVEL(l1) < LEVEL(r1)) { + *s_ptr++ = LEVEL(l1); + *s_ptr++ = HIGH(l1); + *s_ptr++ = r1; + *s_ptr++ = -1; + *s_ptr++ = LOW(l1); + *s_ptr++ = r1; + continue; + } else { + *s_ptr++ = LEVEL(r1); + *s_ptr++ = l1; + *s_ptr++ = HIGH(r1); + *s_ptr++ = -1; + *s_ptr++ = l1; + *s_ptr++ = LOW(r1); + continue; + } + } + } + if (s_top == s_ptr) { + res = res1; + goto end; + } + PUSHREF(res1); + for (;;) { + lev = *(--s_ptr); + if (lev < 0) { + goto outer; + } + hash = *(--s_ptr); + r1 = *(--s_ptr); + l1 = *(--s_ptr); + entry = &andcache.table[hash]; + res1 = bdd_makenode(lev, READREF(2), READREF(1)); + POPREF(2); + + entry->a = l1; + entry->b = r1; + entry->res = res1; + + if (s_top == s_ptr) { + res = res1; + goto end; + } + + PUSHREF(res1); + } + } + end: + return res; + } #endif *************** *** 835,838 **** --- 941,949 ---- return l; + /* Prefetch nodes to get some concurrency between cache lookup + and node table lookup. */ + _mm_prefetch(&bddnodes[l], 0); + _mm_prefetch(&bddnodes[r], 0); + entry = BddCache_lookup(&orcache, ORHASH(l,r)); *************** *** 2314,2318 **** return bdd_error(BDD_MEMORY); #endif ! return relprod_itr(l, r); } #endif --- 2425,2429 ---- return bdd_error(BDD_MEMORY); #endif ! return relprod_rec(l, r); } #endif *************** *** 2445,2448 **** --- 2556,2562 ---- return quant_rec(r); + /* Prefetch LOW(l) to get some concurrency between cache lookup + and node table lookup. LOW(l) is not that expensive because we + need to load LEVEL(l) right after this anyway. */ _mm_prefetch(&bddnodes[LOW(l)], 0); *************** *** 2532,2580 **** } else if (l1 == 1) { res1 = quant_rec(r1); ! } else if (LEVEL(l1) > quantlast && LEVEL(r1) > quantlast) { ! applyop = bddop_and; #if defined(SPECIALIZE_AND) ! res1 = and_rec(l1,r1); #else ! res1 = apply_rec(l1,r1); #endif ! applyop = bddop_or; ! } else { ! entry = BddCache_lookup(&appexcache, APPEXHASH(l1,r1,bddop_and)); ! if (entry->a == l1 && entry->b == r1 && entry->r.c == appexid) { ! res1 = entry->r.res; ! } else if (LEVEL(l1) == LEVEL(r1)) { ! *s_ptr++ = l1; ! *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - appexcache.table); ! *s_ptr++ = LEVEL(l1); ! *s_ptr++ = HIGH(l1); ! *s_ptr++ = HIGH(r1); ! *s_ptr++ = -1; ! *s_ptr++ = LOW(l1); ! *s_ptr++ = LOW(r1); ! continue; ! } else if (LEVEL(l1) < LEVEL(r1)) { ! *s_ptr++ = l1; ! *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - appexcache.table); ! *s_ptr++ = LEVEL(l1); ! *s_ptr++ = HIGH(l1); ! *s_ptr++ = r1; ! *s_ptr++ = -1; ! *s_ptr++ = LOW(l1); ! *s_ptr++ = r1; ! continue; } else { ! *s_ptr++ = l1; ! *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - appexcache.table); ! *s_ptr++ = LEVEL(r1); ! *s_ptr++ = l1; ! *s_ptr++ = HIGH(r1); ! *s_ptr++ = -1; ! *s_ptr++ = l1; ! *s_ptr++ = LOW(r1); ! continue; } } --- 2646,2704 ---- } else if (l1 == 1) { res1 = quant_rec(r1); ! } else { ! ! /* Prefetch LOW(l1) to get some concurrency between cache lookup ! and node table lookup. LOW(l1) is not that expensive because we ! need to load LEVEL(l1) right after this anyway. */ ! _mm_prefetch(&bddnodes[LOW(l1)], 0); ! ! if (LEVEL(l1) > quantlast && LEVEL(r1) > quantlast) { ! applyop = bddop_and; #if defined(SPECIALIZE_AND) ! res1 = and_rec(l1,r1); #else ! res1 = apply_rec(l1,r1); #endif ! applyop = bddop_or; } else { ! entry = BddCache_lookup(&appexcache, APPEXHASH(l1,r1,bddop_and)); ! if (entry->a == l1 && entry->b == r1 && entry->r.c == appexid) { ! #ifdef CACHESTATS ! bddcachestats.opHit++; ! #endif ! res1 = entry->r.res; ! } else { ! #ifdef CACHESTATS ! bddcachestats.opMiss++; ! #endif ! *s_ptr++ = l1; ! *s_ptr++ = r1; ! *s_ptr++ = (int)(entry - appexcache.table); ! if (LEVEL(l1) == LEVEL(r1)) { ! *s_ptr++ = LEVEL(l1); ! *s_ptr++ = HIGH(l1); ! *s_ptr++ = HIGH(r1); ! *s_ptr++ = -1; ! *s_ptr++ = LOW(l1); ! *s_ptr++ = LOW(r1); ! continue; ! } else if (LEVEL(l1) < LEVEL(r1)) { ! *s_ptr++ = LEVEL(l1); ! *s_ptr++ = HIGH(l1); ! *s_ptr++ = r1; ! *s_ptr++ = -1; ! *s_ptr++ = LOW(l1); ! *s_ptr++ = r1; ! continue; ! } else { ! *s_ptr++ = LEVEL(r1); ! *s_ptr++ = l1; ! *s_ptr++ = HIGH(r1); ! *s_ptr++ = -1; ! *s_ptr++ = l1; ! *s_ptr++ = LOW(r1); ! continue; ! } ! } } } |
From: John W. <joe...@us...> - 2004-10-01 02:17:34
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22244/buddy/src Modified Files: bddop.c kernel.h kernel.c reorder.c bddio.c Log Message: Implement bitfields directly, because the compiler does a poor job at it. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** kernel.h 29 Sep 2004 10:03:50 -0000 1.2 --- kernel.h 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 79,84 **** --- 79,88 ---- typedef struct s_BddNode /* Node table entry */ { + #if defined(USE_BITFIELDS) unsigned int refcou : 10; unsigned int level : 22; + #else + unsigned int refcou_and_level; + #endif int low; int high; *************** *** 122,141 **** /* Reference counting */ ! #define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou-- ! #define INCREF(n) if (bddnodes[n].refcou<MAXREF) bddnodes[n].refcou++ ! #define DECREFp(n) if (n->refcou!=MAXREF && n->refcou>0) n->refcou-- ! #define INCREFp(n) if (n->refcou<MAXREF) n->refcou++ ! #define HASREF(n) (bddnodes[n].refcou > 0) /* Marking BDD nodes */ ! #define MARKON 0x200000 /* Bit used to mark a node (1) */ ! #define MARKOFF 0x1FFFFF /* - unmark */ #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (bddnodes[n].level |= MARKON) ! #define UNMARK(n) (bddnodes[n].level &= MARKOFF) ! #define MARKED(n) (bddnodes[n].level & MARKON) ! #define SETMARKp(p) (node->level |= MARKON) ! #define UNMARKp(p) (node->level &= MARKOFF) ! #define MARKEDp(p) (node->level & MARKON) /* Hashfunctions */ --- 126,167 ---- /* Reference counting */ ! #if defined(USE_BITFIELDS) ! #define DECREF(n) if (REF(n)!=MAXREF && REF(n)>0) bddnodes[n].refcou-- ! #define INCREF(n) if (REF(n)<MAXREF) bddnodes[n].refcou++ ! #define DECREFp(n) if (REFp(n)!=MAXREF && REFp(n)>0) n->refcou-- ! #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou++ ! #define HASREF(n) (REF(n) > 0) ! #else ! #define DECREF(n) if (REF(n)!=MAXREF && REF(n)>0) bddnodes[n].refcou_and_level-- ! #define INCREF(n) if (REF(n)<MAXREF) bddnodes[n].refcou_and_level++ ! #define DECREFp(n) if (REFp(n)!=MAXREF && REFp(n)>0) n->refcou_and_level-- ! #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ ! #define HASREF(n) (REF(n) > 0) ! #endif /* Marking BDD nodes */ ! ! #if defined(USE_BITFIELDS) ! #define MARKON1 0x200000 /* Bit used to mark a node (1) */ ! #define MARKOFF1 0x1FFFFF /* - unmark */ #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (LEVEL(n) |= MARKON1) ! #define UNMARK(n) (LEVEL(n) &= MARKOFF1) ! #define MARKED(n) (LEVEL(n) & MARKON1) ! #define SETMARKp(p) (LEVELp(p) |= MARKON1) ! #define UNMARKp(p) (LEVELp(p) &= MARKOFF1) ! #define MARKEDp(p) (LEVELp(p) & MARKON1) ! #else ! #define MARKON2 0x80000000 /* Bit used to mark a node (1) */ ! #define MARKOFF2 0x7FFFFFFF /* - unmark */ ! #define MARKHIDE 0x1FFFFF ! #define SETMARK(n) (bddnodes[n].refcou_and_level |= MARKON2) ! #define UNMARK(n) (bddnodes[n].refcou_and_level &= MARKOFF2) ! #define MARKED(n) (bddnodes[n].refcou_and_level & MARKON2) ! #define SETMARKp(p) ((p)->refcou_and_level |= MARKON2) ! #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) ! #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif ! /* Hashfunctions */ *************** *** 150,159 **** #define ISONE(a) ((a) == 1) #define ISZERO(a) ((a) == 0) - #define LEVEL(a) (bddnodes[a].level) #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) - #define LEVELp(p) ((p)->level) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) /* Stacking for garbage collector */ --- 176,204 ---- #define ISONE(a) ((a) == 1) #define ISZERO(a) ((a) == 0) #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) + #if defined(USE_BITFIELDS) + #define REF(n) (bddnodes[n].refcou) + #define REFp(n) ((n)->refcou) + #define SETREF(n,v) (bddnodes[n].refcou = (v)) + #define SETREFp(n,v) ((n)->refcou = (v)) + #define LEVEL(n) (bddnodes[n].level) + #define LEVELp(p) ((p)->level) + #define SETLEVEL(n,v) (LEVEL(n) = (v)) + #define SETLEVELp(p,v) (LEVELp(p) = (v)) + #define CLRLEVELREF(n) (bddnodes[n].refcou = bddnodes[n].level = 0) + #else + #define REF(n) (bddnodes[n].refcou_and_level & MAXREF) + #define REFp(n) ((n)->refcou_and_level & MAXREF) + #define SETREF(n,v) (bddnodes[n].refcou_and_level = (bddnodes[n].refcou_and_level & ~MAXREF) | (v)) + #define SETREFp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & ~MAXREF) | (v)) + #define LEVEL(n) (bddnodes[n].refcou_and_level >> 10) + #define LEVELp(p) ((p)->refcou_and_level >> 10) + #define SETLEVEL(n,v) (bddnodes[n].refcou_and_level = (bddnodes[n].refcou_and_level & MAXREF) | (v << 10)) + #define SETLEVELp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) + #define CLRLEVELREF(n) (bddnodes[n].refcou_and_level = 0) + #endif /* Stacking for garbage collector */ *************** *** 181,188 **** #define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) ) ! ! #ifdef _MSC_VER #define srand48(x) srand(x) #define lrand48(x) rand(x) #endif --- 226,234 ---- #define NEW(t,n) ( (t*)malloc(sizeof(t)*(n)) ) ! /* Compatibility with Windows */ ! #if defined(_MSC_VER) || defined(WIN32) #define srand48(x) srand(x) #define lrand48(x) rand(x) + #define alloca(x) _alloca(x) #endif Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** kernel.c 29 Sep 2004 10:00:50 -0000 1.2 --- kernel.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 217,229 **** for (n=0 ; n<bddnodesize ; n++) { ! bddnodes[n].refcou = 0; LOW(n) = -1; bddnodes[n].hash = 0; - LEVEL(n) = 0; bddnodes[n].next = n+1; } bddnodes[bddnodesize-1].next = 0; ! bddnodes[0].refcou = bddnodes[1].refcou = MAXREF; LOW(0) = HIGH(0) = 0; LOW(1) = HIGH(1) = 1; --- 217,229 ---- for (n=0 ; n<bddnodesize ; n++) { ! CLRLEVELREF(n); LOW(n) = -1; bddnodes[n].hash = 0; bddnodes[n].next = n+1; } bddnodes[bddnodesize-1].next = 0; ! SETREF(0, MAXREF); ! SETREF(1, MAXREF); LOW(0) = HIGH(0) = 0; LOW(1) = HIGH(1) = 1; *************** *** 398,409 **** } ! bddnodes[bddvarset[bddvarnum*2]].refcou = MAXREF; ! bddnodes[bddvarset[bddvarnum*2+1]].refcou = MAXREF; bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; } ! LEVEL(0) = num; ! LEVEL(1) = num; bddvar2level[num] = num; bddlevel2var[num] = num; --- 398,409 ---- } ! SETREF(bddvarset[bddvarnum*2], MAXREF); ! SETREF(bddvarset[bddvarnum*2+1], MAXREF); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; } ! SETLEVEL(0, num); ! SETLEVEL(1, num); bddvar2level[num] = num; bddlevel2var[num] = num; *************** *** 1139,1143 **** for (n=0 ; n<bddnodesize ; n++) { ! if (bddnodes[n].refcou > 0) bdd_mark(n); bddnodes[n].hash = 0; --- 1139,1143 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (REF(n) > 0) bdd_mark(n); bddnodes[n].hash = 0; *************** *** 1151,1159 **** register BddNode *node = &bddnodes[n]; ! if ((LEVELp(node) & MARKON) && LOWp(node) != -1) { register unsigned int hash; ! LEVELp(node) &= MARKOFF; hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); node->next = bddnodes[hash].hash; --- 1151,1159 ---- register BddNode *node = &bddnodes[n]; ! if (MARKEDp(node) && LOWp(node) != -1) { register unsigned int hash; ! UNMARKp(node); hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); node->next = bddnodes[hash].hash; *************** *** 1261,1268 **** node = &bddnodes[i]; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; ! LEVELp(node) |= MARKON; bdd_mark(LOWp(node)); --- 1261,1268 ---- node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == -1) return; ! SETMARKp(node); bdd_mark(LOWp(node)); *************** *** 1278,1282 **** return; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; --- 1278,1282 ---- return; ! if (MARKEDp(node) || LOWp(node) == -1) return; *************** *** 1284,1288 **** return; ! LEVELp(node) |= MARKON; bdd_mark_upto(LOWp(node), level); --- 1284,1288 ---- return; ! SETMARKp(node); bdd_mark_upto(LOWp(node), level); *************** *** 1335,1342 **** return; ! if (!(LEVELp(node) & MARKON)) return; ! LEVELp(node) &= MARKOFF; if (LEVELp(node) > level) --- 1335,1342 ---- return; ! if (!MARKEDp(node)) return; ! UNMARKp(node); if (LEVELp(node) > level) *************** *** 1428,1432 **** node = &bddnodes[res]; ! LEVELp(node) = level; LOWp(node) = low; HIGHp(node) = high; --- 1428,1432 ---- node = &bddnodes[res]; ! SETLEVELp(node, level); LOWp(node) = low; HIGHp(node) = high; *************** *** 1478,1484 **** for (n=oldsize ; n<bddnodesize ; n++) { ! bddnodes[n].refcou = 0; bddnodes[n].hash = 0; - LEVEL(n) = 0; LOW(n) = -1; bddnodes[n].next = n+1; --- 1478,1483 ---- for (n=oldsize ; n<bddnodesize ; n++) { ! CLRLEVELREF(n); bddnodes[n].hash = 0; LOW(n) = -1; bddnodes[n].next = n+1; Index: bddio.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddio.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** bddio.c 29 Sep 2004 10:00:49 -0000 1.2 --- bddio.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 133,137 **** if (LOW(n) != -1) { ! fprintf(ofile, "[%5d - %2d] ", n, bddnodes[n].refcou); if (filehandler) filehandler(ofile, bddlevel2var[LEVEL(n)]); --- 133,137 ---- if (LOW(n) != -1) { ! fprintf(ofile, "[%5d - %2d] ", n, REF(n)); if (filehandler) filehandler(ofile, bddlevel2var[LEVEL(n)]); *************** *** 185,193 **** for (n=0 ; n<bddnodesize ; n++) { ! if (LEVEL(n) & MARKON) { node = &bddnodes[n]; ! LEVELp(node) &= MARKOFF; fprintf(ofile, "[%5d] ", n); --- 185,193 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (MARKED(n)) { node = &bddnodes[n]; ! UNMARKp(node); fprintf(ofile, "[%5d] ", n); *************** *** 441,447 **** return 0; ! if (LEVELp(node) & MARKON) return 0; ! LEVELp(node) |= MARKON; if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) --- 441,447 ---- return 0; ! if (MARKEDp(node)) return 0; ! SETMARKp(node); if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** reorder.c 29 Sep 2004 10:00:50 -0000 1.2 --- reorder.c 1 Oct 2004 02:17:20 -0000 1.3 *************** *** 53,62 **** /* Change macros to reflect the above idea */ #define VAR(n) (bddnodes[n].level) ! #define VARp(p) (p->level) /* Avoid these - they are misleading! */ #undef LEVEL #undef LEVELp --- 53,71 ---- /* Change macros to reflect the above idea */ + #if defined(USE_BITFIELDS) #define VAR(n) (bddnodes[n].level) ! #define VARp(p) ((p)->level) ! #define SETVARp(p,v) (VARp(p) = (v)) ! #else ! #define VAR(n) (bddnodes[n].refcou_and_level >> 10) ! #define VARp(p) ((p)->refcou_and_level >> 10) ! #define SETVARp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) ! #endif /* Avoid these - they are misleading! */ #undef LEVEL #undef LEVELp + #undef SETLEVEL + #undef SETLEVELp *************** *** 813,817 **** return; ! if (bddnodes[r].refcou == 0) { bddfreenum--; --- 822,826 ---- return; ! if (REF(r) == 0) { bddfreenum--; *************** *** 871,877 **** /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ bddnodes[n].level = bddlevel2var[bddnodes[n].level]; ! if (bddnodes[n].refcou > 0) { SETMARK(n); --- 880,890 ---- /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ + #if defined(USE_BITFIELDS) bddnodes[n].level = bddlevel2var[bddnodes[n].level]; + #else + bddnodes[n].refcou_and_level = (bddlevel2var[bddnodes[n].refcou_and_level >> 10] << 10) | REF(n); + #endif ! if (REF(n) > 0) { SETMARK(n); *************** *** 934,938 **** register BddNode *node = &bddnodes[n]; ! if (node->refcou > 0) { register unsigned int hash; --- 947,951 ---- register BddNode *node = &bddnodes[n]; ! if (REFp(node) > 0) { register unsigned int hash; *************** *** 995,999 **** register BddNode *node = &bddnodes[n]; ! if (node->refcou > 0) { register unsigned int hash; --- 1008,1012 ---- register BddNode *node = &bddnodes[n]; ! if (REFp(node) > 0) { register unsigned int hash; *************** *** 1093,1097 **** node = &bddnodes[res]; ! VARp(node) = var; LOWp(node) = low; HIGHp(node) = high; --- 1106,1110 ---- node = &bddnodes[res]; ! SETVARp(node, var); LOWp(node) = low; HIGHp(node) = high; *************** *** 1102,1106 **** /* Make sure it is reference counted */ ! node->refcou = 1; INCREF(LOWp(node)); INCREF(HIGHp(node)); --- 1115,1119 ---- /* Make sure it is reference counted */ ! SETREFp(node, 1); INCREF(LOWp(node)); INCREF(HIGHp(node)); *************** *** 1212,1216 **** /* Update in-place */ ! VARp(node) = var1; LOWp(node) = f0; HIGHp(node) = f1; --- 1225,1229 ---- /* Update in-place */ ! SETVARp(node, var1); LOWp(node) = f0; HIGHp(node) = f1; *************** *** 1250,1254 **** int next = node->next; ! if (node->refcou > 0) { node->next = bddnodes[hash].hash; --- 1263,1267 ---- int next = node->next; ! if (REFp(node) > 0) { node->next = bddnodes[hash].hash; *************** *** 1352,1356 **** int next = node->next; ! if (node->refcou > 0) { node->next = toBeProcessed; --- 1365,1369 ---- int next = node->next; ! if (REFp(node) > 0) { node->next = toBeProcessed; *************** *** 1437,1441 **** for (n=2 ; n<bddnodesize ; n++) { ! if (bddnodes[n].refcou > 0) { assert(LEVEL(n) < LEVEL(LOW(n))); --- 1450,1454 ---- for (n=2 ; n<bddnodesize ; n++) { ! if (REF(n) > 0) { assert(LEVEL(n) < LEVEL(LOW(n))); *************** *** 1689,1697 **** UNMARK(n); else ! bddnodes[n].refcou = 0; /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ bddnodes[n].level = bddvar2level[bddnodes[n].level]; } --- 1702,1714 ---- UNMARK(n); else ! SETREF(n, 0); /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ + #if defined(USE_BITFIELDS) bddnodes[n].level = bddvar2level[bddnodes[n].level]; + #else + bddnodes[n].refcou_and_level = (bddvar2level[bddnodes[n].refcou_and_level >> 10] << 10) | REF(n); + #endif } Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** bddop.c 30 Sep 2004 03:21:38 -0000 1.3 --- bddop.c 1 Oct 2004 02:17:20 -0000 1.4 *************** *** 774,777 **** --- 774,779 ---- return l; + _mm_prefetch(&bddnodes[l], 0); + entry = BddCache_lookup(&andcache, ANDHASH(l,r)); *************** *** 2712,2716 **** node = &bddnodes[r]; ! if (LEVELp(node) & MARKON || LOWp(node) == -1) return; --- 2714,2718 ---- node = &bddnodes[r]; ! if (MARKEDp(node) || LOWp(node) == -1) return; *************** *** 2720,2724 **** supportMax = LEVELp(node); ! LEVELp(node) |= MARKON; support_rec(LOWp(node), support); --- 2722,2726 ---- supportMax = LEVELp(node); ! SETMARKp(node); support_rec(LOWp(node), support); *************** *** 3341,3349 **** node = &bddnodes[r]; ! if (LEVELp(node) & MARKON) return; varprofile[bddlevel2var[LEVELp(node)]]++; ! LEVELp(node) |= MARKON; varprofile_rec(LOWp(node)); --- 3343,3351 ---- node = &bddnodes[r]; ! if (MARKEDp(node)) return; varprofile[bddlevel2var[LEVELp(node)]]++; ! SETMARKp(node); varprofile_rec(LOWp(node)); |
From: John W. <joe...@us...> - 2004-09-30 03:26:30
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8582 Modified Files: Makefile Log Message: Added intel compiler flags. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.29 retrieving revision 1.30 diff -C2 -d -r1.29 -r1.30 *** Makefile 30 Sep 2004 03:21:37 -0000 1.29 --- Makefile 30 Sep 2004 03:26:14 -0000 1.30 *************** *** 34,38 **** CAL_DLL_NAME = cal.dll ifeq (${CC},icl) # Intel Windows compiler ! CFLAGS = $(EXTRA_CFLAGS) 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 --- 34,38 ---- CAL_DLL_NAME = cal.dll ifeq (${CC},icl) # Intel Windows compiler ! CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_OR -DSPECIALIZE_AND /fast $(EXTRA_CFLAGS) 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 |
From: John W. <joe...@us...> - 2004-09-30 03:21:47
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7752/buddy/src Modified Files: bddop.c cache.c cache.h Log Message: Updates to buddy to improve cache architecture. Index: cache.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/cache.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** cache.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- cache.c 30 Sep 2004 03:21:38 -0000 1.2 *************** *** 43,47 **** *************************************************************************/ ! int BddCache_init(BddCache *cache, int size) { int n; --- 43,47 ---- *************************************************************************/ ! int BddCache3_init(BddCache3 *cache, int size) { int n; *************** *** 49,53 **** size = bdd_prime_gte(size); ! if ((cache->table=NEW(BddCacheData,size)) == NULL) return bdd_error(BDD_MEMORY); --- 49,53 ---- size = bdd_prime_gte(size); ! if ((cache->table=NEW(BddCacheData3,size)) == NULL) return bdd_error(BDD_MEMORY); *************** *** 59,64 **** } ! void BddCache_done(BddCache *cache) { free(cache->table); --- 59,80 ---- } + int BddCache4_init(BddCache4 *cache, int size) + { + int n; ! size = bdd_prime_gte(size); ! ! if ((cache->table=NEW(BddCacheData4,size)) == NULL) ! return bdd_error(BDD_MEMORY); ! ! for (n=0 ; n<size ; n++) ! cache->table[n].a = -1; ! cache->tablesize = size; ! ! return 0; ! } ! ! ! void BddCache3_done(BddCache3 *cache) { free(cache->table); *************** *** 68,72 **** ! int BddCache_resize(BddCache *cache, int newsize) { int n; --- 84,96 ---- ! void BddCache4_done(BddCache4 *cache) ! { ! free(cache->table); ! cache->table = NULL; ! cache->tablesize = 0; ! } ! ! ! int BddCache3_resize(BddCache3 *cache, int newsize) { int n; *************** *** 76,80 **** newsize = bdd_prime_gte(newsize); ! if ((cache->table=NEW(BddCacheData,newsize)) == NULL) return bdd_error(BDD_MEMORY); --- 100,104 ---- newsize = bdd_prime_gte(newsize); ! if ((cache->table=NEW(BddCacheData3,newsize)) == NULL) return bdd_error(BDD_MEMORY); *************** *** 86,91 **** } ! void BddCache_reset(BddCache *cache) { register int n; --- 110,140 ---- } + int BddCache4_resize(BddCache4 *cache, int newsize) + { + int n; ! free(cache->table); ! ! newsize = bdd_prime_gte(newsize); ! ! if ((cache->table=NEW(BddCacheData4,newsize)) == NULL) ! return bdd_error(BDD_MEMORY); ! ! for (n=0 ; n<newsize ; n++) ! cache->table[n].a = -1; ! cache->tablesize = newsize; ! ! return 0; ! } ! ! ! void BddCache3_reset(BddCache3 *cache) ! { ! register int n; ! for (n=0 ; n<cache->tablesize ; n++) ! cache->table[n].a = -1; ! } ! ! void BddCache4_reset(BddCache4 *cache) { register int n; Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** bddop.c 29 Sep 2004 10:00:50 -0000 1.2 --- bddop.c 30 Sep 2004 03:21:38 -0000 1.3 *************** *** 102,111 **** static int supportMax; /* Max. used level in support calc. */ static int* supportSet; /* The found support set */ ! static BddCache applycache; /* Cache for apply results */ ! static BddCache itecache; /* Cache for ITE results */ ! static BddCache quantcache; /* Cache for exist/forall results */ ! static BddCache appexcache; /* Cache for appex/appall results */ ! static BddCache replacecache; /* Cache for replace results */ ! static BddCache misccache; /* Cache for other results */ static int cacheratio; static BDD satPolarity; [...1304 lines suppressed...] --- 3390,3394 ---- entry = BddCache_lookup(&misccache, PATHCOUHASH(r)); ! if (entry->a == r && entry->b == miscid) return entry->r.dres; *************** *** 3146,3150 **** entry->a = r; ! entry->c = miscid; entry->r.dres = size; --- 3396,3400 ---- entry->a = r; ! entry->b = miscid; entry->r.dres = size; Index: cache.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/cache.h,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** cache.h 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- cache.h 30 Sep 2004 03:21:38 -0000 1.2 *************** *** 41,67 **** typedef struct { ! union ! { ! double dres; ! int res; ! } r; ! int a,b,c; ! } BddCacheData; typedef struct { ! BddCacheData *table; int tablesize; ! } BddCache; ! extern int BddCache_init(BddCache *, int); ! extern void BddCache_done(BddCache *); ! extern int BddCache_resize(BddCache *, int); ! extern void BddCache_reset(BddCache *); ! #define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize]) #endif /* _CACHE_H */ --- 41,80 ---- typedef struct { ! int a,b,res; ! } BddCacheData3; + typedef struct + { + int a,b; + union + { + struct { int c,res; }; + double dres; + } r; + } BddCacheData4; typedef struct { ! BddCacheData3 *table; int tablesize; ! } BddCache3; + typedef struct + { + BddCacheData4 *table; + int tablesize; + } BddCache4; ! extern int BddCache3_init(BddCache3 *, int); ! extern void BddCache3_done(BddCache3 *); ! extern int BddCache3_resize(BddCache3 *, int); ! extern void BddCache3_reset(BddCache3 *); ! extern int BddCache4_init(BddCache4 *, int); ! extern void BddCache4_done(BddCache4 *); ! extern int BddCache4_resize(BddCache4 *, int); ! extern void BddCache4_reset(BddCache4 *); + #define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize]) #endif /* _CACHE_H */ |
From: John W. <joe...@us...> - 2004-09-30 03:21:47
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7752 Modified Files: Makefile Log Message: Updates to buddy to improve cache architecture. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.28 retrieving revision 1.29 diff -C2 -d -r1.28 -r1.29 *** Makefile 16 Sep 2004 23:49:55 -0000 1.28 --- Makefile 30 Sep 2004 03:21:37 -0000 1.29 *************** *** 68,74 **** CAL_DLL_NAME = libcal.so ifeq (${CC},icc) # Intel Linux compiler ! CFLAGS = -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -shared -static $(EXTRA_CFLAGS) endif endif --- 68,74 ---- CAL_DLL_NAME = libcal.so ifeq (${CC},icc) # Intel Linux compiler ! CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -static -shared $(CFLAGS) endif endif |