INSTALL.rst

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