Thread: [Javabdd-checkins] SF.net SVN: javabdd:[479] trunk/JavaBDD

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

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.




Thread: [Javabdd-checkins] SF.net SVN: javabdd:[479] trunk/JavaBDD

javabdd-checkins