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 - [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
  61
  62
  63 ### ANTLR 3.4 parser generator
  64
  65 For most systems, the package manager no longer contains pre-packaged versions
  66 of ANTLR 3.4. With `--auto-download`, cvc5 will automatically download and build
  67 ANTLR 3.4.
  68
  69
  70 ### GMP (GNU Multi-Precision arithmetic library)
  71
  72 GMP is usually available on you distribution and should be used from there. It
  73 can be downloaded and built automatically. If it does not, or you want to
  74 cross-compile, or you want to build cvc5 statically but the distribution does
  75 not ship static libraries, cvc5 builds GMP automatically when `--auto-download`
  76 is given.
  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 downloaded and built automatically.
  85
  86 ## Optional Dependencies
  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 ### Dependencies for Language Bindings
 184
 185 * Python
 186   * [Cython](https://cython.org/)
 187   * [scikit-build](https://pypi.org/project/scikit-build/)
 188   * [pytest](https://docs.pytest.org/en/6.2.x/)
 189
 190 If you're interested in helping to develop, maintain, and test a language
 191 binding, please contact one of the project leaders.
 192
 193
 194 ## Building the API Documentation
 195
 196 Building the API documentation of cvc5 requires the following dependencies:
 197 * [Doxygen](https://www.doxygen.nl)
 198 * [Sphinx](https://www.sphinx-doc.org),
 199   [sphinx-tabs](https://sphinx-tabs.readthedocs.io/),
 200   [sphinxcontrib-bibtex](https://sphinxcontrib-bibtex.readthedocs.io)
 201 * [Breathe](https://breathe.readthedocs.io)
 202
 203 To build the documentation, configure cvc5 with `./configure.sh --docs`.
 204 Building cvc5 will then include building the API documentation.
 205
 206 The API documentation can then be found at `<build_dir>/docs/sphinx/index.html`.
 207
 208 To only build the documentation, change to the build directory and call
 209 `make docs`.
 210
 211 To build the documentation for GitHub pages, change to the build directory
 212 and call `make docs-gh`. The content of directory `<build_dir>/docs/sphinx-gh`
 213 can then be copied over to GitHub pages.
 214
 215
 216 ## Building the Examples
 217
 218 See `examples/README.md` for instructions on how to build and run the examples.
 219
 220 ## Testing cvc5
 221
 222 We use `ctest` as test infrastructure, for all command-line options of ctest,
 223 see `ctest -h`. Some useful options are:
 224
 225     ctest -R <regex>           # run all tests with names matching <regex>
 226     ctest -E <regex>           # exclude tests with names matching <regex>
 227     ctest -L <regex>           # run all tests with labels matching <regex>
 228     ctest -LE <regex>          # exclude tests with labels matching <regex>
 229     ctest                      # run all tests
 230     ctest -jN                  # run all tests in parallel with N threads
 231     ctest --output-on-failure  # run all tests and print output of failed tests
 232
 233 We have 4 categories of tests:
 234 - **examples** in directory `examples`
 235   (label: **example**)
 236 - **regression tests** (5 levels) in directory `test/regress`
 237   (label: **regressN** with N the regression level)
 238 - **api tests** in directory `test/api`
 239   (label: **api**)
 240 - **unit tests** in directory `test/unit`
 241   (label: **unit**)
 242
 243 ### Testing System Tests
 244
 245 The system tests are not built by default.
 246
 247     make apitests                         # build and run all system tests
 248     make <api_test>                       # build test/system/<system_test>.<ext>
 249     ctest api/<api_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 `api/` + `<api_test>` (for `<api_test>` in `test/api`)
 254 as test target name.
 255
 256     make ouroborous                       # build test/api/ouroborous.cpp
 257     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
 258                                           # > runs api/ouroborous
 259     ctest -R ouroborous$                  # run all tests that match '*ouroborous'
 260                                           # > runs api/ouroborous
 261     ctest -R api/ouroborous$              # run all tests that match '*api/ouroborous'
 262                                           # > runs api/ouroborous
 263 ### Testing Unit Tests
 264
 265 The unit tests are not built by default.
 266
 267 Note that cvc5 can only be configured with unit tests in non-static builds with
 268 assertions enabled.
 269
 270     make units                            # build and run all unit tests
 271     make <unit_test>                      # build test/unit/<subdir>/<unit_test>.<ext>
 272     ctest unit/<subdir>/<unit_test>       # run test/unit/<subdir>/<unit_test>.<ext>
 273
 274 All unit test binaries are built into `<build_dir>/bin/test/unit`.
 275
 276 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
 277 `test/unit/<subdir>`) as test target name.
 278
 279     make map_util_black                   # build test/unit/base/map_util_black.cpp
 280     ctest -R map_util_black               # run all tests that match '*map_util_black*'
 281                                           # > runs unit/base/map_util_black
 282     ctest -R base/map_util_black$         # run all tests that match '*base/map_util_black'
 283                                           # > runs unit/base/map_util_black
 284     ctest -R unit/base/map_util_black$    # run all tests that match '*unit/base/map_util_black'
 285                                           # > runs unit/base/map_util_black
 286
 287 ### Testing Regression Tests
 288
 289 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
 290 in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 291
 292     ctest -L regress                      # run all regression tests
 293     ctest -L regress0                     # run all regression tests in level 0
 294     ctest -L regress[0-1]                 # run all regression tests in level 0 and 1
 295     ctest -R regress                      # run all regression tests
 296     ctest -R regress0                     # run all regression tests in level 0
 297     ctest -R regress[0-1]                 # run all regression tests in level 0 and 1
 298     ctest -R regress0/bug288b             # run all tests that match '*regress0/bug288b*'
 299                                           # > runs regress0/bug288b
 300 ### Custom Targets
 301
 302 All custom test targets build and run a preconfigured set of tests.
 303
 304 - `make check [-jN] [ARGS=-jN]`
 305   The default build-and-test target for cvc5, builds and runs all examples,
 306   all system and unit tests, and regression tests from levels 0 to 2.
 307
 308 - `make systemtests [-jN] [ARGS=-jN]`
 309   Build and run all system tests.
 310
 311 - `make units [-jN] [ARGS=-jN]`
 312   Build and run all unit tests.
 313
 314 - `make regress [-jN] [ARGS=-jN]`
 315   Build and run regression tests from levels 0 to 2.
 316
 317 - `make runexamples [-jN] [ARGS=-jN]`
 318   Build and run all examples.
 319
 320 - `make coverage [-jN] [ARGS=-jN]`
 321   Build and run all tests (system and unit tests, regression tests level 0-4)
 322   with gcov to determine code coverage.
 323
 324 We use `ctest` as test infrastructure, and by default all test targets
 325 are configured to **run** in parallel with the maximum number of threads
 326 available on the system. Override with `ARGS=-jN`.
 327
 328 Use `-jN` for parallel **building** with `N` threads.
 329
 330
 331 ## Recompiling a specific cvc5 version with different LGPL library versions
 332
 333 To recompile a specific static binary of cvc5 with different versions of the
 334 linked LGPL libraries perform the following steps:
 335
 336 1. Make sure that you have installed the desired LGPL library versions.
 337    You can check the versions found by cvc5's build system during the configure
 338    phase.
 339
 340 2. Determine the commit sha and configuration of the cvc5 binary
 341 ```
 342 cvc5 --show-config
 343 ```
 344 3. Download the specific source code version:
 345 ```
 346 wget https://github.com/CVC4/CVC4/archive/<commit-sha>.tar.gz
 347 ```
 348 4. Extract the source code
 349 ```
 350 tar xf <commit-sha>.tar.gz
 351 ```
 352 5. Change into source code directory
 353 ```
 354 cd cvc5-<commit-sha>
 355 ```
 356 6. Configure cvc5 with options listed by `cvc5 --show-config`
 357 ```
 358 ./configure.sh --static <options>
 359 ```
 360
 361 7. Follow remaining steps from [build instructions](#building-cvc5)