==========================================================================
                              *** BuDDy ***
                         Binary Decision Diagrams
                           Library Package v2.2a
--------------------------------------------------------------------------
               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
                            All rights reserved

    Permission is hereby granted, without written agreement and without
    license or royalty fees, to use, reproduce, prepare derivative
    works, distribute, and display this software and its documentation
    for any purpose, provided that (1) the above copyright notice and
    the following two paragraphs appear in all copies of the source code
    and (2) redistributions, including without limitation binaries,
    reproduce these notices in the supporting documentation. Substantial
    modifications to this software may be copyrighted by their authors
    and need not follow the licensing terms described here, provided
    that the new terms are clearly indicated in all files where they apply.

    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
    MODIFICATIONS.
==========================================================================



---------------------------------------------------------------------
--- REQUIREMENTS ----------------------------------------------------
---------------------------------------------------------------------

* A (not to old) C++ compiler
* A machine that supports 32 bit integers


---------------------------------------------------------------------
--- INSTALLING ------------------------------------------------------
---------------------------------------------------------------------

The following commands should build and install the library.

  ./configure
  make
  make install

`./configure' accepts many arguments to tune your installation.
The following options are noteworthy:

  --includedir=/somewhere/include   
    Specify where header files will be installed.

  --libdir=/somewhere/lib    
    Specify where libraries will be installed.

  --disable-shared
    Do not build the shared library for BuDDy.

  --disable-static
    Do not build the static library for BuDDy.

  --enable-swap-count
    Count number of fundamental variable swaps (for debugging)

  --enable-cache-stats
    Gather statistical information about operator and unique node 
    caching (for debugging)

Run `./configure --help' for a complete listing, and see
the INSTALL file for generic intrustions.

Run `make check' to build the examples.


---------------------------------------------------------------------
--- USING -----------------------------------------------------------
---------------------------------------------------------------------

Assuming that the files "bdd.h" and "libbdd.a" are in directories
"/usr/local/include" and "/usr/local/lib" then the compile command
could be:

 g++ -I/usr/local/include myfile.cc -o myfile -L/usr/local/lib -lbdd

Your machine may be setup to use the above directories auto-
matically, so you might be able to do:

 g++ myfile.cc -o myfile -lbdd


---------------------------------------------------------------------
--- FILES -----------------------------------------------------------
---------------------------------------------------------------------

src:           All files needed for the BuDDy package.
examples:      Example files
  fdd:         An example of use of the FDD interface.
  calculator:  An example of a BDD calculator. Uses reordering.
  adder:       Construction of a N-bit adder. Uses reordering.
  milner:      A calculation of the reachable statespace for Milner's
               scheduler. C++.
  cmilner:     As above but purely in ANSI-C.
  queen:       Solution to the N-queen chess problem.
  solitare:    Solution to a solitare game.
  money:       Solution to the send-more-money problem (bvec demo).
  internal:    Some internal regression tests.
doc:           Documentation.
  buddy.ps:    Package documentation.
  bddnotes.ps: BDD introduction notes.
tools:         Tools used during the build.
m4:            A couple of macros used to build ./configure.

---------------------------------------------------------------------
--- FEEDBACK --------------------------------------------------------
---------------------------------------------------------------------

Please do not hesitate to send any questions or bug reports to:

  Jorn Lind-Nielsen:  buddy@itu.dk
  (or maybe jorn_lind_nielsen@hotmail.com or jln@fjeldgruppen.dk)

It may take some time to get an answer since BuDDy do not have that
much focus any more - but I'll try to give a reasonable answer
in (finite) time.

New updates and other info can be found at:

  http://www.it-c.dk/research/buddy/
  (or http://www.itu.dk/research/buddy)


Hope you find some use for this software

      Jorn Lind-Nielsen

