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)
62 ### ANTLR 3.4 parser generator
64 For most systems, the package manager no longer contains pre-packaged versions
65 of ANTLR 3.4. With `--auto-download`, cvc5 will automatically download and build
69 ### GMP (GNU Multi-Precision arithmetic library)
71 GMP is usually available on you distribution and should be used from there. It
72 can be downloaded and built automatically. If it does not, or you want to
73 cross-compile, or you want to build cvc5 statically but the distribution does
74 not ship static libraries, cvc5 builds GMP automatically when `--auto-download`
77 ## Optional Dependencies
79 ### SymFPU (Support for the Theory of Floating Point Numbers)
81 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
82 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
83 of bit-vector operations.
84 It is required for supporting the theory of floating-point numbers and
85 can be downloaded and built automatically.
86 Configure cvc5 with `configure.sh --symfpu` to build with this dependency.
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 If you're interested in helping to develop, maintain, and test a language
184 binding, please contact one of the project leaders.
187 ## Building the API Documentation
189 Building the API documentation of cvc5 requires the following dependencies:
190 * [Doxygen](https://www.doxygen.nl)
191 * [Sphinx](https://www.sphinx-doc.org),
192 [sphinx-tabs](https://sphinx-tabs.readthedocs.io/),
193 [sphinxcontrib-bibtex](https://sphinxcontrib-bibtex.readthedocs.io)
194 * [Breathe](https://breathe.readthedocs.io)
196 To build the documentation, configure cvc5 with `./configure.sh --docs`.
197 Building cvc5 will then include building the API documentation.
199 The API documentation can then be found at `<build_dir>/docs/sphinx/index.html`.
201 To only build the documentation, change to the build directory and call
204 To build the documentation for GitHub pages, change to the build directory
205 and call `make docs-gh`. The content of directory `<build_dir>/docs/sphinx-gh`
206 can then be copied over to GitHub pages.
209 ## Building the Examples
211 See `examples/README.md` for instructions on how to build and run the examples.
215 We use `ctest` as test infrastructure, for all command-line options of ctest,
216 see `ctest -h`. Some useful options are:
218 ctest -R <regex> # run all tests with names matching <regex>
219 ctest -E <regex> # exclude tests with names matching <regex>
220 ctest -L <regex> # run all tests with labels matching <regex>
221 ctest -LE <regex> # exclude tests with labels matching <regex>
222 ctest # run all tests
223 ctest -jN # run all tests in parallel with N threads
224 ctest --output-on-failure # run all tests and print output of failed tests
226 We have 4 categories of tests:
227 - **examples** in directory `examples`
229 - **regression tests** (5 levels) in directory `test/regress`
230 (label: **regressN** with N the regression level)
231 - **api tests** in directory `test/api`
233 - **unit tests** in directory `test/unit`
236 ### Testing System Tests
238 The system tests are not built by default.
240 make apitests # build and run all system tests
241 make <api_test> # build test/system/<system_test>.<ext>
242 ctest api/<api_test> # run test/system/<system_test>.<ext>
244 All system test binaries are built into `<build_dir>/bin/test/system`.
246 We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
249 make ouroborous # build test/api/ouroborous.cpp
250 ctest -R ouroborous # run all tests that match '*ouroborous*'
251 # > runs api/ouroborous
252 ctest -R ouroborous$ # run all tests that match '*ouroborous'
253 # > runs api/ouroborous
254 ctest -R api/ouroborous$ # run all tests that match '*api/ouroborous'
255 # > runs api/ouroborous
256 ### Testing Unit Tests
258 The unit tests are not built by default.
260 Note that cvc5 can only be configured with unit tests in non-static builds with
263 make units # build and run all unit tests
264 make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext>
265 ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext>
267 All unit test binaries are built into `<build_dir>/bin/test/unit`.
269 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
270 `test/unit/<subdir>`) as test target name.
272 make map_util_black # build test/unit/base/map_util_black.cpp
273 ctest -R map_util_black # run all tests that match '*map_util_black*'
274 # > runs unit/base/map_util_black
275 ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black'
276 # > runs unit/base/map_util_black
277 ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black'
278 # > runs unit/base/map_util_black
280 ### Testing Regression Tests
282 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
283 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
285 ctest -L regress # run all regression tests
286 ctest -L regress0 # run all regression tests in level 0
287 ctest -L regress[0-1] # run all regression tests in level 0 and 1
288 ctest -R regress # run all regression tests
289 ctest -R regress0 # run all regression tests in level 0
290 ctest -R regress[0-1] # run all regression tests in level 0 and 1
291 ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*'
292 # > runs regress0/bug288b
295 All custom test targets build and run a preconfigured set of tests.
297 - `make check [-jN] [ARGS=-jN]`
298 The default build-and-test target for cvc5, builds and runs all examples,
299 all system and unit tests, and regression tests from levels 0 to 2.
301 - `make systemtests [-jN] [ARGS=-jN]`
302 Build and run all system tests.
304 - `make units [-jN] [ARGS=-jN]`
305 Build and run all unit tests.
307 - `make regress [-jN] [ARGS=-jN]`
308 Build and run regression tests from levels 0 to 2.
310 - `make runexamples [-jN] [ARGS=-jN]`
311 Build and run all examples.
313 - `make coverage [-jN] [ARGS=-jN]`
314 Build and run all tests (system and unit tests, regression tests level 0-4)
315 with gcov to determine code coverage.
317 We use `ctest` as test infrastructure, and by default all test targets
318 are configured to **run** in parallel with the maximum number of threads
319 available on the system. Override with `ARGS=-jN`.
321 Use `-jN` for parallel **building** with `N` threads.
324 ## Recompiling a specific cvc5 version with different LGPL library versions
326 To recompile a specific static binary of cvc5 with different versions of the
327 linked LGPL libraries perform the following steps:
329 1. Make sure that you have installed the desired LGPL library versions.
330 You can check the versions found by cvc5's build system during the configure
333 2. Determine the commit sha and configuration of the cvc5 binary
337 3. Download the specific source code version:
339 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
341 4. Extract the source code
343 tar xf <commit-sha>.tar.gz
345 5. Change into source code directory
349 6. Configure cvc5 with options listed by `cvc5 --show-config`
351 ./configure.sh --static <options>
354 7. Follow remaining steps from [build instructions](#building-cvc5)