Installation 

Compilation on macOS 

On macOS, we recommend using Homebrew to install the dependencies. We also have a Homebrew Tap available at https://github.com/cvc5/homebrew-cvc5 . Note that linking system libraries statically is strongly discouraged on macOS. Using ./configure.sh --static will thus produce a binary that uses static versions of all our dependencies, but is still a dynamically linked binary.

Compilation on Windows 

Install MSYS2 and Python on your system. Launch a MINGW64 environment and install the required packages for building cvc5:

pacman -S git make mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp zip

Clone the cvc5 repository and follow the general build steps above. The built binary cvc5.exe and the DLL libraries are located in <build_dir>/bin . The import libraries and the static libraries can be found in <build_dir>/lib .

Cross-compiling for Windows 

Cross-compiling cvc5 with Mingw-w64 can be done as follows:

./configure.sh --win64 --static <configure options...>

cd <build_dir>   # default is ./build
make             # use -jN for parallel build with N threads

The built binary cvc5.exe and the DLL libraries are located in <build_dir>/bin . The import libraries and the static libraries can be found in <build_dir>/lib .

WebAssembly Compilation 

Compiling cvc5 to WebAssembly needs the Emscripten SDK (version 3.1.18 or latter). Setting up emsdk can be done as follows:

git clone https://github.com/emscripten-core/emsdk.git
cd emsdk
./emsdk install <version>   # <version> = '3.1.18' is preferable, but
                            # <version> = 'latest' has high chance of working
./emsdk activate <version>
source ./emsdk_env.sh   # Activate PATH and other environment variables in the
                        # current terminal. Whenever Emscripten is going to be
                        # used this command needs to be called before because
                        # emsdk doesn't insert the binaries paths directly in
                        # the system PATH variable.

Refer to the emscripten dependencies list to ensure that all required dependencies are installed on the system.

Then, in the cvc5 directory:

./configure.sh --static --static-binary --auto-download --wasm=<value> --wasm-flags='<emscripten flags>' <configure options...>

cd <build_dir>   # default is ./build
make             # use -jN for parallel build with N threads

--wasm can take three values: WASM (will generate the wasm file for cvc5), JS (not only the wasm, but the .js glue code for web integration) and HTML (both the last two files and also an .html file which supports the run of the glue code).

--wasm-flags take a string wrapped by a single quote containing the emscripten flags , which modifies how the wasm and glue code are built and how they behave. An -s should precede each flag.

For example, to generate a HTML page, use:

./configure.sh --static --static-binary --auto-download --wasm=HTML --name=prod

cd prod
make            # use -jN for parallel build with N threads

After that, you can run python -m http.server within prod/bin , open http://0.0.0.0:8000/cvc5.html with Chrome to visualize the page generated by Emscripten, write down a valid SMTLIB input, and press ESC twice to obtain its output.

On the other hand, to generate a modularized glue code to be imported by custom web pages, use:

./configure.sh --static --static-binary --auto-download --wasm=JS --wasm-flags='-s MODULARIZE' --name=prod

cd prod
make            # use -jN for parallel build with N threads

CaDiCaL (SAT solver) 

CaDiCaL is a SAT solver that can be used for the bit-vector solver. It can be downloaded and built automatically.

GMP (GNU Multi-Precision arithmetic library) 

GMP is usually available on your distribution and should be used from there. If it is not, or you want to cross-compile, or you want to build cvc5 statically but the distribution does not ship static libraries, cvc5 builds GMP automatically when --auto-download is given.

SymFPU (Support for the Theory of Floating Point Numbers) 

SymFPU 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 downloaded and built automatically.

CryptoMiniSat (Optional SAT solver) 

CryptoMinisat 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 downloaded and built automatically. Configure cvc5 with configure.sh --cryptominisat to build with this dependency.

Kissat (Optional SAT solver) 

Kissat 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 downloaded and built automatically. Configure cvc5 with configure.sh --kissat to build with this dependency.

LibPoly >= v0.1.13 (Optional polynomial library) 

LibPoly is required for CAD-based nonlinear reasoning. It can be downloaded and built automatically. Configure cvc5 with configure.sh --poly to build with this dependency.

CoCoA (Optional computer algebra library) 

CoCoA is required for some non-linear reasoning and for finite field reasoning. We use a patched version of it, so we recommend downloading it using the --auto-download configuration flag, which applies our patch automatically. It is included in the build through the --cocoa --gpl configuration flag.

CoCoA is covered by the GPLv3 license. See below for the ramifications of this.

CLN >= v1.3 (Class Library for Numbers) 

CLN is an alternative multiprecision arithmetic package that may offer better performance and memory footprint than GMP. Configure cvc5 with configure.sh --cln --gpl to build with this dependency.

Note that CLN is covered by the GNU General Public License, version 3 . If you choose to use cvc5 with CLN support, you are licensing cvc5 under that same license. (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 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 cvc5. (This is not recommended for most users.)

cvc5 is not compatible with the official version of the GLPK library. To use the patched version of it, we recommend downloading it using the --auto-download configuration flag, which applies the patch automatically. Configure cvc5 with configure.sh --glpk --gpl to build with this dependency.

Note that GLPK and glpk-cut-log are covered by the GNU General Public License, version 3 . If you choose to use cvc5 with GLPK support, you are licensing cvc5 under that same license. (Usually cvc5’s license is more permissive; see above discussion.)

Editline library (Improved Interactive Experience) 

The Editline Library library is optionally used to provide command editing, tab completion, and history functionality at the cvc5 prompt (when running in interactive mode). Check your distribution for a package named “libedit-dev” or “libedit-devel” or similar.

Google Test Unit Testing Framework (Unit Tests) 

Google Test is required to optionally run cvc5’s unit tests (included with the distribution). See Testing cvc5 below for more details.

Dependencies for Language Bindings 

• Java

  • JDK >= 1.8

• Python

  • Cython >= 3.0.0

  • pip >= 23.0

  • pytest

  • repairwheel >= 0.3.1

  • setuptools >= 66.1.0

  • The source for the pythonic API

If --auto-download is given, the Python modules will be installed automatically in a virtual environment if they are missing. To install the modules globally and skip the creation of the virtual environment, configure cvc5 with ./configure.sh --no-pyvenv .

If configured with --pythonic-path=PATH , the build system will expect the Pythonic API’s source to be at PATH . Otherwise, if configured with --auto-download , the build system will download it.

Installing the Python bindings after building from source requires a Python environment with pip version 20.3 or higher.

If you’re interested in helping to develop, maintain, and test a language binding, please contact the cvc5 team via our issue tracker .

Testing System Tests 

The system tests are not built by default.

make apitests                         # build and run all system tests
make <api_test>                       # build test/system/<system_test>.<ext>
ctest api/<api_test>                  # run test/system/<system_test>.<ext>

All system test binaries are built into <build_dir>/bin/test/system .

We use prefix api/ + <api_test> (for <api_test> in test/api ) as test target name.

make ouroborous                       # build test/api/ouroborous.cpp
ctest -R ouroborous                   # run all tests that match '*ouroborous*'
                                      # > runs api/ouroborous
ctest -R ouroborous$                  # run all tests that match '*ouroborous'
                                      # > runs api/ouroborous
ctest -R api/ouroborous$              # run all tests that match '*api/ouroborous'
                                      # > runs api/ouroborous

Testing Unit Tests 

The unit tests are not built by default.

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
make <unit_test>                      # build test/unit/<subdir>/<unit_test>.<ext>
ctest unit/<subdir>/<unit_test>       # run test/unit/<subdir>/<unit_test>.<ext>

All unit test binaries are built into <build_dir>/bin/test/unit .

We use prefix unit/ + <subdir>/ + <unit_test> (for <unit_test> in test/unit/<subdir> ) as test target name.

make map_util_black                   # build test/unit/base/map_util_black.cpp
ctest -R map_util_black               # run all tests that match '*map_util_black*'
                                      # > runs unit/base/map_util_black
ctest -R base/map_util_black$         # run all tests that match '*base/map_util_black'
                                      # > runs unit/base/map_util_black
ctest -R unit/base/map_util_black$    # run all tests that match '*unit/base/map_util_black'
                                      # > runs unit/base/map_util_black

Testing Regression Tests 

We use prefix regressN/ + <subdir>/ + <regress_test> (for <regress_test> in level N in test/regress/regressN/<subdir> ) as test target name.

ctest -L regress                      # run all regression tests
ctest -L regress0                     # run all regression tests in level 0
ctest -L regress[0-1]                 # run all regression tests in level 0 and 1
ctest -R regress                      # run all regression tests
ctest -R regress0                     # run all regression tests in level 0
ctest -R regress[0-1]                 # run all regression tests in level 0 and 1
ctest -R regress0/bug288b             # run all tests that match '*regress0/bug288b*'
                                      # > runs regress0/bug288b

Custom Targets 

All custom test targets build and run a preconfigured set of tests.

• make check [-jN] [ARGS=-jN] 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] Build and run all system tests.

• make units [-jN] [ARGS=-jN] Build and run all unit tests.

• make regress [-jN] [ARGS=-jN] Build and run regression tests from levels 0 to 2.

• make runexamples [-jN] [ARGS=-jN] Build and run all examples.

• make coverage-test [-jN] [ARGS=-jN] Build and run all tests (system and unit tests, regression tests level 0-4) with gcov to determine code coverage.

We use ctest as test infrastructure, and by default all test targets are configured to run in parallel with the maximum number of threads available on the system. Override with ARGS=-jN .

Use -jN for parallel building with N threads.