1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
This is a prerelease version of CVC4.
*** Quick-start instructions
./configure
make
(To build from a Subversion checkout, you'll need reasonably new
automake, autoconf, and libtool installed (see below). The
"configure" script isn't in the repository, so run "./autogen.sh"
first to produce it. Then proceed as above.)
You can then "make install" to install in the prefix you gave to
the configure script (/usr/local by default). ** 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 doc/ but is not installed by "make install".
To build a source release, use "make dist"; this will include the
configure script and all the bits of automake/autoconf/libtool that
are necessary for an independent install. You'll find the resulting
tarball in builds/cvc4-${VERSION}.tar.gz.
*** 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)
The Boost C++ base libraries
For libantlr3c, you can use the convenience script in
contrib/get-antlr-3.4 --this will download, patch, and install
libantlr3c. On a 32-bit machine, or if you have difficulty
building libantlr3c (or difficulty getting CVC4 to link against
it later), you may need to remove the --enable-64bit part in the
script. (If you're curious, the manual instructions are at
http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .)
Optional: CLN v1.3 (Class Library for Numbers)
Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
Optional: GNU Readline library (for an improved interactive experience)
Optional: The Boost C++ threading library (libboost_thread)
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.
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 (remember, you need the C++
development package for CVC4), 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-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 is here:
deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/
The Debian source package "cudd", available from the same repository,
includes a diff of all changes made to cudd makefiles.
*** Build dependencies
The following tools and libraries are required to build CVC4 from
scratch (i.e., from the repository rather than from a source tarball).
Automake v1.11
Autoconf v2.61
Libtool v2.2
ANTLR3 v3.2
*** Emacs support
For a suggestion of editing CVC4 source code with emacs, see the file
contrib/editing-with-emacs. For a CVC language mode (the native input
language for CVC4), see contrib/cvc-mode.el.
|
