CVC4 prerelease version 1.7. ** Quick-start instructions *** Supported operating systems CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled using Mingw-w64. We recommend a 64-bit operating system. On macOS, we recommend using Homebrew (https://brew.sh/) to install the dependencies. We also have a Homebrew Tap available at https://github.com/CVC4/homebrew-cvc4 . *** Build dependencies The following tools and libraries are required to build and run CVC4. Versions given are minimum versions; more recent versions should be compatible. GNU C and C++ (gcc and g++) or Clang, 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 Some features, such as the theory of floating-point numbers, require optional dependencies, please refer to the section "Optional dependencies" below for details. 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. 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://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#ANTLR3 .) *** Installing the Boost C++ base libraries A Boost package is available on most Linux distributions and Homebrew; 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 dependencies None of these is required, but can improve CVC4 as described below: Optional: SymFPU (an implementation of SMT-LIB/IEEE-754 floating-point operations in terms of bit-vector operations) Optional: CaDiCaL (optional SAT solver) Optional: CryptoMiniSat (optional SAT solver) Optional: LFSC (the LFSC proof checker) Optional: SWIG 3.0.x (Simplified Wrapper and Interface Generator) Optional: CLN v1.3 or newer (Class Library for Numbers) Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit) Optional: ABC library (for improved bitvector support) Optional: GNU Readline library (for an improved interactive experience) Optional: The Boost C++ threading library (libboost_thread) Optional: CxxTest unit testing framework SymFPU is required for supporting the theory of floating-point numbers. It can be installed using the contrib/get-symfpu script. Use --with-symfpu when configuring CVC4 to build with the dependency. CaDiCaL is a SAT solver that can be used for solving non-incremental bit-vector problems when using eager bit-blasting. This dependency may improve performance. It can be installed using the contrib/get-cadical script. Use --with-cadical when configuring CVC4 to build with this dependency. CryptoMiniSat is a SAT solver that can be used for solving bit-vector problems when using eager bit-blasting. This dependency may improve performance. It can be installed using the contrib/get-cryptominisat script. Use --with-cryptominisat when configuring CVC4 to build with this dependency. LFSC is required to check proofs internally with --check-proofs. It can be installed using the contrib/get-lfsc script. Use --with-lfsc when configuring CVC4 to build with this dependency. SWIG is necessary to build the Java API (and of course a JDK is necessary, too). SWIG 1.x/2.x won't work; you'll need 3.0, and the more recent the better. See "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. glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit). This can be used to speed up certain classes of problems for the arithmetic implementation in CVC4. (This is not recommended for most users.) The source code for glpk-cut-log is available at: https://github.com/timothy-king/glpk-cut-log/ The only option for installation of glpk-cut-log is downloading the library, compiling and installing it manually. CVC4 is no longer compatible with the main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public License, version 3; so if you choose to use CVC4 with GLPK support, you are licensing CVC4 under that same license. (Usually CVC4's license is more permissive; see above discussion.) Please visit http://www.gnu.org/software/glpk/ for more details about GLPK. ABC: A System for Sequential Synthesis and Verification is a library for synthesis and verification of logic circuits. This can be used to speed up the eager bit-vector solver by first encoding the bit-blasted formula into AIG format and then using ABC to simplify the AIG. To install abc run the contrib/get-abc script which will download and install a compatible version of ABC in the cvc4 directory. To configure CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where PATH corresponds to the install path of ABC. To run CVC4 using ABC use the --bitblast-aig command line argument. Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details on ABC. 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. This library is covered by the GNU General Public License, version 3. Like the above-mentioned libraries, if you choose to use CVC4 with readline support, you are licensing CVC4 under that same license. (Please visit http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more details about readline.) 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 CVC4 Once the build dependencies are satisfied, you should be able to configure, make, make check, and make install without incident: ./autogen.sh [not required when building from a source distribution] ./configure [use --prefix to specify a prefix; default /usr/local use --with-* to use optional dependencies] make make check [optional but a good idea!] To build from a repository checkout (rather than a distributed CVC4 tarball), there are additional dependencies; see below. 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". Examples and tutorials are not installed with "make install." You may want to "make install-examples". See below. For more information about the build system itself (probably not necessary for casual users), see the Appendix at the bottom of this file. *** 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 The examples/ directory includes some basic examples (the "simple vc" 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 one of the project leaders. *** Building CVC4 from a repository checkout CVC4's main repository is kept on GitHub at: https://github.com/CVC4/CVC4 and there are numerous experimental forks housed on GitHub as well, by different developers, implementing various features. 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 or later Autoconf v2.61 or later Libtool v2.2 or later ANTLR3 v3.2 or v3.4 Python (2.x or 3.x) 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 requirement to generate the source code for the parsers, when building from the repository. Similarly, Python is required for generating some of the code. *** Examples and tutorials are not built or installed Examples are not built by "make" or "make install". See examples/README 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 until you re-configure. 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/.