diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 17:27:51 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 17:27:51 +0000 |
commit | 99cad5495be99efae434177d1537d4cfac35581c (patch) | |
tree | d96995c91bfcec7d4cd40d9aa6cedef5a19fa18f /INSTALL | |
parent | 8116fa6b55db64301ed89f1f174b95780449007f (diff) |
* Some documentation about building compatibility and language bindings
* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available
Diffstat (limited to 'INSTALL')
-rw-r--r-- | INSTALL | 77 |
1 files changed, 77 insertions, 0 deletions
@@ -24,6 +24,10 @@ under doc/ but is not installed by "make install". Examples/tutorials are not installed with "make install." See below. +For more information about the build system itself (probably not +necessary for casual users), see the Appendix at the bottom of this +file. + *** Build dependences The following tools and libraries are required to run CVC4. Versions @@ -78,10 +82,18 @@ Boost project, please visit http://www.boost.org/. None of these is required, but can improve CVC4 as described below: + Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator) Optional: CLN v1.3 or newer (Class Library for Numbers) Optional: CUDD v2.4.2 or newer (Colorado University Decision Diagram package) Optional: GNU Readline library (for an improved interactive experience) Optional: The Boost C++ threading library (libboost_thread) + Optional: CxxTest unit testing framework + +SWIG is necessary to build the Java API (and of course a JDK is +necessary, too). SWIG 1.x won't work; you'll need 2.0, and the more +recent the better. On Mac, we've seen SWIG segfault when generating +CVC4 language bindings; version 2.0.8 or higher is recommended to +avoid this. See "Language bindings" below for build instructions. CLN is an alternative multiprecision arithmetic package that can offer better performance and memory footprint than GMP. CLN is covered by @@ -106,6 +118,13 @@ Boost base library) is needed to run CVC4 in "portfolio" (multithreaded) mode. Check your distribution for a package named "libboost-thread-dev" or similar. +CxxTest is necessary to run CVC4's unit tests (included with the +distribution). Running these is not really required for users of +CVC4; "make check" will skip unit tests if CxxTest isn't available, +and go on to run the extensive system- and regresion-tests in the +source tree. However, if you're interested, you can download CxxTest +at http://cxxtest.com/ . + *** Building with CUDD (optional) CUDD, if desired, must be installed delicately. The CVC4 configure @@ -137,6 +156,47 @@ here: The Debian source package "cudd", available from the same repository, includes a diff of all changes made to cudd makefiles. +*** Language bindings + +There are several options available for using CVC4 from the API. + +First, CVC4 offers a complete and flexible API for manipulating +expressions, maintaining a stack of assertions, and checking +satisfiability, and related things. The C++ libraries (libcvc4.so and +libcvc4parser.so) and required headers are installed normally via a +"make install". This API is also available from Java (via CVC4.jar +and libcvc4jni.so) by configuring with --enable-language-bindings=java. +You'll also need SWIG 2.0 installed (and you might need to help +configure find it if you installed it in a nonstandard place with +--with-swig-dir=/path/to/swig/installation). You may also need to +give the configure script the path to your Java headers (in +particular, jni.h). You might do so with (for example): + + ./configure --enable-language-bindings=java \ + JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include + +There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h> +and link against libcvc4compat.so) that attempts to maintain +source-level backwards-compatibility with the CVC3 C++ API. The +compatibility library is built by default, and +--enable-language-bindings=java enables the Java compatibility library +(CVC4compat.jar and libcvc4compatjni.so). +--enable-language-bindings=c enables the C compatibility library +(#include <cvc4/bindings/compat/c/c_interface.h> and link against +libcvc4bindings_c_compat.so), and if you want both C and Java +bindings, use --enable-language-bindings=c,java. These compatibility +language bindings do NOT require SWIG. + +The examples/ directory includes some basic examples (the "simple vc" +and "simple vc compat" family of examples) of all these interfaces. + +In principle, since we use SWIG to generate the native Java API, we +could support other languages as well. However, using CVC4 from other +languages is not supported, nor expected to work, at this time. If +you're interested in helping to develop, maintain, and test a language +binding, please contact us via the users' mailing list at +cvc-users@cs.nyu.edu. + *** Building CVC4 from a repository checkout The following tools and libraries are additionally required to build @@ -159,3 +219,20 @@ repository. Examples are not built by "make" or "make install". See examples/README for information on what to find in the examples/ directory, as well as information about building and installing them. + +*** Appendix: Build architecture + +The build system is generated by automake, libtool, and autoconf. It +is somewhat nonstandard, though, which (for one thing) requires that +GNU Make be used. If you ./configure in the top-level source +directory, the objects will actually all appear in +builds/${arch}/${build_id}. This is to allow multiple, separate +builds in the same place (e.g., an assertions-enabled debugging build +alongside a production build), without changing directories at the +shell. The "current" build is maintained, and you can still use +(e.g.) "make -C src/main" to rebuild objects in just one subdirectory. + +You can also create your own build directory inside or outside of the +source tree and configure from there. All objects will then be built +in that directory, and you'll ultimately find the "cvc4" binary in +src/main/, and the libraries under src/ and src/parser/. |