source: vis_dev/cusp-1.1/README @ 12

This is release 1.1 of CUSP, a system that combines CirCUs(SAT solver)
and Sateen(SMT solver).

To build CUSP, you will need

   * An ANSI C compiler (gcc will do, as will several versions of cc)
   * GNU Flex version 2.5 or greater
   * GNU Bison version 1.22 or greater
   * GMP Arithmetic Library
   * GNU's make utility
   * GNU's gzip utility
   * Approximately 90 MB of free disk space for the build of cusp
   * Approximately 60 MB of free disk space for the installation

---------------------------------------------------------------------------
* Changes from previous release

  - Command line options to enable the preprocessor of CirCUs
  - Command line options to suppress printing satisfying assignment in CirCUs. 
    By default, CirCUs will print out satisfying assignment.
  - Recent version of CirCUs
  - Recent version of Sateen


---------------------------------------------------------------------------
* Useful Addresses

The most recent versions of CUSP:

        http://vlsi.colorado.edu/

The most recent version of the GMP:

        http://gmplib.org/

The most recent version of the GNU tools:

        http://www.gnu.org

---------------------------------------------------------------------------
* Platforms

This is the list of architecture/operating system/compiler
combinations we have tested. (For installation with compilers marked
with (*) please refer to the Platform Specific Instructions.)

        * Intel ix86 / Linux / gcc, g++, icc
        * Intel ix86 / Windows XP with Cygwin 1.5.16-1 / gcc, g++(*)

The following instructions are for the generic build process.  Before
building the tool please refer to the section "Platform Specific
Instructions".

---------------------------------------------------------------------------
* Building CUSP

To build a CUSP executable for a single operating system:

1. Download the most recent versions of CUSP from the address above
into a convenient directory, (e.g., /tmp).

2. Move to where you would like to build CUSP and unpack the
distributions:

        % cd /home/cusp                                  # for example
        % gzip -dc /tmp/cusp-1.1.tar.gz | tar xf -

3. Move into the common directory and run configure, which will
   determine some system-specific parameters and create the Makefile:

        % cd cusp-1.1/common
        % ./configure

   By default, this will use your system's native compiler.  To use gcc,

        % ./configure --enable-gcc

   (You may want to do this because you don't have the native compiler
   installed or because it is not ANSI.)

   Note: If you want to compile 32 bit version of CUSP in 64 bit machine,

        % ./configure --enable-gcc="gcc -m32"

   (You need to compile 32 bit version of GMP library and specify the 
   path manually.)

   Note: For platforms where CUSP is not supported for the native compiler,
   the default compiler is set to gcc.

   Note: Not all checks in ./configure will return "yes."  This is
   normal and should not affect compilation.  However, do be concerned
   with any warnings "configure" produces.

   Note: Occasionally, configure will make a bad guess or will choose
   a default you do not want.  In this case, simply edit the Makefile
   after configure finishes.

   Note: You may want to specify parameters to configure -- see the
   "Installing" sections below.

   Note: The Makefile by default uses the "-g" option for
   compilation.  The resultant "vis" executable may be much larger than
   the executable generated without using the "-g" option.  Using the
   "-g" option however, provides debugging capabilities.

   Note: The following is of interest only to people developing code
   within cusp.  For full debugging support, specify
   --with-comp-mode=debug.  This will turn off optimization, and turn
   on the assertions (sanity checks) in the code.  Similarly,

4. Build the GLU system by running GNU's make utility:

        % make

   This builds an executable "cusp" in the current directory.

   WARNING: If you are not successful in building a CUSP executable,
   double check that you are using Flex version 2.5 or greater (check
   using "flex -V") and GNU Bison version 1.22 or greater (check with
   "bison -V").  Having out-of-date versions of these programs can
   lead to obscure compilation and linking errors.  You can download
   the new versions from the GNU FTP address above.  CUSP for SMT
   solver only works with GMP Arithmetic Library.  If GMP Arithmetic
   Libarary is not installed, CUSP works as SAT solver.


5. OPTIONAL: Verify CUSP works by running it on some of the examples
   included in the distribution:

        % make check

   This step finishes in less than five minutes on most machines
   and requires approximately 32MB of RAM.

---------------------------------------------------------------------------
* Installing CUSP:

Administrators and people who want to discard the source files after
building VIS may install VIS in a central area:

To install the CUSPS executable, library, headers, and help files, type,
while in the cusp-1.1 directory,

        % make install

By default, this will put binaries, libraries, headers, and help files
in /usr/local/bin, /usr/local/lib, /usr/local/include, and
/usr/local/share respectively.  To choose a different location,
provide a default prefix when you invoke configure, e.g., to install
in /projects/cusp/bin, etc., use

        % ./configure --prefix=/projects/cusp

when configuring CUSP.

"make clean" removes all the files generated during "make."  This is
useful when you want to rebuild VIS with a different prefix,
different compiler options, etc.

---------------------------------------------------------------------------
* Files in the CUSP distribution:

README          This file.

INSTALL         Generic installation instructions for use with configure, 
                including instructions for simultaneous multi-platform 
                builds.  These are not specific to CUSP, so don't 
                follow them word for word.

configure       An executable shell script that creates "Makefile" from
                Makefile.in after determining system-specific parameters.

configure.in    Autoconf source for generating the configure file.
                Only needed if you want to modify the configure script.

Makefile.in     The template Makefile.

helpers/        Programs useful during configuration and building
 install-sh     Shell scripts used by "make install."
 mkinstalldirs
 config.guess
 config.sub
 dependency.make

src/*/          Source code and headers for the CUSP system.

obj/            Directory where .o files and generated .c files are
                placed during a build.

checkresults/   Directory where tests (i.e., make check) are run.
                Results of the tests are placed here.  The directory
                is only created when 'make check' is run.