-CVC4 release version 1.5.
+CVC4 prerelease version 1.7.
-*** Quick-start instructions
+** Quick-start instructions
-*** Build dependences
+*** 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++), reasonably recent versions
+ GNU C and C++ (gcc and g++) or Clang, reasonably recent versions
GNU Make
GNU Bash
GMP v4.2 (GNU Multi-Precision arithmetic library)
- MacPorts [only if on a Mac; see below]
libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)
The Boost C++ base libraries
-The hardest to obtain and install is the libantlr3c requirement, so
-that one is explained next.
-
-On a Mac, you need to additionally install MacPorts (see
-http://www.macports.org/). Doing so is easy. Then, simply run the
-script contrib/mac-build, which installs a few ports from the MacPorts
-repository, then compiles and installs antlr3c using the get-antlr-3.4
-script (as described next). The mac-build script should set you up
-with all requirements, and will tell you how to configure CVC4 when it
-completes successfully.
+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,
*** 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
+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 .)
-*** Building CVC4
-
-The hardest build dependence to satisfy is libantlr3c; that's why it
-is explained above. Problems in satisfying other build dependences are
-explained below.
-
-Once the build dependences are satisfied, you should be able to
-configure, make, make check, and make install without incident:
-
- ./autogen.sh
- ./configure [use --prefix to specify a prefix; default /usr/local]
- make
- make check [optional but a good idea!]
-
-To build from a repository checkout (rather than a distributed CVC4
-tarball), there are additional dependences; 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.
-
*** Installing the Boost C++ base libraries
-A Boost package is available on most Linux distributions; 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.
+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 requirements
+*** Optional dependencies
None of these is required, but can improve CVC4 as described below:
- Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
+ 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: 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 won't work; you'll need 2.0, and the more
-recent the better. On Mac, we've seen SWIG segfault when generating
-CVC4 language bindings; version 2.0.8 or higher is recommended to
-avoid this. See "Language bindings" below for build instructions.
+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
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.
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.
+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
projects / cvc5.git / commitdiff