INSTALL.md

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