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