ChangeLog 10.6 KB
Newer Older
1
2
3
4
5
2011-06-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/bddop.c (apply_rec, appquant_rec): Improve caching by
	reordering operands of commutative operators.

6
7
8
9
10
11
12
13
14
15
2011-06-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove some valgrind warnings about uninitialized memory when
	BddCache_lookup return an entry from a Not operation.

	* src/bddop.c (apply_rec, simplify_rec): When checking the cache
	entry, always check entry->a and entry->c before checking
	entry->b, because the "not_rec()" function does not initialize
	the latter.

16
17
18
19
20
21
2011-06-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* examples/cmilner/cmilner.c (A, transitions, initial_state)
	(reachable_states, has_deadlocks): Declare as static functions,
	to suppress a GCC warning.

22
23
24
25
26
27
28
29
30
31
32
33
34
2011-04-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Inline the "is bdd constant" check performed in copies/constructors.

	This avoids a library call to bdd_addref or bdd_delref.

	* src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function,
	that work only on BDD that are not constant.
	* src/cpext.cxx (bdd::operator=): Move...
	* src/bdd.hh (bdd::operator=): ... here.
	(bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant"
	check and call bdd_delref_nc/bdd_addref_nc only otherwise.

35
36
37
38
39
40
41
2011-04-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Hint gcc about likely/unlikely branches.

	* src/bdd.h (__likely, __unlikely): Introduce these two macros.
	* src/bddop.c, src/kerner.c: Use them in many situations.

42
43
44
45
2011-04-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/pairs.c (bdd_pairalloc): Fix prototype.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
46
47
48
49
50
51
52
53
54
2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix some warnings reported by gcc.

	* buddy/src/kernel.c (errorstrings): Mark these as const.
	* buddy/src/reorder.c (reorder_gbc): Fix prototype.
	(siftTestCmp): Add missing const in cast.
	(bdd_reorder_auto): Actually call bdd_reorder_ready().

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
55
56
57
58
59
60
61
62
63
64
65
66
2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add support for --enable-devel and similar macros.

	* m4/debug.m4: Rename to ...
	* m4/bdebug.m4: ... this.
	* m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New file.
	* m4/gccwarns.m4: Fix usage of cache variable.  Fix shell
	syntax.  Do not check for -Waggregate-return.  Update CFLAGS.
	* configure.ac: Adjust to handle --enable-devel and similar macros
	in the same way as Spot.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
67
68
69
70
71
72
73
74
75
76
2011-04-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Tag functions with attributes pure, const, or noreturn.

	* src/bdd.h (__purefn, __constfn, __noreturnfn): Define
	new macros.
	* src/bdd.h, src/bddio.c, src/bvec.h, src/imatrix.h: Use them
	to tag many functions as suggested by -Wsuggest-attribute=pure,
	-Wsuggest-attribute=const, -Wsuggest-attribute=noreturn.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
77
78
79
80
81
82
83
84
2011-04-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove more sanity checks when NDEBUG is set.

	* src/kernel.h (CHECKnc): New macro.
	* src/kernel.c (bdd_var, bdd_low, bdd_high, bdd_ithvar,
	bdd_nithvar): Use it.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
85
86
87
88
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/kernel.h (CHECK, CHECKa, CHECKn): Disable if NDEBUG is set.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
89
90
91
92
93
94
95
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix declaration of bddproduced.

	* src/reorder.c (bddproduced): Declare a longint, to match
	the definition in kerner.c.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
96
97
98
99
100
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* buddy/src/kernel.c (bdd_addref, bdd_delref): Disable sanity
	checks when compiled with NDEBUG.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
101
102
103
104
105
2011-02-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* examples/cmilner/Makefile.am (cmilner_LDADD): Link with -lm, to
	find the pow() function.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
106
107
108
109
110
2010-11-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/bddop.c (bdd_setxor): New function.
	* src/bdd.h (bdd_setxor): New function.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
111
112
113
114
115
116
117
118
119
2010-01-22  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Get rid of some "deprecated conversion from string constant to
	`char*'" warnings.

	* examples/bddcalc/parser_.h (yyerror): Declare the format
	as a "const char*".
	* examples/bddcalc/parser.yxx (yyerror): Likewise.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
120
121
122
123
124
2010-01-21  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/bddio.c (bdd_load): Check the return value of fscanf() to
	kill a warning.

Alexandre Duret-Lutz's avatar
[buddy]    
Alexandre Duret-Lutz committed
125
126
127
128
129
130
131
2009-11-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Introduce bdd_satprefix, to speedup spot::minato().

	* src/bdd.h (bdd_satprefix): New function.
	* src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions.

132
133
134
135
136
137
138
139
140
2009-10-01  Alexandre Duret-Lutz  <adl@lrde.epita.net>

	Fix the previous patch in reorder.c: I missread the
	function name in the Clang report...

	* src/reorder.c (reorder_win3): Do initialize THIS.
	(reorder_win3ite): Do not initialize THIS, its
	initial value is never read.

141
142
143
144
145
146
147
148
149
2009-09-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix some issues reported by LLVM/Clang's static analyser.

	* src/bddop.c (bdd_operator_varresize): Do not write into
	quantvarset if it could not be allocated.
	* src/reorder.c (reorder_win3): Do not initialize THIS, its
	initial value is never read.

150
151
152
153
154
2009-08-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and
	add an AC_CONFIG_MACRO_DIR call.

155
156
157
158
159
160
161
2009-06-12  Guillaume Sadegh  <sadegh@lrde.epita.fr>

	Adjust to support the Intel compiler (icc).

	* configure.ac: Adjust to call...
	* m4/intel.m4: ...this new macro.

162
163
164
165
2008-03-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/bddtest.cxx: Include <cstdlib> to compile with g++-4.3.

166
167
168
169
170
171
2007-09-19  Alexandre Duret-Lutz  <adl@gnu.org>

	* src/kernel.c (bdd_default_gbchandler): Log garbage collection to
	stderr, not stdout.  Reported by Kristin Yvonne Rozier
	<kyrozier@cs.rice.edu>.

172
173
2004-07-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

174
	* configure.ac: Call AC_LIBTOOL_WIN32_DLL
175
176
	* src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined.

177
178
179
180
181
2004-07-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as
	left-recursive rules.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
182
183
184
185
186
187
188
189
190
191
192
193
194
195
2004-06-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Merge BuDDy 2.3.
	* examples/calculator/, examples/internal/: Were renamed as ...
	* examples/bddcalc/, examples/bddtest/: ... these.
	* configure.ac: Adjust version and output Makefiles.
	* examples/Makefile.am (SUBDIRS): Adjust subdir renaming.
	* examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were
	renamed as ...
	* examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these.
	* examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust
	accordingly.
	* src/Makefile.am (AM_CPPFLAGS): Define VERSION.

196
197
198
199
200
201
2004-01-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/bddop.c (bdd_support): Free supportSet if it needs to be
	reallocated.  This fixes a memory leak reported by
	Souheib.Baarir@lip6.fr.

202
203
204
205
2003-11-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* examples/Makefile.def (AM_CPPFLAGS): Add -I$(srcdir).

206
207
2003-08-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

208
209
210
211
	* doc/Makefile.am (EXTRA_DIST): Replace buddy.ps by buddy.pdf
	(the latter has been rebuilt and on Jrn's request it explicitly
	mentions the differences with the 2.2 manual).

212
213
	* src/bddop.c (bdd_forallcomp, bdd_uniquecomp): Fix documentation.

214
215
2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
216
	* src/bdd.h (bdd_existcomp, bdd_forallcomp,
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
	bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp,
	bdd_appunicomp): Declare for C and C++.
	* src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC,
	CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC,
	CACHEID_APPUNCC): New macros.
	(quatvarsetcomp): New variables.
	(varset2vartable): Take a second argument to indicate negation,
	set quatvarsetcomp.
	(INVARSET): Honor quatvarsetcomp.
	(quantify): New function, extracted from bdd_exist, bdd_forall,
	and bdd_appunicomp.
	(bdd_exist, bdd_forall, bdd_appunicomp): Use quantify.
	(bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions.
	(appquantify): New function, extracted from bdd_appex, bdd_appall,
	and bdd_appuni.
	(bdd_appex, bdd_appall, bdd_appuni): Use appquantify.
	(bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions.

	* src/bddop.c (bdd_support): Return bddtrue when the support
	is empty, because variable sets are conjunctions.

238
239
2003-05-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

240
241
242
243
244
245
246
	* src/pairs.c (bdd_mergepairs): New function.
	(bdd_copypair): Revert 2003-05-20's change.  Use bdd_addref
	to copy result variables.
	* src/bdd.h (BDD_INVMERGE): New error code.
	(bdd_mergepairs): Declare.
	* src/kernel.c (errorstrings): Add string of BDDINV.

247
248
	* src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/.

249
250
2003-05-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

251
252
	* src/pairs.c (bdd_copypair): Use memcpy to copy from->result,
	and correctly copy p->last from from->last.
253

254
255
	* src/pairs.c (bdd_setbddpair): Fix prototype in documentation.

256
257
258
259
260
261
2003-05-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/bdd.h: Declare bdd_copypair().
	* src/pairs.c (bdd_copypair, bdd_pairalloc): New functions.
	(bdd_newpair): Use bdd_pairalloc.

262
263
264
265
2003-05-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1).

266
267
268
269
2003-05-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/bddop.c (bdd_allsat): Fix description.

270
271
2003-05-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

272
273
274
275
	* configure.ac: Output config.h.
	* src/kernel.h: Include it.
	* src/Makefile.am (AM_CPPFLAGS): New variable.

276
	* configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am,
277
	examples/Makefile.am, examples/Makefile.def,
278
	examples/adder/Makefile.am, examples/calculator/Makefile.am,
279
	examples/cmilner/Makefile.am, examples/fdd/Makefile.am,
280
281
282
283
284
285
286
287
288
289
	examples/internal/Makefile.am, examples/milner/Makefile.am,
	examples/money/Makefile.am, examples/queen/Makefile.am,
	examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4,
	ChangeLog, INSTALL: New files.
	* config, makefile, src/makefile, doc/makefile,
	examples/adder/makefile, examples/calculator/makefile
	examples/cmilner/makefile, examples/fdd/makefile,
	examples/internal/makefile, examples/milner/makefile,
	examples/money/makefile, examples/queen/makefile,
	examples/solitare/makefile : Delete.
290
	* examples/adder/adder.cxx, examples/fdd/statespace.cxx,
291
	examples/internal/bddtest.cxx, examples/milner/milner.cxx,
292
	examples/money/money.cxx, examples/queen/queen.cxx,
293
294
295
296
297
298
299
300
301
302
	examples/solitare/solitare.cxx: Include iostream.
	* examples/calculator/parser.y: Rename as ...
	* examples/calculator/parser.yxx: ... this.  Remove spurious
	comas in %token, %right, and %left arguments.
	* examples/calculator/parser.h: Rename as ...
	* examples/calculator/parser_.h: ... this, because the bison
	rule with output parser.h (not tokens.h) from parser.y.
	* examples/calculator/lexer.l: Rename as ...
	* examples/calculator/lexer.lxx: ... this.  Include parser.h
	instead of tokens.h.
303
	* examples/calculator/slist.h
304
305
306
307
	(voidSList::voisSListElem, SList::ite): Fix friend usage.
	* src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already
	defined.
	* README: Update build instruction, and file listing.