You can download a source distribution of CVC3 from the CVC3 downloads page. Save the source archive as
cvc3.tar.gz in the directory of your choice and extract the contents using your favorite archive program (you can use
tar xzvf cvc3.tar.gz from a terminal). This will create a directory containing the source of CVC3, normally called
cvc3-XXX. In the following we will denote the this directory as
$CVC3_SRC. To build CVC3, open your favorite terminal program and run the following sequence of commands
cd $CVC3_SRC ./configure make
If any part of the build process fails, please read the following section for more information.
A successful build will create a library
libcvc3 in the
$CVC3_SRC/lib directory, and an executable
cvc3 in the
$CVC3_SRC/bin directory (these are symbolic links to the actual files which are stored in architecture- and configuration-dependent subdirectories). The directory
$CVC3_SRC/test contains an example program using the CVC3 library
libcvc3. To try it out, run the following commands in the terminal:
cd test make bin/test
make 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:
In case you prefer to build shared libraries (and thus a much smaller executable), use the following configuration command:
If you do choose to buld the shared libraries, you must set your
LD_LIBRARY_PATH environment variable to
$CVC3_SRC/lib before running CVC3 or using the shared libraries.
Alternatively, these and other options can be changed by editing the
Makefile.local file after running
configure. However, be aware that re-running
configure will overwrite any changes you have made to
CVC3 has the following build dependencies:
All of these tools are available from common package repositories (e.g., Debian, Ubuntu, Red Hat, Cygwin).
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
configure.ac by running
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
CPPFLAGS to "
-I $includeDir" if you have headers in a nonstandard directory
LDFLAGS to "
-L $libDir" if you have libraries in a nonstandard directory
$libDir. Alternatively you can pass these directories to the
configure script using the following command
./configure --with-extra-includes=$includeDir --with-extra-libs=$libDir
./configure --help for a list of all such environment variables and options.
One of the components CVC3 depends on is the GNU Multiple Precision (GMP) library. Many Unix-like distributions include gmp packages.
If you do not have GMP installed or your installation does not work, we recommend that you install it manually:
1. Download the GMP source code from http://gmplib.org/
2. Unpack the sources, and from the root-directory of the GMP source code, run
On some Solaris machines, you may need to configure GMP with
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.
3. Now, either install GMP system-wide (make install), or supply the appropriate values for CPPFLAGS and LDFLAGS to the CVC3 configure script.
If for some reason, you do not want to use GMP, you can configure CVC3 to use native arithmetic by running:
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.
Note: The Java interface is experimental. The API may change in future releases.
To build the Java interface to CVC3, use the
--enable-java configuration option. The configuration script refers to the environment variables
CXX to set up the standard Java and C++ compiler commands. It refers to the environment variable
JFLAGS for default Java compiler flags. It refers to the variable
javadir for the installation directory of the CVC3 Java library.
The configuration options
--with-java-includes can be used to specify the path to the directories containing the JDK installation and JNI header files, respectively.
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:
./configure --enable-dynamic --enable-java
Note: 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).
To access the library, you must add the file
libcvc3-X.Y.Z.jar (where "X.Y.Z" is the CVC3 version) to the classpath (e.g., by setting the
CLASSPATH environment variable) and both
libcvc3jni.so to the runtime library path (e.g., by setting the
LD_LIBRARY_PATH environment variable java.library.path JVM variable).
For example, to compile the class Client.java:
javac -cp lib/libcvc3-X.Y.Z.jar Client.java
export LD_LIBRARY_PATH=/path/to/cvc3/libs java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3-X.Y.Z.jar Client
Mac OS X uses
DYLD_LIBRARY_PATH in place of
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.
To run regression testing (make regress), you'll need GNU time. We suggest you install MacPorts (from macports.org) and then the "gtime" package.
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 CVC3 when you configure it:
or it may not find your installation of libgmp.
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.
On Windows, it's common to have directory names with embedded spaces. This can be problematic for the CVC3 build system. Therefore on Cygwin we recommend symbolically linking to names without embedded spaces, something like the following:
$ 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...
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 CVC3 to it. Again using symbolic linking as above:
$ pwd /home/acsys/cvc3 $ ln -s '/cygdrive/c/Program Files' /programs $ ./configure --enable-java --with-java-home=/programs/Java/jdk1.6.0_16 ...
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.
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
./config.guess to see the default platform type:
$ ./config.guess i686-pc-linux-gnu
You can use the
--build argument to
configure to override the default. For example, to compile in 64-bit mode on a x86-64 CPU, you can use
Note: Compiling CVC3 with LLVM is not supported and may cause runtime errors.
To compile with LLVM, run configure with the options:
./configure CXX=llvm-gcc LIBS='-lstdc++'
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
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.
To rebuild dependencies, type:
To remove just the executable or libraries in the current configuration, type:
To remove in addition all object files and makefile dependencies for the current configuration, type:
To remove all files that are not part of the distribution (including all object, library, and executables built for any configuration or platform), type:
To build a tarball distribution of the current source tree, type:
To install CVC3 system-wide, (assuming you have already run configure) run:
Installation depends on two configuration options:
exec_prefix. By default, both are set to
/usr/local, but these can be overridden by specifying the correct arguments to configure or by editing
Installation copies all necessary header files to
$prefix/include/cvc3. It installs the library
$exec_prefix/lib and the executable
$exec_prefix/bin. By default, a static library and executable are installed. If you want to install shared library versions, configure for shared libraries as described above.
To build HTML documentation, run
doc/html/index.html in your favorite browser.
libgmp.a is not found
Make sure the GMP library is in your
gmp.h is in your
CPATH (or use the
--with-extra-include arguments to
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
file utility. For example, running
file on a 32-bit Linux GMP shared library will return:
$ 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
You can use the
--build arguments to
./configure to set the target binary type for CVC3. For example,
./configure --build=i686-linux-gnu or
Unable to locate Java directories
JAVA_HOME environment variable or use the
--with-java-home argument to
./configure. Some typical
JAVA_HOME settings are as follows (where X.Y.Z is the version number of the installed Java runtime).
|Debian/Ubuntu Linux||Install the |
|Mac OS X|
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
Mis-handled the ref. counting
This can be cause by a number of problems. Make sure that all
Expr objects are out of scope or have been manually deleted before deleting the
Exception in thread "main" java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path
The Java runtime was not able to find the CVC3 JNI library. Use
java -Djava.library.path=PATH_TO_CVC3JNI, where
PATH_TO_CVC3JNI is the directory containing the file
Exception in thread "main" java.lang.UnsatisfiedLinkError: libcvc3jni.so.x.y.z
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
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
-d64 argument to
terminate called after throwing an instance of 'CVC3::TypecheckException'
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
If you find a problem with the instructions in this installation guide, please send email to email@example.com.