1 cvc5 prerelease version 1.0
2 ===========================
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
19 ## Supported Operating Systems
21 cvc5 can be built on Linux and macOS. Cross-compilation is possible for Arm64
22 systems and Windows using Mingw-w64. We recommend a 64-bit operating system.
24 On macOS, we recommend using Homebrew (https://brew.sh/) to install the
25 dependencies. We also have a Homebrew Tap available at
26 https://github.com/CVC4/homebrew-cvc4 .
27 To build a static binary for macOS, use:
28 `./configure.sh --static --no-static-binary`.
30 ### Cross-compiling for Windows
32 Cross-compiling cvc5 with Mingw-w64 can be done as follows:
35 ./configure.sh --win64 --static <configure options...>
37 cd <build_dir> # default is ./build
38 make # use -jN for parallel build with N threads
41 The built binary `cvc5.exe` is located in `<build_dir>/bin` and the cvc5 library
42 can be found in `<build_dir>/lib`.
46 cvc5 makes uses of a number of tools and libraries. Some of these are required
47 while others are only used with certain configuration options. If
48 `--auto-download` is given, cvc5 can automatically download and build most
49 libraries that are not already installed on your system. Versions given are
50 minimum versions; more recent versions should be compatible.
52 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
53 or [Clang](https://clang.llvm.org) (reasonably recent versions)
54 - [CMake >= 3.9](https://cmake.org)
55 - [Python 3.x](https://www.python.org)
56 + module [toml](https://pypi.org/project/toml/)
57 - [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
58 - [ANTLR 3.4](http://www.antlr3.org/)
59 - [Java >= 1.6](https://www.java.com)
60 - [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
63 ### ANTLR 3.4 parser generator
65 For most systems, the package manager no longer contains pre-packaged versions
66 of ANTLR 3.4. With `--auto-download`, cvc5 will automatically download and build
70 ### GMP (GNU Multi-Precision arithmetic library)
72 GMP is usually available on you distribution and should be used from there. It
73 can be downloaded and built automatically. If it does not, or you want to
74 cross-compile, or you want to build cvc5 statically but the distribution does
75 not ship static libraries, cvc5 builds GMP automatically when `--auto-download`
78 ### SymFPU (Support for the Theory of Floating Point Numbers)
80 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
81 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
82 of bit-vector operations.
83 It is required for supporting the theory of floating-point numbers and
84 can be downloaded and built automatically.
86 ## Optional Dependencies
88 ### CaDiCaL (Optional SAT solver)
90 [CaDiCaL](https://github.com/arminbiere/cadical)
91 is a SAT solver that can be used for solving non-incremental bit-vector
92 problems with eager bit-blasting. This dependency may improve performance.
93 It can be downloaded and built automatically.
94 Configure cvc5 with `configure.sh --cadical` to build with this dependency.
96 ### CryptoMiniSat (Optional SAT solver)
98 [CryptoMinisat](https://github.com/msoos/cryptominisat)
99 is a SAT solver that can be used for solving bit-vector problems with eager
100 bit-blasting. This dependency may improve performance.
101 It can be downloaded and built automatically.
102 Configure cvc5 with `configure.sh --cryptominisat` to build with this
105 ### Kissat (Optional SAT solver)
107 [Kissat](https://github.com/arminbiere/kissat)
108 is a SAT solver that can be used for solving bit-vector problems with eager
109 bit-blasting. This dependency may improve performance.
110 It can be downloaded and built automatically.
111 Configure cvc5 with `configure.sh --kissat` to build with this
114 ### LibPoly (Optional polynomial library)
116 [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based
117 nonlinear reasoning. It can be downloaded and built automatically. Configure
118 cvc5 with `configure.sh --poly` to build with this dependency.
120 ### CLN >= v1.3 (Class Library for Numbers)
122 [CLN](http://www.ginac.de/CLN)
123 is an alternative multiprecision arithmetic package that may offer better
124 performance and memory footprint than GMP.
125 Configure cvc5 with `configure.sh --cln` to build with this dependency.
127 Note that CLN is covered by the [GNU General Public License, version
128 3](https://www.gnu.org/licenses/gpl-3.0.en.html). If you choose to use cvc5 with
129 CLN support, you are licensing cvc5 under that same license. (Usually cvc5's
130 license is more permissive than GPL, see the file `COPYING` in the cvc5 source
131 distribution for details.)
133 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
135 [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
136 [GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
137 This can be used to speed up certain classes of problems for the arithmetic
138 implementation in cvc5. (This is not recommended for most users.)
140 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
141 Note that the only installation option is manual installation via this script.
142 cvc5 is no longer compatible with the main GLPK library.
143 Configure cvc5 with `configure.sh --glpk` to build with this dependency.
145 Note that GLPK and glpk-cut-log are covered by the [GNU General Public License,
146 version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). If you choose to use
147 cvc5 with GLPK support, you are licensing cvc5 under that same license. (Usually
148 cvc5's license is more permissive; see above discussion.)
150 ### ABC library (Improved Bit-Vector Support)
152 [ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
153 Synthesis and Verification) is a library for synthesis and verification of
154 logic circuits. This dependency may improve performance of the eager
155 bit-vector solver. When enabled, the bit-blasted formula is encoded into
156 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
158 ABC can be installed using the `contrib/get-abc` script.
159 Configure cvc5 with `configure.sh --abc` to build with this dependency.
161 ### Editline library (Improved Interactive Experience)
163 The [Editline Library](https://thrysoee.dk/editline/) library is optionally
164 used to provide command editing, tab completion, and history functionality at
165 the cvc5 prompt (when running in interactive mode). Check your distribution
166 for a package named "libedit-dev" or "libedit-devel" or similar.
168 ### Google Test Unit Testing Framework (Unit Tests)
170 [Google Test](https://github.com/google/googletest) is required to optionally
171 run cvc5's unit tests (included with the distribution).
172 See [Testing cvc5](#Testing-cvc5) below for more details.
176 cvc5 provides a complete and flexible C++ API (see `examples/api` for
177 examples). It further provides Java (see `examples/SimpleVC.java` and
178 `examples/api/java`) and Python (see `examples/api/python`) API bindings.
180 Configure cvc5 with `configure.sh --<lang>-bindings` to build with language
181 bindings for `<lang>`.
183 ### Dependencies for Language Bindings
186 * [Cython](https://cython.org/)
187 * [scikit-build](https://pypi.org/project/scikit-build/)
188 * [pytest](https://docs.pytest.org/en/6.2.x/)
190 If you're interested in helping to develop, maintain, and test a language
191 binding, please contact one of the project leaders.
194 ## Building the API Documentation
196 Building the API documentation of cvc5 requires the following dependencies:
197 * [Doxygen](https://www.doxygen.nl)
198 * [Sphinx](https://www.sphinx-doc.org),
199 [sphinx-tabs](https://sphinx-tabs.readthedocs.io/),
200 [sphinxcontrib-bibtex](https://sphinxcontrib-bibtex.readthedocs.io)
201 * [Breathe](https://breathe.readthedocs.io)
203 To build the documentation, configure cvc5 with `./configure.sh --docs`.
204 Building cvc5 will then include building the API documentation.
206 The API documentation can then be found at `<build_dir>/docs/sphinx/index.html`.
208 To only build the documentation, change to the build directory and call
211 To build the documentation for GitHub pages, change to the build directory
212 and call `make docs-gh`. The content of directory `<build_dir>/docs/sphinx-gh`
213 can then be copied over to GitHub pages.
216 ## Building the Examples
218 See `examples/README.md` for instructions on how to build and run the examples.
222 We use `ctest` as test infrastructure, for all command-line options of ctest,
223 see `ctest -h`. Some useful options are:
225 ctest -R <regex> # run all tests with names matching <regex>
226 ctest -E <regex> # exclude tests with names matching <regex>
227 ctest -L <regex> # run all tests with labels matching <regex>
228 ctest -LE <regex> # exclude tests with labels matching <regex>
229 ctest # run all tests
230 ctest -jN # run all tests in parallel with N threads
231 ctest --output-on-failure # run all tests and print output of failed tests
233 We have 4 categories of tests:
234 - **examples** in directory `examples`
236 - **regression tests** (5 levels) in directory `test/regress`
237 (label: **regressN** with N the regression level)
238 - **api tests** in directory `test/api`
240 - **unit tests** in directory `test/unit`
243 ### Testing System Tests
245 The system tests are not built by default.
247 make apitests # build and run all system tests
248 make <api_test> # build test/system/<system_test>.<ext>
249 ctest api/<api_test> # run test/system/<system_test>.<ext>
251 All system test binaries are built into `<build_dir>/bin/test/system`.
253 We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
256 make ouroborous # build test/api/ouroborous.cpp
257 ctest -R ouroborous # run all tests that match '*ouroborous*'
258 # > runs api/ouroborous
259 ctest -R ouroborous$ # run all tests that match '*ouroborous'
260 # > runs api/ouroborous
261 ctest -R api/ouroborous$ # run all tests that match '*api/ouroborous'
262 # > runs api/ouroborous
263 ### Testing Unit Tests
265 The unit tests are not built by default.
267 Note that cvc5 can only be configured with unit tests in non-static builds with
270 make units # build and run all unit tests
271 make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext>
272 ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext>
274 All unit test binaries are built into `<build_dir>/bin/test/unit`.
276 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
277 `test/unit/<subdir>`) as test target name.
279 make map_util_black # build test/unit/base/map_util_black.cpp
280 ctest -R map_util_black # run all tests that match '*map_util_black*'
281 # > runs unit/base/map_util_black
282 ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black'
283 # > runs unit/base/map_util_black
284 ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black'
285 # > runs unit/base/map_util_black
287 ### Testing Regression Tests
289 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
290 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
292 ctest -L regress # run all regression tests
293 ctest -L regress0 # run all regression tests in level 0
294 ctest -L regress[0-1] # run all regression tests in level 0 and 1
295 ctest -R regress # run all regression tests
296 ctest -R regress0 # run all regression tests in level 0
297 ctest -R regress[0-1] # run all regression tests in level 0 and 1
298 ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*'
299 # > runs regress0/bug288b
302 All custom test targets build and run a preconfigured set of tests.
304 - `make check [-jN] [ARGS=-jN]`
305 The default build-and-test target for cvc5, builds and runs all examples,
306 all system and unit tests, and regression tests from levels 0 to 2.
308 - `make systemtests [-jN] [ARGS=-jN]`
309 Build and run all system tests.
311 - `make units [-jN] [ARGS=-jN]`
312 Build and run all unit tests.
314 - `make regress [-jN] [ARGS=-jN]`
315 Build and run regression tests from levels 0 to 2.
317 - `make runexamples [-jN] [ARGS=-jN]`
318 Build and run all examples.
320 - `make coverage [-jN] [ARGS=-jN]`
321 Build and run all tests (system and unit tests, regression tests level 0-4)
322 with gcov to determine code coverage.
324 We use `ctest` as test infrastructure, and by default all test targets
325 are configured to **run** in parallel with the maximum number of threads
326 available on the system. Override with `ARGS=-jN`.
328 Use `-jN` for parallel **building** with `N` threads.
331 ## Recompiling a specific cvc5 version with different LGPL library versions
333 To recompile a specific static binary of cvc5 with different versions of the
334 linked LGPL libraries perform the following steps:
336 1. Make sure that you have installed the desired LGPL library versions.
337 You can check the versions found by cvc5's build system during the configure
340 2. Determine the commit sha and configuration of the cvc5 binary
344 3. Download the specific source code version:
346 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
348 4. Extract the source code
350 tar xf <commit-sha>.tar.gz
352 5. Change into source code directory
356 6. Configure cvc5 with options listed by `cvc5 --show-config`
358 ./configure.sh --static <options>
361 7. Follow remaining steps from [build instructions](#building-cvc5)