INSTALL

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