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