From 44299210154706701d56bfa40e8cb5c58079e9ca Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 15 Jun 2021 23:00:47 +0200 Subject: [PATCH] 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. --- CMakeLists.txt | 7 ++++ cmake/FindCoCoA.cmake | 96 +++++++++++++++++++++++++++++++++++++++++++ configure.sh | 7 ++++ 3 files changed, 110 insertions(+) create mode 100644 cmake/FindCoCoA.cmake 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= + 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 /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-