INSTALL.md

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