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

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

@@ -96,7 +96,7 @@ runs:
         for cnt,asset in enumerate(assets):
           delete = False
           # We generate 10 artifacts per build:
-          # {Linux, Linux-arm64, macOS, macOS-arm64, Windows} * {static, shared}
+          # {Linux-x86_64, Linux-arm64, macOS-x86_64, macOS-arm64, Win64-x86_64} * {static, shared}
           if cnt >= 20: # Keep at most 2 builds
             delete = True
           if asset.name.startswith(samedayprefix):

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

@@ -109,6 +109,14 @@ runs:
         echo "$HOME/.venv/bin" >> $GITHUB_PATH
         echo "::endgroup::"
     
+    # Required for the installation of Python bindings
+    - name: Upgrade Python pip
+      shell: ${{ inputs.shell }}
+      run: |
+        echo "::group::Upgrade Python pip"
+        python3 -m pip install --upgrade pip
+        echo "::endgroup::"
+
     - name: Install software for documentation
       if: inputs.with-documentation == 'true'
       shell: ${{ inputs.shell }}

.github/workflows/ci.yml

@@ -19,7 +19,7 @@ jobs:
             python-bindings: true
             build-documentation: true
             check-examples: true
-            package-name: cvc5-Linux
+            package-name: cvc5-Linux-x86_64
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
@@ -37,7 +37,7 @@ jobs:
             strip-bin: strip
             python-bindings: true
             check-examples: true
-            package-name: cvc5-macOS
+            package-name: cvc5-macOS-x86_64
             macos-target: 10.13
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
@@ -69,7 +69,7 @@ jobs:
             windows-build: true
             shell: 'msys2 {0}'
             check-examples: true
-            package-name: cvc5-Win64
+            package-name: cvc5-Win64-x86_64
             exclude_regress: 1-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
@@ -192,18 +192,3 @@ jobs:
         github-token-latest: ${{ secrets.GITHUB_TOKEN }}
         github-token-release: ${{ secrets.ACTION_USER_TOKEN }}
         shell: ${{ matrix.shell }}
-
-  update-pr:
-    runs-on: ubuntu-latest
-    if: github.repository == 'cvc5/cvc5' && github.event_name == 'push' && github.ref == 'refs/heads/main'
-    concurrency:
-      group: update-pr
-    steps:
-      - name: Automatically update PR
-        uses: adRise/[email protected]
-        with:
-          token: ${{ secrets.ACTION_USER_TOKEN }}
-          base: 'main'
-          sort: 'created'
-          direction: 'asc'
-          required_approval_count: 1

CMakeLists.txt

@@ -232,6 +232,7 @@ add_check_cxx_flag("-Wsuggest-override")
 add_check_cxx_flag("-Wnon-virtual-dtor")
 add_check_c_cxx_flag("-Wimplicit-fallthrough")
 add_check_c_cxx_flag("-Wshadow")
+add_check_c_cxx_flag("-fno-operator-names")
 
 # Assume no dynamic initialization of thread-local variables in non-defining
 # translation units. This option should result in better performance and works

INSTALL.rst

@@ -267,10 +267,12 @@ Dependencies for Language Bindings
   - `JDK >= 1.8 <https://www.java.com>`_
 
 - Python
-
   - `Cython <https://cython.org/>`_ >= 3.0.0
+  - `pip <https://pip.pypa.io/>`_ >= 23.0
   - `pytest <https://docs.pytest.org/en/6.2.x/>`_
-  - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`.
+  - `repairwheel <https://github.com/jvolkman/repairwheel>`_ >= 0.2.9
+  - `setuptools <https://setuptools.pypa.io/>`_ >= 66.1.0
+  - The source for the `pythonic API <https://github.com/cvc5/cvc5_pythonic_api>`_
 
 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
@@ -279,6 +281,9 @@ the creation of the virtual environment, configure cvc5 with ``./configure.sh --
 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.
 
+Installing the Python bindings after building from source requires a Python environment with
+pip version 20.3 or higher.
+
 If you're interested in helping to develop, maintain, and test a language
 binding, please contact the cvc5 team via `our issue tracker
 <https://github.com/cvc5/cvc5/issues>`_.

cmake/FindGMP.cmake

@@ -164,4 +164,21 @@ if(GMP_FOUND_SYSTEM)
 else()
   message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
   add_dependencies(GMP GMP-EP)
+  # Static builds install the GMP static libraries.
+  # These libraries are required to compile a program that
+  # uses the cvc5 static library.
+  # On Windows, this installs the import libraries (LIB) and
+  # the DLL libraries (BIN)
+  install(
+    DIRECTORY ${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/
+    TYPE LIB
+    FILES_MATCHING PATTERN libgmp* PATTERN gmp*.pc
+  )
+  if(BUILD_SHARED_LIBS AND WIN32)
+    install(
+      DIRECTORY ${DEPS_BASE}/${CMAKE_INSTALL_BINDIR}/
+      TYPE BIN
+      FILES_MATCHING PATTERN libgmp*
+    )
+  endif()
 endif()

cmake/FindPip.cmake

@@ -0,0 +1,69 @@
+###############################################################################
+# Top contributors (to current version):
+#   Daniel Larraz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2024 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 Pip
+# Pip_FOUND - found Python pip
+# Pip_VERSION - Python pip version
+##
+
+macro(get_pip_version)
+  execute_process(
+    COMMAND "${Python_EXECUTABLE}" -c "import pip; print(pip.__version__)"
+    RESULT_VARIABLE Pip_VERSION_CHECK_RESULT
+    OUTPUT_VARIABLE Pip_VERSION
+    ERROR_QUIET
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+  )
+endmacro()
+
+get_pip_version()
+
+if (Pip_FIND_REQUIRED)
+  set(Pip_FIND_MODE FATAL_ERROR)
+else()
+  set(Pip_FIND_MODE STATUS)
+endif()
+
+if(Pip_VERSION_CHECK_RESULT EQUAL 0)
+  set(Pip_FOUND TRUE)
+  if(DEFINED Pip_FIND_VERSION)
+    if(Pip_VERSION VERSION_LESS ${Pip_FIND_VERSION})
+      if(ENABLE_AUTO_DOWNLOAD)
+        execute_process (
+          COMMAND "${Python_EXECUTABLE}" -m pip install -U pip
+        )
+        get_pip_version()
+      else()
+        message(${Pip_FIND_MODE}
+          "Pip version >= ${Pip_FIND_VERSION} is required, "
+          "but found version ${Pip_VERSION}")
+      endif()
+    endif()
+  endif()
+else()
+  set(Pip_FOUND FALSE)
+  if(ENABLE_AUTO_DOWNLOAD)
+    execute_process (
+      COMMAND "${Python_EXECUTABLE}" -m ensurepip --upgrade
+      RESULT_VARIABLE ENSUREPIP_RESULT
+    )
+    if (ENSUREPIP_RESULT EQUAL 0)
+      set(Pip_FOUND TRUE)
+    else()
+      message(${Pip_FIND_MODE} "Could NOT install pip for Python version "
+        "${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}")
+    endif()
+  else()
+    message(${Pip_FIND_MODE} "Could NOT find pip for Python version "
+      "${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}")
+  endif()
+endif()

cmake/FindRepairwheel.cmake

@@ -0,0 +1,83 @@
+###############################################################################
+# Top contributors (to current version):
+#   Daniel Larraz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2024 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 Repairwheel
+# Repairwheel_FOUND - system has the repairwheel executable
+# Repairwheel_EXECUTABLE - path to the repairwheel executable
+# Repairwheel_VERSION - repairwheel version
+##
+
+set(Python_SCRIPTS_Paths "")
+
+macro(add_scripts_path python_bin scheme)
+  execute_process(
+    COMMAND "${python_bin}" -c 
+      "import sysconfig; print(sysconfig.get_paths('${scheme}')['scripts'])"
+    RESULT_VARIABLE Python_SCRIPTS_RESULT
+    OUTPUT_VARIABLE Python_SCRIPTS
+    ERROR_QUIET
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+  )
+  if (NOT Python_SCRIPTS_RESULT AND Python_SCRIPTS)
+    list(APPEND Python_SCRIPTS_Paths ${Python_SCRIPTS})
+  endif()
+endmacro()
+
+# Look for repairwheel executable in Python "Scripts" directories
+add_scripts_path("${Python_EXECUTABLE}" "posix_prefix")
+add_scripts_path("${Python_BASE_EXECUTABLE}" "posix_user")
+add_scripts_path("${Python_BASE_EXECUTABLE}" "posix_prefix")
+if(WIN32)
+  add_scripts_path("${Python_EXECUTABLE}" "nt")
+  add_scripts_path("${Python_BASE_EXECUTABLE}" "nt_user")
+  add_scripts_path("${Python_BASE_EXECUTABLE}" "nt")
+endif()
+
+if (Repairwheel_FIND_REQUIRED)
+  set(Repairwheel_FIND_MODE FATAL_ERROR)
+else()
+  set(Repairwheel_FIND_MODE STATUS)
+endif()
+
+macro(find_repairwheel)
+  find_program(Repairwheel_EXECUTABLE repairwheel ${Python_SCRIPTS_Paths})
+  if(Repairwheel_EXECUTABLE)
+    execute_process(
+      COMMAND "${Repairwheel_EXECUTABLE}" --version
+      RESULT_VARIABLE Repairwheel_VERSION_CHECK_RESULT
+      OUTPUT_VARIABLE Repairwheel_VERSION
+    )
+    # Check we can run repairwheel successfully.
+    # Otherwise, reset path to executable.
+    if(NOT(Repairwheel_VERSION_CHECK_RESULT EQUAL 0))
+      set(Repairwheel_EXECUTABLE "")
+    endif()
+  endif()
+endmacro()
+
+find_repairwheel()
+
+if(NOT Repairwheel_EXECUTABLE AND ENABLE_AUTO_DOWNLOAD)
+  message(STATUS "Installing repairwheel")
+  execute_process(
+    COMMAND ${Python_EXECUTABLE} -m pip install repairwheel
+  )
+  find_repairwheel()
+endif()
+
+if(Repairwheel_EXECUTABLE)
+  set(Repairwheel_FOUND TRUE)
+  message(STATUS "Found repairwheel: ${Repairwheel_EXECUTABLE}")
+else()
+  set(Repairwheel_FOUND FALSE)
+  message(${Repairwheel_FIND_MODE} "Could NOT find repairwheel executable")
+endif()

contrib/get-alf-checker

@@ -24,7 +24,7 @@ ALFC_DIR="$BASE_DIR/alf-checker"
 mkdir -p $ALFC_DIR
 
 # download and unpack ALFC
-ALF_VERSION="da1903230c1d7cc5adbacb65d4eee602dcba93a0"
+ALF_VERSION="612c7ad99d3e3679c14f9f907d9ec490fea88914"
 download "https://github.com/cvc5/alfc/archive/$ALF_VERSION.tar.gz" $BASE_DIR/tmp/alfc.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/alfc.tgz -C $ALFC_DIR
 

docs/examples/uf.rst

@@ -0,0 +1,10 @@
+Theory of Uninterpreted Functions
+==================================
+
+
+.. api-examples::
+    <examples>/api/cpp/uf.cpp
+    <examples>/api/java/Uf.java
+    <examples>/api/python/pythonic/uf.py
+    <examples>/api/python/uf.py
+    <examples>/api/smtlib/uf.smt2

examples/api/cpp/CMakeLists.txt

@@ -31,6 +31,7 @@ set(CVC5_EXAMPLES_API
   transcendentals
   parser
   parser_sym_manager
+  uf
 )
 
 foreach(example ${CVC5_EXAMPLES_API})

examples/api/cpp/uf.cpp

@@ -0,0 +1,62 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 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.
+ * ****************************************************************************
+ *
+ * A simple demonstration of the capabilities of the cvc5 uf solver.
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+using namespace cvc5;
+
+int main()
+{
+  TermManager tm;
+  Solver slv(tm);
+  slv.setLogic("QF_UF");
+
+  // Sorts
+  Sort u = tm.mkUninterpretedSort("U");
+  Sort boolean = tm.getBooleanSort();
+  Sort uTou = tm.mkFunctionSort({u}, u);
+  Sort uPred = tm.mkFunctionSort({u}, boolean);
+
+  // Variables
+  Term x = tm.mkConst(u, "x");
+  Term y = tm.mkConst(u, "y");
+
+  // Functions
+  Term f = tm.mkConst(uTou, "f");
+  Term p = tm.mkConst(uPred, "p");
+
+  // Terms
+  Term f_x = tm.mkTerm(Kind::APPLY_UF, {f, x});
+  Term f_y = tm.mkTerm(Kind::APPLY_UF, {f, y});
+  Term p_f_x = tm.mkTerm(Kind::APPLY_UF, {p, f_x});
+  Term p_f_y = tm.mkTerm(Kind::APPLY_UF, {p, f_y});
+
+  // Construct the assertions
+  Term assertions =
+      tm.mkTerm(Kind::AND,
+                {
+                    tm.mkTerm(Kind::EQUAL, {x, f_x}),  
+                    tm.mkTerm(Kind::EQUAL, {y, f_y}),
+                    p_f_x.notTerm(),
+                    p_f_y
+                });
+  slv.assertFormula(assertions);
+
+  std::cout << slv.checkSat()  << std::endl;
+
+  return 0;
+}

examples/api/java/CMakeLists.txt

@@ -34,6 +34,7 @@ set(EXAMPLES_API_JAVA
    SygusInv
    Transcendentals
    UnsatCores
+   Uf
 )
 
 function(add_java_example example)