1---------------------------------------------------------------------------- 2 Logfile for changes to the BDD package 3---------------------------------------------------------------------------- 4 5+ means added code 6x means bugfix or changed code 7- means removed code 8 9Thanks to the following people for bug reports, suggestions and source code: 10 Alan Mishchenko 11 Gerd Behrmann 12 Henrik Hulgaard 13 Henrik Reif Andersen 14 Jacob Lichtenberg 15 Ken Larsen 16 Nikolaj Bjorner 17 18 19VER 2.0 (march 2001) 20-------------------- 21 x Change the copyright notice to a more acceptable form. 22 x Speedup changes in bdd_support() 23 x Rewrote all the prime number calculations in order to get the 24 copyright right. 25 26 27VER 1.9 (august 2000) 28--------------------- 29 + Added bdd_pathcount 30 + Added bdd_anodecount 31 + Added bdd_buildcube, bdd_ibuildcube 32 x Bugfix in bdd_satcountset and bdd_satcountlnset. This corrects a bug 33 introduced in version 1.8. 34 x bug fixes in bdd_constraint and bdd_simplify. Both did calculate a 35 correct cofactor, but not necessarily a minimal one. Changed the name 36 of bdd_constraint to bdd_constrain at the same time. 37 x bug fix in memory allocation for bdd_addvarblock 38 x Changed functions in bddop.c in order to avoid some compiler warnings. 39 x Makefile also installs "fdd.h" and "bvec.h". 40 x Small #include fix in N-Queen example. 41 x Minor changes in the documentation. 42 43 44VER 1.8 (may 2000) 45------------------ 46 + Bugfix in the kernel: canonicity was not unfortunately not guaranteed 47 on certain compilers (at least the microsoft visual C compiler) due to a 48 signed/unsigned bug in kernel.c (and actually not microsofts fault). 49 + Speedups in the reordering code. 50 + Added the use of an interaction matrix for variable swapping. 51 + Added bdd_satoneset 52 + Added bdd_getallocnum 53 + Added bdd_setvarorder 54 + Added bdd_unique, bdd_appuni. 55 + Added bvec_shlfixed, bvec_shrfixed and changed the prototype for 56 bvec_shl and bvec_shr. 57 + Added bvec_mulfixed, bdd_divfixed, bdd_div and changed the 58 prototype for bvec_mul. 59 + Added bdd_printstat 60 + Added new examples: solitare and money 61 + Forces cache tables to prime-number size. 62 + Added bdd_clear_error() if anybody needs that. 63 + Added reorder method WIN3 and WIN3ITE 64 x Small change in queen.cxx - with a huge impact on runtime! 65 x Bugfix in reordering. In some cases reordering would go on forever; 66 first reroder, then retry, then reorder again without resize etc. always 67 reordering in the same operation. Now at most one reordering is allowed 68 for each bdd operation. 69 x Bugfix in C++ printing in Dot format. Wrote zero for one and vice versa. 70 x Bugfix in the garbage collector. If bdd_setmaxincrease was used, then 71 BuDDy would call bdd_error prematurely. Not a major bug, but annoying. 72 x Bugfix in bdd_load. 73 x Speedup in bdd_satcountset and bdd_satcountlnset 74 x Updates to the docs. 75 x Updates to the makefiles 76 77 78VER 1.7 (september 1999) 79------------------------ 80 + Added support for boolean vector operations used in integer arithmetics 81 + Split "bdd.h" into "bdd.h", "fdd.h" and "bvec.h" 82 + Added bdd_cachestats 83 + Added bdd_and, bdd_or, bdd_xor, bdd_impl, bdd_biimpl 84 (wrappers for bdd_apply). 85 + Added a BDD calculator for combinatorial circuits as an example. 86 + Added an example showing the use of the FDD interface. 87 + Added bdd_autoreorder_times, bdd_getreorder_method, bdd_getreorder_times, 88 bdd_reorder_probe, bdd_enable_reorder, bdd_disable_reorder, 89 bdd_var2level, bdd_level2var, bdd_reorder_gain, bdd_swapvar 90 + Added bdd_file_hook, bdd_strm_hook, fdd_file_hook, fdd_strm_hook 91 + Added support for dynamic resizing of the operator caches with 92 the function bdd_setcacheratio. 93 + Added more documentation. 94 x Bugfix in reordering code. This would appear when recursive variable 95 blocks were defined (blocks with sub-blocks). 96 x Speedup changes in the variable reordering code 97 x The automatic reordering threshhold function has been changed 98 x Automatic reordering is now interrupting and restarts bdd operations 99 x Prototype for bdd_reorder_hook changed. 100 x Printing of reorder information (verbose level > 0) is changed. 101 x The threshold for stopping of the iterative reordering methods has 102 been changed. The reordering now continues until no progress is done 103 at all (before it would stop when less than 5% where gained). 104 x Added a few sanity checks to many of the functions. 105 x Bugfix (parameter checking) in fdd_ithvar. 106 - bdd_varlevel removed (use bdd_var2level and bdd_level2var). 107 108 109VER 1.6 (november 1998) 110----------------------- 111 + Added bdd_resetpair 112 + Added bdd_satcountset, bdd_satcountlnset 113 + Added macro bdd_relprod 114 + Added fdd_overlapdomain 115 + Added fdd_domain 116 x Fixed a bug in bdd_setvarnum and bdd_extvarnum. 117 x Fixed a bug in bdd_newpair() which would give problems with reordering. 118 x Speedup changes in bdd_exist, bdd_forall, bdd_appex, bdd_appall 119 x Speedup changes in bdd_restrict 120 x Changed bdd_gbc_hook to include both pre and post garbage collection. 121 122 123VER 1.5 (september 1998) 124------------------------ 125 + Added bdd_cofactor 126 + Added and fixed some error checks in fdd.c 127 x Fixed a bug in bdd_setvarnum(). 128 129 130VER 1.4 (july 1998) 131------------------- 132 The package just got a name: BuDDy 133 + Added functions bdd_compose, bdd_veccompose, bdd_ite. 134 + Added functions bdd_setbddpair, bdd_setbddpairs. 135 + Added functions bdd_var, bdd_low, bdd_high. 136 + Added technical documentation in docs/tech.txt 137 x Overloaded C++ functions are not used any more. This mainly changes 138 the name of the printing functions in C++. 139 x Changed datatype names (You'll hate me for this one): 140 BddPair -> bddPair 141 BddStat -> bddStat 142 BddGbcStat -> bddGbcStat 143 x Added slightly more documentation. 144 x Some internal changes to the code - should not be visible to users. 145 146 147VER 1.3 (june 1998) 148------------------- 149 x Fixed a few serious bugs in the reordering code 150 151 152VER 1.2 (june 1998) 153------------------- 154 + Added support for dynamic variable reordering 155 + Added reordering handler (bdd_reorder_hook) 156 + More added to the docs 157 x Changed the event handlers (bdd_xxx_hook) 158 159 160VER 1.1 (april 1998) 161-------------------- 162 + Added bdd_varprofile 163 + Added fdd_scanset 164 + Mucho better documentation. 165 + Added Henrik Reif Andersen's BDD notes to the documentation. 166 + Added BDD_REORDER_RANDOM for test purposes (usefull for others?) 167 x Fixed a bug in bdd_appex and bdd_appall. 168 x Fixed a bug in bdd_simplify. 169 x Speed fixup to fdd_extdomain 170 x Lots of small (insignificant?) bug fixes in fdd.c. 171 x bdd_load/save updated to take reordering into account. 172 x Generalized bdd_restrict to use a BDD variable set. 173 x Fixed the identifiers for the operator caches. 174 x The math functions log1p and pow2 has been removed as they didn't 175 exist on some systems. The same applies to M_LN2. 176 x New file structure and makefiles. 177 - Removed bdd_break, bdd_restart1 178 179 180