From ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 21 Apr 2021 10:21:34 -0700 Subject: Goodbye CVC4, hello cvc5! (#6371) This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/. --- INSTALL.md | 86 +++++++++++++++++++++++++++++++------------------------------- 1 file changed, 43 insertions(+), 43 deletions(-) (limited to 'INSTALL.md') diff --git a/INSTALL.md b/INSTALL.md index 14290afca..8d7bf44c7 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,7 +1,7 @@ CVC4 prerelease version 1.9 =========================== -## Building CVC4 +## Building cvc5 ./contrib/get-antlr-3.4 # download and build ANTLR ./configure.sh # use --prefix to specify a prefix (default: /usr/local) @@ -11,12 +11,12 @@ CVC4 prerelease version 1.9 make check # to run default set of tests make install # to install into the prefix specified above -All binaries are built into `/bin`, the CVC4 library is built into +All binaries are built into `/bin`, the cvc5 library is built into `/lib`. ## Supported Operating Systems -CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled +cvc5 can be built on Linux and macOS. For Windows, cvc5 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 @@ -27,7 +27,7 @@ To build a static binary for macOS, use: ### Cross-compiling for Windows -Cross-compiling CVC4 with Mingw-w64 can be done as follows: +Cross-compiling cvc5 with Mingw-w64 can be done as follows: ``` ./configure.sh --win64 --static @@ -36,12 +36,12 @@ Cross-compiling CVC4 with Mingw-w64 can be done as follows: make # use -jN for parallel build with N threads ``` -The built binary `cvc4.exe` is located in `/bin` and the CVC4 library +The built binary `cvc5.exe` is located in `/bin` and the cvc5 library can be found in `/lib`. ## Build dependencies -The following tools and libraries are required to build and run CVC4. +The following tools and libraries are required to build and run cvc5. Versions given are minimum versions; more recent versions should be compatible. @@ -64,14 +64,14 @@ For libantlr3c, you can use the script `contrib/get-antlr-3.4`. This will download, patch, and install libantlr3c. If you're on a 32-bit machine, or if you have difficulty building -libantlr3c (or difficulty getting CVC4 to link against it), you +libantlr3c (or difficulty getting cvc5 to link against it), you may need to remove the configure option `--enable-64bit` in the script. ### Warning: GCC 4.5.1 GCC version 4.5.1 seems to have a bug in the optimizer that may result 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. +for MiniSat, and since MiniSat is at the core of cvc5, a problem for cvc5. We recommend using a GCC version > 4.5.1. ### Warning: Installing GMP via `contrib/get-gmp-dev` @@ -82,7 +82,7 @@ your distribution `contrib/get-gmp-dev` is used in `configure.sh` when cross-compiling GMP for Windows. * does not ship with static GMP libraries (e.g., Arch Linux) - and you want to build CVC4 statically. + and you want to build cvc5 statically. In most of the cases the GMP version installed on your system is the one you want and should use. @@ -96,7 +96,7 @@ is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms of bit-vector operations. It is required for supporting the theory of floating-point numbers and can be installed using the `contrib/get-symfpu` script. -Configure CVC4 with `configure.sh --symfpu` to build with this dependency. +Configure cvc5 with `configure.sh --symfpu` to build with this dependency. ### CaDiCaL (Optional SAT solver) @@ -104,7 +104,7 @@ Configure CVC4 with `configure.sh --symfpu` to build with this dependency. is a SAT solver that can be used for solving non-incremental bit-vector problems with eager bit-blasting. This dependency may improve performance. It can be installed using the `contrib/get-cadical script`. -Configure CVC4 with `configure.sh --cadical` to build with this dependency. +Configure cvc5 with `configure.sh --cadical` to build with this dependency. ### CryptoMiniSat (Optional SAT solver) @@ -112,7 +112,7 @@ Configure CVC4 with `configure.sh --cadical` to build with this dependency. is a SAT solver that can be used for solving bit-vector problems with eager bit-blasting. This dependency may improve performance. It can be installed using the `contrib/get-cryptominisat` script. -Configure CVC4 with `configure.sh --cryptominisat` to build with this +Configure cvc5 with `configure.sh --cryptominisat` to build with this dependency. ### Kissat (Optional SAT solver) @@ -121,44 +121,44 @@ dependency. is a SAT solver that can be used for solving bit-vector problems with eager bit-blasting. This dependency may improve performance. It can be installed using the `contrib/get-kissat` script. -Configure CVC4 with `configure.sh --kissat` to build with this +Configure cvc5 with `configure.sh --kissat` to build with this dependency. ### LibPoly (Optional polynomial library) [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning. It can be installed using the `contrib/get-poly` script. -Configure CVC4 with `configure.sh --poly` to build with this dependency. +Configure cvc5 with `configure.sh --poly` to build with this dependency. ### CLN >= v1.3 (Class Library for Numbers) [CLN](http://www.ginac.de/CLN) is an alternative multiprecision arithmetic package that may offer better performance and memory footprint than GMP. -Configure CVC4 with `configure.sh --cln` to build with this dependency. +Configure cvc5 with `configure.sh --cln` to build with this dependency. Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). -If you choose to use CVC4 with CLN support, you are licensing CVC4 under that +If you choose to use cvc5 with CLN support, you are licensing cvc5 under that same license. -(Usually CVC4's license is more permissive than GPL, see the file `COPYING` in -the CVC4 source distribution for details.) +(Usually cvc5's license is more permissive than GPL, see the file `COPYING` in +the cvc5 source distribution for details.) ### glpk-cut-log (A fork of the GNU Linear Programming Kit) [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of [GLPK](http://www.gnu.org/software/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.) +implementation in cvc5. (This is not recommended for most users.) glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script. Note that the only installation option is manual installation via this script. -CVC4 is no longer compatible with the main GLPK library. -Configure CVC4 with `configure.sh --glpk` to build with this dependency. +cvc5 is no longer compatible with the main GLPK library. +Configure cvc5 with `configure.sh --glpk` to build with this dependency. Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). -If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that +If you choose to use cvc5 with GLPK support, you are licensing cvc5 under that same license. -(Usually CVC4's license is more permissive; see above discussion.) +(Usually cvc5's license is more permissive; see above discussion.) ### ABC library (Improved Bit-Vector Support) @@ -169,33 +169,33 @@ bit-vector solver. When enabled, the bit-blasted formula is encoded into and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. ABC can be installed using the `contrib/get-abc` script. -Configure CVC4 with `configure.sh --abc` to build with this dependency. +Configure cvc5 with `configure.sh --abc` to build with this dependency. ### Editline library (Improved Interactive Experience) The [Editline Library](https://thrysoee.dk/editline/) library is optionally used to provide command editing, tab completion, and history functionality at -the CVC4 prompt (when running in interactive mode). Check your distribution +the cvc5 prompt (when running in interactive mode). Check your distribution for a package named "libedit-dev" or "libedit-devel" or similar. ### Boost C++ base libraries (Examples) The [Boost](http://www.boost.org) C++ base library is needed for some examples -provided with CVC4. +provided with cvc5. ### Google Test Unit Testing Framework (Unit Tests) [Google Test](https://github.com/google/googletest) is required to optionally -run CVC4's unit tests (included with the distribution). -See [Testing CVC4](#Testing-CVC4) below for more details. +run cvc5's unit tests (included with the distribution). +See [Testing cvc5](#Testing-cvc5) below for more details. ## Language bindings -CVC4 provides a complete and flexible C++ API (see `examples/api` for +cvc5 provides a complete and flexible C++ API (see `examples/api` for examples). It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`) and Python (see `examples/api/python`) API bindings. -Configure CVC4 with `configure.sh ---bindings` to build with language +Configure cvc5 with `configure.sh ---bindings` to build with language bindings for ``. If you're interested in helping to develop, maintain, and test a language @@ -204,13 +204,13 @@ binding, please contact one of the project leaders. ## Building the API Documentation -Building the API documentation of CVC4 requires the following dependencies: +Building the API documentation of cvc5 requires the following dependencies: * [Doxygen](https://www.doxygen.nl) * [Sphinx](https://www.sphinx-doc.org) * [Breathe](https://breathe.readthedocs.io) -To build the documentation, configure CVC4 with `./configure.sh --docs`. -Building CVC4 will then include building the API documentation. +To build the documentation, configure cvc5 with `./configure.sh --docs`. +Building cvc5 will then include building the API documentation. The API documentation can then be found at `/docs/sphinx/index.html`. @@ -226,7 +226,7 @@ can then be copied over to GitHub pages. See `examples/README.md` for instructions on how to build and run the examples. -## Testing CVC4 +## Testing cvc5 We use `ctest` as test infrastructure, for all command-line options of ctest, see `ctest -h`. Some useful options are: @@ -273,7 +273,7 @@ as test target name. The unit tests are not built by default. -Note that CVC4 can only be configured with unit tests in non-static builds with +Note that cvc5 can only be configured with unit tests in non-static builds with assertions enabled. make units # build and run all unit tests @@ -311,7 +311,7 @@ in level `N` in `test/regress/regressN/`) as test target name. All custom test targets build and run a preconfigured set of tests. - `make check [-jN] [ARGS=-jN]` - The default build-and-test target for CVC4, builds and runs all examples, + The default build-and-test target for cvc5, builds and runs all examples, all system and unit tests, and regression tests from levels 0 to 2. - `make systemtests [-jN] [ARGS=-jN]` @@ -337,18 +337,18 @@ available on the system. Override with `ARGS=-jN`. Use `-jN` for parallel **building** with `N` threads. -## Recompiling a specific CVC4 version with different LGPL library versions +## Recompiling a specific cvc5 version with different LGPL library versions -To recompile a specific static binary of CVC4 with different versions of the +To recompile a specific static binary of cvc5 with different versions of the linked LGPL libraries perform the following steps: 1. Make sure that you have installed the desired LGPL library versions. - You can check the versions found by CVC4's build system during the configure + You can check the versions found by cvc5's build system during the configure phase. -2. Determine the commit sha and configuration of the CVC4 binary +2. Determine the commit sha and configuration of the cvc5 binary ``` -cvc4 --show-config +cvc5 --show-config ``` 3. Download the specific source code version: ``` @@ -362,9 +362,9 @@ tar xf .tar.gz ``` cd CVC4- ``` -6. Configure CVC4 with options listed by `cvc4 --show-config` +6. Configure cvc5 with options listed by `cvc5 --show-config` ``` ./configure.sh --static ``` -7. Follow remaining steps from [build instructions](#building-cvc4) +7. Follow remaining steps from [build instructions](#building-cvc5) -- cgit v1.2.3