00001 /*! 00002 00003 \page INSTALL INSTALL 00004 00005 <strong>Contents:</strong> 00006 00007 <ul> 00008 <li>\ref quickstart</li> 00009 <li>\ref requirements</li> 00010 <li>\ref advanced</li> 00011 <li>\ref installing</li> 00012 <li>\ref documentation</li> 00013 <li>\ref faq</li> 00014 <li>\ref help</li> 00015 </ul> 00016 00017 \section quickstart Quick Start 00018 00019 You can download a source distribution of %CVC3 from the 00020 <a href="http://www.cs.nyu.edu/acsys/cvc3/download.html">CVC3 downloads 00021 page</a>. Save the source archive as <code>cvc3.tar.gz</code> in the 00022 directory of your choice and extract the contents using your favorite 00023 archive program (you can use <code>tar xzvf cvc3.tar.gz</code> from a 00024 terminal). This will create a directory containing the source of 00025 %CVC3, normally called <code>cvc3-XXX</code>. In the following we will 00026 denote the this directory as <code>$CVC3_SRC</code>. To build %CVC3, 00027 open your favorite terminal program and run the following sequence of 00028 commands 00029 00030 <pre> 00031 cd $CVC3_SRC 00032 ./configure 00033 make 00034 </pre> 00035 00036 If any part of the build process fails, please read the following section for more information. 00037 00038 A successful build will create a library <code>libcvc3</code> in the 00039 <code>$CVC3_SRC/lib</code> directory, and an executable 00040 <code>cvc3</code> in the <code>$CVC3_SRC/bin</code> directory (these 00041 are symbolic links to the actual files which are stored in 00042 architecture- and configuration-dependent subdirectories). The 00043 directory <code>$CVC3_SRC/test</code> contains an example program 00044 using the %CVC3 library <code>libcvc3</code>. To try it out, run the 00045 following commands in the terminal: 00046 00047 <pre> 00048 cd test 00049 make 00050 bin/test 00051 </pre> 00052 00053 By default, <code>make</code> will build optimized code, static 00054 libraries, and a static executable. To build the "debug" version (much 00055 slower but with more error checking) use the following configuration 00056 command instead: 00057 00058 <pre> 00059 ./configure --with-build=debug 00060 </pre> 00061 00062 In case you prefer to build shared libraries (and thus a much smaller 00063 executable), use the following configuration command: 00064 00065 <pre> 00066 ./configure --enable-dynamic 00067 </pre> 00068 00069 If you do choose to buld the shared libraries, you must set your 00070 <code>LD_LIBRARY_PATH</code> environment variable to 00071 <code>$CVC3_SRC/lib</code> before running %CVC3 or using the shared 00072 libraries. 00073 00074 Alternatively, these and other options can be changed by editing the 00075 <code>Makefile.local</code> file after running 00076 <code>configure</code>. However, be aware that re-running 00077 <code>configure</code> will overwrite any changes you have made to 00078 <code>Makefile.local</code>. 00079 00080 \section requirements Requirements 00081 00082 %CVC3 has the following build dependencies: 00083 00084 <ul> 00085 <li><a href="http://www.gnu.org/software/gcc/">GCC</a> version 3.0 or later</li> 00086 <li><a href="http://www.gnu.org/software/bash/">Bash</a></li> 00087 <li><a href="http://flex.sourceforge.net/">Flex</a></li> 00088 <li><a href="http://www.gnu.org/software/bison/">Bison</a></li> 00089 <li><a href="http://gmplib.org/">GMP</a> <em>(recommended)</em></li> 00090 <li>A <a href="http://python.org/">Python</a> interpreter 00091 <em>(optional, for Java support)</em></li> 00092 <li>A <a href="http://java.sun.com/">Java</a> compiler 00093 <em>(optional, for Java support)</em></li> 00094 </ul> 00095 00096 All of these tools are available from common package repositories 00097 (e.g., Debian, Ubuntu, Red Hat, Cygwin). 00098 00099 \section advanced Advanced Configuration 00100 00101 The configure script checks for the components needed to build %CVC3. 00102 If for some reason, the configure script is missing or doesn't run on 00103 your platform, you can recreate it from <code>configure.ac</code> by 00104 running <code>autoconf</code>. 00105 00106 As the configure script runs, if something is not found, it 00107 complains. configure looks for components in standard locations and 00108 also uses several environment variables that you can set to help it 00109 find things. In particular, you can set <code>CPPFLAGS</code> to 00110 "<code>-I $includeDir</code>" if you have headers in a nonstandard 00111 directory <code>$includeDir</code>, and <code>LDFLAGS</code> to 00112 "<code>-L $libDir</code>" if you have libraries in a nonstandard 00113 directory <code>$libDir</code>. Alternatively you can pass these 00114 directories to the <code>configure</code> script using the following 00115 command 00116 00117 <pre> 00118 ./configure --with-extra-includes=$includeDir --with-extra-libs=$libDir 00119 </pre> 00120 00121 Run <code>./configure --help</code> for a list of all such environment 00122 variables and options. 00123 00124 <h3> 00125 GMP 00126 </h3> 00127 00128 One of the components %CVC3 depends on is the GNU Multiple Precision (GMP) 00129 library. Many Unix-like distributions include gmp packages. 00130 00131 If you do not have GMP installed or your installation does not work, we 00132 recommend that you install it manually: 00133 00134 1. Download the GMP source code from http://gmplib.org/ 00135 00136 2. Unpack the sources, and from the root-directory of the GMP source code, run 00137 00138 <pre> 00139 ./configure 00140 make 00141 </pre> 00142 00143 On some Solaris machines, you may need to configure GMP with 00144 00145 <pre> 00146 ./configure ABI=32 00147 </pre> 00148 00149 to make the resulting GMP library compatible with the %CVC3 00150 libraries. The reason for this is that the default ABI that gcc 00151 chooses in %CVC3 compilation is not necessarily the default ABI 00152 that the GMP configure script selects, and one of them may need to be 00153 adjusted. 00154 00155 3. Now, either install GMP system-wide (make install), or supply the 00156 appropriate values for CPPFLAGS and LDFLAGS to the %CVC3 configure script. 00157 00158 If for some reason, you do not want to use GMP, you can configure %CVC3 to use 00159 native arithmetic by running: 00160 00161 <pre> 00162 ./configure --with-arith=native 00163 </pre> 00164 00165 If you compile %CVC3 with native arithmetic, it is possible that %CVC3 may fail 00166 as the result of arithmetic overflow. If an overflow occurs, you will get 00167 an error message and %CVC3 will abort. 00168 00169 <h3> 00170 Java interface 00171 </h3> 00172 00173 <em><strong>Note: The Java interface is experimental. The API may 00174 change in future releases.</strong></em> 00175 00176 To build the Java interface to %CVC3, use the 00177 <code>--enable-java</code> configuration option. The configuration 00178 script refers to the environment variables <code>JAVAC</code>, 00179 <code>JAVAH</code>, <code>JAR</code>, and <code>CXX</code> to set up 00180 the standard Java and C++ compiler commands. It refers to the 00181 environment variable <code>JFLAGS</code> for default Java compiler 00182 flags. It refers to the variable <code>javadir</code> for the 00183 installation directory of <code>libcvc3.jar</code>. 00184 00185 The configuration options <code>--with-java-home</code> and 00186 <code>--with-java-includes</code> can be used to specify the path to 00187 the directories containing the JDK installation and JNI header files, 00188 respectively. 00189 00190 You must build %CVC3 as a dynamic library to use the Java 00191 interface. For example, you might configure the build by running the 00192 following in the top-level %CVC3 directory: 00193 00194 <pre> 00195 ./configure --enable-dynamic --enable-java 00196 </pre> 00197 00198 <b>Note:</b> The Java interface depends on the "build type" (e.g., 00199 "optimized", "debug) of %CVC3. If you choose to re-configure and 00200 re-build %CVC3 with a different build type, you must run "make clean" 00201 in the current directory and re-build the interface (cleaning and 00202 rebuilding the entire %CVC3 package will suffice). 00203 00204 <h4> 00205 Using the Java interface 00206 </h4> 00207 00208 To access the library, you must add <code>libcvc3.jar</code> to the 00209 classpath (e.g., by setting the <code>CLASSPATH</code> environment 00210 variable) and both <code>libcvc3.so</code> and 00211 <code>libcvc3jni.so</code> to the runtime library path (e.g., by 00212 setting the <code>LD_LIBRARY_PATH</code> environment variable 00213 java.library.path JVM variable). 00214 00215 For example, to compile the class Client.java: 00216 00217 <pre> 00218 javac -cp lib/libcvc3.jar Client.java 00219 </pre> 00220 00221 To run: 00222 00223 <pre> 00224 export LD_LIBRARY_PATH=/path/to/cvc3/libs 00225 java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3.jar Client 00226 </pre> 00227 00228 <h3> 00229 .NET interface 00230 </h3> 00231 00232 <em><strong>Note: The .NET interface is experimental. The API may 00233 change in future releases.</strong></em> 00234 00235 A .NET interface to the %CVC3 library can be built using Visual Studio 00236 2005 or later. To build the interface: 00237 00238 <ol> 00239 <li>The lexers and parsers for the supported input languages need to be generated outside of Visual Studio. This can be done in two ways: 00240 <ul> 00241 <li>Use the lexer/parser files created by a Cygwin build. It suffices to run Make in <code>src/parser</code>: 00242 <pre> 00243 ./configure 00244 cd src/parser 00245 make 00246 </pre> 00247 </li> 00248 00249 <li>Run the script <code>make_parser.bat</code> in directory <code>src/parser</code> with the native Windows versions of <a href="http://gnuwin32.sourceforge.net/packages/flex.htm">Flex</a> and <a href="http://gnuwin32.sourceforge.net/packages/bison.htm">Bison</a>.</li> 00250 </ul> 00251 </li> 00252 <li>Open the solution file <code>windows/cvc3.sln</code> in Visual Studio. The solution file contains the following projects (each with Debug/Release versions): 00253 <ul> 00254 <li>cvc3lib: the C++ %CVC3 library</li> 00255 <li>cvc3: the %CVC3 command-line program</li> 00256 <li>cvc3test: tests for cvc3lib</li> 00257 <li>cvc3libcli: the .NET %CVC3 library</li> 00258 <li>cvc3cli: a C# clone of the %CVC3 command-line program</li> 00259 <li>cvc3testcli: tests for cvc3libcli</li> 00260 </ul> 00261 </li> 00262 </ol> 00263 00264 Each project can be built as usual with Visual Studio. Binaries will 00265 be put in the folders <code>windows/release</code> (for Release 00266 builds) and <code>windows/debug</code> (for Debug builds). 00267 00268 For more information, see the file <code>windows/INSTALL</code>. 00269 00270 <b>Note:</b> the .NET interface can only be used on Microsoft's CLR, 00271 because Visual Studio produces <a 00272 href="http://mono-project.com/CPlusPlus">mixed-mode assemblies</a>. 00273 00274 <h3> 00275 Mac OS X 00276 </h3> 00277 00278 Mac OS X uses <code>DYLD_LIBRARY_PATH</code> in place of 00279 <code>LD_LIBRARY_PATH</code>. 00280 00281 By default, %CVC3 compiles in 32-bit mode on 64-bit Intel Macs. Use 00282 <code>./configure --build=x86_64-darwin</code> to build in 64-bit 00283 mode. (See <a href="#64-bit Platforms">64-bit Platforms</a>.) 00284 00285 <h3> 00286 Cygwin 00287 </h3> 00288 00289 In order to use GMP on Cygwin, make sure the following packages are 00290 installed: gmp, libgmp-devel, libgmp3, bison, flex, and make, as well 00291 as standard UNIX tools. 00292 00293 On Windows, it's common to have directory names with embedded spaces. 00294 This can be problematic for the CVC3 build system. Therefore on 00295 Cygwin we recommend symbolically linking to names without embedded 00296 spaces, something like the following: 00297 00298 <pre> 00299 $ pwd 00300 /home/ACSys Group 00301 $ ln -s 'ACSys Group' /home/acsys 00302 $ export HOME=/home/acsys 00303 $ cd 00304 $ pwd 00305 /home/acsys 00306 $ cd cvc3 00307 $ ./configure --prefix=/home/acsys/cvc3.installation ...etc... 00308 </pre> 00309 00310 On Windows, Sun's JDK doesn't install the Java compiler "javac" into the 00311 standard path for executables. If you want to build Java bindings, 00312 you'll need to point CVC3 to it. Again using symbolic linking as above: 00313 00314 <pre> 00315 $ pwd 00316 /home/acsys/cvc3 00317 $ ln -s '/cygdrive/c/Program Files' /programs 00318 $ ./configure --enable-java --with-java-home=/programs/Java/jdk1.6.0_16 ... 00319 </pre> 00320 00321 Further, note that building CVC3 with dynamic libraries under cygwin is 00322 currently unsupported. If you encounter problems, please configure 00323 with --enable-static. 00324 00325 <h3> 00326 <a name="64-bit Platforms">64-bit Platforms</a> 00327 </h3> 00328 00329 When building %CVC3 on 64-bit platforms, you must compile %CVC3 in the 00330 same mode as any libraries it uses. For example, if GMP is compiled in 00331 64-bit mode, then %CVC3 must compiled in 64-bit mode as well. The 00332 configuration script will try to infer the correct compilation 00333 settings. You can run <code>./config.guess</code> to see the default 00334 platform type: 00335 00336 $ ./config.guess 00337 i686-pc-linux-gnu 00338 00339 You can use the <code>--build</code> argument to 00340 <code>configure</code> to override the default. For example, to 00341 compile in 64-bit mode on a x86-64 CPU, you can use <code>./configure 00342 --build=x86_64-pc-linux-gnu</code>. 00343 00344 <h3> 00345 Other Configuration Options 00346 </h3> 00347 00348 Other configuration options include where to install the results of 00349 "make install" (see below), what type of build to use (optimized, 00350 debug, gprof, or gcov), and whether to use static or dynamic 00351 libraries. For help on these options, type 00352 00353 <pre> 00354 ./configure --help 00355 </pre> 00356 00357 configure creates the file Makefile.local which stores all of the 00358 configuration information. If you want to customize your build 00359 without re-running configure, or if you want to customize it in a way 00360 that configure does not allow, you can do it by editing 00361 Makefile.local. For example, you can build a debug, gprof version by 00362 editing Makefile.local and setting OPTIMIZED to 0 and GPROF to 1 (by 00363 default, gprof runs with an optimized executable). Note that for most 00364 configuration options, the objects, libraries, and executables are 00365 stored in a configuration-dependent directory, with only symbolic 00366 links being stored in the main bin and lib directories. This allows 00367 you to easily maintain multiple configurations and multiple platforms 00368 using the same source tree. 00369 00370 <h4> 00371 Additional make options 00372 </h4> 00373 00374 To rebuild dependencies, type: 00375 00376 <pre> 00377 make depend 00378 </pre> 00379 00380 To remove just the executable or libraries in the current 00381 configuration, type: 00382 00383 <pre> 00384 make spotty 00385 </pre> 00386 00387 To remove in addition all object files and makefile dependencies for 00388 the current configuration, type: 00389 00390 <pre> 00391 make clean 00392 </pre> 00393 00394 To remove all files that are not part of the distribution (including 00395 all object, library, and executables built for any configuration or 00396 platform), type: 00397 00398 <pre> 00399 make distclean 00400 </pre> 00401 00402 To build a tarball distribution of the current source tree, type: 00403 00404 <pre> 00405 make dist 00406 </pre> 00407 00408 \section installing Installing CVC3 00409 00410 To install %CVC3 system-wide, (assuming you have already run configure) 00411 run: 00412 00413 <pre> 00414 make install 00415 </pre> 00416 00417 Installation depends on two configuration options: <code>prefix</code> 00418 and <code>exec_prefix</code>. By default, both are set to 00419 <code>/usr/local</code>, but these can be overridden by specifying the 00420 correct arguments to configure or by editing 00421 <code>Makefile.local</code>. 00422 00423 Installation copies all necessary header files to 00424 <code>$prefix/include/cvc3</code>. It installs the library 00425 <code>libcvc3</code> in <code>$exec_prefix/lib</code> and the 00426 executable <code>cvc3</code> in <code>$exec_prefix/bin</code>. By 00427 default, a static library and executable are installed. If you want 00428 to install shared library versions, configure for shared libraries as 00429 described above. 00430 00431 00432 \section documentation Documentation 00433 00434 To build HTML documentation, run 00435 00436 <pre> 00437 00438 make doc 00439 00440 </pre> 00441 00442 Then open <code>doc/html/index.html</code> in your favorite browser. 00443 00444 \section faq Frequently Asked Questions 00445 00446 <h3> 00447 Configuration Errors 00448 </h3> 00449 00450 <h4> 00451 <code>libgmp.a is not found</code> 00452 </h4> 00453 00454 Make sure the GMP library is in your <code>LD_LIBRARY_PATH</code> and 00455 <code>gmp.h</code> is in your <code>CPATH</code> (or use the 00456 <code>--with-extra-lib</code> and <code>--with-extra-include</code> 00457 arguments to <code>./configure</code>). 00458 00459 If your paths are properly configured and you are compiling for a 00460 64-bit architecture, you may have a 32/64-bit mismatch. Check the 00461 binary type of the GMP library using the <code>file</code> 00462 utility. For example, running <code>file</code> on a 32-bit Linux GMP 00463 shared library will return: 00464 00465 <pre> 00466 $ file /usr/lib/libgmp.so.3.4.2 00467 /usr/lib/libgmp.so.3.4.2: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked, stripped 00468 </pre> 00469 00470 You can use the <code>--build</code> arguments to 00471 <code>./configure</code> to set the target binary type for %CVC3. For 00472 example, <code>./configure --build=i686-linux-gnu</code> or 00473 <code>./configure --build=x86_64-linux-gnu</code>. 00474 00475 <h4> 00476 <code>Unable to locate Java directories</code> 00477 </h4> 00478 00479 Set the <code>JAVA_HOME</code> environment variable or use the 00480 <code>--with-java-home</code> argument to 00481 <code>./configure</code>. Some typical <code>JAVA_HOME</code> settings 00482 are as follows (where <em>X.Y.Z</em> is the version number of the installed 00483 Java runtime). 00484 00485 <table> 00486 <tr> 00487 <th> Platform </th><th> <code>JAVA_HOME</code> </th><th> Notes 00488 </th></tr> 00489 <tr> 00490 <td> Debian/Ubuntu Linux </td> 00491 <td> <code>/usr/lib/jvm/default-java</code> </td> 00492 <td> Install the <code>default-jre</code> or 00493 <code>default-jre-headless</code> package </td></tr> 00494 <tr> 00495 <td> Fedora Linux </td> 00496 <td> <code>/usr/java/jre<em>X.Y.Z</em></code> </td> 00497 <td> </td></tr> 00498 <tr> 00499 <td> Mac OS X </td> 00500 <td> <code>/System/Library/Frameworks/JavaVM.framework/Home</code> </td> 00501 <td> </td></tr> 00502 <tr> 00503 <td> Windows </td> 00504 <td> <code>C:\\Program Files\\Java\\jdk<em>X.Y.Z</em></code> </td> 00505 <td> </td></tr> 00506 </table> 00507 00508 <h3> 00509 Runtime Errors (CVC3 library) 00510 </h3> 00511 00512 <h4>Segmentation fault when running a dynamically-linked executable.</h4> 00513 00514 This can be caused by a mismatched "build type". The debug and 00515 optimized version of the %CVC3 shared library are not binary 00516 compatible. If you are linking against a debug version of the shared 00517 library, you must define the symbol _CVC3_DEBUG_MODE during 00518 compilation. E.g., add <code>-D_CVC3_DEBUG_MODE</code> to 00519 <code>CXXARGS</code>. 00520 00521 <h4>Fatal error: <code>Mis-handled the ref. counting</code></h4> 00522 00523 This can be cause by a number of problems. Make sure that all <code>Expr</code> 00524 objects are out of scope or have been manually deleted before deleting 00525 the <code>ValidityChecker</code>. 00526 00527 <h4> 00528 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path</code> 00529 </h4> 00530 00531 The Java runtime was not able to find the %CVC3 JNI library. Use 00532 <code>java -Djava.library.path=PATH_TO_CVC3JNI</code>, where 00533 <code>PATH_TO_CVC3JNI</code> is the directory containing the file 00534 <code>libcvc3jni.so</code>. 00535 00536 <h4> 00537 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: libcvc3jni.so.<em>x.y.z</em></code> 00538 </h4> 00539 00540 The Java runtime was not able to satisfy the link dependencies of the 00541 %CVC3 JNI library. Make sure that the %CVC3 and GMP libraries are in 00542 your <code>LD_LIBRARY_PATH</code>. 00543 00544 If your paths are properly configured and you are compiling for a 00545 64-bit architecture, you may have a 32/64-bit mismatch. Make sure the 00546 JVM is running in the same mode as the %CVC3 library using the 00547 <code>-d32</code> or <code>-d64</code> argument to <code>java</code>. 00548 00549 <h4> 00550 On Mac: 00551 <code>terminate called after throwing an instance of 'CVC3::TypecheckException'</code> 00552 </h4> 00553 00554 This appears to be a bug in certain versions of GCC distributed by 00555 Apple. Upgrade to XCode 3.1.2 or later (GCC version "4.0.1 (Apple 00556 Inc. build 5490)") or configure with <code>CXXFLAGS=-01</code>. 00557 00558 \section help Getting help 00559 00560 If you find a problem with the instructions in this installation guide, please 00561 send email to <a href="mailto:cvc-bugs@cs.nyu.edu">cvc-bugs@cs.nyu.edu</a>. 00562 00563 */