<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: INSTALL</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li class="current"><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">INSTALL </div> </div>
</div><!--header-->
<div class="contents">
<div class="textblock"><p><b>Contents:</b></p>
<ul>
<li>
<a class="el" href="INSTALL.html#quickstart">Quick Start</a> </li>
<li>
<a class="el" href="INSTALL.html#requirements">Requirements</a> </li>
<li>
<a class="el" href="INSTALL.html#advanced">Advanced Configuration</a> </li>
<li>
<a class="el" href="INSTALL.html#installing">Installing CVC3</a> </li>
<li>
<a class="el" href="INSTALL.html#documentation">Documentation</a> </li>
<li>
<a class="el" href="INSTALL.html#faq">Frequently Asked Questions</a> </li>
<li>
<a class="el" href="INSTALL.html#help">Getting help</a> </li>
</ul>
<h1><a class="anchor" id="quickstart"></a>
Quick Start</h1>
<p>You can download a source distribution of CVC3 from the <a href="http://www.cs.nyu.edu/acsys/cvc3/download.html">CVC3 downloads page</a>. Save the source archive as <code>cvc3.tar.gz</code> in the directory of your choice and extract the contents using your favorite archive program (you can use <code>tar xzvf cvc3.tar.gz</code> from a terminal). This will create a directory containing the source of CVC3, normally called <code>cvc3-XXX</code>. In the following we will denote the this directory as <code>$CVC3_SRC</code>. To build CVC3, open your favorite terminal program and run the following sequence of commands</p>
<pre>
cd $CVC3_SRC
./configure
make
</pre><p>If any part of the build process fails, please read the following section for more information.</p>
<p>A successful build will create a library <code>libcvc3</code> in the <code>$CVC3_SRC/lib</code> directory, and an executable <code>cvc3</code> in the <code>$CVC3_SRC/bin</code> directory (these are symbolic links to the actual files which are stored in architecture- and configuration-dependent subdirectories). The directory <code>$CVC3_SRC/test</code> contains an example program using the CVC3 library <code>libcvc3</code>. To try it out, run the following commands in the terminal:</p>
<pre>
cd test
make
bin/test
</pre><p>By default, <code>make</code> will build optimized code, static libraries, and a static executable. To build the "debug" version (much slower but with more error checking) use the following configuration command instead:</p>
<pre>
./configure --with-build=debug
</pre><p>In case you prefer to build shared libraries (and thus a much smaller executable), use the following configuration command:</p>
<pre>
./configure --enable-dynamic
</pre><p>If you do choose to buld the shared libraries, you must set your <code>LD_LIBRARY_PATH</code> environment variable to <code>$CVC3_SRC/lib</code> before running CVC3 or using the shared libraries.</p>
<p>Alternatively, these and other options can be changed by editing the <code>Makefile.local</code> file after running <code>configure</code>. However, be aware that re-running <code>configure</code> will overwrite any changes you have made to <code>Makefile.local</code>.</p>
<h1><a class="anchor" id="requirements"></a>
Requirements</h1>
<p>CVC3 has the following build dependencies:</p>
<ul>
<li>
<a href="http://www.gnu.org/software/gcc/">GCC</a> version 3.0 or later </li>
<li>
<a href="http://www.gnu.org/software/bash/">Bash</a> </li>
<li>
<a href="http://flex.sourceforge.net/">Flex</a> </li>
<li>
<a href="http://www.gnu.org/software/bison/">Bison</a> </li>
<li>
<a href="http://gmplib.org/">GMP</a> <em>(recommended)</em> </li>
<li>
A <a href="http://python.org/">Python</a> interpreter <em>(optional, for Java support)</em> </li>
<li>
A <a href="http://java.sun.com/">Java</a> compiler <em>(optional, for Java support)</em> </li>
</ul>
<p>All of these tools are available from common package repositories (e.g., Debian, Ubuntu, Red Hat, Cygwin).</p>
<h1><a class="anchor" id="advanced"></a>
Advanced Configuration</h1>
<p>The configure script checks for the components needed to build CVC3. If for some reason, the configure script is missing or doesn't run on your platform, you can recreate it from <code>configure.ac</code> by running <code>autoconf</code>.</p>
<p>As the configure script runs, if something is not found, it complains. configure looks for components in standard locations and also uses several environment variables that you can set to help it find things. In particular, you can set <code>CPPFLAGS</code> to "<code>-I $includeDir</code>" if you have headers in a nonstandard directory <code>$includeDir</code>, and <code>LDFLAGS</code> to "<code>-L $libDir</code>" if you have libraries in a nonstandard directory <code>$libDir</code>. Alternatively you can pass these directories to the <code>configure</code> script using the following command</p>
<pre>
./configure --with-extra-includes=$includeDir --with-extra-libs=$libDir
</pre><p>Run <code>./configure –help</code> for a list of all such environment variables and options.</p>
<h3>GMP </h3>
<p>One of the components CVC3 depends on is the GNU Multiple Precision (GMP) library. Many Unix-like distributions include gmp packages.</p>
<p>If you do not have GMP installed or your installation does not work, we recommend that you install it manually:</p>
<ol type="1">
<li>Download the GMP source code from <a href="http://gmplib.org/">http://gmplib.org/</a></li>
</ol>
<ol type="1">
<li>Unpack the sources, and from the root-directory of the GMP source code, run</li>
</ol>
<pre>
./configure
make
</pre><p>On some Solaris machines, you may need to configure GMP with</p>
<pre>
./configure ABI=32
</pre><p>to make the resulting GMP library compatible with the CVC3 libraries. The reason for this is that the default ABI that gcc chooses in CVC3 compilation is not necessarily the default ABI that the GMP configure script selects, and one of them may need to be adjusted.</p>
<ol type="1">
<li>Now, either install GMP system-wide (make install), or supply the appropriate values for CPPFLAGS and LDFLAGS to the CVC3 configure script.</li>
</ol>
<p>If for some reason, you do not want to use GMP, you can configure CVC3 to use native arithmetic by running:</p>
<pre>
./configure --with-arith=native
</pre><p>If you compile CVC3 with native arithmetic, it is possible that CVC3 may fail as the result of arithmetic overflow. If an overflow occurs, you will get an error message and CVC3 will abort.</p>
<h3>Java interface </h3>
<p><em><b>Note: The Java interface is experimental. The API may change in future releases.</b></em></p>
<p>To build the Java interface to CVC3, use the <code>–enable-java</code> configuration option. The configuration script refers to the environment variables <code>JAVAC</code>, <code>JAVAH</code>, <code>JAR</code>, and <code>CXX</code> to set up the standard Java and C++ compiler commands. It refers to the environment variable <code>JFLAGS</code> for default Java compiler flags. It refers to the variable <code>javadir</code> for the installation directory of the <a class="el" href="namespaceCVC3.html">CVC3</a> Java library.</p>
<p>The configuration options <code>–with-java-home</code> and <code>–with-java-includes</code> can be used to specify the path to the directories containing the JDK installation and JNI header files, respectively.</p>
<p>You must build CVC3 as a dynamic library to use the Java interface. For example, you might configure the build by running the following in the top-level CVC3 directory:</p>
<pre>
./configure --enable-dynamic --enable-java
</pre><p><b>Note:</b> The Java interface depends on the "build type" (e.g., "optimized", "debug") of CVC3. If you choose to re-configure and re-build CVC3 with a different build type, you must run "make clean" in the current directory and re-build the interface (cleaning and rebuilding the entire CVC3 package will suffice).</p>
<h4>Using the Java interface </h4>
<p>To access the library, you must add the file <code>libcvc3-X.Y.Z.jar</code> (where "X.Y.Z" is the <a class="el" href="namespaceCVC3.html">CVC3</a> version) to the classpath (e.g., by setting the <code>CLASSPATH</code> environment variable) and both <code>libcvc3.so</code> and <code>libcvc3jni.so</code> to the runtime library path (e.g., by setting the <code>LD_LIBRARY_PATH</code> environment variable java.library.path JVM variable).</p>
<p>For example, to compile the class Client.java:</p>
<pre>
javac -cp lib/libcvc3-X.Y.Z.jar Client.java
</pre><p>To run:</p>
<pre>
export LD_LIBRARY_PATH=/path/to/cvc3/libs
java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3-X.Y.Z.jar Client
</pre><h3>Mac OS X </h3>
<p>Mac OS X uses <code>DYLD_LIBRARY_PATH</code> in place of <code>LD_LIBRARY_PATH</code>.</p>
<p>On Intel Macs, by default, CVC3 compiles in 32-bit or 64-bit mode based on the compiler's default. If you want to build as one or the other in particular (for example, to match your libgmp installation), put CXXFLAGS=-m32 (and JREFLAGS=-d32, if you are compiling the Java bindings) in the environment when you run configure.</p>
<p>To run regression testing (make regress), you'll need GNU time. We suggest you install MacPorts (from macports.org) and then the "gtime" package.</p>
<p>You'll need also a libgmp installation. libgmp can be downloaded from gmplib.org. If you install it in a nonstandard location (with ./configure –prefix=...) you'll need to give this location to <a class="el" href="namespaceCVC3.html">CVC3</a> when you configure it:</p>
<p>./configure –with-extra-includes=...–with-extra-libs=...</p>
<p>or it may not find your installation of libgmp.</p>
<h3>Cygwin </h3>
<p>In order to use GMP on Cygwin, make sure the following packages are installed: gmp, libgmp-devel, libgmp3, bison, flex, and make, as well as standard UNIX tools.</p>
<p>On Windows, it's common to have directory names with embedded spaces. This can be problematic for the <a class="el" href="namespaceCVC3.html">CVC3</a> build system. Therefore on Cygwin we recommend symbolically linking to names without embedded spaces, something like the following:</p>
<pre>
$ pwd
/home/ACSys Group
$ ln -s 'ACSys Group' /home/acsys
$ export HOME=/home/acsys
$ cd
$ pwd
/home/acsys
$ cd cvc3
$ ./configure --prefix=/home/acsys/cvc3.installation ...etc...
</pre><p>On Windows, Sun's JDK doesn't install the Java compiler "javac" into the standard path for executables. If you want to build Java bindings, you'll need to point <a class="el" href="namespaceCVC3.html">CVC3</a> to it. Again using symbolic linking as above:</p>
<pre>
$ pwd
/home/acsys/cvc3
$ ln -s '/cygdrive/c/Program Files' /programs
$ ./configure --enable-java --with-java-home=/programs/Java/jdk1.6.0_16 ...
</pre><p>Such symbolic linking (and in general using cygwin full paths) may cause problems with non-cygwin programs. In particular, if you have Windows emacs installed (instead of cygwin's emacs), you have a version of etags that may give errors at the end of the install. These errors (about source files not existing when in fact they do) shouldn't break the build (make won't complain and bomb out; it's just that these are at the very end of the build, so it looks like they are causing problems) and can be safely ignored.</p>
<h3><a class="anchor" id="64-bit Platforms"></a>64-bit Platforms </h3>
<p>When building CVC3 on 64-bit platforms, you must compile CVC3 in the same mode as any libraries it uses. For example, if GMP is compiled in 64-bit mode, then CVC3 must compiled in 64-bit mode as well. The configuration script will try to infer the correct compilation settings. You can run <code>./config.guess</code> to see the default platform type: </p>
<pre class="fragment">$ ./config.guess
i686-pc-linux-gnu
</pre><p>You can use the <code>–build</code> argument to <code>configure</code> to override the default. For example, to compile in 64-bit mode on a x86-64 CPU, you can use <code>./configure –build=x86_64-pc-linux-gnu</code>.</p>
<h3>LLVM </h3>
<p><em><b>Note: Compiling CVC3 with LLVM is not supported and may cause runtime errors.</b></em></p>
<p>To compile with LLVM, run configure with the options:</p>
<pre>
./configure CXX=llvm-gcc LIBS='-lstdc++'
</pre><h3>Other Configuration Options </h3>
<p>Other configuration options include where to install the results of "make install" (see below), what type of build to use (optimized, debug, gprof, or gcov), and whether to use static or dynamic libraries. For help on these options, type</p>
<pre>
./configure --help
</pre><p>configure creates the file Makefile.local which stores all of the configuration information. If you want to customize your build without re-running configure, or if you want to customize it in a way that configure does not allow, you can do it by editing Makefile.local. For example, you can build a debug, gprof version by editing Makefile.local and setting OPTIMIZED to 0 and GPROF to 1 (by default, gprof runs with an optimized executable). Note that for most configuration options, the objects, libraries, and executables are stored in a configuration-dependent directory, with only symbolic links being stored in the main bin and lib directories. This allows you to easily maintain multiple configurations and multiple platforms using the same source tree.</p>
<h4>Additional make options </h4>
<p>To rebuild dependencies, type:</p>
<pre>
make depend
</pre><p>To remove just the executable or libraries in the current configuration, type:</p>
<pre>
make spotty
</pre><p>To remove in addition all object files and makefile dependencies for the current configuration, type:</p>
<pre>
make clean
</pre><p>To remove all files that are not part of the distribution (including all object, library, and executables built for any configuration or platform), type:</p>
<pre>
make distclean
</pre><p>To build a tarball distribution of the current source tree, type:</p>
<pre>
make dist
</pre><h1><a class="anchor" id="installing"></a>
Installing CVC3</h1>
<p>To install CVC3 system-wide, (assuming you have already run configure) run:</p>
<pre>
make install
</pre><p>Installation depends on two configuration options: <code>prefix</code> and <code>exec_prefix</code>. By default, both are set to <code>/usr/local</code>, but these can be overridden by specifying the correct arguments to configure or by editing <code>Makefile.local</code>.</p>
<p>Installation copies all necessary header files to <code>$prefix/include/cvc3</code>. It installs the library <code>libcvc3</code> in <code>$exec_prefix/lib</code> and the executable <code>cvc3</code> in <code>$exec_prefix/bin</code>. By default, a static library and executable are installed. If you want to install shared library versions, configure for shared libraries as described above.</p>
<h1><a class="anchor" id="documentation"></a>
Documentation</h1>
<p>To build HTML documentation, run</p>
<pre></pre><pre> make doc</pre><pre></pre><p>Then open <code>doc/html/index.html</code> in your favorite browser.</p>
<h1><a class="anchor" id="faq"></a>
Frequently Asked Questions</h1>
<h3>Configuration Errors </h3>
<h4><code>libgmp.a is not found</code> </h4>
<p>Make sure the GMP library is in your <code>LD_LIBRARY_PATH</code> and <code>gmp.h</code> is in your <code>CPATH</code> (or use the <code>–with-extra-lib</code> and <code>–with-extra-include</code> arguments to <code>./configure</code>).</p>
<p>If your paths are properly configured and you are compiling for a 64-bit architecture, you may have a 32/64-bit mismatch. Check the binary type of the GMP library using the <code>file</code> utility. For example, running <code>file</code> on a 32-bit Linux GMP shared library will return:</p>
<pre>
$ file /usr/lib/libgmp.so.3.4.2
/usr/lib/libgmp.so.3.4.2: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked, stripped
</pre><p>You can use the <code>–build</code> arguments to <code>./configure</code> to set the target binary type for CVC3. For example, <code>./configure –build=i686-linux-gnu</code> or <code>./configure –build=x86_64-linux-gnu</code>.</p>
<h4><code>Unable to locate Java directories</code> </h4>
<p>Set the <code>JAVA_HOME</code> environment variable or use the <code>–with-java-home</code> argument to <code>./configure</code>. Some typical <code>JAVA_HOME</code> settings are as follows (where <em>X.Y.Z</em> is the version number of the installed Java runtime).</p>
<table class="doxtable">
<tr>
<th>Platform </th><th><code>JAVA_HOME</code> </th><th>Notes </th></tr>
<tr>
<td>Debian/Ubuntu Linux </td><td><code>/usr/lib/jvm/default-java</code> </td><td>Install the <code>default-jre</code> or <code>default-jre-headless</code> package </td></tr>
<tr>
<td>Fedora Linux </td><td><code>/usr/java/jre<em>X.Y.Z</em></code> </td><td></td></tr>
<tr>
<td>Mac OS X </td><td><code>/System/Library/Frameworks/JavaVM.framework/Home</code> </td><td></td></tr>
<tr>
<td>Windows </td><td><code>C:\Program Files\Java\jdk<em>X.Y.Z</em></code> </td><td></td></tr>
</table>
<h3>Runtime Errors (<a class="el" href="namespaceCVC3.html">CVC3</a> library) </h3>
<h4>Segmentation fault when running a dynamically-linked executable.</h4>
<p>This can be caused by a mismatched "build type". The debug and optimized version of the CVC3 shared library are not binary compatible. If you are linking against a debug version of the shared library, you must define the symbol _CVC3_DEBUG_MODE during compilation. E.g., add <code>-D_CVC3_DEBUG_MODE</code> to <code>CXXARGS</code>.</p>
<h4>Fatal error: <code>Mis-handled the ref. counting</code></h4>
<p>This can be cause by a number of problems. Make sure that all <code>Expr</code> objects are out of scope or have been manually deleted before deleting the <code>ValidityChecker</code>.</p>
<h4><code>Exception in thread "main" java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path</code> </h4>
<p>The Java runtime was not able to find the CVC3 JNI library. Use <code>java -Djava.library.path=PATH_TO_CVC3JNI</code>, where <code>PATH_TO_CVC3JNI</code> is the directory containing the file <code>libcvc3jni.so</code>.</p>
<h4><code>Exception in thread "main" java.lang.UnsatisfiedLinkError: libcvc3jni.so.<em>x.y.z</em></code> </h4>
<p>The Java runtime was not able to satisfy the link dependencies of the CVC3 JNI library. Make sure that the CVC3 and GMP libraries are in your <code>LD_LIBRARY_PATH</code>.</p>
<p>If your paths are properly configured and you are compiling for a 64-bit architecture, you may have a 32/64-bit mismatch. Make sure the JVM is running in the same mode as the CVC3 library using the <code>-d32</code> or <code>-d64</code> argument to <code>java</code>.</p>
<h4>On Mac: <code>terminate called after throwing an instance of '<a class="el" href="classCVC3_1_1TypecheckException.html">CVC3::TypecheckException</a>'</code> </h4>
<p>This appears to be a bug in certain versions of GCC distributed by Apple. Upgrade to XCode 3.1.2 or later (GCC version "4.0.1 (Apple
Inc. build 5490)") or configure with <code>CXXFLAGS=-01</code>.</p>
<h1><a class="anchor" id="help"></a>
Getting help</h1>
<p>If you find a problem with the instructions in this installation guide, please send email to <a href="#" onclick="location.href='mai'+'lto:'+'cvc'+'-b'+'ugs'+'@c'+'s.n'+'yu'+'.ed'+'u'; return false;">cvc-bugs@cs.nyu.edu</a>. </p>
</div></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
