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