[Buddy-developers] bits to merge?

[Alexandre Duret-L. <ad...@sr...>]

Hi there,

I'm glad to learn BuDDy is reviving.

Over the last year I have been maintaining my own copy of BuDDy.
I had to fix a few bugs, and added a couple of feature needed
for the development of Spot (a model-checking library).

You can find the BuDDy version I'm using in the spot distribution
available at http://spot.lip6.fr/.  The main changes are:

  - build with autoconf+automake+libtool for better integration into
    similar source trees
  - new functions:
      bdd_existcomp, bdd_forallcomp, bdd_uniquecomp,=20
      bdd_appexcomp, bdd_appallcomp, bdd_appunicomp
         these are similar to the existing version without
         *comp, but these complement the BDD set given
      bdd_mergepairs, bdd_copypairs
         merge or copy pairs (I don't use these anymore, but they
         were useful at some point)
  - bug fixes:
      * bdd_support should return bddtrue when the support is empty.
      * Memory leak in bdd_support.
      * Spurious coma in the calculator grammar.
      * various typos in documentation
  - usability improvement:
      arrange so that bdd_default_errhandler coredumps on fatal errors,
      so we can debug more easily.

I'd be happy if any of these could be merged back into mainline.
Below is the detailed list of the changes I made.  I can send diffs
for any of these on request.

2004-01-07  Alexandre Duret-Lutz  <ad...@sr...>

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

2003-11-14  Alexandre Duret-Lutz  <ad...@sr...>

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

2003-08-06  Alexandre Duret-Lutz  <ad...@sr...>

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

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

2003-07-17  Alexandre Duret-Lutz  <ad...@sr...>

	* src/bdd.h (bdd_existcomp, bdd_forallcomp,
	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.

2003-05-22  Alexandre Duret-Lutz  <ad...@sr...>

	* 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.

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

2003-05-20  Alexandre Duret-Lutz  <ad...@sr...>

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

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

2003-05-19  Alexandre Duret-Lutz  <ad...@sr...>

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

2003-05-12  Alexandre Duret-Lutz  <ad...@sr...>

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

2003-05-07  Alexandre Duret-Lutz  <ad...@sr...>

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

2003-05-05  Alexandre Duret-Lutz  <ad...@sr...>

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

	* configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am,
	examples/Makefile.am, examples/Makefile.def,
	examples/adder/Makefile.am, examples/calculator/Makefile.am,
	examples/cmilner/Makefile.am, examples/fdd/Makefile.am,
	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.
	* examples/adder/adder.cxx, examples/fdd/statespace.cxx,
	examples/internal/bddtest.cxx, examples/milner/milner.cxx,
	examples/money/money.cxx, examples/queen/queen.cxx,
	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.
	* examples/calculator/slist.h
	(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.

--=20
Alexandre Duret-Lutz