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 To build a static binary for macOS, use:
  26 `./configure.sh --static --no-static-binary`.
  27
  28 ### Cross-compiling for Windows
  29
  30 Cross-compiling CVC4 with Mingw-w64 can be done as follows:
  31
  32 ```
  33   ./configure.sh --win64 --static <configure options...>
  34
  35   cd <build_dir>   # default is ./build
  36   make             # use -jN for parallel build with N threads
  37 ```
  38
  39 The built binary `cvc4.exe` is located in `<build_dir>/bin` and the CVC4 library
  40 can be found in `<build_dir>/lib`.
  41
  42 ## Build dependencies
  43
  44 The following tools and libraries are required to build and run CVC4.
  45 Versions given are minimum versions; more recent versions should be
  46 compatible.
  47
  48 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
  49   or [Clang](https://clang.llvm.org) (reasonably recent versions)
  50 - [CMake >= 3.9](https://cmake.org)
  51 - [GNU Bash](https://www.gnu.org/software/bash/)
  52 - [Python 3.x](https://www.python.org)
  53   + module [toml](https://pypi.org/project/toml/)
  54 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
  55 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
  56 - [Java >= 1.6](https://www.java.com)
  57
  58 Some features, such as the theory of floating-point numbers, require
  59 [optional dependencies](optional-dependencies) (see below).
  60
  61 ### Installing libantlr3c: ANTLR parser generator C support library
  62
  63 For libantlr3c, you can use the script `contrib/get-antlr-3.4`.
  64 This will download, patch, and install libantlr3c.
  65
  66 If you're on a 32-bit machine, or if you have difficulty building
  67 libantlr3c (or difficulty getting CVC4 to link against it), you
  68 may need to remove the configure option `--enable-64bit` in the script.
  69
  70 ### Warning: GCC 4.5.1
  71
  72 GCC version 4.5.1 seems to have a bug in the optimizer that may result in
  73 incorrect behavior (and wrong results) in many builds. This is a known problem
  74 for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4.
  75 We recommend using a GCC version > 4.5.1.
  76
  77 ### Warning: Installing GMP via `contrib/get-gmp-dev`
  78
  79 Do **not** install GMP via the provided script `contrib/get-gmp-dev` unless
  80 your distribution
  81 * does not ship with the GMP configuration you need, e.g.,
  82   `contrib/get-gmp-dev` is used in `configure.sh` when cross-compiling GMP for
  83   Windows.
  84 * does not ship with static GMP libraries (e.g., Arch Linux)
  85   and you want to build CVC4 statically.
  86
  87 In most of the cases the GMP version installed on your system is the one you
  88 want and should use.
  89
  90 ## Optional Dependencies
  91
  92 ### SymFPU (Support for the Theory of Floating Point Numbers)
  93
  94 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
  95 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
  96 of bit-vector operations.
  97 It is required for supporting the theory of floating-point numbers and
  98 can be installed using the `contrib/get-symfpu` script.
  99 Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
 100
 101 ### CaDiCaL (Optional SAT solver)
 102
 103 [CaDiCaL](https://github.com/arminbiere/cadical)
 104 is a SAT solver that can be used for solving non-incremental bit-vector
 105 problems with eager bit-blasting. This dependency may improve performance.
 106 It can be installed using the `contrib/get-cadical script`.
 107 Configure CVC4 with `configure.sh --cadical` to build with this dependency.
 108
 109 ### CryptoMiniSat (Optional SAT solver)
 110
 111 [CryptoMinisat](https://github.com/msoos/cryptominisat)
 112 is a SAT solver that can be used for solving bit-vector problems with eager
 113 bit-blasting. This dependency may improve performance.
 114 It can be installed using the `contrib/get-cryptominisat` script.
 115 Configure CVC4 with `configure.sh --cryptominisat` to build with this
 116 dependency.
 117
 118 ### Kissat (Optional SAT solver)
 119
 120 [Kissat](https://github.com/arminbiere/kissat)
 121 is a SAT solver that can be used for solving bit-vector problems with eager
 122 bit-blasting. This dependency may improve performance.
 123 It can be installed using the `contrib/get-kissat` script.
 124 Configure CVC4 with `configure.sh --kissat` to build with this
 125 dependency.
 126
 127 ### LibPoly (Optional polynomial library)
 128
 129 [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning.
 130 It can be installed using the `contrib/get-poly` script.
 131 Configure CVC4 with `configure.sh --poly` to build with this dependency.
 132
 133 ### CLN >= v1.3 (Class Library for Numbers)
 134
 135 [CLN](http://www.ginac.de/CLN)
 136 is an alternative multiprecision arithmetic package that may offer better
 137 performance and memory footprint than GMP.
 138 Configure CVC4 with `configure.sh --cln` to build with this dependency.
 139
 140 Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
 141 If you choose to use CVC4 with CLN support, you are licensing CVC4 under that
 142 same license.
 143 (Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
 144 the CVC4 source distribution for details.)
 145
 146 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
 147
 148 [glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
 149 [GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
 150 This can be used to speed up certain classes of problems for the arithmetic
 151 implementation in CVC4. (This is not recommended for most users.)
 152
 153 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
 154 Note that the only installation option is manual installation via this script.
 155 CVC4 is no longer compatible with the main GLPK library.
 156 Configure CVC4 with `configure.sh --glpk` to build with this dependency.
 157
 158 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).
 159 If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that
 160 same license.
 161 (Usually CVC4's license is more permissive; see above discussion.)
 162
 163 ### ABC library (Improved Bit-Vector Support)
 164
 165 [ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
 166 Synthesis and Verification) is a library for synthesis and verification of
 167 logic circuits. This dependency may improve performance of the eager
 168 bit-vector solver. When enabled, the bit-blasted formula is encoded into
 169 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
 170
 171 ABC can be installed using the `contrib/get-abc` script.
 172 Configure CVC4 with `configure.sh --abc` to build with this dependency.
 173
 174 ### Editline library (Improved Interactive Experience)
 175
 176 The [Editline Library](https://thrysoee.dk/editline/) library is optionally
 177 used to provide command editing, tab completion, and history functionality at
 178 the CVC4 prompt (when running in interactive mode).  Check your distribution
 179 for a package named "libedit-dev" or "libedit-devel" or similar.
 180
 181 ### Boost C++ base libraries (Examples)
 182
 183 The [Boost](http://www.boost.org) C++ base library is needed for some examples
 184 provided with CVC4.
 185
 186 ### Google Test Unit Testing Framework (Unit Tests)
 187
 188 [Google Test](https://github.com/google/googletest) is required to optionally
 189 run CVC4's unit tests (included with the distribution).
 190 See [Testing CVC4](#Testing-CVC4) below for more details.
 191
 192 ## Language bindings
 193
 194 CVC4 provides a complete and flexible C++ API (see `examples/api` for
 195 examples). It further provides Java (see `examples/SimpleVC.java` and
 196 `examples/api/java`) and Python (see `examples/api/python`) API bindings.
 197
 198 Configure CVC4 with `configure.sh --<lang>-bindings` to build with language
 199 bindings for `<lang>`.
 200
 201 If you're interested in helping to develop, maintain, and test a language
 202 binding, please contact one of the project leaders.
 203
 204 ## Building the Examples
 205
 206 See `examples/README.md` for instructions on how to build and run the examples.
 207
 208 ## Testing CVC4
 209
 210 We use `ctest` as test infrastructure, for all command-line options of ctest,
 211 see `ctest -h`. Some useful options are:
 212
 213     ctest -R <regex>           # run all tests with names matching <regex>
 214     ctest -E <regex>           # exclude tests with names matching <regex>
 215     ctest -L <regex>           # run all tests with labels matching <regex>
 216     ctest -LE <regex>          # exclude tests with labels matching <regex>
 217     ctest                      # run all tests
 218     ctest -jN                  # run all tests in parallel with N threads
 219     ctest --output-on-failure  # run all tests and print output of failed tests
 220
 221 We have 4 categories of tests:
 222 - **examples** in directory `examples`
 223   (label: **example**)
 224 - **regression tests** (5 levels) in directory `test/regress`
 225   (label: **regressN** with N the regression level)
 226 - **api tests** in directory `test/api`
 227   (label: **api**)
 228 - **unit tests** in directory `test/unit`
 229   (label: **unit**)
 230
 231 ### Testing System Tests
 232
 233 The system tests are not built by default.
 234
 235     make apitests                         # build and run all system tests
 236     make <api_test>                       # build test/system/<system_test>.<ext>
 237     ctest api/<api_test>                  # run test/system/<system_test>.<ext>
 238
 239 All system test binaries are built into `<build_dir>/bin/test/system`.
 240
 241 We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
 242 as test target name.
 243
 244     make ouroborous                       # build test/api/ouroborous.cpp
 245     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
 246                                           # > runs api/ouroborous
 247     ctest -R ouroborous$                  # run all tests that match '*ouroborous'
 248                                           # > runs api/ouroborous
 249     ctest -R api/ouroborous$              # run all tests that match '*api/ouroborous'
 250                                           # > runs api/ouroborous
 251 ### Testing Unit Tests
 252
 253 The unit tests are not built by default.
 254
 255 Note that CVC4 can only be configured with unit tests in non-static builds with
 256 assertions enabled.
 257
 258     make units                            # build and run all unit tests
 259     make <unit_test>                      # build test/unit/<subdir>/<unit_test>.<ext>
 260     ctest unit/<subdir>/<unit_test>       # run test/unit/<subdir>/<unit_test>.<ext>
 261
 262 All unit test binaries are built into `<build_dir>/bin/test/unit`.
 263
 264 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
 265 `test/unit/<subdir>`) as test target name.
 266
 267     make map_util_black                   # build test/unit/base/map_util_black.cpp
 268     ctest -R map_util_black               # run all tests that match '*map_util_black*'
 269                                           # > runs unit/base/map_util_black
 270     ctest -R base/map_util_black$         # run all tests that match '*base/map_util_black'
 271                                           # > runs unit/base/map_util_black
 272     ctest -R unit/base/map_util_black$    # run all tests that match '*unit/base/map_util_black'
 273                                           # > runs unit/base/map_util_black
 274
 275 ### Testing Regression Tests
 276
 277 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
 278 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 279
 280     ctest -L regress                      # run all regression tests
 281     ctest -L regress0                     # run all regression tests in level 0
 282     ctest -L regress[0-1]                 # run all regression tests in level 0 and 1
 283     ctest -R regress                      # run all regression tests
 284     ctest -R regress0                     # run all regression tests in level 0
 285     ctest -R regress[0-1]                 # run all regression tests in level 0 and 1
 286     ctest -R regress0/bug288b             # run all tests that match '*regress0/bug288b*'
 287                                           # > runs regress0/bug288b
 288 ### Custom Targets
 289
 290 All custom test targets build and run a preconfigured set of tests.
 291
 292 - `make check [-jN] [ARGS=-jN]`
 293   The default build-and-test target for CVC4, builds and runs all examples,
 294   all system and unit tests, and regression tests from levels 0 to 2.
 295
 296 - `make systemtests [-jN] [ARGS=-jN]`
 297   Build and run all system tests.
 298
 299 - `make units [-jN] [ARGS=-jN]`
 300   Build and run all unit tests.
 301
 302 - `make regress [-jN] [ARGS=-jN]`
 303   Build and run regression tests from levels 0 to 2.
 304
 305 - `make runexamples [-jN] [ARGS=-jN]`
 306   Build and run all examples.
 307
 308 - `make coverage [-jN] [ARGS=-jN]`
 309   Build and run all tests (system and unit tests, regression tests level 0-4)
 310   with gcov to determine code coverage.
 311
 312 We use `ctest` as test infrastructure, and by default all test targets
 313 are configured to **run** in parallel with the maximum number of threads
 314 available on the system. Override with `ARGS=-jN`.
 315
 316 Use `-jN` for parallel **building** with `N` threads.
 317
 318
 319 ## Recompiling a specific CVC4 version with different LGPL library versions
 320
 321 To recompile a specific static binary of CVC4 with different versions of the
 322 linked LGPL libraries perform the following steps:
 323
 324 1. Make sure that you have installed the desired LGPL library versions.
 325    You can check the versions found by CVC4's build system during the configure
 326    phase.
 327
 328 2. Determine the commit sha and configuration of the CVC4 binary
 329 ```
 330 cvc4 --show-config
 331 ```
 332 3. Download the specific source code version:
 333 ```
 334 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
 335 ```
 336 4. Extract the source code
 337 ```
 338 tar xf <commit-sha>.tar.gz
 339 ```
 340 5. Change into source code directory
 341 ```
 342 cd CVC4-<commit-sha>
 343 ```
 344 6. Configure CVC4 with options listed by `cvc4 --show-config`
 345 ```
 346 ./configure.sh --static <options>
 347 ```
 348
 349 7. Follow remaining steps from [build instructions](#building-cvc4)