|
CVC3
2.4.1
|
Contents:
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
By default, 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:
./configure --with-build=debug
In case you prefer to build shared libraries (and thus a much smaller executable), use the following configuration command:
./configure --enable-dynamic
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 Makefile.local.
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 autoconf.
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 $includeDir, and 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
Run ./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:
./configure make
On some Solaris machines, you may need to configure GMP with
./configure ABI=32
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.
If for some reason, you do not want to use GMP, you can configure CVC3 to use native arithmetic by running:
./configure --with-arith=native
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 JAVAC, JAVAH, JAR, and 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-home and –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 libcvc3.so and 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
To run:
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 LD_LIBRARY_PATH.
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:
./configure –with-extra-includes=...–with-extra-libs=...
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 ./configure –build=x86_64-pc-linux-gnu.
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 --help
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:
make depend
To remove just the executable or libraries in the current configuration, type:
make spotty
To remove in addition all object files and makefile dependencies for the current configuration, type:
make clean
To remove all files that are not part of the distribution (including all object, library, and executables built for any configuration or platform), type:
make distclean
To build a tarball distribution of the current source tree, type:
make dist
To install CVC3 system-wide, (assuming you have already run configure) run:
make install
Installation depends on two configuration options: prefix and 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 Makefile.local.
Installation copies all necessary header files to $prefix/include/cvc3. It installs the library libcvc3 in $exec_prefix/lib and the executable cvc3 in $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
make doc
Then open doc/html/index.html in your favorite browser.
libgmp.a is not found Make sure the GMP library is in your LD_LIBRARY_PATH and gmp.h is in your CPATH (or use the –with-extra-lib and –with-extra-include arguments to ./configure).
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 ./configure –build=x86_64-linux-gnu.
Unable to locate Java directories Set the 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).
| Platform | JAVA_HOME | Notes |
|---|---|---|
| Debian/Ubuntu Linux | /usr/lib/jvm/default-java | Install the default-jre or default-jre-headless package |
| Fedora Linux | /usr/java/jreX.Y.Z | |
| Mac OS X | /System/Library/Frameworks/JavaVM.framework/Home | |
| Windows | C:\Program Files\Java\jdkX.Y.Z |
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 -D_CVC3_DEBUG_MODE to CXXARGS.
Mis-handled the ref. countingThis 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 ValidityChecker.
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 libcvc3jni.so.
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 LD_LIBRARY_PATH.
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 -d32 or -d64 argument to java.
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 CXXFLAGS=-01.
If you find a problem with the instructions in this installation guide, please send email to cvc-bugs@cs.nyu.edu.
1.8.3.1