1 CVC4 prerelease version 1.9
2 ===========================
6 ./contrib/get-antlr-3.4 # download and build ANTLR
7 ./configure.sh # use --prefix to specify a prefix (default: /usr/local)
8 # use --name=<PATH> for custom build directory
9 cd <build_dir> # default is ./build
10 make # use -jN for parallel build with N threads
11 make check # to run default set of tests
12 make install # to install into the prefix specified above
14 All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
17 ## Supported Operating Systems
19 CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled
20 using Mingw-w64. We recommend a 64-bit operating system.
22 On macOS, we recommend using Homebrew (https://brew.sh/) to install the
23 dependencies. We also have a Homebrew Tap available at
24 https://github.com/CVC4/homebrew-cvc4 .
26 ### Cross-compiling for Windows
28 Cross-compiling CVC4 with Mingw-w64 can be done as follows:
31 HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies
32 ./configure --win64 --static <configure options...>
34 cd <build_dir> # default is ./build
35 make # use -jN for parallel build with N threads
38 The built binary `cvc4.exe` is located in `<build_dir>/bin` and the CVC4 library
39 can be found in `<build_dir>/lib`.
43 The following tools and libraries are required to build and run CVC4.
44 Versions given are minimum versions; more recent versions should be
47 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
48 or [Clang](https://clang.llvm.org) (reasonably recent versions)
49 - [CMake >= 3.1](https://cmake.org)
50 - [GNU Bash](https://www.gnu.org/software/bash/)
51 - [Python >= 2.7](https://www.python.org)
52 + module [toml](https://pypi.org/project/toml/)
53 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
54 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
55 - [Java >= 1.6](https://www.java.com)
57 Some features, such as the theory of floating-point numbers, require
58 [optional dependencies](optional-dependencies) (see below).
60 ### Installing libantlr3c: ANTLR parser generator C support library
62 For libantlr3c, you can use the script `contrib/get-antlr-3.4`.
63 This will download, patch, and install libantlr3c.
65 If you're on a 32-bit machine, or if you have difficulty building
66 libantlr3c (or difficulty getting CVC4 to link against it), you
67 may need to remove the configure option `--enable-64bit` in the script.
69 ### Warning: GCC 4.5.1
71 GCC version 4.5.1 seems to have a bug in the optimizer that may result in
72 incorrect behavior (and wrong results) in many builds. This is a known problem
73 for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4.
74 We recommend using a GCC version > 4.5.1.
76 ### Warning: Installing GMP via `contrib/get-gmp-dev`
78 Do **not** install GMP via the provided script `contrib/get-gmp-dev` unless
80 * does not ship with the GMP configuration you need, e.g.,
81 script `contrib/get-win-dependencies` uses `contrib/get-gmp-dev` when
82 cross-compiling GMP for Windows.
83 * does not ship with static GMP libraries (e.g., Arch Linux)
84 and you want to build CVC4 statically.
86 In most of the cases the GMP version installed on your system is the one you
89 ## Optional Dependencies
91 ### SymFPU (Support for the Theory of Floating Point Numbers)
93 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
94 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
95 of bit-vector operations.
96 It is required for supporting the theory of floating-point numbers and
97 can be installed using the `contrib/get-symfpu` script.
98 Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
100 ### CaDiCaL (Optional SAT solver)
102 [CaDiCaL](https://github.com/arminbiere/cadical)
103 is a SAT solver that can be used for solving non-incremental bit-vector
104 problems with eager bit-blasting. This dependency may improve performance.
105 It can be installed using the `contrib/get-cadical script`.
106 Configure CVC4 with `configure.sh --cadical` to build with this dependency.
108 ### CryptoMiniSat (Optional SAT solver)
110 [CryptoMinisat](https://github.com/msoos/cryptominisat)
111 is a SAT solver that can be used for solving bit-vector problems with eager
112 bit-blasting. This dependency may improve performance.
113 It can be installed using the `contrib/get-cryptominisat` script.
114 Configure CVC4 with `configure.sh --cryptominisat` to build with this
117 ### Kissat (Optional SAT solver)
119 [Kissat](https://github.com/arminbiere/kissat)
120 is a SAT solver that can be used for solving bit-vector problems with eager
121 bit-blasting. This dependency may improve performance.
122 It can be installed using the `contrib/get-kissat` script.
123 Configure CVC4 with `configure.sh --kissat` to build with this
126 ### LFSC (The LFSC Proof Checker)
128 [LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally
129 with --check-proofs. It can be installed using the `contrib/get-lfsc` script.
130 Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
132 ### CLN >= v1.3 (Class Library for Numbers)
134 [CLN](http://www.ginac.de/CLN)
135 is an alternative multiprecision arithmetic package that may offer better
136 performance and memory footprint than GMP.
137 Configure CVC4 with `configure.sh --cln` to build with this dependency.
139 Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
140 If you choose to use CVC4 with CLN support, you are licensing CVC4 under that
142 (Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
143 the CVC4 source distribution for details.)
145 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
147 [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
148 [GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
149 This can be used to speed up certain classes of problems for the arithmetic
150 implementation in CVC4. (This is not recommended for most users.)
152 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
153 Note that the only installation option is manual installation via this script.
154 CVC4 is no longer compatible with the main GLPK library.
155 Configure CVC4 with `configure.sh --glpk` to build with this dependency.
157 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).
158 If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that
160 (Usually CVC4's license is more permissive; see above discussion.)
162 ### ABC library (Improved Bit-Vector Support)
164 [ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
165 Synthesis and Verification) is a library for synthesis and verification of
166 logic circuits. This dependency may improve performance of the eager
167 bit-vector solver. When enabled, the bit-blasted formula is encoded into
168 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
170 ABC can be installed using the `contrib/get-abc` script.
171 Configure CVC4 with `configure.sh --abc` to build with this dependency.
173 ### GNU Readline library (Improved Interactive Experience)
175 The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html)
176 library is optionally used to provide command editing, tab completion, and
177 history functionality at the CVC4 prompt (when running in interactive mode).
178 Check your distribution for a package named "libreadline-dev" or
179 "readline-devel" or similar.
181 Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
182 If you choose to use CVC4 with GNU Readline support, you are licensing CVC4
183 under that same license.
184 (Usually CVC4's license is more permissive; see above discussion.)
186 ### Boost C++ base libraries (Examples)
188 The [Boost](http://www.boost.org) C++ base library is needed for some examples
191 ### CxxTest Unit Testing Framework (Unit Tests)
193 [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
194 (included with the distribution).
195 See [Testing CVC4](#Testing-CVC4) below for more details.
200 CVC4 provides a complete and flexible C++ API (see `examples/api` for
201 examples). It further provides Java (see `examples/SimpleVC.java` and
202 `examples/api/java`) and Python (see `examples/api/python`) API bindings.
204 Configure CVC4 with `configure.sh --<lang>-bindings` to build with language
205 bindings for `<lang>`.
207 If you're interested in helping to develop, maintain, and test a language
208 binding, please contact one of the project leaders.
210 ## Building the Examples
212 See `examples/README.md` for instructions on how to build and run the examples.
216 We use `ctest` as test infrastructure, for all command-line options of ctest,
217 see `ctest -h`. Some useful options are:
219 ctest -R <regex> # run all tests with names matching <regex>
220 ctest -E <regex> # exclude tests with names matching <regex>
221 ctest -L <regex> # run all tests with labels matching <regex>
222 ctest -LE <regex> # exclude tests with labels matching <regex>
223 ctest # run all tests
224 ctest -jN # run all tests in parallel with N threads
225 ctest --output-on-failure # run all tests and print output of failed tests
227 We have 4 categories of tests:
228 - **examples** in directory `examples`
230 - **regression tests** (5 levels) in directory `test/regress`
231 (label: **regressN** with N the regression level)
232 - **system tests** in directory `test/system`
234 - **unit tests** in directory `test/unit`
237 ### Testing System Tests
239 The system tests are not built by default.
241 make systemtests # build and run all system tests
242 make <system_test> # build test/system/<system_test>.<ext>
243 ctest system/<system_test> # run test/system/<system_test>.<ext>
245 All system test binaries are built into `<build_dir>/bin/test/system`.
247 We use prefix `system/` + `<system_test>` (for `<system_test>` in `test/system`)
250 make ouroborous # build test/system/ouroborous.cpp
251 ctest -R ouroborous # run all tests that match '*ouroborous*'
252 # > runs system/ouroborous
253 ctest -R ouroborous$ # run all tests that match '*ouroborous'
254 # > runs system/ouroborous
255 ctest -R system/ouroborous$ # run all tests that match '*system/ouroborous'
256 # > runs system/ouroborous
257 ### Testing Unit Tests
259 The unit tests are not built by default.
261 make units # build and run all unit tests
262 make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext>
263 ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext>
265 All unit test binaries are built into `<build_dir>/bin/test/unit`.
267 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
268 `test/unit/<subdir>`) as test target name.
270 make map_util_black # build test/unit/base/map_util_black.cpp
271 ctest -R map_util_black # run all tests that match '*map_util_black*'
272 # > runs unit/base/map_util_black
273 ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black'
274 # > runs unit/base/map_util_black
275 ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black'
276 # > runs unit/base/map_util_black
278 ### Testing Regression Tests
280 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
281 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
283 ctest -L regress # run all regression tests
284 ctest -L regress0 # run all regression tests in level 0
285 ctest -L regress[0-1] # run all regression tests in level 0 and 1
286 ctest -R regress # run all regression tests
287 ctest -R regress0 # run all regression tests in level 0
288 ctest -R regress[0-1] # run all regression tests in level 0 and 1
289 ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*'
290 # > runs regress0/bug288b
293 All custom test targets build and run a preconfigured set of tests.
295 - `make check [-jN] [ARGS=-jN]`
296 The default build-and-test target for CVC4, builds and runs all examples,
297 all system and unit tests, and regression tests from levels 0 to 2.
299 - `make systemtests [-jN] [ARGS=-jN]`
300 Build and run all system tests.
302 - `make units [-jN] [ARGS=-jN]`
303 Build and run all unit tests.
305 - `make regress [-jN] [ARGS=-jN]`
306 Build and run regression tests from levels 0 to 2.
308 - `make runexamples [-jN] [ARGS=-jN]`
309 Build and run all examples.
311 - `make coverage [-jN] [ARGS=-jN]`
312 Build and run all tests (system and unit tests, regression tests level 0-4)
313 with gcov to determine code coverage.
315 We use `ctest` as test infrastructure, and by default all test targets
316 are configured to **run** in parallel with the maximum number of threads
317 available on the system. Override with `ARGS=-jN`.
319 Use `-jN` for parallel **building** with `N` threads.