diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-15 23:00:47 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-15 21:00:47 +0000 |
| commit | 44299210154706701d56bfa40e8cb5c58079e9ca (patch) | |
| tree | b7447be8cd5401b738b986971f036f8022cfbb64 /CMakeLists.txt | |
| parent | 6bae871954c48993009ed91d4b907c136017ed38 (diff) | |
Add cocoalib (#6731)
This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization.
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index d7512e874..b555c7bdc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -127,6 +127,7 @@ cvc5_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(USE_POLY "Use LibPoly for polynomial arithmetic") +option(USE_COCOA "Use CoCoALib for further polynomial operations") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Force Python 2 (deprecated)") @@ -462,6 +463,11 @@ else() set(CVC5_USE_POLY_IMP 0) endif() +if(USE_COCOA) + find_package(CoCoA REQUIRED 0.99711) + add_definitions(-DCVC5_USE_COCOA) +endif() + if(USE_EDITLINE) find_package(Editline REQUIRED) set(HAVE_LIBEDITLINE 1) @@ -657,6 +663,7 @@ print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT}) print_config("GLPK " ${USE_GLPK}) print_config("Kissat " ${USE_KISSAT}) print_config("LibPoly " ${USE_POLY}) +print_config("CoCoALib " ${USE_COCOA}) message("") print_config("Build libcvc5 only " ${BUILD_LIB_ONLY}) |