[Javabdd-checkins] SF.net SVN: javabdd:[479] trunk/JavaBDD
Brought to you by:
joewhaley
From: <rob...@us...> - 2010-10-14 01:42:55
|
Revision: 479 http://javabdd.svn.sourceforge.net/javabdd/?rev=479&view=rev Author: robimalik Date: 2010-10-14 01:42:49 +0000 (Thu, 14 Oct 2010) Log Message: ----------- Enable variable reordering and variable groups for CUDD. Modified Paths: -------------- trunk/JavaBDD/cudd_jni.c trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java Modified: trunk/JavaBDD/cudd_jni.c =================================================================== --- trunk/JavaBDD/cudd_jni.c 2007-06-15 22:22:53 UTC (rev 478) +++ trunk/JavaBDD/cudd_jni.c 2010-10-14 01:42:49 UTC (rev 479) @@ -46,6 +46,84 @@ (*env)->DeleteLocalRef(env, cls); } + +/*************************************************************************** + * Auxiliary Methods + */ + +const char* BDDFACTORY_CLASS_NAME = "net/sf/javabdd/BDDFactory"; + +jfieldID JAVA_REORDER_NONE; +jfieldID JAVA_REORDER_RANDOM; +jfieldID JAVA_REORDER_SIFT; +jfieldID JAVA_REORDER_SIFTITE; +jfieldID JAVA_REORDER_WIN2; +jfieldID JAVA_REORDER_WIN2ITE; +jfieldID JAVA_REORDER_WIN3; +jfieldID JAVA_REORDER_WIN3ITE; + + +static jboolean isJavaReorderMethod(JNIEnv *env, jclass cls, + jfieldID id, jobject method) +{ + jobject field = (*env)->GetStaticObjectField(env, cls, id); + return (*env)->IsSameObject(env, field, method); +} + + +static Cudd_ReorderingType getCUDDReorderMethod(JNIEnv *env, + jobject javamethod) +{ + jclass cls = (*env)->FindClass(env, BDDFACTORY_CLASS_NAME); + if (isJavaReorderMethod(env, cls, JAVA_REORDER_NONE, javamethod)) { + return CUDD_REORDER_NONE; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_RANDOM, javamethod)) { + return CUDD_REORDER_RANDOM; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_SIFT, javamethod)) { + return CUDD_REORDER_SIFT; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_SIFTITE, javamethod)) { + return CUDD_REORDER_SIFT_CONVERGE; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_WIN2, javamethod)) { + return CUDD_REORDER_WINDOW2; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_WIN2ITE, javamethod)) { + return CUDD_REORDER_WINDOW2_CONV; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_WIN3, javamethod)) { + return CUDD_REORDER_WINDOW3; + } else if (isJavaReorderMethod(env, cls, JAVA_REORDER_WIN3ITE, javamethod)) { + return CUDD_REORDER_WINDOW3_CONV; + } else { + die(env, "Unknown Java reorder method!"); + return 0; + } +} + +static jfieldID getJavaReorderMethodId(JNIEnv *env, + Cudd_ReorderingType cuddmethod) +{ + switch (cuddmethod) { + case CUDD_REORDER_NONE: + return JAVA_REORDER_NONE; + case CUDD_REORDER_RANDOM: + return JAVA_REORDER_RANDOM; + case CUDD_REORDER_SIFT: + return JAVA_REORDER_SIFT; + case CUDD_REORDER_SIFT_CONVERGE: + return JAVA_REORDER_SIFTITE; + case CUDD_REORDER_WINDOW2: + return JAVA_REORDER_WIN2; + case CUDD_REORDER_WINDOW2_CONV: + return JAVA_REORDER_WIN2ITE; + case CUDD_REORDER_WINDOW3: + return JAVA_REORDER_WIN3; + case CUDD_REORDER_WINDOW3_CONV: + return JAVA_REORDER_WIN3ITE; + default: + die(env, "Unknown reorder method in CUDD!"); + return 0; + } +} + + /**** START OF NATIVE METHOD IMPLEMENTATIONS ****/ /* @@ -56,6 +134,24 @@ JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_registerNatives (JNIEnv *env, jclass cl) { + jclass cls = (*env)->FindClass(env, BDDFACTORY_CLASS_NAME); + const char* type = "Lnet/sf/javabdd/BDDFactory$ReorderMethod;"; + JAVA_REORDER_NONE = + (*env)->GetStaticFieldID(env, cls, "REORDER_NONE", type); + JAVA_REORDER_RANDOM = + (*env)->GetStaticFieldID(env, cls, "REORDER_RANDOM", type);; + JAVA_REORDER_SIFT = + (*env)->GetStaticFieldID(env, cls, "REORDER_SIFT", type); + JAVA_REORDER_SIFTITE = + (*env)->GetStaticFieldID(env, cls, "REORDER_SIFTITE", type); + JAVA_REORDER_WIN2 = + (*env)->GetStaticFieldID(env, cls, "REORDER_WIN2", type); + JAVA_REORDER_WIN2ITE = + (*env)->GetStaticFieldID(env, cls, "REORDER_WIN2ITE", type); + JAVA_REORDER_WIN3 = + (*env)->GetStaticFieldID(env, cls, "REORDER_WIN3", type); + JAVA_REORDER_WIN3ITE = + (*env)->GetStaticFieldID(env, cls, "REORDER_WIN3ITE", type); } typedef struct CuddPairing { @@ -146,12 +242,15 @@ Cudd_Deref((DdNode *)(intptr_cast_type) bdd_one); Cudd_Deref((DdNode *)(intptr_cast_type) bdd_zero); - + /* fprintf(stderr, "Garbage collections: %d Time spent: %ldms\n", - Cudd_ReadGarbageCollections(manager), Cudd_ReadGarbageCollectionTime(manager)); - + Cudd_ReadGarbageCollections(manager), + Cudd_ReadGarbageCollectionTime(manager)); bdds = Cudd_CheckZeroRef(manager); - if (bdds > 0) fprintf(stderr, "Note: %d BDDs still in memory when terminating\n", bdds); + if (bdds > 0) + fprintf(stderr, "Note: %d BDDs still in memory when terminating\n", + bdds); + */ m = manager; manager = NULL; // race condition with delRef Cudd_Quit(m); @@ -248,6 +347,34 @@ /* * Class: net_sf_javabdd_CUDDFactory + * Method: reorder0 + * Signature: (Lnet/sf/javabdd/BDDFactory/ReorderMethod;)V + */ +JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_reorder0 + (JNIEnv *env, jclass cl, jobject javamethod) +{ + Cudd_ReorderingType cuddmethod = getCUDDReorderMethod(env, javamethod); + if (!(*env)->ExceptionOccurred(env)) { + Cudd_ReduceHeap(manager, cuddmethod, INT_MAX); + } +} + +/* + * Class: net_sf_javabdd_CUDDFactory + * Method: autoreorder0 + * Signature: (Lnet/sf/javabdd/BDDFactory/ReorderMethod;)V + */ +JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_autoreorder0 + (JNIEnv *env, jclass cl, jobject javamethod) +{ + Cudd_ReorderingType cuddmethod = getCUDDReorderMethod(env, javamethod); + if (!(*env)->ExceptionOccurred(env)) { + Cudd_AutodynEnable(manager, cuddmethod); + } +} + +/* + * Class: net_sf_javabdd_CUDDFactory * Method: setVarOrder0 * Signature: ([I)V */ @@ -271,6 +398,35 @@ /* * Class: net_sf_javabdd_CUDDFactory + * Method: addVarBlock0 + * Signature: (IIZ)V + */ +JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_addVarBlock0 + (JNIEnv *env, jclass cl, jint first, jint last, jboolean fixed) +{ + int firstp = Cudd_ReadPerm(manager, first); + int lastp = Cudd_ReadPerm(manager, last); + if (firstp <= lastp) { + int len = lastp - firstp + 1; + Cudd_MakeTreeNode(manager, first, len, fixed ? MTR_FIXED : MTR_DEFAULT); + } else { + die(env, "Bad indexes in variable block!"); + } +} + +/* + * Class: net_sf_javabdd_CUDDFactory + * Method: clearVarBlocks0 + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_net_sf_javabdd_CUDDFactory_clearVarBlocks0 + (JNIEnv *env, jclass cl) +{ + Cudd_FreeTree(manager); +} + +/* + * Class: net_sf_javabdd_CUDDFactory * Method: getAllocNum0 * Signature: ()I */ Modified: trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2007-06-15 22:22:53 UTC (rev 478) +++ trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2010-10-14 01:42:49 UTC (rev 479) @@ -1,6 +1,9 @@ +//# -*- tab-width: 4 indent-tabs-mode: nil c-basic-offset: 4 -*- + // CUDDFactory.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 net.sf.javabdd; import java.util.Collection; @@ -277,57 +280,55 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod) */ - public void reorder(ReorderMethod m) { - // TODO Implement this. - throw new UnsupportedOperationException(); + public void reorder(final ReorderMethod method) + { + reorder0(method); } + private static native void reorder0(ReorderMethod method); /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod) */ - public void autoReorder(ReorderMethod method) { - // TODO Implement this. - throw new UnsupportedOperationException(); + public void autoReorder(final ReorderMethod method) + { + mAutoReorderMethod = method; + autoreorder0(method); } + private static native void autoreorder0(ReorderMethod method); /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int) */ public void autoReorder(ReorderMethod method, int max) { - // TODO Implement this. - throw new UnsupportedOperationException(); + autoReorder(method); } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#getReorderMethod() */ public ReorderMethod getReorderMethod() { - // TODO Implement this. - throw new UnsupportedOperationException(); + return mAutoReorderMethod; } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#getReorderTimes() */ public int getReorderTimes() { - // TODO Implement this. - throw new UnsupportedOperationException(); + return Integer.MAX_VALUE; } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#disableReorder() */ public void disableReorder() { - // TODO Implement this. - System.err.println("Warning: disableReorder() not yet implemented"); + autoReorder(BDDFactory.REORDER_NONE); } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#enableReorder() */ public void enableReorder() { - // TODO Implement this. - System.err.println("Warning: enableReorder() not yet implemented"); + autoReorder(mAutoReorderMethod); } /* (non-Javadoc) @@ -349,34 +350,56 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean) */ - public void addVarBlock(BDD var, boolean fixed) { - // TODO Implement this. - throw new UnsupportedOperationException(); + public void addVarBlock(BDD vars, final boolean fixed) + { + if (vars.isZero()) { + return; + } else if (vars.isOne()) { + throw new IllegalArgumentException + ("Bad cube in CUDDFactory.addVarBlock()!"); + } else { + final int first = vars.var(); + int last; + do { + last = vars.var(); + vars = vars.high(); + if (vars.isZero()) { + throw new IllegalArgumentException + ("Bad cube in CUDDFactory.addVarBlock()!"); + } + } while (!vars.isOne()); + addVarBlock(first, last, fixed); + } } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean) */ - public void addVarBlock(int first, int last, boolean fixed) { - // TODO Implement this. - throw new UnsupportedOperationException(); + public void addVarBlock + (final int first, final int last, final boolean fixed) + { + addVarBlock0(first, last, fixed); } + private static native void addVarBlock0 + (int first, int last, boolean fixed); /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#varBlockAll() */ public void varBlockAll() { - // TODO Implement this. - throw new UnsupportedOperationException(); + final int varnum = varNum(); + for (int i = 0; i < varnum; i++) { + addVarBlock(i, i, false); + } } /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#clearVarBlocks() */ public void clearVarBlocks() { - // TODO Implement this. - throw new UnsupportedOperationException(); + clearVarBlocks0(); } + private static native void clearVarBlocks0(); /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#printOrder() @@ -954,5 +977,9 @@ public String getVersion() { return "CUDD "+REVISION.substring(11, REVISION.length()-2); } - + + + private static BDDFactory.ReorderMethod mAutoReorderMethod = + BDDFactory.REORDER_NONE; + } This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |