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...> - 2004-09-29 10:20:10
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv27562/buddy/src Modified Files: Makefile.am Log Message: Index: Makefile.am =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/Makefile.am,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** Makefile.am 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- Makefile.am 29 Sep 2004 10:19:56 -0000 1.2 *************** *** 21,25 **** prime.h \ reorder.c \ ! tree.c # See the `Updating version info' node of the Libtool manual before --- 21,26 ---- prime.h \ reorder.c \ ! tree.c \ ! trace.c # See the `Updating version info' node of the Libtool manual before |
|
From: John W. <joe...@us...> - 2004-09-29 10:13:58
|
Update of /cvsroot/javabdd/buddy/xdocs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26648 Removed Files: compiling.xml installing.xml navigation.xml performance.xml Log Message: --- installing.xml DELETED --- --- navigation.xml DELETED --- --- performance.xml DELETED --- --- compiling.xml DELETED --- |
|
From: John W. <joe...@us...> - 2004-09-29 10:09:22
|
Update of /cvsroot/javabdd/buddy/.externalToolBuilders In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25926/.externalToolBuilders Removed Files: Makefile builder.launch Log Message: --- Makefile builder.launch DELETED --- |
Update of /cvsroot/javabdd/buddy/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25254/org/sf/javabdd Removed Files: BuDDyFactory.java BDDPairing.java TypedBDDFactory.java BDDDomain.java JDDFactory.java CUDDFactory.java HijackingClassLoader.java BDD.java FindBestOrder.java BDDFactory.java JFactory.java BDDBitVector.java TestBDDFactory.java TryVarOrder.java CALFactory.java BDDException.java Log Message: --- BuDDyFactory.java DELETED --- --- BDDDomain.java DELETED --- --- JFactory.java DELETED --- --- TypedBDDFactory.java DELETED --- --- JDDFactory.java DELETED --- --- BDDException.java DELETED --- --- BDDFactory.java DELETED --- --- FindBestOrder.java DELETED --- --- CUDDFactory.java DELETED --- --- BDD.java DELETED --- --- TestBDDFactory.java DELETED --- --- BDDPairing.java DELETED --- --- HijackingClassLoader.java DELETED --- --- TryVarOrder.java DELETED --- --- CALFactory.java DELETED --- --- BDDBitVector.java DELETED --- |
Update of /cvsroot/javabdd/buddy/buddy/examples/bddcalc/examples In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25254/buddy/examples/bddcalc/examples Removed Files: c432.cal c1355.cal c3540.cal c499.cal c1908.cal c2670.cal readme Log Message: --- c432.cal DELETED --- --- c3540.cal DELETED --- --- c1908.cal DELETED --- --- readme DELETED --- --- c2670.cal DELETED --- --- c1355.cal DELETED --- --- c499.cal DELETED --- |
Update of /cvsroot/javabdd/buddy/buddy_new/examples/bddcalc/examples In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25254/buddy_new/examples/bddcalc/examples Removed Files: c499.cal c3540.cal c432.cal readme c1908.cal c1355.cal c2670.cal Log Message: --- c432.cal DELETED --- --- c3540.cal DELETED --- --- c1908.cal DELETED --- --- readme DELETED --- --- c2670.cal DELETED --- --- c1355.cal DELETED --- --- c499.cal DELETED --- |
|
From: John W. <joe...@us...> - 2004-09-29 10:04:44
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24980/src Modified Files: prime.h Log Message: Index: prime.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/prime.h,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** prime.h 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- prime.h 29 Sep 2004 10:04:34 -0000 1.2 *************** *** 42,45 **** --- 42,49 ---- unsigned int bdd_prime_lte(unsigned int src); + #ifdef _MSC_VER + #define srand48(x) srand(x) + #define lrand48(x) rand(x) + #endif #endif /* _PRIME_H */ |
|
From: John W. <joe...@us...> - 2004-09-29 10:04:03
|
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24826/src Modified Files: kernel.h Log Message: Index: kernel.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.h,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** kernel.h 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- kernel.h 29 Sep 2004 10:03:50 -0000 1.2 *************** *** 182,185 **** --- 182,191 ---- + #ifdef _MSC_VER + #define srand48(x) srand(x) + #define lrand48(x) rand(x) + #endif + + /*=== KERNEL PROTOTYPES ================================================*/ |
Update of /cvsroot/javabdd/JavaBDD/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24254 Modified Files: bdd.h bddio.c bddop.c fdd.c kernel.c pairs.c reorder.c Added Files: trace.c trace.h Log Message: Index: reorder.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/reorder.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** reorder.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- reorder.c 29 Sep 2004 10:00:50 -0000 1.2 *************** *** 1524,1538 **** int l1, l2; /* Do not swap when variable-blocks are used */ if (vartree != NULL) ! return bdd_error(BDD_VARBLK); /* Don't bother swapping x with x */ if (v1 == v2) ! return 0; /* Make sure the variable exists */ if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum) ! return bdd_error(BDD_VAR); l1 = bddvar2level[v1]; --- 1524,1542 ---- int l1, l2; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v1); + ADD_ARG1(T_INT,v2); + /* Do not swap when variable-blocks are used */ if (vartree != NULL) ! RETURN(bdd_error(BDD_VARBLK)); /* Don't bother swapping x with x */ if (v1 == v2) ! RETURN(0); /* Make sure the variable exists */ if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum) ! RETURN(bdd_error(BDD_VAR)); l1 = bddvar2level[v1]; *************** *** 1561,1565 **** reorder_done(); ! return 0; } --- 1565,1569 ---- reorder_done(); ! RETURN(0); } *************** *** 1598,1602 **** --- 1602,1608 ---- void bdd_disable_reorder(void) { + BUDDY_PROLOGUE; reorderdisabled = 1; + RETURN(); } *************** *** 1612,1616 **** --- 1618,1624 ---- void bdd_enable_reorder(void) { + BUDDY_PROLOGUE; reorderdisabled = 0; + RETURN(); } *************** *** 1804,1807 **** --- 1812,1818 ---- int savemethod = bddreordermethod; int savetimes = bddreordertimes; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,method); bddreordermethod = method; *************** *** 1809,1815 **** if ((top=bddtree_new(-1)) == NULL) ! return; if (reorder_init() < 0) ! return; usednum_before = bddnodesize - bddfreenum; --- 1820,1826 ---- if ((top=bddtree_new(-1)) == NULL) ! RETURN(); if (reorder_init() < 0) ! RETURN(); usednum_before = bddnodesize - bddfreenum; *************** *** 1830,1833 **** --- 1841,1845 ---- bddreordermethod = savemethod; bddreordertimes = savetimes; + RETURN(); } *************** *** 1847,1854 **** int bdd_reorder_gain(void) { if (usednum_before == 0) ! return 0; ! return (100*(usednum_before - usednum_after)) / usednum_before; } --- 1859,1867 ---- int bdd_reorder_gain(void) { + BUDDY_PROLOGUE; if (usednum_before == 0) ! RETURN(0); ! RETURN((100*(usednum_before - usednum_after)) / usednum_before); } *************** *** 1948,1954 **** { int tmp = bddreordermethod; bddreordermethod = method; bddreordertimes = -1; ! return tmp; } --- 1961,1969 ---- { int tmp = bddreordermethod; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,method); bddreordermethod = method; bddreordertimes = -1; ! RETURN(tmp); } *************** *** 1957,1963 **** { int tmp = bddreordermethod; bddreordermethod = method; bddreordertimes = num; ! return tmp; } --- 1972,1981 ---- { int tmp = bddreordermethod; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,method); + ADD_ARG1(T_INT,num); bddreordermethod = method; bddreordertimes = num; ! RETURN(tmp); } *************** *** 1974,1981 **** int bdd_var2level(int var) { if (var < 0 || var >= bddvarnum) ! return bdd_error(BDD_VAR); ! return bddvar2level[var]; } --- 1992,2001 ---- int bdd_var2level(int var) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); if (var < 0 || var >= bddvarnum) ! RETURN(bdd_error(BDD_VAR)); ! RETURN(bddvar2level[var]); } *************** *** 1992,1999 **** int bdd_level2var(int level) { if (level < 0 || level >= bddvarnum) ! return bdd_error(BDD_VAR); ! return bddlevel2var[level]; } --- 2012,2021 ---- int bdd_level2var(int level) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,level); if (level < 0 || level >= bddvarnum) ! RETURN(bdd_error(BDD_VAR)); ! RETURN(bddlevel2var[level]); } *************** *** 2010,2014 **** int bdd_getreorder_times(void) { ! return bddreordertimes; } --- 2032,2037 ---- int bdd_getreorder_times(void) { ! BUDDY_PROLOGUE; ! RETURN(bddreordertimes); } *************** *** 2025,2029 **** int bdd_getreorder_method(void) { ! return bddreordermethod; } --- 2048,2053 ---- int bdd_getreorder_method(void) { ! BUDDY_PROLOGUE; ! RETURN(bddreordermethod); } *************** *** 2045,2050 **** { int tmp = verbose; verbose = v; ! return tmp; } --- 2069,2076 ---- { int tmp = verbose; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v); verbose = v; ! RETURN(tmp); } *************** *** 2078,2084 **** --- 2104,2115 ---- { bddsizehandler old = reorder_nodenum; + BUDDY_IGNOREFN_PROLOGUE; if (handler == NULL) + { + BUDDY_IGNOREFN_EPILOGUE; return reorder_nodenum; + } reorder_nodenum = handler; + BUDDY_IGNOREFN_EPILOGUE; return old; } *************** *** 2096,2102 **** --- 2127,2135 ---- void bdd_clrvarblocks(void) { + BUDDY_PROLOGUE; bddtree_del(vartree); vartree = NULL; blockid = 0; + RETURN(); } *************** *** 2142,2150 **** int n, *v, size; int first, last; if ((n=bdd_scanset(b, &v, &size)) < 0) ! return n; if (size < 1) ! return bdd_error(BDD_VARBLK); first = last = v[0]; --- 2175,2187 ---- int n, *v, size; int first, last; + + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,b); + ADD_ARG1(T_INT,fixed); if ((n=bdd_scanset(b, &v, &size)) < 0) ! RETURN(n); if (size < 1) ! RETURN(bdd_error(BDD_VARBLK)); first = last = v[0]; *************** *** 2159,2166 **** if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) ! return bdd_error(BDD_VARBLK); vartree = t; ! return blockid++; } --- 2196,2203 ---- if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) ! RETURN(bdd_error(BDD_VARBLK)); vartree = t; ! RETURN(blockid++); } *************** *** 2169,2181 **** { BddTree *t; if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum) ! return bdd_error(BDD_VAR); if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) ! return bdd_error(BDD_VARBLK); vartree = t; ! return blockid++; } --- 2206,2222 ---- { BddTree *t; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,first); + ADD_ARG1(T_INT,last); + ADD_ARG1(T_INT,fixed); if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum) ! RETURN(bdd_error(BDD_VAR)); if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL) ! RETURN(bdd_error(BDD_VARBLK)); vartree = t; ! RETURN(blockid++); } *************** *** 2197,2202 **** --- 2238,2246 ---- int n; + BUDDY_PROLOGUE; + for (n=0 ; n<bddvarnum ; n++) bdd_intaddvarblock(n,n,1); + RETURN(); } *************** *** 2230,2234 **** --- 2274,2280 ---- void bdd_printorder(void) { + BUDDY_PROLOGUE; bdd_fprintorder(stdout); + RETURN(); } *************** *** 2252,2260 **** int level; /* Do not set order when variable-blocks are used */ if (vartree != NULL) { bdd_error(BDD_VARBLK); ! return; } --- 2298,2309 ---- int level; + BUDDY_PROLOGUE; + ADD_ARG2(T_INT_PTR,neworder,bddvarnum); + /* Do not set order when variable-blocks are used */ if (vartree != NULL) { bdd_error(BDD_VARBLK); ! RETURN(); } *************** *** 2270,2273 **** --- 2319,2323 ---- reorder_done(); + RETURN(); } Index: bddio.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddio.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** bddio.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- bddio.c 29 Sep 2004 10:00:49 -0000 1.2 *************** *** 119,123 **** --- 119,125 ---- void bdd_printall(void) { + BUDDY_PROLOGUE; bdd_fprintall(stdout); + RETURN(); } *************** *** 163,167 **** --- 165,172 ---- void bdd_printtable(BDD r) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); bdd_fprinttable(stdout, r); + RETURN(); } *************** *** 226,230 **** --- 231,238 ---- void bdd_printset(BDD r) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); bdd_fprintset(stdout, r); + RETURN(); } *************** *** 312,316 **** --- 320,327 ---- void bdd_printdot(BDD r) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); bdd_fprintdot(stdout, r); + RETURN(); } *************** *** 384,393 **** int ok; if ((ofile=fopen(fname,"w")) == NULL) ! return bdd_error(BDD_FILE); ok = bdd_save(ofile, r); fclose(ofile); ! return ok; } --- 395,408 ---- int ok; + BUDDY_PROLOGUE; + ADD_ARG1(T_CHAR_PTR,fname); + ADD_ARG1(T_BDD,r); + if ((ofile=fopen(fname,"w")) == NULL) ! RETURN(bdd_error(BDD_FILE)); ok = bdd_save(ofile, r); fclose(ofile); ! RETURN(ok); } *************** *** 478,487 **** int ok; if ((ifile=fopen(fname,"r")) == NULL) ! return bdd_error(BDD_FILE); ok = bdd_load(ifile, root); fclose(ifile); ! return ok; } --- 493,510 ---- int ok; + BUDDY_PROLOGUE; + ADD_ARG1(T_CHAR_PTR,fname); + if ((ifile=fopen(fname,"r")) == NULL) ! { ! ! ADD_ARG1(T_BDD_LOAD,*root); ! RETURN(bdd_error(BDD_FILE)); ! } ok = bdd_load(ifile, root); + ADD_ARG1(T_BDD_LOAD,*root); fclose(ifile); ! RETURN(ok); } *************** *** 533,541 **** else *root = tmproot; - return 0; } - static int bdd_loaddata(FILE *ifile) { --- 556,562 ---- --- NEW FILE: trace.c --- #ifdef GENERATE_TRACE #include <unistd.h> #include <stdio.h> #include <stdlib.h> #include <assert.h> #include <string.h> #include "bdd.h" #ifndef EXIT_FAILURE #define EXIT_FAILURE -1 #endif /* Simple trace file generation */ FILE * tracefp; const char * trace_fname; #define NR_TABLE (1<<16) #define HASH_MASK ((NR_TABLE)-1) struct bdd_decl { struct bdd_decl * next; union { BDD bval; bddPair * pval; }; int is_pair, is_collected; const char * identifier; }; struct bdd_decl * decltbl[NR_TABLE]; struct bdd_arg { struct bdd_arg * next; enum arg_type type; union { const char * ident; /* T_BDD, T_BDD_PAIR */ struct /* T_BDD_PTR */ { BDD * barr; int blen; }; struct /* T_INT_PTR */ { int * iarr; int len; }; char * str; /* T_CHAR_PTR */ int i; /* T_INT */ }; }; struct bdd_function { struct bdd_function * next, * prev; const char * fn_ident; struct bdd_arg * args; /* NULL if void */ const char * retval; }; struct bdd_function * currfn; struct bdd_function * bddfns; const char * last_id; static unsigned long hash_bdd(BDD b) { return (unsigned long)b & HASH_MASK; } static unsigned long hash_bddpair(bddPair * p) { unsigned long tmp = (unsigned long)p; return tmp & HASH_MASK; } static __inline__ int id_done(const char * id) { const char * pos = id + 4; /* skip _bdd header */ while(*pos == 'z') pos++; if(*pos == '\0') return 1; return 0; } static const char * genid(void) { char * retval; int i,j; if(!last_id) { retval = "_bdda"; } else if(id_done(last_id)) { retval = xmalloc(strlen(last_id) + 2); memcpy(retval,"_bdd",4); memset(retval+4,'a',strlen(last_id)-4 + 1); retval[strlen(last_id)+1] = '\0'; } else { for(i = 4; last_id[i] == 'z' ; i++) ; retval = strdup(last_id); for(j = 4; j < i; j++) retval[j] = 'a'; retval[i]++; } last_id = retval; return retval; } static struct bdd_decl * lookup_bdd(enum arg_type type, void * arg) { struct bdd_decl * d; if(type == T_BDD) { BDD b = (BDD) arg; d = decltbl[hash_bdd(b)]; while(d) { if(!(d->is_pair) && d->bval == b && !d->is_collected) return d; d = d->next; } } else if(type == T_BDD_PAIR) { bddPair * p = (bddPair *) arg; d = decltbl[hash_bddpair(p)]; while(d) { if( d->is_pair && d->pval == p & !d->is_collected) { return d; } d = d->next; } } else assert(0); return NULL; } static const char * lookup_bdd_ident(enum arg_type type, void * arg) { struct bdd_decl * d; if(type == T_BDD) { BDD b = (BDD) arg; if(b == bddtrue) return "bddtrue"; if(b == bddfalse) return "bddfalse"; } d = lookup_bdd(type,arg); if(!d) return NULL; return d->identifier; } void trace_init(const char * filename) { tracefp = fopen(filename,"w"); if(!tracefp) { fprintf(stderr,"Unable to open file %s for tracing\n",filename); exit(EXIT_FAILURE); } atexit(output_trace); memset(decltbl, 0, sizeof(decltbl)); currfn = NULL; bddfns = NULL; } void trace_begin_function(const char * fn) { assert(!currfn); currfn = xmalloc(sizeof(struct bdd_function)); currfn->fn_ident = fn; currfn->retval = NULL; currfn->args = NULL; currfn->next = currfn->prev = currfn; } void trace_end_function(void) { if(bddfns == NULL) bddfns = currfn; else { bddfns->prev->next = currfn; currfn->next = bddfns; currfn->prev = bddfns->prev; bddfns->prev = currfn; } currfn = NULL; } void trace_add_bdd(enum arg_type type, void * retval) { if(!lookup_bdd_ident(type,retval)) { struct bdd_decl * d = xmalloc(sizeof(struct bdd_decl)); d->identifier = genid(); d->is_pair = type == T_BDD_PAIR; d->is_collected = 0; if(type == T_BDD) { BDD b = (BDD) retval; d->bval = b; d->next = decltbl[hash_bdd(b)]; decltbl[hash_bdd(b)] = d; } else { bddPair * p = (bddPair *) retval; if(!p) { printf("ERROR at %s\n",__func__); return; } d->pval = p; d->next = decltbl[hash_bddpair(p)]; decltbl[hash_bddpair(p)] = d; } } } void trace_del_bdd(enum arg_type type, void * arg) { struct bdd_decl * d = lookup_bdd(type,arg); if(d) { if(type == T_BDD_PAIR) printf("removing pair\n"); d->is_collected = 1; } } void * trace_end_function_bdd(enum arg_type type, void * retval) { const char * id; trace_add_bdd(type,retval); id = lookup_bdd_ident(type,retval); assert(id); currfn->retval = id; trace_end_function(); return retval; } void trace_add_arg(enum arg_type type, void * arg1, void * arg2) { struct bdd_arg *a = xmalloc(sizeof(struct bdd_arg)); a->next = NULL; a->type = type; switch(type) { case T_INT: a->i = (int) arg1; break; case T_INT_PTR: a->len = (int) arg2; a->iarr = xmalloc(a->len * sizeof(int)); memcpy(a->iarr,arg1,a->len * sizeof(int)); break; case T_CHAR_PTR: a->str = strdup((char *)arg1); break; case T_BDD: case T_BDD_PAIR: a->ident = lookup_bdd_ident(type,arg1); assert(a->ident); break; case T_BDD_LOAD: { BDD b = (BDD) arg1; trace_add_bdd(T_BDD,(void *)b); a->ident = lookup_bdd_ident(T_BDD,(void *)b); assert(a->ident); break; } case T_BDD_PTR: { int i; a->blen = (int) arg2; a->barr = malloc(sizeof(BDD) * a->blen); memcpy(a->barr,arg1,sizeof(BDD) * a->blen); /* broken code manufactures bdds and then * passes them as aray elements. bleh */ for(i = 0; i < a->blen; i++) { trace_add_bdd(T_BDD,(void *)a->barr[i]); } break; } default: assert(0); } if(currfn->args == NULL) currfn->args = a; else { struct bdd_arg * c = currfn->args; while(c->next) c = c->next; c->next = a; } } static void print_args(struct bdd_arg * args) { struct bdd_arg * a = args; while(a) { switch(a->type) { case T_INT: fprintf(tracefp,"%d",a->i); break; case T_INT_PTR: { int i; fprintf(tracefp,"(int []) { "); for(i = 0; i < a->len; i++) fprintf(tracefp,"%d,", a->iarr[i]); fprintf(tracefp,"}"); break; } case T_CHAR_PTR: fprintf(tracefp,"\"%s\"",a->str); break; case T_BDD: case T_BDD_PAIR: fprintf(tracefp,"%s",a->ident); break; case T_BDD_LOAD: fprintf(tracefp,"&%s",a->ident); break; case T_BDD_PTR: { int i; fprintf(tracefp, "(BDD []) {"); for(i = 0; i < a->blen; i++) { fprintf(tracefp,"%s,", lookup_bdd_ident(T_BDD,(void *)a->barr[i])); } fprintf(tracefp,"}"); break; } default: assert(0); } if(a->next) fprintf(tracefp,","); a = a->next; } } void emit_header(void) { fprintf(tracefp,"#include \"bdd.h\"\n"); fprintf(tracefp,"int main(void)\n{\n"); } void emit_trailer(void) { fprintf(tracefp,"return 0; }\n"); } void output_trace(void) { if(trace_outputted) return; trace_outputted = 1; int i, first = 0; struct bdd_function * f; emit_header(); for(i = 0; i < NR_TABLE; i++) { struct bdd_decl * d = decltbl[i]; while(d) { if(d->is_pair) fprintf(tracefp,"\tbddPair *"); else fprintf(tracefp,"\tBDD "); fprintf(tracefp,"%s;\n",d->identifier); d = d->next; } } f = bddfns; while(f != bddfns || !first) { if(f->retval && strcmp(f->retval,"bddtrue") && strcmp(f->retval,"bddfalse")) fprintf(tracefp,"\n\t%s = ", f->retval); else fprintf(tracefp,"\n\t"); fprintf(tracefp, f->fn_ident); fprintf(tracefp,"("); print_args(f->args); fprintf(tracefp,");"); f = f->next; first = 1; } emit_trailer(); } #endif // GENERATE_TRACE Index: bddop.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** bddop.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- bddop.c 29 Sep 2004 10:00:50 -0000 1.2 *************** *** 122,129 **** --- 122,131 ---- static BDD not_rec(BDD); static BDD apply_rec(BDD, BDD); + static BDD apply_rec0(BDD, BDD); static BDD ite_rec(BDD, BDD, BDD); static int simplify_rec(BDD, BDD); static int quant_rec(int); static int appquant_rec(int, int); + static int appquant_rec0(int, int); static int restrict_rec(int); [...1532 lines suppressed...] { CHECKa(r, 0.0); miscid = CACHEID_PATHCOU; ! return bdd_pathcount_rec(r); } --- 3119,3129 ---- double bdd_pathcount(BDD r) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); CHECKa(r, 0.0); miscid = CACHEID_PATHCOU; ! RETURN(bdd_pathcount_rec(r)); } Index: fdd.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/fdd.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** fdd.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- fdd.c 29 Sep 2004 10:00:50 -0000 1.2 *************** *** 128,133 **** int n, bn, more; if (!bddrunning) ! return bdd_error(BDD_RUNNING); /* Build domain table */ --- 128,137 ---- int n, bn, more; + BUDDY_PROLOGUE; + ADD_ARG2(T_INT_PTR,dom,num); + ADD_ARG1(T_INT,num); + if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); /* Build domain table */ *************** *** 136,140 **** fdvaralloc = num; if ((domain=(Domain*)malloc(sizeof(Domain)*num)) == NULL) ! return bdd_error(BDD_MEMORY); } else /* Allocated before */ --- 140,144 ---- fdvaralloc = num; if ((domain=(Domain*)malloc(sizeof(Domain)*num)) == NULL) ! RETURN(bdd_error(BDD_MEMORY)); } else /* Allocated before */ *************** *** 146,150 **** domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); if (domain == NULL) ! return bdd_error(BDD_MEMORY); } } --- 150,154 ---- domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); if (domain == NULL) ! RETURN(bdd_error(BDD_MEMORY)); } } *************** *** 184,188 **** firstbddvar += extravars; ! return offset; } --- 188,192 ---- firstbddvar += extravars; ! RETURN(offset); } *************** *** 209,218 **** Domain *d; int n; if (!bddrunning) ! return bdd_error(BDD_RUNNING); if (v1 < 0 || v1 >= fdvarnum || v2 < 0 || v2 >= fdvarnum) ! return bdd_error(BDD_VAR); if (fdvarnum + 1 > fdvaralloc) --- 213,226 ---- Domain *d; int n; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v1); + ADD_ARG1(T_INT,v2); if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); if (v1 < 0 || v1 >= fdvarnum || v2 < 0 || v2 >= fdvarnum) ! RETURN(bdd_error(BDD_VAR)); if (fdvarnum + 1 > fdvaralloc) *************** *** 222,226 **** domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); if (domain == NULL) ! return bdd_error(BDD_MEMORY); } --- 230,234 ---- domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc); if (domain == NULL) ! RETURN(bdd_error(BDD_MEMORY)); } *************** *** 238,242 **** bdd_addref(d->var); ! return fdvarnum++; } --- 246,250 ---- bdd_addref(d->var); ! RETURN(fdvarnum++); } *************** *** 252,257 **** --- 260,267 ---- void fdd_clearall(void) { + BUDDY_PROLOGUE; bdd_fdd_done(); bdd_fdd_init(); + RETURN(); } *************** *** 274,281 **** int fdd_domainnum(void) { if (!bddrunning) ! return bdd_error(BDD_RUNNING); ! return fdvarnum; } --- 284,292 ---- int fdd_domainnum(void) { + BUDDY_PROLOGUE; if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); ! RETURN(fdvarnum); } *************** *** 293,302 **** int fdd_domainsize(int v) { if (!bddrunning) ! return bdd_error(BDD_RUNNING); if (v < 0 || v >= fdvarnum) ! return bdd_error(BDD_VAR); ! return domain[v].realsize; } --- 304,315 ---- int fdd_domainsize(int v) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v); if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); if (v < 0 || v >= fdvarnum) ! RETURN(bdd_error(BDD_VAR)); ! RETURN(domain[v].realsize); } *************** *** 314,323 **** int fdd_varnum(int v) { if (!bddrunning) ! return bdd_error(BDD_RUNNING); if (v >= fdvarnum || v < 0) ! return bdd_error(BDD_VAR); ! return domain[v].binsize; } --- 327,339 ---- int fdd_varnum(int v) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v); + if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); if (v >= fdvarnum || v < 0) ! RETURN(bdd_error(BDD_VAR)); ! RETURN(domain[v].binsize); } *************** *** 339,346 **** int *fdd_vars(int v) { if (!bddrunning) { bdd_error(BDD_RUNNING); ! return NULL; } --- 355,365 ---- int *fdd_vars(int v) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,v); + if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN(NULL); } *************** *** 348,355 **** { bdd_error(BDD_VAR); ! return NULL; } ! return domain[v].ivar; } --- 367,374 ---- { bdd_error(BDD_VAR); ! RETURN(NULL); } ! RETURN(domain[v].ivar); } *************** *** 379,387 **** int n; int v=1, tmp; if (!bddrunning) { bdd_error(BDD_RUNNING); ! return bddfalse; } --- 398,410 ---- int n; int v=1, tmp; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); + ADD_ARG1(T_INT,val); if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN_BDD(bddfalse); } *************** *** 389,393 **** { bdd_error(BDD_VAR); ! return bddfalse; } --- 412,416 ---- { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } *************** *** 395,399 **** { bdd_error(BDD_RANGE); ! return bddfalse; } --- 418,422 ---- { bdd_error(BDD_RANGE); ! RETURN_BDD(bddfalse); } *************** *** 412,416 **** } ! return v; } --- 435,439 ---- } ! RETURN_BDD(v); } *************** *** 432,440 **** int res; CHECK(r); if (r == bddfalse) ! return -1; if (var < 0 || var >= fdvarnum) ! return bdd_error(BDD_VAR); allvar = fdd_scanallvar(r); --- 455,467 ---- int res; + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); + ADD_ARG1(T_INT,var); + CHECK(r); if (r == bddfalse) ! RETURN(-1); if (var < 0 || var >= fdvarnum) ! RETURN(bdd_error(BDD_VAR)); allvar = fdd_scanallvar(r); *************** *** 442,446 **** free(allvar); ! return res; } --- 469,473 ---- free(allvar); ! RETURN(res); } *************** *** 466,473 **** int *res; BDD p = r; CHECKa(r,NULL); if (r == bddfalse) ! return NULL; store = NEW(char,bddvarnum); --- 493,503 ---- int *res; BDD p = r; + + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,r); CHECKa(r,NULL); if (r == bddfalse) ! RETURN(NULL); store = NEW(char,bddvarnum); *************** *** 507,511 **** free(store); ! return res; } --- 537,541 ---- free(store); ! RETURN(res); } *************** *** 522,529 **** BDD fdd_ithset(int var) { if (!bddrunning) { bdd_error(BDD_RUNNING); ! return bddfalse; } --- 552,562 ---- BDD fdd_ithset(int var) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); + if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN_BDD(bddfalse); } *************** *** 531,538 **** { bdd_error(BDD_VAR); ! return bddfalse; } ! return domain[var].var; } --- 564,571 ---- { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } ! RETURN_BDD(domain[var].var); } *************** *** 554,562 **** Domain *dom; BDD d; if (!bddrunning) { bdd_error(BDD_RUNNING); ! return bddfalse; } --- 587,598 ---- Domain *dom; BDD d; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN_BDD(bddfalse); } *************** *** 564,568 **** { bdd_error(BDD_VAR); ! return bddfalse; } --- 600,604 ---- { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } *************** *** 589,593 **** } ! return d; } --- 625,629 ---- } ! RETURN_BDD(d); } *************** *** 608,616 **** BDD e = bddtrue, tmp1, tmp2; int n; if (!bddrunning) { bdd_error(BDD_RUNNING); ! return bddfalse; } --- 644,656 ---- BDD e = bddtrue, tmp1, tmp2; int n; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,left); + ADD_ARG1(T_INT,right); if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN_BDD(bddfalse); } *************** *** 618,627 **** { bdd_error(BDD_VAR); ! return bddfalse; } if (domain[left].realsize != domain[right].realsize) { bdd_error(BDD_RANGE); ! return bddfalse; } --- 658,667 ---- { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } if (domain[left].realsize != domain[right].realsize) { bdd_error(BDD_RANGE); ! RETURN_BDD(bddfalse); } *************** *** 639,643 **** bdd_delref(e); ! return e; } --- 679,683 ---- bdd_delref(e); ! RETURN_BDD(e); } *************** *** 893,900 **** int n; if (!bddrunning) { bdd_error(BDD_RUNNING); ! return bddfalse; } --- 933,944 ---- int n; + BUDDY_PROLOGUE; + ADD_ARG2(T_INT_PTR,varset,varnum); + ADD_ARG1(T_INT,varnum); + if (!bddrunning) { bdd_error(BDD_RUNNING); ! RETURN_BDD(bddfalse); } *************** *** 903,907 **** { bdd_error(BDD_VAR); ! return bddfalse; } --- 947,951 ---- { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } *************** *** 914,918 **** } ! return res; } --- 958,962 ---- } ! RETURN_BDD(res); } *************** *** 933,942 **** bdd res = bddtrue, tmp; int n, err; if (!bddrunning) ! return bdd_error(BDD_RUNNING); if (first > last || first < 0 || last >= fdvarnum) ! return bdd_error(BDD_VARBLK); for (n=first ; n<=last ; n++) --- 977,991 ---- bdd res = bddtrue, tmp; int n, err; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,first); + ADD_ARG1(T_INT,last); + ADD_ARG1(T_INT,fixed); if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); if (first > last || first < 0 || last >= fdvarnum) ! RETURN(bdd_error(BDD_VARBLK)); for (n=first ; n<=last ; n++) *************** *** 951,955 **** bdd_delref(res); ! return err; } --- 1000,1004 ---- bdd_delref(res); ! RETURN(err); } *************** *** 971,988 **** int n,e; if (!bddrunning) ! return bdd_error(BDD_RUNNING); if (p1<0 || p1>=fdvarnum || p2<0 || p2>=fdvarnum) ! return bdd_error(BDD_VAR); if (domain[p1].binsize != domain[p2].binsize) ! return bdd_error(BDD_VARNUM); for (n=0 ; n<domain[p1].binsize ; n++) if ((e=bdd_setpair(pair, domain[p1].ivar[n], domain[p2].ivar[n])) < 0) ! return e; ! return 0; } --- 1020,1042 ---- int n,e; + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,pair); + ADD_ARG1(T_INT,p1); + ADD_ARG1(T_INT,p2); + if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); if (p1<0 || p1>=fdvarnum || p2<0 || p2>=fdvarnum) ! RETURN(bdd_error(BDD_VAR)); if (domain[p1].binsize != domain[p2].binsize) ! RETURN(bdd_error(BDD_VARNUM)); for (n=0 ; n<domain[p1].binsize ; n++) if ((e=bdd_setpair(pair, domain[p1].ivar[n], domain[p2].ivar[n])) < 0) ! RETURN(e); ! RETURN(0); } *************** *** 1005,1020 **** int n,e; if (!bddrunning) ! return bdd_error(BDD_RUNNING); for (n=0 ; n<size ; n++) if (p1[n]<0 || p1[n]>=fdvarnum || p2[n]<0 || p2[n]>=fdvarnum) ! return bdd_error(BDD_VAR); for (n=0 ; n<size ; n++) if ((e=fdd_setpair(pair, p1[n], p2[n])) < 0) ! return e; ! return 0; } --- 1059,1080 ---- int n,e; + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,pair); + ADD_ARG2(T_INT_PTR,p1,size); + ADD_ARG2(T_INT_PTR,p2,size); + ADD_ARG1(T_INT,size); + if (!bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); for (n=0 ; n<size ; n++) if (p1[n]<0 || p1[n]>=fdvarnum || p2[n]<0 || p2[n]>=fdvarnum) ! RETURN(bdd_error(BDD_VAR)); for (n=0 ; n<size ; n++) if ((e=fdd_setpair(pair, p1[n], p2[n])) < 0) ! RETURN(e); ! RETURN(0); } Index: pairs.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/pairs.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** pairs.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- pairs.c 29 Sep 2004 10:00:50 -0000 1.2 *************** *** 148,156 **** int n; bddPair *p; if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL) { bdd_error(BDD_MEMORY); ! return NULL; } --- 148,158 ---- int n; bddPair *p; + + BUDDY_PROLOGUE; if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL) { bdd_error(BDD_MEMORY); ! RETURN_BDD_PAIR(NULL); } *************** *** 159,163 **** free(p); bdd_error(BDD_MEMORY); ! return NULL; } --- 161,165 ---- free(p); bdd_error(BDD_MEMORY); ! RETURN_BDD_PAIR(NULL); } *************** *** 169,173 **** bdd_register_pair(p); ! return p; } --- 171,175 ---- bdd_register_pair(p); ! RETURN_BDD_PAIR(p); } *************** *** 196,206 **** int bdd_setpair(bddPair *pair, int oldvar, int newvar) { if (pair == NULL) return 0; if (oldvar < 0 || oldvar > bddvarnum-1) ! return bdd_error(BDD_VAR); if (newvar < 0 || newvar > bddvarnum-1) ! return bdd_error(BDD_VAR); bdd_delref( pair->result[bddvar2level[oldvar]] ); --- 198,213 ---- int bdd_setpair(bddPair *pair, int oldvar, int newvar) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,pair); + ADD_ARG1(T_INT,oldvar); + ADD_ARG1(T_INT,newvar); + if (pair == NULL) return 0; if (oldvar < 0 || oldvar > bddvarnum-1) ! RETURN(bdd_error(BDD_VAR)); if (newvar < 0 || newvar > bddvarnum-1) ! RETURN(bdd_error(BDD_VAR)); bdd_delref( pair->result[bddvar2level[oldvar]] ); *************** *** 211,215 **** pair->last = bddvar2level[oldvar]; ! return 0; } --- 218,222 ---- pair->last = bddvar2level[oldvar]; ! RETURN(0); } *************** *** 218,228 **** { int oldlevel; if (pair == NULL) ! return 0; CHECK(newvar); if (oldvar < 0 || oldvar >= bddvarnum) ! return bdd_error(BDD_VAR); oldlevel = bddvar2level[oldvar]; --- 225,240 ---- { int oldlevel; + + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,pair); + ADD_ARG1(T_INT, oldvar); + ADD_ARG1(T_BDD,newvar); if (pair == NULL) ! RETURN(0); CHECK(newvar); if (oldvar < 0 || oldvar >= bddvarnum) ! RETURN(bdd_error(BDD_VAR)); oldlevel = bddvar2level[oldvar]; *************** *** 234,238 **** pair->last = oldlevel; ! return 0; } --- 246,250 ---- pair->last = oldlevel; ! RETURN(0); } *************** *** 253,258 **** { int n,e; if (pair == NULL) ! return 0; for (n=0 ; n<size ; n++) --- 265,277 ---- { int n,e; + + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,pair); + ADD_ARG2(T_INT_PTR,oldvar,size); + ADD_ARG2(T_INT_PTR,newvar,size); + ADD_ARG1(T_INT,size); + if (pair == NULL) ! RETURN(0); for (n=0 ; n<size ; n++) *************** *** 260,264 **** return e; ! return 0; } --- 279,283 ---- return e; ! RETURN(0); } *************** *** 290,296 **** { int n; if (p == NULL) ! return; if (pairs != p) --- 309,318 ---- { int n; + + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,p); if (p == NULL) ! RETURN(); if (pairs != p) *************** *** 306,313 **** --- 328,337 ---- pairs = p->next; + trace_del_bdd(T_BDD_PAIR,p); for (n=0 ; n<bddvarnum ; n++) bdd_delref( p->result[n] ); free(p->result); free(p); + RETURN(); } *************** *** 326,332 **** --- 350,360 ---- int n; + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD_PAIR,p); + for (n=0 ; n<bddvarnum ; n++) p->result[n] = bdd_ithvar(n); p->last = 0; + RETURN(); } Index: kernel.c =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** kernel.c 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- kernel.c 29 Sep 2004 10:00:50 -0000 1.2 *************** *** 104,107 **** --- 104,111 ---- bddCacheStat bddcachestats; + int trace_enable = 0; /* Flag indicating whether to trace lib calls */ + int trace_outputted = 0; /* Flag indicating whether the trace file + * has been outputted yet + */ *************** *** 117,120 **** --- 121,127 ---- static bdd2inthandler resize_handler; /* Node-table-resize handler */ + /* Pre-allocate node table */ + static int MAX_ALLOC_NODES = 100000000; + static BddNode* alloced; /* Strings for all error mesages */ *************** *** 175,188 **** { int n, err; srand48( SRAND48SEED ) ; if (bddrunning) ! return bdd_error(BDD_RUNNING); bddnodesize = bdd_prime_gte(initnodesize); ! if ((bddnodes=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) ! return bdd_error(BDD_MEMORY); bddresized = 0; --- 182,215 ---- { int n, err; + char * str; + + + /* Check to see if tracing is enabled */ + + if( (str = getenv("BUDDY_TRACE_FILE")) != NULL) + { + trace_enable = 1; + trace_init(str); + } + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,initnodesize); + ADD_ARG1(T_INT,cs); srand48( SRAND48SEED ) ; if (bddrunning) ! RETURN(bdd_error(BDD_RUNNING)); bddnodesize = bdd_prime_gte(initnodesize); ! if ((MAX_ALLOC_NODES == 0) || ! (alloced=(BddNode*)malloc(sizeof(BddNode)*MAX_ALLOC_NODES)) == NULL) { ! if ((alloced=(BddNode*)malloc(sizeof(BddNode)*bddnodesize)) == NULL) { ! RETURN(bdd_error(BDD_MEMORY)); ! } ! MAX_ALLOC_NODES = bddnodesize; ! } ! bddnodes = alloced; bddresized = 0; *************** *** 205,209 **** { bdd_done(); ! return err; } --- 232,236 ---- { bdd_done(); ! RETURN(err); } *************** *** 238,242 **** assert(0); ! return 0; } --- 265,269 ---- assert(0); ! RETURN(0); } *************** *** 254,257 **** --- 281,289 ---- { /*sanitycheck(); FIXME */ + + + if(trace_enable) + output_trace(); + bdd_fdd_done(); bdd_reorder_done(); *************** *** 301,304 **** --- 333,339 ---- int oldbddvarnum = bddvarnum; + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,num); + bdd_disable_reorder(); *************** *** 306,325 **** { bdd_error(BDD_RANGE); ! return bddfalse; } if (num < bddvarnum) ! return bdd_error(BDD_DECVNUM); if (num == bddvarnum) ! return 0; if (bddvarset == NULL) { if ((bddvarset=(BDD*)malloc(sizeof(BDD)*num*2)) == NULL) ! return bdd_error(BDD_MEMORY); if ((bddlevel2var=(int*)malloc(sizeof(int)*(num+1))) == NULL) { free(bddvarset); ! return bdd_error(BDD_MEMORY); } if ((bddvar2level=(int*)malloc(sizeof(int)*(num+1))) == NULL) --- 341,360 ---- { bdd_error(BDD_RANGE); ! RETURN(bddfalse); } if (num < bddvarnum) ! RETURN(bdd_error(BDD_DECVNUM)); if (num == bddvarnum) ! RETURN(0); if (bddvarset == NULL) { if ((bddvarset=(BDD*)malloc(sizeof(BDD)*num*2)) == NULL) ! RETURN(bdd_error(BDD_MEMORY)); if ((bddlevel2var=(int*)malloc(sizeof(int)*(num+1))) == NULL) { free(bddvarset); ! RETURN(bdd_error(BDD_MEMORY)); } if ((bddvar2level=(int*)malloc(sizeof(int)*(num+1))) == NULL) *************** *** 327,331 **** free(bddvarset); free(bddlevel2var); ! return bdd_error(BDD_MEMORY); } } --- 362,366 ---- free(bddvarset); free(bddlevel2var); ! RETURN(bdd_error(BDD_MEMORY)); } } *************** *** 333,341 **** { if ((bddvarset=(BDD*)realloc(bddvarset,sizeof(BDD)*num*2)) == NULL) ! return bdd_error(BDD_MEMORY); if ((bddlevel2var=(int*)realloc(bddlevel2var,sizeof(int)*(num+1))) == NULL) { free(bddvarset); ! return bdd_error(BDD_MEMORY); } if ((bddvar2level=(int*)realloc(bddvar2level,sizeof(int)*(num+1))) == NULL) --- 368,376 ---- { if ((bddvarset=(BDD*)realloc(bddvarset,sizeof(BDD)*num*2)) == NULL) ! RETURN(bdd_error(BDD_MEMORY)); if ((bddlevel2var=(int*)realloc(bddlevel2var,sizeof(int)*(num+1))) == NULL) { free(bddvarset); ! RETURN(bdd_error(BDD_MEMORY)); } if ((bddvar2level=(int*)realloc(bddvar2level,sizeof(int)*(num+1))) == NULL) *************** *** 343,347 **** free(bddvarset); free(bddlevel2var); ! return bdd_error(BDD_MEMORY); } } --- 378,382 ---- free(bddvarset); free(bddlevel2var); ! RETURN(bdd_error(BDD_MEMORY)); } } *************** *** 360,364 **** { bddvarnum = bdv; ! return -bdderrorcond; } --- 395,399 ---- { bddvarnum = bdv; ! RETURN(-bdderrorcond); } *************** *** 376,383 **** bdd_pairs_resize(oldbddvarnum, bddvarnum); bdd_operator_varresize(); ! bdd_enable_reorder(); ! ! return 0; } --- 411,418 ---- bdd_pairs_resize(oldbddvarnum, bddvarnum); bdd_operator_varresize(); ! bdd_enable_reorder(); ! ! RETURN(0); } *************** *** 396,405 **** { int start = bddvarnum; if (num < 0 || num > 0x3FFFFFFF) ! return bdd_error(BDD_RANGE); bdd_setvarnum(bddvarnum+num); ! return start; } --- 431,443 ---- { int start = bddvarnum; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,num); if (num < 0 || num > 0x3FFFFFFF) ! RETURN(bdd_error(BDD_RANGE)); bdd_setvarnum(bddvarnum+num); ! RETURN(start); } *************** *** 435,439 **** --- 473,479 ---- { bddinthandler tmp = err_handler; + BUDDY_IGNOREFN_PROLOGUE; err_handler = handler; + BUDDY_IGNOREFN_EPILOGUE; return tmp; } *************** *** 457,462 **** --- 497,504 ---- void bdd_clear_error(void) { + BUDDY_PROLOGUE; bdderrorcond = 0; bdd_operator_reset(); + RETURN(); } *************** *** 546,555 **** { int old = bddmaxnodeincrease; if (size < 0) ! return bdd_error(BDD_SIZE); bddmaxnodeincrease = size; ! return old; } --- 588,600 ---- { int old = bddmaxnodeincrease; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,size); if (size < 0) ! RETURN(bdd_error(BDD_SIZE)); bddmaxnodeincrease = size; ! RETURN(old); } *************** *** 573,584 **** int bdd_setmaxnodenum(int size) { if (size > bddnodesize || size == 0) { int old = bddmaxnodesize; bddmaxnodesize = size; ! return old; } ! return bdd_error(BDD_NODES); } --- 618,632 ---- int bdd_setmaxnodenum(int size) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,size); + if (size > bddnodesize || size == 0) { int old = bddmaxnodesize; bddmaxnodesize = size; ! RETURN(old); } ! RETURN(bdd_error(BDD_NODES)); } *************** *** 605,614 **** { int old = minfreenodes; if (mf<0 || mf>100) ! return bdd_error(BDD_RANGE); minfreenodes = mf; ! return old; } --- 653,665 ---- { int old = minfreenodes; + + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,mf); if (mf<0 || mf>100) ! RETURN(bdd_error(BDD_RANGE)); minfreenodes = mf; ! RETURN(old); } *************** *** 628,632 **** int bdd_getnodenum(void) { ! return bddnodesize - bddfreenum; } --- 679,684 ---- int bdd_getnodenum(void) { ! BUDDY_PROLOGUE; ! RETURN(bddnodesize - bddfreenum); } *************** *** 644,648 **** int bdd_getallocnum(void) { ! return bddnodesize; } --- 696,701 ---- int bdd_getallocnum(void) { ! BUDDY_PROLOGUE; ! RETURN(bddnodesize); } *************** *** 660,666 **** int bdd_isrunning(void) { ! return bddrunning; } /* --- 713,726 ---- int bdd_isrunning(void) { ! BUDDY_PROLOGUE; ! RETURN(bddrunning); } + #ifndef VERSION + #define VERSION (MAJOR_VERSION*10+MINOR_VERSION) + #endif + #ifndef PACKAGE_VERSION + #define PACKAGE_VERSION "VERSION" + #endif /* *************** *** 676,680 **** { static char str[] = "BuDDy - release " PACKAGE_VERSION; ! return str; } --- 736,741 ---- { static char str[] = "BuDDy - release " PACKAGE_VERSION; ! BUDDY_PROLOGUE; ! RETURN(str); } *************** *** 691,695 **** int bdd_versionnum(void) { ! return MAJOR_VERSION * 10 + MINOR_VERSION; } --- 752,757 ---- int bdd_versionnum(void) { ! BUDDY_PROLOGUE; ! RETURN(MAJOR_VERSION * 10 + MINOR_VERSION); } *************** *** 778,782 **** --- 840,846 ---- void bdd_printstat(void) { + BUDDY_PROLOGUE; bdd_fprintstat(stdout); + RETURN(); } *************** *** 798,805 **** const char *bdd_errstring(int e) { e = abs(e); if (e<1 || e>BDD_ERRNUM) ! return NULL; ! return errorstrings[e-1]; } --- 862,872 ---- const char *bdd_errstring(int e) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,e); + e = abs(e); if (e<1 || e>BDD_ERRNUM) ! RETURN(NULL); ! RETURN(errorstrings[e-1]); } *************** *** 814,821 **** int bdd_error(int e) { if (err_handler != NULL) err_handler(e); ! return e; } --- 881,889 ---- int bdd_error(int e) { + BUDDY_PROLOGUE; if (err_handler != NULL) err_handler(e); ! RETURN(e); } *************** *** 838,842 **** BDD bdd_true(void) { ! return 1; } --- 906,911 ---- BDD bdd_true(void) { ! BUDDY_PROLOGUE; ! RETURN_BDD(1); } *************** *** 855,859 **** BDD bdd_false(void) { ! return 0; } --- 924,929 ---- BDD bdd_false(void) { ! BUDDY_PROLOGUE; ! RETURN_BDD(0); } *************** *** 878,888 **** BDD bdd_ithvar(int var) { if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); ! return bddfalse; } ! return bddvarset[var*2]; } --- 948,960 ---- BDD bdd_ithvar(int var) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } ! RETURN_BDD(bddvarset[var*2]); } *************** *** 904,914 **** BDD bdd_nithvar(int var) { if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); ! return bddfalse; } ! return bddvarset[var*2+1]; } --- 976,988 ---- BDD bdd_nithvar(int var) { + BUDDY_PROLOGUE; + ADD_ARG1(T_INT,var); if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); ! RETURN_BDD(bddfalse); } ! RETURN_BDD(bddvarset[var*2+1]); } *************** *** 926,930 **** int bdd_varnum(void) { ! return bddvarnum; } --- 1000,1005 ---- int bdd_varnum(void) { ! BUDDY_PROLOGUE; ! RETURN(bddvarnum); } *************** *** 940,948 **** int bdd_var(BDD root) { CHECK(root); if (root < 2) ! return bdd_error(BDD_ILLBDD); ! return (bddlevel2var[LEVEL(root)]); } --- 1015,1026 ---- int bdd_var(BDD root) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,root); + CHECK(root); if (root < 2) ! RETURN(bdd_error(BDD_ILLBDD)); ! RETURN(bddlevel2var[LEVEL(root)]); } *************** *** 959,967 **** BDD bdd_low(BDD root) { CHECK(root); if (root < 2) ! return bdd_error(BDD_ILLBDD); ! return (LOW(root)); } --- 1037,1048 ---- BDD bdd_low(BDD root) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,root); + CHECK(root); if (root < 2) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); ! RETURN_BDD(LOW(root)); } *************** *** 978,986 **** BDD bdd_high(BDD root) { CHECK(root); if (root < 2) ! return bdd_error(BDD_ILLBDD); ! return (HIGH(root)); } --- 1059,1070 ---- BDD bdd_high(BDD root) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,root); + CHECK(root); if (root < 2) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); ! RETURN_BDD(HIGH(root)); } *************** *** 1118,1130 **** BDD bdd_addref(BDD root) { if (root < 2 || !bddrunning) ! return root; if (root >= bddnodesize) ! return bdd_error(BDD_ILLBDD); if (LOW(root) == -1) ! return bdd_error(BDD_ILLBDD); INCREF(root); ! return root; } --- 1202,1217 ---- BDD bdd_addref(BDD root) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,root); + if (root < 2 || !bddrunning) ! RETURN_BDD(root); if (root >= bddnodesize) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); if (LOW(root) == -1) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); INCREF(root); ! RETURN_BDD(root); } *************** *** 1144,1159 **** BDD bdd_delref(BDD root) { if (root < 2 || !bddrunning) ! return root; if (root >= bddnodesize) ! return bdd_error(BDD_ILLBDD); if (LOW(root) == -1) ! return bdd_error(BDD_ILLBDD); /* if the following line is present, fails there much earlier */ ! if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */ DECREF(root); ! return root; } --- 1231,1251 ---- BDD bdd_delref(BDD root) { + BUDDY_PROLOGUE; + ADD_ARG1(T_BDD,root); if (root < 2 || !bddrunning) ! RETURN_BDD(root); if (root >= bddnodesize) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); if (LOW(root) == -1) ! RETURN_BDD(bdd_error(BDD_ILLBDD)); /* if the following line is present, fails there much earlier */ ! if (!HASREF(root)) ! bdd_error(BDD_BREAK); /* distinctive */ DECREF(root); ! if(!HASREF(root)) ! trace_del_bdd(T_BDD,(void *)root); ! RETURN_BDD(root); } *************** *** 1370,1377 **** resize_handler(oldsize, bddnodesize); ! newnodes = (BddNode*)realloc(bddnodes, sizeof(BddNode)*bddnodesize); ! if (newnodes == NULL) ! return bdd_error(BDD_MEMORY); ! bddnodes = newnodes; if (doRehash) --- 1462,1474 ---- resize_handler(oldsize, bddnodesize); ! if (bddnodesize > MAX_ALLOC_NODES) { ! alloced = (BddNode*)realloc(alloced, sizeof(BddNode)*bddnodesize); ! if (alloced == NULL) ! return bdd_error(BDD_MEMORY); ! bddnodes = alloced; ! MAX_ALLOC_NODES = bddnodesize; ! } else { ! bddnodes = alloced; ! } if (doRehash) *************** *** 1480,1483 **** --- 1577,1584 ---- { int v, res=1; + + BUDDY_PROLOGUE; + ADD_ARG2(T_INT_PTR,varset,varnum); + ADD_ARG1(T_INT,varnum); for (v=varnum-1 ; v>=0 ; v--) *************** *** 1490,1494 **** } ! return res; } --- 1591,1595 ---- } ! RETURN_BDD(res); } --- NEW FILE: trace.h --- #include <stdlib.h> #include <assert.h> #ifdef GENERATE_TRACE #define BUDDY_PROLOGUE \ int was_enabled = trace_enable; \ if(was_enabled) \ trace_begin_function(__func__); \ trace_enable=0 #define BUDDY_IGNOREFN_PROLOGUE int was_enabled = trace_enable;trace_enable = 0 #define BUDDY_IGNOREFN_EPILOGUE trace_enable = was_enabled #define ADD_ARG1(type,expr) if(was_enabled) trace_add_arg(type,(void *)expr, NULL) #define ADD_ARG2(type,expr1,expr2) if(was_enabled) trace_add_arg(type,(void *)expr1, (void *)expr2) #define RETURN_BDD(expr) \ if(was_enabled) \ { \ trace_enable = 1; \ return (BDD) trace_end_function_bdd(T_BDD,(void *)expr); \ } else return expr; #define RETURN_BDD_PAIR(expr) \ if(was_enabled) \ { \ trace_enable = 1; \ return (bddPair *) trace_end_function_bdd(T_BDD_PAIR,(void *)expr); \ } else return expr; #define RETURN(expr) \ do \ { \ if(was_enabled) \ {\ trace_enable = 1; \ trace_end_function(); \ } \ return expr; \ } while(0) enum arg_type { T_INT, T_INT_PTR, T_CHAR_PTR, T_BDD, T_BDD_PTR, T_BDD_LOAD, T_BDD_PAIR }; static __inline__ void * xmalloc(int sz) { void * retval = malloc(sz); assert(retval); return retval; } void trace_init(const char *filename); void trace_add_bdd(enum arg_type type,void * val); void trace_del_bdd(enum arg_type type, void * val); void trace_begin_function(const char * fn); void trace_end_function(void); void * trace_end_function_bdd(enum arg_type type, void * arg); void trace_add_arg(enum arg_type type, void * arg1, void * arg2); void output_trace(void); extern int trace_enable; extern int trace_outputted; #else // GENERATE_TRACE #define BUDDY_PROLOGUE do { } while (0); #define BUDDY_IGNOREFN_PROLOGUE do { } while (0); #define BUDDY_IGNOREFN_EPILOGUE do { } while (0); #define ADD_ARG1(type,expr) do { } while (0); #define ADD_ARG2(type,expr1,expr2) do { } while (0); #define RETURN_BDD(expr) do { return expr; } while (0); #define RETURN_BDD_PAIR(expr) do { return expr; } while (0); #define RETURN(expr) do { return expr; } while (0); #define trace_init(filename) do { } while (0); #define trace_del_bdd(type,val) do { } while (0); #define output_trace() do { } while (0); #endif // !GENERATE_TRACE Index: bdd.h =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bdd.h,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -C2 -d -r1.1.1.1 -r1.2 *** bdd.h 29 Sep 2004 09:50:25 -0000 1.1.1.1 --- bdd.h 29 Sep 2004 10:00:49 -0000 1.2 *************** *** 81,85 **** } bddPair; - /*=== Status information ===============================================*/ --- 81,84 ---- *************** *** 412,415 **** --- 411,416 ---- #define BDD_ERRNUM 24 + #include "trace.h" + /************************************************************************* If this file is included from a C++ compiler then the following *************** *** 823,826 **** --- 824,829 ---- extern bdd_ioformat fddset; + extern int trace_enable; + typedef void (*bddstrmhandler)(std::ostream &, int); |
|
From: John W. <joe...@us...> - 2004-09-29 06:23:41
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20196/org/sf/javabdd Modified Files: TryVarOrder.java Log Message: Make it Java 1.4 compatible. Index: TryVarOrder.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TryVarOrder.java,v retrieving revision 1.1 retrieving revision 1.2 diff -C2 -d -r1.1 -r1.2 *** TryVarOrder.java 21 Sep 2004 22:32:13 -0000 1.1 --- TryVarOrder.java 29 Sep 2004 06:23:30 -0000 1.2 *************** *** 42,48 **** Class c = cl.loadClass("org.sf.javabdd.BDDFactory"); Method m = c.getMethod("init", new Class[] { String.class, int.class, int.class }); ! bdd = m.invoke(null, new Object[] { s, Integer.valueOf(nodeTableSize), Integer.valueOf(cacheSize) }); m = c.getMethod("setMaxIncrease", new Class[] { int.class }); ! m.invoke(bdd, new Object[] { Integer.valueOf(maxIncrease) }); BufferedReader in = null; --- 42,48 ---- Class c = cl.loadClass("org.sf.javabdd.BDDFactory"); Method m = c.getMethod("init", new Class[] { String.class, int.class, int.class }); ! bdd = m.invoke(null, new Object[] { s, new Integer(nodeTableSize), new Integer(cacheSize) }); m = c.getMethod("setMaxIncrease", new Class[] { int.class }); ! m.invoke(bdd, new Object[] { new Integer(maxIncrease) }); BufferedReader in = null; *************** *** 113,117 **** bddoperation = c.newInstance(null); Method m = bddop_class.getMethod("setOp", new Class[] { int.class }); ! m.invoke(bddoperation, new Object[] { Integer.valueOf(op.id) }); m = bddop_class.getMethod("setFilenames", new Class[] { String.class, String.class, String.class }); m.invoke(bddoperation, new Object[] { filename1, filename2, filename3 }); --- 113,117 ---- bddoperation = c.newInstance(null); Method m = bddop_class.getMethod("setOp", new Class[] { int.class }); ! m.invoke(bddoperation, new Object[] { new Integer(op.id) }); m = bddop_class.getMethod("setFilenames", new Class[] { String.class, String.class, String.class }); m.invoke(bddoperation, new Object[] { filename1, filename2, filename3 }); |
|
From: John W. <joe...@us...> - 2004-09-21 22:32:23
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv10385/org/sf/javabdd Added Files: TryVarOrder.java Log Message: Try var order, now uses new class loader. --- NEW FILE: TryVarOrder.java --- // TryVarOrder.java, created Apr 2, 2004 10:43:21 PM 2004 by jwhaley // Copyright (C) 2004 John Whaley <jw...@al...> // Licensed under the terms of the GNU LGPL; see COPYING for details. package org.sf.javabdd; import java.util.StringTokenizer; import java.io.BufferedReader; import java.io.BufferedWriter; import java.io.File; import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; import java.lang.reflect.Constructor; import java.lang.reflect.Method; import java.math.BigInteger; /** * TryVarOrder * * @author jwhaley * @version $Id: TryVarOrder.java,v 1.1 2004/09/21 22:32:13 joewhaley Exp $ */ public class TryVarOrder { /** BDD Factory, reused if possible. */ static Object bdd = null; static ClassLoader makeClassLoader() { return HijackingClassLoader.makeClassLoader(); } /** * Initialize the named BDD factory under a new class loader. * * @param s BDD factory to initialize */ void initBDDFactory(String s) { try { ClassLoader cl; if (bddoperation != null) cl = bddoperation.getClass().getClassLoader(); else cl = makeClassLoader(); Class c = cl.loadClass("org.sf.javabdd.BDDFactory"); Method m = c.getMethod("init", new Class[] { String.class, int.class, int.class }); bdd = m.invoke(null, new Object[] { s, Integer.valueOf(nodeTableSize), Integer.valueOf(cacheSize) }); m = c.getMethod("setMaxIncrease", new Class[] { int.class }); m.invoke(bdd, new Object[] { Integer.valueOf(maxIncrease) }); BufferedReader in = null; try { in = new BufferedReader(new FileReader(filename0)); for (;;) { String s2 = in.readLine(); if (s2 == null || s2.equals("")) break; StringTokenizer st = new StringTokenizer(s2); String name = st.nextToken(); long size = Long.parseLong(st.nextToken())-1; makeDomain(c, name, BigInteger.valueOf(size).bitLength()); } } catch (IOException x) { } finally { if (in != null) try { in.close(); } catch (IOException _) { } } } catch (Exception x) { System.err.println("Exception occurred while initializing BDD factory: "+x.getLocalizedMessage()); x.printStackTrace(); } } /** * Destroy the BDD factory. */ void destroyBDDFactory() { if (bdd != null) { Class c = bdd.getClass(); try { Method m = c.getMethod("done", new Class[] { }); m.invoke(bdd, new Object[] { }); } catch (Exception x) { System.err.println("Exception occurred while destroying BDD factory: "+x.getLocalizedMessage()); x.printStackTrace(); } bdd = null; } } /** * Make a domain in the BDD factory. * * @param c BDD factory class * @param name name of domain * @param bits bits in domain * @throws Exception */ static void makeDomain(Class c, String name, int bits) throws Exception { Method m = c.getMethod("extDomain", new Class[] { long[].class }); Object[] ds = (Object[]) m.invoke(null, new Object[] { new long[] { 1L << bits } }); c = c.getClassLoader().loadClass("org.sf.javabdd.BDDDomain"); m = c.getMethod("setName", new Class[] { String.class }); m.invoke(ds[0], new Object[] { name }); } Object bddoperation = null; void initBDDOperation() throws Exception { ClassLoader cl; if (bdd != null) { cl = bdd.getClass().getClassLoader(); } else { cl = makeClassLoader(); } Class bddop_class = cl.loadClass("org.sf.javabdd.TryVarOrder$BDDOperation"); Constructor c = bddop_class.getConstructor(new Class[0]); bddoperation = c.newInstance(null); Method m = bddop_class.getMethod("setOp", new Class[] { int.class }); m.invoke(bddoperation, new Object[] { Integer.valueOf(op.id) }); m = bddop_class.getMethod("setFilenames", new Class[] { String.class, String.class, String.class }); m.invoke(bddoperation, new Object[] { filename1, filename2, filename3 }); } void setVarOrder(boolean reverse, String varOrderToTry) throws Exception { Class bddop_class = bddoperation.getClass(); Method m = bddop_class.getMethod("setVarOrder", new Class[] { boolean.class, String.class }); m.invoke(bddoperation, new Object[] { Boolean.valueOf(reverse), varOrderToTry }); } void load() throws Exception { Class bddop_class = bddoperation.getClass(); Method m = bddop_class.getMethod("load", new Class[] { }); m.invoke(bddoperation, new Object[] { }); } long doIt() throws Exception { Class bddop_class = bddoperation.getClass(); Method m = bddop_class.getMethod("doIt", new Class[] { }); Long result = (Long) m.invoke(bddoperation, new Object[] { }); return result.longValue(); } void free() throws Exception { Class bddop_class = bddoperation.getClass(); Method m = bddop_class.getMethod("free", new Class[] { }); m.invoke(bddoperation, new Object[] { }); } public static class BDDOperation { public BDDOperation() { } public BDDOperation(int op, String f1, String f2, String f3) { setOp(op); setFilenames(f1, f2, f3); } public void setOp(int op) { switch (op) { case 0: this.op = BDDFactory.and; break; case 1: this.op = BDDFactory.xor; break; case 2: this.op = BDDFactory.or; break; case 3: this.op = BDDFactory.nand; break; case 4: this.op = BDDFactory.nor; break; case 5: this.op = BDDFactory.imp; break; case 6: this.op = BDDFactory.biimp; break; case 7: this.op = BDDFactory.diff; break; case 8: this.op = BDDFactory.less; break; case 9: this.op = BDDFactory.invimp; break; default: throw new InternalError("Invalid op: "+op); } } public void setFilenames(String f1, String f2, String f3) { this.filename1 = f1; this.filename2 = f2; this.filename3 = f3; } /** Operation for applyEx. */ BDDFactory.BDDOp op; /** Filenames for inputs. */ String filename1; String filename2; String filename3; /** Inputs to applyEx. */ BDD b1 = null; BDD b2 = null; BDD b3 = null; public void setVarOrder(boolean reverse, String varOrderToTry) { BDDFactory f = (BDDFactory) bdd; int[] varorder = f.makeVarOrdering(reverse, varOrderToTry); f.setVarOrder(varorder); } public void load() throws IOException { BDDFactory f = (BDDFactory) bdd; if (b1 == null) { b1 = f.load(filename1); b2 = f.load(filename2); b3 = f.load(filename3); } } public long doIt() { long t = System.currentTimeMillis(); BDD result = b1.applyEx(b2, op, b3); long time = System.currentTimeMillis() - t; result.free(); return time; } public void free() { b1.free(); b1 = null; b2.free(); b2 = null; b3.free(); b3 = null; } } BDDFactory.BDDOp op; /** Filename for BDD config. */ String filename0; /** Filenames for inputs. */ String filename1; String filename2; String filename3; /** How long to delay for loading, in ms. */ long DELAY_TIME = 20000; /** Best calc time so far. */ long bestCalcTime; /** Best varorder so far. */ String bestOrder; /** Initial node table size. */ int nodeTableSize; /** Initial cache size. */ int cacheSize; /** Initial max increase. */ int maxIncrease; /** File pointers for output and input BDDs. */ File f0, f1, f2, f3; /** Construct a new TryVarOrder. */ public TryVarOrder(int nodeTableSize, int cacheSize, int maxIncrease, long bestTime, long delayTime) { this.bestCalcTime = bestTime; //this.nodeTableSize = b1.getFactory().getAllocNum(); this.nodeTableSize = nodeTableSize; this.cacheSize = cacheSize; this.maxIncrease = maxIncrease; this.DELAY_TIME = delayTime; } /** * Initialize for a new trial. * Takes the given input BDDs and saves them out to temporary files. * * @param b1 first input to applyEx * @param b2 second input to applyEx * @param dom third input to applyEx * @param op operation to be passed to applyEx * @throws IOException */ public void init(BDD b1, BDD b2, BDD dom, BDDFactory.BDDOp op) throws IOException { this.op = op; f0 = File.createTempFile("fbo", "a"); filename0 = f0.getAbsolutePath(); f0.deleteOnExit(); f1 = File.createTempFile("fbo", "b"); filename1 = f1.getAbsolutePath(); f1.deleteOnExit(); f2 = File.createTempFile("fbo", "c"); filename2 = f2.getAbsolutePath(); f2.deleteOnExit(); f3 = File.createTempFile("fbo", "d"); filename3 = f3.getAbsolutePath(); f3.deleteOnExit(); //System.out.print("Writing BDDs to files..."); writeBDDConfig(b1.getFactory(), filename0); b1.getFactory().save(filename1, b1); b2.getFactory().save(filename2, b2); dom.getFactory().save(filename3, dom); //System.out.println("done."); try { initBDDOperation(); } catch (Exception x) { System.err.println("Exception occurred while initializing: "+x.getLocalizedMessage()); x.printStackTrace(); } } /** * Clean up the temporary files. */ public void cleanup() { //System.out.println("Cleaning up temporary files."); try { f0.delete(); f1.delete(); f2.delete(); f3.delete(); free(); } catch (Exception x) { System.err.println("Exception occurred while cleaning up: "+x.getLocalizedMessage()); x.printStackTrace(); } } /** * Write the BDD configuration to a file. * * @param bdd BDD factory * @param fileName filename * @throws IOException */ public void writeBDDConfig(BDDFactory bdd, String fileName) throws IOException { BufferedWriter dos = null; try { dos = new BufferedWriter(new FileWriter(fileName)); for (int i = 0; i < bdd.numberOfDomains(); ++i) { BDDDomain d = bdd.getDomain(i); dos.write(d.getName()+" "+d.size()+"\n"); } } finally { if (dos != null) dos.close(); } } /** * Try out a variable order. * * @param reverse whether to reverse the bits * @param varOrder variable order to try * @return time spent, or Long.MAX_VALUE if it didn't terminate */ public long tryOrder(String factory, boolean reverse, String varOrder) { if (bdd == null) initBDDFactory(factory); //System.gc(); TryThread t = new TryThread(reverse, varOrder); t.start(); boolean stopped; try { t.join(DELAY_TIME); if (t.initTime >= 0L) { t.join(bestCalcTime); } } catch (InterruptedException x) { } if (t.isAlive()) { t.stop(); Thread.yield(); // Help ThreadDeath exception to propagate. System.out.print("Free memory: "+Runtime.getRuntime().freeMemory()); destroyBDDFactory(); System.gc(); System.out.println(" bytes -> "+Runtime.getRuntime().freeMemory()+" bytes"); } if (t.computeTime < 0) { if (t.initTime < 0) { // Couldn't even initialize in time! System.out.println("BDD factory took too long to initialize, aborted."); } else { System.out.println("Took too long to compute, aborted."); } } else if (t.computeTime < bestCalcTime) { bestOrder = varOrder; bestCalcTime = t.computeTime; } return t.computeTime; } public String getBestOrder() { return bestOrder; } public long getBestTime() { return bestCalcTime; } public class TryThread extends Thread { boolean reverse; String varOrderToTry; long initTime = -1; long computeTime = -1; TryThread(boolean r, String v) { reverse = r; varOrderToTry = v; } public void run() { //System.out.println("\nTrying ordering "+varOrderToTry); try { long time = System.currentTimeMillis(); setVarOrder(reverse, varOrderToTry); load(); initTime = time - System.currentTimeMillis(); computeTime = doIt(); free(); System.out.println("Ordering: "+varOrderToTry+" time: "+time); } catch (Exception x) { System.err.println("Exception occurred while trying order: "+x.getLocalizedMessage()); x.printStackTrace(); } } } } |
|
From: John W. <joe...@us...> - 2004-09-21 22:30:15
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9922/org/sf/javabdd Added Files: HijackingClassLoader.java Log Message: Hijacking class loader. --- NEW FILE: HijackingClassLoader.java --- // HijackingClassLoader.java, created Jun 24, 2004 5:39:24 PM 2004 by jwhaley // Copyright (C) 2004 John Whaley <jw...@al...> // Licensed under the terms of the GNU LGPL; see COPYING for details. package org.sf.javabdd; import java.util.LinkedList; import java.util.List; import java.util.StringTokenizer; import java.util.jar.Attributes; import java.util.jar.Manifest; import java.util.jar.Attributes.Name; import java.io.File; import java.io.IOException; import java.net.URL; import java.net.URLClassLoader; import java.net.URLStreamHandlerFactory; import java.security.AccessControlContext; import java.security.AccessController; import java.security.CodeSource; import java.security.PrivilegedExceptionAction; import sun.misc.Resource; import sun.misc.URLClassPath; /** * A special classloader that allows you to hijack all of the classes and load * them from your list of URLs. Plus, you can dynamically change the classpath * at run time! * * @author jwhaley * @version $Id: HijackingClassLoader.java,v 1.1 2004/09/21 22:30:05 joewhaley Exp $ */ public class HijackingClassLoader extends URLClassLoader { public static HijackingClassLoader makeClassLoader() { String cp = System.getProperty("java.class.path"); StringTokenizer st = new StringTokenizer(cp, System.getProperty("path.separator")); List urls = new LinkedList(); while (st.hasMoreTokens()) { String s = st.nextToken(); try { URL url = getFileURL(s); if (url != null) urls.add(url); } catch (IOException x) {} } URL[] u = (URL[]) urls.toArray(new URL[urls.size()]); return new HijackingClassLoader(u); } public static URL getFileURL(String name) throws IOException { File f = new File(name); if (f.exists()) return f.toURL(); else return null; } public static final boolean TRACE = false; /* The search path for classes and resources */ private URLClassPath ucp; /* The context to be used when loading classes and resources */ private AccessControlContext acc; /* Whether we should skip hijacking java.lang stuff. */ boolean skipJavaLang = true; /** * @param urls * @param parent */ public HijackingClassLoader(URL[] urls, ClassLoader parent) { super(urls, parent); ucp = new URLClassPath(urls); acc = AccessController.getContext(); } /** * @param urls */ public HijackingClassLoader(URL[] urls) { super(urls); ucp = new URLClassPath(urls); acc = AccessController.getContext(); } /** * @param urls * @param parent * @param factory */ public HijackingClassLoader(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory) { super(urls, parent, factory); ucp = new URLClassPath(urls, factory); acc = AccessController.getContext(); } /* (non-Javadoc) * @see java.net.URLClassLoader#addURL(java.net.URL) */ public void addURL(URL url) { ucp.addURL(url); super.addURL(url); } /* * Defines a Class using the class bytes obtained from the specified * Resource. The resulting Class must be resolved before it can be used. */ private Class defineClass(String name, Resource res) throws IOException { int i = name.lastIndexOf('.'); URL url = res.getCodeSourceURL(); if (i != -1) { String pkgname = name.substring(0, i); // Check if package already loaded. Package pkg = getPackage(pkgname); Manifest man = res.getManifest(); if (pkg != null) { // Package found, so check package sealing. if (pkg.isSealed()) { // Verify that code source URL is the same. if (!pkg.isSealed(url)) { throw new SecurityException( "sealing violation: package " + pkgname + " is sealed"); } } else { // Make sure we are not attempting to seal the package // at this code source URL. if ((man != null) && isSealed(pkgname, man)) { throw new SecurityException( "sealing violation: can't seal package " + pkgname + ": already loaded"); } } } else { if (man != null) { definePackage(pkgname, man, url); } else { definePackage(pkgname, null, null, null, null, null, null, null); } } } // Now read the class bytes and define the class byte[] b = res.getBytes(); java.security.cert.Certificate[] certs = res.getCertificates(); CodeSource cs = new CodeSource(url, certs); return defineClass(name, b, 0, b.length, cs); } /* * Returns true if the specified package name is sealed according to the * given manifest. */ private boolean isSealed(String name, Manifest man) { String path = name.replace('.', '/').concat("/"); Attributes attr = man.getAttributes(path); String sealed = null; if (attr != null) { sealed = attr.getValue(Name.SEALED); } if (sealed == null) { if ((attr = man.getMainAttributes()) != null) { sealed = attr.getValue(Name.SEALED); } } return "true".equalsIgnoreCase(sealed); } /* (non-Javadoc) * Overridden so that we can add trace info. * * @see java.lang.ClassLoader#findClass(java.lang.String) */ protected Class findClass(final String name) throws ClassNotFoundException { try { return (Class) AccessController.doPrivileged( new PrivilegedExceptionAction() { public Object run() throws ClassNotFoundException { String path = name.replace('.', '/').concat(".class"); Resource res = ucp.getResource(path, false); if (res != null) { if (TRACE) System.out.println("Hijacked! " + res); try { return defineClass(name, res); } catch (IOException e) { throw new ClassNotFoundException(name, e); } } else { throw new ClassNotFoundException(name); } } }, acc); } catch (java.security.PrivilegedActionException pae) { throw (ClassNotFoundException) pae.getException(); } } /* (non-Javadoc) * @see java.lang.ClassLoader#loadClass(java.lang.String, boolean) */ public final synchronized Class loadClass(String name, boolean resolve) throws ClassNotFoundException { if (!skipJavaLang || !name.startsWith("java.lang.")) { // Check if we have it before we check the parent class loader. try { return findClass(name); } catch (ClassNotFoundException e) { } } Class c = super.loadClass(name, resolve); return c; } } |
|
From: John W. <joe...@us...> - 2004-09-16 23:50:09
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4567 Modified Files: Makefile Log Message: Change to static linking. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.27 retrieving revision 1.28 diff -C2 -d -r1.27 -r1.28 *** Makefile 14 Sep 2004 21:38:28 -0000 1.27 --- Makefile 16 Sep 2004 23:49:55 -0000 1.28 *************** *** 70,74 **** CFLAGS = -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -static-libcxa -shared $(EXTRA_CFLAGS) endif endif --- 70,74 ---- CFLAGS = -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -shared -static $(EXTRA_CFLAGS) endif endif *************** *** 221,231 **** ipo: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -ipo $(INCLUDES) -shared -static-libcxa $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) pdogen: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -prof_gen $(INCLUDES) -shared -static-libcxa $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) pdouse: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -prof_use -ipo $(INCLUDES) -shared -static-libcxa $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) opt_report: --- 221,231 ---- ipo: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -ipo $(INCLUDES) -shared -static $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) pdogen: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -prof_gen $(INCLUDES) -shared -static $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) pdouse: buddy_jni.h ! icc -D_REENTRANT -D_GNU_SOURCE -O2 -Ob2 -prof_use -ipo $(INCLUDES) -shared -static $(DLL_OUTPUT_OPTION)libbuddy.so $(BUDDY_SRCS) opt_report: |
|
From: John W. <joe...@us...> - 2004-09-15 19:35:38
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17706/org/sf/javabdd Modified Files: BDDFactory.java Log Message: Add error message. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDFactory.java,v retrieving revision 1.27 retrieving revision 1.28 diff -C2 -d -r1.27 -r1.28 *** BDDFactory.java 14 Sep 2004 04:25:09 -0000 1.27 --- BDDFactory.java 15 Sep 2004 19:35:25 -0000 1.28 *************** *** 66,71 **** if (bddpackage.equals("typed")) return TypedBDDFactory.init(nodenum, cachesize); ! } catch (LinkageError _) { ! System.out.println("Could not load BDD package "+bddpackage); } try { --- 66,71 ---- if (bddpackage.equals("typed")) return TypedBDDFactory.init(nodenum, cachesize); ! } catch (LinkageError e) { ! System.out.println("Could not load BDD package "+bddpackage+": "+e.getLocalizedMessage()); } try { |
|
From: John W. <joe...@us...> - 2004-09-15 03:03:51
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29500/org/sf/javabdd Modified Files: JDDFactory.java Log Message: Fix ordering bug. Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.5 retrieving revision 1.6 diff -C2 -d -r1.5 -r1.6 *** JDDFactory.java 15 Sep 2004 00:34:02 -0000 1.5 --- JDDFactory.java 15 Sep 2004 03:03:39 -0000 1.6 *************** *** 737,747 **** for (int i = 0; i < bdd.numberOfVariables(); ++i) { int k = neworder[i]; ! //System.out.println("Var "+i+" (node "+vars[i]+") in original order -> var "+k+" (node "+vars[k]+") in new order"); ! newvars[i] = vars[k]; ! var2level[i] = k; ! level2var[k] = i; } vars = newvars; for (int i = 0; i < numberOfDomains(); ++i) { BDDDomain d = getDomain(i); --- 737,748 ---- for (int i = 0; i < bdd.numberOfVariables(); ++i) { int k = neworder[i]; ! //System.out.println("Var "+k+" (node "+vars[k]+") in original order -> var "+i+" (node "+vars[i]+") in new order"); ! newvars[k] = vars[i]; ! var2level[k] = i; ! level2var[i] = k; } vars = newvars; + //System.out.println("Number of domains: "+numberOfDomains()); for (int i = 0; i < numberOfDomains(); ++i) { BDDDomain d = getDomain(i); |
|
From: John W. <joe...@us...> - 2004-09-15 03:03:02
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29317/org/sf/javabdd Modified Files: TestBDDFactory.java Log Message: Change to JDD factory test. Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.11 retrieving revision 1.12 diff -C2 -d -r1.11 -r1.12 *** TestBDDFactory.java 2 Aug 2004 20:20:53 -0000 1.11 --- TestBDDFactory.java 15 Sep 2004 03:02:53 -0000 1.12 *************** *** 30,34 **** public static BDDFactory init(int nodenum, int cachesize) { BDDFactory a = BuDDyFactory.init(nodenum, cachesize); ! BDDFactory b = CUDDFactory.init(nodenum, cachesize); return new TestBDDFactory(a, b); } --- 30,34 ---- 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); } *************** *** 586,590 **** int r1 = f1.setVarNum(num); int r2 = f2.setVarNum(num); ! assertSame(r1 == r2, "setVarNum"); return r1; } --- 586,590 ---- int r1 = f1.setVarNum(num); int r2 = f2.setVarNum(num); ! //assertSame(r1 == r2, "setVarNum"); return r1; } |
|
From: John W. <joe...@us...> - 2004-09-15 02:54:53
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv27952 Modified Files: jdd.jar Log Message: Changed node table grow() to be more aggressive. Index: jdd.jar =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/jdd.jar,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 Binary files /tmp/cvsyqlODU and /tmp/cvspmSsOe differ |
|
From: John W. <joe...@us...> - 2004-09-15 00:34:11
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4351/org/sf/javabdd Modified Files: JDDFactory.java Log Message: Added setmaxincrease, etc. Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.4 retrieving revision 1.5 diff -C2 -d -r1.4 -r1.5 *** JDDFactory.java 14 Sep 2004 23:54:10 -0000 1.4 --- JDDFactory.java 15 Sep 2004 00:34:02 -0000 1.5 *************** *** 22,25 **** --- 22,26 ---- bdd = new jdd.bdd.BDD(nodenum, cachesize); vars = new int[256]; + jdd.util.Options.verbose = true; } *************** *** 548,553 **** */ public void setMinFreeNodes(int x) { ! // TODO Auto-generated method stub ! //throw new BDDException(); } --- 549,553 ---- */ public void setMinFreeNodes(int x) { ! jdd.util.Configuration.minFreeNodesProcent = x; } *************** *** 556,561 **** */ public int setMaxIncrease(int x) { ! //throw new BDDException(); ! return 0; } --- 556,562 ---- */ public int setMaxIncrease(int x) { ! int old = jdd.util.Configuration.maxNodeIncrease; ! jdd.util.Configuration.maxNodeIncrease = x; ! return old; } |
|
From: John W. <joe...@us...> - 2004-09-15 00:09:29
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32432 Modified Files: jdd.jar Log Message: New version of jdd from cvs. Index: jdd.jar =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/jdd.jar,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 Binary files /tmp/cvstdLAMC and /tmp/cvs2dgTA3 differ |
|
From: John W. <joe...@us...> - 2004-09-15 00:03:04
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31395 Modified Files: .classpath Log Message: Added jdd src path. Index: .classpath =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/.classpath,v retrieving revision 1.2 retrieving revision 1.3 diff -C2 -d -r1.2 -r1.3 *** .classpath 23 Jun 2004 04:11:58 -0000 1.2 --- .classpath 15 Sep 2004 00:02:55 -0000 1.3 *************** *** 3,7 **** <classpathentry kind="src" path=""/> <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/> ! <classpathentry kind="lib" path="jdd.jar"/> <classpathentry kind="output" path=""/> </classpath> --- 3,7 ---- <classpathentry kind="src" path=""/> <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/> ! <classpathentry sourcepath="/jdd/src" kind="lib" path="jdd.jar"/> <classpathentry kind="output" path=""/> </classpath> |
|
From: John W. <joe...@us...> - 2004-09-15 00:02:16
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31273/org/sf/javabdd Modified Files: JFactory.java Log Message: Special-case and, or, relprod operations. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JFactory.java,v retrieving revision 1.8 retrieving revision 1.9 diff -C2 -d -r1.8 -r1.9 *** JFactory.java 9 Aug 2004 21:31:11 -0000 1.8 --- JFactory.java 15 Sep 2004 00:02:07 -0000 1.9 *************** *** 1161,1165 **** if (firstReorder == 0) bdd_disable_reorder(); ! res = apply_rec(l, r); if (firstReorder == 0) bdd_enable_reorder(); --- 1161,1169 ---- if (firstReorder == 0) bdd_disable_reorder(); ! switch (op) { ! case bddop_and: res = and_rec(l, r); break; ! case bddop_or: res = or_rec(l, r); break; ! default: res = apply_rec(l, r); break; ! } if (firstReorder == 0) bdd_enable_reorder(); *************** *** 1183,1207 **** int res; switch (applyop) { - case bddop_and : - if (l == r) - return l; - if (ISZERO(l) || ISZERO(r)) - return 0; - if (ISONE(l)) - return r; - if (ISONE(r)) - return l; - break; - case bddop_or : - if (l == r) - return l; - if (ISONE(l) || ISONE(r)) - return 1; - if (ISZERO(l)) - return r; - if (ISZERO(r)) - return l; - break; case bddop_xor : if (l == r) --- 1187,1193 ---- int res; + if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or); + switch (applyop) { case bddop_xor : if (l == r) *************** *** 1268,1271 **** --- 1254,1349 ---- } + int and_rec(int l, int r) { + BddCacheDataI entry; + int res; + + if (l == r) + return l; + if (ISZERO(l) || ISZERO(r)) + return 0; + if (ISONE(l)) + return r; + if (ISONE(r)) + return l; + entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and)); + + if (entry.a == l && entry.b == r && entry.c == bddop_and) { + if (CACHESTATS) + bddcachestats.opHit++; + return entry.res; + } + if (CACHESTATS) + bddcachestats.opMiss++; + + if (LEVEL(l) == LEVEL(r)) { + PUSHREF(and_rec(LOW(l), LOW(r))); + PUSHREF(and_rec(HIGH(l), HIGH(r))); + res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else if (LEVEL(l) < LEVEL(r)) { + PUSHREF(and_rec(LOW(l), r)); + PUSHREF(and_rec(HIGH(l), r)); + res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else { + PUSHREF(and_rec(l, LOW(r))); + PUSHREF(and_rec(l, HIGH(r))); + res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } + + POPREF(2); + + entry.a = l; + entry.b = r; + entry.c = bddop_and; + entry.res = res; + + return res; + } + + int or_rec(int l, int r) { + BddCacheDataI entry; + int res; + + if (l == r) + return l; + if (ISONE(l) || ISONE(r)) + return 1; + if (ISZERO(l)) + return r; + if (ISZERO(r)) + return l; + entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or)); + + if (entry.a == l && entry.b == r && entry.c == bddop_or) { + if (CACHESTATS) + bddcachestats.opHit++; + return entry.res; + } + if (CACHESTATS) + bddcachestats.opMiss++; + + if (LEVEL(l) == LEVEL(r)) { + PUSHREF(or_rec(LOW(l), LOW(r))); + PUSHREF(or_rec(HIGH(l), HIGH(r))); + res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else if (LEVEL(l) < LEVEL(r)) { + PUSHREF(or_rec(LOW(l), r)); + PUSHREF(or_rec(HIGH(l), r)); + res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else { + PUSHREF(or_rec(l, LOW(r))); + PUSHREF(or_rec(l, HIGH(r))); + res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } + + POPREF(2); + + entry.a = l; + entry.b = r; + entry.c = bddop_or; + entry.res = res; + + return res; + } + int relprod_rec(int l, int r) { BddCacheDataI entry; *************** *** 1284,1293 **** int LEVEL_r = LEVEL(r); if (LEVEL_l > quantlast && LEVEL_r > quantlast) { ! int oldop = applyop; ! applyop = appexop; ! res = apply_rec(l, r); ! applyop = oldop; } else { ! entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop)); if (entry.a == l && entry.b == r && entry.c == appexid) { if (CACHESTATS) --- 1362,1370 ---- int LEVEL_r = LEVEL(r); if (LEVEL_l > quantlast && LEVEL_r > quantlast) { ! applyop = bddop_and; ! res = and_rec(l, r); ! applyop = bddop_or; } else { ! entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and)); if (entry.a == l && entry.b == r && entry.c == appexid) { if (CACHESTATS) *************** *** 1302,1306 **** PUSHREF(relprod_rec(HIGH(l), HIGH(r))); if (INVARSET(LEVEL_l)) ! res = apply_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_l, READREF(2), READREF(1)); --- 1379,1383 ---- PUSHREF(relprod_rec(HIGH(l), HIGH(r))); if (INVARSET(LEVEL_l)) ! res = or_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_l, READREF(2), READREF(1)); *************** *** 1309,1313 **** PUSHREF(relprod_rec(HIGH(l), r)); if (INVARSET(LEVEL_l)) ! res = apply_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_l, READREF(2), READREF(1)); --- 1386,1390 ---- PUSHREF(relprod_rec(HIGH(l), r)); if (INVARSET(LEVEL_l)) ! res = or_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_l, READREF(2), READREF(1)); *************** *** 1316,1320 **** PUSHREF(relprod_rec(l, HIGH(r))); if (INVARSET(LEVEL_r)) ! res = apply_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_r, READREF(2), READREF(1)); --- 1393,1397 ---- PUSHREF(relprod_rec(l, HIGH(r))); if (INVARSET(LEVEL_r)) ! res = or_rec(READREF(2), READREF(1)); else res = bdd_makenode(LEVEL_r, READREF(2), READREF(1)); *************** *** 1365,1369 **** if (firstReorder == 0) bdd_disable_reorder(); ! res = opr == -1 ? relprod_rec(l, r) : appquant_rec(l, r); if (firstReorder == 0) bdd_enable_reorder(); --- 1442,1446 ---- if (firstReorder == 0) bdd_disable_reorder(); ! res = opr == bddop_and ? relprod_rec(l, r) : appquant_rec(l, r); if (firstReorder == 0) bdd_enable_reorder(); *************** *** 1439,1453 **** int res; switch (appexop) { - case bddop_and : - if (l == 0 || r == 0) - return 0; - if (l == r) - return quant_rec(l); - if (l == 1) - return quant_rec(r); - if (r == 1) - return quant_rec(l); - break; case bddop_or : if (l == 1 || r == 1) --- 1516,1522 ---- int res; + if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and); + switch (appexop) { case bddop_or : if (l == 1 || r == 1) *************** *** 1483,1487 **** int oldop = applyop; applyop = appexop; ! res = apply_rec(l, r); applyop = oldop; } else { --- 1552,1560 ---- int oldop = applyop; applyop = appexop; ! switch (applyop) { ! case bddop_and: res = and_rec(l, r); break; ! case bddop_or: res = or_rec(l, r); break; ! default: res = apply_rec(l, r); break; ! } applyop = oldop; } else { *************** *** 1495,1519 **** bddcachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { PUSHREF(appquant_rec(LOW(l), LOW(r))); PUSHREF(appquant_rec(HIGH(l), HIGH(r))); ! if (INVARSET(LEVEL(l))) ! res = apply_rec(READREF(2), READREF(1)); ! else ! res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); } else if (LEVEL(l) < LEVEL(r)) { PUSHREF(appquant_rec(LOW(l), r)); PUSHREF(appquant_rec(HIGH(l), r)); ! if (INVARSET(LEVEL(l))) ! res = apply_rec(READREF(2), READREF(1)); ! else ! res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); } else { PUSHREF(appquant_rec(l, LOW(r))); PUSHREF(appquant_rec(l, HIGH(r))); ! if (INVARSET(LEVEL(r))) ! res = apply_rec(READREF(2), READREF(1)); ! else ! res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); } --- 1568,1594 ---- bddcachestats.opMiss++; + int lev; if (LEVEL(l) == LEVEL(r)) { PUSHREF(appquant_rec(LOW(l), LOW(r))); PUSHREF(appquant_rec(HIGH(l), HIGH(r))); ! lev = LEVEL(l); } else if (LEVEL(l) < LEVEL(r)) { PUSHREF(appquant_rec(LOW(l), r)); PUSHREF(appquant_rec(HIGH(l), r)); ! lev = LEVEL(l); } else { PUSHREF(appquant_rec(l, LOW(r))); PUSHREF(appquant_rec(l, HIGH(r))); ! lev = LEVEL(r); ! } ! if (INVARSET(lev)) { ! int r2 = READREF(2), r1 = READREF(1); ! switch (applyop) { ! case bddop_and: res = and_rec(r2, r1); break; ! case bddop_or: res = or_rec(r2, r1); break; ! default: res = apply_rec(r2, r1); break; ! } ! } else { ! res = bdd_makenode(lev, READREF(2), READREF(1)); } *************** *** 1548,1555 **** PUSHREF(quant_rec(HIGH(r))); ! if (INVARSET(LEVEL(r))) ! res = apply_rec(READREF(2), READREF(1)); ! else res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); POPREF(2); --- 1623,1636 ---- PUSHREF(quant_rec(HIGH(r))); ! if (INVARSET(LEVEL(r))) { ! int r2 = READREF(2), r1 = READREF(1); ! switch (applyop) { ! case bddop_and: res = and_rec(r2, r1); break; ! case bddop_or: res = or_rec(r2, r1); break; ! default: res = apply_rec(r2, r1); break; ! } ! } else { res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } POPREF(2); *************** *** 2053,2057 **** POPREF(2); } else /* LEVEL(d) < LEVEL(f) */ { ! PUSHREF(apply_rec(LOW(d), HIGH(d))); /* Exist quant */ res = simplify_rec(f, READREF(1)); POPREF(1); --- 2134,2138 ---- POPREF(2); } else /* LEVEL(d) < LEVEL(f) */ { ! PUSHREF(or_rec(LOW(d), HIGH(d))); /* Exist quant */ res = simplify_rec(f, READREF(1)); POPREF(1); |
|
From: John W. <joe...@us...> - 2004-09-14 23:54:18
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30084/org/sf/javabdd Modified Files: JDDFactory.java Log Message: Added BDD cleanup call. Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.3 retrieving revision 1.4 diff -C2 -d -r1.3 -r1.4 *** JDDFactory.java 2 Aug 2004 20:20:53 -0000 1.3 --- JDDFactory.java 14 Sep 2004 23:54:10 -0000 1.4 *************** *** 532,536 **** */ public void done() { ! // TODO Auto-generated method stub } --- 532,536 ---- */ public void done() { ! bdd.cleanup(); } |
|
From: John W. <joe...@us...> - 2004-09-14 23:53:40
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29936/org/sf/javabdd Modified Files: BuDDyFactory.java Log Message: Made it so that you can change buddy library name with a system property. Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.34 retrieving revision 1.35 diff -C2 -d -r1.34 -r1.35 *** BuDDyFactory.java 2 Aug 2004 20:20:53 -0000 1.34 --- BuDDyFactory.java 14 Sep 2004 23:53:30 -0000 1.35 *************** *** 43,47 **** static { ! String libname = "buddy"; try { System.loadLibrary(libname); --- 43,47 ---- static { ! String libname = System.getProperty("buddylib", "buddy"); try { System.loadLibrary(libname); |
|
From: John W. <joe...@us...> - 2004-09-14 21:38:37
|
Update of /cvsroot/javabdd/JavaBDD In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32427 Modified Files: Makefile Log Message: Added static linking of Intel library. Index: Makefile =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/Makefile,v retrieving revision 1.26 retrieving revision 1.27 diff -C2 -d -r1.26 -r1.27 *** Makefile 28 Jul 2004 11:38:08 -0000 1.26 --- Makefile 14 Sep 2004 21:38:28 -0000 1.27 *************** *** 70,74 **** CFLAGS = -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -shared $(EXTRA_CFLAGS) endif endif --- 70,74 ---- CFLAGS = -O2 -Ob2 -ip $(EXTRA_CFLAGS) LINK = icc ! LINKFLAGS = -static-libcxa -shared $(EXTRA_CFLAGS) endif endif |
|
From: John W. <joe...@us...> - 2004-09-14 04:25:20
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3424/org/sf/javabdd Modified Files: BDDFactory.java Log Message: Fixed bug, Java version of save() was implicitly freeing the saved BDD. Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDFactory.java,v retrieving revision 1.26 retrieving revision 1.27 diff -C2 -d -r1.26 -r1.27 *** BDDFactory.java 2 Aug 2004 20:32:59 -0000 1.26 --- BDDFactory.java 14 Sep 2004 04:25:09 -0000 1.27 *************** *** 511,515 **** for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) { BDD b = (BDD) it.next(); ! b.free(); } } --- 511,515 ---- for (Iterator it = visited.keySet().iterator(); it.hasNext(); ) { BDD b = (BDD) it.next(); ! if (b != r) b.free(); } } |
