Merge branch 'main' of https://github.com/cvc5/cvc5

.github/workflows/ci.yml

@@ -63,7 +63,7 @@ jobs:
 
           - name: win64:production
             os: windows-latest
-            config: production --auto-download
+            config: production --auto-download --java-bindings
             cache-key: production-win64-native
             strip-bin: strip
             windows-build: true

AUTHORS

@@ -10,35 +10,37 @@ Current:
   Leni Aniva, Stanford University
   Haniel Barbosa, The University of Iowa, Universidade Federal de Minas Gerais
   Clark Barrett, New York University, Google, Stanford University
-  Martin Brain, University of Oxford
-  Vinicius Camillo, Universidade Federal de Minas Gerais
-  Gereon Kremer, Stanford University
   Hanna Lachnitt, Stanford University
+  Daniel Larraz, The University of Iowa
   Abdalrhman Mohamed, The University of Iowa
   Mudathir Mohamed, The University of Iowa
   Aina Niemetz, Stanford University
-  Andres Noetzli, Stanford University
   Alex Ozdemir, Stanford University
   Mathias Preiner, Stanford University
   Andrew Reynolds, The University of Iowa, EPFL
-  Ying Sheng, Stanford University
+  Hans-Jörg Schurr, The University of Iowa
   Cesare Tinelli, The University of Iowa
   Amalee Wilson, Stanford University
   Yoni Zohar, Stanford University
 
 Alumni:
   Kshitij Bansal, New York University, Google
   Francois Bobot, The University of Iowa, Commissariat a l'Energie Atomique
+  Martin Brain, University of Oxford
+  Vinicius Camillo, Universidade Federal de Minas Gerais
   Christopher Conway, New York University, Google
   Morgan Deters, New York University
   Liana Hadarean, New York University, Mentor Graphics Corporation
   Ahmed Irfan, Stanford University
   Dejan Jovanovic, New York University, SRI International
   Guy Katz, New York University, Stanford University
-  Makai Mann, Stanford University
   Tim King, New York University, Universite Joseph Fourier, Google
+  Gereon Kremer, Stanford University
   Tianyi Liang, The University of Iowa
+  Makai Mann, Stanford University
   Paul Meng, The University of Iowa
+  Andres Noetzli, Stanford University
+  Ying Sheng, Stanford University
 
 Other contributors to the cvc5 codebase are listed in the THANKS file.
 

CMakeLists.txt

@@ -99,7 +99,11 @@ cvc5_option(ENABLE_TRACING        "Enable tracing")
 cvc5_option(ENABLE_UNIT_TESTING   "Enable unit testing")
 cvc5_option(ENABLE_VALGRIND       "Enable valgrind instrumentation")
 cvc5_option(ENABLE_AUTO_DOWNLOAD  "Enable automatic download of dependencies")
+cvc5_option(USE_PYTHON_VENV       "Install Python dependencies in virtual environment")
 cvc5_option(ENABLE_IPO            "Enable interprocedural optimization")
+
+cvc5_set_option(USE_PYTHON_VENV ON)
+
 # >> 2-valued: ON OFF
 #    > for options where we don't need to detect if set by user (default: OFF)
 option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
@@ -364,37 +368,52 @@ else()
   endif()
 endif()
 
-if(DEFINED BUILD_BINDINGS_PYTHON_VERSION) 
-  find_package(Python ${BUILD_BINDINGS_PYTHON_VERSION} EXACT COMPONENTS Interpreter REQUIRED)
+# Find a Python interpreter on the system. It serves two exclusive purposes:
+# either to be used when the '--auto-download' option is not specified, or
+# to create a virtual environment when the '--auto-download' option is given.
+# In the latter case, it is also used to install the Python bindings (if built).
+if(DEFINED BUILD_BINDINGS_PYTHON_VERSION)
+  find_package(Python ${BUILD_BINDINGS_PYTHON_VERSION}
+    EXACT COMPONENTS Interpreter REQUIRED
+  )
 else()
   find_package(Python COMPONENTS Interpreter REQUIRED)
 endif()
 
 # Keep the PATH to the Python binary before setting venv.
+# Use a CACHE variable to remember the original value.
 # We use this path in the installation step of the Python bindings.
-set(Python_BASE_EXECUTABLE "${Python_EXECUTABLE}")
-
-# Set up Python venv if one doesn't exist already
-set(VENV_PATH "${CMAKE_BINARY_DIR}/venv-${Python_VERSION}")
-if(NOT EXISTS ${VENV_PATH})
-  message(STATUS "Creating Python virtual environment")
-  # Use packages installed in the base installation if they're already present
-  execute_process (COMMAND
-    "${Python_EXECUTABLE}" -m venv --system-site-packages "${VENV_PATH}"
-  )
-endif()
+set(Python_BASE_EXECUTABLE "${Python_EXECUTABLE}"
+    CACHE STRING "Base Python executable")
+
+if(ENABLE_AUTO_DOWNLOAD AND USE_PYTHON_VENV)
+  # Set up Python venv if one doesn't exist already
+  set(VENV_PATH "${CMAKE_BINARY_DIR}/venv-${Python_VERSION}")
+  if(NOT EXISTS ${VENV_PATH})
+    message(STATUS "Creating Python virtual environment")
+    # Use packages installed in the base installation if they're already present
+    execute_process (
+      COMMAND
+        "${Python_EXECUTABLE}" -m venv --system-site-packages "${VENV_PATH}"
+      RESULT_VARIABLE VENV_CMD_EXIT_CODE
+    )
+    if(VENV_CMD_EXIT_CODE)
+      message(FATAL_ERROR "Could not create Python virtual environment")
+    endif()
+  endif()
 
-# Find (and set up) the Python interpreter within the virtual environment
-set(ENV{VIRTUAL_ENV} "${VENV_PATH}")
-set(Python_FIND_VIRTUALENV FIRST)
-unset(Python_EXECUTABLE)
-unset(Python_EXECUTABLE CACHE)
+  # Set up variables to find Python within the virtual environment
+  set(ENV{VIRTUAL_ENV} "${VENV_PATH}")
+  unset(Python_EXECUTABLE CACHE)
+  if(EXISTS ${VENV_PATH}/bin/python3)
+    set(Python_EXECUTABLE ${VENV_PATH}/bin/python3)
+  elseif(EXISTS ${VENV_PATH}/Scripts/python.exe)
+    set(Python_EXECUTABLE ${VENV_PATH}/Scripts/python.exe)
+  else()
+    message(FATAL_ERROR "Could not find Python interpreter in venv")
+  endif()
 
-if(BUILD_BINDINGS_PYTHON)
-  # If the component Development is requested, CMake strongly recommends to
-  # also include the component Interpreter to get expected result.
-  find_package(Python COMPONENTS Interpreter Development REQUIRED)
-else()
+  # Find the Python interpreter within the virtual environment
   find_package(Python COMPONENTS Interpreter REQUIRED)
 endif()
 

INSTALL.rst

@@ -127,8 +127,9 @@ versions; more recent versions should be compatible.
 - `CaDiCaL >= 1.6.0 (SAT solver) <https://github.com/arminbiere/cadical>`_
 - `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_
 
-The Python modules will be installed automatically in
-a virtual environment if they are missing.
+If ``--auto-download`` is given, the Python modules will be installed automatically in
+a virtual environment if they are missing. To install the modules globally and skip
+the creation of the virtual environment, configure cvc5 with ``./configure.sh --no-pyvenv``.
 
 CaDiCaL (SAT solver)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -271,8 +272,9 @@ Dependencies for Language Bindings
   - `pytest <https://docs.pytest.org/en/6.2.x/>`_
   - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`.
 
-The Python modules will be installed automatically in
-a virtual environment if they are missing.
+If ``--auto-download`` is given, the Python modules will be installed automatically in
+a virtual environment if they are missing. To install the modules globally and skip
+the creation of the virtual environment, configure cvc5 with ``./configure.sh --no-pyvenv``.
 
 If configured with ``--pythonic-path=PATH``, the build system will expect the Pythonic API's source to be at ``PATH``.
 Otherwise, if configured with ``--auto-download``, the build system will download it.

THANKS

@@ -15,6 +15,8 @@ Thanks to:
 
 - Simon Dierl for fixing the ENABLE_BEST option in the build system in 2019.
 
+- Florian Frohn for fixing the compilation of cvc5 with musl-libc in 2023.
+
 - Finn Haedicke of University of Bremen, Germany for fixing namespace specifiers
   in CVC4's version of minisat in 2015.
 
@@ -23,6 +25,8 @@ Thanks to:
 - Thomas Hunger for some important patches to CVC4's SWIG interfaces in March
   2014.
 
+- Jerry James for multiple bugfixes in 2023.
+
 - Andrew V. Jones (now Teylu) for several fixes, refactoring the GLPK-based
   approximating Simplex solver, and working towards a native Windows build
   since 2019.
@@ -34,20 +38,38 @@ Thanks to:
 - Cristian Mattarei of Stanford University for fixing an issue with parsing
   floating point numbers in 2017.
 
+- José Neto for improvements to build system and web version of cvc5 in
+  2023 and 2024.
+
+- Tobias Nießen for a correction to the API documentation in 2023.
+
 - Jordy Ruiz of University of Toulouse for fixing throw specifiers on the theory
   output channels in 2015.
 
+- Áron Ricardo Perez-Lopez for solving an issue with static compilation in 2023.
+
 - Clement Pit-Claudel of MIT for improving the signal handling support for
   Windows builds in 2017.
 
+- Sorawee Porncharoenwase for fixing an issue related to compiling cvc5 with
+  CoCoA on M1/M2 CPUs.
+
+- sarkoxed for extending the finite fields API to allow custom bases for string
+  representations in 2023.
+
 - Florian Schanda for improving the readability of output of get-model in 2018.
 
 - Tom Smeding for a fix in the contrib/get-antlr-3.4 script in 2018.
 
+- Scott Talbert for improvements to the build systems and correcting spelling
+  errors in the documentation in 2023 and 2024.
+
 - Piotr Troja for several fixes in 2019.
 
 - Arjun Viswanathan for improvements in the CVC and the SMT2 parser.
 
+- Anjiang-Wei for fixing a typo in the Python API documentation in 2023.
+
 - Fabian Wolff in 2016 for fixing several spelling mistakes.
 
 - Justin Xu for contributing to refactoring CVC4's preprocessing infrastructure.

cmake/FindCLN.cmake

@@ -47,40 +47,87 @@ if(NOT CLN_FOUND_SYSTEM)
   include(ExternalProject)
 
   fail_if_cross_compiling("Windows" "" "CLN" "autoconf fails")
-  fail_if_cross_compiling("" "arm" "CLN" "syntax error in configure")
+
+  if("${CMAKE_GENERATOR}" STREQUAL "MSYS Makefiles")
+    message(FATAL_ERROR
+      "Compilation of CLN in the MSYS2 environment is not supported."
+    )
+  endif()
 
   set(CLN_VERSION "1.3.7")
+  set(CLN_SO_MAJOR_VER "6")
+  set(CLN_SO_MINOR_VER "0")
+  set(CLN_SO_PATCH_VER "7")
+  set(CLN_SO_VERSION
+    "${CLN_SO_MAJOR_VER}.${CLN_SO_MINOR_VER}.${CLN_SO_PATCH_VER}"
+  )
   string(REPLACE "." "-" CLN_TAG ${CLN_VERSION})
 
   find_program(AUTORECONF autoreconf)
   if(NOT AUTORECONF)
-    message(SEND_ERROR "Can not build CLN, missing binary for autoreconf")
+    message(FATAL_ERROR "Can not build CLN, missing binary for autoreconf")
+  endif()
+
+  set(CLN_INCLUDE_DIR "${DEPS_BASE}/include/")
+  if(BUILD_SHARED_LIBS)
+    set(LINK_OPTS --enable-shared --disable-static)
+    set(CLN_LIBRARIES "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+      set(CLN_BYPRODUCTS
+        <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln.${CLN_SO_MAJOR_VER}${CMAKE_SHARED_LIBRARY_SUFFIX}
+      )
+    else()
+      set(CLN_BYPRODUCTS
+        <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}.${CLN_SO_MAJOR_VER}
+        <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}.${CLN_SO_VERSION}
+      )
+    endif()
+  else()
+    set(LINK_OPTS --enable-static --disable-shared)
+    set(CLN_LIBRARIES "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_STATIC_LIBRARY_SUFFIX}")
+    set(CLN_BYPRODUCTS <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_STATIC_LIBRARY_SUFFIX})
+  endif()
+
+  set(CONFIGURE_OPTS "")
+  # CLN yields the following message at the end of the build process.
+  #     WARNING: `makeinfo' is missing on your system.
+  # This is a specific issue to Github CI on linux environments.
+  # Since makeinfo just builds the documentation for CLN,
+  # it is possible to get around this issue by just disabling it:
+  set(CONFIGURE_ENV env "MAKEINFO=true")
+
+  if(CMAKE_CROSSCOMPILING OR CMAKE_CROSSCOMPILING_MACOS)
+    set(CONFIGURE_OPTS
+      --host=${TOOLCHAIN_PREFIX}
+      --build=${CMAKE_HOST_SYSTEM_PROCESSOR})
+
+    set(CONFIGURE_ENV ${CONFIGURE_ENV} ${CMAKE_COMMAND} -E
+      env "CC_FOR_BUILD=cc")
+    if (CMAKE_CROSSCOMPILING_MACOS)
+      set(CONFIGURE_ENV
+        ${CONFIGURE_ENV}
+        env "CFLAGS=--target=${TOOLCHAIN_PREFIX}"
+        env "LDFLAGS=-arch ${CMAKE_OSX_ARCHITECTURES}")
+    endif()
   endif()
 
   ExternalProject_Add(
     CLN-EP
     ${COMMON_EP_CONFIG}
-    URL "https://www.ginac.de/CLN/cln.git/?p=cln.git\\\;a=snapshot\\\;h=cln_${CLN_TAG}\\\;sf=tgz"
-    URL_HASH SHA1=bd6dec17cf1088bdd592794d9239d47c752cf3da
-    DOWNLOAD_NAME cln.tgz
+    URL "https://www.ginac.de/CLN/cln-1.3.7.tar.bz2"
+    URL_HASH SHA1=17cf2c60e262e30f57caae39692fce7917e11d95
+    DOWNLOAD_NAME cln.tar.bz2
     CONFIGURE_COMMAND
-      ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> ./autogen.sh
-    COMMAND
-      ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> autoreconf -iv
-    COMMAND ${SHELL} <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-shared
-            --enable-static --with-pic
-    BUILD_BYPRODUCTS <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln.a
-                     <INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}
+      ${CONFIGURE_ENV} ${SHELL} <SOURCE_DIR>/configure
+        --prefix=<INSTALL_DIR> ${LINK_OPTS} --with-pic
+        ${CONFIGURE_OPTS}
+    BUILD_BYPRODUCTS ${CLN_BYPRODUCTS}
   )
 
   add_dependencies(CLN-EP GMP)
 
-  set(CLN_INCLUDE_DIR "${DEPS_BASE}/include/")
-  if(BUILD_SHARED_LIBS)
-    set(CLN_LIBRARIES "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}")
-  else()
-    set(CLN_LIBRARIES "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libcln.a")
-  endif()
 endif()
 
 set(CLN_FOUND TRUE)
@@ -107,4 +154,12 @@ if(CLN_FOUND_SYSTEM)
 else()
   message(STATUS "Building CLN ${CLN_VERSION}: ${CLN_LIBRARIES}")
   add_dependencies(CLN CLN-EP)
+
+  ExternalProject_Get_Property(CLN-EP BUILD_BYPRODUCTS INSTALL_DIR)
+  string(REPLACE "<INSTALL_DIR>" "${INSTALL_DIR}" BUILD_BYPRODUCTS "${BUILD_BYPRODUCTS}")
+
+  # Static builds install the CLN static libraries.
+  # These libraries are required to compile a program that
+  # uses the cvc5 static library.
+  install(FILES ${BUILD_BYPRODUCTS} TYPE ${LIB_BUILD_TYPE})
 endif()

cmake/FindCoCoA.cmake

@@ -100,4 +100,8 @@ if(CoCoA_FOUND_SYSTEM)
 else()
   message(STATUS "Building CoCoA ${CoCoA_VERSION}: ${CoCoA_LIBRARIES}")
   add_dependencies(CoCoA CoCoA-EP)
+  # Install static library only if it is a static build.
+  if(NOT BUILD_SHARED_LIBS)
+    install(FILES ${CoCoA_LIBRARIES} TYPE ${LIB_BUILD_TYPE})
+  endif()
 endif()

cmake/FindCryptoMiniSat.cmake

@@ -110,4 +110,8 @@ else()
       "Building CryptoMiniSat ${CryptoMiniSat_VERSION}: ${CryptoMiniSat_LIBRARIES}"
   )
   add_dependencies(CryptoMiniSat CryptoMiniSat-EP)
+  # Install static library only if it is a static build.
+  if(NOT BUILD_SHARED_LIBS)
+    install(FILES ${CryptoMiniSat_LIBRARIES} TYPE ${LIB_BUILD_TYPE})
+  endif()
 endif()