reordering operands of commutative operators.

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.

(reachable_states, has_deadlocks): Declare as static functions,
to suppress a GCC warning.

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.

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

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().

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.

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.

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.

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

Fix declaration of bddproduced.

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

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

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

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

This reverts commit d462f50b.

Conflicts:

	buddy/ChangeLog

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.

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

Inline bdd_addref() and bdd_delref() to speedup BDD operations.

* src/kernel.c, src/kernel.h (bdd_addref, bdd_delref): Move these
functions and there associated global variables...
* src/bdd.c (bdd_error): ... and this function ...
* src/bdd.h (bdd_addref, bdd_delref, bdd_error): ...here so that
they can be inlined.

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

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

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

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

stderr, not stdout.  Reported by Kristin Yvonne Rozier
<kyrozier@cs.rice.edu>.

* src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined.

left-recursive rules.

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

reallocated.  This fixes a memory leak reported by
Souheib.Baarir@lip6.fr.

(the latter has been rebuilt and on Jørn's request it explicitly
mentions the differences with the 2.2 manual).

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.

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

(bdd_copypair): Revert 2003-05-20's change.  Use bdd_addref
to copy result variables.

and correctly copy p->last from from->last.