source: vis_dev/cusp-1.1/README @ 23

Last change on this file since 23 was 12, checked in by cecile, 13 years ago

cusp added

File size: 6.6 KB
Line 
1This is release 1.1 of CUSP, a system that combines CirCUs(SAT solver)
2and Sateen(SMT solver).
3
4To build CUSP, you will need
5
6   * An ANSI C compiler (gcc will do, as will several versions of cc)
7   * GNU Flex version 2.5 or greater
8   * GNU Bison version 1.22 or greater
9   * GMP Arithmetic Library
10   * GNU's make utility
11   * GNU's gzip utility
12   * Approximately 90 MB of free disk space for the build of cusp
13   * Approximately 60 MB of free disk space for the installation
14
15---------------------------------------------------------------------------
16* Changes from previous release
17
18  - Command line options to enable the preprocessor of CirCUs
19  - Command line options to suppress printing satisfying assignment in CirCUs.
20    By default, CirCUs will print out satisfying assignment.
21  - Recent version of CirCUs
22  - Recent version of Sateen
23
24
25---------------------------------------------------------------------------
26* Useful Addresses
27
28The most recent versions of CUSP:
29
30        http://vlsi.colorado.edu/
31
32The most recent version of the GMP:
33
34        http://gmplib.org/
35
36The most recent version of the GNU tools:
37
38        http://www.gnu.org
39
40---------------------------------------------------------------------------
41* Platforms
42
43This is the list of architecture/operating system/compiler
44combinations we have tested. (For installation with compilers marked
45with (*) please refer to the Platform Specific Instructions.)
46
47        * Intel ix86 / Linux / gcc, g++, icc
48        * Intel ix86 / Windows XP with Cygwin 1.5.16-1 / gcc, g++(*)
49
50The following instructions are for the generic build process.  Before
51building the tool please refer to the section "Platform Specific
52Instructions".
53
54---------------------------------------------------------------------------
55* Building CUSP
56
57To build a CUSP executable for a single operating system:
58
591. Download the most recent versions of CUSP from the address above
60into a convenient directory, (e.g., /tmp).
61
622. Move to where you would like to build CUSP and unpack the
63distributions:
64
65        % cd /home/cusp                                  # for example
66        % gzip -dc /tmp/cusp-1.1.tar.gz | tar xf -
67
683. Move into the common directory and run configure, which will
69   determine some system-specific parameters and create the Makefile:
70
71        % cd cusp-1.1/common
72        % ./configure
73
74   By default, this will use your system's native compiler.  To use gcc,
75
76        % ./configure --enable-gcc
77
78   (You may want to do this because you don't have the native compiler
79   installed or because it is not ANSI.)
80
81   Note: If you want to compile 32 bit version of CUSP in 64 bit machine,
82
83        % ./configure --enable-gcc="gcc -m32"
84
85   (You need to compile 32 bit version of GMP library and specify the
86   path manually.)
87
88   Note: For platforms where CUSP is not supported for the native compiler,
89   the default compiler is set to gcc.
90
91   Note: Not all checks in ./configure will return "yes."  This is
92   normal and should not affect compilation.  However, do be concerned
93   with any warnings "configure" produces.
94
95   Note: Occasionally, configure will make a bad guess or will choose
96   a default you do not want.  In this case, simply edit the Makefile
97   after configure finishes.
98
99   Note: You may want to specify parameters to configure -- see the
100   "Installing" sections below.
101
102   Note: The Makefile by default uses the "-g" option for
103   compilation.  The resultant "vis" executable may be much larger than
104   the executable generated without using the "-g" option.  Using the
105   "-g" option however, provides debugging capabilities.
106
107   Note: The following is of interest only to people developing code
108   within cusp.  For full debugging support, specify
109   --with-comp-mode=debug.  This will turn off optimization, and turn
110   on the assertions (sanity checks) in the code.  Similarly,
111
1124. Build the GLU system by running GNU's make utility:
113
114        % make
115
116   This builds an executable "cusp" in the current directory.
117
118   WARNING: If you are not successful in building a CUSP executable,
119   double check that you are using Flex version 2.5 or greater (check
120   using "flex -V") and GNU Bison version 1.22 or greater (check with
121   "bison -V").  Having out-of-date versions of these programs can
122   lead to obscure compilation and linking errors.  You can download
123   the new versions from the GNU FTP address above.  CUSP for SMT
124   solver only works with GMP Arithmetic Library.  If GMP Arithmetic
125   Libarary is not installed, CUSP works as SAT solver.
126
127
1285. OPTIONAL: Verify CUSP works by running it on some of the examples
129   included in the distribution:
130
131        % make check
132
133   This step finishes in less than five minutes on most machines
134   and requires approximately 32MB of RAM.
135
136---------------------------------------------------------------------------
137* Installing CUSP:
138
139Administrators and people who want to discard the source files after
140building VIS may install VIS in a central area:
141
142To install the CUSPS executable, library, headers, and help files, type,
143while in the cusp-1.1 directory,
144
145        % make install
146
147By default, this will put binaries, libraries, headers, and help files
148in /usr/local/bin, /usr/local/lib, /usr/local/include, and
149/usr/local/share respectively.  To choose a different location,
150provide a default prefix when you invoke configure, e.g., to install
151in /projects/cusp/bin, etc., use
152
153        % ./configure --prefix=/projects/cusp
154
155when configuring CUSP.
156
157"make clean" removes all the files generated during "make."  This is
158useful when you want to rebuild VIS with a different prefix,
159different compiler options, etc.
160
161---------------------------------------------------------------------------
162* Files in the CUSP distribution:
163
164README          This file.
165
166INSTALL         Generic installation instructions for use with configure,
167                including instructions for simultaneous multi-platform
168                builds.  These are not specific to CUSP, so don't
169                follow them word for word.
170
171configure       An executable shell script that creates "Makefile" from
172                Makefile.in after determining system-specific parameters.
173
174configure.in    Autoconf source for generating the configure file.
175                Only needed if you want to modify the configure script.
176
177Makefile.in     The template Makefile.
178
179helpers/        Programs useful during configuration and building
180 install-sh     Shell scripts used by "make install."
181 mkinstalldirs
182 config.guess
183 config.sub
184 dependency.make
185
186src/*/          Source code and headers for the CUSP system.
187
188obj/            Directory where .o files and generated .c files are
189                placed during a build.
190
191checkresults/   Directory where tests (i.e., make check) are run.
192                Results of the tests are placed here.  The directory
193                is only created when 'make check' is run.
194
Note: See TracBrowser for help on using the repository browser.