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

.github/actions/add-package/action.yml

@@ -45,6 +45,10 @@ runs:
     - name: install pyGithub
       shell: ${{ inputs.shell }}
       run: |
+        # Upgrading pyopenssl resolves the following error:
+        # AttributeError:
+        #   module 'lib' has no attribute 'X509_V_FLAG_NOTIFY_POLICY'
+        python3 -m pip install -U pyopenssl
         python3 -m pip install pyGithub
 
     - name: Store to latest

.github/actions/install-dependencies/action.yml

@@ -3,10 +3,6 @@ description: Install necessary dependencies on the target system
 inputs:
   with-documentation:
     default: false
-  with-python-bindings:
-    default: false
-  with-python-packaging:
-    default: false
   windows-build:
     default: false
     type: boolean
@@ -112,33 +108,6 @@ runs:
         python3 -m venv ~/.venv
         echo "$HOME/.venv/bin" >> $GITHUB_PATH
         echo "::endgroup::"
-
-    - name: Install Python modules for building and testing
-      shell: ${{ inputs.shell }}
-      run: |
-        echo "::group::Install Python modules for building and testing"
-        python3 -m pip install -r contrib/requirements_build.txt
-        python3 -m pip install pexpect # For interactive shell tests
-        echo "::endgroup::"
-
-    - name: Install software for Python bindings
-      if: inputs.with-python-bindings == 'true'
-      shell: ${{ inputs.shell }}
-      run: |
-        echo "::group::Install software for Python bindings"
-        python3 -m pip install -q --upgrade pip
-        python3 -m pip install -r contrib/requirements_python_dev.txt
-        echo "::endgroup::"
-
-    - name: Install software for Python packaging
-      if: inputs.with-python-packaging == 'true'
-      shell: ${{ inputs.shell }}
-      run: |
-        echo "::group::Install software for Python packaging"
-        python3 -m pip install -q --upgrade pip
-        python3 -m pip install twine
-        python3 -m pip install -U urllib3 requests
-        echo "::endgroup::"
     
     - name: Install software for documentation
       if: inputs.with-documentation == 'true'

.github/workflows/ci.yml

@@ -121,7 +121,6 @@ jobs:
       uses: ./.github/actions/install-dependencies
       with:
         with-documentation: ${{ matrix.build-documentation }}
-        with-python-bindings: ${{ matrix.python-bindings }}
         windows-build: ${{ matrix.windows-build }}
         shell: ${{ matrix.shell }}
 

.github/workflows/cmake-version.yml

@@ -29,7 +29,6 @@ jobs:
       uses: ./.github/actions/install-dependencies
       with:
         with-documentation: true
-        with-python-bindings: true
 
     - name: Setup caches
       uses: ./.github/actions/setup-cache

CMakeLists.txt

@@ -222,6 +222,7 @@ include(Config${CMAKE_BUILD_TYPE})
 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 add_check_c_cxx_flag("-Wall")
 add_check_c_cxx_supression_flag("-Wno-unused-private-field")
+add_check_c_cxx_supression_flag("-Wno-dangling-reference")
 add_check_c_flag("-fexceptions")
 add_check_cxx_flag("-Wsuggest-override")
 add_check_cxx_flag("-Wnon-virtual-dtor")
@@ -369,6 +370,34 @@ else()
   find_package(Python COMPONENTS Interpreter REQUIRED)
 endif()
 
+# Keep the PATH to the Python binary before setting venv.
+# 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()
+
+# 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)
+
+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_package(Python COMPONENTS Interpreter REQUIRED)
+endif()
+
 find_package(GMP 6.3 REQUIRED)
 
 if(ENABLE_ASAN)

INSTALL.rst

@@ -121,15 +121,14 @@ versions; more recent versions should be compatible.
 - `GNU Make <https://www.gnu.org/software/make/>`_
   or `Ninja <https://ninja-build.org/>`_
 - `Python >= 3.6 <https://www.python.org>`_
-  + module `tomli <https://pypi.org/project/tomli/>`_
+  + module `tomli <https://pypi.org/project/tomli/>`_ (Python < 3.11)
   + module `pyparsing <https://pypi.org/project/pyparsing/>`_
 - `GMP v6.3 (GNU Multi-Precision arithmetic library) <https://gmplib.org>`_
 - `CaDiCaL >= 1.6.0 (SAT solver) <https://github.com/arminbiere/cadical>`_
 - `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_
 
-For Python, to install these dependencies automatically, please use:
-
-  - `pip install -r contrib/requirements_build.txt`
+The Python modules will be installed automatically in
+a virtual environment if they are missing.
 
 CaDiCaL (SAT solver)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -272,9 +271,8 @@ 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)>`.
 
-For Python, to install these depedencies automatically, please use:
-
-  - `pip install -r contrib/requirements_python_dev.txt`
+The Python modules will be installed automatically in
+a virtual environment if they are missing.
 
 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.

cmake/FindCython.cmake

@@ -22,36 +22,33 @@ execute_process(
     OUTPUT_STRIP_TRAILING_WHITESPACE
 )
 
-if (Cython_FIND_REQUIRED)
-  set(Cython_FIND_MODE FATAL_ERROR)
-else()
-  set(Cython_FIND_MODE STATUS)
-endif()
+set(Cython_FOUND FALSE)
 
 if (Cython_VERSION_CHECK_RESULT EQUAL 0)
-    set(Cython_FOUND TRUE)
     message(STATUS "Found Cython version: ${Cython_VERSION}")
     if (DEFINED Cython_FIND_VERSION)
         if(Cython_FIND_VERSION_EXACT)
             if (NOT (Cython_VERSION VERSION_EQUAL ${Cython_FIND_VERSION}))
-            message(${Cython_FIND_MODE}
-                "Cython version == ${Cython_FIND_VERSION} is required, "
-                "but found version ${Cython_VERSION}")
+              message(STATUS
+                "Installing module Cython==${Cython_FIND_VERSION} in Python venv"
+              )
+              execute_process(
+                COMMAND
+                ${Python_EXECUTABLE} -m pip install Cython==${Cython_FIND_VERSION}
+              )
             endif()
         else()
             if (Cython_VERSION VERSION_LESS ${Cython_FIND_VERSION})
-                message(${Cython_FIND_MODE}
-                    "Cython version >= ${Cython_FIND_VERSION} is required, "
-                    "but found version ${Cython_VERSION}")
+              message(STATUS "Upgrading module Cython in Python venv")
+              execute_process(COMMAND
+                ${Python_EXECUTABLE} -m pip install Cython -U
+              )
             endif()
         endif()
     endif()
 else()
-    set(Cython_FOUND FALSE)
-    message(${Cython_FIND_MODE}
-        "Could not find module Cython for Python "
-        "version ${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}. "
-        "Make sure to install Cython for this Python version "
-        "via \n`${Python_EXECUTABLE} -m pip install Cython'.\n"
-        "Note: You need to have pip installed for this Python version.")
+    message(STATUS "Installing module Cython in Python venv")
+    execute_process(COMMAND ${Python_EXECUTABLE} -m pip install Cython)
 endif()
+
+set(Cython_FOUND TRUE)

cmake/Helpers.cmake

@@ -247,12 +247,11 @@ function(check_python_module module)
   endif()
 
   if(RET_MODULE_TEST)
-    message(FATAL_ERROR
-        "Could not find module ${module_name} for Python "
-        "version ${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}. "
-        "Make sure to install ${module_name} for this Python version "
-        "via \n`${Python_EXECUTABLE} -m pip install ${module_name}'.\n"
-        "Note: You need to have pip installed for this Python version.")
+    message(STATUS "Installing module ${module} in Python venv")
+    execute_process(
+      COMMAND
+      ${Python_EXECUTABLE} -m pip install ${module}
+    )
   endif()
 endfunction()
 

contrib/cibw/before_all_linux.sh

@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
 
-python3 -m pip install --user -r contrib/requirements_build.txt
-
 ./configure.sh production --auto-download --python-bindings --python-only-src --prefix=./install
 
 SETUP_CFG=./build/src/api/python/setup.cfg

contrib/cibw/before_all_macos.sh

@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
 
-python3 -m pip install -r contrib/requirements_build.txt
-
 ./configure.sh production --auto-download \
   --python-bindings --python-only-src --prefix=./install -DBUILD_GMP=1
 

contrib/cibw/before_all_windows.sh

@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
 
-python3 -m pip install --user -r contrib/requirements_build.txt
-
 ./configure.sh production --auto-download --python-bindings --python-only-src --prefix=./install
 
 SETUP_CFG=./build/src/api/python/setup.cfg

docs/api/python/python.rst

@@ -47,7 +47,6 @@ Before building and installing, the following dependencies should be installed,
 .. code:: bash
 
   brew install cmake python gmp java
-  pip3 install -r contrib/requirements_python_dev.txt
 
 
 Then `cvc5` can be installed from source as follows:

docs/theories/finite_field.rst

@@ -99,6 +99,16 @@ Examples
   (check-sat)
   ; unsat
 
+
+Experimental Extensions
+^^^^^^^^^^^^^^^^^^^^^^^
+
+These features of the theory are experimental; they may be removed in the
+future:
+
+* ``ff.bitsum``: an n-ary operator for bitsums: ``(ff.bitsum x0 x1 x2)`` is equivalent to :math:`x_0 + 2x_1 + 4x_2`.
+* ``ff.neg``: unary negation
+
 Solvers
 ^^^^^^^
 

docs/theories/sets-and-relations.rst

@@ -41,6 +41,10 @@ a `cvc5::Solver solver` object.
 +----------------------+----------------------------------------------+---------------------------------------------------------------------------+
 | Singleton Set        | ``(set.singleton 1)``                        | ``Term t = solver.mkTerm(Kind::SET_SINGLETON, {solver.mkInteger(1)});``   |
 +----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Emptyset tester      | ``(set.is_empty X)``                         | ``Term t = solver.mkTerm(Kind::SET_IS_EMPTY, {X});``                      |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Singleton tester     | ``(set.is_singleton X)``                     | ``Term t = solver.mkTerm(Kind::SET_IS_SINGLETON, {X});``                  |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
 | Cardinality          | ``(set.card X)``                             | ``Term t = solver.mkTerm(Kind::SET_CARD, {X});``                          |
 +----------------------+----------------------------------------------+---------------------------------------------------------------------------+
 | Insert / Finite Sets | ``(set.insert 1 2 3 (set.singleton 4))``     | ``Term one = solver.mkInteger(1);``                                       |

examples/api/python/CMakeLists.txt

@@ -39,15 +39,24 @@ set(EXAMPLES_API_PYTHON
 
 find_package(Python ${CVC5_BINDINGS_PYTHON_VERSION} EXACT REQUIRED)
 
-# Find Python bindings in the corresponding python-*/site-packages directory.
-# Lookup Python module directory and store path in PYTHON_MODULE_PATH.
-execute_process(COMMAND
-                  ${Python_EXECUTABLE} -c
-                    "from distutils.sysconfig import get_python_lib;\
-                     print(get_python_lib(plat_specific=True,\
-                             prefix='${CMAKE_PREFIX_PATH}/../..'))"
-                OUTPUT_VARIABLE PYTHON_MODULE_PATH
-                OUTPUT_STRIP_TRAILING_WHITESPACE)
+# Check whether the cvc5 module is already installed
+execute_process(
+  COMMAND ${Python_EXECUTABLE} -c "import cvc5"
+  RESULT_VARIABLE PYTHON_CVC5_RC
+  ERROR_QUIET
+)
+
+if(NOT (PYTHON_CVC5_RC EQUAL 0))
+  # Find Python bindings in the corresponding python-*/site-packages directory.
+  # Lookup Python module directory and store path in PYTHON_MODULE_PATH.
+  execute_process(COMMAND
+  ${Python_EXECUTABLE} -c
+    "import sysconfig;\
+     print('${CMAKE_PREFIX_PATH}/../..'+\
+     sysconfig.get_paths()['platlib'].split(sysconfig.get_config_var('platbase'))[1])"
+  OUTPUT_VARIABLE PYTHON_MODULE_PATH
+  OUTPUT_STRIP_TRAILING_WHITESPACE)
+endif()
 
 function(create_python_example example)
   set(example_test example/api/python/${example})