1 CVC4 prerelease version 1.7.
2 ============================
4 ## Supported Operating Systems
6 CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled
7 using Mingw-w64. We recommend a 64-bit operating system.
9 On macOS, we recommend using Homebrew (https://brew.sh/) to install the
10 dependencies. We also have a Homebrew Tap available at
11 https://github.com/CVC4/homebrew-cvc4 .
15 The following tools and libraries are required to build and run CVC4.
16 Versions given are minimum versions; more recent versions should be
19 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
20 or [Clang](https://clang.llvm.org) (reasonably recent versions)
21 - [CMake >= 3.1](https://cmake.org)
22 - [GNU Bash](https://www.gnu.org/software/bash/)
23 - [Python >= 2.7](https://www.python.org)
24 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
25 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
27 Some features, such as the theory of floating-point numbers, require
28 [optional dependencies](optional-dependencies) (see below).
30 ### Installing libantlr3c: ANTLR parser generator C support library
32 For libantlr3c, you can use the script contrib/get-antlr-3.4.
33 This will download, patch, and install libantlr3c.
35 If you're on a 32-bit machine, or if you have difficulty building
36 libantlr3c (or difficulty getting CVC4 to link against it), you
37 may need to remove the configure option `--enable-64bit` in the script.
39 ### Warning: GCC 4.5.1
41 GCC version 4.5.1 seems to have a bug in the optimizer that may result in
42 incorrect behavior (and wrong results) in many builds. This is a known problem
43 for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4.
44 We recommend using a GCC version > 4.5.1.
46 ## Optional Dependencies
48 ### SymFPU (Support for the Theory of Floating Point Numbers)
50 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
51 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
52 of bit-vector operations.
53 It is required for supporting the theory of floating-point numbers and
54 can be installed using the `contrib/get-symfpu` script.
55 Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
57 ### CaDiCaL (Optional SAT solver)
59 [CaDiCaL](https://github.com/arminbiere/cadical)
60 is a SAT solver that can be used for solving non-incremental bit-vector
61 problems with eager bit-blasting. This dependency may improve performance.
62 It can be installed using the `contrib/get-cadical script`.
63 Configure CVC4 with `configure.sh --cadical` to build with this dependency.
65 ### CryptoMiniSat (Optional SAT solver)
67 [CryptoMinisat](https://github.com/msoos/cryptominisat)
68 is a SAT solver that can be used for solving bit-vector problems with eager
69 bit-blasting. This dependency may improve performance.
70 It can be installed using the `contrib/get-cryptominisat` script.
71 Configure CVC4 with `configure.sh --cryptominisat` to build with this
74 ### LFSC (The LFSC Proof Checker)
76 [LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally
77 with --check-proofs. It can be installed using the `contrib/get-lfsc` script.
78 Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
80 ### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator)
82 SWIG 3.0.x (and a JDK) is necessary to build the Java API.
83 See [Language Bindings](language-bindings) below for build instructions.
85 ### CLN >= v1.3 (Class Library for Numbers)
87 [CLN](http://www.ginac.de/CLN)
88 is an alternative multiprecision arithmetic package that may offer better
89 performance and memory footprint than GMP.
90 Configure CVC4 with `configure.sh --cln` to build with this dependency.
92 Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
93 If you choose to use CVC4 with CLN support, you are licensing CVC4 under that
95 (Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
96 the CVC4 source distribution for details.)
98 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
100 [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
101 [GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
102 This can be used to speed up certain classes of problems for the arithmetic
103 implementation in CVC4. (This is not recommended for most users.)
105 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
106 Note that the only installation option is manual installation via this script.
107 CVC4 is no longer compatible with the main GLPK library.
108 Configure CVC4 with `configure.sh --glpk` to build with this dependency.
110 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).
111 If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that
113 (Usually CVC4's license is more permissive; see above discussion.)
115 ### ABC library (Improved Bit-Vector Support)
117 [ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
118 Synthesis and Verification) is a library for synthesis and verification of
119 logic circuits. This dependency may improve performance of the eager
120 bit-vector solver. When enabled, the bit-blasted formula is encoded into
121 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
123 ABC can be installed using the `contrib/get-abc` script.
124 Configure CVC4 with `configure.sh --abc` to build with this dependency.
126 ### GNU Readline library (Improved Interactive Experience)
128 The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html)
129 library is optionally used to provide command editing, tab completion, and
130 history functionality at the CVC4 prompt (when running in interactive mode).
131 Check your distribution for a package named "libreadline-dev" or
132 "readline-devel" or similar.
134 Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
135 If you choose to use CVC4 with GNU Readline support, you are licensing CVC4
136 under that same license.
137 (Usually CVC4's license is more permissive; see above discussion.)
139 ### libboost_thread: The Boost C++ threading library (Portfolio Builds)
141 The [Boost](http://www.boost.org) C++ threading library (often packaged
142 independently of the Boost base library) is needed to run CVC4 in "portfolio"
143 (multithreaded) mode.
144 Check your distribution for a package named "libboost-thread-dev" or similar.
146 ### Boost C++ base libraries (Examples)
148 The [Boost](http://www.boost.org) C++ base library is needed for some examples
151 ### CxxTest Unit Testing Framework (Unit Tests)
153 [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
154 (included with the distribution). See [Testing](testing) below for more details.
159 ./configure.sh # use --prefix to specify a prefix (default: /usr/local)
160 # use --name=<PATH> for custom build directory
161 cd <build_dir> # default is ./build
162 make # use -jN for parallel build with N threads
163 make check # to run default set of tests
164 make install # to install into the prefix specified above
166 All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
171 CVC4 provides a complete and flexible C++ API (see `examples/api` for examples).
172 It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`)
173 and Python (see `examples/SimpleVC.py`) API bindings.
175 Configure CVC4 with `configure.sh --language-bindings=[java,python,all]`
176 to build with language bindings.
177 Note that this requires SWIG >= 3.0.x.
179 In principle, since we use SWIG to generate the native Java and PythonAPI,
180 we could support other languages as well. However, using CVC4 from other
181 languages is not supported, nor expected to work, at this time.
182 If you're interested in helping to develop, maintain, and test a language
183 binding, please contact one of the project leaders.
185 ## Building the Examples
187 The examples provided in directory `examples` are not built by default.
189 make examples # build all examples
190 make runexamples # build and run all examples
191 make <example> # build examples/<subdir>/<example>.<ext>
192 ctest example/<subdir>/<example> # run test example/<subdir>/<example>
194 All examples binaries are built into `<build_dir>/bin/examples`.
196 See `examples/README` for more detailed information on what to find in the
197 `examples` directory.
201 We use `ctest` as test infrastructure, for all command-line options of ctest,
202 see `ctest -h`. Some useful options are:
204 ctest -R <regex> # run all tests with names matching <regex>
205 ctest -E <regex> # exclude tests with names matching <regex>
206 ctest -L <regex> # run all tests with labels matching <regex>
207 ctest -LE <regex> # exclude tests with labels matching <regex>
208 ctest # run all tests
209 ctest -jN # run all tests in parallel with N threads
210 ctest --output-on-failure # run all tests and print output of failed tests
212 We have 4 categories of tests:
213 - **examples** in directory `examples`
215 - **regression tests** (5 levels) in directory `test/regress`
216 (label: **regressN** with N the regression level)
217 - **system tests** in directory `test/system`
219 - **unit tests** in directory `test/unit`
224 For building instructions, see [Building the Examples](building-the-examples).
226 We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in
227 `example/<subdir>/`) as test target name.
229 make bitvectors # build example/api/bitvectors.cpp
230 ctest -R bitvectors # run all tests that match '*bitvectors*'
231 # > runs example/api/bitvectors
232 # > example/api/bitvectors_and_arrays
234 ctest -R bitvectors$ # run all tests that match '*bitvectors'
235 # > runs example/api/bitvectors
236 ctest -R example/api/bitvectors$ # run all tests that match '*example/api/bitvectors'
237 # > runs example/api/bitvectors
240 ### Testing System Tests
242 The system tests are not built by default.
244 make systemtests # build and run all system tests
245 make <system_test> # build test/system/<system_test>.<ext>
246 ctest system/<system_test> # run test/system/<system_test>.<ext>
248 All system test binaries are built into `<build_dir>/bin/test/system`.
250 We use prefix `system/` + `<system_test>` (for `<system_test>` in `test/system`)
253 make ouroborous # build test/system/ouroborous.cpp
254 ctest -R ouroborous # run all tests that match '*ouroborous*'
255 # > runs system/ouroborous
256 ctest -R ouroborous$ # run all tests that match '*ouroborous'
257 # > runs system/ouroborous
258 ctest -R system/ouroborous$ # run all tests that match '*system/ouroborous'
259 # > runs system/ouroborous
260 ### Testing Unit Tests
262 The unit tests are not built by default.
264 make units # build and run all unit tests
265 make <unit_test> # build test/unit/<subdir>/<unit_test>.<ext>
266 ctest unit/<subdir>/<unit_test> # run test/unit/<subdir>/<unit_test>.<ext>
268 All unit test binaries are built into `<build_dir>/bin/test/unit`.
270 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
271 `test/unit/<subdir>`) as test target name.
273 make map_util_black # build test/unit/base/map_util_black.cpp
274 ctest -R map_util_black # run all tests that match '*map_util_black*'
275 # > runs unit/base/map_util_black
276 ctest -R base/map_util_black$ # run all tests that match '*base/map_util_black'
277 # > runs unit/base/map_util_black
278 ctest -R unit/base/map_util_black$ # run all tests that match '*unit/base/map_util_black'
279 # > runs unit/base/map_util_black
281 ### Testing Regression Tests
283 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
284 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
286 ctest -L regress # run all regression tests
287 ctest -L regress0 # run all regression tests in level 0
288 ctest -L regress[0-1] # run all regression tests in level 0 and 1
289 ctest -R regress # run all regression tests
290 ctest -R regress0 # run all regression tests in level 0
291 ctest -R regress[0-1] # run all regression tests in level 0 and 1
292 ctest -R regress0/bug288b # run all tests that match '*regress0/bug288b*'
293 # > runs regress0/bug288b
296 All custom test targets build and run a preconfigured set of tests.
298 - `make check [-jN] [ARGS=-jN]`
299 The default build-and-test target for CVC4, builds and runs all examples,
300 all system and unit tests, and regression tests from levels 0 and 1.
302 - `make systemtests [-jN] [ARGS=-jN]`
303 Build and run all system tests.
305 - `make units [-jN] [ARGS=-jN]`
306 Build and run all unit tests.
308 - `make regress [-jN] [ARGS=-jN]`
309 Build and run all regression tests.
311 - `make runexamples [-jN] [ARGS=-jN]`
312 Build and run all examples.
314 - `make coverage [-jN] [ARGS=-jN]`
315 Build and run all tests (system and unit tests, regression tests level 0-4)
316 with gcov to determine code coverage.
318 We use `ctest` as test infrastructure, and by default all test targets
319 are configured to **run** in parallel with the maximum number of threads
320 available on the system. Override with `ARGS=-jN`.
322 Use `-jN` for parallel **building** with `N` threads.