5 <strong>Contents:</strong>
8 <li>\ref quickstart</li>
9 <li>\ref requirements</li>
10 <li>\ref advanced</li>
11 <li>\ref installing</li>
12 <li>\ref documentation</li>
17 \section quickstart Quick Start
19 You can download a source distribution of %CVC3 from the
20 <a href="http://www.cs.nyu.edu/acsys/cvc3/download.html">CVC3 downloads
21 page</a>. Save the source archive as <code>cvc3.tar.gz</code> in the
22 directory of your choice and extract the contents using your favorite
23 archive program (you can use <code>tar xzvf cvc3.tar.gz</code> from a
24 terminal). This will create a directory containing the source of
25 %CVC3, normally called <code>cvc3-XXX</code>. In the following we will
26 denote the this directory as <code>$CVC3_SRC</code>. To build %CVC3,
27 open your favorite terminal program and run the following sequence of
36 If any part of the build process fails, please read the following section for more information.
38 A successful build will create a library <code>libcvc3</code> in the
39 <code>$CVC3_SRC/lib</code> directory, and an executable
40 <code>cvc3</code> in the <code>$CVC3_SRC/bin</code> directory (these
41 are symbolic links to the actual files which are stored in
42 architecture- and configuration-dependent subdirectories). The
43 directory <code>$CVC3_SRC/test</code> contains an example program
44 using the %CVC3 library <code>libcvc3</code>. To try it out, run the
45 following commands in the terminal:
53 By default, <code>make</code> will build optimized code, static
54 libraries, and a static executable. To build the "debug" version (much
55 slower but with more error checking) use the following configuration
59 ./configure --with-build=debug
62 In case you prefer to build shared libraries (and thus a much smaller
63 executable), use the following configuration command:
66 ./configure --enable-dynamic
69 If you do choose to buld the shared libraries, you must set your
70 <code>LD_LIBRARY_PATH</code> environment variable to
71 <code>$CVC3_SRC/lib</code> before running %CVC3 or using the shared
74 Alternatively, these and other options can be changed by editing the
75 <code>Makefile.local</code> file after running
76 <code>configure</code>. However, be aware that re-running
77 <code>configure</code> will overwrite any changes you have made to
78 <code>Makefile.local</code>.
80 \section requirements Requirements
82 %CVC3 has the following build dependencies:
85 <li><a href="http://www.gnu.org/software/gcc/">GCC</a> version 3.0 or later</li>
86 <li><a href="http://www.gnu.org/software/bash/">Bash</a></li>
87 <li><a href="http://flex.sourceforge.net/">Flex</a></li>
88 <li><a href="http://www.gnu.org/software/bison/">Bison</a></li>
89 <li><a href="http://gmplib.org/">GMP</a> <em>(recommended)</em></li>
90 <li>A <a href="http://python.org/">Python</a> interpreter
91 <em>(optional, for Java support)</em></li>
92 <li>A <a href="http://java.sun.com/">Java</a> compiler
93 <em>(optional, for Java support)</em></li>
96 All of these tools are available from common package repositories
97 (e.g., Debian, Ubuntu, Red Hat, Cygwin).
99 \section advanced Advanced Configuration
101 The configure script checks for the components needed to build %CVC3.
102 If for some reason, the configure script is missing or doesn't run on
103 your platform, you can recreate it from <code>configure.ac</code> by
104 running <code>autoconf</code>.
106 As the configure script runs, if something is not found, it
107 complains. configure looks for components in standard locations and
108 also uses several environment variables that you can set to help it
109 find things. In particular, you can set <code>CPPFLAGS</code> to
110 "<code>-I $includeDir</code>" if you have headers in a nonstandard
111 directory <code>$includeDir</code>, and <code>LDFLAGS</code> to
112 "<code>-L $libDir</code>" if you have libraries in a nonstandard
113 directory <code>$libDir</code>. Alternatively you can pass these
114 directories to the <code>configure</code> script using the following
118 ./configure --with-extra-includes=$includeDir --with-extra-libs=$libDir
121 Run <code>./configure --help</code> for a list of all such environment
122 variables and options.
128 One of the components %CVC3 depends on is the GNU Multiple Precision (GMP)
129 library. Many Unix-like distributions include gmp packages.
131 If you do not have GMP installed or your installation does not work, we
132 recommend that you install it manually:
134 1. Download the GMP source code from http://gmplib.org/
136 2. Unpack the sources, and from the root-directory of the GMP source code, run
143 On some Solaris machines, you may need to configure GMP with
149 to make the resulting GMP library compatible with the %CVC3
150 libraries. The reason for this is that the default ABI that gcc
151 chooses in %CVC3 compilation is not necessarily the default ABI
152 that the GMP configure script selects, and one of them may need to be
155 3. Now, either install GMP system-wide (make install), or supply the
156 appropriate values for CPPFLAGS and LDFLAGS to the %CVC3 configure script.
158 If for some reason, you do not want to use GMP, you can configure %CVC3 to use
159 native arithmetic by running:
162 ./configure --with-arith=native
165 If you compile %CVC3 with native arithmetic, it is possible that %CVC3 may fail
166 as the result of arithmetic overflow. If an overflow occurs, you will get
167 an error message and %CVC3 will abort.
173 <em><strong>Note: The Java interface is experimental. The API may
174 change in future releases.</strong></em>
176 To build the Java interface to %CVC3, use the
177 <code>--enable-java</code> configuration option. The configuration
178 script refers to the environment variables <code>JAVAC</code>,
179 <code>JAVAH</code>, <code>JAR</code>, and <code>CXX</code> to set up
180 the standard Java and C++ compiler commands. It refers to the
181 environment variable <code>JFLAGS</code> for default Java compiler
182 flags. It refers to the variable <code>javadir</code> for the
183 installation directory of the CVC3 Java library.
185 The configuration options <code>--with-java-home</code> and
186 <code>--with-java-includes</code> can be used to specify the path to
187 the directories containing the JDK installation and JNI header files,
190 You must build %CVC3 as a dynamic library to use the Java
191 interface. For example, you might configure the build by running the
192 following in the top-level %CVC3 directory:
195 ./configure --enable-dynamic --enable-java
198 <b>Note:</b> The Java interface depends on the "build type" (e.g.,
199 "optimized", "debug") of %CVC3. If you choose to re-configure and
200 re-build %CVC3 with a different build type, you must run "make clean"
201 in the current directory and re-build the interface (cleaning and
202 rebuilding the entire %CVC3 package will suffice).
205 Using the Java interface
208 To access the library, you must add the file
209 <code>libcvc3-X.Y.Z.jar</code> (where "X.Y.Z" is the CVC3 version) to
210 the classpath (e.g., by setting the <code>CLASSPATH</code> environment
211 variable) and both <code>libcvc3.so</code> and
212 <code>libcvc3jni.so</code> to the runtime library path (e.g., by
213 setting the <code>LD_LIBRARY_PATH</code> environment variable
214 java.library.path JVM variable).
216 For example, to compile the class Client.java:
219 javac -cp lib/libcvc3-X.Y.Z.jar Client.java
225 export LD_LIBRARY_PATH=/path/to/cvc3/libs
226 java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3-X.Y.Z.jar Client
229 <!-- !!! THE .NET INTERFACE IS NO LONGER SUPPORTED !!!
234 <em><strong>Note: The .NET interface is experimental. The API may
235 change in future releases.</strong></em>
237 A .NET interface to the %CVC3 library can be built using Visual Studio
238 2005 or later. To build the interface:
241 <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:
243 <li>Use the lexer/parser files created by a Cygwin build. It suffices to run Make in <code>src/parser</code>:
251 <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>
254 <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):
256 <li>cvc3lib: the C++ %CVC3 library</li>
257 <li>cvc3: the %CVC3 command-line program</li>
258 <li>cvc3test: tests for cvc3lib</li>
259 <li>cvc3libcli: the .NET %CVC3 library</li>
260 <li>cvc3cli: a C# clone of the %CVC3 command-line program</li>
261 <li>cvc3testcli: tests for cvc3libcli</li>
266 Each project can be built as usual with Visual Studio. Binaries will
267 be put in the folders <code>windows/release</code> (for Release
268 builds) and <code>windows/debug</code> (for Debug builds).
270 For more information, see the file <code>windows/INSTALL</code>.
272 <b>Note:</b> the .NET interface can only be used on Microsoft's CLR,
273 because Visual Studio produces <a
274 href="http://mono-project.com/CPlusPlus">mixed-mode assemblies</a>.
281 Mac OS X uses <code>DYLD_LIBRARY_PATH</code> in place of
282 <code>LD_LIBRARY_PATH</code>.
284 On Intel Macs, by default, %CVC3 compiles in 32-bit or 64-bit mode
285 based on the compiler's default. If you want to build as one or
286 the other in particular (for example, to match your libgmp
287 installation), put CXXFLAGS=-m32 (and JREFLAGS=-d32, if you are
288 compiling the Java bindings) in the environment when you run
291 To run regression testing (make regress), you'll need GNU time.
292 We suggest you install MacPorts (from macports.org) and then the
295 You'll need also a libgmp installation. libgmp can be downloaded from
296 gmplib.org. If you install it in a nonstandard location (with
297 ./configure --prefix=...) you'll need to give this location to CVC3
298 when you configure it:
300 ./configure --with-extra-includes=...--with-extra-libs=...
302 or it may not find your installation of libgmp.
308 In order to use GMP on Cygwin, make sure the following packages are
309 installed: gmp, libgmp-devel, libgmp3, bison, flex, and make, as well
310 as standard UNIX tools.
312 On Windows, it's common to have directory names with embedded spaces.
313 This can be problematic for the CVC3 build system. Therefore on
314 Cygwin we recommend symbolically linking to names without embedded
315 spaces, something like the following:
320 $ ln -s 'ACSys Group' /home/acsys
321 $ export HOME=/home/acsys
326 $ ./configure --prefix=/home/acsys/cvc3.installation ...etc...
329 On Windows, Sun's JDK doesn't install the Java compiler "javac" into the
330 standard path for executables. If you want to build Java bindings,
331 you'll need to point CVC3 to it. Again using symbolic linking as above:
336 $ ln -s '/cygdrive/c/Program Files' /programs
337 $ ./configure --enable-java --with-java-home=/programs/Java/jdk1.6.0_16 ...
340 Such symbolic linking (and in general using cygwin full paths) may cause
341 problems with non-cygwin programs. In particular, if you have Windows
342 emacs installed (instead of cygwin's emacs), you have a version of etags
343 that may give errors at the end of the install. These errors (about source
344 files not existing when in fact they do) shouldn't break the build (make
345 won't complain and bomb out; it's just that these are at the very end of
346 the build, so it looks like they are causing problems) and can be safely
350 <a name="64-bit Platforms">64-bit Platforms</a>
353 When building %CVC3 on 64-bit platforms, you must compile %CVC3 in the
354 same mode as any libraries it uses. For example, if GMP is compiled in
355 64-bit mode, then %CVC3 must compiled in 64-bit mode as well. The
356 configuration script will try to infer the correct compilation
357 settings. You can run <code>./config.guess</code> to see the default
363 You can use the <code>--build</code> argument to
364 <code>configure</code> to override the default. For example, to
365 compile in 64-bit mode on a x86-64 CPU, you can use <code>./configure
366 --build=x86_64-pc-linux-gnu</code>.
372 <em><strong>Note: Compiling %CVC3 with LLVM is not supported and
373 may cause runtime errors.</strong></em>
375 To compile with LLVM, run configure with the options:
378 ./configure CXX=llvm-gcc LIBS='-lstdc++'
382 Other Configuration Options
385 Other configuration options include where to install the results of
386 "make install" (see below), what type of build to use (optimized,
387 debug, gprof, or gcov), and whether to use static or dynamic
388 libraries. For help on these options, type
394 configure creates the file Makefile.local which stores all of the
395 configuration information. If you want to customize your build
396 without re-running configure, or if you want to customize it in a way
397 that configure does not allow, you can do it by editing
398 Makefile.local. For example, you can build a debug, gprof version by
399 editing Makefile.local and setting OPTIMIZED to 0 and GPROF to 1 (by
400 default, gprof runs with an optimized executable). Note that for most
401 configuration options, the objects, libraries, and executables are
402 stored in a configuration-dependent directory, with only symbolic
403 links being stored in the main bin and lib directories. This allows
404 you to easily maintain multiple configurations and multiple platforms
405 using the same source tree.
408 Additional make options
411 To rebuild dependencies, type:
417 To remove just the executable or libraries in the current
424 To remove in addition all object files and makefile dependencies for
425 the current configuration, type:
431 To remove all files that are not part of the distribution (including
432 all object, library, and executables built for any configuration or
439 To build a tarball distribution of the current source tree, type:
445 \section installing Installing CVC3
447 To install %CVC3 system-wide, (assuming you have already run configure)
454 Installation depends on two configuration options: <code>prefix</code>
455 and <code>exec_prefix</code>. By default, both are set to
456 <code>/usr/local</code>, but these can be overridden by specifying the
457 correct arguments to configure or by editing
458 <code>Makefile.local</code>.
460 Installation copies all necessary header files to
461 <code>$prefix/include/cvc3</code>. It installs the library
462 <code>libcvc3</code> in <code>$exec_prefix/lib</code> and the
463 executable <code>cvc3</code> in <code>$exec_prefix/bin</code>. By
464 default, a static library and executable are installed. If you want
465 to install shared library versions, configure for shared libraries as
469 \section documentation Documentation
471 To build HTML documentation, run
479 Then open <code>doc/html/index.html</code> in your favorite browser.
481 \section faq Frequently Asked Questions
488 <code>libgmp.a is not found</code>
491 Make sure the GMP library is in your <code>LD_LIBRARY_PATH</code> and
492 <code>gmp.h</code> is in your <code>CPATH</code> (or use the
493 <code>--with-extra-lib</code> and <code>--with-extra-include</code>
494 arguments to <code>./configure</code>).
496 If your paths are properly configured and you are compiling for a
497 64-bit architecture, you may have a 32/64-bit mismatch. Check the
498 binary type of the GMP library using the <code>file</code>
499 utility. For example, running <code>file</code> on a 32-bit Linux GMP
500 shared library will return:
503 $ file /usr/lib/libgmp.so.3.4.2
504 /usr/lib/libgmp.so.3.4.2: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked, stripped
507 You can use the <code>--build</code> arguments to
508 <code>./configure</code> to set the target binary type for %CVC3. For
509 example, <code>./configure --build=i686-linux-gnu</code> or
510 <code>./configure --build=x86_64-linux-gnu</code>.
513 <code>Unable to locate Java directories</code>
516 Set the <code>JAVA_HOME</code> environment variable or use the
517 <code>--with-java-home</code> argument to
518 <code>./configure</code>. Some typical <code>JAVA_HOME</code> settings
519 are as follows (where <em>X.Y.Z</em> is the version number of the installed
524 <th> Platform </th><th> <code>JAVA_HOME</code> </th><th> Notes
527 <td> Debian/Ubuntu Linux </td>
528 <td> <code>/usr/lib/jvm/default-java</code> </td>
529 <td> Install the <code>default-jre</code> or
530 <code>default-jre-headless</code> package </td></tr>
532 <td> Fedora Linux </td>
533 <td> <code>/usr/java/jre<em>X.Y.Z</em></code> </td>
537 <td> <code>/System/Library/Frameworks/JavaVM.framework/Home</code> </td>
541 <td> <code>C:\\Program Files\\Java\\jdk<em>X.Y.Z</em></code> </td>
546 Runtime Errors (CVC3 library)
549 <h4>Segmentation fault when running a dynamically-linked executable.</h4>
551 This can be caused by a mismatched "build type". The debug and
552 optimized version of the %CVC3 shared library are not binary
553 compatible. If you are linking against a debug version of the shared
554 library, you must define the symbol _CVC3_DEBUG_MODE during
555 compilation. E.g., add <code>-D_CVC3_DEBUG_MODE</code> to
556 <code>CXXARGS</code>.
558 <h4>Fatal error: <code>Mis-handled the ref. counting</code></h4>
560 This can be cause by a number of problems. Make sure that all <code>Expr</code>
561 objects are out of scope or have been manually deleted before deleting
562 the <code>ValidityChecker</code>.
565 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path</code>
568 The Java runtime was not able to find the %CVC3 JNI library. Use
569 <code>java -Djava.library.path=PATH_TO_CVC3JNI</code>, where
570 <code>PATH_TO_CVC3JNI</code> is the directory containing the file
571 <code>libcvc3jni.so</code>.
574 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: libcvc3jni.so.<em>x.y.z</em></code>
577 The Java runtime was not able to satisfy the link dependencies of the
578 %CVC3 JNI library. Make sure that the %CVC3 and GMP libraries are in
579 your <code>LD_LIBRARY_PATH</code>.
581 If your paths are properly configured and you are compiling for a
582 64-bit architecture, you may have a 32/64-bit mismatch. Make sure the
583 JVM is running in the same mode as the %CVC3 library using the
584 <code>-d32</code> or <code>-d64</code> argument to <code>java</code>.
588 <code>terminate called after throwing an instance of 'CVC3::TypecheckException'</code>
591 This appears to be a bug in certain versions of GCC distributed by
592 Apple. Upgrade to XCode 3.1.2 or later (GCC version "4.0.1 (Apple
593 Inc. build 5490)") or configure with <code>CXXFLAGS=-01</code>.
595 \section help Getting help
597 If you find a problem with the instructions in this installation guide, please
598 send email to <a href="mailto:cvc-bugs@cs.nyu.edu">cvc-bugs@cs.nyu.edu</a>.