diff options
-rw-r--r-- | CMakeLists.txt | 7 | ||||
-rw-r--r-- | cmake/FindCoCoA.cmake | 96 | ||||
-rwxr-xr-x | configure.sh | 7 |
3 files changed, 110 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}) diff --git a/cmake/FindCoCoA.cmake b/cmake/FindCoCoA.cmake new file mode 100644 index 000000000..1a4f82e9f --- /dev/null +++ b/cmake/FindCoCoA.cmake @@ -0,0 +1,96 @@ +############################################################################### +# Top contributors (to current version): +# Gereon Kremer +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Find CoCoA +# CoCoA_FOUND - system has CoCoA lib +# CoCoA_INCLUDE_DIR - the CoCoA include directory +# CoCoA_LIBRARIES - Libraries needed to use CoCoA +## + +include(deps-helper) + +find_path(CoCoA_INCLUDE_DIR NAMES CoCoA/CoCoA.h) +find_library(CoCoA_LIBRARIES NAMES CoCoA) + +set(CoCoA_FOUND_SYSTEM FALSE) +if(CoCoA_INCLUDE_DIR AND CoCoA_LIBRARIES) + set(CoCoA_FOUND_SYSTEM TRUE) + + file(STRINGS ${CoCoA_INCLUDE_DIR}/CoCoA/library.H CoCoA_VERSION + REGEX "^COCOALIB_VERSION=.*" + ) + string(REGEX MATCH "[0-9]+\\.[0-9]+" CoCoA_VERSION "${CoCoA_VERSION}") + + check_system_version("CoCoA") +endif() + +if(NOT CoCoA_FOUND_SYSTEM) + check_ep_downloaded("CoCoA-EP") + if(NOT CoCoA-EP_DOWNLOADED) + check_auto_download("CoCoA" "--no-cocoa") + endif() + + include(ExternalProject) + + set(CoCoA_VERSION "0.99712") + + if("${CMAKE_GENERATOR}" STREQUAL "Unix Makefiles") + # use $(MAKE) instead of "make" to allow for parallel builds + set(make_cmd "$(MAKE)") + else() + # $(MAKE) does not work with ninja + set(make_cmd "make") + endif() + + ExternalProject_Add( + CoCoA-EP + ${COMMON_EP_CONFIG} + URL "http://cocoa.dima.unige.it/cocoalib/tgz/CoCoALib-${CoCoA_VERSION}.tgz" + URL_HASH SHA1=873d0b60800cd3852939816ce0aa2e7f72dac4ce + BUILD_IN_SOURCE YES + CONFIGURE_COMMAND ./configure --prefix=<INSTALL_DIR> + BUILD_COMMAND ${make_cmd} library + ) + # Remove install directory before make install. CoCoA will complain otherwise + ExternalProject_Add_Step( + CoCoA-EP clear-install + COMMAND ${CMAKE_COMMAND} -E remove_directory <INSTALL_DIR>/include/CoCoA-${CoCoA_VERSION} + DEPENDEES build + DEPENDERS install + ) + + add_dependencies(CoCoA-EP GMP) + + set(CoCoA_INCLUDE_DIR "${DEPS_BASE}/include/") + set(CoCoA_LIBRARIES "${DEPS_BASE}/lib/libcocoa.a") +endif() + +set(CoCoA_FOUND TRUE) + +add_library(CoCoA STATIC IMPORTED GLOBAL) +set_target_properties(CoCoA PROPERTIES IMPORTED_LOCATION "${CoCoA_LIBRARIES}") +set_target_properties( + CoCoA PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${CoCoA_INCLUDE_DIR}" +) +set_target_properties(CoCoA PROPERTIES INTERFACE_LINK_LIBRARIES GMP) + +mark_as_advanced(CoCoA_FOUND) +mark_as_advanced(CoCoA_FOUND_SYSTEM) +mark_as_advanced(CoCoA_INCLUDE_DIR) +mark_as_advanced(CoCoA_LIBRARIES) + +if(CoCoA_FOUND_SYSTEM) + message(STATUS "Found CoCoA ${CoCoA_VERSION}: ${CoCoA_LIBRARIES}") +else() + message(STATUS "Building CoCoA ${CoCoA_VERSION}: ${CoCoA_LIBRARIES}") + add_dependencies(CoCoA CoCoA-EP) +endif() diff --git a/configure.sh b/configure.sh index 3e59cadc9..487bbcb5a 100755 --- a/configure.sh +++ b/configure.sh @@ -63,6 +63,7 @@ The following flags enable optional packages (disable with --no-<option name>). --cryptominisat use the CryptoMiniSat SAT solver --kissat use the Kissat SAT solver --poly use the LibPoly library [default=yes] + --cocoa use the CoCoA library --symfpu use SymFPU for floating point solver [default=yes] --editline support the editline library @@ -121,6 +122,7 @@ glpk=default gpl=default kissat=default poly=ON +cocoa=default muzzle=default ninja=default profiling=default @@ -240,6 +242,9 @@ do --poly) poly=ON;; --no-poly) poly=OFF;; + --cocoa) cocoa=ON;; + --no-cocoa) cocoa=OFF;; + --muzzle) muzzle=ON;; --no-muzzle) muzzle=OFF;; @@ -391,6 +396,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat" [ $poly != default ] \ && cmake_opts="$cmake_opts -DUSE_POLY=$poly" +[ $cocoa != default ] \ + && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa" [ $symfpu != default ] \ && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" [ "$abc_dir" != default ] \ |