INSTALL

   1 CVC4 release version 1.5.
   2
   3 *** Quick-start instructions
   4
   5 *** Build dependences
   6
   7 The following tools and libraries are required to build and run CVC4.
   8 Versions given are minimum versions; more recent versions should be
   9 compatible.
  10
  11   GNU C and C++ (gcc and g++), reasonably recent versions
  12   GNU Make
  13   GNU Bash
  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
  18
  19 The hardest to obtain and install is the libantlr3c requirement, so
  20 that one is explained next.
  21
  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.
  29
  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.
  35
  36 *** Installing libantlr3c: ANTLR parser generator C support library
  37
  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.stanford.edu/wiki/Developer%27s_Guide#ANTLR3 .)
  45
  46 *** Building CVC4
  47
  48 The hardest build dependence to satisfy is libantlr3c; that's why it
  49 is explained above.  Problems in satisfying other build dependences are
  50 explained below.
  51
  52 Once the build dependences are satisfied, you should be able to
  53 configure, make, make check, and make install without incident:
  54
  55     ./autogen.sh
  56     ./configure   [use --prefix to specify a prefix; default /usr/local]
  57     make
  58     make check    [optional but a good idea!]
  59
  60 To build from a repository checkout (rather than a distributed CVC4
  61 tarball), there are additional dependences; see below.
  62
  63 You can then "make install" to install in the prefix you gave to
  64 the configure script (/usr/local by default).  ** You should run
  65 "make check" ** before installation to ensure that CVC4 has been
  66 built correctly.  In particular, GCC version 4.5.1 seems to have a
  67 bug in the optimizer that results in incorrect behavior (and wrong
  68 results) in many builds.  This is a known problem for Minisat, and
  69 since Minisat is at the core of CVC4, a problem for CVC4.  "make check"
  70 easily detects this problem (by showing a number of FAILed test cases).
  71 It is ok if the unit tests aren't run as part of "make check", but all
  72 system tests and regression tests should pass without incident.
  73
  74 To build API documentation, use "make doc".  Documentation is produced
  75 under doc/ but is not installed by "make install".
  76
  77 Examples and tutorials are not installed with "make install."  You may
  78 want to "make install-examples".  See below.
  79
  80 For more information about the build system itself (probably not
  81 necessary for casual users), see the Appendix at the bottom of this
  82 file.
  83
  84 *** Installing the Boost C++ base libraries
  85
  86 A Boost package is available on most Linux distributions; check yours
  87 for a package named something like libboost-dev or boost-devel.  There
  88 are a number of additional Boost packages in some distributions, but
  89 this "basic" one should be sufficient for building CVC4.
  90
  91 Should you want to install Boost manually, or to learn more about the
  92 Boost project, please visit http://www.boost.org/.
  93
  94 *** Optional requirements
  95
  96 None of these is required, but can improve CVC4 as described below:
  97
  98   Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
  99   Optional: CLN v1.3 or newer (Class Library for Numbers)
 100   Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit)
 101   Optional: ABC library (for improved bitvector support)
 102   Optional: GNU Readline library (for an improved interactive experience)
 103   Optional: The Boost C++ threading library (libboost_thread)
 104   Optional: CxxTest unit testing framework
 105
 106 SWIG is necessary to build the Java API (and of course a JDK is
 107 necessary, too).  SWIG 1.x won't work; you'll need 2.0, and the more
 108 recent the better.  On Mac, we've seen SWIG segfault when generating
 109 CVC4 language bindings; version 2.0.8 or higher is recommended to
 110 avoid this.  See "Language bindings" below for build instructions.
 111
 112 CLN is an alternative multiprecision arithmetic package that can offer
 113 better performance and memory footprint than GMP.  CLN is covered by
 114 the GNU General Public License, version 3; so if you choose to use
 115 CVC4 with CLN support, you are licensing CVC4 under that same license.
 116 (Usually CVC4's license is more permissive than GPL is; see the file
 117 COPYING in the CVC4 source distribution for details.)  Please visit
 118 http://www.ginac.de/CLN/ for more details about CLN.
 119
 120 glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit).
 121 This can be used to speed up certain classes of problems for the arithmetic
 122 implementation in CVC4. (This is not recommended for most users.) The source
 123 code for glpk-cut-log is available at:
 124 https://github.com/timothy-king/glpk-cut-log/
 125 The only option for installation of glpk-cut-log is downloading the library,
 126 compiling and installing it manually.  CVC4 is no longer compatible with the
 127 main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public
 128 License, version 3; so if you choose to use CVC4 with GLPK support, you are
 129 licensing CVC4 under that same license.
 130 (Usually CVC4's license is more permissive; see above discussion.)
 131 Please visit http://www.gnu.org/software/glpk/ for more details about GLPK.
 132
 133 ABC: A System for Sequential Synthesis and Verification is a library
 134 for synthesis and verification of logic circuits. This can be used to
 135 speed up the eager bit-vector solver by first encoding the bit-blasted
 136 formula into AIG format and then using ABC to simplify the AIG. To
 137 install abc run the contrib/get-abc script which will download and
 138 install a compatible version of ABC in the cvc4 directory. To configure
 139 CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where
 140 PATH corresponds to the install path of ABC. To run CVC4 using ABC use
 141 the --bitblast-aig command line argument.
 142 Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details
 143 on ABC.
 144
 145 The GNU Readline library is optionally used to provide command
 146 editing, tab completion, and history functionality at the CVC prompt
 147 (when running in interactive mode).  Check your distribution for a
 148 package named "libreadline-dev" or "readline-devel" or similar.  This
 149 library is covered by the GNU General Public License, version 3.  Like
 150 the above-mentioned libraries, if you choose to use CVC4 with readline
 151 support, you are licensing CVC4 under that same license.  (Please visit
 152 http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more
 153 details about readline.)
 154
 155 The Boost C++ threading library (often packaged independently of the
 156 Boost base library) is needed to run CVC4 in "portfolio"
 157 (multithreaded) mode.  Check your distribution for a package named
 158 "libboost-thread-dev" or similar.
 159
 160 CxxTest is necessary to run CVC4's unit tests (included with the
 161 distribution).  Running these is not really required for users of
 162 CVC4; "make check" will skip unit tests if CxxTest isn't available,
 163 and go on to run the extensive system- and regression-tests in the
 164 source tree.  However, if you're interested, you can download CxxTest
 165 at http://cxxtest.com/ .
 166
 167 *** Language bindings
 168
 169 There are several options available for using CVC4 from the API.
 170
 171 First, CVC4 offers a complete and flexible API for manipulating
 172 expressions, maintaining a stack of assertions, and checking
 173 satisfiability, and related things.  The C++ libraries (libcvc4.so and
 174 libcvc4parser.so) and required headers are installed normally via a
 175 "make install".  This API is also available from Java (via CVC4.jar
 176 and libcvc4jni.so) by configuring with --enable-language-bindings=java.
 177 You'll also need SWIG 2.0 installed (and you might need to help
 178 configure find it if you installed it in a nonstandard place with
 179 --with-swig-dir=/path/to/swig/installation).  You may also need to
 180 give the configure script the path to your Java headers (in
 181 particular, jni.h).  You might do so with (for example):
 182
 183   ./configure --enable-language-bindings=java \
 184       JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
 185
 186 There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h>
 187 and link against libcvc4compat.so) that attempts to maintain
 188 source-level backwards-compatibility with the CVC3 C++ API.  The
 189 compatibility library is built by default, and
 190 --enable-language-bindings=java enables the Java compatibility library
 191 (CVC4compat.jar and libcvc4compatjni.so).
 192 --enable-language-bindings=c enables the C compatibility library
 193 (#include <cvc4/bindings/compat/c/c_interface.h> and link against
 194 libcvc4bindings_c_compat.so), and if you want both C and Java
 195 bindings, use --enable-language-bindings=c,java.  These compatibility
 196 language bindings do NOT require SWIG.
 197
 198 The examples/ directory includes some basic examples (the "simple vc"
 199 and "simple vc compat" family of examples) of all these interfaces.
 200
 201 In principle, since we use SWIG to generate the native Java API, we
 202 could support other languages as well.  However, using CVC4 from other
 203 languages is not supported, nor expected to work, at this time.  If
 204 you're interested in helping to develop, maintain, and test a language
 205 binding, please contact one of the project leaders.
 206
 207 *** Building CVC4 from a repository checkout
 208
 209 CVC4's main repository is kept on GitHub at:
 210
 211   https://github.com/CVC4/CVC4
 212
 213 and there are numerous experimental forks housed on GitHub as well,
 214 by different developers, implementing various features.
 215
 216 The following tools and libraries are additionally required to build
 217 CVC4 from from a repository checkout rather than from a prepared
 218 source tarball.
 219
 220   Automake v1.11 or later
 221   Autoconf v2.61 or later
 222   Libtool v2.2 or later
 223   ANTLR3 v3.2 or v3.4
 224
 225 First, use "./autogen.sh" to create the configure script.  Then
 226 proceed as normal for any distribution tarball.  The parsers are
 227 pre-generated for the tarballs, but don't exist in the repository;
 228 hence the extra ANTLR3 requirement to generate the source code for the
 229 parsers, when building from the repository.
 230
 231 *** Examples and tutorials are not built or installed
 232
 233 Examples are not built by "make" or "make install".  See
 234 examples/README for information on what to find in the examples/
 235 directory, as well as information about building and installing them.
 236
 237 *** Appendix: Build architecture
 238
 239 The build system is generated by automake, libtool, and autoconf.  It
 240 is somewhat nonstandard, though, which (for one thing) requires that
 241 GNU Make be used.  If you ./configure in the top-level source
 242 directory, the objects will actually all appear in
 243 builds/${arch}/${build_id}.  This is to allow multiple, separate
 244 builds in the same place (e.g., an assertions-enabled debugging build
 245 alongside a production build), without changing directories at the
 246 shell.  The "current" build is maintained until you re-configure.
 247
 248 You can also create your own build directory inside or outside of the
 249 source tree and configure from there.  All objects will then be built
 250 in that directory, and you'll ultimately find the "cvc4" binary in
 251 src/main/, and the libraries under src/ and src/parser/.