javabdd-checkins Mailing List for JavaBDD (Page 6)
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins — CVS updates. High traffic.
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...> - 2005-02-04 11:07:13
|
Update of /cvsroot/javabdd/JavaBDD/xdocs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25884/xdocs Modified Files: links.xml Log Message: Added links to projects using JavaBDD. Index: links.xml =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/xdocs/links.xml,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** links.xml 20 Jan 2005 07:50:25 -0000 1.1 --- links.xml 4 Feb 2005 11:06:59 -0000 1.2 *************** *** 25,28 **** --- 25,43 ---- </ul> </section> + <section name="Projects using JavaBDD"> + <ul> + <li> + <a href="http://bddbddb.sourceforge.net/">bddbddb</a>, BDD-Based Deductive DataBase. + </li> + <li> + <a href="http://joeq.sourceforge.net">Joeq</a> virtual machine and compiler infrastructure. + </li> + <li> + <a href="http://www.sable.mcgill.ca/jedd/">Jedd</a>, a Java language extension adding BDDs as a primitive data type. + </li> + <li> + <a href="http://staff.aist.go.jp/tanabe.yoshinori/04/09/4D-2.pdf">Checking Satisfiability of Guarded Fragments</a>. + </li> + </ul> <section name="Related Links"> <ul> |
|
From: John W. <joe...@us...> - 2005-02-03 02:12:43
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6975/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Added hashCode() methods. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** MicroFactory.java 31 Jan 2005 12:04:45 -0000 1.5 --- MicroFactory.java 3 Feb 2005 02:12:27 -0000 1.6 *************** *** 718,721 **** --- 718,722 ---- return false; } + public int hashCode() { return a ^ b; } } *************** *** 731,734 **** --- 732,736 ---- return false; } + public int hashCode() { return a ^ b ^ c; } } |
|
From: John W. <joe...@us...> - 2005-02-02 08:03:45
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25223 Modified Files: Makefile Log Message: Automatically find JDK 1.5, as well as 1.4. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.39 retrieving revision 1.40 diff -C2 -d -r1.39 -r1.40 *** Makefile 29 Jan 2005 11:38:03 -0000 1.39 --- Makefile 2 Feb 2005 08:03:35 -0000 1.40 *************** *** 50,54 **** endif else ! JDK_ROOT = $(firstword $(wildcard /usr/java/j2sdk*)) CLASSPATH = .:jdd.jar CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -O2 -fomit-frame-pointer $(EXTRA_CFLAGS) --- 50,54 ---- endif else ! JDK_ROOT = $(firstword $(wildcard /usr/java/j*dk*)) CLASSPATH = .:jdd.jar CFLAGS = -DSPECIALIZE_RELPROD -DSPECIALIZE_AND -DSPECIALIZE_OR -O2 -fomit-frame-pointer $(EXTRA_CFLAGS) |
|
From: John W. <joe...@us...> - 2005-01-31 12:18:02
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv19095 Modified Files: buddy_jni.c Log Message: A little more robust. Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.27 retrieving revision 1.28 diff -C2 -d -r1.27 -r1.28 *** buddy_jni.c 31 Jan 2005 12:15:16 -0000 1.27 --- buddy_jni.c 31 Jan 2005 12:17:46 -0000 1.28 *************** *** 150,158 **** fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "time", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->time / (CLOCKS_PER_SEC/1000)); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "sumtime", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->sumtime / (CLOCKS_PER_SEC/1000)); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "num", "I"); --- 150,164 ---- fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "time", "J"); if (fid) { ! long t = s->time; ! if (CLOCKS_PER_SEC < 1000) t = t * 1000 / CLOCKS_PER_SEC; ! else t /= (CLOCKS_PER_SEC/1000); ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "sumtime", "J"); if (fid) { ! long t = s->sumtime; ! if (CLOCKS_PER_SEC < 1000) t = t * 1000 / CLOCKS_PER_SEC; ! else t /= (CLOCKS_PER_SEC/1000); ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, t); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "num", "I"); |
|
From: John W. <joe...@us...> - 2005-01-31 12:15:26
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv18698 Modified Files: buddy_jni.c Log Message: Scale time by clocks_per_sec Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.26 retrieving revision 1.27 diff -C2 -d -r1.26 -r1.27 *** buddy_jni.c 31 Jan 2005 10:09:15 -0000 1.26 --- buddy_jni.c 31 Jan 2005 12:15:16 -0000 1.27 *************** *** 3,6 **** --- 3,7 ---- #include <fdd.h> #include <stdlib.h> + #include <time.h> #include "buddy_jni.h" *************** *** 149,157 **** fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "time", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->time); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "sumtime", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->sumtime); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "num", "I"); --- 150,158 ---- fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "time", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->time / (CLOCKS_PER_SEC/1000)); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "sumtime", "J"); if (fid) { ! (*jnienv)->SetLongField(jnienv, gc_obj, fid, s->sumtime / (CLOCKS_PER_SEC/1000)); } fid = (*jnienv)->GetFieldID(jnienv, gc_cls, "num", "I"); |
|
From: John W. <joe...@us...> - 2005-01-31 12:04:54
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16618/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Fix typo in appuni() Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** MicroFactory.java 31 Jan 2005 10:34:18 -0000 1.4 --- MicroFactory.java 31 Jan 2005 12:04:45 -0000 1.5 *************** *** 2136,2142 **** } ! if (ISCONST(l) && ISCONST(r)) res = oprres[appexop][(l << 1) | r]; ! else if (ISCONST(var)) { int oldop = applyop; applyop = appexop; --- 2136,2143 ---- } ! if (ISCONST(l) && ISCONST(r)) { res = oprres[appexop][(l << 1) | r]; ! return res; ! } else if (ISCONST(var)) { int oldop = applyop; applyop = appexop; |
|
From: John W. <joe...@us...> - 2005-01-31 12:04:25
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16538/buddy/src Modified Files: reorder.c Log Message: Fix stupid bug. Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** reorder.c 31 Jan 2005 10:04:59 -0000 1.7 --- reorder.c 31 Jan 2005 12:04:16 -0000 1.8 *************** *** 59,64 **** (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) #define SETVARp(p,v) { \ ! (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & ~NODE_MASK); \ ! (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & ~NODE_MASK); \ } #else --- 59,64 ---- (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) #define SETVARp(p,v) { \ ! (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & NODE_MASK); \ ! (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & NODE_MASK); \ } #else *************** *** 894,898 **** SETVARp(&bddnodes[n], v); ! if (REF(n) > 0) { SETMARK(n); --- 894,898 ---- SETVARp(&bddnodes[n], v); ! if (HASREF(n)) { SETMARK(n); *************** *** 1117,1121 **** SETLOWp(node, low); SETHIGHp(node, high); ! /* Insert node in hash chain */ SETNEXTp(node, HASH(hash)); --- 1117,1121 ---- SETLOWp(node, low); SETHIGHp(node, high); ! /* Insert node in hash chain */ SETNEXTp(node, HASH(hash)); |
|
From: John W. <joe...@us...> - 2005-01-31 12:03:44
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16409/buddy/src Modified Files: bddop.c Log Message: Added correct support for unique() and appuni(). Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.9 retrieving revision 1.10 diff -C2 -d -r1.9 -r1.10 *** bddop.c 31 Jan 2005 10:02:43 -0000 1.9 --- bddop.c 31 Jan 2005 12:03:34 -0000 1.10 *************** *** 134,139 **** --- 134,141 ---- static int simplify_rec(BDD, BDD); static int quant_rec(int); + static int unique_rec(int, int); static int appquant_rec(int, int); static int appquant_rec0(int, int); + static int appuni_rec(int, int, int); static int restrict_rec(int); static BDD constrain_rec(BDD, BDD); *************** *** 2158,2164 **** if (setjmp(bddexception) == 0) { - if (varset2vartable(var) < 0) - RETURN_BDD(bddfalse); - INITREF; quantid = (var << 3) | CACHEID_UNIQUE; --- 2160,2163 ---- *************** *** 2167,2171 **** if (!firstReorder) bdd_disable_reorder(); ! res = quant_rec(r); if (!firstReorder) bdd_enable_reorder(); --- 2166,2170 ---- if (!firstReorder) bdd_disable_reorder(); ! res = unique_rec(r, var); if (!firstReorder) bdd_enable_reorder(); *************** *** 2223,2226 **** --- 2222,2267 ---- } + static int unique_rec(int r, int q) { + BddCacheData3 *entry; + int res; + int LEVEL_r, LEVEL_q; + + LEVEL_r = LEVEL(r); + LEVEL_q = LEVEL(q); + if (LEVEL_r > LEVEL_q) { + // Skipped a quantified node, answer is zero. + return BDDZERO; + } + + if (r < 2 || q < 2) + return r; + + entry = BddCache_lookup(&quantcache, QUANTHASH(r)); + if (entry->a == r && entry->b == quantid) { + #ifdef CACHESTATS + bddcachestats.opHit++; + #endif + return entry->res; + } + #ifdef CACHESTATS + bddcachestats.opMiss++; + #endif + if (LEVEL_r == LEVEL_q) { + PUSHREF(unique_rec(LOW(r), HIGH(q))); + PUSHREF(unique_rec(HIGH(r), HIGH(q))); + res = apply_rec(READREF(2), READREF(1)); + } else { + PUSHREF(unique_rec(LOW(r), q)); + PUSHREF(unique_rec(HIGH(r), q)); + res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } + POPREF(2); + + entry->a = r; + entry->b = quantid; + entry->res = res; + return res; + } + /*=== APPLY & QUANTIFY =================================================*/ *************** *** 2422,2432 **** if (quantcache.table == NULL && BddCache3_init(&quantcache,cachesize) < 0) return bdd_error(BDD_MEMORY); again: if (setjmp(bddexception) == 0) { - if (varset2vartable(var) < 0) - RETURN_BDD(bddfalse); - INITREF; applyop = bddop_xor; --- 2463,2472 ---- if (quantcache.table == NULL && BddCache3_init(&quantcache,cachesize) < 0) return bdd_error(BDD_MEMORY); + if (appexcache.table == NULL && BddCache4_init(&appexcache,cachesize) < 0) + return bdd_error(BDD_MEMORY); again: if (setjmp(bddexception) == 0) { INITREF; applyop = bddop_xor; *************** *** 2437,2441 **** if (!firstReorder) bdd_disable_reorder(); ! res = appquant_rec(l, r); if (!firstReorder) bdd_enable_reorder(); --- 2477,2481 ---- if (!firstReorder) bdd_disable_reorder(); ! res = appuni_rec(l, r, var); if (!firstReorder) bdd_enable_reorder(); *************** *** 2588,2591 **** --- 2628,2712 ---- } + static int appuni_rec(int l, int r, int var) { + BddCacheData4 *entry; + int res; + + int LEVEL_l, LEVEL_r, LEVEL_var; + LEVEL_l = LEVEL(l); + LEVEL_r = LEVEL(r); + LEVEL_var = LEVEL(var); + + if (LEVEL_l > LEVEL_var && LEVEL_r > LEVEL_var) { + // Skipped a quantified node, answer is zero. + return BDDZERO; + } + + if (ISCONST(l) && ISCONST(r)) + res = oprres[appexop][(l << 1) | r]; + else if (ISCONST(var)) { + int oldop = applyop; + applyop = appexop; + res = apply_rec(l, r); + applyop = oldop; + } else { + int lev; + entry = BddCache_lookup(&appexcache, APPEXHASH(l,r,appexop)); + if (entry->a == l && entry->b == r && entry->r.c == appexid) { + #ifdef CACHESTATS + bddcachestats.opHit++; + #endif + return entry->r.res; + } + #ifdef CACHESTATS + bddcachestats.opMiss++; + #endif + + if (LEVEL_l == LEVEL_r) { + if (LEVEL_l == LEVEL_var) { + lev = -1; + var = HIGH(var); + } else { + lev = LEVEL_l; + } + PUSHREF(appuni_rec(LOW(l), LOW(r), var)); + PUSHREF(appuni_rec(HIGH(l), HIGH(r), var)); + lev = LEVEL_l; + } else if (LEVEL_l < LEVEL_r) { + if (LEVEL_l == LEVEL_var) { + lev = -1; + var = HIGH(var); + } else { + lev = LEVEL_l; + } + PUSHREF(appuni_rec(LOW(l), r, var)); + PUSHREF(appuni_rec(HIGH(l), r, var)); + } else { + if (LEVEL_r == LEVEL_var) { + lev = -1; + var = HIGH(var); + } else { + lev = LEVEL_r; + } + PUSHREF(appuni_rec(l, LOW(r), var)); + PUSHREF(appuni_rec(l, HIGH(r), var)); + } + if (lev == -1) { + int r2 = READREF(2), r1 = READREF(1); + res = apply_rec(r2, r1); + } else { + res = bdd_makenode(lev, READREF(2), READREF(1)); + } + + POPREF(2); + + entry->a = l; + entry->b = r; + entry->r.c = appexid; + entry->r.res = res; + } + + return res; + } + #if defined(SPECIALIZE_RELPROD) /* Special version of appex for common case of relprod. */ |
|
From: John W. <joe...@us...> - 2005-01-31 10:34:37
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30282/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Optimized makenode search and DECREF() macro. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** MicroFactory.java 31 Jan 2005 10:08:35 -0000 1.3 --- MicroFactory.java 31 Jan 2005 10:34:18 -0000 1.4 *************** *** 154,166 **** private final void DECREF(int node) { int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK; ! if (a == 0 || a == REF_LMASK) { ! if (REF_HMASK == 0) return; ! int b = bddnodes[node*__node_size + offset__href] & REF_HMASK; ! if (a == 0) { ! if (b == 0) return; ! bddnodes[node*__node_size + offset__href] -= REF_HINC; ! } else if (b == REF_HMASK) return; } - bddnodes[node*__node_size + offset__lref] -= REF_LINC; } --- 154,163 ---- private final void DECREF(int node) { int a = bddnodes[node*__node_size + offset__lref] & REF_LMASK; ! if (a != REF_LMASK || ! (REF_HMASK != 0 && ! (bddnodes[node*__node_size + offset__href] & REF_HMASK) != REF_HMASK)) { ! if (REF_HMASK != 0 && a == 0) bddnodes[node*__node_size + offset__href] -= REF_HINC; ! bddnodes[node*__node_size + offset__lref] -= REF_LINC; } } *************** *** 3290,3300 **** res = HASH(hash2); ! while (res != 0) { ! if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) { ! if (CACHESTATS > 0) cachestats.uniqueHit++; ! return res; ! } ! res = NEXT(res); ! if (CACHESTATS > 0) cachestats.uniqueChain++; } --- 3287,3302 ---- res = HASH(hash2); ! if (res != 0) { ! int m1 = (level << LEV_LPOS) | low; ! int m2 = ((level << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | high; ! do { ! if (bddnodes[res*__node_size + offset__low] == m1 && ! bddnodes[res*__node_size + offset__high] == m2) { ! if (CACHESTATS > 0) cachestats.uniqueHit++; ! return res; ! } ! res = NEXT(res); ! if (CACHESTATS > 0) cachestats.uniqueChain++; ! } while (res != 0); } |
|
From: John W. <joe...@us...> - 2005-01-31 10:23:54
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv27783/buddy/src Modified Files: kernel.c Log Message: Special optimization in makenode search when using small nodes. Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** kernel.c 31 Jan 2005 10:03:20 -0000 1.6 --- kernel.c 31 Jan 2005 10:23:39 -0000 1.7 *************** *** 1366,1369 **** --- 1366,1387 ---- res = HASH(hash); + #if defined(SMALL_NODES) + if (res != 0) { + int m1 = (level << LEV_LPOS) | low; + int m2 = ((level << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | high; + do { + if (bddnodes[res].low_llev == m1 && bddnodes[res].high_hlev == m2) { + #ifdef CACHESTATS + bddcachestats.uniqueHit++; + #endif + return res; + } + res = NEXT(res); + #ifdef CACHESTATS + bddcachestats.uniqueChain++; + #endif + } while (res != 0); + } + #else // SMALL_NODES while(res != 0) { *************** *** 1381,1384 **** --- 1399,1403 ---- #endif } + #endif // SMALL_NODES /* No existing node -> build one */ |
|
From: John W. <joe...@us...> - 2005-01-31 10:09:24
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24377 Modified Files: buddy_jni.c Log Message: Added getVersion0() Index: buddy_jni.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy_jni.c,v retrieving revision 1.25 retrieving revision 1.26 diff -C2 -d -r1.25 -r1.26 *** buddy_jni.c 29 Jan 2005 11:37:22 -0000 1.25 --- buddy_jni.c 31 Jan 2005 10:09:15 -0000 1.26 *************** *** 1048,1051 **** --- 1048,1071 ---- /* + * Class: net_sf_javabdd_BuDDyFactory + * Method: getVersion0 + * Signature: ()Ljava/lang/String; + */ + JNIEXPORT jstring JNICALL Java_net_sf_javabdd_BuDDyFactory_getVersion0 + (JNIEnv *env, jclass c) + { + char *buf; + jstring result; + jnienv = env; + #if defined(TRACE_BUDDYLIB) + printf("bdd_versionstr()\n"); + #endif + buf = bdd_versionstr(); + result = (*env)->NewStringUTF(env, buf); + check_error(env); + return result; + } + + /* * Class: net_sf_javabdd_BuDDyFactory_BuDDyBDD * Method: var0 *************** *** 1862,1863 **** --- 1882,1884 ---- } } + |
|
From: John W. <joe...@us...> - 2005-01-31 10:09:11
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24209/net/sf/javabdd Modified Files: JFactory.java Log Message: Small cleanups here and there. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** JFactory.java 31 Jan 2005 00:05:17 -0000 1.13 --- JFactory.java 31 Jan 2005 10:08:59 -0000 1.14 *************** *** 72,77 **** int _index; - static final int INVALID_BDD = -1; - bdd(int index) { this._index = index; --- 72,75 ---- *************** *** 442,445 **** --- 440,445 ---- static final int MARK_MASK = 0x00200000; static final int LEV_MASK = 0x001FFFFF; + static final int MAXVAR = LEV_MASK; + static final int INVALID_BDD = -1; static final int REF_INC = 0x00400000; *************** *** 703,707 **** "Division by zero" }; - static final int MAXVAR = 0x1FFFFF; static final int DEFAULTMAXNODEINC = 50000; --- 703,706 ---- *************** *** 779,783 **** else if (r < 0 || r >= bddnodesize) bdd_error(BDD_ILLBDD); ! else if (r >= 2 && LOW(r) == -1) bdd_error(BDD_ILLBDD); } --- 778,782 ---- else if (r < 0 || r >= bddnodesize) bdd_error(BDD_ILLBDD); ! else if (r >= 2 && LOW(r) == INVALID_BDD) bdd_error(BDD_ILLBDD); } *************** *** 2377,2381 **** return; ! if (MARKED(r) || LOW(r) == -1) return; --- 2376,2380 ---- return; ! if (MARKED(r) || LOW(r) == INVALID_BDD) return; *************** *** 2645,2649 **** for (n = bddnodesize - 1; n >= 2; n--) { ! if (LOW(n) != -1) { int hash2; --- 2644,2648 ---- for (n = bddnodesize - 1; n >= 2; n--) { ! if (LOW(n) != INVALID_BDD) { int hash2; *************** *** 2897,2901 **** for (n = bddnodesize - 1; n >= 2; n--) { ! if (MARKED(n) && LOW(n) != -1) { int hash2; --- 2896,2900 ---- for (n = bddnodesize - 1; n >= 2; n--) { ! if (MARKED(n) && LOW(n) != INVALID_BDD) { int hash2; *************** *** 2905,2909 **** SETHASH(hash2, n); } else { ! SETLOW(n, -1); SETNEXT(n, bddfreepos); bddfreepos = n; --- 2904,2908 ---- SETHASH(hash2, n); } else { ! SETLOW(n, INVALID_BDD); SETNEXT(n, bddfreepos); bddfreepos = n; *************** *** 2936,2940 **** int bdd_addref(int root) { ! if (root == -1) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) --- 2935,2939 ---- int bdd_addref(int root) { ! if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) *************** *** 2942,2946 **** if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == -1) return bdd_error(BDD_ILLBDD); --- 2941,2945 ---- if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == INVALID_BDD) return bdd_error(BDD_ILLBDD); *************** *** 2951,2955 **** int bdd_delref(int root) { ! if (root == -1) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) --- 2950,2954 ---- int bdd_delref(int root) { ! if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) *************** *** 2957,2961 **** if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == -1) return bdd_error(BDD_ILLBDD); --- 2956,2960 ---- if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == INVALID_BDD) return bdd_error(BDD_ILLBDD); *************** *** 2974,2978 **** return; ! if (MARKED(i) || LOW(i) == -1) return; --- 2973,2977 ---- return; ! if (MARKED(i) || LOW(i) == INVALID_BDD) return; *************** *** 2983,3003 **** } - void bdd_mark_upto(int i, int level) { - - if (i < 2) - return; - - if (MARKED(i) || LOW(i) == -1) - return; - - if (LEVEL(i) > level) - return; - - SETMARK(i); - - bdd_mark_upto(LOW(i), level); - bdd_mark_upto(LOW(i), level); - } - void bdd_markcount(int i, int[] cou) { --- 2982,2985 ---- *************** *** 3005,3009 **** return; ! if (MARKED(i) || LOW(i) == -1) return; --- 2987,2991 ---- return; ! if (MARKED(i) || LOW(i) == INVALID_BDD) return; *************** *** 3020,3024 **** return; ! if (!MARKED(i) || LOW(i) == -1) return; UNMARK(i); --- 3002,3006 ---- return; ! if (!MARKED(i) || LOW(i) == INVALID_BDD) return; UNMARK(i); *************** *** 3028,3048 **** } - void bdd_unmark_upto(int i, int level2) { - - if (i < 2) - return; - - if (!MARKED(i)) - return; - - UNMARK(i); - - if (LEVEL(i) > level2) - return; - - bdd_unmark_upto(LOW(i), level2); - bdd_unmark_upto(HIGH(i), level2); - } - public static final boolean CACHESTATS = false; --- 3010,3013 ---- *************** *** 3181,3185 **** for (n = oldsize; n < bddnodesize; n++) { ! SETLOW(n, -1); //SETREFCOU(n, 0); //SETHASH(n, 0); --- 3146,3150 ---- for (n = oldsize; n < bddnodesize; n++) { ! SETLOW(n, INVALID_BDD); //SETREFCOU(n, 0); //SETHASH(n, 0); *************** *** 3215,3219 **** for (n = 0; n < bddnodesize; n++) { ! SETLOW(n, -1); //SETREFCOU(n, 0); //SETHASH(n, 0); --- 3180,3184 ---- for (n = 0; n < bddnodesize; n++) { ! SETLOW(n, INVALID_BDD); //SETREFCOU(n, 0); //SETHASH(n, 0); *************** *** 3510,3514 **** for (n = 0; n < cache.tablesize; n++) { int a = cache.table[n].a; ! if (a >= 0 && LOW(a) == -1) { cache.table[n].a = -1; } --- 3475,3479 ---- for (n = 0; n < cache.tablesize; n++) { int a = cache.table[n].a; ! if (a >= 0 && LOW(a) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3522,3527 **** int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == -1 || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3487,3492 ---- int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == INVALID_BDD || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3535,3541 **** int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == -1 || ! (cache.table[n].b != 0 && LOW(cache.table[n].b) == -1) || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3500,3506 ---- int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == INVALID_BDD || ! (cache.table[n].b != 0 && LOW(cache.table[n].b) == INVALID_BDD) || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3550,3556 **** if (a < 0) continue; if (LOW(a) == -1 || ! LOW(cache.table[n].b) == -1 || ! LOW(cache.table[n].c) == -1 || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3515,3521 ---- if (a < 0) continue; if (LOW(a) == -1 || ! LOW(cache.table[n].b) == INVALID_BDD || ! LOW(cache.table[n].c) == INVALID_BDD || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 5093,5097 **** DECREF(HIGH(r)); ! SETLOW(r, -1); SETNEXT(r, bddfreepos); bddfreepos = r; --- 5058,5062 ---- DECREF(HIGH(r)); ! SETLOW(r, INVALID_BDD); SETNEXT(r, bddfreepos); bddfreepos = r; *************** *** 5220,5224 **** DECREF(HIGH(r)); ! SETLOW(r, -1); SETNEXT(r, bddfreepos); bddfreepos = r; --- 5185,5189 ---- DECREF(HIGH(r)); ! SETLOW(r, INVALID_BDD); SETNEXT(r, bddfreepos); bddfreepos = r; *************** *** 5547,5551 **** } else { ! SETLOW(n, -1); SETNEXT(n, bddfreepos); bddfreepos = n; --- 5512,5516 ---- } else { ! SETLOW(n, INVALID_BDD); SETNEXT(n, bddfreepos); bddfreepos = n; *************** *** 5750,5754 **** for (n = 0; n < bddnodesize; n++) { ! if (LOW(n) != -1) { out.print( "[" --- 5715,5719 ---- for (n = 0; n < bddnodesize; n++) { ! if (LOW(n) != INVALID_BDD) { out.print( "[" |
|
From: John W. <joe...@us...> - 2005-01-31 10:08:46
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24130/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Added support for finding compulsory misses in cache. Standardized naming so we can move code between here and JFactory. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** MicroFactory.java 31 Jan 2005 00:07:11 -0000 1.2 --- MicroFactory.java 31 Jan 2005 10:08:35 -0000 1.3 *************** *** 7,14 **** --- 7,16 ---- import java.util.Collection; import java.util.Comparator; + import java.util.HashSet; import java.util.Iterator; import java.util.LinkedList; import java.util.List; import java.util.Random; + import java.util.Set; import java.io.BufferedReader; [...1833 lines suppressed...] + if (itecache != null) { + System.out.println("ITE cache: "+itecache); + cachestats.opHit += itecache.cacheHit; + cachestats.opMiss += itecache.cacheMiss; + } + if (countcache != null) { + System.out.println("Count cache: "+countcache); + cachestats.opHit += countcache.cacheHit; + cachestats.opMiss += countcache.cacheMiss; + } + if (misccache != null) { + System.out.println("Misc cache: "+misccache); + cachestats.opHit += misccache.cacheHit; + cachestats.opMiss += misccache.cacheMiss; + } + return cachestats; + } + public static final String REVISION = "$Revision$"; |
|
From: John W. <joe...@us...> - 2005-01-31 10:05:10
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23333/buddy/src Modified Files: kernel.h reorder.c Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** kernel.h 1 Oct 2004 02:17:20 -0000 1.3 --- kernel.h 31 Jan 2005 10:04:59 -0000 1.4 *************** *** 57,61 **** if (!bddrunning) return bdd_error(BDD_RUNNING);\ else if ((r) < 0 || (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\ ! else if (r >= 2 && LOW(r) == -1) return bdd_error(BDD_ILLBDD)\ /* Sanity check argument and return eventually the argument 'a' */ --- 57,61 ---- if (!bddrunning) return bdd_error(BDD_RUNNING);\ else if ((r) < 0 || (r) >= bddnodesize) return bdd_error(BDD_ILLBDD);\ ! else if (r >= 2 && LOW(r) == INVALID_BDD) return bdd_error(BDD_ILLBDD)\ /* Sanity check argument and return eventually the argument 'a' */ *************** *** 64,68 **** else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return (a); }\ ! else if (r >= 2 && LOW(r) == -1)\ { bdd_error(BDD_ILLBDD); return (a); } --- 64,68 ---- else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return (a); }\ ! else if (r >= 2 && LOW(r) == INVALID_BDD)\ { bdd_error(BDD_ILLBDD); return (a); } *************** *** 71,77 **** else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return; }\ ! else if (r >= 2 && LOW(r) == -1)\ { bdd_error(BDD_ILLBDD); return; } /*=== SEMI-INTERNAL TYPES ==============================================*/ --- 71,217 ---- else if ((r) < 0 || (r) >= bddnodesize)\ { bdd_error(BDD_ILLBDD); return; }\ ! else if (r >= 2 && LOW(r) == INVALID_BDD)\ { bdd_error(BDD_ILLBDD); return; } + #if defined(SMALL_NODES) + + /*=== SEMI-INTERNAL TYPES ==============================================*/ + + typedef struct s_BddNode /* Node table entry */ + { + unsigned int hash_lref; + unsigned int next_href_mark; + unsigned int low_llev; + unsigned int high_hlev; + } BddNode; + + /*=== KERNEL DEFINITIONS ===============================================*/ + + #define NODE_MASK 0x07FFFFFF + #define LEV_LMASK 0xF8000000 + #define LEV_HMASK 0xF8000000 + + #define REF_LMASK 0xF8000000 + #define REF_HMASK 0xF0000000 + #define REF_LINC 0x08000000 + #define REF_HINC 0x10000000 + #define MARK_MASK 0x08000000 + #define HASH_MASK 0x07FFFFFF + #define NEXT_MASK 0x07FFFFFF + + #define NODE_BITS 27 + #define LEV_LPOS 27 + #define LEV_LBITS 5 + #define LEV_HPOS 27 + #define LEV_HBITS 5 + #define REF_LPOS 27 + #define REF_LBITS 5 + #define REF_HPOS 28 + #define REF_HBITS 4 + + #define INVALID_BDD NODE_MASK + #define MAXVAR ((1 << (LEV_LBITS + LEV_HBITS)) - 1) + #define MAX_PAIRSID MAXVAR + #define MAXREF ((1 << (REF_LBITS + REF_HBITS)) - 1) + + /* Reference counting */ + #define LREF(n) (bddnodes[n].hash_lref & REF_LMASK) + #define LREFp(n) (n->hash_lref & REF_LMASK) + #define HREF(n) (bddnodes[n].next_href_mark & REF_HMASK) + #define HREFp(n) (n->next_href_mark & REF_HMASK) + #define REF(n) ((bddnodes[n].hash_lref >> REF_LPOS) | \ + ((bddnodes[n].next_href_mark & REF_HMASK) >> (REF_HPOS-REF_LBITS))) + #define REFp(n) (((n)->hash_lref >> REF_LPOS) | \ + (((n)->next_href_mark & REF_HMASK) >> (REF_HPOS-REF_LBITS))) + + #define DECREF(n) { \ + if (LREF(n)!=REF_LMASK || HREF(n)!=REF_HMASK) { \ + if (LREF(n)==0) bddnodes[n].next_href_mark -= REF_HINC; \ + bddnodes[n].hash_lref -= REF_LINC; \ + } } + #define INCREF(n) { \ + if (LREF(n)!=REF_LMASK) bddnodes[n].hash_lref += REF_LINC; \ + else if (HREF(n)!=REF_HMASK) { \ + bddnodes[n].hash_lref += REF_LINC; \ + bddnodes[n].next_href_mark += REF_HINC; \ + } } + #define DECREFp(n) { \ + if (LREFp(n)!=REF_LMASK || HREFp(n)!=REF_HMASK) { \ + if (LREFp(n)==0) (n)->next_href_mark -= REF_HINC; \ + (n)->hash_lref -= REF_LINC; \ + } } + #define INCREFp(n) { \ + if (LREFp(n)!=REF_LMASK) (n)->hash_lref += REF_LINC; \ + else if (HREFp(n)!=REF_HMASK) { \ + (n)->hash_lref += REF_LINC; \ + (n)->next_href_mark += REF_HINC; \ + } } + #define HASREF(n) (LREF(n) != 0 || HREF(n) != 0) + + /* Marking BDD nodes */ + + #define MARKHIDE NEXT_MASK + #define SETMARK(n) (bddnodes[n].next_href_mark |= MARK_MASK) + #define UNMARK(n) (bddnodes[n].next_href_mark &= ~MARK_MASK) + #define MARKED(n) (bddnodes[n].next_href_mark & MARK_MASK) + #define SETMARKp(p) ((p)->next_href_mark |= MARK_MASK) + #define UNMARKp(p) ((p)->next_href_mark &= ~MARK_MASK) + #define MARKEDp(p) ((p)->next_href_mark & MARK_MASK) + + #define LOW(a) (bddnodes[a].low_llev & NODE_MASK) + #define HIGH(a) (bddnodes[a].high_hlev & NODE_MASK) + #define LOWp(p) ((p)->low_llev & NODE_MASK) + #define HIGHp(p) ((p)->high_hlev & NODE_MASK) + #define SETLOW(a,n) (bddnodes[a].low_llev = (n) | (bddnodes[a].low_llev & ~NODE_MASK)) + #define SETLOWp(p,n) ((p)->low_llev = (n) | ((p)->low_llev & ~NODE_MASK)) + #define SETLOWpz(p,n) ((p)->low_llev = (n)) + #define SETHIGH(a,n) (bddnodes[a].high_hlev = (n) | (bddnodes[a].high_hlev & ~NODE_MASK)) + #define SETHIGHp(p,n) ((p)->high_hlev = (n) | ((p)->high_hlev & ~NODE_MASK)) + #define HASH(a) (bddnodes[a].hash_lref & HASH_MASK) + #define HASHp(p) ((p)->hash_lref & HASH_MASK) + #define SETHASH(a,n) (bddnodes[a].hash_lref = (n) | (bddnodes[a].hash_lref & ~HASH_MASK)) + #define SETHASHp(p,n) ((p)->hash_lref = (n) | ((p)->hash_lref & ~HASH_MASK)) + #define NEXT(a) (bddnodes[a].next_href_mark & NEXT_MASK) + #define NEXTp(p) ((p)->next_href_mark & NEXT_MASK) + #define SETNEXT(a,n) (bddnodes[a].next_href_mark = (n) | (bddnodes[a].next_href_mark & ~NEXT_MASK)) + #define SETNEXTp(p,n) ((p)->next_href_mark = (n) | ((p)->next_href_mark & ~NEXT_MASK)) + #define SETNEXTpz(p,n) ((p)->next_href_mark = (n)) + #define CLRREF(n) { bddnodes[n].hash_lref &= ~REF_LMASK; bddnodes[n].next_href_mark &= ~REF_HMASK; } + #define CLRREFp(p) { (p)->hash_lref &= ~REF_LMASK; (p)->next_href_mark &= ~REF_HMASK; } + #define SETMAXREF(n) { bddnodes[n].hash_lref |= REF_LMASK; bddnodes[n].next_href_mark |= REF_HMASK; } + #define SETMAXREFp(p) { (p)->hash_lref |= REF_LMASK; (p)->next_href_mark |= REF_HMASK; } + #define LEVEL(n) ((bddnodes[n].low_llev >> LEV_LPOS) | \ + ((bddnodes[n].high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define LEVELp(p) (((p)->low_llev >> LEV_LPOS) | \ + (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define SETLEVEL(n,v) { \ + bddnodes[n].low_llev = ((v) << LEV_LPOS) | (bddnodes[n].low_llev & NODE_MASK); \ + bddnodes[n].high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | (bddnodes[n].high_hlev & NODE_MASK); \ + } + #define SETLEVELp(p,v) { \ + (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & NODE_MASK); \ + (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & NODE_MASK); \ + } + #define CLRLEVELREF(n) { \ + bddnodes[n].hash_lref &= ~REF_LMASK; \ + bddnodes[n].next_href_mark &= ~REF_HMASK; \ + bddnodes[n].low_llev &= ~LEV_LMASK; \ + bddnodes[n].high_hlev &= ~LEV_HMASK; \ + } + + #define INIT_NODE(n) { \ + bddnodes[n].hash_lref = 0; \ + bddnodes[n].next_href_mark = (n)+1; \ + bddnodes[n].low_llev = INVALID_BDD; \ + bddnodes[n].high_hlev = 0; \ + } + + #define CREATE_NODE(n, lev, lo, hi, nxt) { \ + bddnodes[n].next_href_mark = nxt; \ + bddnodes[n].low_llev = lo | ((lev) << LEV_LPOS); \ + bddnodes[n].high_hlev = hi | (((lev) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK); \ + } + + #else // SMALL_NODES /*=== SEMI-INTERNAL TYPES ==============================================*/ *************** *** 91,127 **** } BddNode; - - /*=== KERNEL VARIABLES =================================================*/ - - #ifdef CPLUSPLUS - extern "C" { - #endif - - extern int bddrunning; /* Flag - package initialized */ - extern int bdderrorcond; /* Some error condition was met */ - extern int bddnodesize; /* Number of allocated nodes */ - extern int bddmaxnodesize; /* Maximum allowed number of nodes */ - extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ - extern BddNode* bddnodes; /* All of the bdd nodes */ - extern int bddvarnum; /* Number of defined BDD variables */ - extern int* bddrefstack; /* Internal node reference stack */ - extern int* bddrefstacktop; /* Internal node reference stack top */ - extern int* bddvar2level; - extern int* bddlevel2var; - extern jmp_buf bddexception; - extern int bddreorderdisabled; - extern int bddresized; - extern bddCacheStat bddcachestats; - - #ifdef CPLUSPLUS - } - #endif - - /*=== KERNEL DEFINITIONS ===============================================*/ #define MAXVAR 0x1FFFFF #define MAXREF 0x3FF ! #define SRAND48SEED 0xbeef /* Reference counting */ --- 231,239 ---- } BddNode; /*=== KERNEL DEFINITIONS ===============================================*/ #define MAXVAR 0x1FFFFF #define MAXREF 0x3FF ! #define INVALID_BDD -1 /* Reference counting */ *************** *** 132,136 **** #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++ --- 244,248 ---- #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou++ #define HASREF(n) (REF(n) > 0) ! #else // USE_BITFIELDS #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++ *************** *** 138,142 **** #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ #define HASREF(n) (REF(n) > 0) ! #endif /* Marking BDD nodes */ --- 250,254 ---- #define INCREFp(n) if (REFp(n)<MAXREF) n->refcou_and_level++ #define HASREF(n) (REF(n) > 0) ! #endif // USE_BITFIELDS /* Marking BDD nodes */ *************** *** 152,156 **** #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 */ --- 264,268 ---- #define UNMARKp(p) (LEVELp(p) &= MARKOFF1) #define MARKEDp(p) (LEVELp(p) & MARKON1) ! #else // USE_BITFIELDS #define MARKON2 0x80000000 /* Bit used to mark a node (1) */ #define MARKOFF2 0x7FFFFFFF /* - unmark */ *************** *** 162,188 **** #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif ! ! ! /* Hashfunctions */ ! ! #define PAIR(a,b) ((unsigned int)((((unsigned int)a)+((unsigned int)b))*(((unsigned int)a)+((unsigned int)b)+((unsigned int)1))/((unsigned int)2)+((unsigned int)a))) ! #define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b)))) ! - /* Inspection of BDD nodes */ - #define ISCONST(a) ((a) < 2) - #define ISNONCONST(a) ((a) >= 2) - #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) --- 274,304 ---- #define UNMARKp(p) ((p)->refcou_and_level &= MARKOFF2) #define MARKEDp(p) ((p)->refcou_and_level & MARKON2) ! #endif // USE_BITFIELDS #define LOW(a) (bddnodes[a].low) #define HIGH(a) (bddnodes[a].high) #define LOWp(p) ((p)->low) #define HIGHp(p) ((p)->high) + #define SETLOW(a,n) (bddnodes[a].low = (n)) + #define SETLOWp(p,n) ((p)->low = (n)) + #define SETLOWpz(p,n) ((p)->low = (n)) + #define SETHIGH(a,n) (bddnodes[a].high = (n)) + #define SETHIGHp(p,n) ((p)->high = (n)) + #define NEXT(a) (bddnodes[a].next) + #define NEXTp(p) ((p)->next) + #define SETNEXT(a,n) (bddnodes[a].next = (n)) + #define SETNEXTp(p,n) ((p)->next = (n)) + #define SETNEXTpz(p,n) ((p)->next = (n)) + #define HASH(a) (bddnodes[a].hash) + #define HASHp(p) ((p)->hash) + #define SETHASH(a,n) (bddnodes[a].hash = (n)) + #define SETHASHp(p,n) ((p)->hash = (n)) #if defined(USE_BITFIELDS) #define REF(n) (bddnodes[n].refcou) #define REFp(n) ((n)->refcou) ! #define CLRREF(n) (bddnodes[n].refcou = 0) ! #define CLRREFp(p) ((p)->refcou = 0) ! #define SETMAXREF(n) (bddnodes[n].refcou = MAXREF) ! #define SETMAXREFp(p) ((p)->refcou |= MAXREF) #define LEVEL(n) (bddnodes[n].level) #define LEVELp(p) ((p)->level) *************** *** 190,198 **** #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) --- 306,317 ---- #define SETLEVELp(p,v) (LEVELp(p) = (v)) #define CLRLEVELREF(n) (bddnodes[n].refcou = bddnodes[n].level = 0) ! #define SETLEVELREF(n,v) { bddnodes[n].refcou = 0; bddnodes[n].level = v; } ! #else // USE_BITFIELDS #define REF(n) (bddnodes[n].refcou_and_level & MAXREF) #define REFp(n) ((n)->refcou_and_level & MAXREF) ! #define CLRREF(n) (bddnodes[n].refcou_and_level &= ~MAXREF) ! #define CLRREFp(p) ((p)->refcou_and_level &= ~MAXREF) ! #define SETMAXREF(n) (bddnodes[n].refcou_and_level |= MAXREF) ! #define SETMAXREFp(p) ((p)->refcou_and_level |= MAXREF) #define LEVEL(n) (bddnodes[n].refcou_and_level >> 10) #define LEVELp(p) ((p)->refcou_and_level >> 10) *************** *** 200,204 **** #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 */ --- 319,354 ---- #define SETLEVELp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) #define CLRLEVELREF(n) (bddnodes[n].refcou_and_level = 0) ! #define SETLEVELREF(n,v) (bddnodes[n].refcou_and_level = v << 10) ! #endif // USE_BITFIELDS ! ! #define INIT_NODE(n) { \ ! CLRLEVELREF(n); \ ! SETLOW(n, INVALID_BDD); \ ! SETHASH(n, 0); \ ! SETNEXT(n, n+1); \ ! } ! ! #define CREATE_NODE(n,lev,lo,hi,nxt) { \ ! SETLEVELREF(n, lev); \ ! SETLOW(n, lo); \ ! SETHIGH(n, hi); \ ! SETNEXT(n, nxt); \ ! } ! ! #endif // SMALL_NODES ! ! /* Hashfunctions */ ! ! #define PAIR(a,b) ((unsigned int)((((unsigned int)a)+((unsigned int)b))*(((unsigned int)a)+((unsigned int)b)+((unsigned int)1))/((unsigned int)2)+((unsigned int)a))) ! #define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b)))) ! ! ! /* Inspection of BDD nodes */ ! #define ISCONST(a) ((a) < 2) ! #define ISNONCONST(a) ((a) >= 2) ! #define ISONE(a) ((a) == 1) ! #define ISZERO(a) ((a) == 0) ! ! #define SRAND48SEED 0xbeef /* Stacking for garbage collector */ *************** *** 234,237 **** --- 384,413 ---- + /*=== KERNEL VARIABLES =================================================*/ + + #ifdef CPLUSPLUS + extern "C" { + #endif + + extern int bddrunning; /* Flag - package initialized */ + extern int bdderrorcond; /* Some error condition was met */ + extern int bddnodesize; /* Number of allocated nodes */ + extern int bddmaxnodesize; /* Maximum allowed number of nodes */ + extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ + extern BddNode* bddnodes; /* All of the bdd nodes */ + extern int bddvarnum; /* Number of defined BDD variables */ + extern int* bddrefstack; /* Internal node reference stack */ + extern int* bddrefstacktop; /* Internal node reference stack top */ + extern int* bddvar2level; + extern int* bddlevel2var; + extern jmp_buf bddexception; + extern int bddreorderdisabled; + extern int bddresized; + extern bddCacheStat bddcachestats; + + #ifdef CPLUSPLUS + } + #endif + /*=== KERNEL PROTOTYPES ================================================*/ Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** reorder.c 29 Jan 2005 11:33:58 -0000 1.6 --- reorder.c 31 Jan 2005 10:04:59 -0000 1.7 *************** *** 53,56 **** --- 53,66 ---- /* Change macros to reflect the above idea */ + #if defined(SMALL_NODES) + #define VAR(n) ((bddnodes[n].low_llev >> LEV_LPOS) | \ + ((bddnodes[n].high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define VARp(p) (((p)->low_llev >> LEV_LPOS) | \ + (((p)->high_hlev & LEV_HMASK) >> (LEV_HPOS-LEV_LBITS))) + #define SETVARp(p,v) { \ + (p)->low_llev = ((v) << LEV_LPOS) | ((p)->low_llev & ~NODE_MASK); \ + (p)->high_hlev = (((v) << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | ((p)->high_hlev & ~NODE_MASK); \ + } + #else #if defined(USE_BITFIELDS) #define VAR(n) (bddnodes[n].level) *************** *** 62,65 **** --- 72,76 ---- #define SETVARp(p,v) ((p)->refcou_and_level = ((p)->refcou_and_level & MAXREF) | (v << 10)) #endif + #endif /* Avoid these - they are misleading! */ *************** *** 880,888 **** /* 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) --- 891,896 ---- /* This is where we go from .level to .var! * - Do NOT use the LEVEL macro here. */ ! int v = bddlevel2var[VAR(n)]; ! SETVARp(&bddnodes[n], v); if (REF(n) > 0) *************** *** 919,927 **** /* Make sure the hash field is empty. This saves a loop in the initial GBC */ ! node->hash = 0; } ! bddnodes[0].hash = 0; ! bddnodes[1].hash = 0; free(dep); --- 927,935 ---- /* Make sure the hash field is empty. This saves a loop in the initial GBC */ ! SETHASHp(node, 0); } ! SETHASH(0, 0); ! SETHASH(1, 0); free(dep); *************** *** 952,963 **** hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = n; bddfreenum++; --- 960,971 ---- hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = n; bddfreenum++; *************** *** 1002,1006 **** for (n=bddnodesize-1 ; n>=0 ; n--) ! bddnodes[n].hash = 0; for (n=bddnodesize-1 ; n>=2 ; n--) --- 1010,1014 ---- for (n=bddnodesize-1 ; n>=0 ; n--) ! SETHASH(n, 0); for (n=bddnodesize-1 ; n>=2 ; n--) *************** *** 1013,1022 **** hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! node->next = bddfreepos; bddfreepos = n; } --- 1021,1030 ---- hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETNEXTp(node, bddfreepos); bddfreepos = n; } *************** *** 1052,1056 **** /* Try to find an existing node of this kind */ hash = NODEHASH(var, low, high); ! res = bddnodes[hash].hash; while(res != 0) --- 1060,1064 ---- /* Try to find an existing node of this kind */ hash = NODEHASH(var, low, high); ! res = HASH(hash); while(res != 0) *************** *** 1064,1068 **** return res; } ! res = bddnodes[res].next; #ifdef CACHESTATS --- 1072,1076 ---- return res; } ! res = NEXT(res); #ifdef CACHESTATS *************** *** 1100,1104 **** /* Build new node */ res = bddfreepos; ! bddfreepos = bddnodes[bddfreepos].next; levels[var].nodenum++; bddproduced++; --- 1108,1112 ---- /* Build new node */ res = bddfreepos; ! bddfreepos = NEXT(bddfreepos); levels[var].nodenum++; bddproduced++; *************** *** 1107,1119 **** node = &bddnodes[res]; SETVARp(node, var); ! LOWp(node) = low; ! HIGHp(node) = high; /* Insert node in hash chain */ ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = res; /* Make sure it is reference counted */ ! SETREFp(node, 1); INCREF(LOWp(node)); INCREF(HIGHp(node)); --- 1115,1128 ---- node = &bddnodes[res]; SETVARp(node, var); ! SETLOWp(node, low); ! SETHIGHp(node, high); /* Insert node in hash chain */ ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, res); /* Make sure it is reference counted */ ! CLRREFp(node); // <-- is this necessary? ! INCREFp(node); INCREF(LOWp(node)); INCREF(HIGHp(node)); *************** *** 1142,1158 **** int r; ! r = bddnodes[n + vl0].hash; ! bddnodes[n + vl0].hash = 0; while (r != 0) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) { /* Node does not depend on next var, let it stay in the chain */ ! node->next = bddnodes[n+vl0].hash; ! bddnodes[n+vl0].hash = r; levels[var0].nodenum++; } --- 1151,1167 ---- int r; ! r = HASH(n + vl0); ! SETHASH(n + vl0, 0); while (r != 0) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1) { /* Node does not depend on next var, let it stay in the chain */ ! SETNEXTp(node, HASH(n+vl0)); ! SETHASH(n+vl0, r); levels[var0].nodenum++; } *************** *** 1160,1164 **** { /* Node depends on next var - save it for later procesing */ ! node->next = toBeProcessed; toBeProcessed = r; #ifdef SWAPCOUNT --- 1169,1173 ---- { /* Node depends on next var - save it for later procesing */ ! SETNEXTp(node, toBeProcessed); toBeProcessed = r; #ifdef SWAPCOUNT *************** *** 1188,1192 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int f0 = LOWp(node); int f1 = HIGHp(node); --- 1197,1201 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int f0 = LOWp(node); int f1 = HIGHp(node); *************** *** 1226,1231 **** /* Update in-place */ SETVARp(node, var1); ! LOWp(node) = f0; ! HIGHp(node) = f1; levels[var1].nodenum++; --- 1235,1240 ---- /* Update in-place */ SETVARp(node, var1); ! SETLOWp(node, f0); ! SETHIGHp(node, f1); levels[var1].nodenum++; *************** *** 1233,1238 **** /* Rehash the node since it got new childs */ hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = toBeProcessed; toBeProcessed = next; --- 1242,1247 ---- /* Rehash the node since it got new childs */ hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, toBeProcessed); toBeProcessed = next; *************** *** 1255,1270 **** { int hash = n+vl1; ! int r = bddnodes[hash].hash; ! bddnodes[hash].hash = 0; while (r) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (REFp(node) > 0) { ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = r; } else --- 1264,1279 ---- { int hash = n+vl1; ! int r = HASH(hash); ! SETHASH(hash, 0); while (r) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (REFp(node) > 0) { ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, r); } else *************** *** 1273,1278 **** DECREF(HIGHp(node)); ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = r; levels[var1].nodenum--; --- 1282,1287 ---- DECREF(HIGHp(node)); ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = r; levels[var1].nodenum--; *************** *** 1297,1301 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int f0 = LOWp(node); int f1 = HIGHp(node); --- 1306,1310 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int f0 = LOWp(node); int f1 = HIGHp(node); *************** *** 1334,1340 **** /* Update in-place */ ! VARp(node) = var1; ! LOWp(node) = f0; ! HIGHp(node) = f1; levels[var1].nodenum++; --- 1343,1349 ---- /* Update in-place */ ! SETVARp(node, var1); ! SETLOWp(node, f0); ! SETHIGHp(node, f1); levels[var1].nodenum++; *************** *** 1357,1371 **** { int hash = n+vl1; ! int r = bddnodes[hash].hash; ! bddnodes[hash].hash = 0; while (r) { BddNode *node = &bddnodes[r]; ! int next = node->next; if (REFp(node) > 0) { ! node->next = toBeProcessed; toBeProcessed = r; } --- 1366,1380 ---- { int hash = n+vl1; ! int r = HASH(hash); ! SETHASH(hash, 0); while (r) { BddNode *node = &bddnodes[r]; ! int next = NEXTp(node); if (REFp(node) > 0) { ! SETNEXTp(node, toBeProcessed); toBeProcessed = r; } *************** *** 1375,1380 **** DECREF(HIGHp(node)); ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = r; levels[var1].nodenum--; --- 1384,1389 ---- DECREF(HIGHp(node)); ! SETLOWp(node, INVALID_BDD); ! SETNEXTp(node, bddfreepos); bddfreepos = r; levels[var1].nodenum--; *************** *** 1399,1407 **** { BddNode *node = &bddnodes[toBeProcessed]; ! int next = node->next; int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = toBeProcessed; toBeProcessed = next; --- 1408,1416 ---- { BddNode *node = &bddnodes[toBeProcessed]; ! int next = NEXTp(node); int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, toBeProcessed); toBeProcessed = next; *************** *** 1439,1443 **** { assert(VAR(r) == v); ! r = bddnodes[r].next; cou++; vcou++; --- 1448,1452 ---- { assert(VAR(r) == v); ! r = NEXT(r); cou++; vcou++; *************** *** 1700,1725 **** 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 } - #if 0 - for (n=0 ; n<bddvarnum ; n++) - printf("%3d\n", bddlevel2var[n]); - printf("\n"); - #endif - - #if 0 - for (n=0 ; n<bddvarnum ; n++) - printf("%3d: %4d nodes , %4d entries\n", n, levels[n].nodenum, - levels[n].size); - #endif free(extroots); free(levels); --- 1709,1719 ---- UNMARK(n); else ! CLRREF(n); /* This is where we go from .var to .level again! * - Do NOT use the LEVEL macro here. */ ! { int v = bddvar2level[VAR(n)]; SETVARp(&bddnodes[n], v); } } free(extroots); free(levels); |
|
From: John W. <joe...@us...> - 2005-01-31 10:03:30
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22921/buddy/src Modified Files: kernel.c Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** kernel.c 17 Nov 2004 23:05:14 -0000 1.5 --- kernel.c 31 Jan 2005 10:03:20 -0000 1.6 *************** *** 213,227 **** 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; if ((err=bdd_operator_init(cs)) < 0) { --- 213,224 ---- for (n=0 ; n<bddnodesize ; n++) { ! INIT_NODE(n); } ! SETNEXT(bddnodesize-1, 0); ! SETMAXREF(0); ! SETMAXREF(1); ! SETLOW(0,0); SETHIGH(0,0); ! SETLOW(1,1); SETHIGH(1,1); if ((err=bdd_operator_init(cs)) < 0) { *************** *** 394,399 **** } ! SETREF(bddvarset[bddvarnum*2], MAXREF); ! SETREF(bddvarset[bddvarnum*2+1], MAXREF); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; --- 391,396 ---- } ! SETMAXREF(bddvarset[bddvarnum*2]); ! SETMAXREF(bddvarset[bddvarnum*2+1]); bddlevel2var[bddvarnum] = bddvarnum; bddvar2level[bddvarnum] = bddvarnum; *************** *** 731,735 **** char *bdd_versionstr(void) { ! static char str[] = "BuDDy - release " PACKAGE_VERSION; BUDDY_PROLOGUE; RETURN(str); --- 728,732 ---- char *bdd_versionstr(void) { ! static char str[] = "BuDDy - release " PACKAGE_VERSION; BUDDY_PROLOGUE; RETURN(str); *************** *** 944,947 **** --- 941,945 ---- BDD bdd_ithvar(int var) { + int res; BUDDY_PROLOGUE; ADD_ARG1(T_INT,var); *************** *** 952,956 **** } ! RETURN_BDD(bddvarset[var*2]); } --- 950,955 ---- } ! res = bddvarset[var*2]; ! RETURN_BDD(res); } *************** *** 972,975 **** --- 971,975 ---- BDD bdd_nithvar(int var) { + int res; BUDDY_PROLOGUE; ADD_ARG1(T_INT,var); *************** *** 980,984 **** } ! RETURN_BDD(bddvarset[var*2+1]); } --- 980,985 ---- } ! res = bddvarset[var*2+1]; ! RETURN_BDD(res); } *************** *** 1095,1109 **** register BddNode *node = &bddnodes[n]; ! if (LOWp(node) != -1) { register unsigned int hash; hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! node->next = bddfreepos; bddfreepos = n; bddfreenum++; --- 1096,1110 ---- register BddNode *node = &bddnodes[n]; ! if (LOWp(node) != INVALID_BDD) { register unsigned int hash; hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETNEXTpz(node, bddfreepos); bddfreepos = n; bddfreenum++; *************** *** 1135,1141 **** for (n=0 ; n<bddnodesize ; n++) { ! if (REF(n) > 0) ! bdd_mark(n); ! bddnodes[n].hash = 0; } --- 1136,1141 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (HASREF(n)) bdd_mark(n); ! SETHASH(n, 0); } *************** *** 1147,1151 **** register BddNode *node = &bddnodes[n]; ! if (MARKEDp(node) && LOWp(node) != -1) { register unsigned int hash; --- 1147,1151 ---- register BddNode *node = &bddnodes[n]; ! if (MARKEDp(node) && LOWp(node) != INVALID_BDD) { register unsigned int hash; *************** *** 1153,1163 **** UNMARKp(node); hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = n; } else { ! LOWp(node) = -1; ! node->next = bddfreepos; bddfreepos = n; bddfreenum++; --- 1153,1163 ---- UNMARKp(node); hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node)); ! SETNEXTp(node, HASH(hash)); ! SETHASH(hash, n); } else { ! SETLOWpz(node, INVALID_BDD); // obliterates refcount ! SETNEXTpz(node, bddfreepos); // obliterates lev, mark bddfreepos = n; bddfreenum++; *************** *** 1205,1209 **** if (root >= bddnodesize) RETURN_BDD(bdd_error(BDD_ILLBDD)); ! if (LOW(root) == -1) RETURN_BDD(bdd_error(BDD_ILLBDD)); --- 1205,1209 ---- if (root >= bddnodesize) RETURN_BDD(bdd_error(BDD_ILLBDD)); ! if (LOW(root) == INVALID_BDD) RETURN_BDD(bdd_error(BDD_ILLBDD)); *************** *** 1233,1237 **** if (root >= bddnodesize) RETURN_BDD(bdd_error(BDD_ILLBDD)); ! if (LOW(root) == -1) RETURN_BDD(bdd_error(BDD_ILLBDD)); --- 1233,1237 ---- if (root >= bddnodesize) RETURN_BDD(bdd_error(BDD_ILLBDD)); ! if (LOW(root) == INVALID_BDD) RETURN_BDD(bdd_error(BDD_ILLBDD)); *************** *** 1257,1261 **** node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == -1) return; --- 1257,1261 ---- node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == INVALID_BDD) return; *************** *** 1274,1278 **** return; ! if (MARKEDp(node) || LOWp(node) == -1) return; --- 1274,1278 ---- return; ! if (MARKEDp(node) || LOWp(node) == INVALID_BDD) return; *************** *** 1295,1299 **** node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == -1) return; --- 1295,1299 ---- node = &bddnodes[i]; ! if (MARKEDp(node) || LOWp(node) == INVALID_BDD) return; *************** *** 1315,1319 **** node = &bddnodes[i]; ! if (!MARKEDp(node) || LOWp(node) == -1) return; UNMARKp(node); --- 1315,1319 ---- node = &bddnodes[i]; ! if (!MARKEDp(node) || LOWp(node) == INVALID_BDD) return; UNMARKp(node); *************** *** 1364,1368 **** /* Try to find an existing node of this kind */ hash = NODEHASH(level, low, high); ! res = bddnodes[hash].hash; while(res != 0) --- 1364,1368 ---- /* Try to find an existing node of this kind */ hash = NODEHASH(level, low, high); ! res = HASH(hash); while(res != 0) *************** *** 1376,1380 **** } ! res = bddnodes[res].next; #ifdef CACHESTATS bddcachestats.uniqueChain++; --- 1376,1380 ---- } ! res = NEXT(res); #ifdef CACHESTATS bddcachestats.uniqueChain++; *************** *** 1419,1434 **** /* Build new node */ res = bddfreepos; ! bddfreepos = bddnodes[bddfreepos].next; bddfreenum--; bddproduced++; ! node = &bddnodes[res]; ! SETLEVELp(node, level); ! LOWp(node) = low; ! HIGHp(node) = high; ! ! /* Insert node */ ! node->next = bddnodes[hash].hash; ! bddnodes[hash].hash = res; return res; --- 1419,1432 ---- /* Build new node */ res = bddfreepos; ! bddfreepos = NEXT(bddfreepos); bddfreenum--; bddproduced++; ! { ! int next = HASH(hash); ! CREATE_NODE(res, level, low, high, next); ! /* Insert node */ ! SETHASH(hash, res); ! } return res; *************** *** 1461,1474 **** if (doRehash) for (n=0 ; n<oldsize ; n++) ! bddnodes[n].hash = 0; for (n=oldsize ; n<bddnodesize ; n++) { ! CLRLEVELREF(n); ! bddnodes[n].hash = 0; ! LOW(n) = -1; ! bddnodes[n].next = n+1; } ! bddnodes[bddnodesize-1].next = bddfreepos; bddfreepos = oldsize; bddfreenum += bddnodesize - oldsize; --- 1459,1469 ---- if (doRehash) for (n=0 ; n<oldsize ; n++) ! SETHASH(n, 0); for (n=oldsize ; n<bddnodesize ; n++) { ! INIT_NODE(n); } ! SETNEXT(bddnodesize-1, bddfreepos); bddfreepos = oldsize; bddfreenum += bddnodesize - oldsize; |
|
From: John W. <joe...@us...> - 2005-01-31 10:03:02
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22834/buddy/src Modified Files: cppext.cxx Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: cppext.cxx =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/cppext.cxx,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** cppext.cxx 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- cppext.cxx 31 Jan 2005 10:02:53 -0000 1.2 *************** *** 335,339 **** const BddNode *node = &bddnodes[n]; ! if (LOWp(node) != -1) { o << "[" << setw(5) << n << "] "; --- 335,339 ---- const BddNode *node = &bddnodes[n]; ! if (LOWp(node) != INVALID_BDD) { o << "[" << setw(5) << n << "] "; |
|
From: John W. <joe...@us...> - 2005-01-31 10:02:53
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22791/buddy/src Modified Files: bddop.c Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** bddop.c 17 Nov 2004 23:03:43 -0000 1.8 --- bddop.c 31 Jan 2005 10:02:43 -0000 1.9 *************** *** 2910,2914 **** node = &bddnodes[r]; ! if (MARKEDp(node) || LOWp(node) == -1) return; --- 2910,2914 ---- node = &bddnodes[r]; ! if (MARKEDp(node) || LOWp(node) == INVALID_BDD) return; |
|
From: John W. <joe...@us...> - 2005-01-31 10:02:29
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22750/buddy/src Modified Files: bddio.c Log Message: Updates to buddy to support small (4 word) BDD nodes. Index: bddio.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddio.c,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** bddio.c 1 Oct 2004 02:17:20 -0000 1.3 --- bddio.c 31 Jan 2005 10:02:20 -0000 1.4 *************** *** 131,135 **** for (n=0 ; n<bddnodesize ; n++) { ! if (LOW(n) != -1) { fprintf(ofile, "[%5d - %2d] ", n, REF(n)); --- 131,135 ---- for (n=0 ; n<bddnodesize ; n++) { ! if (LOW(n) != INVALID_BDD) { fprintf(ofile, "[%5d - %2d] ", n, REF(n)); |
|
From: John W. <joe...@us...> - 2005-01-31 00:09:21
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1098/bdd Modified Files: BDDTestCase.java Log Message: Better printing of exception information on BDD factory creation. Index: BDDTestCase.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BDDTestCase.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** BDDTestCase.java 30 Jan 2005 14:43:40 -0000 1.5 --- BDDTestCase.java 31 Jan 2005 00:09:12 -0000 1.6 *************** *** 7,10 **** --- 7,11 ---- import java.util.Iterator; import java.util.LinkedList; + import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; import junit.framework.TestCase; *************** *** 44,48 **** } catch (Throwable _) { ! System.out.println("Failed: "+_); } } --- 45,51 ---- } catch (Throwable _) { ! if (_ instanceof InvocationTargetException) ! _ = ((InvocationTargetException)_).getTargetException(); ! System.out.println("Failed initializing "+bddpackage+": "+_); } } |
|
From: John W. <joe...@us...> - 2005-01-31 00:08:49
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv944/bdd Modified Files: BasicTests.java Log Message: Add support for MicroFactory Index: BasicTests.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BasicTests.java,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** BasicTests.java 17 Nov 2004 08:21:32 -0000 1.2 --- BasicTests.java 31 Jan 2005 00:08:33 -0000 1.3 *************** *** 182,186 **** static boolean isFreed(BDD b) { ! return b.hashCode() == -1; } --- 182,186 ---- static boolean isFreed(BDD b) { ! return b.hashCode() == -1 || b.hashCode() == 0x07ffffff; } |
|
From: John W. <joe...@us...> - 2005-01-31 00:08:14
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv833/net/sf/javabdd Modified Files: TestBDDFactory.java Log Message: Fix getVersion(). Get BDD factories to test from system properties. Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** TestBDDFactory.java 19 Oct 2004 11:11:35 -0000 1.4 --- TestBDDFactory.java 31 Jan 2005 00:08:05 -0000 1.5 *************** *** 30,35 **** public static BDDFactory init(int nodenum, int cachesize) { ! BDDFactory a = BuDDyFactory.init(nodenum, cachesize); ! BDDFactory b = JDDFactory.init(nodenum, cachesize); return new TestBDDFactory(a, b); } --- 30,37 ---- public static BDDFactory init(int nodenum, int cachesize) { ! String bdd1 = System.getProperty("bdd1", "j"); ! String bdd2 = System.getProperty("bdd2", "micro"); ! BDDFactory a = BDDFactory.init(bdd1, nodenum, cachesize); ! BDDFactory b = BDDFactory.init(bdd2, nodenum, cachesize); return new TestBDDFactory(a, b); } *************** *** 992,996 **** public String getVersion() { return "TestBDD "+REVISION.substring(11, REVISION.length()-2)+ ! " of ("+f1.getVersion()+","+f1.getVersion()+")"; } } --- 994,998 ---- public String getVersion() { return "TestBDD "+REVISION.substring(11, REVISION.length()-2)+ ! " of ("+f1.getVersion()+","+f2.getVersion()+")"; } } |
|
From: John W. <joe...@us...> - 2005-01-31 00:07:23
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv620/net/sf/javabdd Modified Files: MicroFactory.java Log Message: Bug fixes to make it actually work. Index: MicroFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/MicroFactory.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** MicroFactory.java 30 Jan 2005 14:42:22 -0000 1.1 --- MicroFactory.java 31 Jan 2005 00:07:11 -0000 1.2 *************** *** 37,41 **** static final boolean USE_FINALIZER = false; static final boolean CACHESTATS = false; ! public static boolean FLUSH_CACHE_ON_GC = false; private MicroFactory() { } --- 37,41 ---- static final boolean USE_FINALIZER = false; static final boolean CACHESTATS = false; ! public static boolean FLUSH_CACHE_ON_GC = true; private MicroFactory() { } *************** *** 61,65 **** static final int offset__llev = 2; static final int offset__hlev = 3; ! static final int offset__mark = 0; static final int NODE_MASK = 0x07FFFFFF; --- 61,65 ---- static final int offset__llev = 2; static final int offset__hlev = 3; ! static final int offset__mark = 1; static final int NODE_MASK = 0x07FFFFFF; *************** *** 122,129 **** if (a == 0) { if (b == 0) return; ! table[node*__node_size + offset__high] -= REF_HINC; } else if (b == REF_HMASK) return; } ! table[node*__node_size + offset__low] -= REF_LINC; } --- 122,129 ---- if (a == 0) { if (b == 0) return; ! table[node*__node_size + offset__href] -= REF_HINC; } else if (b == REF_HMASK) return; } ! table[node*__node_size + offset__lref] -= REF_LINC; } *************** *** 137,141 **** int a = table[node*__node_size + offset__llev] & LEV_LMASK; int b = table[node*__node_size + offset__hlev] & LEV_HMASK; ! return a >>> LEV_LPOS | b >>> (LEV_HPOS-LEV_LBITS); } --- 137,142 ---- int a = table[node*__node_size + offset__llev] & LEV_LMASK; int b = table[node*__node_size + offset__hlev] & LEV_HMASK; ! int lev = a >>> LEV_LPOS | b >>> (LEV_HPOS-LEV_LBITS); ! return lev; } *************** *** 207,211 **** private final void INIT_NODE(int r, int lev, int lo, int hi, int next) { ! table[r*__node_size + offset__hash] = 0; table[r*__node_size + offset__next] = next; table[r*__node_size + offset__low] = lo | (lev << LEV_LPOS); --- 208,212 ---- private final void INIT_NODE(int r, int lev, int lo, int hi, int next) { ! //table[r*__node_size + offset__hash] = 0; table[r*__node_size + offset__next] = next; table[r*__node_size + offset__low] = lo | (lev << LEV_LPOS); *************** *** 644,648 **** final OpCache1 copy() { OpCache1 that = new OpCache1(this.table.length); ! System.arraycopy(this.table, 0, that.table, 0, this.table.length); that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; --- 645,652 ---- final OpCache1 copy() { OpCache1 that = new OpCache1(this.table.length); ! for (int i = 0; i < this.table.length; ++i) { ! that.table[i].a = this.table[i].a; ! that.table[i].res = this.table[i].res; ! } that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; *************** *** 683,687 **** final OpCache2 copy() { OpCache2 that = new OpCache2(this.table.length); ! System.arraycopy(this.table, 0, that.table, 0, this.table.length); that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; --- 687,695 ---- final OpCache2 copy() { OpCache2 that = new OpCache2(this.table.length); ! for (int i = 0; i < this.table.length; ++i) { ! that.table[i].a = this.table[i].a; ! that.table[i].b = this.table[i].b; ! that.table[i].res = this.table[i].res; ! } that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; *************** *** 723,727 **** final OpCache3 copy() { OpCache3 that = new OpCache3(this.table.length); ! System.arraycopy(this.table, 0, that.table, 0, this.table.length); that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; --- 731,780 ---- final OpCache3 copy() { OpCache3 that = new OpCache3(this.table.length); ! for (int i = 0; i < this.table.length; ++i) { ! that.table[i].a = this.table[i].a; ! that.table[i].b = this.table[i].b; ! that.table[i].c = this.table[i].c; ! that.table[i].res = this.table[i].res; ! } ! that.cacheHit = this.cacheHit; ! that.cacheMiss = this.cacheMiss; ! return that; ! } ! } ! ! private class OpCacheD { ! OpCacheDEntry table[]; ! int cacheHit; ! int cacheMiss; ! OpCacheD(int size) { alloc(size); } ! final void alloc(int size) { ! table = new OpCacheDEntry[size]; ! for (int i = 0; i < table.length; ++i) { ! table[i] = new OpCacheDEntry(); ! } ! } ! final OpCacheDEntry lookup(int hash) { ! return (OpCacheDEntry) table[Math.abs(hash % table.length)]; ! } ! final void reset() { ! for (int i = 0; i < table.length; ++i) { ! table[i].a = -1; ! } ! } ! final void clean() { ! for (int i = 0; i < table.length; ++i) { ! int a = table[i].a; ! if (a == -1) continue; ! if (LOW(a & NODE_MASK) == INVALID_BDD) { ! table[i].a = -1; ! } ! } ! } ! final OpCacheD copy() { ! OpCacheD that = new OpCacheD(this.table.length); ! for (int i = 0; i < this.table.length; ++i) { ! that.table[i].a = this.table[i].a; ! that.table[i].res = this.table[i].res; ! } that.cacheHit = this.cacheHit; that.cacheMiss = this.cacheMiss; *************** *** 841,844 **** --- 894,921 ---- } + + private static class OpCacheDEntry { + int a; + double res; + + final double get_sid(int node, int id) { + if (VERIFY_ASSERTIONS) { + _assert(node == (node & NODE_MASK)); + _assert(id == (id & ~NODE_MASK)); + } + int k = node | id; + if (a != k) return -1; + return res; + } + + final void set_sid(int node, int id, double r) { + if (VERIFY_ASSERTIONS) { + _assert(node == (node & NODE_MASK)); + _assert(id == (id & ~NODE_MASK)); + } + a = node | id; + res = r; + } + } private static class JavaBDDException extends BDDException { *************** *** 859,863 **** int bddmaxnodesize; /* Maximum allowed number of nodes */ int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ - int[] bddnodes; /* All of the bdd nodes */ int bddfreepos; /* First free node */ int bddfreenum; /* Number of free nodes */ --- 936,939 ---- *************** *** 2802,2824 **** CHECK(r); ! miscid = CACHEID_PATHCOU; ! if (countcache == null) countcache = new OpCache2(cachesize); return bdd_pathcount_rec(r); } ! float bdd_pathcount_rec(int r) { ! OpCache2Entry entry; ! float size; if (ISZERO(r)) return 0f; if (ISONE(r)) return 1f; - int res; entry = countcache.lookup(PATHCOUHASH(r)); ! if ((res = entry.get(r, miscid)) != -1) { if (CACHESTATS) countcache.cacheHit++; ! return Float.intBitsToFloat(res); } if (CACHESTATS) countcache.cacheMiss++; --- 2878,2899 ---- CHECK(r); ! miscid = CACHEID_PATHCOU << NODE_BITS; ! if (countcache == null) countcache = new OpCacheD(cachesize); return bdd_pathcount_rec(r); } ! double bdd_pathcount_rec(int r) { ! OpCacheDEntry entry; ! double size; if (ISZERO(r)) return 0f; if (ISONE(r)) return 1f; entry = countcache.lookup(PATHCOUHASH(r)); ! if ((size = entry.get_sid(r, miscid)) >= 0) { if (CACHESTATS) countcache.cacheHit++; ! return size; } if (CACHESTATS) countcache.cacheMiss++; *************** *** 2826,2830 **** size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r)); ! entry.set(r, miscid, Float.floatToIntBits(size)); return size; --- 2901,2905 ---- size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r)); ! entry.set_sid(r, miscid, size); return size; *************** *** 2892,2898 **** CHECK(r); ! if (countcache == null) countcache = new OpCache2(cachesize); ! miscid = CACHEID_SATCOU; size = Math.pow(2.0, (double) LEVEL(r)); --- 2967,2973 ---- CHECK(r); ! if (countcache == null) countcache = new OpCacheD(cachesize); ! miscid = CACHEID_SATCOU << NODE_BITS; size = Math.pow(2.0, (double) LEVEL(r)); *************** *** 2915,2929 **** } ! float satcount_rec(int r) { ! OpCache2Entry entry; ! float size, s; if (ISCONST(r)) return r; - int res; entry = countcache.lookup(SATCOUHASH(r)); ! if ((res = entry.get(r, miscid)) != -1) { if (CACHESTATS) countcache.cacheHit++; ! return Float.intBitsToFloat(res); } --- 2990,3003 ---- } ! double satcount_rec(int r) { ! OpCacheDEntry entry; ! double size, s; if (ISCONST(r)) return r; entry = countcache.lookup(SATCOUHASH(r)); ! if ((size = entry.get_sid(r, miscid)) >= 0) { if (CACHESTATS) countcache.cacheHit++; ! return size; } *************** *** 2941,2945 **** size += s * satcount_rec(HIGH_r); ! entry.set(r, miscid, Float.floatToIntBits(size)); return size; --- 3015,3019 ---- size += s * satcount_rec(HIGH_r); ! entry.set_sid(r, miscid, size); return size; *************** *** 3185,3190 **** int n; newnodes = new int[bddnodesize*__node_size]; ! System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length); ! bddnodes = newnodes; if (doRehash) --- 3259,3264 ---- int n; newnodes = new int[bddnodesize*__node_size]; ! System.arraycopy(table, 0, newnodes, 0, table.length); ! table = newnodes; if (doRehash) *************** *** 3218,3223 **** bddnodesize = bdd_prime_gte(initnodesize); ! bddnodes = new int[bddnodesize*__node_size]; bddresized = false; --- 3292,3298 ---- bddnodesize = bdd_prime_gte(initnodesize); + cachesize = bdd_prime_gte(cs); ! table = new int[bddnodesize*__node_size]; bddresized = false; *************** *** 3234,3238 **** SETLOW(1, 1); SETHIGH(1, 1); ! bdd_operator_init(cs); bddfreepos = 2; --- 3309,3313 ---- SETLOW(1, 1); SETHIGH(1, 1); ! bdd_operator_init(cachesize); bddfreepos = 2; *************** *** 3242,3246 **** gbcollectnum = 0; gbcclock = 0; - cachesize = cs; usednodes_nextreorder = bddnodesize; bddmaxnodeincrease = DEFAULTMAXNODEINC; --- 3317,3320 ---- *************** *** 3250,3255 **** bdd_pairs_init(); bdd_reorder_init(); - - return; } --- 3324,3327 ---- *************** *** 3319,3324 **** OpCache3 appexcache; /* appex(), appall(), appuni(), constrain(), compose() */ OpCache3 itecache; /* ite() */ - OpCache2 countcache; /* satcount() */ OpCache2 misccache; /* other functions */ void bdd_operator_init(int cachesize) { --- 3391,3396 ---- OpCache3 appexcache; /* appex(), appall(), appuni(), constrain(), compose() */ OpCache3 itecache; /* ite() */ OpCache2 misccache; /* other functions */ + OpCacheD countcache; /* satcount(), pathcount() */ void bdd_operator_init(int cachesize) { *************** *** 3347,3375 **** void bdd_operator_reset() { ! singlecache.reset(); ! replacecache.reset(); ! andcache.reset(); ! orcache.reset(); ! applycache.reset(); ! relprodcache.reset(); ! quantcache.reset(); ! appexcache.reset(); ! itecache.reset(); ! countcache.reset(); ! misccache.reset(); } void bdd_operator_clean() { ! singlecache.clean(); ! replacecache.clean(); ! andcache.clean(); ! orcache.clean(); ! applycache.clean(); ! relprodcache.clean(); ! quantcache.clean(); ! appexcache.clean(); ! itecache.clean(); ! countcache.clean(); ! misccache.clean(); } --- 3419,3469 ---- void bdd_operator_reset() { ! if (singlecache != null) ! singlecache.reset(); ! if (replacecache != null) ! replacecache.reset(); ! if (andcache != null) ! andcache.reset(); ! if (orcache != null) ! orcache.reset(); ! if (applycache != null) ! applycache.reset(); ! if (relprodcache != null) ! relprodcache.reset(); ! if (quantcache != null) ! quantcache.reset(); ! if (appexcache != null) ! appexcache.reset(); ! if (itecache != null) ! itecache.reset(); ! if (countcache != null) ! countcache.reset(); ! if (misccache != null) ! misccache.reset(); } void bdd_operator_clean() { ! if (singlecache != null) ! singlecache.clean(); ! if (replacecache != null) ! replacecache.clean(); ! if (andcache != null) ! andcache.clean(); ! if (orcache != null) ! orcache.clean(); ! if (applycache != null) ! applycache.clean(); ! if (relprodcache != null) ! relprodcache.clean(); ! if (quantcache != null) ! quantcache.clean(); ! if (appexcache != null) ! appexcache.clean(); ! if (itecache != null) ! itecache.clean(); ! if (countcache != null) ! countcache.clean(); ! if (misccache != null) ! misccache.clean(); } *************** *** 3377,3381 **** quantvarset = new int[bddvarnum]; quantvarsetID = 0; ! countcache.reset(); } --- 3471,3475 ---- quantvarset = new int[bddvarnum]; quantvarsetID = 0; ! if (countcache != null) countcache.reset(); } *************** *** 4313,4317 **** bdd_pairs_done(); ! bddnodes = null; bddrefstack = null; bddvarset = null; --- 4407,4411 ---- bdd_pairs_done(); ! table = null; bddrefstack = null; bddvarset = null; *************** *** 5258,5262 **** for (n = 2, extrootsize = 0; n < bddnodesize; n++) { /* This is where we go from .level to .var! */ ! SETVARr(n, bddlevel2var[LEVEL(n)]); if (HASREF(n)) { --- 5352,5358 ---- for (n = 2, extrootsize = 0; n < bddnodesize; n++) { /* This is where we go from .level to .var! */ ! int lev = LEVEL(n); ! int var = bddlevel2var[lev]; ! SETVARr(n, var); if (HASREF(n)) { *************** *** 6198,6203 **** INSTANCE.bddresized = this.bddresized; INSTANCE.minfreenodes = this.minfreenodes; ! INSTANCE.bddnodes = new int[this.bddnodes.length]; ! System.arraycopy(this.bddnodes, 0, INSTANCE.bddnodes, 0, this.bddnodes.length); INSTANCE.bddrefstack = new int[this.bddrefstack.length]; System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length); --- 6294,6299 ---- INSTANCE.bddresized = this.bddresized; INSTANCE.minfreenodes = this.minfreenodes; ! INSTANCE.table = new int[this.table.length]; ! System.arraycopy(this.table, 0, INSTANCE.table, 0, this.table.length); INSTANCE.bddrefstack = new int[this.bddrefstack.length]; System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length); |
|
From: John W. <joe...@us...> - 2005-01-31 00:05:27
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32682/net/sf/javabdd Modified Files: JFactory.java Log Message: Turn on cache flush on gc. Also fix bug in cloneFactory(). Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.12 retrieving revision 1.13 diff -C2 -d -r1.12 -r1.13 *** JFactory.java 30 Jan 2005 14:42:22 -0000 1.12 --- JFactory.java 31 Jan 2005 00:05:17 -0000 1.13 *************** *** 47,51 **** static final boolean USE_FINALIZER = false; ! public static boolean FLUSH_CACHE_ON_GC = false; /** --- 47,51 ---- static final boolean USE_FINALIZER = false; ! public static boolean FLUSH_CACHE_ON_GC = true; /** *************** *** 6348,6358 **** public JFactory cloneFactory() { JFactory INSTANCE = new JFactory(); ! INSTANCE.applycache = this.applycache.copy(); ! INSTANCE.itecache = this.itecache.copy(); ! INSTANCE.quantcache = this.quantcache.copy(); INSTANCE.appexcache = this.appexcache.copy(); ! INSTANCE.replacecache = this.replacecache.copy(); ! INSTANCE.misccache = this.misccache.copy(); ! INSTANCE.countcache = this.countcache.copy(); // TODO: potential difference here (!) INSTANCE.rng = new Random(); --- 6348,6364 ---- public JFactory cloneFactory() { JFactory INSTANCE = new JFactory(); ! if (applycache != null) ! INSTANCE.applycache = this.applycache.copy(); ! if (itecache != null) ! INSTANCE.itecache = this.itecache.copy(); ! if (quantcache != null) ! INSTANCE.quantcache = this.quantcache.copy(); INSTANCE.appexcache = this.appexcache.copy(); ! if (replacecache != null) ! INSTANCE.replacecache = this.replacecache.copy(); ! if (misccache != null) ! INSTANCE.misccache = this.misccache.copy(); ! if (countcache != null) ! INSTANCE.countcache = this.countcache.copy(); // TODO: potential difference here (!) INSTANCE.rng = new Random(); |
|
From: John W. <joe...@us...> - 2005-01-30 14:44:09
|
Update of /cvsroot/javabdd/JavaBDD_tests/bdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31620/bdd Modified Files: BDDTestCase.java Log Message: Added new microBDD factory: each BDD node is only 4 words. Index: BDDTestCase.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD_tests/bdd/BDDTestCase.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** BDDTestCase.java 19 Oct 2004 11:46:29 -0000 1.4 --- BDDTestCase.java 30 Jan 2005 14:43:40 -0000 1.5 *************** *** 22,25 **** --- 22,26 ---- "net.sf.javabdd.BuDDyFactory", "net.sf.javabdd.JFactory", + "net.sf.javabdd.MicroFactory", //"net.sf.javabdd.CUDDFactory", //"net.sf.javabdd.CALFactory", |
|
From: John W. <joe...@us...> - 2005-01-30 14:43:11
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31490/buddy/src Modified Files: pairs.c Log Message: Added comment. Index: pairs.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/pairs.c,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** pairs.c 29 Sep 2004 10:00:50 -0000 1.2 --- pairs.c 30 Jan 2005 14:43:02 -0000 1.3 *************** *** 82,85 **** --- 82,86 ---- for (p=pairs ; p!=NULL ; p=p->next) p->id = pairsid++; + // TODO: only need to reset replacecache bdd_operator_reset(); } |
