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.