View source for Building CVC4 from source

From CVC4
You do not have permission to edit this page, for the following reason:
The action you have requested is limited to users in the group: Users.
You can view and copy the source of this page.
To compile CVC4 from a source package you must do the following:
# Install antlr
# Configure cvc4
# Compile cvc4
# Install cvc4 [optional]

To do so run the following commands in the CVC4 directory:

    cd contrib
    ./get-antlr-3.4
    cd ..
    ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3
    make
    make check   [recommended]
    make install [optional]

Below are more details instructions about the various dependencies and options. 

=Common make Options=
* "''make install''" will install into the "--prefix" option you gave to
the configure script (''/usr/local'' by default).
    ./configure --prefix=~/install_targets/cvc4 ...
    make install
* '''You should run "''make check''"''' before installation to ensure that CVC4 has been
built correctly.  In particular, GCC version 4.5.1 seems to have a
bug in the optimizer that results in incorrect behavior (and wrong
results) in many builds.  This is a known problem for Minisat, and
since Minisat is at the core of CVC4, a problem for CVC4.  "''make check''"
easily detects this problem (by showing a number of FAILed test cases).
It is ok if the unit tests aren't run as part of "''make check''", but all
system tests and regression tests should pass without incident.
* To build API documentation, use "''make doc''".  Documentation is produced
under ''builds/doc/'' but is not installed by "''make install''".

Examples and tutorials are not installed with "''make install''."  See [[#Examples_and_tutorials_are_not_built_or_installed|below]].

For more information about the build system itself (probably not
necessary for casual users), see the [[#Appendix:_Build_architecture|Appendix]] at the bottom of this
file.

=Common configure Options=
*'''--prefix=PREFIX''' install architecture-independent files in PREFIX (by default /usr/local)
*'''--with-build={production,debug,default,competition}''' 
*'''--with-antlr-dir=PATH'''
*'''--with-cln'''/'''--with-gmp''' selects the numbers package to use by default ([[#Optional requirements]])
*'''--enable-static-binary''' build a fully statically-linked binary. (This is recommended for Mac OS X users that want to be able to use gdb.)
*'''ANTLR=PATH''' location of the antlr3 script
*'''--with-boost=DIR''' installation location of the boost libraries (most users will not need this)

See '''./configure --help''' for more.

=Build dependencies=

The following tools and libraries are required to run CVC4. Versions
given are minimum versions; more recent versions should be compatible.

*'''GNU C and C++''' (gcc and g++), reasonably recent versions
*'''GNU Make'''
*'''GNU Bash'''
*'''GMP v4.2''' (GNU Multi-Precision arithmetic library)
*'''libantlr3c v3.2 or v3.4''' (ANTLR parser generator C support library)
*'''The Boost C++ base libraries'''
*'''MacPorts'''   [highly recommended if on a Mac; see [[#MacPorts]]]


The hardest to obtain and install is the libantlr3c requirement, and
is explained [[#Installing libantlr3c: ANTLR parser generator C support library|next]].

If "make" is non-GNU on your system, make sure to invoke "gmake" (or
whatever GNU Make is installed as).  If your usual shell is not Bash,
the configure script should auto-correct this.  If it does not, you'll
see strange shell syntax errors, and you may need to explicitly set
SHELL or CONFIG_SHELL to the location of bash on your system.

==Installing libantlr3c: ANTLR parser generator C support library==

For libantlr3c, you can use the convenience script in
''contrib/get-antlr-3.4'' in the source distribution---this will download, patch, compile and install
libantlr3c into your cvc4 directory as ''cvc4/antlr-3.4/''.
  cd contrib
  ./get-antlr-3.4

CVC4 must be configured with the antlr library installation directory, '''--with-antlr-dir''', and an antlr executable script file, '''ANTLR'''.  If libantlr3c was installed via get-antlr-3.4, the following configure line should suffice for CVC44
  ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

For 64 bit machines, libantlr3c needs to be configured with 64 bit explicitly
  ./configure --enable-64bit ...
The get-antlr-3.4 script makes a guess at whether the machine is 64 bit and adds the appropriate flag.
To force the script to compile 32 bit:
  MACHINE_TYPE="x86" ./get-antlr-3.4
To force the script to compile 64 bit:
  MACHINE_TYPE="x86_64" ./get-antlr-3.4

For a longer discussion, instructions for manual installation, and more in depth troubleshooting, see [[Developer's Guide#ANTLR3]].

==MacPorts==

On a Mac, it is '''highly''' recommended that you use MacPorts (see
http://www.macports.org/).  Doing so is easy.  Then, simply run the
script ''contrib/mac-build'', which installs a few ports from the MacPorts
repository, then compiles and installs antlr3c using the ''get-antlr-3.4''
script.  The mac-build script should set you up
with all requirements, and will tell you how to configure CVC4 when it
completes successfully.

==Installing the Boost C++ base libraries==

A Boost package is available on most Linux distributions; check yours
for a package named something like libboost-dev or boost-devel.  There
are a number of additional Boost packages in some distributions, but
this "basic" one should be sufficient for building CVC4.

Should you want to install Boost manually, or to learn more about the
Boost project, please visit http://www.boost.org/.

=Optional requirements=

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|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
the GNU General Public License, version 3; so if you choose to use
CVC4 with CLN support, you are licensing CVC4 under that same license.
(Usually CVC4's license is more permissive than GPL is; see the file
COPYING in the CVC4 source distribution for details.)  Please visit
http://www.ginac.de/CLN/ for more details about CLN.

CUDD is a decision diagram package that changes the behavior of the
CVC4 arithmetic solver in some cases; it may or may not improve the
arithmetic solver's performance.  See [[#Building_with_CUDD_(optional)|below]] for instructions on
obtaining and building CUDD.

The GNU Readline library is optionally used to provide command
editing, tab completion, and history functionality at the CVC prompt
(when running in interactive mode).  Check your distribution for a
package named "libreadline-dev" or "readline-devel" or similar.

The Boost C++ threading library (often packaged independently of the
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 regression-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
script attempts to auto-detect the locations and names of CUDD headers
and libraries the way that the Fedora RPMs install them, the way that
our NYU-provided Debian packages install them, and the way they exist
when you download and build the CUDD sources directly.  If you install
from Fedora RPMs or our Debian packages, the process should be
completely automatic, since the libraries and headers are installed in
a standard location.  If you download the sources yourself, you need
to build them in a special way.  Fortunately, the
"contrib/build-cudd-2.4.2-with-libtool.sh" script in the CVC4 source
tree does exactly what you need: it patches the CUDD makefiles to use
libtool, builds the libtool libraries, then reverses the patch to
leave the makefiles as they were.  Once you run this script on an
unpacked CUDD 2.4.2 source distribution, then CVC4's configure script
should pick up the libraries if you provide
--with-cudd-dir=/PATH/TO/CUDD/SOURCES.

If you want to force linking to CUDD, provide --with-cudd to the
configure script; this makes it a hard requirement rather than an
optional add-on.

The NYU-provided Debian packaging of CUDD 2.4.2 and CUDD 2.5.0 are
here (along with the CVC4 Debian packages):

  deb http://cvc4.cs.nyu.edu/debian/ unstable/

On Debian (and Debian-derived distributions like Ubuntu), you only
need to drop that one line in your /etc/apt/sources.list file, then install with your favorite package manager.

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 in the source distribution 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
CVC4 from from a repository checkout rather than from a prepared
source tarball.

*'''Automake v1.11'''
*'''Autoconf v2.61'''
*'''Libtool v2.2'''
*'''ANTLR3 v3.2 or v3.4'''
*'''Java Development Kit''' ([http://www.antlr.org/wiki/pages/viewpage.action?pageId=728 required for ANTLR3])

First, use "''./autogen.sh''" to create the configure script.  Then
proceed as normal for any distribution tarball.  The parsers are
pre-generated for the tarballs, but don't exist in the repository; hence the extra ANTLR3 and JDK requirements to
generate the source code for the parsers, when building from the
repository.

=Examples and tutorials are not built or installed=

Examples are not built by "''make''" or "''make install''".  See
''examples/README'' in the source distribution 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/.
Return to Building CVC4 from source.
Retrieved from "http://cvc4.cs.stanford.edu/wiki/Building_CVC4_from_source"
View source for Building CVC4 from source

Navigation menu

Views

Personal tools

CVC4

For CVC4 Developers

Cascade

Meta

Wiki

Search

Tools
