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.

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 ] \