7 # use --prefix to specify an install prefix (default: /usr/local)
8 # use --name=<PATH> for custom build directory
9 # use --auto-download to download and build missing, required or
10 # enabled, dependencies
11 cd <build_dir> # default is ./build
12 make # use -jN for parallel build with N threads
13 make check # to run default set of tests
14 make install # to install into the prefix specified above
16 All binaries are built into ``<build_dir>/bin``, the cvc5 library is built into
20 Supported Operating Systems
21 ---------------------------
23 cvc5 can be built natively on Linux and macOS, cross-compilation is possible for
24 Windows using Mingw-w64. cvc5 also supports cross-compilation for ARM64 systems.
25 We generally recommend a 64-bit operating system.
31 On macOS, we recommend using `Homebrew <https://brew.sh/>`_ to install the
32 dependencies. We also have a Homebrew Tap available at
33 https://github.com/CVC4/homebrew-cvc4 .
34 Note that linking system libraries statically is
35 `strongly discouraged <https://developer.apple.com/library/archive/qa/qa1118/_index.html>`_
36 on macOS. Using ``./configure.sh --static-binary`` will thus produce a binary
37 that uses static versions of all our dependencies, but is still a dynamically
41 Cross-compiling for Windows
42 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
44 Cross-compiling cvc5 with Mingw-w64 can be done as follows:
48 ./configure.sh --win64 --static-binary <configure options...>
50 cd <build_dir> # default is ./build
51 make # use -jN for parallel build with N threads
53 The built binary ``cvc5.exe`` is located in ``<build_dir>/bin`` and the cvc5
54 library can be found in ``<build_dir>/lib``.
60 cvc5 makes uses of a number of tools and libraries. Some of these are required
61 while others are only used with certain configuration options. If
62 ``--auto-download`` is given, cvc5 can automatically download and build most
63 libraries that are not already installed on your system. If your libraries are
64 installed in a non-standard location, you can use ``--dep-path`` to define an
65 additional search path for all dependencies. Versions given are minimum
66 versions; more recent versions should be compatible.
68 - `GNU C and C++ (gcc and g++, >= 7) <https://gcc.gnu.org>`_
69 or `Clang (>= 5) <https://clang.llvm.org>`_
70 - `CMake >= 3.9 <https://cmake.org>`_
71 - `Python >= 3.6 <https://www.python.org>`_
72 + module `toml <https://pypi.org/project/toml/>`_
73 - `GMP v6.1 (GNU Multi-Precision arithmetic library) <https://gmplib.org>`_
74 - `ANTLR 3.4 <http://www.antlr3.org/>`_
75 - `CaDiCaL (SAT solver) <https://github.com/arminbiere/cadical>`_
76 - `Java >= 1.6 <https://www.java.com>`_
77 - `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_
80 ANTLR 3.4 parser generator
81 ^^^^^^^^^^^^^^^^^^^^^^^^^^
83 For most systems, the package manager no longer contains pre-packaged versions
84 of ANTLR 3.4. With ``--auto-download``, cvc5 will automatically download and
89 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
91 `CaDiCaL <https://github.com/arminbiere/cadical>`_ is a SAT solver that can be
92 used for the bit-vector solver. It can be downloaded and built automatically.
95 GMP (GNU Multi-Precision arithmetic library)
96 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
98 GMP is usually available on your distribution and should be used from there. If
99 it is not, or you want to cross-compile, or you want to build cvc5 statically
100 but the distribution does not ship static libraries, cvc5 builds GMP
101 automatically when ``--auto-download`` is given.
104 SymFPU (Support for the Theory of Floating Point Numbers)
105 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
107 `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_ is an implementation
108 of SMT-LIB/IEEE-754 floating-point operations in terms of bit-vector operations.
109 It is required for supporting the theory of floating-point numbers and can be
110 downloaded and built automatically.
113 Optional Dependencies
114 ---------------------
117 CryptoMiniSat (Optional SAT solver)
118 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
120 `CryptoMinisat <https://github.com/msoos/cryptominisat>`_ is a SAT solver that
121 can be used for solving bit-vector problems with eager bit-blasting. This
122 dependency may improve performance. It can be downloaded and built
123 automatically. Configure cvc5 with ``configure.sh --cryptominisat`` to build
124 with this dependency.
127 Kissat (Optional SAT solver)
128 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
130 `Kissat <https://github.com/arminbiere/kissat>`_ is a SAT solver that can be
131 used for solving bit-vector problems with eager bit-blasting. This dependency
132 may improve performance. It can be downloaded and built automatically. Configure
133 cvc5 with ``configure.sh --kissat`` to build with this dependency.
136 LibPoly (Optional polynomial library)
137 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
139 `LibPoly <https://github.com/SRI-CSL/libpoly>`_ is required for CAD-based
140 nonlinear reasoning. It can be downloaded and built automatically. Configure
141 cvc5 with ``configure.sh --poly`` to build with this dependency.
144 CLN >= v1.3 (Class Library for Numbers)
145 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
147 `CLN <http://www.ginac.de/CLN>`_ is an alternative multiprecision arithmetic
148 package that may offer better performance and memory footprint than GMP.
149 Configure cvc5 with ``configure.sh --cln`` to build with this dependency.
151 Note that CLN is covered by the `GNU General Public License, version 3
152 <https://www.gnu.org/licenses/gpl-3.0.en.html>`_. If you choose to use cvc5 with
153 CLN support, you are licensing cvc5 under that same license. (Usually cvc5's
154 license is more permissive than GPL, see the file `COPYING` in the cvc5 source
155 distribution for details.)
158 glpk-cut-log (A fork of the GNU Linear Programming Kit)
159 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
161 `glpk-cut-log <https://github.com/timothy-king/glpk-cut-log/>`_ is a fork of
162 `GLPK <http://www.gnu.org/software/glpk/>`_ (the GNU Linear Programming Kit).
163 This can be used to speed up certain classes of problems for the arithmetic
164 implementation in cvc5. (This is not recommended for most users.)
166 glpk-cut-log can be installed using the ``contrib/get-glpk-cut-log`` script.
167 Note that the only installation option is manual installation via this script.
168 cvc5 is no longer compatible with the main GLPK library. Configure cvc5 with
169 ``configure.sh --glpk`` to build with this dependency.
171 Note that GLPK and glpk-cut-log are covered by the `GNU General Public License,
172 version 3 <https://www.gnu.org/licenses/gpl-3.0.en.html>`_. If you choose to use
173 cvc5 with GLPK support, you are licensing cvc5 under that same license. (Usually
174 cvc5's license is more permissive; see above discussion.)
177 ABC library (Improved Bit-Vector Support)
178 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
180 `ABC <http://www.eecs.berkeley.edu/~alanmi/abc/>`_ (A System for Sequential
181 Synthesis and Verification) is a library for synthesis and verification of logic
182 circuits. This dependency may improve performance of the eager bit-vector
183 solver. When enabled, the bit-blasted formula is encoded into
184 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
186 ABC can be installed using the ``contrib/get-abc`` script. Configure cvc5 with
187 ``configure.sh --abc`` to build with this dependency.
190 Editline library (Improved Interactive Experience)
191 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
193 The `Editline Library <https://thrysoee.dk/editline/>`_ library is optionally
194 used to provide command editing, tab completion, and history functionality at
195 the cvc5 prompt (when running in interactive mode). Check your distribution for
196 a package named "libedit-dev" or "libedit-devel" or similar.
199 Google Test Unit Testing Framework (Unit Tests)
200 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
202 `Google Test <https://github.com/google/googletest>`_ is required to optionally
203 run cvc5's unit tests (included with the distribution). See :ref:`Testing cvc5
204 <testing-cvc5>` below for more details.
210 cvc5 provides a complete and flexible C++ API (see ``examples/api`` for
211 examples). It further provides Java (see ``examples/SimpleVC.java`` and
212 ``examples/api/java``) and Python (see ``examples/api/python``) API bindings.
214 Configure cvc5 with ``configure.sh --<lang>-bindings`` to build with language
215 bindings for ``<lang>``.
218 Dependencies for Language Bindings
219 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
223 - `Cython <https://cython.org/>`_
224 - `scikit-build <https://pypi.org/project/scikit-build/>`_
225 - `pytest <https://docs.pytest.org/en/6.2.x/>`_
227 If you're interested in helping to develop, maintain, and test a language
228 binding, please contact the cvc5 team via `our issue tracker
229 <https://github.com/cvc5/cvc5/issues>`_.
232 Building the API Documentation
233 ------------------------------
235 Building the API documentation of cvc5 requires the following dependencies:
237 - `Doxygen <https://www.doxygen.nl>`_
238 - `Sphinx <https://www.sphinx-doc.org>`_,
239 `sphinx-tabs <https://sphinx-tabs.readthedocs.io/>`_,
240 `sphinxcontrib-bibtex <https://sphinxcontrib-bibtex.readthedocs.io>`_
241 - `Breathe <https://breathe.readthedocs.io>`_
243 To build the documentation, configure cvc5 with ``./configure.sh --docs`` and
244 run ``make docs`` from within the build directory.
246 The API documentation can then be found at
247 ``<build_dir>/docs/sphinx/index.html``.
249 To build the documentation for GitHub pages, change to the build directory and
250 call ``make docs-gh``. The content of directory ``<build_dir>/docs/sphinx-gh``
251 can then be copied over to GitHub pages.
254 Building the Examples
255 ---------------------
257 See ``examples/README.md`` for instructions on how to build and run the
266 We use ``ctest`` as test infrastructure. For all command-line options of ctest,
267 see ``ctest -h``. Some useful options are:
271 ctest -R <regex> # run all tests with names matching <regex>
272 ctest -E <regex> # exclude tests with names matching <regex>
273 ctest -L <regex> # run all tests with labels matching <regex>
274 ctest -LE <regex> # exclude tests with labels matching <regex>
275 ctest # run all tests
276 ctest -jN # run all tests in parallel with N threads
277 ctest --output-on-failure # run all tests and print output of failed tests
279 We have 4 categories of tests:
281 - **examples** in directory ``examples`` (label: **example**)
282 - **regression tests** (5 levels) in directory ``test/regress`` (label:
283 **regressN** with N the regression level)
284 - **api tests** in directory ``test/api`` (label: **api**)
285 - **unit tests** in directory ``test/unit`` (label: **unit**)
291 The system tests are not built by default.
295 make apitests # build and run all system tests
296 make <api_test> # build test/system/<system_test>.<ext>
297 ctest api/<api_test> # run test/system/<system_test>.<ext>
299 All system test binaries are built into ``<build_dir>/bin/test/system``.
301 We use prefix ``api/`` + ``<api_test>`` (for ``<api_test>`` in ``test/api``)
306 make ouroborous # build test/api/ouroborous.cpp
307 ctest -R ouroborous # run all tests that match '*ouroborous*'
308 # > runs api/ouroborous
309 ctest -R ouroborous$ # run all tests that match '*ouroborous'
310 # > runs api/ouroborous
311 ctest -R api/ouroborous$ # run all tests that match '*api/ouroborous'
312 # > runs api/ouroborous
318 The unit tests are not built by default.
320 Note that cvc5 can only be configured with unit tests in non-static builds with
325 make units # build and run all unit tests
326 make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext>
327 ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext>
329 All unit test binaries are built into ``<build_dir>/bin/test/unit``.
331 We use prefix ``unit/`` + ``<subdir>/`` + ``<unit_test>`` (for ``<unit_test>``
332 in ``test/unit/<subdir>``) as test target name.
336 make map_util_black # build test/unit/base/map_util_black.cpp
337 ctest -R map_util_black # run all tests that match '*map_util_black*'
338 # > runs unit/base/map_util_black
339 ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black'
340 # > runs unit/base/map_util_black
341 ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black'
342 # > runs unit/base/map_util_black
345 Testing Regression Tests
346 ^^^^^^^^^^^^^^^^^^^^^^^^
348 We use prefix ``regressN/`` + ``<subdir>/`` + ``<regress_test>`` (for
349 ``<regress_test>`` in level ``N`` in ``test/regress/regressN/<subdir>``) as test
354 ctest -L regress # run all regression tests
355 ctest -L regress0 # run all regression tests in level 0
356 ctest -L regress[0-1] # run all regression tests in level 0 and 1
357 ctest -R regress # run all regression tests
358 ctest -R regress0 # run all regression tests in level 0
359 ctest -R regress[0-1] # run all regression tests in level 0 and 1
360 ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*'
361 # > runs regress0/bug288b
367 All custom test targets build and run a preconfigured set of tests.
369 - ``make check [-jN] [ARGS=-jN]``
370 The default build-and-test target for cvc5, builds and runs all examples,
371 all system and unit tests, and regression tests from levels 0 to 2.
373 - ``make systemtests [-jN] [ARGS=-jN]``
374 Build and run all system tests.
376 - ``make units [-jN] [ARGS=-jN]``
377 Build and run all unit tests.
379 - ``make regress [-jN] [ARGS=-jN]``
380 Build and run regression tests from levels 0 to 2.
382 - ``make runexamples [-jN] [ARGS=-jN]``
383 Build and run all examples.
385 - ``make coverage-test [-jN] [ARGS=-jN]``
386 Build and run all tests (system and unit tests, regression tests level 0-4)
387 with gcov to determine code coverage.
389 We use ``ctest`` as test infrastructure, and by default all test targets
390 are configured to **run** in parallel with the maximum number of threads
391 available on the system. Override with ``ARGS=-jN``.
393 Use ``-jN`` for parallel **building** with ``N`` threads.
396 Recompiling a specific cvc5 version with different LGPL library versions
397 ------------------------------------------------------------------------
399 To recompile a specific static binary of cvc5 with different versions of the
400 linked LGPL libraries perform the following steps:
402 1. Make sure that you have installed the desired LGPL library versions.
403 You can check the versions found by cvc5's build system during the configure
406 2. Determine the commit sha and configuration of the cvc5 binary
412 3. Download the specific source code version:
416 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
418 4. Extract the source code
422 tar xf <commit-sha>.tar.gz
424 5. Change into source code directory
430 6. Configure cvc5 with options listed by ``cvc5 --show-config``
434 ./configure.sh --static-binary <options>
436 7. Follow remaining steps from `build instructions <#building-cvc5>`_