[Javabdd-checkins] JavaBDD cudd_jni.c,1.12,1.13

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Update of /cvsroot/javabdd/JavaBDD
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3183

Modified Files:
	cudd_jni.c 
Log Message:
Fixed implementation of CUDD pairing.
Also added getCacheSize()

Index: cudd_jni.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/cudd_jni.c,v
retrieving revision 1.12
retrieving revision 1.13
diff -C2 -d -r1.12 -r1.13
*** cudd_jni.c	16 Oct 2004 02:58:57 -0000	1.12
--- cudd_jni.c	29 Jun 2005 08:00:44 -0000	1.13
***************
*** 60,63 ****
--- 60,70 ----
  }
  
+ typedef struct CuddPairing {
+     DdNode** table;
+     struct CuddPairing *next;
+ } CuddPairing;
+ 
+ static CuddPairing *pair_list;
+ 
  /*
   * Class:     net_sf_javabdd_CUDDFactory
***************
*** 91,94 ****
--- 98,103 ----
      Cudd_Ref((DdNode *)(intptr_cast_type) bdd_zero);
      
+     pair_list = NULL;
+     
      one_fid = (*env)->GetStaticFieldID(env, cl, "one", "J");
      zero_fid = (*env)->GetStaticFieldID(env, cl, "zero", "J");
***************
*** 124,132 ****
      DdManager* m;
  
      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));
      
      bdds = Cudd_CheckZeroRef(manager);
--- 133,153 ----
      DdManager* m;
  
+     while (pair_list) {
+         CuddPairing *p;
+         int n;
+         for (n=0 ; n<varnum ; n++) {
+             Cudd_RecursiveDeref(manager, pair_list->table[n]);
+         }
+         free(pair_list->table);
+         p = pair_list->next;
+         free(pair_list);
+         pair_list = p;
+     }
+ 
      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));
      
      bdds = Cudd_CheckZeroRef(manager);
***************
*** 134,138 ****
      m = manager;
      manager = NULL; // race condition with delRef
! 	Cudd_Quit(m);
  }
  
--- 155,159 ----
      m = manager;
      manager = NULL; // race condition with delRef
!     Cudd_Quit(m);
  }
  
***************
*** 157,160 ****
--- 178,197 ----
  {
      jint old = varnum;
+     CuddPairing *p = pair_list;
+     while (p) {
+         int n;
+         DdNode** t = (DdNode**) malloc(sizeof(DdNode*)*x);
+         if (t == NULL) return 0;
+         memcpy(t, p->table, sizeof(DdNode*)*old);
+         for (n=old ; n<x ; n++) {
+             int var = n;
+             //int var = Cudd_ReadInvPerm(manager, n); // level2var
+             t[n] = Cudd_bddIthVar(manager, var);
+             Cudd_Ref(t[n]);
+         }
+         free(p->table);
+         p->table = t;
+         p = p->next;
+     }
      varnum = varcount = x;
      return old;
***************
*** 185,190 ****
    (JNIEnv *env, jclass cl, jint level)
  {
! 	//return manager->invperm[level];
! 	return (jint) Cudd_ReadInvPerm(manager, level);
  }
  
--- 222,227 ----
    (JNIEnv *env, jclass cl, jint level)
  {
!     //return manager->invperm[level];
!     return (jint) Cudd_ReadInvPerm(manager, level);
  }
  
***************
*** 197,202 ****
    (JNIEnv *env, jclass cl, jint v)
  {
! 	//return (jint) cuddI(manager, v);
! 	return (jint) Cudd_ReadPerm(manager, v);
  }
  
--- 234,239 ----
    (JNIEnv *env, jclass cl, jint v)
  {
!     //return (jint) cuddI(manager, v);
!     return (jint) Cudd_ReadPerm(manager, v);
  }
  
***************
*** 245,248 ****
--- 282,296 ----
  }
  
+ /*
+  * Class:     net_sf_javabdd_CUDDFactory
+  * Method:    getCacheSize0
+  * Signature: ()I
+  */
+ JNIEXPORT jint JNICALL Java_net_sf_javabdd_CUDDFactory_getCacheSize0
+   (JNIEnv *env, jclass cl)
+ {
+   return Cudd_ReadCacheSlots(manager);
+ }
+ 
  /* class net_sf_javabdd_CUDDFactory_CUDDBDD */
  
***************
*** 529,542 ****
      
      if (F == zero ||
!     	F == one) {
!     	return f;
      }
!   	
      index = F->index;
      high = cuddT(F);
      low = cuddE(F);
      if (Cudd_IsComplement(f)) {
! 	high = Cudd_Not(high);
! 	low = Cudd_Not(low);
      }
      if (low == (DdNode*)(intptr_cast_type)bdd_zero) {
--- 577,590 ----
      
      if (F == zero ||
!         F == one) {
!         return f;
      }
!     
      index = F->index;
      high = cuddT(F);
      low = cuddE(F);
      if (Cudd_IsComplement(f)) {
!         high = Cudd_Not(high);
!         low = Cudd_Not(low);
      }
      if (low == (DdNode*)(intptr_cast_type)bdd_zero) {
***************
*** 544,548 ****
          if (res == NULL) {
              return NULL;
!   	}
          cuddRef(res);
          if (Cudd_IsComplement(res)) {
--- 592,596 ----
          if (res == NULL) {
              return NULL;
!         }
          cuddRef(res);
          if (Cudd_IsComplement(res)) {
***************
*** 675,685 ****
    (JNIEnv *env, jclass cl, jlong a, jlong b)
  {
! 	DdNode* d;
! 	DdNode** e;
! 	DdNode* f;
      jlong result;
      d = (DdNode*) (intptr_cast_type) a;
!     e = (DdNode**) (intptr_cast_type) b;
!     f = Cudd_bddVectorCompose(manager, d, e);
      result = (jlong) (intptr_cast_type) f;
      return result;
--- 723,733 ----
    (JNIEnv *env, jclass cl, jlong a, jlong b)
  {
!     DdNode* d;
!     CuddPairing* e;
!     DdNode* f;
      jlong result;
      d = (DdNode*) (intptr_cast_type) a;
!     e = (CuddPairing*) (intptr_cast_type) b;
!     f = Cudd_bddVectorCompose(manager, d, e->table);
      result = (jlong) (intptr_cast_type) f;
      return result;
***************
*** 694,714 ****
    (JNIEnv *env, jclass cl, jlong a, jlong b)
  {
! 	DdNode* d;
! 	DdNode** e;
! 	DdNode* f;
      jlong result;
! 	int n;
! 	int *arr;
! 	arr = (int*) malloc(sizeof(int)*varnum);
! 	if (arr == NULL) return INVALID_BDD;
      d = (DdNode*) (intptr_cast_type) a;
!     e = (DdNode**) (intptr_cast_type) b;
! 	for (n=0; n<varnum; ++n) {
! 		DdNode* node = e[n];
! 		int var = Cudd_Regular(node)->index;
! 		int level = var;
! 		//int level = Cudd_ReadPerm(manager, var);
! 		arr[n] = level;
! 	}
      f = Cudd_bddPermute(manager, d, arr);
      free(arr);
--- 742,762 ----
    (JNIEnv *env, jclass cl, jlong a, jlong b)
  {
!     DdNode* d;
!     CuddPairing* e;
!     DdNode* f;
      jlong result;
!     int n;
!     int *arr;
!     arr = (int*) malloc(sizeof(int)*varnum);
!     if (arr == NULL) return INVALID_BDD;
      d = (DdNode*) (intptr_cast_type) a;
!     e = (CuddPairing*) (intptr_cast_type) b;
!     for (n=0; n<varnum; ++n) {
!         DdNode* node = e->table[n];
!         int var = Cudd_Regular(node)->index;
!         int level = var;
!         //int level = Cudd_ReadPerm(manager, var);
!         arr[n] = level;
!     }
      f = Cudd_bddPermute(manager, d, arr);
      free(arr);
***************
*** 727,740 ****
    (JNIEnv *env, jclass cl)
  {
! 	int n;
! 	DdNode **r = (DdNode**) malloc(sizeof(DdNode*)*varnum);
! 	if (r == NULL) return 0;
! 	for (n=0 ; n<varnum ; n++) {
! 		int var = n;
! 		//int var = Cudd_ReadInvPerm(manager, n); // level2var
! 		r[n] = Cudd_bddIthVar(manager, var);
! 		Cudd_Ref(r[n]);
! 	}
! 	return (jlong) (intptr_cast_type) r;
  }
  
--- 775,795 ----
    (JNIEnv *env, jclass cl)
  {
!     int n;
!     CuddPairing* r = (CuddPairing*) malloc(sizeof(CuddPairing));
!     if (r == NULL) return 0;
!     r->table = (DdNode**) malloc(sizeof(DdNode*)*varnum);
!     if (r->table == NULL) {
!         free(r);
!         return 0;
!     }
!     for (n=0 ; n<varnum ; n++) {
!         int var = n;
!         //int var = Cudd_ReadInvPerm(manager, n); // level2var
!         r->table[n] = Cudd_bddIthVar(manager, var);
!         Cudd_Ref(r->table[n]);
!     }
!     r->next = pair_list;
!     pair_list = r;
!     return (jlong) (intptr_cast_type) r;
  }
  
***************
*** 747,757 ****
    (JNIEnv *env, jclass cl, jlong p, jint var, jint b)
  {
! 	DdNode **r = (DdNode**) (intptr_cast_type) p;
! 	int level1 = var;
! 	//int level1 = Cudd_ReadPerm(manager, var);
! 	//int level2 = Cudd_ReadPerm(manager, b);
! 	Cudd_RecursiveDeref(manager, r[level1]);
!     r[level1] = Cudd_bddIthVar(manager, b);
!     Cudd_Ref(r[level1]);
  }
  
--- 802,812 ----
    (JNIEnv *env, jclass cl, jlong p, jint var, jint b)
  {
!     CuddPairing* r = (CuddPairing*) (intptr_cast_type) p;
!     int level1 = var;
!     //int level1 = Cudd_ReadPerm(manager, var);
!     //int level2 = Cudd_ReadPerm(manager, b);
!     Cudd_RecursiveDeref(manager, r->table[level1]);
!     r->table[level1] = Cudd_bddIthVar(manager, b);
!     Cudd_Ref(r->table[level1]);
  }
  
***************
*** 764,774 ****
    (JNIEnv *env, jclass cl, jlong p, jint var, jlong b)
  {
! 	DdNode **r = (DdNode**) (intptr_cast_type) p;
! 	DdNode *d = (DdNode*) (intptr_cast_type) b;
! 	int level1 = var;
! 	//int level1 = Cudd_ReadPerm(manager, var);
! 	Cudd_RecursiveDeref(manager, r[level1]);
!     r[level1] = d;
!     Cudd_Ref(r[level1]);
  }
  
--- 819,829 ----
    (JNIEnv *env, jclass cl, jlong p, jint var, jlong b)
  {
!     CuddPairing* r = (CuddPairing*) (intptr_cast_type) p;
!     DdNode *d = (DdNode*) (intptr_cast_type) b;
!     int level1 = var;
!     //int level1 = Cudd_ReadPerm(manager, var);
!     Cudd_RecursiveDeref(manager, r->table[level1]);
!     r->table[level1] = d;
!     Cudd_Ref(r->table[level1]);
  }
  
***************
*** 781,794 ****
    (JNIEnv *env, jclass cl, jlong p)
  {
! 	int n;
! 	DdNode **r = (DdNode**) (intptr_cast_type) p;
! 	for (n=0 ; n<varnum ; n++) {
! 		int var;
! 		Cudd_RecursiveDeref(manager, r[n]);
! 		var = n;
! 		//int var = Cudd_ReadInvPerm(manager, n); // level2var
! 		r[n] = Cudd_bddIthVar(manager, var);
! 		Cudd_Ref(r[n]);
! 	}
  }
  
--- 836,849 ----
    (JNIEnv *env, jclass cl, jlong p)
  {
!     int n;
!     CuddPairing* r = (CuddPairing*) (intptr_cast_type) p;
!     for (n=0 ; n<varnum ; n++) {
!         int var;
!         Cudd_RecursiveDeref(manager, r->table[n]);
!         var = n;
!         //int var = Cudd_ReadInvPerm(manager, n); // level2var
!         r->table[n] = Cudd_bddIthVar(manager, var);
!         Cudd_Ref(r->table[n]);
!     }
  }
  
***************
*** 801,809 ****
    (JNIEnv *env, jclass cl, jlong p)
  {
! 	int n;
! 	DdNode **r = (DdNode**) (intptr_cast_type) p;
! 	for (n=0 ; n<varnum ; n++) {
! 		Cudd_RecursiveDeref(manager, r[n]);
! 	}
! 	free(r);
  }
--- 856,870 ----
    (JNIEnv *env, jclass cl, jlong p)
  {
!     int n;
!     CuddPairing* r = (CuddPairing*) (intptr_cast_type) p;
!     CuddPairing** ptr;
!     for (n=0 ; n<varnum ; n++) {
!         Cudd_RecursiveDeref(manager, r->table[n]);
!     }
!     ptr = &pair_list; 
!     while (*ptr != r)
!         ptr = &(*ptr)->next;
!     *ptr = r->next;
!     free(r->table);
!     free(r);
  }