INSTALL.md

   1 CVC4 prerelease version 1.9
   2 ===========================
   3
   4 ## Building CVC4
   5
   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
  13
  14 All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
  15 `<build_dir>/lib`.
  16
  17 ## Supported Operating Systems
  18
  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.
  21
  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 .
  25
  26 ### Cross-compiling for Windows
  27
  28 Cross-compiling CVC4 with Mingw-w64 can be done as follows:
  29
  30 ```
  31   HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies
  32   ./configure --win64 --static <configure options...>
  33
  34   cd <build_dir>   # default is ./build
  35   make             # use -jN for parallel build with N threads
  36 ```
  37
  38 The built binary `cvc4.exe` is located in `<build_dir>/bin` and the CVC4 library
  39 can be found in `<build_dir>/lib`.
  40
  41 ## Build dependencies
  42
  43 The following tools and libraries are required to build and run CVC4.
  44 Versions given are minimum versions; more recent versions should be
  45 compatible.
  46
  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)
  56
  57 Some features, such as the theory of floating-point numbers, require
  58 [optional dependencies](optional-dependencies) (see below).
  59
  60 ### Installing libantlr3c: ANTLR parser generator C support library
  61
  62 For libantlr3c, you can use the script `contrib/get-antlr-3.4`.
  63 This will download, patch, and install libantlr3c.
  64
  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.
  68
  69 ### Warning: GCC 4.5.1
  70
  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.
  75
  76 ### Warning: Installing GMP via `contrib/get-gmp-dev`
  77
  78 Do **not** install GMP via the provided script `contrib/get-gmp-dev` unless
  79 your distribution
  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.
  85
  86 In most of the cases the GMP version installed on your system is the one you
  87 want and should use.
  88
  89 ## Optional Dependencies
  90
  91 ### SymFPU (Support for the Theory of Floating Point Numbers)
  92
  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.
  99
 100 ### CaDiCaL (Optional SAT solver)
 101
 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.
 107
 108 ### CryptoMiniSat (Optional SAT solver)
 109
 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
 115 dependency.
 116
 117 ### Kissat (Optional SAT solver)
 118
 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
 124 dependency.
 125
 126 ### LFSC (The LFSC Proof Checker)
 127
 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.
 131
 132 ### LibPoly (Optional polynomial library)
 133
 134 [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning.
 135 It can be installed using the `contrib/get-poly` script.
 136 Configure CVC4 with `configure.sh --poly` to build with this dependency.
 137
 138 ### CLN >= v1.3 (Class Library for Numbers)
 139
 140 [CLN](http://www.ginac.de/CLN)
 141 is an alternative multiprecision arithmetic package that may offer better
 142 performance and memory footprint than GMP.
 143 Configure CVC4 with `configure.sh --cln` to build with this dependency.
 144
 145 Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
 146 If you choose to use CVC4 with CLN support, you are licensing CVC4 under that
 147 same license.
 148 (Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
 149 the CVC4 source distribution for details.)
 150
 151 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
 152
 153 [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
 154 [GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
 155 This can be used to speed up certain classes of problems for the arithmetic
 156 implementation in CVC4. (This is not recommended for most users.)
 157
 158 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
 159 Note that the only installation option is manual installation via this script.
 160 CVC4 is no longer compatible with the main GLPK library.
 161 Configure CVC4 with `configure.sh --glpk` to build with this dependency.
 162
 163 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).
 164 If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that
 165 same license.
 166 (Usually CVC4's license is more permissive; see above discussion.)
 167
 168 ### ABC library (Improved Bit-Vector Support)
 169
 170 [ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
 171 Synthesis and Verification) is a library for synthesis and verification of
 172 logic circuits. This dependency may improve performance of the eager
 173 bit-vector solver. When enabled, the bit-blasted formula is encoded into
 174 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
 175
 176 ABC can be installed using the `contrib/get-abc` script.
 177 Configure CVC4 with `configure.sh --abc` to build with this dependency.
 178
 179 ### Editline library (Improved Interactive Experience)
 180
 181 The [Editline Library](https://thrysoee.dk/editline/) library is optionally
 182 used to provide command editing, tab completion, and history functionality at
 183 the CVC4 prompt (when running in interactive mode).  Check your distribution
 184 for a package named "libedit-dev" or "libedit-devel" or similar.
 185
 186 ### Boost C++ base libraries (Examples)
 187
 188 The [Boost](http://www.boost.org) C++ base library is needed for some examples
 189 provided with CVC4.
 190
 191 ### CxxTest Unit Testing Framework (Unit Tests)
 192
 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.
 196
 197
 198 ## Language bindings
 199
 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.
 203
 204 Configure CVC4 with `configure.sh --<lang>-bindings` to build with language
 205 bindings for `<lang>`.
 206
 207 If you're interested in helping to develop, maintain, and test a language
 208 binding, please contact one of the project leaders.
 209
 210 ## Building the Examples
 211
 212 See `examples/README.md` for instructions on how to build and run the examples.
 213
 214 ## Testing CVC4
 215
 216 We use `ctest` as test infrastructure, for all command-line options of ctest,
 217 see `ctest -h`. Some useful options are:
 218
 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
 226
 227 We have 4 categories of tests:
 228 - **examples** in directory `examples`
 229   (label: **example**)
 230 - **regression tests** (5 levels) in directory `test/regress`
 231   (label: **regressN** with N the regression level)
 232 - **api tests** in directory `test/api`
 233   (label: **api**)
 234 - **unit tests** in directory `test/unit`
 235   (label: **unit**)
 236
 237 ### Testing System Tests
 238
 239 The system tests are not built by default.
 240
 241     make apitests                         # build and run all system tests
 242     make <api_test>                       # build test/system/<system_test>.<ext>
 243     ctest api/<api_test>                  # run test/system/<system_test>.<ext>
 244
 245 All system test binaries are built into `<build_dir>/bin/test/system`.
 246
 247 We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
 248 as test target name.
 249
 250     make ouroborous                       # build test/api/ouroborous.cpp
 251     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
 252                                           # > runs api/ouroborous
 253     ctest -R ouroborous$                  # run all tests that match '*ouroborous'
 254                                           # > runs api/ouroborous
 255     ctest -R api/ouroborous$              # run all tests that match '*api/ouroborous'
 256                                           # > runs api/ouroborous
 257 ### Testing Unit Tests
 258
 259 The unit tests are not built by default.
 260
 261 Note that CVC4 can only be configured with unit tests in non-static builds with
 262 assertions enabled.
 263
 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>
 267
 268 All unit test binaries are built into `<build_dir>/bin/test/unit`.
 269
 270 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
 271 `test/unit/<subdir>`) as test target name.
 272
 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
 280
 281 ### Testing Regression Tests
 282
 283 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
 284 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 285
 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
 294 ### Custom Targets
 295
 296 All custom test targets build and run a preconfigured set of tests.
 297
 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 to 2.
 301
 302 - `make systemtests [-jN] [ARGS=-jN]`
 303   Build and run all system tests.
 304
 305 - `make units [-jN] [ARGS=-jN]`
 306   Build and run all unit tests.
 307
 308 - `make regress [-jN] [ARGS=-jN]`
 309   Build and run regression tests from levels 0 to 2.
 310
 311 - `make runexamples [-jN] [ARGS=-jN]`
 312   Build and run all examples.
 313
 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.
 317
 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`.
 321
 322 Use `-jN` for parallel **building** with `N` threads.
 323
 324
 325 ## Recompiling a specific CVC4 version with different LGPL library versions
 326
 327 To recompile a specific static binary of CVC4 with different versions of the
 328 linked LGPL libraries perform the following steps:
 329
 330 1. Make sure that you have installed the desired LGPL library versions.
 331    You can check the versions found by CVC4's build system during the configure
 332    phase.
 333
 334 2. Determine the commit sha and configuration of the CVC4 binary
 335 ```
 336 cvc4 --show-config
 337 ```
 338 3. Download the specific source code version:
 339 ```
 340 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
 341 ```
 342 4. Extract the source code
 343 ```
 344 tar xf <commit-sha>.tar.gz
 345 ```
 346 5. Change into source code directory
 347 ```
 348 cd CVC4-<commit-sha>
 349 ```
 350 6. Configure CVC4 with options listed by `cvc4 --show-config`
 351 ```
 352 ./configure.sh --static <options>
 353 ```
 354
 355 7. Follow remaining steps from [build instructions](#building-cvc4)