INSTALL.md

   1 CVC4 prerelease version 1.7.
   2 ============================
   3
   4 ## Supported Operating Systems
   5
   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.
   8
   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 .
  12
  13 ## Build dependencies
  14
  15 The following tools and libraries are required to build and run CVC4.
  16 Versions given are minimum versions; more recent versions should be
  17 compatible.
  18
  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/)
  26
  27 Some features, such as the theory of floating-point numbers, require
  28 [optional dependencies](optional-dependencies) (see below).
  29
  30 ### Installing libantlr3c: ANTLR parser generator C support library
  31
  32 For libantlr3c, you can use the script contrib/get-antlr-3.4.
  33 This will download, patch, and install libantlr3c.
  34
  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.
  38
  39 ### Warning: GCC 4.5.1
  40
  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.
  45
  46 ## Optional Dependencies
  47
  48 ### SymFPU (Support for the Theory of Floating Point Numbers)
  49
  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.
  56
  57 ### CaDiCaL (Optional SAT solver)
  58
  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.
  64
  65 ### CryptoMiniSat (Optional SAT solver)
  66
  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
  72 dependency.
  73
  74 ### LFSC (The LFSC Proof Checker)
  75
  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.
  79
  80 ### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator)
  81
  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.
  84
  85 ### CLN >= v1.3 (Class Library for Numbers)
  86
  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.
  91
  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
  94 same license.
  95 (Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
  96 the CVC4 source distribution for details.)
  97
  98 ### glpk-cut-log (A fork of the GNU Linear Programming Kit)
  99
 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.)
 104
 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.
 109
 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
 112 same license.
 113 (Usually CVC4's license is more permissive; see above discussion.)
 114
 115 ### ABC library (Improved Bit-Vector Support)
 116
 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.
 122
 123 ABC can be installed using the `contrib/get-abc` script.
 124 Configure CVC4 with `configure.sh --abc` to build with this dependency.
 125
 126 ### GNU Readline library (Improved Interactive Experience)
 127
 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.
 133
 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.)
 138
 139 ### libboost_thread: The Boost C++ threading library (Portfolio Builds)
 140
 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.
 145
 146 ### Boost C++ base libraries (Examples)
 147
 148 The [Boost](http://www.boost.org) C++ base library is needed for some examples
 149 provided with CVC4.
 150
 151 ### CxxTest Unit Testing Framework (Unit Tests)
 152
 153 [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
 154 (included with the distribution).
 155 See [Testing CVC4](#Testing-CVC4) below for more details.
 156
 157
 158 ## Building CVC4
 159
 160     ./configure.sh   # use --prefix to specify a prefix (default: /usr/local)
 161                      # use --name=<PATH> for custom build directory
 162     cd <build_dir>   # default is ./build
 163     make             # use -jN for parallel build with N threads
 164     make check       # to run default set of tests
 165     make install     # to install into the prefix specified above
 166
 167 All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
 168 `<build_dir>/src`.
 169
 170 ## Language bindings
 171
 172 CVC4 provides a complete and flexible C++ API (see `examples/api` for examples).
 173 It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`)
 174 and Python (see `examples/SimpleVC.py`) API bindings.
 175
 176 Configure CVC4 with `configure.sh --language-bindings=[java,python,all]`
 177 to build with language bindings.
 178 Note that this requires SWIG >= 3.0.x.
 179
 180 In principle, since we use SWIG to generate the native Java and PythonAPI,
 181 we could support other languages as well. However, using CVC4 from other
 182 languages is not supported, nor expected to work, at this time.
 183 If you're interested in helping to develop, maintain, and test a language
 184 binding, please contact one of the project leaders.
 185
 186 ## Building the Examples
 187
 188 The examples provided in directory `examples` are not built by default.
 189
 190     make examples                      # build all examples
 191     make runexamples                   # build and run all examples
 192     make <example>                     # build examples/<subdir>/<example>.<ext>
 193     ctest example/<subdir>/<example>   # run test example/<subdir>/<example>
 194
 195 All examples binaries are built into `<build_dir>/bin/examples`.
 196
 197 See `examples/README` for more detailed information on what to find in the
 198 `examples` directory.
 199
 200 ## Testing CVC4
 201
 202 We use `ctest` as test infrastructure, for all command-line options of ctest,
 203 see `ctest -h`. Some useful options are:
 204
 205     ctest -R <regex>           # run all tests with names matching <regex>
 206     ctest -E <regex>           # exclude tests with names matching <regex>
 207     ctest -L <regex>           # run all tests with labels matching <regex>
 208     ctest -LE <regex>          # exclude tests with labels matching <regex>
 209     ctest                      # run all tests
 210     ctest -jN                  # run all tests in parallel with N threads
 211     ctest --output-on-failure  # run all tests and print output of failed tests
 212
 213 We have 4 categories of tests:
 214 - **examples** in directory `examples`
 215   (label: **example**)
 216 - **regression tests** (5 levels) in directory `test/regress`
 217   (label: **regressN** with N the regression level)
 218 - **system tests** in directory `test/system`
 219   (label: **system**)
 220 - **unit tests** in directory `test/unit`
 221   (label: **unit**)
 222
 223 ### Testing Examples
 224
 225 For building instructions, see [Building the Examples](building-the-examples).
 226
 227 We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in
 228 `example/<subdir>/`) as test target name.
 229
 230     make bitvectors                       # build example/api/bitvectors.cpp
 231     ctest -R bitvectors                   # run all tests that match '*bitvectors*'
 232                                           # > runs example/api/bitvectors
 233                                           # >      example/api/bitvectors_and_arrays
 234                                           # >      ...
 235     ctest -R bitvectors$                  # run all tests that match '*bitvectors'
 236                                           # > runs example/api/bitvectors
 237     ctest -R example/api/bitvectors$      # run all tests that match '*example/api/bitvectors'
 238                                           # > runs example/api/bitvectors
 239
 240
 241 ### Testing System Tests
 242
 243 The system tests are not built by default.
 244
 245     make systemtests                      # build and run all system tests
 246     make <system_test>                    # build test/system/<system_test>.<ext>
 247     ctest system/<system_test>            # run test/system/<system_test>.<ext>
 248
 249 All system test binaries are built into `<build_dir>/bin/test/system`.
 250
 251 We use prefix `system/` + `<system_test>` (for `<system_test>` in `test/system`)
 252 as test target name.
 253
 254     make ouroborous                       # build test/system/ouroborous.cpp
 255     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
 256                                           # > runs system/ouroborous
 257     ctest -R ouroborous$                  # run all tests that match '*ouroborous'
 258                                           # > runs system/ouroborous
 259     ctest -R system/ouroborous$           # run all tests that match '*system/ouroborous'
 260                                           # > runs system/ouroborous
 261 ### Testing Unit Tests
 262
 263 The unit tests are not built by default.
 264
 265     make units                            # build and run all unit tests
 266     make <unit_test>                      # build test/unit/<subdir>/<unit_test>.<ext>
 267     ctest unit/<subdir>/<unit_test>       # run test/unit/<subdir>/<unit_test>.<ext>
 268
 269 All unit test binaries are built into `<build_dir>/bin/test/unit`.
 270
 271 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
 272 `test/unit/<subdir>`) as test target name.
 273
 274     make map_util_black                   # build test/unit/base/map_util_black.cpp
 275     ctest -R map_util_black               # run all tests that match '*map_util_black*'
 276                                           # > runs unit/base/map_util_black
 277     ctest -R base/map_util_black$         # run all tests that match '*base/map_util_black'
 278                                           # > runs unit/base/map_util_black
 279     ctest -R unit/base/map_util_black$    # run all tests that match '*unit/base/map_util_black'
 280                                           # > runs unit/base/map_util_black
 281
 282 ### Testing Regression Tests
 283
 284 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
 285 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 286
 287     ctest -L regress                      # run all regression tests
 288     ctest -L regress0                     # run all regression tests in level 0
 289     ctest -L regress[0-1]                 # run all regression tests in level 0 and 1
 290     ctest -R regress                      # run all regression tests
 291     ctest -R regress0                     # run all regression tests in level 0
 292     ctest -R regress[0-1]                 # run all regression tests in level 0 and 1
 293     ctest -R regress0/bug288b             # run all tests that match '*regress0/bug288b*'
 294                                           # > runs regress0/bug288b
 295 ### Custom Targets
 296
 297 All custom test targets build and run a preconfigured set of tests.
 298
 299 - `make check [-jN] [ARGS=-jN]`
 300   The default build-and-test target for CVC4, builds and runs all examples,
 301   all system and unit tests, and regression tests from levels 0 to 2.
 302
 303 - `make systemtests [-jN] [ARGS=-jN]`
 304   Build and run all system tests.
 305
 306 - `make units [-jN] [ARGS=-jN]`
 307   Build and run all unit tests.
 308
 309 - `make regress [-jN] [ARGS=-jN]`
 310   Build and run regression tests from levels 0 to 2.
 311
 312 - `make runexamples [-jN] [ARGS=-jN]`
 313   Build and run all examples.
 314
 315 - `make coverage [-jN] [ARGS=-jN]`
 316   Build and run all tests (system and unit tests, regression tests level 0-4)
 317   with gcov to determine code coverage.
 318
 319 We use `ctest` as test infrastructure, and by default all test targets
 320 are configured to **run** in parallel with the maximum number of threads
 321 available on the system. Override with `ARGS=-jN`.
 322
 323 Use `-jN` for parallel **building** with `N` threads.
 324
 325
 326