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/.

1 files changed, 43 insertions, 43 deletions

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 `<build_dir>/bin`, the CVC4 library is built into
+All binaries are built into `<build_dir>/bin`, the cvc5 library is built into
 `<build_dir>/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 <configure options...>
@@ -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 `<build_dir>/bin` and the CVC4 library
+The built binary `cvc5.exe` is located in `<build_dir>/bin` and the cvc5 library
 can be found in `<build_dir>/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 --<lang>-bindings` to build with language
+Configure cvc5 with `configure.sh --<lang>-bindings` to build with language
 bindings for `<lang>`.
 
 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 `<build_dir>/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/<subdir>`) 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 <commit-sha>.tar.gz
 ```
 cd CVC4-<commit-sha>
 ```
-6. Configure CVC4 with options listed by `cvc4 --show-config`
+6. Configure cvc5 with options listed by `cvc5 --show-config`
 ```
 ./configure.sh --static <options>
 ```
 
-7. Follow remaining steps from [build instructions](#building-cvc4)
+7. Follow remaining steps from [build instructions](#building-cvc5)