Menu
▾
▴
buddy-developers — Participating in BuDDy development
You can subscribe to this list here.
| 2004 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
(4) |
Jul
(53) |
Aug
(5) |
Sep
(2) |
Oct
(1) |
Nov
|
Dec
|
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2005 |
Jan
(8) |
Feb
(2) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
| 2006 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(4) |
Dec
|
| 2007 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
(3) |
Jul
(28) |
Aug
(9) |
Sep
|
Oct
|
Nov
|
Dec
|
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(4) |
Sep
|
Oct
|
Nov
|
Dec
|
| 2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(2) |
Jun
|
Jul
|
Aug
|
Sep
(1) |
Oct
|
Nov
|
Dec
|
| 2011 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(1) |
Dec
|
| 2013 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2014 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
(5) |
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: Haim C. <hai...@us...> - 2007-07-07 04:13:51
|
Looks great to me Nikos ! Can we also make it part of the Makefiles, so the docs get generated (if doxygen is available on the system) when you run make ? On 7/4/07, Nikos Gkorogiannis <N.G...@cs...> wrote: > Hi all, > > I'm just new to the project and I thought I'd start from something easy. > Haim mentioned that it would be nice to convert the (reference) > documentation to something like Doxygen. Any suggestions/objections? > > I have a working conversion script in Python. The results can be seen at > the following URL. I haven't made any effort to customise the style. > > http://www.cs.ucl.ac.uk/staff/N.Gkorogiannis/buddy/index.html > > There are a few issues like > - The EXTRA keyword in the original sources, what does it mean? I have > ignored it for the moment (as well as others that are catered for by > doxygen without any user effort like NAME and PROTO). > - Not sure how to do SECTION yet, but apparently doxygen has something > similar. > - Code segments in the docs and other latex-specific code are at copied > verbatim at the moment. This needs fixing by hand. > - The doxygen-recommended way is to put the documenting comments in the > header files. Since this is not the case with the current code, every > documented member will appear in two places, the header file and > the .c/.cxx. > > The source itself seems untouched, i.e. compilation works and regression > test fail only when they fail in the pristine sources (fdd). > > What do you think? > > Thanks > Nikos > > > > ------------------------------------------------------------------------- > This SF.net email is sponsored by DB2 Express > Download DB2 Express C - the FREE version of DB2 express and take > control of your XML. No limits. Just data. Click to get it now. > http://sourceforge.net/powerbar/db2/ > _______________________________________________ > Buddy-developers mailing list > Bud...@li... > https://lists.sourceforge.net/lists/listinfo/buddy-developers > -- _______________________________ Haim Cohen (212) 289 5405 |
|
From: Nikos G. <N.G...@cs...> - 2007-07-04 14:47:33
|
Hi all, I'm just new to the project and I thought I'd start from something easy. Haim mentioned that it would be nice to convert the (reference) documentation to something like Doxygen. Any suggestions/objections? I have a working conversion script in Python. The results can be seen at the following URL. I haven't made any effort to customise the style. http://www.cs.ucl.ac.uk/staff/N.Gkorogiannis/buddy/index.html There are a few issues like - The EXTRA keyword in the original sources, what does it mean? I have ignored it for the moment (as well as others that are catered for by doxygen without any user effort like NAME and PROTO). - Not sure how to do SECTION yet, but apparently doxygen has something similar. - Code segments in the docs and other latex-specific code are at copied verbatim at the moment. This needs fixing by hand. - The doxygen-recommended way is to put the documenting comments in the header files. Since this is not the case with the current code, every documented member will appear in two places, the header file and the .c/.cxx. The source itself seems untouched, i.e. compilation works and regression test fail only when they fail in the pristine sources (fdd). What do you think? Thanks Nikos |
|
From: Nikos G. <N.G...@cs...> - 2007-06-01 12:25:09
|
Hi Haim, Thanks for your reply. I understand that BuDDy is mature - I have been using it on and off since 2000. It would be nice to work out the last few kinks though (like the open patches and bugs) and maybe make small feature updates. I'd be more than happy to help, though I've never used Sourceforge in such a capacity before. Thanks Nikos On Fri, 2007-06-01 at 07:46 -0400, Haim Cohen wrote: > Hi Nikos, > > Please keep in mind that the library is relatively mature - first > release was by Jorn at 1996, so it is quite stable. It has been > spending its majority of life cycle outside of SF and only ~3 years > ago added here. > I will be more than happy to add a new developer to the project ;-) > > Haim |
|
From: Haim C. <hai...@us...> - 2007-06-01 11:46:25
|
Hi Nikos, Please keep in mind that the library is relatively mature - first release was by Jorn at 1996, so it is quite stable. It has been spending its majority of life cycle outside of SF and only ~3 years ago added here. I will be more than happy to add a new developer to the project ;-) Haim On 6/1/07, Nikos Gkorogiannis <N.G...@cs...> wrote: > Hi, > > Buddy is a great package and thanks go to all involved in its > development. However, activity (patches applied, etc) and list traffic > seem low, so is Buddy still being maintained? > > Regards > Nikos > > > > ------------------------------------------------------------------------- > This SF.net email is sponsored by DB2 Express > Download DB2 Express C - the FREE version of DB2 express and take > control of your XML. No limits. Just data. Click to get it now. > http://sourceforge.net/powerbar/db2/ > _______________________________________________ > Buddy-developers mailing list > Bud...@li... > https://lists.sourceforge.net/lists/listinfo/buddy-developers > |
|
From: Nikos G. <N.G...@cs...> - 2007-06-01 10:43:27
|
Hi, Buddy is a great package and thanks go to all involved in its development. However, activity (patches applied, etc) and list traffic seem low, so is Buddy still being maintained? Regards Nikos |
|
From: Haim C. <hai...@us...> - 2006-11-20 04:50:40
|
Update of /cvsroot/buddy/buddy/doc In directory sc8-pr-cvs3.sourceforge.net:/tmp/cvs-serv20659/doc Added Files: jbln.bib Log Message: bib file |
|
From: Haim C. <hai...@us...> - 2006-11-20 02:01:21
|
Update of /cvsroot/buddy/buddy/doc In directory sc8-pr-cvs3.sourceforge.net:/tmp/cvs-serv16316/doc Added Files: varblock.fig example.fig Log Message: adding the fig files |
|
From: Haim C. <hai...@us...> - 2006-11-20 00:55:13
|
Update of /cvsroot/buddy/buddy/doc In directory sc8-pr-cvs3.sourceforge.net:/tmp/cvs-serv21863/doc Added Files: example.pstex example.pstex_t varblock.pstex varblock.pstex_t Log Message: more files required by the documentation |
|
From: Haim C. <hai...@us...> - 2006-11-18 23:45:56
|
Update of /cvsroot/buddy/buddy/doc In directory sc8-pr-cvs3.sourceforge.net:/tmp/cvs-serv11564/doc Added Files: buddy.tex specs.tex Log Message: adding tex files I got from Jorn |
|
From: SourceForge.net <no...@so...> - 2006-04-28 03:06:14
|
Bugs item #1345805, was opened at 2005-11-02 12:20 Message generated for change (Comment added) made by haimcohen You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: code Group: None Status: Closed Resolution: Fixed Priority: 1 Submitted By: Alexander Becker (buddy-user) Assigned to: Haim Cohen (haimcohen) Summary: BuDDy2.4: bug in fdd.c Initial Comment: In BuDDy2.4 there is a bug in code of function fdd_fprintset_rec: Line 767: printf(":"); must be: fprintf(ofile, ":"); When you use function fdd_printset, output to Std_Out is O.K., something like this: <0:2, 3:7><0:6, 3:4> But when you use fdd_fprintset, in your file see you: <02, 37><06, 34> and in your bash (Std_Out): :::: Alex ---------------------------------------------------------------------- >Comment By: Haim Cohen (haimcohen) Date: 2006-04-28 06:06 Message: Logged In: YES user_id=1024352 fixed in CVS. Thanks. ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 |
|
From: SourceForge.net <no...@so...> - 2006-04-28 03:05:08
|
Bugs item #1345805, was opened at 2005-11-02 12:20 Message generated for change (Settings changed) made by haimcohen You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: code Group: None >Status: Closed >Resolution: Fixed Priority: 1 Submitted By: Alexander Becker (buddy-user) >Assigned to: Haim Cohen (haimcohen) Summary: BuDDy2.4: bug in fdd.c Initial Comment: In BuDDy2.4 there is a bug in code of function fdd_fprintset_rec: Line 767: printf(":"); must be: fprintf(ofile, ":"); When you use function fdd_printset, output to Std_Out is O.K., something like this: <0:2, 3:7><0:6, 3:4> But when you use fdd_fprintset, in your file see you: <02, 37><06, 34> and in your bash (Std_Out): :::: Alex ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 |
|
From: Haim C. <hai...@us...> - 2006-04-28 03:00:59
|
Update of /cvsroot/buddy/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31901/buddy/src Modified Files: fdd.c Log Message: Fixing bug [ 1345805 ] BuDDy2.4: bug in fdd.c . I also updated the fdd example / test to reflect the fix. |
|
From: Haim C. <hai...@us...> - 2006-04-28 03:00:59
|
Update of /cvsroot/buddy/buddy/examples/bddtest/.libs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31901/buddy/examples/bddtest/.libs Added Files: .cvsignore Log Message: Fixing bug [ 1345805 ] BuDDy2.4: bug in fdd.c . I also updated the fdd example / test to reflect the fix. |
|
From: Haim C. <hai...@us...> - 2006-04-28 03:00:59
|
Update of /cvsroot/buddy/buddy/examples/fdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31901/buddy/examples/fdd Modified Files: fdd.cxx .cvsignore Log Message: Fixing bug [ 1345805 ] BuDDy2.4: bug in fdd.c . I also updated the fdd example / test to reflect the fix. |
|
From: Haim C. <hai...@us...> - 2006-04-28 03:00:59
|
Update of /cvsroot/buddy/buddy/examples/queen In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31901/buddy/examples/queen Modified Files: .cvsignore Log Message: Fixing bug [ 1345805 ] BuDDy2.4: bug in fdd.c . I also updated the fdd example / test to reflect the fix. |
|
From: Haim C. <hai...@us...> - 2006-04-28 03:00:51
|
Update of /cvsroot/buddy/buddy/examples/bddtest/.libs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31875/buddy/examples/bddtest/.libs Log Message: Directory /cvsroot/buddy/buddy/examples/bddtest/.libs added to the repository |
|
From: SourceForge.net <no...@so...> - 2006-04-27 03:01:56
|
Bugs item #1345805, was opened at 2005-11-02 12:20 Message generated for change (Settings changed) made by haimcohen You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: code Group: None Status: Open Resolution: None >Priority: 1 Submitted By: Alexander Becker (buddy-user) Assigned to: Nobody/Anonymous (nobody) Summary: BuDDy2.4: bug in fdd.c Initial Comment: In BuDDy2.4 there is a bug in code of function fdd_fprintset_rec: Line 767: printf(":"); must be: fprintf(ofile, ":"); When you use function fdd_printset, output to Std_Out is O.K., something like this: <0:2, 3:7><0:6, 3:4> But when you use fdd_fprintset, in your file see you: <02, 37><06, 34> and in your bash (Std_Out): :::: Alex ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 |
|
From: SourceForge.net <no...@so...> - 2006-04-12 16:14:23
|
Bugs item #1469374, was opened at 2006-04-12 11:14 Message generated for change (Tracker Item Submitted) made by Item Submitter You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1469374&group_id=112658 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: code Group: None Status: Open Resolution: None Priority: 5 Submitted By: axelco (axelco) Assigned to: Nobody/Anonymous (nobody) Summary: non-recursive support for bdd_allsat Initial Comment: Buddy 2.2 makes a mistake in the function bdd_allsat when you try to run it with a direct or indirect recursive call. I haven't yet checked the source code, but apparently it's caused because bdd_allsat uses in every call THE SAME location in memory to store a char * array called varset. ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1469374&group_id=112658 |
|
From: SourceForge.net <no...@so...> - 2005-11-02 10:20:42
|
Bugs item #1345805, was opened at 2005-11-02 10:20 Message generated for change (Tracker Item Submitted) made by Item Submitter You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: code Group: None Status: Open Resolution: None Priority: 5 Submitted By: Alexander Becker (buddy-user) Assigned to: Nobody/Anonymous (nobody) Summary: BuDDy2.4: bug in fdd.c Initial Comment: In BuDDy2.4 there is a bug in code of function fdd_fprintset_rec: Line 767: printf(":"); must be: fprintf(ofile, ":"); When you use function fdd_printset, output to Std_Out is O.K., something like this: <0:2, 3:7><0:6, 3:4> But when you use fdd_fprintset, in your file see you: <02, 37><06, 34> and in your bash (Std_Out): :::: Alex ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1345805&group_id=112658 |
|
From: John W. <joe...@us...> - 2005-05-04 22:43:25
|
Update of /cvsroot/buddy/buddy/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv11176 Modified Files: reorder.c Log Message: Fixed a stupid bug where someone forgot a () to make bdd_reorder_ready into a procedure call. As it was, it was succeeding every time. |
|
From: John W. <jw...@st...> - 2005-02-15 05:47:01
|
Hi Ondrej, I think at one point back in version 1.0 there was a "bdd_break" and "bdd_restart1". I'm not sure of the provenance of returning BDD_BREAK in this case, though. I think it probably should be BDD_DEREF. (Although if you run into this error your code is broken anyway.) I'll change it to return bdd_error(BDD_DEREF), if no one objects. -John -----Original Message----- From: bud...@li... [mailto:bud...@li...] On Behalf Of Ondrej Lhotak Sent: Monday, February 14, 2005 6:54 AM To: bud...@li... Subject: [Buddy-developers] confusing return value from bdd_delref The bdd_delref function in kernel.c contains the following code: /* if the following line is present, fails there much earlier */ if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */ If the node whose ref count is to be decremented already has a ref count of 0, it returns BDD_BREAK. This is confusing, since BDD_BREAK is supposed to indicate that the user interrupted BuDDy, not that an error occurred. Would BDD_DEREF be more appropriate? Ondrej ------------------------------------------------------- SF email is sponsored by - The IT Product Guide Read honest & candid reviews on hundreds of IT Products from real users. Discover which products truly live up to the hype. Start reading now. http://ads.osdn.com/?ad_id=6595&alloc_id=14396&op=click _______________________________________________ Buddy-developers mailing list Bud...@li... https://lists.sourceforge.net/lists/listinfo/buddy-developers |
|
From: Ondrej L. <ol...@sa...> - 2005-02-14 14:54:53
|
The bdd_delref function in kernel.c contains the following code: /* if the following line is present, fails there much earlier */ if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */ If the node whose ref count is to be decremented already has a ref count of 0, it returns BDD_BREAK. This is confusing, since BDD_BREAK is supposed to indicate that the user interrupted BuDDy, not that an error occurred. Would BDD_DEREF be more appropriate? Ondrej |
|
From: SourceForge.net <no...@so...> - 2005-01-29 02:44:21
|
Bugs item #1040620, was opened at 2004-10-05 05:52 Message generated for change (Comment added) made by joewhaley You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 Category: None Group: None Status: Closed >Resolution: Fixed Priority: 5 Submitted By: Christophe Mauras (mauras) >Assigned to: John Whaley (joewhaley) Summary: Bug in bdd_appuni and in bdd_unique Initial Comment: It seems to me there is a bug in bdd_appuni and same in bdd_unique. These operations may not depend on variable order : Exists unique x0 such that (x0 or x1) = (x0 or x1)[x0\0] xor (x0 or x1)[x0\1] = x1 xor true = not x1 Exists unique x1 such that x0 or x1 = (x0 or x1)[x1\0] xor (x0 or x1)[x1\1] = x0 xor true = not x0 Here is the bug : Buddy reply 1 More simply : Exists unique x0 such that true = (true)[x0\0] xor (true)[x0\1] = true xor true = false Buddy reply 1 Please look at following code : ---------------------------------- #include "bdd.h" #include "stdio.h" main(void) { bdd x0,x1,y0,y1,z0,z1,t; bdd_init (100,10); bdd_setvarnum(5); x0 = bdd_ithvar(0); x1 = bdd_ithvar(1); y0 = bdd_appuni(x0,x1,bddop_or,x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(y0); printf("Good!\n\n"); y1 = bdd_appuni(x0,x1,bddop_or,x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(y1); printf("Bad !\n"); z0 = bdd_unique(bdd_or(x0,x1),x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(z0); printf("Good!\n\n"); z1 = bdd_unique(bdd_or(x0,x1),x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(z1); printf("Bad !\n"); t = bdd_unique(bdd_true(), x0); printf("Result should be 0 \n"); bdd_printtable(z1); printf("Bad !\n"); bdd_done(); } ---------------------------------------------------------------------- >Comment By: John Whaley (joewhaley) Date: 2005-01-28 18:44 Message: Logged In: YES user_id=93687 Actually, I spoke too soon. I just implemented a correct bdd_unique and bdd_appuni. The trick is that the algorithm must determine when a quantified variable is skipped. When it is skipped, the result must be zero. (This is because conceptually the zero branch and one branch point to the same function, and therefore the xor is zero.) Note that unique quantification really says "Are there an odd number where this is true?" rather than "Is this true under exactly one?" If you are only quantifying out one variable, then the "odd" case is exactly the "one" case. But if you are quantifying multiple variables, then the behavior may be different than you would expect. I checked in an implementation in the copy of buddy in the JavaBDD repository and it passes the test cases. I'll backport it into buddy at some point. ---------------------------------------------------------------------- Comment By: John Whaley (joewhaley) Date: 2005-01-28 13:32 Message: Logged In: YES user_id=93687 The problem seems to be in the specification of "unique quantification". The implementation doesn't do what you might expect. To do what you would like seems like it would be a complicated algorithm. I'm not sure how it could be implemented efficiently. If you can come up with an algorithm to perform the operation on a BDD, I can change the bdd_unique implementation. ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 |
|
From: SourceForge.net <no...@so...> - 2005-01-28 21:32:38
|
Bugs item #1040620, was opened at 2004-10-05 05:52 Message generated for change (Comment added) made by joewhaley You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 Category: None Group: None >Status: Closed >Resolution: Later Priority: 5 Submitted By: Christophe Mauras (mauras) Assigned to: Nobody/Anonymous (nobody) Summary: Bug in bdd_appuni and in bdd_unique Initial Comment: It seems to me there is a bug in bdd_appuni and same in bdd_unique. These operations may not depend on variable order : Exists unique x0 such that (x0 or x1) = (x0 or x1)[x0\0] xor (x0 or x1)[x0\1] = x1 xor true = not x1 Exists unique x1 such that x0 or x1 = (x0 or x1)[x1\0] xor (x0 or x1)[x1\1] = x0 xor true = not x0 Here is the bug : Buddy reply 1 More simply : Exists unique x0 such that true = (true)[x0\0] xor (true)[x0\1] = true xor true = false Buddy reply 1 Please look at following code : ---------------------------------- #include "bdd.h" #include "stdio.h" main(void) { bdd x0,x1,y0,y1,z0,z1,t; bdd_init (100,10); bdd_setvarnum(5); x0 = bdd_ithvar(0); x1 = bdd_ithvar(1); y0 = bdd_appuni(x0,x1,bddop_or,x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(y0); printf("Good!\n\n"); y1 = bdd_appuni(x0,x1,bddop_or,x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(y1); printf("Bad !\n"); z0 = bdd_unique(bdd_or(x0,x1),x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(z0); printf("Good!\n\n"); z1 = bdd_unique(bdd_or(x0,x1),x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(z1); printf("Bad !\n"); t = bdd_unique(bdd_true(), x0); printf("Result should be 0 \n"); bdd_printtable(z1); printf("Bad !\n"); bdd_done(); } ---------------------------------------------------------------------- >Comment By: John Whaley (joewhaley) Date: 2005-01-28 13:32 Message: Logged In: YES user_id=93687 The problem seems to be in the specification of "unique quantification". The implementation doesn't do what you might expect. To do what you would like seems like it would be a complicated algorithm. I'm not sure how it could be implemented efficiently. If you can come up with an algorithm to perform the operation on a BDD, I can change the bdd_unique implementation. ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 |
|
From: SourceForge.net <no...@so...> - 2005-01-28 21:25:43
|
Bugs item #1111195, was opened at 2005-01-27 19:05 Message generated for change (Settings changed) made by joewhaley You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658 Category: code Group: None Status: Closed >Resolution: Fixed Priority: 8 Submitted By: John Whaley (joewhaley) Assigned to: John Whaley (joewhaley) Summary: bug in mark_roots causes BDD corruption Initial Comment: I have tracked down a tricky bug involving garbage collection and variable reordering. When calling setvarorder(), some BDDs are not getting reordered, leading to invalid BDDs because the levels are no longer monotonically increasing. This bug affects all BDD reordering (swapvar, dynamic reordering, etc.) The problem seems to be in the construction of the dependency imatrix. mark_roots() is supposed to mark the externally-accessible BDD references and mark which variables depend on each other in the imatrix. mark_roots() calls addref_rec(), which is supposed to recurse down the BDD, adding variable dependencies. mark_roots() uses "REF(r) == 0" to test whether or not it has already visited and therefore computed the dependencies for a BDD node. Herein lies the problem. If an internal BDD node has an external reference, its refcount will not be zero, and mark_roots() will assume it has computed the imatrix dependencies when it has not. The whole mark_roots() process seems to assume that it can use the refcount field as a marker for BDD nodes. This is wrong and we should think about the right way to do this. We may need to use an external table instead. Coming up with a test case that exhibits the bug is nontrivial because the BDDs must be allocated in a non-sequential order. For this to happen, there must have been a garbage collection in the past where nodes were reclaimed and new nodes were given numbers before old nodes. ---------------------------------------------------------------------- Comment By: John Whaley (joewhaley) Date: 2005-01-28 13:24 Message: Logged In: YES user_id=93687 Fixed in CVS. I will be doing a new release shortly. ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658 |
