1 CVC4 release version 1.3.
3 *** Quick-start instructions
7 The following tools and libraries are required to build and run CVC4.
8 Versions given are minimum versions; more recent versions should be
11 GNU C and C++ (gcc and g++), reasonably recent versions
14 GMP v4.2 (GNU Multi-Precision arithmetic library)
15 MacPorts [only if on a Mac; see below]
16 libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)
17 The Boost C++ base libraries
19 The hardest to obtain and install is the libantlr3c requirement, so
20 that one is explained next.
22 On a Mac, you need to additionally install MacPorts (see
23 http://www.macports.org/). Doing so is easy. Then, simply run the
24 script contrib/mac-build, which installs a few ports from the MacPorts
25 repository, then compiles and installs antlr3c using the get-antlr-3.4
26 script (as described next). The mac-build script should set you up
27 with all requirements, and will tell you how to configure CVC4 when it
28 completes successfully.
30 If "make" is non-GNU on your system, make sure to invoke "gmake" (or
31 whatever GNU Make is installed as). If your usual shell is not Bash,
32 the configure script should auto-correct this. If it does not, you'll
33 see strange shell syntax errors, and you may need to explicitly set
34 SHELL or CONFIG_SHELL to the location of bash on your system.
36 *** Installing libantlr3c: ANTLR parser generator C support library
38 For libantlr3c, you can use the convenience script in
39 contrib/get-antlr-3.4 --this will download, patch, and install
40 libantlr3c. On a 32-bit machine, or if you have difficulty building
41 libantlr3c (or difficulty getting CVC4 to link against it later), you
42 may need to remove the --enable-64bit part in the script. (If you're
43 curious, the manual instructions are at
44 http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .)
48 The hardest build dependence to satisfy is libantlr3c; that's why it
49 is explained above. Problems in satisfying other build dependences are
52 Once the build dependences are satisfied, you should be able to
53 configure, make, make check, and make install without incident:
55 ./configure [use --prefix to specify a prefix; default /usr/local]
57 make check [optional but a good idea!]
59 To build from a repository checkout (rather than a distributed CVC4
60 tarball), there are additional dependences; see below.
62 You can then "make install" to install in the prefix you gave to
63 the configure script (/usr/local by default). ** You should run
64 "make check" ** before installation to ensure that CVC4 has been
65 built correctly. In particular, GCC version 4.5.1 seems to have a
66 bug in the optimizer that results in incorrect behavior (and wrong
67 results) in many builds. This is a known problem for Minisat, and
68 since Minisat is at the core of CVC4, a problem for CVC4. "make check"
69 easily detects this problem (by showing a number of FAILed test cases).
70 It is ok if the unit tests aren't run as part of "make check", but all
71 system tests and regression tests should pass without incident.
73 To build API documentation, use "make doc". Documentation is produced
74 under doc/ but is not installed by "make install".
76 Examples and tutorials are not installed with "make install." You may
77 want to "make install-examples". See below.
79 For more information about the build system itself (probably not
80 necessary for casual users), see the Appendix at the bottom of this
83 *** Installing the Boost C++ base libraries
85 A Boost package is available on most Linux distributions; check yours
86 for a package named something like libboost-dev or boost-devel. There
87 are a number of additional Boost packages in some distributions, but
88 this "basic" one should be sufficient for building CVC4.
90 Should you want to install Boost manually, or to learn more about the
91 Boost project, please visit http://www.boost.org/.
93 *** Optional requirements
95 None of these is required, but can improve CVC4 as described below:
97 Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
98 Optional: CLN v1.3 or newer (Class Library for Numbers)
99 Optional: GLPK (GNU Linear Programming Kit)
100 Optional: GNU Readline library (for an improved interactive experience)
101 Optional: The Boost C++ threading library (libboost_thread)
102 Optional: CxxTest unit testing framework
104 SWIG is necessary to build the Java API (and of course a JDK is
105 necessary, too). SWIG 1.x won't work; you'll need 2.0, and the more
106 recent the better. On Mac, we've seen SWIG segfault when generating
107 CVC4 language bindings; version 2.0.8 or higher is recommended to
108 avoid this. See "Language bindings" below for build instructions.
110 CLN is an alternative multiprecision arithmetic package that can offer
111 better performance and memory footprint than GMP. CLN is covered by
112 the GNU General Public License, version 3; so if you choose to use
113 CVC4 with CLN support, you are licensing CVC4 under that same license.
114 (Usually CVC4's license is more permissive than GPL is; see the file
115 COPYING in the CVC4 source distribution for details.) Please visit
116 http://www.ginac.de/CLN/ for more details about CLN.
118 GLPK is the GNU Linear Programming Kit, and can be used to speed up
119 the arithmetic implementation in CVC4. GLPK is covered by the GNU
120 General Public License, version 3; so if you choose to use CVC4 with
121 GLPK support, you are licensing CVC4 under that same license.
122 (Usually CVC4's license is more permissive; see above discussion.)
123 Please visit http://www.gnu.org/software/glpk/ for more details about
126 The GNU Readline library is optionally used to provide command
127 editing, tab completion, and history functionality at the CVC prompt
128 (when running in interactive mode). Check your distribution for a
129 package named "libreadline-dev" or "readline-devel" or similar.
131 The Boost C++ threading library (often packaged independently of the
132 Boost base library) is needed to run CVC4 in "portfolio"
133 (multithreaded) mode. Check your distribution for a package named
134 "libboost-thread-dev" or similar.
136 CxxTest is necessary to run CVC4's unit tests (included with the
137 distribution). Running these is not really required for users of
138 CVC4; "make check" will skip unit tests if CxxTest isn't available,
139 and go on to run the extensive system- and regression-tests in the
140 source tree. However, if you're interested, you can download CxxTest
141 at http://cxxtest.com/ .
143 *** Language bindings
145 There are several options available for using CVC4 from the API.
147 First, CVC4 offers a complete and flexible API for manipulating
148 expressions, maintaining a stack of assertions, and checking
149 satisfiability, and related things. The C++ libraries (libcvc4.so and
150 libcvc4parser.so) and required headers are installed normally via a
151 "make install". This API is also available from Java (via CVC4.jar
152 and libcvc4jni.so) by configuring with --enable-language-bindings=java.
153 You'll also need SWIG 2.0 installed (and you might need to help
154 configure find it if you installed it in a nonstandard place with
155 --with-swig-dir=/path/to/swig/installation). You may also need to
156 give the configure script the path to your Java headers (in
157 particular, jni.h). You might do so with (for example):
159 ./configure --enable-language-bindings=java \
160 JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
162 There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h>
163 and link against libcvc4compat.so) that attempts to maintain
164 source-level backwards-compatibility with the CVC3 C++ API. The
165 compatibility library is built by default, and
166 --enable-language-bindings=java enables the Java compatibility library
167 (CVC4compat.jar and libcvc4compatjni.so).
168 --enable-language-bindings=c enables the C compatibility library
169 (#include <cvc4/bindings/compat/c/c_interface.h> and link against
170 libcvc4bindings_c_compat.so), and if you want both C and Java
171 bindings, use --enable-language-bindings=c,java. These compatibility
172 language bindings do NOT require SWIG.
174 The examples/ directory includes some basic examples (the "simple vc"
175 and "simple vc compat" family of examples) of all these interfaces.
177 In principle, since we use SWIG to generate the native Java API, we
178 could support other languages as well. However, using CVC4 from other
179 languages is not supported, nor expected to work, at this time. If
180 you're interested in helping to develop, maintain, and test a language
181 binding, please contact us via the users' mailing list at
182 cvc-users@cs.nyu.edu.
184 *** Building CVC4 from a repository checkout
186 CVC4's main repository is kept on GitHub at:
188 https://github.com/CVC4/CVC4
190 and there are numerous experimental forks housed on GitHub as well,
191 by different developers, implementing various features.
193 The following tools and libraries are additionally required to build
194 CVC4 from from a repository checkout rather than from a prepared
202 First, use "./autogen.sh" to create the configure script. Then
203 proceed as normal for any distribution tarball. The parsers are
204 pre-generated for the tarballs, but don't exist in the repository;
205 hence the extra ANTLR3 requirement to generate the source code for the
206 parsers, when building from the repository.
208 *** Examples and tutorials are not built or installed
210 Examples are not built by "make" or "make install". See
211 examples/README for information on what to find in the examples/
212 directory, as well as information about building and installing them.
214 *** Appendix: Build architecture
216 The build system is generated by automake, libtool, and autoconf. It
217 is somewhat nonstandard, though, which (for one thing) requires that
218 GNU Make be used. If you ./configure in the top-level source
219 directory, the objects will actually all appear in
220 builds/${arch}/${build_id}. This is to allow multiple, separate
221 builds in the same place (e.g., an assertions-enabled debugging build
222 alongside a production build), without changing directories at the
223 shell. The "current" build is maintained, and you can still use
224 (e.g.) "make -C src/main" to rebuild objects in just one subdirectory.
226 You can also create your own build directory inside or outside of the
227 source tree and configure from there. All objects will then be built
228 in that directory, and you'll ultimately find the "cvc4" binary in
229 src/main/, and the libraries under src/ and src/parser/.