diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md index 0df44e807e3..2826db51517 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -17,7 +17,7 @@ A clear and concise description of what the bug is. **Operating system**: Name/version of the operating system. **`configure.sh` options** -Paste `configure.sh` here. +Paste the options passed to `configure.sh` here. **`configure.sh` output** Paste the output of `configure.sh` here. diff --git a/.github/actions/add-jar/action.yml b/.github/actions/add-jar/action.yml new file mode 100644 index 00000000000..c22f4d62b76 --- /dev/null +++ b/.github/actions/add-jar/action.yml @@ -0,0 +1,82 @@ +name: Add self-contained JAR with the cvc5 Java bindings +description: | + Creates a JAR that includes the cvc5 Java bindings + along with the necessary native libraries. +inputs: + install-path: + description: path to the directory with installed artifacts + jar-libs-dir: + description: name of the directory that will contain the libraries within the JAR + jar-name: + description: target name of the JAR + github-token-latest: + description: token to upload JAR to latest + github-token-release: + description: token to upload JAR to release + shell: + default: bash +runs: + using: composite + steps: + - name: Create JAR contents (Linux) + if: runner.os == 'Linux' + shell: ${{ inputs.shell }} + run: | + echo "::group::Create JAR contents (Linux)" + mkdir ${{ inputs.jar-libs-dir }} + cd ${{ inputs.jar-libs-dir }} + cp ${{ inputs.install-path }}/lib/libcvc5jni.so . + echo "::endgroup::" + + - name: Create JAR contents (macOS) + if: runner.os == 'macOS' + shell: ${{ inputs.shell }} + run: | + echo "::group::Create JAR contents (macOS)" + mkdir ${{ inputs.jar-libs-dir }} + cd ${{ inputs.jar-libs-dir }} + cp ${{ inputs.install-path }}/lib/libcvc5jni.dylib . + echo "::endgroup::" + + - name: Create JAR contents (Windows) + if: runner.os == 'Windows' + shell: ${{ inputs.shell }} + run: | + echo "::group::Create JAR contents (Windows)" + mkdir ${{ inputs.jar-libs-dir }} + cd ${{ inputs.jar-libs-dir }} + cp ${{ inputs.install-path }}/bin/cvc5jni.dll . + echo "::endgroup::" + + - name: Create JAR + shell: ${{ inputs.shell }} + run: | + echo "::group::Create JAR" + unzip ${{ inputs.install-path }}/share/java/cvc5.jar + jar cf ${{ inputs.jar-name }}.jar AUTHORS COPYING licenses io ${{ inputs.jar-libs-dir }} + echo "::endgroup::" + + - name: Test JAR + shell: ${{ inputs.shell }} + run: | + javac -cp "${{ inputs.jar-name }}.jar" ./examples/api/java/QuickStart.java -d . + if [[ "$RUNNER_OS" == "Windows" ]]; then + java -cp "${{ inputs.jar-name }}.jar;." QuickStart + else + java -cp "${{ inputs.jar-name }}.jar:." QuickStart + fi + rm QuickStart.class + + - name: Store to latest + if: github.ref == 'refs/heads/main' + uses: ./.github/actions/store-to-latest + with: + asset-filename: ${{ inputs.jar-name }}.jar + github-token: ${{ inputs.github-token-latest }} + + - name: Store to release + if: startsWith(github.ref, 'refs/tags/') + uses: ./.github/actions/store-to-release + with: + asset-filename: ${{ inputs.jar-name }}.jar + github-token: ${{ inputs.github-token-release }} diff --git a/.github/actions/add-package/action.yml b/.github/actions/add-package/action.yml index a25665f9990..dcb0d16d52b 100644 --- a/.github/actions/add-package/action.yml +++ b/.github/actions/add-package/action.yml @@ -11,10 +11,15 @@ inputs: description: token to upload package to release shell: default: bash +outputs: + install-path: + description: path to the installation directory + value: ${{ steps.create-zip.outputs.install-path }} runs: using: composite steps: - name: Create ZIP file + id: create-zip shell: ${{ inputs.shell }} run: | echo "::group::Create ZIP file" @@ -27,14 +32,26 @@ runs: # They are built for testing purposes, but # only work for the specific CI Python version. rm -rf ${{ inputs.build-dir }}/install/lib/python* - - # Copy COPYING file and licenses directory to install directory - cp COPYING ${{ inputs.build-dir }}/install/ + rm -rf ${{ inputs.build-dir }}/install/lib/site-packages + + if [[ "$RUNNER_OS" == "Windows" ]]; then + if [ -f ${{ inputs.build-dir }}/install/bin/libcvc5.dll ]; then + cp /mingw64/bin/libgcc_s_seh-1.dll ${{ inputs.build-dir }}/install/bin/ + cp /mingw64/bin/libstdc++-6.dll ${{ inputs.build-dir }}/install/bin/ + cp /mingw64/bin/libwinpthread-1.dll ${{ inputs.build-dir }}/install/bin/ + else + cp /mingw64/lib/libgmp.a ${{ inputs.build-dir }}/install/lib/ + fi + fi + + # Copy AUTHORS and COPYING files and licenses directory to install directory + cp AUTHORS COPYING ${{ inputs.build-dir }}/install/ cp -r licenses ${{ inputs.build-dir }}/install/ # Create ZIP file pushd ${{ inputs.build-dir }} mv install ${{ inputs.package-name }} + echo "install-path=${{ inputs.build-dir }}/${{ inputs.package-name }}" >> $GITHUB_OUTPUT zip -r ${{ inputs.package-name }} ${{ inputs.package-name }} popd @@ -42,7 +59,7 @@ runs: mv ${{ inputs.build-dir }}/${{ inputs.package-name }}.zip . echo "::endgroup::" - - name: install pyGithub + - name: Install pyGithub shell: ${{ inputs.shell }} run: | # Upgrading pyopenssl resolves the following error: @@ -53,82 +70,14 @@ runs: - name: Store to latest if: github.ref == 'refs/heads/main' - shell: 'python3 {0}' - env: - GITHUB_TOKEN: ${{ inputs.github-token-latest }} - PACKAGE: ${{ inputs.package-name }}.zip - run: | - import datetime - import os - from github import Github - - sha = os.getenv('GITHUB_SHA') - - gh = Github(os.getenv('GITHUB_TOKEN')) - repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY')) - - try: - ref = repo.get_git_ref('tags/latest') - # update "latest" to current commit if sha changed - if ref.object.sha != sha: - ref.edit(sha) - except: - print('tag `latest` does not exist.') - exit - - try: - rel = repo.get_release('latest') - except: - print('New `latest` release') - rel = repo.create_git_release('latest', 'latest', 'Latest builds') - - # generate new filename - package = os.getenv('PACKAGE') - name,ext = os.path.splitext(package) - curtime = repo.get_git_commit(sha).committer.date.strftime('%Y-%m-%d') - samedayprefix = '{}-{}-'.format(name, curtime) - filename = '{}-{}-{}{}'.format(name, curtime, sha[:7], ext) - - # prune old commits - assets = list(rel.get_assets()) - assets.sort(key=lambda x: x.created_at, reverse=True) - - for cnt,asset in enumerate(assets): - delete = False - # We generate 10 artifacts per build: - # {Linux, Linux-arm64, macOS, macOS-arm64, Windows} * {static, shared} - if cnt >= 20: # Keep at most 2 builds - delete = True - if asset.name.startswith(samedayprefix): - delete = True - # convert to timezone-aware datetime - age = datetime.datetime.now().replace(tzinfo=datetime.timezone.utc) - asset.created_at - if age.days > 7: - delete = True - if delete: - asset.delete_asset() - - # upload as asset with proper name - rel.upload_asset(package, name=filename) + uses: ./.github/actions/store-to-latest + with: + asset-filename: ${{ inputs.package-name }}.zip + github-token: ${{ inputs.github-token-latest }} - name: Store to release if: startsWith(github.ref, 'refs/tags/') - shell: 'python3 {0}' - env: - GITHUB_TOKEN: ${{ inputs.github-token-release }} - PACKAGE: ${{ inputs.package-name }}.zip - run: | - import os - from github import Github - - refname = os.getenv('GITHUB_REF_NAME') - gh = Github(os.getenv('GITHUB_TOKEN')) - repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY')) - try: - rel = repo.get_release(refname) - except: - print("New release from " + refname) - ref = repo.get_git_ref('tags/' + refname) - commit = repo.get_git_commit(ref.object.sha) - rel = repo.create_git_release(refname, refname, commit.message) - rel.upload_asset(os.getenv('PACKAGE')) + uses: ./.github/actions/store-to-release + with: + asset-filename: ${{ inputs.package-name }}.zip + github-token: ${{ inputs.github-token-release }} diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml index b4431185e50..995fd7d934b 100644 --- a/.github/actions/configure-and-build/action.yml +++ b/.github/actions/configure-and-build/action.yml @@ -45,12 +45,7 @@ runs: -DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache cd build-shared/ && pwd=$(pwd) - if [[ "$RUNNER_OS" == "Windows" ]]; then - ccache --set-config="base_dir=$pwd" - else - # can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10 - $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH - fi + ccache --set-config="base_dir=$pwd" make -j${{ env.num_proc }} @@ -66,16 +61,11 @@ runs: run: | echo "::group::Static build" ${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \ - --prefix=$(pwd)/build-static/install --werror --static --name=build-static --no-java-bindings \ + --prefix=$(pwd)/build-static/install --werror --static --name=build-static \ -DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache cd build-static/ && pwd=$(pwd) - if [[ "$RUNNER_OS" == "Windows" ]]; then - ccache --set-config="base_dir=$pwd" - else - # can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10 - $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH - fi + ccache --set-config="base_dir=$pwd" make -j${{ env.num_proc }} @@ -90,11 +80,7 @@ runs: shell: ${{ inputs.shell }} run: | echo "::group::Reset ccache base_dir" - if [[ "$RUNNER_OS" == "Windows" ]]; then - ccache --set-config="base_dir=" - else - $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir =" $CCACHE_CONFIGPATH - fi + ccache --set-config="base_dir=" echo "::endgroup::" - name: ccache Statistics diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml index 2eb92d29c37..efd1958b282 100644 --- a/.github/actions/install-dependencies/action.yml +++ b/.github/actions/install-dependencies/action.yml @@ -6,8 +6,12 @@ inputs: windows-build: default: false type: boolean + wasm-build: + default: false + type: boolean shell: default: bash + runs: using: composite steps: @@ -27,7 +31,6 @@ runs: libtinfo-dev \ libfl-dev echo "SED=sed" >> $GITHUB_ENV - echo "CCACHE_CONFIGPATH=/home/runner/.ccache/ccache.conf" >> $GITHUB_ENV echo "::endgroup::" - name: Install software for cross-compiling for arm64 Linux @@ -57,6 +60,21 @@ runs: sudo update-alternatives --set x86_64-w64-mingw32-g++ /usr/bin/x86_64-w64-mingw32-g++-posix echo "::endgroup::" + - name: Install software for WebAssembly compilation + # Boolean inputs are actually strings: + # https://github.com/actions/runner/issues/1483 + if: inputs.wasm-build == 'true' + shell: bash + run: | + echo "::group::Install software for WebAssembly compilation" + sudo apt-get update + git clone https://github.com/emscripten-core/emsdk.git + cd emsdk/ + ./emsdk install '3.1.18' + ./emsdk activate '3.1.18' + echo "$(pwd)" >> $GITHUB_PATH + echo "$(pwd)/upstream/emscripten" >> $GITHUB_PATH + - name: Install Windows software if: runner.os == 'Windows' && inputs.windows-build == 'true' uses: msys2/setup-msys2@v2 @@ -66,6 +84,7 @@ runs: path-type: inherit install: | make + mingw-w64-x86_64-autotools mingw-w64-x86_64-ccache mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc @@ -89,13 +108,14 @@ runs: brew config brew untap homebrew/core homebrew/cask brew config - - brew install \ + if [[ $RUNNER_ARCH == "ARM64" ]]; then + AUTOTOOLS="autoconf libtool" + fi + brew install $AUTOTOOLS \ + automake \ ccache \ - pkgconfig \ gnu-sed echo "SED=gsed" >> $GITHUB_ENV - echo "CCACHE_CONFIGPATH=/Users/runner/Library/Preferences/ccache/ccache.conf" >> $GITHUB_ENV echo "num_proc=$(( $(sysctl -n hw.logicalcpu) + 1 ))" >> $GITHUB_ENV echo "::endgroup::" @@ -109,6 +129,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 }} @@ -118,5 +146,5 @@ runs: python3 -m pip install \ sphinx==7.1.2 \ sphinxcontrib-bibtex==2.5.0 sphinx-tabs==3.4.1 sphinx-rtd-theme==1.3.0 breathe==4.35.0 \ - sphinxcontrib-programoutput==0.17 + sphinxcontrib-programoutput==0.17 sphinxcontrib-googleanalytics==0.4 echo "::endgroup::" diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index fc708b7b829..f81546506ec 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -46,7 +46,12 @@ runs: shell: ${{ inputs.shell }} run: | if [[ "${{ inputs.check-python-bindings }}" != "true" ]]; then exit 0; fi - export PYTHONPATH="$PYTHONPATH:$(dirname $(dirname $(find ${{ inputs.build-dir }}/install -name 'cvc5_python_base*')))" + PYTHON_MODULE_PATH="$(dirname $(dirname $(find ${{ inputs.build-dir }}/install -name 'cvc5_python_base*')))" + if [[ "$RUNNER_OS" == "Windows" ]]; then + export PYTHONPATH="$PYTHONPATH;$(cygpath -w $PYTHON_MODULE_PATH)" + else + export PYTHONPATH="$PYTHONPATH:$PYTHON_MODULE_PATH" + fi python3 -c "import cvc5" - name: Check Examples @@ -59,6 +64,8 @@ runs: export PATH="${{ inputs.build-dir }}/install/bin:$PATH" export CMAKE_GENERATOR="MSYS Makefiles" fi + export CFLAGS=-Werror + export CXXFLAGS=-Werror cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake \ -DPython_EXECUTABLE=$(command -v python3) make -j${{ env.num_proc }} diff --git a/.github/actions/setup-cache/action.yml b/.github/actions/setup-cache/action.yml index 44d58856410..0e65634ce68 100644 --- a/.github/actions/setup-cache/action.yml +++ b/.github/actions/setup-cache/action.yml @@ -3,6 +3,10 @@ description: Setup caches (ccache, contribs and dependencies) inputs: cache-key: default: "none" + install-ethos: + default: false + install-carcara: + default: false shell: default: bash @@ -60,7 +64,14 @@ runs: - name: Install contrib dependencies if: steps.contrib-cache.outputs.cache-hit != 'true' shell: ${{ inputs.shell }} - run: ./contrib/get-alf-checker + run: | + mkdir -p ./deps/bin + if [ "${{ inputs.install-carcara }}" = "true" ]; then + ./contrib/get-carcara-checker + fi + if [ "${{ inputs.install-ethos }}" = "true" ]; then + ./contrib/get-ethos-checker + fi - name: Setup dependencies cache uses: actions/cache@v4 @@ -69,4 +80,3 @@ runs: build-shared/deps build-static/deps key: ${{ inputs.cache-key }}-${{ runner.os }}-deps-${{ hashFiles('cmake/**') }}-${{ hashFiles('.github/**') }} - diff --git a/.github/actions/setup-cmake/action.yml b/.github/actions/setup-cmake/action.yml new file mode 100644 index 00000000000..e6e3c97eb0c --- /dev/null +++ b/.github/actions/setup-cmake/action.yml @@ -0,0 +1,25 @@ +name: Setup CMake +description: Find the minimum required CMake version and set it up +inputs: + shell: + default: bash + +runs: + using: composite + steps: + - name: Find minimum required CMake version + id: cmake + shell: ${{ inputs.shell }} + run: | + echo "::group::Get minimum required CMake version" + echo "version=$( \ + grep "cmake_minimum_required" CMakeLists.txt | \ + awk -F'[()]' '{print $2}' | \ + awk '{print $2}' \ + )" >> "$GITHUB_OUTPUT" + echo "::endgroup::" + + - name: Setup CMake + uses: jwlawson/actions-setup-cmake@v2 + with: + cmake-version: '${{ steps.cmake.outputs.version }}.x' diff --git a/.github/actions/store-to-latest/action.yml b/.github/actions/store-to-latest/action.yml new file mode 100644 index 00000000000..e254f228e54 --- /dev/null +++ b/.github/actions/store-to-latest/action.yml @@ -0,0 +1,70 @@ +name: Store to latest +description: Store an asset on the release page associated to the latest tag +inputs: + asset-filename: + description: filename of the asset + github-token: + description: token to upload asset to latest + +runs: + using: composite + steps: + - name: Store to latest + shell: 'python3 {0}' + env: + GITHUB_TOKEN: ${{ inputs.github-token }} + PACKAGE: ${{ inputs.asset-filename }} + run: | + import datetime + import os + from github import Github + + sha = os.getenv('GITHUB_SHA') + + gh = Github(os.getenv('GITHUB_TOKEN')) + repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY')) + + try: + ref = repo.get_git_ref('tags/latest') + # update "latest" to current commit if sha changed + if ref.object.sha != sha: + ref.edit(sha) + except: + print('tag `latest` does not exist.') + exit + + try: + rel = repo.get_release('latest') + except: + print('New `latest` release') + rel = repo.create_git_release('latest', 'latest', 'Latest builds') + + # generate new filename + package = os.getenv('PACKAGE') + name,ext = os.path.splitext(package) + curtime = repo.get_git_commit(sha).committer.date.strftime('%Y-%m-%d') + samedayprefix = '{}-{}-'.format(name, curtime) + filename = '{}-{}-{}{}'.format(name, curtime, sha[:7], ext) + + # prune old commits + assets = list(rel.get_assets()) + assets.sort(key=lambda x: x.created_at, reverse=True) + + for cnt,asset in enumerate(assets): + delete = False + # We generate 10 packages per build: + # {Linux-x86_64, Linux-arm64, macOS-x86_64, macOS-arm64, Win64-x86_64} * {static, shared} + # and 5 JARS {Linux-x86_64, Linux-arm64, macOS-x86_64, macOS-arm64, Win64-x86_64} + if cnt >= 30: # Keep at most 2 builds + delete = True + if asset.name.startswith(samedayprefix): + delete = True + # convert to timezone-aware datetime + age = datetime.datetime.now().replace(tzinfo=datetime.timezone.utc) - asset.created_at + if age.days > 7: + delete = True + if delete: + asset.delete_asset() + + # upload as asset with proper name + rel.upload_asset(package, name=filename) diff --git a/.github/actions/store-to-release/action.yml b/.github/actions/store-to-release/action.yml new file mode 100644 index 00000000000..af98727be04 --- /dev/null +++ b/.github/actions/store-to-release/action.yml @@ -0,0 +1,31 @@ +name: Store to release +description: Store an asset on the release page associated to current release +inputs: + asset-filename: + description: filename of the asset + github-token: + description: token to upload asset to current release + +runs: + using: composite + steps: + - name: Store to release + shell: 'python3 {0}' + env: + GITHUB_TOKEN: ${{ inputs.github-token }} + PACKAGE: ${{ inputs.asset-filename }} + run: | + import os + from github import Github + + refname = os.getenv('GITHUB_REF_NAME') + gh = Github(os.getenv('GITHUB_TOKEN')) + repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY')) + try: + rel = repo.get_release(refname) + except: + print("New release from " + refname) + ref = repo.get_git_ref('tags/' + refname) + commit = repo.get_git_commit(ref.object.sha) + rel = repo.create_git_release(refname, refname, commit.message) + rel.upload_asset(os.getenv('PACKAGE')) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml deleted file mode 100644 index 7190936a7af..00000000000 --- a/.github/workflows/ci.yml +++ /dev/null @@ -1,209 +0,0 @@ -on: [push, pull_request] -name: CI - -# Prevents github from relying on clones of homebrew-core or homebrew-cask. -# https://github.com/orgs/Homebrew/discussions/4612 -env: - HOMEBREW_NO_INSTALL_FROM_API: "" - -jobs: - build: - strategy: - matrix: - include: - - name: ubuntu:production - os: ubuntu-20.04 - config: production --auto-download --all-bindings --editline --docs - cache-key: production - strip-bin: strip - python-bindings: true - build-documentation: true - check-examples: true - package-name: cvc5-Linux - exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - - - name: ubuntu:production-arm64-cross - os: ubuntu-latest - config: production --auto-download --arm64 - cache-key: production-arm64-cross - strip-bin: aarch64-linux-gnu-strip - package-name: cvc5-Linux-arm64 - - - name: macos:production - os: macos-13 - config: production --auto-download --all-bindings --editline -DBUILD_GMP=1 - cache-key: production - strip-bin: strip - python-bindings: true - check-examples: true - package-name: cvc5-macOS - macos-target: 10.13 - exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - - - name: macos:production-arm64 - os: macos-14 - config: production --auto-download --all-bindings --editline -DBUILD_GMP=1 - cache-key: production-arm64 - strip-bin: strip - python-bindings: true - check-examples: true - package-name: cvc5-macOS-arm64 - macos-target: 11.0 - exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - - - name: macos:production-arm64-cross - os: macos-13 - config: production --auto-download --all-bindings --editline --arm64 - cache-key: production-arm64-cross - strip-bin: strip - python-bindings: true - - - name: win64:production - os: windows-latest - config: production --auto-download --java-bindings - cache-key: production-win64-native - strip-bin: strip - windows-build: true - shell: 'msys2 {0}' - check-examples: true - package-name: cvc5-Win64 - exclude_regress: 1-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - - - name: win64:production-cross - os: ubuntu-latest - config: production --auto-download --win64 - cache-key: production-win64-cross - strip-bin: x86_64-w64-mingw32-strip - windows-build: true - - - name: ubuntu:production-clang - os: ubuntu-20.04 - env: CC=clang CXX=clang++ - config: production --auto-download --no-poly - cache-key: productionclang - check-examples: true - exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - - - name: ubuntu:production-dbg - os: ubuntu-20.04 - config: production --auto-download --assertions --tracing --unit-testing --all-bindings --editline --cocoa - cache-key: dbg - exclude_regress: 3-4 - run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump - python-bindings: true - - - name: ubuntu:production-dbg-clang - os: ubuntu-20.04 - env: CC=clang CXX=clang++ - config: production --auto-download --assertions --tracing --cln --gpl - cache-key: dbgclang - exclude_regress: 3-4 - run_regression_args: --tester alf --tester base --tester model --tester synth --tester abduct --tester unsat-core --tester dump - - name: ${{ matrix.name }} - runs-on: ${{ matrix.os }} - - # cancel already running jobs for the same branch/pr/tag - concurrency: - group: build-${{ github.ref }}-${{ matrix.name }}-${{ github.ref != 'refs/heads/main' || github.run_id }} - cancel-in-progress: ${{ github.repository != 'cvc5/cvc5' || startsWith(github.ref, 'refs/pull/') }} - - steps: - - - uses: actions/checkout@v4 - - - name: Install dependencies - uses: ./.github/actions/install-dependencies - with: - with-documentation: ${{ matrix.build-documentation }} - windows-build: ${{ matrix.windows-build }} - shell: ${{ matrix.shell }} - - - name: Setup caches - uses: ./.github/actions/setup-cache - with: - cache-key: ${{ matrix.cache-key }} - shell: ${{ matrix.shell }} - - - name: Configure and build - id: configure-and-build - uses: ./.github/actions/configure-and-build - with: - configure-env: ${{ matrix.env }} - configure-config: ${{ matrix.config }} - macos-target: ${{ matrix.macos-target }} - build-shared: ${{ matrix.build-shared }} - build-static: ${{ matrix.build-static }} - strip-bin: ${{ matrix.strip-bin }} - shell: ${{ matrix.shell }} - - - name: Run tests - if: matrix.run_regression_args - uses: ./.github/actions/run-tests - with: - build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} - check-examples: ${{ matrix.check-examples }} - check-python-bindings: ${{ matrix.python-bindings }} - regressions-args: ${{ matrix.run_regression_args }} - regressions-exclude: ${{ matrix.exclude_regress }} - shell: ${{ matrix.shell }} - - - name: Run tests - if: matrix.run_regression_args - uses: ./.github/actions/run-tests - with: - build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} - check-examples: false - check-install: false - check-python-bindings: false - regressions-args: ${{ matrix.run_regression_args }} - regressions-exclude: 1-4 - shell: ${{ matrix.shell }} - - - name: Build documentation - if: matrix.build-documentation - uses: ./.github/actions/build-documentation - with: - build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} - - - name: Create and add shared package to latest and release - if: matrix.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) - uses: ./.github/actions/add-package - with: - build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} - package-name: ${{ matrix.package-name }}-shared - # when using GITHUB_TOKEN, no further workflows are triggered - github-token-latest: ${{ secrets.GITHUB_TOKEN }} - github-token-release: ${{ secrets.ACTION_USER_TOKEN }} - shell: ${{ matrix.shell }} - - - name: Create and add static package to latest and release - if: matrix.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) - uses: ./.github/actions/add-package - with: - build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} - package-name: ${{ matrix.package-name }}-static - # when using GITHUB_TOKEN, no further workflows are triggered - 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/update-pr-branch@v0.7.2 - with: - token: ${{ secrets.ACTION_USER_TOKEN }} - base: 'main' - sort: 'created' - direction: 'asc' - required_approval_count: 1 diff --git a/.github/workflows/cmake-version.yml b/.github/workflows/cmake-version.yml deleted file mode 100644 index e9abaf744cb..00000000000 --- a/.github/workflows/cmake-version.yml +++ /dev/null @@ -1,65 +0,0 @@ -on: [workflow_dispatch] -name: cmake-version - -jobs: - build: - continue-on-error: true - name: ubuntu:production-dbg - runs-on: ubuntu-latest - strategy: - matrix: - cmake_version: [ - "3.8", "3.9", "3.10", "3.11", "3.12", "3.13", "3.14", "3.15", "3.16", - "3.17", "3.18", "3.19", "3.20", "3.21" - ] - - steps: - - name: Setup cmake - uses: jwlawson/actions-setup-cmake@v1.9 - with: - cmake-version: ${{ matrix.cmake_version }} - - - uses: actions/checkout@v2 - - - name: Adapt cmake version checks - run: | - sed -i'orig' -E 's/cmake_minimum_required\(VERSION [0-9.]+\)/cmake_minimum_required(VERSION ${{ matrix.cmake_version }})/' CMakeLists.txt - - - name: Install dependencies - uses: ./.github/actions/install-dependencies - with: - with-documentation: true - - - name: Setup caches - uses: ./.github/actions/setup-cache - with: - cache-key: cmake - - - name: Configure - run: | - ./configure.sh production --auto-download --static --python-bindings --assertions --tracing --unit-testing --editline --docs \ - --prefix=$(pwd)/build/install \ - --werror - - - name: Build - run: make -j${{ env.num_proc }} - working-directory: build - - - name: ccache Statistics - run: ccache -s - - - name: Run tests - uses: ./.github/actions/run-tests - with: - check-examples: true - check-python-bindings: true - check-unit-tests: true - - - name: Build Documentation - run: | - make -j${{ env.num_proc }} docs-gh - if [ "${{ github.event_name }}" == "pull_request" ] ; then - echo "${{ github.event.number }}" > docs/sphinx-gh/prnum - fi - working-directory: build - diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml deleted file mode 100644 index d6545473a28..00000000000 --- a/.github/workflows/docs_cleanup.yml +++ /dev/null @@ -1,78 +0,0 @@ -name: documentation cleanup -on: - schedule: - - cron: '0 1 * * *' - -jobs: - docs-cleanup: - runs-on: ubuntu-latest - if: github.repository == 'cvc5/cvc5' - steps: - - name: Install Packages - run: | - sudo apt-get update - sudo apt-get install -y python3 python3-jinja2 - - - name: Setup Deploy Key - env: - SSH_AUTH_SOCK: /tmp/ssh_agent.sock - run: | - ssh-agent -a $SSH_AUTH_SOCK > /dev/null - ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}" - - - name: Clone docs repo - env: - SSH_AUTH_SOCK: /tmp/ssh_agent.sock - run: | - git config --global user.email "docbot@cvc5" - git config --global user.name "DocBot" - git clone git@github.com:cvc5/docs-ci.git target/ - - - name: Remove stale docs - run: | - cd target - for file in `find ./ -maxdepth 1 -name "docs-*"`; do - mod=`git log -1 HEAD --pretty="%ai" $file` - touch -d "$mod" $file - done - find ./ -maxdepth 1 -name "docs-*" -mtime +7 -exec git rm -r {} + - find ./ -maxdepth 1 -name "docs-*" -xtype l -exec git rm {} + - git commit -m "Prune docs" || echo "Nothing to prune" - - - name: Squash old commits - env: - SSH_AUTH_SOCK: /tmp/ssh_agent.sock - run: | - cd target - first=`git rev-list --max-parents=0 HEAD` - cutoff=`date -d "-1 month" +%Y-%m-%d` - last=`git log --pretty='%as %H' | awk -v cutoff=$cutoff '$1 < cutoff { print $2 }' | head -n1` - if [ -n "$last" ]; then - git checkout $last - ts=`git log -1 --format=%ct` - git reset --soft $first - if git diff --cached --exit-code - then - echo "Nothing to squash" - else - git commit -m "Squash old history" --date=$ts - fi - git cherry-pick $last..main - fi - - - name: Push - env: - SSH_AUTH_SOCK: /tmp/ssh_agent.sock - run: | - cd target - - python3 genindex.py - git add README.md - if git diff --cached --exit-code - then - echo "Nothing changed" - else - git commit -m "Update README.md" - fi - - git push -f origin HEAD:main diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml deleted file mode 100644 index 5ad1900add5..00000000000 --- a/.github/workflows/docs_upload.yml +++ /dev/null @@ -1,154 +0,0 @@ -name: Upload Docs - -on: - workflow_run: - workflows: ["CI"] - types: - - completed - -jobs: - upload-docs: - name: upload-docs - runs-on: ubuntu-latest - continue-on-error: true - if: github.repository == 'cvc5/cvc5' && github.event.workflow_run.conclusion == 'success' - steps: - - name: Setup git config - run: | - git config --global user.email "docbot@cvc5" - git config --global user.name "DocBot" - - - name: Download artifact - uses: actions/github-script@v7 - with: - script: | - var artifacts = await github.rest.actions.listWorkflowRunArtifacts({ - owner: context.repo.owner, - repo: context.repo.repo, - run_id: ${{github.event.workflow_run.id }}, - }); - var matchArtifact = artifacts.data.artifacts.filter((artifact) => { - return artifact.name == "documentation" - })[0]; - var download = await github.rest.actions.downloadArtifact({ - owner: context.repo.owner, - repo: context.repo.repo, - artifact_id: matchArtifact.id, - archive_format: 'zip', - }); - var fs = require('fs'); - fs.writeFileSync('${{github.workspace}}/download.zip', Buffer.from(download.data)); - - - name: Unpack artifact - run: unzip download.zip -d docs-new/ - - - name: Check for broken links - continue-on-error: true - run: | - python3 -m pip install linkchecker - linkchecker --check-extern docs-new/index.html - -# This workflow is run for commits in PRs (from branches in forks), commits -# (from branches in main repo, usually main branch) and tags. Unfortunately, -# there are only two properties in the github context that can be used here: -# - workflow_run.event is "pull_request" for PRs and "push" otherwise -# - workflow_run.head_branch contains the branch or tag name -# We can not reliably identify a tag from that, so we simply match the -# head_branch against the naming pattern of our tags ("cvc5-*"). To prevent PRs -# with a matching branch name to be recognized as tags, we proceed as follows: -# - handle PRs (event == "pull_request") -# - handle tags (head_branch == "cvc5-*") -# - rest are regular commits - - name: Setup Context - run: | - HASH=${{ github.event.workflow_run.head_commit.id }} - ISRELEASE=false - if [ "${{ github.event.workflow_run.event }}" == "pull_request" ] ; then - NAME=$(cat docs-new/prnum) - rm docs-new/prnum - echo "Identified PR #$NAME (from $HASH)" - NAME="pr$NAME" - elif [ "${{ startsWith(github.event.workflow_run.head_branch, 'cvc5-') }}" == "true" ] ; then - ISRELEASE=true - NAME=${{ github.event.workflow_run.head_branch }} - echo "Identified tag $NAME" - elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then - NAME=${{ github.event.workflow_run.head_branch }} - echo "Identified branch $NAME" - fi - echo "NAME=$NAME" >> $GITHUB_ENV - echo "HASH=$HASH" >> $GITHUB_ENV - echo "ISRELEASE=$ISRELEASE" >> $GITHUB_ENV - - - name: Update versions - continue-on-error: true - run: | - python3 -m pip install beautifulsoup4 lxml - - eval $(ssh-agent -s) - ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}" - - git clone git@github.com:cvc5/docs.git target-releases/ - - TARGET_DIR= - if [ "$ISRELEASE" = true ]; then - TARGET_DIR=target-releases/$NAME - else - TARGET_DIR=target-releases/cvc5-main - fi - cp -r docs-new "${TARGET_DIR}" - pushd target-releases/ - python3 genversions.py - popd - cp -rf "${TARGET_DIR}" docs-new - - - name: Update docs - continue-on-error: true - run: | - if [ -n "$NAME" ]; then - eval $(ssh-agent -s) - ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}" - - git clone git@github.com:cvc5/docs-ci.git target/ - cp -r docs-new target/docs-$NAME-$HASH - cd target/ - - isdiff=$(diff -r -x "*.zip" docs-main/ docs-$NAME-$HASH >&2; echo $?; exit 0) - - if [[ ("$ISRELEASE" != true) && ($isdiff = 0) ]] - then - echo "Ignored run, documentation is the same as for current main" - else - rm -f docs-$NAME - ln -s docs-$NAME-$HASH docs-$NAME - git add docs-$NAME docs-$NAME-$HASH - - python3 genindex.py - git add README.md - git commit -m "Update docs for $NAME" - - git push - fi - else - echo "Ignored run" - fi - - - name: Update docs for release - continue-on-error: true - run: | - if [ "$ISRELEASE" = true ]; then - eval $(ssh-agent -s) - ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}" - - cd target-releases/ - - rm -f latest - ln -s $NAME latest - - git add . - - git commit -m "Update docs for $NAME" - git push - else - echo "Ignored run" - fi diff --git a/.github/workflows/package_pypi.yml b/.github/workflows/package_pypi.yml deleted file mode 100644 index 2ea203e8e5a..00000000000 --- a/.github/workflows/package_pypi.yml +++ /dev/null @@ -1,140 +0,0 @@ -on: - release: - types: [published] - schedule: - - cron: '0 1 * * *' - workflow_dispatch: - -name: PyPi packaging - -jobs: - build_wheels: - name: Build wheels for ${{ matrix.name }} - runs-on: ${{ matrix.os }} - if: (github.repository == 'cvc5/cvc5') || (github.event_name != 'schedule') - strategy: - matrix: - include: - - name: manylinux-x86_64 - os: ubuntu-latest - arch: x86_64 - shell: bash - - name: manylinux-aarch64 - os: ubuntu-latest - arch: aarch64 - shell: bash - - name: macos-x86_64 - os: macos-13 - macos-target: 10.13 - shell: bash - - name: macos-arm64 - os: macos-14 - macos-target: 11 - shell: bash - - name: windows-x86_64 - os: windows-latest - shell: 'msys2 {0}' - defaults: - run: - shell: ${{ matrix.shell }} - - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - # Required by PEP-668 - - name: Set up Python virtual environment - if: runner.os == 'macOS' - run: | - python3 -m venv ~/.venv - echo "$HOME/.venv/bin" >> $GITHUB_PATH - - # cibuildwheel only supports arm64 Linux wheels through emulation. - # It works fine, but it is slow. Cross-compilation is not supported yet, - # see: https://github.com/pypa/cibuildwheel/issues/598 - - name: Set up QEMU for arm64 Linux builds - if: runner.os == 'Linux' && matrix.arch == 'aarch64' - uses: docker/setup-qemu-action@v3 - with: - platforms: "linux/arm64" - - - uses: msys2/setup-msys2@v2 - if: runner.os == 'Windows' - with: - msystem: mingw64 - path-type: inherit - install: | - make - mingw-w64-x86_64-cmake - mingw-w64-x86_64-gcc - mingw-w64-x86_64-gmp - - # cibuildwheel requires pyproject.toml to be present from the beginning - - name: Create pyproject.toml - run: | - echo "::group::Create pyproject.toml" - mkdir -p build/src/api/python - cp src/api/python/pyproject.toml build/src/api/python/ - echo "::endgroup::" - - - name: Store MinGW64 path - if: runner.os == 'Windows' - id: mingw64-path - shell: msys2 {0} - run: echo "bin=$(cygpath -m $(dirname $(which gcc)))" >> $GITHUB_OUTPUT - - - name: Build wheels - uses: pypa/cibuildwheel@v2.17.0 - with: - package-dir: ./build/src/api/python/ - env: - CIBW_SKIP: "cp36-* pp*-win* *-win32 *-manylinux_i686 *-musllinux_*" - CIBW_ARCHS_LINUX: "${{ matrix.arch }}" - CIBW_BEFORE_ALL_LINUX: bash ./contrib/cibw/before_all_linux.sh - CIBW_BEFORE_ALL_MACOS: bash ./contrib/cibw/before_all_macos.sh - CIBW_BEFORE_ALL_WINDOWS: msys2 -c ./contrib/cibw/before_all_windows.sh - # Use delvewheel on windows - CIBW_BEFORE_BUILD_WINDOWS: "pip install delvewheel" - CIBW_REPAIR_WHEEL_COMMAND_WINDOWS: > - delvewheel repair -w {dest_dir} {wheel} --add-path "${{ github.workspace }}\install\bin;${{ steps.mingw64-path.outputs.bin }}" - CIBW_ENVIRONMENT_LINUX: > - LD_LIBRARY_PATH="$(pwd)/install/lib64:$LD_LIBRARY_PATH" - CIBW_ENVIRONMENT_MACOS: > - DYLD_LIBRARY_PATH="$(pwd)/install/lib:$DYLD_LIBRARY_PATH" - MACOSX_DEPLOYMENT_TARGET=${{ matrix.macos-target }} - - # - uses: actions/upload-artifact@v4 - # with: - # name: wheels-${{ matrix.name }} - # path: ./wheelhouse/*.whl - - - name: Install software for publishing the wheels - run: | - python3 -m pip install twine - - - name: Upload wheels to pypi.org - if: ${{ github.event_name == 'release' }} - env: - TWINE_USERNAME: __token__ - TWINE_PASSWORD: ${{ secrets.PYPI_TOKEN }} - run: | - echo "::group::Upload to pypi.org" - for wheel in `ls ./wheelhouse/*.whl` - do - twine upload $wheel - done - echo "::endgroup::" - - - name: Upload wheels to test.pypi.org - if: false - env: - TWINE_USERNAME: __token__ - TWINE_PASSWORD: ${{ secrets.PYPI_TOKEN }} - run: | - echo "::group::Upload to test.pypi.org" - for wheel in `ls ./wheelhouse/*.whl` - do - twine upload --repository testpypi $wheel - done - echo "::endgroup::" diff --git a/AUTHORS b/AUTHORS index bb498504588..499c84ed0cc 100644 --- a/AUTHORS +++ b/AUTHORS @@ -10,18 +10,15 @@ 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 @@ -29,16 +26,21 @@ Current: 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. diff --git a/CMakeLists.txt b/CMakeLists.txt index f20fda2f6de..9d03d764b90 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Mathias Preiner, Gereon Kremer +# Aina Niemetz, Mathias Preiner, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -37,6 +37,9 @@ set(CMAKE_VISIBILITY_INLINES_HIDDEN 1) # plugins. set(CMAKE_EXPORT_COMPILE_COMMANDS ON) +# Default component used in install() commands +set(CMAKE_INSTALL_DEFAULT_COMPONENT_NAME cvc5) + #-----------------------------------------------------------------------------# # Policies @@ -90,10 +93,9 @@ cvc5_option(ENABLE_ASAN "Enable ASAN build") cvc5_option(ENABLE_UBSAN "Enable UBSan build") cvc5_option(ENABLE_TSAN "Enable TSan build") cvc5_option(ENABLE_ASSERTIONS "Enable assertions") -cvc5_option(ENABLE_COMP_INC_TRACK - "Enable optimizations for incremental SMT-COMP tracks") cvc5_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc5_option(ENABLE_MUZZLE "Suppress ALL non-result output") +cvc5_option(ENABLE_SAFE_MODE "Enable safe mode") cvc5_option(ENABLE_STATISTICS "Enable statistics") cvc5_option(ENABLE_TRACING "Enable tracing") cvc5_option(ENABLE_UNIT_TESTING "Enable unit testing") @@ -140,8 +142,10 @@ option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ") # Api documentation option(BUILD_DOCS "Build Api documentation") +option(BUILD_DOCS_GA "Build API documentation with Google Analytics") -option(BUILD_GMP "Build GMP from sources") +option(BUILD_GMP "Build GMP from source") +option(BUILD_CLN "Build CLN from source") # Link against static system libraries cvc5_option(STATIC_BINARY "Link against static system libraries \ @@ -232,6 +236,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 @@ -246,9 +251,12 @@ if (WIN32) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000") endif () -# Changing the default linker on MSYS prevents the build system from -# using the GMP system library if available -if (NOT ("${CMAKE_GENERATOR}" STREQUAL "MSYS Makefiles") AND NOT USE_DEFAULT_LINKER) +# Keep the default linker on MSYS, as switching it prevents the build system from +# using the GMP system library if available. For Linux ARM64, the default linker is +# also required due to a bug in the gold linker specific to ARM64 architectures. +if (NOT ("${CMAKE_GENERATOR}" STREQUAL "MSYS Makefiles") AND + NOT CMAKE_SYSTEM_PROCESSOR STREQUAL "aarch64" AND + NOT USE_DEFAULT_LINKER) #-----------------------------------------------------------------------------# # Use ld.mold if available, otherwise use ld.gold if available @@ -381,22 +389,48 @@ else() 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(Python_BASE_EXECUTABLE "${Python_EXECUTABLE}" + CACHE STRING "Base Python executable") + +macro(create_venv) + message(STATUS "Creating Python virtual environment") + # Use packages installed in the base installation if they're already present... + if(BUILD_BINDINGS_PYTHON AND NOT ONLY_PYTHON_EXT_SRC) + #... unless we are building the Python bindings. + # Building the Python bindings currently requires a recent version of + # setuptools. On old systems with Python 3.8 or 3.9, upgrading to the latest + # version of setuptools without manually upgrading its dependencies + # can cause problems (see https://github.com/pypa/setuptools/issues/4478). + # Therefore, we start with a clean virtual environment so that + # all the latest dependencies of setuptools are installed. + set(VENV_SYSTEM_PACKAGES_FLAG "") + else() + set(VENV_SYSTEM_PACKAGES_FLAG "--system-site-packages") + endif() + execute_process ( + COMMAND + "${Python_EXECUTABLE}" -m venv ${VENV_SYSTEM_PACKAGES_FLAG} "${VENV_PATH}" + RESULT_VARIABLE VENV_CMD_EXIT_CODE + ) + if(VENV_CMD_EXIT_CODE) + message(FATAL_ERROR "Could not create Python virtual environment") + endif() +endmacro() 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") + find_package(Pip REQUIRED) + create_venv() + else() + if(NOT (EXISTS ${VENV_PATH}/bin/pip OR EXISTS ${VENV_PATH}/Scripts/pip.exe)) + # This situation may be possible if cvc5 was built before 715f649 + execute_process(COMMAND ${CMAKE_COMMAND} -E remove_directory ${VENV_PATH}) + find_package(Pip REQUIRED) + create_venv() endif() endif() @@ -469,10 +503,6 @@ if(ENABLE_DEBUG_SYMBOLS) endif() endif() -if(ENABLE_COMP_INC_TRACK) - add_definitions(-DCVC5_SMTCOMP_APPLICATION_TRACK) -endif() - if(ENABLE_MUZZLE) add_definitions(-DCVC5_MUZZLE) endif() @@ -486,6 +516,10 @@ if(ENABLE_TRACING) add_definitions(-DCVC5_TRACING) endif() +if(ENABLE_SAFE_MODE) + add_definitions(-DCVC5_SAFE_MODE) +endif() + if(ENABLE_STATISTICS) add_definitions(-DCVC5_STATISTICS_ON) endif() @@ -511,10 +545,7 @@ if(USE_CRYPTOMINISAT) # CryptoMiniSat requires pthreads support set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) - if(THREADS_HAVE_PTHREAD_ARG) - add_c_cxx_flag(-pthread) - endif() - find_package(CryptoMiniSat 5.8 REQUIRED) + find_package(CryptoMiniSat 5.11.2 REQUIRED) add_definitions(-DCVC5_USE_CRYPTOMINISAT) endif() @@ -538,6 +569,7 @@ else() endif() if(USE_COCOA) + set(GPL_LIBS "${GPL_LIBS} cocoa") find_package(CoCoA REQUIRED 0.99711) add_definitions(-DCVC5_USE_COCOA) endif() @@ -556,7 +588,8 @@ if(GPL_LIBS) if(NOT ENABLE_GPL) message(FATAL_ERROR "Bad configuration detected: BSD-licensed code only, but also requested " - "GPLed libraries: ${GPL_LIBS}") + "GPLed libraries: ${GPL_LIBS}. (Configure with --gpl to allow GPLed " + "libraries.)") endif() set(CVC5_GPL_DEPS 1) endif() @@ -711,8 +744,8 @@ string(REPLACE ";" " " CVC5_DEFINITIONS "${CVC5_DEFINITIONS}") message("") print_info("cvc5 ${CVC5_VERSION}") message("") -if(ENABLE_COMP_INC_TRACK) - print_config("Build profile " "${CVC5_BUILD_PROFILE_STRING} (incremental)") +if (ENABLE_SAFE_MODE) + print_config("Build profile " "${CVC5_BUILD_PROFILE_STRING} (safe mode)") else() print_config("Build profile " "${CVC5_BUILD_PROFILE_STRING}") endif() diff --git a/COPYING b/COPYING index f589966a6d4..5a041e16217 100644 --- a/COPYING +++ b/COPYING @@ -1,4 +1,4 @@ -cvc5 is copyright (C) 2009-2023 by its authors and contributors (see the file +cvc5 is copyright (C) 2009-2025 by its authors and contributors (see the file AUTHORS) and their institutional affiliations. All rights reserved. The source code of cvc5 is open and available to students, researchers, @@ -74,6 +74,18 @@ The implementation of the floating point solver in cvc5 depends on symfpu See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for copyright and licensing information. +When building with GCC or MinGW-w64, cvc5 links against the libgcc and +libstdc++ libraries, which are licensed under the GNU GPL v3 with +the GCC Runtime Library exception. See the files licenses/gpl-3.0.txt and +licenses/GCC-exception-3.1.txt for a copy of the license and the exception, +respectively. Note that according to the terms of GPLv3 with the GCC-exception, +both cvc5's source, and the combined work (cvc5 linked with the libraries) may +(and do) remain under the more permissive modified BSD license. + +On Windows, cvc5 also links against the Winpthreads library from the MinGW-w64 +project (https://github.com/ldx/winpthreads). See licenses/winpthreads-LICENSE +for copyright and licensing information. + cvc5 optionally links against the following libraries: ABC (https://bitbucket.org/alanmi/abc) diff --git a/INSTALL.rst b/INSTALL.rst index 4eba0a51bab..97eaf71c5d1 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -13,15 +13,16 @@ Building cvc5 make check # to run default set of tests make install # to install into the prefix specified above -All binaries are built into ``/bin``, the cvc5 library is built into +All binaries are built into ``/bin``, the cvc5 libraries are built into ``/lib``. Supported Operating Systems --------------------------- -cvc5 can be built natively on Linux and macOS, cross-compilation is possible for -Windows using Mingw-w64. cvc5 also supports cross-compilation for ARM64 systems. +cvc5 can be built natively on Linux and macOS. Native compilation on Windows is also +possible using MSYS2. Additionally, cvc5 supports cross-compilation for x86_64 Windows +using Mingw-w64 and for ARM64 on both Linux and macOS. We generally recommend a 64-bit operating system. @@ -38,10 +39,37 @@ that uses static versions of all our dependencies, but is still a dynamically linked binary. +Compilation on Windows +^^^^^^^^^^^^^^^^^^^^^^ + +Install `MSYS2 `_ and `Python `_ on your system. +Launch a `MINGW64 environment `_ and +install the required packages for building cvc5: + +.. code:: bash + + pacman -S git make mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp zip + +Clone the cvc5 repository and follow the general build steps above. +The built binary ``cvc5.exe`` and the DLL libraries are located in +``/bin``. The import libraries and the static libraries +can be found in ``/lib``. + + Cross-compiling for Windows ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Cross-compiling cvc5 with Mingw-w64 can be done as follows: +Cross-compiling cvc5 for Windows requires the POSIX version of MinGW-w64. +On some Linux distributions, this is the default variant. On others, like Ubuntu, +you may need to set it manually as follows: + +.. code:: bash + + sudo update-alternatives --set x86_64-w64-mingw32-gcc /usr/bin/x86_64-w64-mingw32-gcc-posix + sudo update-alternatives --set x86_64-w64-mingw32-g++ /usr/bin/x86_64-w64-mingw32-g++-posix + +Once the POSIX variant of MinGW-w64 is installed and set on your system, +you can cross-compile cvc5 as follows: .. code:: bash @@ -50,8 +78,9 @@ Cross-compiling cvc5 with Mingw-w64 can be done as follows: cd # default is ./build make # use -jN for parallel build with N threads -The built binary ``cvc5.exe`` is located in ``/bin`` and the cvc5 -library can be found in ``/lib``. +The built binary ``cvc5.exe`` and the DLL libraries are located in +``/bin``. The import libraries and the static libraries +can be found in ``/lib``. WebAssembly Compilation @@ -95,7 +124,18 @@ code). which modifies how the wasm and glue code are built and how they behave. An ``-s`` should precede each flag. -For example, to generate modularized glue code, use: +For example, to generate a HTML page, use: + +.. code:: bash + + ./configure.sh --static --static-binary --auto-download --wasm=HTML --name=prod + + cd prod + make # use -jN for parallel build with N threads + +After that, you can run ``python -m http.server`` within ``prod/bin``, open http://0.0.0.0:8000/cvc5.html with Chrome to visualize the page generated by Emscripten, write down a valid SMTLIB input, and press ESC twice to obtain its output. + +On the other hand, to generate a modularized glue code to be imported by custom web pages, use: .. code:: bash @@ -120,11 +160,11 @@ versions; more recent versions should be compatible. - `CMake >= 3.16 `_ - `GNU Make `_ or `Ninja `_ -- `Python >= 3.6 `_ +- `Python >= 3.7 `_ + module `tomli `_ (Python < 3.11) + module `pyparsing `_ - `GMP v6.3 (GNU Multi-Precision arithmetic library) `_ -- `CaDiCaL >= 1.6.0 (SAT solver) `_ +- `CaDiCaL >= 2.1.0 (SAT solver) `_ - `SymFPU `_ If ``--auto-download`` is given, the Python modules will be installed automatically in @@ -167,7 +207,7 @@ CryptoMiniSat (Optional SAT solver) can be used for solving bit-vector problems with eager bit-blasting. This dependency may improve performance. It can be downloaded and built automatically. Configure cvc5 with ``configure.sh --cryptominisat`` to build -with this dependency. +with this dependency. Minimum version required is ``5.11.2``. Kissat (Optional SAT solver) @@ -193,7 +233,7 @@ CoCoA (Optional computer algebra library) reasoning and for finite field reasoning. We use a patched version of it, so we recommend downloading it using the ``--auto-download`` configuration flag, which applies our patch automatically. It is included in the build through the -``--cocoa`` configuration flag. +``--cocoa --gpl`` configuration flag. CoCoA is covered by the GPLv3 license. See below for the ramifications of this. @@ -202,7 +242,7 @@ CLN >= v1.3 (Class Library for Numbers) `CLN `_ is an alternative multiprecision arithmetic package that may offer better performance and memory footprint than GMP. -Configure cvc5 with ``configure.sh --cln`` to build with this dependency. +Configure cvc5 with ``configure.sh --cln --gpl`` to build with this dependency. Note that CLN is covered by the `GNU General Public License, version 3 `_. If you choose to use cvc5 with @@ -219,10 +259,11 @@ glpk-cut-log (A fork of the GNU Linear Programming Kit) This can be used to speed up certain classes of problems for the arithmetic implementation in cvc5. (This is not recommended for most users.) -glpk-cut-log can be installed using the ``contrib/get-glpk-cut-log`` script. -Note that the only installation option is manual installation via this script. -cvc5 is no longer compatible with the main GLPK library. Configure cvc5 with -``configure.sh --glpk`` to build with this dependency. +cvc5 is not compatible with the official version of the GLPK library. +To use the patched version of it, we recommend downloading it using +the ``--auto-download`` configuration flag, which applies +the patch automatically. +Configure cvc5 with ``configure.sh --glpk --gpl`` to build with this dependency. Note that GLPK and glpk-cut-log are covered by the `GNU General Public License, version 3 `_. If you choose to use @@ -269,8 +310,11 @@ Dependencies for Language Bindings - Python - `Cython `_ >= 3.0.0 + - `pip `_ >= 23.0 - `pytest `_ - - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`. + - `repairwheel `_ >= 0.3.1 + - `setuptools `_ >= 66.1.0 + - The source for the `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 +323,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 `_. diff --git a/NEWS.md b/NEWS.md index a702b8d47b1..b6579435ea1 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,15 +1,150 @@ This file contains a summary of important user-visible changes. +## New Features + +- We now support the SMT-LIB version 2.7 standard syntax for arithmetic + bit-vector conversion functions whose smt2 syntax is `int_to_bv`, `ubv_to_int` + and `sbv_to_int`. The first maps to the existing kind `Kind::INT_TO_BITVECTOR`. + The kinds `Kind::BITVECTOR_UBV_TO_INT` and `Kind::BITVECTOR_SBV_TO_INT` + are added to the API for the latter two. Note the syntax `int2bv` and `bv2nat` + as well as the kind `Kind::BITVECTOR_TO_NAT` are now deprecated. + +## Changes + +- Bumped CaDiCaL to version 2.1.3. + +cvc5 1.2.1 +========== + +## New Features + +- Updates to the `cpc` proof signature. The 0.1.1 release of Ethos can check + proofs generated by this version of cvc5 (`./contrib/get-ethos-checker`). + +- Increased coverage for proofs, in particular for theories allowed by + `--safe-options`. + +- Added support for `SymbolManager::getNamedTerms()` to retrieve the set of + terms that have been given names by the SMT-LIB attribute `:named`. + +- Added option `--parsing-mode` to allow configuration of both more strict but + also more lenient parsing than default. Already existing option + `--strict-parsing` is an alias `--parsing-mode=strict`. + Parsing symbols that start with `.` or `@` (used for internally freshly + introduced symbols) in lenient parsing mode (`--parsing-mode=lenient`). + +## Changes + +- The option `--safe-options` now **disables experimental** theories and their + extensions in cvc5. This includes the theory of bags, the theory of finite + fields, the theory of separation logic, higher-order extensions to the theory + of equality, as well as extensions of the theory of arithmetic for + transcendental functions, integer-and, and power functions, and the theory of + arrays for constant arrays. These theories are still enabled by default and + further more can be used in combination with safe options by the options e.g. + `--arith-exp` **prior** to setting `--safe-options`. + +- Renamed the flag `--sets-ext` to `--sets-exp`, which enables non-standard + extensions of the sets theory. + +- Fixed a soundness bug in the solver for `set.filter`. + +- When printing with tags `-o pre-asserts` or `-o post-asserts`, by default we + now ensure that declarations are printed in a deterministic order. + +- Bumped CaDiCaL to version 2.0.0. + + +cvc5 1.2.0 +========== + +## New Features + +- New **C API**, implemented as a thin wrapper around the C++ API. + - Documentation: https://cvc5.github.io/docs-ci/docs-main/api/c/c.html + - Examples: https://github.com/cvc5/cvc5/tree/main/examples/api/c + +- Exposed creation and maintenance of **Skolem functions** to the API. Skolem + functions are symbols that are internally introduced by cvc5 during solving. + They are formalized via an identifier (see + https://cvc5.github.io/docs-ci/docs-main/skolem-ids.html for details) as well + as a (possibly empty) set of indices. + + The **API** methods `Term::isSkolem()`, `Term::getSkolemId()`, and + `Term::getSkolemIndices()`may now be used to identify terms corresponding + to skolems. + +- We now export kinds `BITVECTOR_FROM_BOOLS`, `BITVECTOR_BIT`, `DIVISION_TOTAL`, + `INTS_DIVISION_TOTAL`, `INTS_MODULUS_TOTAL` which may appear in terms + resulting from simplification or terms appearing in proofs. + +- Proof rules corresponding to rewrite rules are now exported in the API via + the enum `ProofRewriteRule`. + +- A new `Plugin` class is available in our API. This class allows a user + to be notified when SAT clauses or theory lemmas are learned internally + by cvc5. The plugin class also contains a callback for the user to introduce + new learned clauses into the state of cvc5 during solving. + +- Added a new strategy `--mbqi-fast-sygus` (disabled by default) for **quantifier + instantiation** which uses SyGuS enumeration to augment instantiations from + model-based quantifier instantiation. + +## Changes + +- We now require CMake >= 3.16. + +- **API** + All APIs have been refactored to expose a TermManager to the API. A term + manager manages creation and maintenance of all terms and sorts (across + potentially several solver instances within a thread). + Corresponding functions that were previously associated with a solver + instance and are now associated with a term manager are now deprecated + and will be removed in a future release. + * Python: + - Constructor `SymbolManager(Solver)` is now deprecated and replaced + by `SymbolManager(TermManager)`. + * Pythonic: + - Unsat cores and proofs are now available via the `Solver` methods + `unsat_core()` and `proof()`, respectively. + +- The default proof format of cvc5 has been renamed to the + **Cooperating Proof Calculus (CPC) proof format**. This proof format coincides + with proof objects in our API. + * **API** + + The option `--proof-format=cpc` prints proofs in the CPC format. + This option is now enabled by default. + * The **Ethos** proof checker is available, which can check proofs in this + format. In particular, the 0.1.0 release of Ethos can check proofs generated + by this version of cvc5. This checker is the second generation of the + AletheLF checker (`alfc`). Ethos inherits the code base of alfc and is based + on a logical framework called **Eunoia** (formerly called AletheLF). + See https://github.com/cvc5/ethos for more details. Note that the + development version of Ethos is available for download via the script + `./contrib/get-ethos-checker`, which will be kept in sync with further + development versions of cvc5. + * The rules of this format have been formalized in Eunoia and are available + in the cvc5 repository under the directory `./proofs/eo/cpc/`. + +- The semantics of `SQRT` was changed to assume the result is positive. + +- Fixed a bug involving how sequence terms are printed in model values. + + cvc5 1.1.2 ========== ## New Features -- Added support for **nullable** sorts and lift operator to the theory of **datatypes**. -- Adds a new strategy `--sub-cbqi` (disabled by default) for **quantifier +- Added support for **nullable** sorts and lift operator to the theory of + **datatypes**. + +- Added a new strategy `--sub-cbqi` (disabled by default) for **quantifier instantiation** which uses subsolvers to compute unsat cores of instantiations that are used in proofs of unsatisfiability. +- Add support for the kind `BITVECTOR_NEGO` corresponding to bitvector + negation overflow detection. + ## Changes - SAT clauses are no longer marked as removable in MiniSat. This change @@ -79,9 +214,10 @@ cvc5 1.1.0 SMT-LIB command `get-timeout-core-assuming`, which accept a list of formulas to assume, while all current assertions are implicitly included in the core. - * Add new method `Solver::getUnsatCoreLemmas` which returns the set of theory - lemmas that were relevant to showing the last query was unsatisfiable. This - is also avialable via the SMT-LIB command `get-unsat-core-lemmas`. + * Added new method `Solver::getUnsatCoreLemmas` which returns the set of + theory lemmas that were relevant to showing the last query was + unsatisfiable. This is also avialable via the SMT-LIB command + `get-unsat-core-lemmas`. - Support for the **AletheLF (ALF) proof format**. This format combines the strengths of the Alethe and LFSC proof formats, namely it borrows much of the @@ -111,7 +247,7 @@ Note: This is a pre-release version for the upcoming version 1.1.0. ## New Features - **API** - + Add the ability to query the logic that has been set in the solver via + + Added the ability to query the logic that has been set in the solver via `Solver::isLogicSet` and `Solver::getLogic`. ## Changes diff --git a/README.md b/README.md index c4f64bc02ef..14c5179ad06 100644 --- a/README.md +++ b/README.md @@ -55,13 +55,20 @@ Nightly builds are available [here](https://cvc5.github.io/downloads). Build and Dependencies ------------------------------------------------------------------------------- -cvc5 can be built on Linux and macOS. For Windows, cvc5 can be cross-compiled -using Mingw-w64. +cvc5 can be built on Linux and macOS. For Windows, cvc5 can be built using MSYS2 +or cross-compiled using Mingw-w64. For detailed build and installation instructions on these platforms, see file [INSTALL.rst](https://github.com/cvc5/cvc5/blob/main/INSTALL.rst). +Interfaces +------------------------------------------------------------------------------- + +cvc5 features APIs for several different programming languages such as Python and +Java. See the [user documentation](https://cvc5.github.io/docs/) for more information. + + Bug Reports ------------------------------------------------------------------------------- diff --git a/THANKS b/THANKS index 1e4c092081a..0bbd7aab2d4 100644 --- a/THANKS +++ b/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. diff --git a/cmake/CMakeGraphVizOptions.cmake.in b/cmake/CMakeGraphVizOptions.cmake.in index 1c3e83a302f..3ed47afa5f4 100644 --- a/cmake/CMakeGraphVizOptions.cmake.in +++ b/cmake/CMakeGraphVizOptions.cmake.in @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index f86d0c619c4..58f97ea5fd8 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index ce5c35dac02..0a5125c8622 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Aina Niemetz +# Mathias Preiner, Aina Niemetz, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 5b3ccfc8c90..95ac80ed921 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 5f9e1c524d4..d1fcb3df4c4 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/ConfigureCvc5.cmake b/cmake/ConfigureCvc5.cmake index 233b03e1259..8e43fd63ab1 100644 --- a/cmake/ConfigureCvc5.cmake +++ b/cmake/ConfigureCvc5.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index c0484c34531..0c3b18036e2 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Daniel Larraz +# Daniel Larraz, Gereon Kremer, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -18,8 +18,10 @@ include(deps-helper) -find_path(CLN_INCLUDE_DIR NAMES cln/cln.h) -find_library(CLN_LIBRARIES NAMES cln) +if (NOT BUILD_CLN) + find_path(CLN_INCLUDE_DIR NAMES cln/cln.h) + find_library(CLN_LIBRARIES NAMES cln) +endif() set(CLN_FOUND_SYSTEM FALSE) if(CLN_INCLUDE_DIR AND CLN_LIBRARIES) @@ -47,40 +49,91 @@ 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") - string(REPLACE "." "-" CLN_TAG ${CLN_VERSION}) + 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}" + ) 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}/lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}") + if(CMAKE_SYSTEM_NAME STREQUAL "Darwin") + set(CLN_BYPRODUCTS + /lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libcln.${CLN_SO_MAJOR_VER}${CMAKE_SHARED_LIBRARY_SUFFIX} + ) + else() + set(CLN_BYPRODUCTS + /lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}.${CLN_SO_MAJOR_VER} + /lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}.${CLN_SO_VERSION} + ) + endif() + else() + set(LINK_OPTS --enable-static --disable-shared) + set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln${CMAKE_STATIC_LIBRARY_SUFFIX}") + set(CLN_BYPRODUCTS /lib/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() + + set(CLN_WITH_GMP) + if(NOT GMP_FOUND_SYSTEM) + set(CLN_WITH_GMP "--with-gmp=") 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-${CLN_VERSION}.tar.bz2" + URL_HASH SHA256=7c7ed8474958337e4df5bb57ea5176ad0365004cbb98b621765bc4606a10d86b + DOWNLOAD_NAME cln.tar.bz2 CONFIGURE_COMMAND - ${CMAKE_COMMAND} -E chdir ./autogen.sh - COMMAND - ${CMAKE_COMMAND} -E chdir autoreconf -iv - COMMAND ${SHELL} /configure --prefix= --enable-shared - --enable-static --with-pic - BUILD_BYPRODUCTS /${CMAKE_INSTALL_LIBDIR}/libcln.a - /${CMAKE_INSTALL_LIBDIR}/libcln${CMAKE_SHARED_LIBRARY_SUFFIX} + ${CONFIGURE_ENV} ${SHELL} /configure + --prefix= ${LINK_OPTS} --with-pic ${CLN_WITH_GMP} + ${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 +160,19 @@ 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}" 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}) + + if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE) + foreach(CLN_DYLIB ${BUILD_BYPRODUCTS}) + get_filename_component(CLN_DYLIB_NAME ${CLN_DYLIB} NAME) + update_rpath_macos(${CLN_DYLIB_NAME}) + endforeach() + endif() endif() diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake index 3f34e7e6c2b..a4015abee47 100644 --- a/cmake/FindCVC5PythonicAPI.cmake +++ b/cmake/FindCVC5PythonicAPI.cmake @@ -1,16 +1,16 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Alex Ozdemir +# Gereon Kremer, Alex Ozdemir, Haniel Barbosa # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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 cvc5 pythonic api. +# Find cvc5 pythonic api. # CVC5PythonicAPI_FOUND - found cvc5 pythonic api # CVC5PythonicAPI_BASEDIR - the base directory of the cvc5 pythonic api ## @@ -34,12 +34,12 @@ else() check_auto_download("CVC5PythonicAPI" "--no-python-bindings") endif() - set(CVC5PythonicAPI_VERSION "1582d36944310a96cc8e2dfc01e3682745866812") + set(CVC5PythonicAPI_VERSION "be54c2388b3271f657cad41cf5e3d6bc97cd51a1") ExternalProject_Add( CVC5PythonicAPI ${COMMON_EP_CONFIG} URL https://github.com/cvc5/cvc5_pythonic_api/archive/${CVC5PythonicAPI_VERSION}.zip - URL_HASH SHA1=4380d6bd58ef3e82acc51d4aaf6fd62ba38e6070 + URL_HASH SHA256=2bbee4592f7e01869a1512d11d57dcd88453f44076306c0d294877e81e2c0ca9 CONFIGURE_COMMAND "" BUILD_COMMAND "" INSTALL_COMMAND "" diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index e60363ab312..8d4a637dc42 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -66,7 +66,9 @@ if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRARIES) endif() # Minimum supported version - set(CaDiCaL_FIND_VERSION "1.6.0") + set(CaDiCaL_FIND_VERSION "2.1.0") + # Maximum supported version + set(CaDiCaL_FIND_VERSION_MAX "2.1.3") # Set FOUND_SYSTEM to true; check_system_version will unset this if the # version is less than the minimum required @@ -85,27 +87,32 @@ if(NOT CaDiCaL_FOUND_SYSTEM) include(CheckSymbolExists) include(ExternalProject) - set(CaDiCaL_VERSION "rel-1.7.4") - set(CaDiCaL_CHECKSUM "9cc70c65c80f40c0c13b57cb43ea2a6804cae4eb") + set(CaDiCaL_VERSION "rel-2.1.3") + set(CaDiCaL_CHECKSUM "abfe890aa4ccda7b8449c7ad41acb113cfb8e7e8fbf5e49369075f9b00d70465") # avoid configure script and instantiate the makefile manually the configure # scripts unnecessarily fails for cross compilation thus we do the bare # minimum from the configure script here - set(CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11") + set(CaDiCaL_CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11") if(CMAKE_CROSSCOMPILING_MACOS) - set(CXXFLAGS "${CXXFLAGS} -arch ${CMAKE_OSX_ARCHITECTURES}") + set(CaDiCaL_CXXFLAGS "${CaDiCaL_CXXFLAGS} -arch ${CMAKE_OSX_ARCHITECTURES}") endif() # check for getc_unlocked check_symbol_exists("getc_unlocked" "cstdio" HAVE_UNLOCKED_IO) if(NOT HAVE_UNLOCKED_IO) - string(APPEND CXXFLAGS " -DNUNLOCKED") + string(APPEND CaDiCaL_CXXFLAGS " -DNUNLOCKED") + endif() + # check for closefrom + check_symbol_exists("closefrom" "fcntl.h" HAVE_CLOSEFROM) + if(NOT HAVE_CLOSEFROM) + string(APPEND CaDiCaL_CXXFLAGS " -DNCLOSEFROM") endif() # On macOS, we have to set `-isysroot` to make sure that include headers are # found because they are not necessarily installed at /usr/include anymore. if(CMAKE_OSX_SYSROOT) - string(APPEND CXXFLAGS " ${CMAKE_CXX_SYSROOT_FLAG} ${CMAKE_OSX_SYSROOT}") + string(APPEND CaDiCaL_CXXFLAGS " ${CMAKE_CXX_SYSROOT_FLAG} ${CMAKE_OSX_SYSROOT}") endif() if("${CMAKE_GENERATOR}" STREQUAL "Unix Makefiles") @@ -116,19 +123,26 @@ if(NOT CaDiCaL_FOUND_SYSTEM) set(make_cmd "make") endif() + set(USE_EMAR "") + if(NOT(WASM STREQUAL "OFF")) + set(USE_EMAR "-e s,ar rc,emar rc,") + endif() + + set(CaDiCaL_SOURCE_DIR ) ExternalProject_Add( CaDiCaL-EP ${COMMON_EP_CONFIG} BUILD_IN_SOURCE ON URL https://github.com/arminbiere/cadical/archive/${CaDiCaL_VERSION}.tar.gz - URL_HASH SHA1=${CaDiCaL_CHECKSUM} + URL_HASH SHA256=${CaDiCaL_CHECKSUM} CONFIGURE_COMMAND mkdir -p /build # avoid configure script, prepare the makefile manually COMMAND ${CMAKE_COMMAND} -E copy /makefile.in /build/makefile COMMAND sed -i.orig -e "s,@CXX@,${CMAKE_CXX_COMPILER}," -e - "s,@CXXFLAGS@,${CXXFLAGS}," -e "s,@MAKEFLAGS@,," + "s,@CXXFLAGS@,${CaDiCaL_CXXFLAGS}," -e + "s,@ROOT@,${CaDiCaL_SOURCE_DIR}," -e "s,@CONTRIB@,no," ${USE_EMAR} /build/makefile BUILD_COMMAND ${make_cmd} -C /build libcadical.a INSTALL_COMMAND ${CMAKE_COMMAND} -E copy /build/libcadical.a diff --git a/cmake/FindCoCoA.cmake b/cmake/FindCoCoA.cmake index 5978f8cc4e6..25ec72cdbaa 100644 --- a/cmake/FindCoCoA.cmake +++ b/cmake/FindCoCoA.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Alex Ozdemir, Sorawee Porncharoenwase +# Gereon Kremer, Daniel Larraz, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -31,6 +31,24 @@ if(CoCoA_INCLUDE_DIR AND CoCoA_LIBRARIES) string(REGEX MATCH "[0-9]+\\.[0-9]+" CoCoA_VERSION "${CoCoA_VERSION}") check_system_version("CoCoA") + + # This test checks whether CoCoA has been patched + try_compile(CoCoA_USABLE "${DEPS_BASE}/try_compile/CoCoA-EP" + "${CMAKE_CURRENT_LIST_DIR}/deps-utils/cocoa-test.cpp" + CMAKE_FLAGS + "-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}" + "-DINCLUDE_DIRECTORIES=${CoCoA_INCLUDE_DIR}" + LINK_LIBRARIES ${CoCoA_LIBRARIES} ${GMP_LIBRARIES} ${GMPXX_LIBRARIES} + ) + if(NOT CoCoA_USABLE) + message(STATUS "The system version of CoCoA has not been patched.") + if(ENABLE_AUTO_DOWNLOAD) + message(STATUS "A patched version of CoCoA will be built for you.") + else() + message(STATUS "Use --auto-download to let us download and build a patched version of CoCoA for you.") + endif() + set(CoCoA_FOUND_SYSTEM FALSE) + endif() endif() if(NOT CoCoA_FOUND_SYSTEM) @@ -53,17 +71,30 @@ if(NOT CoCoA_FOUND_SYSTEM) get_target_property(GMP_LIBRARY GMP IMPORTED_LOCATION) + find_program(PATCH_BIN patch) + if(NOT PATCH_BIN) + message(FATAL_ERROR "Can not build CoCoA, missing binary for patch") + endif() + + set(CoCoA_CXXFLAGS "") + # On macOS, we have to set `-isysroot` to make sure that include headers are + # found because they are not necessarily installed at /usr/include anymore. + if(CMAKE_OSX_SYSROOT) + set(CoCoA_CXXFLAGS "${CMAKE_CXX_SYSROOT_FLAG} ${CMAKE_OSX_SYSROOT}") + endif() + ExternalProject_Add( CoCoA-EP ${COMMON_EP_CONFIG} - URL "http://cocoa.dima.unige.it/cocoa/cocoalib/tgz/CoCoALib-${CoCoA_VERSION}.tgz" + URL https://github.com/cvc5/cvc5-deps/blob/main/CoCoALib-${CoCoA_VERSION}.tgz?raw=true URL_HASH SHA256=f8bb227e2e1729e171cf7ac2008af71df25914607712c35db7bcb5a044a928c6 # CoCoA requires C++14, but the check does not work with compilers that # default to C++17 or newer. The patch fixes the check. PATCH_COMMAND patch -p1 -d - -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CoCoALib-0.99800-trace.patch + -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CoCoALib-${CoCoA_VERSION}-trace.patch BUILD_IN_SOURCE YES - CONFIGURE_COMMAND ${SHELL} ./configure --prefix= --with-libgmp=${GMP_LIBRARY} --with-cxx=${CMAKE_CXX_COMPILER} + CONFIGURE_COMMAND ${SHELL} ./configure --prefix= --with-libgmp=${GMP_LIBRARY} + --with-cxx=${CMAKE_CXX_COMPILER} --with-cxxflags=${CoCoA_CXXFLAGS} BUILD_COMMAND ${make_cmd} library BUILD_BYPRODUCTS /lib/libcocoa.a ) @@ -100,4 +131,12 @@ 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) + set(CoCoA_INSTALLED_LIBRARY + "${DEPS_BASE}/lib/libcocoa-${CoCoA_VERSION}.a" + ) + install(FILES ${CoCoA_INSTALLED_LIBRARY} TYPE ${LIB_BUILD_TYPE} + RENAME "libcocoa.a") + endif() endif() diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index 606d2093fc8..2b06470a5a0 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andrew V. Teylu +# Gereon Kremer, Mathias Preiner, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -26,12 +26,6 @@ if(cryptominisat5_FOUND) set(CryptoMiniSat_FOUND_SYSTEM TRUE) add_library(CryptoMiniSat INTERFACE IMPORTED GLOBAL) target_link_libraries(CryptoMiniSat INTERFACE cryptominisat5) - # TODO(gereon): remove this when - # https://github.com/msoos/cryptominisat/pull/645 is merged - set_target_properties( - CryptoMiniSat PROPERTIES INTERFACE_SYSTEM_INCLUDE_DIRECTORIES - "${CRYPTOMINISAT5_INCLUDE_DIRS}" - ) endif() if(NOT CryptoMiniSat_FOUND_SYSTEM) @@ -54,7 +48,7 @@ if(NOT CryptoMiniSat_FOUND_SYSTEM) CryptoMiniSat-EP ${COMMON_EP_CONFIG} URL https://github.com/msoos/cryptominisat/archive/refs/tags/${CryptoMiniSat_VERSION}.tar.gz - URL_HASH SHA1=d97510a186af8eaecc3ecf38dad345e0758288a5 + URL_HASH SHA256=288fd53d801909af797c72023361a75af3229d1806dbc87a0fcda18f5e03763b CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release # make sure not to register with cmake -DCMAKE_EXPORT_NO_PACKAGE_REGISTRY=ON @@ -86,10 +80,6 @@ if(NOT CryptoMiniSat_FOUND_SYSTEM) set_target_properties( CryptoMiniSat PROPERTIES IMPORTED_LOCATION "${CryptoMiniSat_LIBRARIES}" ) - set_target_properties( - CryptoMiniSat PROPERTIES INTERFACE_SYSTEM_INCLUDE_DIRECTORIES - "${CryptoMiniSat_INCLUDE_DIR}" - ) endif() set(CryptoMiniSat_FOUND TRUE) @@ -110,4 +100,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() diff --git a/cmake/FindCython.cmake b/cmake/FindCython.cmake index b2978136e6a..c534e74ba60 100644 --- a/cmake/FindCython.cmake +++ b/cmake/FindCython.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake index 52b4d656c4d..406500a8cee 100644 --- a/cmake/FindDrat2Er.cmake +++ b/cmake/FindDrat2Er.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindDummy.cmake.template b/cmake/FindDummy.cmake.template index e52b3ac77d9..06974ef8605 100644 --- a/cmake/FindDummy.cmake.template +++ b/cmake/FindDummy.cmake.template @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS +# 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. @@ -65,7 +65,7 @@ if(NOT Dummy_FOUND_SYSTEM) Dummy-EP ${COMMON_EP_CONFIG} URL https://dummy.org/download/dummy-${Dummy_VERSION}.tar.bz2 - URL_HASH SHA1=abc123 + URL_HASH SHA256=abc123 CMAKE_ARGS -DCMAKE_INSTALL_PREFIX= -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake index 3aa69fe2943..17ab60d95ac 100644 --- a/cmake/FindEditline.cmake +++ b/cmake/FindEditline.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Andrew V. Jones, Mathias Preiner, Gereon Kremer +# Andrew V. Jones, Mathias Preiner, Andrew V. Teylu # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index 366776fdc75..c1709767621 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner +# Daniel Larraz, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -20,8 +20,8 @@ find_path(GLPK_INCLUDE_DIR NAMES glpk.h) find_library(GLPK_LIBRARIES NAMES glpk) -# Check if we really have GLPK-cut-log. -if(GLPK_INCLUDE_DIR) +set(GLPK_FOUND_SYSTEM FALSE) +if(GLPK_INCLUDE_DIR AND GLPK_LIBRARIES) include(CheckSymbolExists) set(CMAKE_REQUIRED_INCLUDES ${GLPK_INCLUDE_DIR}) set(CMAKE_REQUIRED_LIBRARIES ${GLPK_LIBRARIES} m) @@ -30,14 +30,124 @@ if(GLPK_INCLUDE_DIR) message(FATAL_ERROR "Could not link against GLPK-cut-log. " "Did you forget to install GLPK-cut-log?") endif() + set(GLPK_FOUND_SYSTEM TRUE) endif() -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(GLPK - DEFAULT_MSG - GLPK_INCLUDE_DIR GLPK_LIBRARIES) +if(NOT GLPK_FOUND_SYSTEM) + check_ep_downloaded("GLPK-EP") + if(NOT GLPK-EP_DOWNLOADED) + check_auto_download("GLPK" "--no-glpk") + endif() + + include(ExternalProject) + + set(GLPK_VERSION "4.52") + + 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() + + find_package(Patch) + if(NOT Patch_FOUND) + message(FATAL_ERROR "Can not build GLPK, missing binary for patch") + endif() -mark_as_advanced(GLPK_INCLUDE_DIR GLPK_LIBRARIES) -if(GLPK_LIBRARIES) - message(STATUS "Found GLPK libs: ${GLPK_LIBRARIES}") + find_program(LIBTOOLIZE NAMES libtoolize glibtoolize) + if(NOT LIBTOOLIZE) + message(FATAL_ERROR "Can not build GLPK, missing binary for libtoolize") + endif() + + find_program(ACLOCAL aclocal) + if(NOT ACLOCAL) + message(FATAL_ERROR "Can not build GLPK, missing binary for aclocal") + endif() + + find_program(AUTOHEADER autoheader) + if(NOT AUTOHEADER) + message(FATAL_ERROR "Can not build GLPK, missing binary for autoheader") + endif() + + find_program(AUTOCONF autoconf) + if(NOT AUTOCONF) + message(FATAL_ERROR "Can not build GLPK, missing binary for autoconf") + endif() + + find_program(AUTOMAKE automake) + if(NOT AUTOMAKE) + message(FATAL_ERROR "Can not build GLPK, missing binary for automake") + endif() + + set(CONFIGURE_ENV "") + set(CONFIGURE_OPTS "") + 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( + GLPK-EP + ${COMMON_EP_CONFIG} + URL "https://ftp.gnu.org/gnu/glpk/glpk-${GLPK_VERSION}.tar.gz" + URL_HASH SHA256=9a5dab356268b4f177c33e00ddf8164496dc2434e83bd1114147024df983a3bb + PATCH_COMMAND ${Patch_EXECUTABLE} -p1 -d + -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/glpk-cut-log.patch + CONFIGURE_COMMAND ${CMAKE_COMMAND} -E chdir ${LIBTOOLIZE} + COMMAND ${CMAKE_COMMAND} -E chdir ${ACLOCAL} + COMMAND ${CMAKE_COMMAND} -E chdir ${AUTOHEADER} + COMMAND ${CMAKE_COMMAND} -E chdir ${AUTOCONF} + COMMAND ${CMAKE_COMMAND} -E chdir ${AUTOMAKE} --add-missing + COMMAND ${CONFIGURE_ENV} ${SHELL} /configure + --prefix= --disable-shared + --enable-static --with-pic ${CONFIGURE_OPTS} + BUILD_COMMAND ${MAKE_CMD} install + BUILD_BYPRODUCTS /lib/libglpk.a + /include/glpk.h + ) + + set(GLPK_INCLUDE_DIR "${DEPS_BASE}/include/") + set(GLPK_LIBRARIES "${DEPS_BASE}/lib/libglpk.a") +endif() + +set(GLPK_FOUND TRUE) + +add_library(GLPK STATIC IMPORTED GLOBAL) +set_target_properties(GLPK PROPERTIES + IMPORTED_LOCATION "${GLPK_LIBRARIES}" + INTERFACE_SYSTEM_INCLUDE_DIRECTORIES "${GLPK_INCLUDE_DIR}" +) + +mark_as_advanced(PATCH) +mark_as_advanced(LIBTOOLIZE) +mark_as_advanced(ACLOCAL) +mark_as_advanced(AUTOHEADER) +mark_as_advanced(AUTOCONF) +mark_as_advanced(AUTOMAKE) +mark_as_advanced(GLPK_FOUND) +mark_as_advanced(GLPK_FOUND_SYSTEM) +mark_as_advanced(GLPK_INCLUDE_DIR) +mark_as_advanced(GLPK_LIBRARIES) + +if(GLPK_FOUND_SYSTEM) + message(STATUS "Found GLPK ${GLPK_VERSION}: ${GLPK_LIBRARIES}") +else() + message(STATUS "Building GLPK ${GLPK_VERSION}: ${GLPK_LIBRARIES}") + add_dependencies(GLPK GLPK-EP) + # Install static library only if it is a static build. + if(NOT BUILD_SHARED_LIBS) + install(FILES ${GLPK_LIBRARIES} TYPE ${LIB_BUILD_TYPE}) + endif() endif() diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 19d61a50c96..7aea676fc3a 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Andres Noetzli, Vinícius Camillo +# Gereon Kremer, Daniel Larraz, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -125,7 +125,7 @@ if(NOT GMP_FOUND_SYSTEM) GMP-EP ${COMMON_EP_CONFIG} URL https://ftp.gnu.org/gnu/gmp/gmp-${GMP_VERSION}.tar.bz2 - URL_HASH SHA1=32d21c4fae046de45e8fce37bf4002236d283b71 + URL_HASH SHA256=ac28211a7cfb609bae2e2c8d6058d66c8fe96434f740cf6fe2e47b000d1c20cb CONFIGURE_COMMAND ${CONFIGURE_ENV} ${CONFIGURE_CMD_WRAPPER} ${SHELL} /configure @@ -164,4 +164,34 @@ 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() + if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE) + install(CODE " + file(GLOB GMP_DYLIBS \"\${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/libgmp*.dylib\") + foreach(GMP_DYLIB \${GMP_DYLIBS}) + execute_process(COMMAND \${CMAKE_COMMAND} + -DRPATH=@loader_path + -DINSTALL_NAME_TOOL=${CMAKE_INSTALL_NAME_TOOL} + -DDYLIB_PATH=\${GMP_DYLIB} + -DDEPS_BASE=${DEPS_BASE} + -P ${CMAKE_SOURCE_DIR}/cmake/update_rpath_macos.cmake) + endforeach() + ") + endif() endif() diff --git a/cmake/FindGTest.cmake b/cmake/FindGTest.cmake index 01acf8aa2e4..8ca26591f6f 100644 --- a/cmake/FindGTest.cmake +++ b/cmake/FindGTest.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Yoni Zohar +# Gereon Kremer, Mathias Preiner, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -38,7 +38,7 @@ if(NOT GTest_FOUND_SYSTEM) GTest-EP ${COMMON_EP_CONFIG} URL https://github.com/google/googletest/archive/refs/tags/release-${GTest_VERSION}.tar.gz - URL_HASH SHA1=7b100bb68db8df1060e178c495f3cbe941c9b058 + URL_HASH SHA256=b4870bf121ff7795ba20d20bcdd8627b8e088f2d1dab299a031c1034eddc93d5 DOWNLOAD_NAME gtest.tar.gz CMAKE_ARGS -DCMAKE_INSTALL_PREFIX= diff --git a/cmake/FindHamcrest.cmake b/cmake/FindHamcrest.cmake index 5a4820cf0e1..bd1749b70ed 100644 --- a/cmake/FindHamcrest.cmake +++ b/cmake/FindHamcrest.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindJUnit.cmake b/cmake/FindJUnit.cmake index 80283c9086a..919a3890116 100644 --- a/cmake/FindJUnit.cmake +++ b/cmake/FindJUnit.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mudathir Mohamed, Mathias Preiner +# Mudathir Mohamed, Mathias Preiner, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -38,7 +38,7 @@ if(NOT JUnit_FOUND_SYSTEM) JUnit-EP-jar PREFIX ${DEPS_PREFIX} URL https://repo1.maven.org/maven2/org/junit/platform/junit-platform-console-standalone/${JUNIT_VERSION}/junit-platform-console-standalone-${JUNIT_VERSION}.jar - URL_HASH SHA1=99245bde65d028a8b8ff604be26e929ab6ff2e58 + URL_HASH SHA256=e588d4dab5c8898b241c2a25938bf0b933ab77518626f14028cce403df7ce33d DOWNLOAD_NO_EXTRACT ON CONFIGURE_COMMAND "" BUILD_COMMAND "" @@ -60,4 +60,4 @@ if(JUnit_FOUND_SYSTEM) message(STATUS "Found JUnit: ${JUnit_JAR}") else() message(STATUS "Downloading JUnit: ${JUnit_JAR}") -endif() \ No newline at end of file +endif() diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake index 9cae199594f..2c52cab77b3 100644 --- a/cmake/FindKissat.cmake +++ b/cmake/FindKissat.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -49,14 +49,14 @@ if(NOT Kissat_FOUND_SYSTEM) fail_if_include_missing("sys/resource.h" "Kissat") set(Kissat_VERSION "sc2021") - set(Kissat_CHECKSUM "2541a45e023f51b39686865c40350ce091b5bd50") + set(Kissat_CHECKSUM "ad1945cc6980cc6d8b7049cf0a298f9f806ac3c9ca1ccb51f1bc533253d285cc") ExternalProject_Add( Kissat-EP ${COMMON_EP_CONFIG} BUILD_IN_SOURCE ON URL https://github.com/arminbiere/kissat/archive/${Kissat_VERSION}.tar.gz - URL_HASH SHA1=${Kissat_CHECKSUM} + URL_HASH SHA256=${Kissat_CHECKSUM} CONFIGURE_COMMAND /configure -fPIC --quiet CC=${CMAKE_C_COMPILER} INSTALL_COMMAND ${CMAKE_COMMAND} -E copy /build/libkissat.a @@ -88,4 +88,8 @@ if(Kissat_FOUND_SYSTEM) else() message(STATUS "Building Kissat ${Kissat_VERSION}: ${Kissat_LIBRARIES}") add_dependencies(Kissat Kissat-EP) + # Install static library only if it is a static build. + if(NOT BUILD_SHARED_LIBS) + install(FILES ${Kissat_LIBRARIES} TYPE ${LIB_BUILD_TYPE}) + endif() endif() diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index aba95bb3494..272dc7512a0 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindPip.cmake b/cmake/FindPip.cmake new file mode 100644 index 00000000000..aaa4e7e59de --- /dev/null +++ b/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-2025 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() \ No newline at end of file diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index 89b902f28d6..8914fdd2e5a 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Andres Noetzli, Vinícius Camillo +# Gereon Kremer, Andres Noetzli, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -163,19 +163,12 @@ if(NOT Poly_FOUND_SYSTEM) Poly-EP ${COMMON_EP_CONFIG} URL https://github.com/SRI-CSL/libpoly/archive/refs/tags/v${Poly_VERSION}.tar.gz - URL_HASH SHA1=981ff0081bed0d1e604000a3092e7af8881b7a5e + URL_HASH SHA256=ca7092eeeced3dd8bd86cdd3410207802ef1752d7052d92eee3e9e6bb496763c PATCH_COMMAND sed -i.orig "s,add_subdirectory(test/polyxx),add_subdirectory(test/polyxx EXCLUDE_FROM_ALL),g" /CMakeLists.txt - COMMAND - # LibPoly declares a variable `enabled_count` whose value is only written - # and never read. Newer versions of Clang throw a warning for this, which - # aborts the compilation when -Wall is enabled. - sed -i.orig - "/enabled_count/d" - /src/upolynomial/factorization.c - ${POLY_PATCH_CMD} + ${POLY_PATCH_CMD} CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX= -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} @@ -185,6 +178,7 @@ if(NOT Poly_FOUND_SYSTEM) -DGMP_INCLUDE_DIR=${GMP_INCLUDE_DIR} -DGMP_LIBRARY=${GMP_LIBRARIES} -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=TRUE + -DCMAKE_POLICY_VERSION_MINIMUM=3.5 BUILD_COMMAND ${CMAKE_MAKE_PROGRAM} ${POLY_TARGETS} ${POLY_INSTALL_CMD} BUILD_BYPRODUCTS ${POLY_BYPRODUCTS} @@ -242,4 +236,11 @@ else() # These libraries are required to compile a program that # uses the cvc5 static library. install(FILES ${BUILD_BYPRODUCTS} TYPE ${LIB_BUILD_TYPE}) + + if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE) + foreach(POLY_DYLIB ${BUILD_BYPRODUCTS}) + get_filename_component(POLY_DYLIB_NAME ${POLY_DYLIB} NAME) + update_rpath_macos(${POLY_DYLIB_NAME}) + endforeach() + endif() endif() diff --git a/cmake/FindRepairwheel.cmake b/cmake/FindRepairwheel.cmake new file mode 100644 index 00000000000..8953c6bb92d --- /dev/null +++ b/cmake/FindRepairwheel.cmake @@ -0,0 +1,123 @@ +############################################################################### +# Top contributors (to current version): +# Daniel Larraz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2025 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(get_repairwheel_version) + 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 + ERROR_QUIET + ) + else() + set(Repairwheel_VERSION_CHECK_RESULT 127) # Not-found exit code + endif() +endmacro() + +set(INSTALL_REQUIREWHEEL FALSE) + +get_repairwheel_version() + +if (Repairwheel_VERSION_CHECK_RESULT EQUAL 0) + set(Repairwheel_FOUND TRUE) + message(STATUS "Found repairwheel version: ${Repairwheel_VERSION}") + if (DEFINED Repairwheel_FIND_VERSION) + if (Repairwheel_FIND_VERSION_EXACT) + if (NOT (Repairwheel_VERSION VERSION_EQUAL ${Repairwheel_FIND_VERSION})) + set(INSTALL_REQUIREWHEEL TRUE) + set(INSTALL_REQUIREWHEEL_OPTION "==${Repairwheel_FIND_VERSION}") + set(INSTALL_REQUIREWHEEL_MESSAGE "==${Repairwheel_FIND_VERSION}") + endif() + else() + if (Repairwheel_VERSION VERSION_LESS ${Repairwheel_FIND_VERSION}) + set(INSTALL_REQUIREWHEEL TRUE) + set(INSTALL_REQUIREWHEEL_OPTION ";-U") + set(INSTALL_REQUIREWHEEL_MESSAGE ">=${Repairwheel_FIND_VERSION}") + endif() + endif() + if (INSTALL_REQUIREWHEEL AND NOT ENABLE_AUTO_DOWNLOAD) + set(INSTALL_REQUIREWHEEL FALSE) + message(${Repairwheel_FIND_MODE} + "Repairwheel version${INSTALL_REQUIREWHEEL_MESSAGE} is required, " + "but found version ${Repairwheel_VERSION}.\n" + "Use --auto-download to let us install it for you." + ) + endif() + endif() +else() + set(Repairwheel_FOUND FALSE) + if (NOT ENABLE_AUTO_DOWNLOAD) + message(${Repairwheel_FIND_MODE} + "Could NOT find repairwheel executable. " + "Use --auto-download to let us install it for you.") + else() + set(INSTALL_REQUIREWHEEL TRUE) + set(INSTALL_REQUIREWHEEL_OPTION ";-U") + set(INSTALL_REQUIREWHEEL_MESSAGE "") + endif() +endif() + +if(INSTALL_REQUIREWHEEL) + message(STATUS "Installing repairwheel${INSTALL_REQUIREWHEEL_MESSAGE}") + execute_process( + COMMAND + ${Python_EXECUTABLE} -m pip install repairwheel${INSTALL_REQUIREWHEEL_OPTION} + RESULT_VARIABLE REPAIRWHEEL_INSTALL_CMD_EXIT_CODE + ) + if(REPAIRWHEEL_INSTALL_CMD_EXIT_CODE) + message(${Repairwheel_FIND_MODE} + "Could NOT install repairwheel${INSTALL_REQUIREWHEEL_MESSAGE}" + ) + else() + set(Repairwheel_FOUND TRUE) + get_repairwheel_version() + endif() +endif() diff --git a/cmake/FindSetuptools.cmake b/cmake/FindSetuptools.cmake new file mode 100644 index 00000000000..f0a5e0fabce --- /dev/null +++ b/cmake/FindSetuptools.cmake @@ -0,0 +1,96 @@ +############################################################################### +# Top contributors (to current version): +# Daniel Larraz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2025 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 setuptools +# Setuptools_FOUND - found setuptools Python module +# Setuptools_VERSION - setuptools version +## + +if (Setuptools_FIND_REQUIRED) + set(Setuptools_FIND_MODE FATAL_ERROR) +else() + set(Setuptools_FIND_MODE STATUS) +endif() + +macro(get_setuptools_version) + execute_process( + COMMAND "${Python_EXECUTABLE}" -c "import setuptools; print(setuptools.__version__)" + RESULT_VARIABLE Setuptools_VERSION_CHECK_RESULT + OUTPUT_VARIABLE Setuptools_VERSION + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE + ) +endmacro() + +set(INSTALL_SETUPTOOLS FALSE) + +get_setuptools_version() + +if (Setuptools_VERSION_CHECK_RESULT EQUAL 0) + set(Setuptools_FOUND TRUE) + message(STATUS "Found setuptools version: ${Setuptools_VERSION}") + if (DEFINED Setuptools_FIND_VERSION) + if (Setuptools_FIND_VERSION_EXACT) + if (NOT (Setuptools_VERSION VERSION_EQUAL ${Setuptools_FIND_VERSION})) + set(INSTALL_SETUPTOOLS TRUE) + set(INSTALL_SETUPTOOLS_OPTION "==${Setuptools_FIND_VERSION}") + set(INSTALL_SETUPTOOLS_MESSAGE "==${Setuptools_FIND_VERSION}") + endif() + else() + # Setuptools v70.2.0 is broken on Windows. + # See https://github.com/pypa/distutils/issues/268 + # If v70.2.0 is installed, upgrade it to a newer version. + if (Setuptools_VERSION VERSION_LESS ${Setuptools_FIND_VERSION} OR + (WIN32 AND Setuptools_VERSION VERSION_EQUAL 70.2.0)) + set(INSTALL_SETUPTOOLS TRUE) + set(INSTALL_SETUPTOOLS_OPTION ";-U") + set(INSTALL_SETUPTOOLS_MESSAGE ">=${Setuptools_FIND_VERSION}") + endif() + endif() + if (INSTALL_SETUPTOOLS AND NOT ENABLE_AUTO_DOWNLOAD) + set(INSTALL_SETUPTOOLS FALSE) + message(${Setuptools_FIND_MODE} + "Setuptools version${INSTALL_SETUPTOOLS_MESSAGE} is required, " + "but found version ${Setuptools_VERSION}.\n" + "Use --auto-download to let us install it for you." + ) + endif() + endif() +else() + set(Setuptools_FOUND FALSE) + if (NOT ENABLE_AUTO_DOWNLOAD) + message(${Setuptools_FIND_MODE} + "Could NOT find the setuptools module. " + "Use --auto-download to let us install it for you.") + else() + set(INSTALL_SETUPTOOLS TRUE) + set(INSTALL_SETUPTOOLS_OPTION ";-U") + set(INSTALL_SETUPTOOLS_MESSAGE "") + endif() +endif() + +if(INSTALL_SETUPTOOLS) + message(STATUS "Installing setuptools${INSTALL_SETUPTOOLS_MESSAGE}") + execute_process( + COMMAND + ${Python_EXECUTABLE} -m pip install setuptools${INSTALL_SETUPTOOLS_OPTION} + RESULT_VARIABLE SETUPTOOLS_INSTALL_CMD_EXIT_CODE + ) + if(SETUPTOOLS_INSTALL_CMD_EXIT_CODE) + message(${Setuptools_FIND_MODE} + "Could NOT install setuptools${INSTALL_SETUPTOOLS_MESSAGE}" + ) + else() + set(Setuptools_FOUND TRUE) + get_setuptools_version() + endif() +endif() diff --git a/cmake/FindSphinx.cmake b/cmake/FindSphinx.cmake index 2cb844d99e5..215e1d00a75 100644 --- a/cmake/FindSphinx.cmake +++ b/cmake/FindSphinx.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 3173a659175..3c37c35c32e 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Aina Niemetz +# Gereon Kremer, Mathias Preiner, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -33,13 +33,13 @@ if(NOT SymFPU_FOUND_SYSTEM) include(deps-helper) set(SymFPU_COMMIT "e6ac3af9c2c574498ea171c957425b407625448b") - set(SymFPU_CHECKSUM "6ffc9009d2d665e0908edee634aa03bbbfc11482") + set(SymFPU_CHECKSUM "823aa663fcc2f6844ae5e9ea83ceda4ed393cdb3dadefce9b3c7c41cd0f4f702") ExternalProject_Add( SymFPU-EP ${COMMON_EP_CONFIG} URL https://github.com/cvc5/symfpu/archive/${SymFPU_COMMIT}.tar.gz - URL_HASH SHA1=${SymFPU_CHECKSUM} + URL_HASH SHA256=${SymFPU_CHECKSUM} CONFIGURE_COMMAND "" BUILD_COMMAND "" INSTALL_COMMAND ${CMAKE_COMMAND} -E copy_directory /core diff --git a/cmake/FindValgrind.cmake b/cmake/FindValgrind.cmake index d1481f5cf95..fc1642d89bc 100644 --- a/cmake/FindValgrind.cmake +++ b/cmake/FindValgrind.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index 4fe21941116..3f151367ea7 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -278,3 +278,12 @@ macro(copy_file_from_src filename) DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${filename} ) endmacro() + +macro(update_rpath_macos dylibname) + install(CODE "execute_process(COMMAND \${CMAKE_COMMAND} + -DRPATH=@loader_path + -DINSTALL_NAME_TOOL=${CMAKE_INSTALL_NAME_TOOL} + -DDYLIB_PATH=\${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/${dylibname} + -DDEPS_BASE=${DEPS_BASE} + -P ${CMAKE_SOURCE_DIR}/cmake/update_rpath_macos.cmake)") +endmacro() diff --git a/cmake/IWYU.cmake b/cmake/IWYU.cmake index fc204a57924..ab1769c58c9 100644 --- a/cmake/IWYU.cmake +++ b/cmake/IWYU.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake index 70c7702e188..b846fcb7314 100644 --- a/cmake/Toolchain-aarch64.cmake +++ b/cmake/Toolchain-aarch64.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andres Noetzli +# Gereon Kremer, Mathias Preiner, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake index fbf554bc5d8..5fcaf1235f6 100644 --- a/cmake/Toolchain-mingw64.cmake +++ b/cmake/Toolchain-mingw64.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in index 7ebec6c830c..1ab1cc513da 100644 --- a/cmake/cvc5Config.cmake.in +++ b/cmake/cvc5Config.cmake.in @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Mudathir Mohamed, Mathias Preiner +# Daniel Larraz, Aina Niemetz, Mudathir Mohamed # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -17,6 +17,11 @@ set(CVC5_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@) set(CVC5_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@) set(CVC5_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@) set(CVC5_USE_COCOA @USE_COCOA@) +set(CVC5_USE_CRYPTOMINISAT @USE_CRYPTOMINISAT@) + +if (CVC5_USE_CRYPTOMINISAT) + find_package(Threads REQUIRED) +endif() if(NOT TARGET cvc5::cvc5) include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake) diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake index 115fa4e1aed..2f61b9431d2 100644 --- a/cmake/deps-helper.cmake +++ b/cmake/deps-helper.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andrew V. Teylu +# Gereon Kremer, Mathias Preiner, Daniel Larraz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -107,7 +107,14 @@ macro(check_system_version name) if (${name}_FIND_VERSION) if(${name}_VERSION VERSION_LESS ${name}_FIND_VERSION) message(STATUS "System version for ${name} has incompatible \ -version: required ${${name}_FIND_VERSION} but found ${${name}_VERSION}") +version: minimum required ${${name}_FIND_VERSION} but found ${${name}_VERSION}") + set(${name}_FOUND_SYSTEM FALSE) + endif() + endif() + if (${name}_FIND_VERSION_MAX) + if(${name}_VERSION VERSION_GREATER ${name}_FIND_VERSION_MAX) + message(STATUS "System version for ${name} has incompatible \ +version: maximum required ${${name}_FIND_VERSION_MAX} but found ${${name}_VERSION}") set(${name}_FOUND_SYSTEM FALSE) endif() endif() diff --git a/cmake/deps-utils/CoCoALib-0.99800-trace.patch b/cmake/deps-utils/CoCoALib-0.99800-trace.patch index bacc855635b..a71fbe5f50d 100644 --- a/cmake/deps-utils/CoCoALib-0.99800-trace.patch +++ b/cmake/deps-utils/CoCoALib-0.99800-trace.patch @@ -1,3 +1,58 @@ +diff --git a/configuration/cxx14.sh b/configuration/cxx14.sh +index a5472cd..2a3e608 100755 +--- a/configuration/cxx14.sh ++++ b/configuration/cxx14.sh +@@ -51,7 +51,7 @@ int main() { + EOF + + # First try with no compiler flag... +-"$CXX" language-version.C -o language-version >> LogFile 2>& 1 ++"$CXX" $CXXFLAGS language-version.C -o language-version >> LogFile 2>& 1 + if [ $? -ne 0 ] + then + echo "ERROR: compilation unexpectedly failed; is $CXX a c++ compiler? $SCRIPT_NAME" > /dev/stderr +@@ -74,7 +74,7 @@ fi + # Compilation without flag is not C++14 standard; try with -std=c++14 + + CXX14="-std=c++14" +-"$CXX" $CXX14 language-version.C -o language-version >> LogFile 2>& 1 ++"$CXX" $CXXFLAGS $CXX14 language-version.C -o language-version >> LogFile 2>& 1 + if [ $? -ne 0 ] + then + echo "ERROR: compilation with flag $CXX14 failed $SCRIPT_NAME" > /dev/stderr +diff --git a/configuration/gmp-version.sh b/configuration/gmp-version.sh +index ebd85c7..5693280 100755 +--- a/configuration/gmp-version.sh ++++ b/configuration/gmp-version.sh +@@ -73,7 +73,7 @@ int main() + EOF + + # Use c++ compiler specified in CXX; no need to specify libgmp as all info is in header file!! +-$CXX -I"$COCOA_EXTLIB_DIR/include" test-gmp-version.C -o test-gmp-version > LogFile 2>&1 ++$CXX $CXXFLAGS -I"$COCOA_EXTLIB_DIR/include" test-gmp-version.C -o test-gmp-version > LogFile 2>&1 + + # Check whether compilation failed; if so, complain. + if [ $? -ne 0 ] +diff --git a/configuration/verify-compiler.sh b/configuration/verify-compiler.sh +index 7a70933..c752e34 100755 +--- a/configuration/verify-compiler.sh ++++ b/configuration/verify-compiler.sh +@@ -55,15 +55,6 @@ int main() + } + EOF + +-# Try plain compiler (without CXXFLAGS): +-$CXX test-compiler-gnu.C -o test-compiler-gnu > LogFile 2>&1 +-if [ $? -ne 0 -o \! -f test-compiler-gnu -o \! -x test-compiler-gnu ] +-then +- echo "ERROR: Are you sure \"$CXX\" is a C++ compiler? $SCRIPT_NAME" > /dev/stderr +- exit 1 +-fi +-/bin/rm test-compiler-gnu # not necessary, just being tidy :-) +- + # Try compiler with CXXFLAGS: + $CXX $CXXFLAGS test-compiler-gnu.C -o test-compiler-gnu > LogFile 2>&1 + if [ $? -ne 0 -o \! -f test-compiler-gnu -o \! -x test-compiler-gnu ] diff --git a/configuration/shell-fns.sh b/configuration/shell-fns.sh index 190dbb4..c8d281f 100755 --- a/configuration/shell-fns.sh diff --git a/cmake/deps-utils/cocoa-test.cpp b/cmake/deps-utils/cocoa-test.cpp new file mode 100644 index 00000000000..96f890e5eea --- /dev/null +++ b/cmake/deps-utils/cocoa-test.cpp @@ -0,0 +1,23 @@ +/****************************************************************************** + * Top contributors (to current version): + * Daniel Larraz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2025 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. + * **************************************************************************** + * + * Checks whether CoCoA has been patched. + */ +#include +#include + +int main() +{ + std::cout << "CoCoA::handlersEnabled = "; + std::cout << CoCoA::handlersEnabled << std::endl; + return 0; +} \ No newline at end of file diff --git a/contrib/glpk-cut-log.patch b/cmake/deps-utils/glpk-cut-log.patch similarity index 77% rename from contrib/glpk-cut-log.patch rename to cmake/deps-utils/glpk-cut-log.patch index c8409f7bb37..4919b19ebf7 100644 --- a/contrib/glpk-cut-log.patch +++ b/cmake/deps-utils/glpk-cut-log.patch @@ -1,11 +1,11 @@ -%% This patch is taken from https://github.com/timothy-king/glpk-cut-log and -%% has the following license: -%% -%% GLPK is free software: you can redistribute it and/or modify it under the -%% terms of the GNU General Public License as published by the Free Software -%% Foundation, either version 3 of the License, or (at your option) any later -%% version. -%% +@@ This patch is taken from https://github.com/timothy-king/glpk-cut-log and +@@ has the following license: +@@ +@@ GLPK is free software: you can redistribute it and/or modify it under the +@@ terms of the GNU General Public License as published by the Free Software +@@ Foundation, either version 3 of the License, or (at your option) any later +@@ version. +@@ From cf84e3855d8c5676557daaca434b42b2fc17dc29 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 14 Dec 2013 16:03:35 -0500 @@ -73,10 +73,10 @@ Updating the installation instructions. --- diff --git a/configure.ac b/configure.ac -index cbdb724..ba642ba 100644 +index bbc8929..0bc64d1 100644 --- a/configure.ac +++ b/configure.ac -@@ -6,7 +6,7 @@ AC_CONFIG_SRCDIR([src/glpk.h]) +@@ -5,7 +5,7 @@ AC_CONFIG_SRCDIR([src/glpk.h]) AC_CONFIG_MACRO_DIR([m4]) @@ -86,30 +86,39 @@ index cbdb724..ba642ba 100644 AC_CONFIG_HEADERS([config.h]) diff --git a/src/Makefile.am b/src/Makefile.am -index 48dff15..d04b547 100644 +index b39efa6..2a025bc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am -@@ -27,6 +27,7 @@ libglpk_la_LDFLAGS = \ - ${NOUNDEFINED} +@@ -20,7 +20,10 @@ libglpk_la_LDFLAGS = \ + -version-info 36:0:1 \ + -export-symbols-regex '^glp_*' ++ ++# all of the cut log sources are listed first libglpk_la_SOURCES = \ +cutlog01.c \ - amd/amd_1.c \ - amd/amd_2.c \ - amd/amd_aat.c \ + glpapi01.c \ + glpapi02.c \ + glpapi03.c \ diff --git a/src/cutlog01.c b/src/cutlog01.c new file mode 100644 -index 0000000..c8818df +index 0000000..9a85bb7 --- /dev/null +++ b/src/cutlog01.c -@@ -0,0 +1,446 @@ +@@ -0,0 +1,452 @@ +/* cutlog01.c (api extension routines) */ + -+#include "env.h" -+#include "ios.h" -+#include "npp.h" -+#include "glpk.h" -+#include "ios.h" ++ ++#include "glpapi.h" ++#include "glpios.h" ++ ++int glp_get_it_cnt(glp_prob *P){ ++ if(P == NULL){ ++ return 0; ++ }else{ ++ return P->it_cnt; ++ } ++} + +int glp_ios_get_cut(glp_tree *T, int i, int* ind, double* val, int* klass, int* type, double* rhs){ + xassert(T != NULL); @@ -549,23 +558,23 @@ index 0000000..c8818df + } + return tree->num_deleting_rows; +} -diff --git a/src/draft/glpapi06.c b/src/draft/glpapi06.c -index 635662e..ad6d55a 100644 ---- a/src/draft/glpapi06.c -+++ b/src/draft/glpapi06.c -@@ -524,6 +524,7 @@ void glp_init_smcp(glp_smcp *parm) - parm->shift = GLP_ON; - parm->aorn = GLP_USE_NT; - #endif +diff --git a/src/glpapi06.c b/src/glpapi06.c +index 743d6be..05d0498 100644 +--- a/src/glpapi06.c ++++ b/src/glpapi06.c +@@ -488,6 +488,7 @@ void glp_init_smcp(glp_smcp *parm) + parm->out_frq = 500; + parm->out_dly = 0; + parm->presolve = GLP_OFF; + parm->stability_lmt = 200; return; } -diff --git a/src/draft/glpapi13.c b/src/draft/glpapi13.c -index 0ca2adf..c5d4af6 100644 ---- a/src/draft/glpapi13.c -+++ b/src/draft/glpapi13.c -@@ -451,8 +451,14 @@ void glp_ios_row_attr(glp_tree *tree, int i, glp_attr *attr) +diff --git a/src/glpapi13.c b/src/glpapi13.c +index 926dda4..55adf44 100644 +--- a/src/glpapi13.c ++++ b/src/glpapi13.c +@@ -453,8 +453,14 @@ void glp_ios_row_attr(glp_tree *tree, int i, glp_attr *attr) int glp_ios_pool_size(glp_tree *tree) { /* determine current size of the cut pool */ @@ -580,24 +589,15 @@ index 0ca2adf..c5d4af6 100644 + xerror("glp_ios_pool_size: operation not allowed\n"); + } xassert(tree->local != NULL); - #ifdef NEW_LOCAL /* 02/II-2018 */ - return tree->local->m; -diff --git a/src/draft/ios.h b/src/draft/ios.h -index e2b47c6..2e61fdc 100644 ---- a/src/draft/ios.h -+++ b/src/draft/ios.h -@@ -24,7 +24,7 @@ - - #include "prob.h" - --#if 1 /* 02/II-2018 */ -+#if 0 /* 02/II-2018 */ /* cvc5; NEW_LOCAL is not compatible with cut logging */ - #define NEW_LOCAL 1 - #endif - -@@ -46,6 +46,9 @@ typedef struct IOSPOOL IOSPOOL; + return tree->local->size; + } +diff --git a/src/glpios.h b/src/glpios.h +index 9e2d6b2..3b31901 100644 +--- a/src/glpios.h ++++ b/src/glpios.h +@@ -36,6 +36,9 @@ typedef struct IOSAIJ IOSAIJ; + typedef struct IOSPOOL IOSPOOL; typedef struct IOSCUT IOSCUT; - #endif + +typedef struct IOSAUX IOSAUX; @@ -605,7 +605,7 @@ index e2b47c6..2e61fdc 100644 struct glp_tree { /* branch-and-bound tree */ int magic; -@@ -223,6 +226,19 @@ struct glp_tree +@@ -217,6 +220,19 @@ struct glp_tree GLP_NO_BRNCH - use general selection technique */ int child; /* subproblem reference number corresponding to br_sel */ @@ -625,7 +625,7 @@ index e2b47c6..2e61fdc 100644 }; struct IOSLOT -@@ -235,6 +251,8 @@ struct IOSLOT +@@ -229,6 +245,8 @@ struct IOSLOT struct IOSNPD { /* node subproblem descriptor */ @@ -634,15 +634,19 @@ index e2b47c6..2e61fdc 100644 int p; /* subproblem reference number (it is the index to corresponding slot, i.e. slot[p] points to this descriptor) */ -@@ -406,9 +424,47 @@ struct IOSCUT - /* pointer to previous cut */ - IOSCUT *next; - /* pointer to next cut */ +@@ -393,12 +411,51 @@ struct IOSCUT + GLP_FX: sum a[j] * x[j] = b */ + double rhs; + /* cut right-hand side */ + + IOSAUX *aux; + /* cut auxillary source information */ ++ + IOSCUT *prev; + /* pointer to previous cut */ + IOSCUT *next; + /* pointer to next cut */ }; - #endif +struct IOSAUX +{ @@ -682,7 +686,7 @@ index e2b47c6..2e61fdc 100644 #define ios_create_tree _glp_ios_create_tree glp_tree *ios_create_tree(glp_prob *mip, const glp_iocp *parm); /* create branch-and-bound tree */ -@@ -539,6 +595,31 @@ int ios_choose_node(glp_tree *T); +@@ -615,6 +672,31 @@ int ios_choose_node(glp_tree *T); int ios_choose_var(glp_tree *T, int *next); /* select variable to branch on */ @@ -714,11 +718,11 @@ index e2b47c6..2e61fdc 100644 #endif /* eof */ -diff --git a/src/draft/glpios01.c b/src/draft/glpios01.c -index f1ee43a..f32867d 100644 ---- a/src/draft/glpios01.c -+++ b/src/draft/glpios01.c -@@ -175,6 +175,16 @@ glp_tree *ios_create_tree(glp_prob *mip, const glp_iocp *parm) +diff --git a/src/glpios01.c b/src/glpios01.c +index 70798fd..d9e5703 100644 +--- a/src/glpios01.c ++++ b/src/glpios01.c +@@ -159,6 +159,16 @@ glp_tree *ios_create_tree(glp_prob *mip, const glp_iocp *parm) tree->stop = 0; /* create the root subproblem, which initially is identical to the original MIP */ @@ -735,7 +739,7 @@ index f1ee43a..f32867d 100644 new_node(tree, NULL); return tree; } -@@ -294,6 +304,7 @@ void ios_revive_node(glp_tree *tree, int p) +@@ -278,6 +288,7 @@ void ios_revive_node(glp_tree *tree, int p) double *val; ind = xcalloc(1+n, sizeof(int)); val = xcalloc(1+n, sizeof(double)); @@ -743,7 +747,7 @@ index f1ee43a..f32867d 100644 for (r = node->r_ptr; r != NULL; r = r->next) { i = glp_add_rows(mip, 1); glp_set_row_name(mip, i, r->name); -@@ -473,6 +484,13 @@ void ios_freeze_node(glp_tree *tree) +@@ -457,6 +468,13 @@ void ios_freeze_node(glp_tree *tree) double *val; ind = xcalloc(1+n, sizeof(int)); val = xcalloc(1+n, sizeof(double)); @@ -757,7 +761,7 @@ index f1ee43a..f32867d 100644 for (i = m; i > pred_m; i--) { GLPROW *row = mip->row[i]; IOSROW *r; -@@ -517,6 +535,8 @@ void ios_freeze_node(glp_tree *tree) +@@ -501,6 +519,8 @@ void ios_freeze_node(glp_tree *tree) xassert(nrs > 0); num = xcalloc(1+nrs, sizeof(int)); for (i = 1; i <= nrs; i++) num[i] = root_m + i; @@ -766,7 +770,7 @@ index f1ee43a..f32867d 100644 glp_del_rows(mip, nrs, num); xfree(num); } -@@ -652,6 +672,9 @@ static IOSNPD *new_node(glp_tree *tree, IOSNPD *parent) +@@ -636,6 +656,9 @@ static IOSNPD *new_node(glp_tree *tree, IOSNPD *parent) tree->a_cnt++; tree->n_cnt++; tree->t_cnt++; @@ -776,7 +780,7 @@ index f1ee43a..f32867d 100644 /* increase the number of child subproblems */ if (parent == NULL) xassert(p == 1); -@@ -834,6 +857,8 @@ void ios_delete_tree(glp_tree *tree) +@@ -818,6 +841,8 @@ void ios_delete_tree(glp_tree *tree) xassert(nrs > 0); num = xcalloc(1+nrs, sizeof(int)); for (i = 1; i <= nrs; i++) num[i] = tree->orig_m + i; @@ -785,7 +789,7 @@ index f1ee43a..f32867d 100644 glp_del_rows(mip, nrs, num); xfree(num); } -@@ -1477,6 +1502,7 @@ int ios_add_row(glp_tree *tree, IOSPOOL *pool, +@@ -1417,6 +1442,7 @@ int ios_add_row(glp_tree *tree, IOSPOOL *pool, cut->rhs = rhs; cut->prev = pool->tail; cut->next = NULL; @@ -793,7 +797,7 @@ index f1ee43a..f32867d 100644 if (cut->prev == NULL) pool->head = cut; else -@@ -1591,6 +1617,11 @@ void ios_del_row(glp_tree *tree, IOSPOOL *pool, int i) +@@ -1517,6 +1543,11 @@ void ios_del_row(glp_tree *tree, IOSPOOL *pool, int i) cut->ptr = aij->next; dmp_free_atom(tree->pool, aij, sizeof(IOSAIJ)); } @@ -805,7 +809,7 @@ index f1ee43a..f32867d 100644 dmp_free_atom(tree->pool, cut, sizeof(IOSCUT)); pool->size--; return; -@@ -1624,6 +1655,10 @@ void ios_clear_pool(glp_tree *tree, IOSPOOL *pool) +@@ -1535,6 +1566,10 @@ void ios_clear_pool(glp_tree *tree, IOSPOOL *pool) cut->ptr = aij->next; dmp_free_atom(tree->pool, aij, sizeof(IOSAIJ)); } @@ -816,16 +820,11 @@ index f1ee43a..f32867d 100644 dmp_free_atom(tree->pool, cut, sizeof(IOSCUT)); } pool->size = 0; -@@ -@@ glpios08 was split into src/cglib/{cfg2.c, clqcut.c} in GLPK 4.59 -@@ -@@ This code applies against glpios03 around GLPK 4.65. -@@ -diff --git a/src/draft/glpios03.c b/src/draft/glpios03.c -index 2c1180f..ec1da44 100644 ---- a/src/draft/glpios03.c -+++ b/src/draft/glpios03.c -@@ -359,12 +394,12 @@ static void fix_by_red_cost(glp_tree *T) +diff --git a/src/glpios03.c b/src/glpios03.c +index 80d701b..03e9208 100644 +--- a/src/glpios03.c ++++ b/src/glpios03.c +@@ -358,12 +358,12 @@ static void fix_by_red_cost(glp_tree *T) * 2 - both branches are hopeless and have been pruned; new subproblem * selection is needed to continue the search. */ @@ -840,7 +839,7 @@ index 2c1180f..ec1da44 100644 double lb, ub, beta, new_ub, new_lb, dn_lp, up_lp, dn_bnd, up_bnd; /* determine bounds and value of x[j] in optimal solution to LP relaxation of the current subproblem */ -@@ -432,6 +467,7 @@ static int branch_on(glp_tree *T, int j, int next) +@@ -431,6 +431,7 @@ static int branch_on(glp_tree *T, int j, int next) else xassert(mip != mip); ret = 1; @@ -848,7 +847,7 @@ index 2c1180f..ec1da44 100644 goto done; } else if (dn_bad) -@@ -450,6 +486,7 @@ static int branch_on(glp_tree *T, int j, int next) +@@ -449,6 +450,7 @@ static int branch_on(glp_tree *T, int j, int next) else xassert(mip != mip); ret = 1; @@ -856,40 +855,7 @@ index 2c1180f..ec1da44 100644 goto done; } /* both down- and up-branches seem to be hopeful */ -@@ -650,8 +687,16 @@ static void gmi_gen(glp_tree *T) - val = xcalloc(1+P->n, sizeof(double)); - for (i = 1; i <= pool->m; i++) - { len = glp_get_mat_row(pool, i, ind, val); - glp_ios_add_row(T, NULL, GLP_RF_GMI, 0, len, ind, val, - GLP_LO, pool->row[i]->lb); -+ -+ /** callback for a cut being added to the cut pool */ -+ if (T->parm->cb_func != NULL) -+ { xassert(T->reason == GLP_ICUTGEN); -+ T->reason = GLP_ICUTADDED; -+ T->parm->cb_func(T, T->parm->cb_info); -+ T->reason = GLP_ICUTGEN; -+ } - } - xfree(ind); - xfree(val); -@@ -728,6 +773,15 @@ static void clq_gen(glp_tree *T, glp_cfg *G) - if (len > 0) - glp_ios_add_row(T, NULL, GLP_RF_CLQ, 0, len, ind, val, GLP_UP, - val[0]); -+ -+ /** callback for a cut being added to the cut pool */ -+ if (T->parm->cb_func != NULL) -+ { xassert(T->reason == GLP_ICUTGEN); -+ T->reason = GLP_ICUTADDED; -+ T->parm->cb_func(T, T->parm->cb_info); -+ T->reason = GLP_ICUTGEN; -+ } -+ - tfree(ind); - tfree(val); - return; -@@ -814,7 +868,8 @@ static void remove_cuts(glp_tree *T) +@@ -702,7 +704,8 @@ static void remove_cuts(glp_tree *T) } } if (cnt > 0) @@ -899,7 +865,7 @@ index 2c1180f..ec1da44 100644 #if 0 xprintf("%d inactive cut(s) removed\n", cnt); #endif -@@ -896,6 +951,7 @@ static void display_cut_info(glp_tree *T) +@@ -784,6 +787,7 @@ static void display_cut_info(glp_tree *T) int ios_driver(glp_tree *T) { int p, curr_p, p_stat, d_stat, ret; @@ -907,7 +873,7 @@ index 2c1180f..ec1da44 100644 #if 1 /* carry out to glp_tree */ int pred_p = 0; /* if the current subproblem has been just created due to -@@ -1164,6 +1220,12 @@ more: /* minor loop starts here */ +@@ -1010,6 +1014,12 @@ more: /* minor loop starts here */ if (T->parm->msg_lev >= GLP_MSG_DBG) xprintf("LP relaxation has no feasible solution\n"); /* prune the branch */ @@ -920,7 +886,7 @@ index 2c1180f..ec1da44 100644 goto fath; } else -@@ -1398,6 +1460,14 @@ more: /* minor loop starts here */ +@@ -1219,6 +1229,14 @@ more: /* minor loop starts here */ ios_process_cuts(T); T->reason = 0; } @@ -935,7 +901,7 @@ index 2c1180f..ec1da44 100644 /* clear the local cut pool */ ios_clear_pool(T, T->local); /* perform re-optimization, if necessary */ -@@ -1442,7 +1512,34 @@ more: /* minor loop starts here */ +@@ -1255,7 +1273,34 @@ more: /* minor loop starts here */ T->br_var = ios_choose_var(T, &T->br_sel); /* perform actual branching */ curr_p = T->curr->p; @@ -971,57 +937,37 @@ index 2c1180f..ec1da44 100644 T->br_var = T->br_sel = 0; if (ret == 0) { /* both branches have been created */ -diff --git a/src/intopt/covgen.c b/src/intopt/covgen.c -index 986cf88..bfe708c 100644 ---- a/src/intopt/covgen.c -+++ b/src/intopt/covgen.c -@@ -572,14 +572,14 @@ glp_cov *glp_cov_init(glp_prob *P) - /* the set of "0-1 knapsack" inequalities has been built */ - if (csa.set->m == 0) - { /* the set is empty */ -- xprintf("No 0-1 knapsack inequalities detected\n"); -+ /* xprintf("No 0-1 knapsack inequalities detected\n"); */ - cov = NULL; - glp_delete_prob(csa.set); - } - else - { /* create the cover cut generator working area */ -- xprintf("Number of 0-1 knapsack inequalities = %d\n", -- csa.set->m); -+ /* xprintf("Number of 0-1 knapsack inequalities = %d\n", -+ csa.set->m); */ - cov = talloc(1, glp_cov); - cov->n = P->n; - cov->set = csa.set; -%% -%% glpios05 was split into src/cglib/{gmicut.c, gmigen.c} -%% in GLPK 4.59 -%% -%% src/cglib was renamed into src/intopt in GLPK 4.65 -%% -diff --git a/src/intopt/gmicut.c b/src/intopt/gmicut.c -index ae75a8c..61b2fda 100644 ---- a/src/intopt/gmicut.c -+++ b/src/intopt/gmicut.c -@@ -21,6 +21,7 @@ - - #include "env.h" - #include "prob.h" -+#include "ios.h" - - /*********************************************************************** - * NAME -@@ -104,6 +105,9 @@ int glp_gmi_cut(glp_prob *P, int j, - GLPAIJ *aij; +diff --git a/src/glpios05.c b/src/glpios05.c +index b9322b9..caf69d7 100644 +--- a/src/glpios05.c ++++ b/src/glpios05.c +@@ -65,6 +65,9 @@ static void gen_cut(glp_tree *tree, struct worka *worka, int j) + double *phi = worka->phi; int i, k, len, kind, stat; double lb, ub, alfa, beta, ksi, phi1, rhs; + int input_j; + input_j = j; + - /* sanity checks */ - if (!(P->m == 0 || P->valid)) - { /* current basis factorization is not valid */ -@@ -202,6 +206,7 @@ int glp_gmi_cut(glp_prob *P, int j, + /* compute row of the simplex tableau, which (row) corresponds + to specified basic variable xB[i] = x[m+j]; see (23) */ + len = glp_eval_tab_row(mip, m+j, ind, val); +@@ -73,6 +76,7 @@ static void gen_cut(glp_tree *tree, struct worka *worka, int j) + if it would be computed with formula (27); it is assumed that + beta[i] is fractional enough */ + beta = mip->col[j]->prim; ++ + /* compute cut coefficients phi and right-hand side rho, which + correspond to formula (30); dense format is used, because rows + of the simplex tableau is usually dense */ +@@ -104,6 +108,7 @@ static void gen_cut(glp_tree *tree, struct worka *worka, int j) + xassert(stat != GLP_BS); + /* determine row coefficient ksi[i,j] at xN[j]; see (23) */ + ksi = val[j]; ++ /* printf("%d %4.15f ", k, ksi); */ + /* if ksi[i,j] is too large in the magnitude, do not generate + the cut */ + if (fabs(ksi) > 1e+05) goto fini; +@@ -135,6 +140,7 @@ static void gen_cut(glp_tree *tree, struct worka *worka, int j) /* y[j] is integer */ if (fabs(alfa - floor(alfa + 0.5)) < 1e-10) { /* alfa[i,j] is close to nearest integer; skip it */ @@ -1029,7 +975,7 @@ index ae75a8c..61b2fda 100644 goto skip; } else if (f(alfa) <= f(beta)) -@@ -237,6 +242,13 @@ int glp_gmi_cut(glp_prob *P, int j, +@@ -170,6 +176,13 @@ static void gen_cut(glp_tree *tree, struct worka *worka, int j) } skip: ; } @@ -1041,14 +987,19 @@ index ae75a8c..61b2fda 100644 + /* printf("\n"); */ + /* now the cut has the form sum_k phi[k] * x[k] >= rho, where cut - * coefficients are stored in the array phi in dense format; - * x[1,...,m] are auxiliary variables, x[m+1,...,m+n] are struc- -@@ -276,6 +288,17 @@ skip: ; - rhs = 0.0; - ind[0] = 0, val[0] = rhs; - /* the cut has been successfully generated */ -+ -+ glp_tree *tree = P->tree; + coefficients are stored in the array phi in dense format; + x[1,...,m] are auxiliary variables, x[m+1,...,m+n] are struc- +@@ -218,8 +231,20 @@ skip: ; + ios_add_cut_row(tree, pool, GLP_RF_GMI, len, ind, val, GLP_LO, + rhs); + #else +- glp_ios_add_row(tree, NULL, GLP_RF_GMI, 0, len, ind, val, GLP_LO, +- rhs); ++ int ord; ++ ord = glp_ios_add_row(tree, NULL, GLP_RF_GMI, 0, len, ind, val, ++ GLP_LO, rhs); ++ ios_cut_set_single_aux(tree, ord, input_j); ++ + /* printf("ord: % d beta %f\n", ord, beta); */ + + /** callback for a cut being added to the cut pool */ @@ -1058,14 +1009,14 @@ index ae75a8c..61b2fda 100644 + tree->parm->cb_func(tree, tree->parm->cb_info); + tree->reason = GLP_ICUTGEN; + } - return len; + #endif + fini: return; } - -diff --git a/src/intopt/mirgen.c b/src/intopt/mirgen.c -index 4467189..4b03dcb 100644 ---- a/src/intopt/mirgen.c -+++ b/src/intopt/mirgen.c -@@ -123,6 +123,29 @@ struct glp_mir +diff --git a/src/glpios06.c b/src/glpios06.c +index 2bd0453..4bd3cf5 100644 +--- a/src/glpios06.c ++++ b/src/glpios06.c +@@ -100,6 +100,29 @@ struct MIR /* sparse vector of cutting plane coefficients, alpha[k] */ double cut_rhs; /* right-hand size of the cutting plane, beta */ @@ -1095,7 +1046,7 @@ index 4467189..4b03dcb 100644 }; /*********************************************************************** -@@ -166,6 +189,7 @@ static void set_row_attrib(glp_prob *mip, glp_mir *mir) +@@ -146,6 +169,7 @@ static void set_row_attrib(glp_tree *tree, struct MIR *mir) xassert(row != row); } mir->vlb[k] = mir->vub[k] = 0; @@ -1103,7 +1054,7 @@ index 4467189..4b03dcb 100644 } return; } -@@ -200,6 +224,7 @@ static void set_col_attrib(glp_prob *mip, glp_mir *mir) +@@ -181,6 +205,7 @@ static void set_col_attrib(glp_tree *tree, struct MIR *mir) xassert(col != col); } mir->vlb[k] = mir->vub[k] = 0; @@ -1111,7 +1062,7 @@ index 4467189..4b03dcb 100644 } return; } -@@ -248,6 +273,7 @@ static void set_var_bounds(glp_prob *mip, glp_mir *mir) +@@ -230,6 +255,7 @@ static void set_var_bounds(glp_tree *tree, struct MIR *mir) { /* set variable lower bound for x1 */ mir->lb[k1] = - a2 / a1; mir->vlb[k1] = k2; @@ -1119,7 +1070,7 @@ index 4467189..4b03dcb 100644 /* the row should not be used */ mir->skip[i] = 1; } -@@ -258,6 +284,7 @@ static void set_var_bounds(glp_prob *mip, glp_mir *mir) +@@ -240,6 +266,7 @@ static void set_var_bounds(glp_tree *tree, struct MIR *mir) { /* set variable upper bound for x1 */ mir->ub[k1] = - a2 / a1; mir->vub[k1] = k2; @@ -1127,10 +1078,10 @@ index 4467189..4b03dcb 100644 /* the row should not be used */ mir->skip[i] = 1; } -@@ -329,6 +356,13 @@ glp_mir *glp_mir_init(glp_prob *mip) +@@ -313,6 +340,13 @@ void *ios_mir_init(glp_tree *tree) mir->subst = xcalloc(1+m+n, sizeof(char)); - mir->mod_vec = spv_create_vec(m+n); - mir->cut_vec = spv_create_vec(m+n); + mir->mod_vec = ios_create_vec(m+n); + mir->cut_vec = ios_create_vec(m+n); + + /* added */ + mir->cut_cset = xcalloc(1+m+n, sizeof(char)); @@ -1139,9 +1090,9 @@ index 4467189..4b03dcb 100644 + mir->agg_coeffs = xcalloc(1+MAXAGGR, sizeof(double)); + /* set global row attributes */ - set_row_attrib(mip, mir); + set_row_attrib(tree, mir); /* set global column attributes */ -@@ -426,6 +460,9 @@ static void initial_agg_row(glp_prob *mip, glp_mir *mir, int i) +@@ -405,6 +439,9 @@ static void initial_agg_row(glp_tree *tree, struct MIR *mir, int i) mir->skip[i] = 2; mir->agg_cnt = 1; mir->agg_row[1] = i; @@ -1150,8 +1101,8 @@ index 4467189..4b03dcb 100644 + /* use x[i] - sum a[i,j] * x[m+j] = 0, where x[i] is auxiliary variable of row i, x[m+j] are structural variables */ - spv_clear_vec(mir->agg_vec); -@@ -805,19 +842,19 @@ static int CDECL cmir_cmp(const void *p1, const void *p2) + ios_clear_vec(mir->agg_vec); +@@ -784,19 +821,19 @@ static int cmir_cmp(const void *p1, const void *p2) static double cmir_sep(const int n, const double a[], const double b, const double u[], const double x[], const double s, @@ -1176,7 +1127,7 @@ index 4467189..4b03dcb 100644 for (j = 1; j <= n; j++) { xassert(a[j] != 0.0); /* if x[j] is close to its bounds, skip it */ -@@ -830,16 +867,16 @@ static double cmir_sep(const int n, const double a[], const double b, +@@ -809,16 +846,16 @@ static double cmir_sep(const int n, const double a[], const double b, /* compute violation */ r = - (*beta) - (*gamma) * s; for (k = 1; k <= n; k++) r += alpha[k] * x[k]; @@ -1198,7 +1149,7 @@ index 4467189..4b03dcb 100644 for (j = 1; j <= 3; j++) { /* construct c-MIR inequality */ fail = cmir_ineq(n, a, b, u, cset, d_try[j], alpha, beta, -@@ -848,7 +885,7 @@ static double cmir_sep(const int n, const double a[], const double b, +@@ -827,7 +864,7 @@ static double cmir_sep(const int n, const double a[], const double b, /* compute violation */ r = - (*beta) - (*gamma) * s; for (k = 1; k <= n; k++) r += alpha[k] * x[k]; @@ -1207,7 +1158,7 @@ index 4467189..4b03dcb 100644 } /* build subset of variables lying strictly between their bounds and order it by nondecreasing values of |x[j] - u[j]/2| */ -@@ -870,7 +907,7 @@ static double cmir_sep(const int n, const double a[], const double b, +@@ -849,7 +886,7 @@ static double cmir_sep(const int n, const double a[], const double b, /* replace x[j] by its complement or vice versa */ cset[j] = (char)!cset[j]; /* construct c-MIR inequality */ @@ -1216,7 +1167,7 @@ index 4467189..4b03dcb 100644 /* restore the variable */ cset[j] = (char)!cset[j]; /* do not replace the variable in case of failure */ -@@ -881,10 +918,11 @@ static double cmir_sep(const int n, const double a[], const double b, +@@ -860,10 +897,11 @@ static double cmir_sep(const int n, const double a[], const double b, if (r_best < r) r_best = r, cset[j] = (char)!cset[j]; } /* construct the best c-MIR inequality chosen */ @@ -1230,17 +1181,17 @@ index 4467189..4b03dcb 100644 xfree(vset); /* return to the calling routine */ return r_best; -@@ -895,7 +933,8 @@ static double generate(glp_mir *mir) +@@ -874,7 +912,8 @@ static double generate(struct MIR *mir) int m = mir->m; int n = mir->n; int j, k, kk, nint; - double s, *u, *x, *alpha, r_best = 0.0, b, beta, gamma; + double s, *u, *x, *alpha, r_best = 0.0, b, beta, gamma, delta; + char *cset; - spv_copy_vec(mir->cut_vec, mir->mod_vec); + ios_copy_vec(mir->cut_vec, mir->mod_vec); mir->cut_rhs = mir->mod_rhs; /* remove small terms, which can appear due to substitution of -@@ -944,6 +983,7 @@ static double generate(glp_mir *mir) +@@ -923,6 +962,7 @@ static double generate(struct MIR *mir) u = xcalloc(1+nint, sizeof(double)); x = xcalloc(1+nint, sizeof(double)); alpha = xcalloc(1+nint, sizeof(double)); @@ -1248,7 +1199,23 @@ index 4467189..4b03dcb 100644 /* determine u and x */ for (j = 1; j <= nint; j++) { k = mir->cut_vec->ind[j]; -@@ -1010,7 +1050,7 @@ static double generate(glp_mir *mir) +@@ -936,6 +976,7 @@ static double generate(struct MIR *mir) + x[j] = mir->ub[k] - mir->x[k]; + else + xassert(k != k); ++ if(!(x[j] >= -0.001)) { goto skip; } + xassert(x[j] >= -0.001); + if (x[j] < 0.0) x[j] = 0.0; + } +@@ -965,6 +1006,7 @@ static double generate(struct MIR *mir) + } + else + xassert(k != k); ++ if(!(x >= -0.001)) { goto skip; } + xassert(x >= -0.001); + if (x < 0.0) x = 0.0; + s -= mir->cut_vec->val[j] * x; +@@ -973,7 +1015,7 @@ static double generate(struct MIR *mir) /* apply heuristic to obtain most violated c-MIR inequality */ b = mir->cut_rhs; r_best = cmir_sep(nint, mir->cut_vec->val, b, u, x, s, alpha, @@ -1257,9 +1224,9 @@ index 4467189..4b03dcb 100644 if (r_best == 0.0) goto skip; xassert(r_best > 0.0); /* convert to raw cut */ -@@ -1025,10 +1065,22 @@ static double generate(glp_mir *mir) - #if MIR_DEBUG - spv_check_vec(mir->cut_vec); +@@ -988,10 +1030,22 @@ static double generate(struct MIR *mir) + #if _MIR_DEBUG + ios_check_vec(mir->cut_vec); #endif + /* added */ + mir->cut_delta = delta; @@ -1280,7 +1247,7 @@ index 4467189..4b03dcb 100644 done: return r_best; } -@@ -1236,8 +1288,25 @@ static void add_cut(glp_mir *mir, glp_prob *pool) +@@ -1199,8 +1253,25 @@ static void add_cut(glp_tree *tree, struct MIR *mir) ios_add_cut_row(tree, pool, GLP_RF_MIR, len, ind, val, GLP_UP, mir->cut_rhs); #else @@ -1305,32 +1272,32 @@ index 4467189..4b03dcb 100644 + tree->reason = GLP_ICUTGEN; + } #endif - #else - { int i; -@@ -1265,6 +1334,7 @@ static int aggregate_row(glp_prob *mip, glp_mir *mir, SPV *v) - #endif + xfree(ind); + xfree(val); +@@ -1216,6 +1287,7 @@ static int aggregate_row(glp_tree *tree, struct MIR *mir) + IOSVEC *v; int ii, j, jj, k, kk, kappa = 0, ret = 0; double d1, d2, d, d_max = 0.0; + double guass_coeff; /* choose appropriate structural variable in the aggregated row to be substituted */ for (j = 1; j <= mir->agg_vec->nnz; j++) -@@ -1369,8 +1439,9 @@ static int aggregate_row(glp_prob *mip, glp_mir *mir, SPV *v) +@@ -1300,8 +1372,9 @@ static int aggregate_row(glp_tree *tree, struct MIR *mir) xassert(j != 0); jj = v->pos[kappa]; xassert(jj != 0); -- spv_linear_comb(mir->agg_vec, +- ios_linear_comb(mir->agg_vec, - - mir->agg_vec->val[j] / v->val[jj], v); + guass_coeff = - mir->agg_vec->val[j] / v->val[jj]; + mir->agg_coeffs[mir->agg_cnt] = guass_coeff; -+ spv_linear_comb(mir->agg_vec, guass_coeff, v); - #if 0 /* 29/II-2016 by Chris */ ++ ios_linear_comb(mir->agg_vec, guass_coeff, v); ios_delete_vec(v); - #endif -@@ -1520,6 +1591,13 @@ void glp_mir_free(glp_mir *mir) + ios_set_vj(mir->agg_vec, kappa, 0.0); + #if _MIR_DEBUG +@@ -1440,6 +1513,13 @@ void ios_mir_term(void *gen) xfree(mir->subst); - spv_delete_vec(mir->mod_vec); - spv_delete_vec(mir->cut_vec); + ios_delete_vec(mir->mod_vec); + ios_delete_vec(mir->cut_vec); + + /* added */ + xfree(mir->cut_cset); @@ -1341,11 +1308,11 @@ index 4467189..4b03dcb 100644 xfree(mir); return; } -diff --git a/src/draft/glpios07.c b/src/draft/glpios07.c -index b8e700e..a246634 100644 ---- a/src/draft/glpios07.c -+++ b/src/draft/glpios07.c -@@ -537,6 +537,14 @@ void ios_cov_gen(glp_tree *tree) +diff --git a/src/glpios07.c b/src/glpios07.c +index 0892550..9f742e6 100644 +--- a/src/glpios07.c ++++ b/src/glpios07.c +@@ -543,6 +543,14 @@ void ios_cov_gen(glp_tree *tree) /* add the cut to the cut pool */ glp_ios_add_row(tree, NULL, GLP_RF_COV, 0, len, ind, val, GLP_UP, val[0]); @@ -1360,11 +1327,31 @@ index b8e700e..a246634 100644 } /* free working arrays */ xfree(ind); -diff --git a/src/draft/glpios11.c b/src/draft/glpios11.c -index e23b97f..13978d1 100644 ---- a/src/draft/glpios11.c -+++ b/src/draft/glpios11.c -@@ -324,6 +324,9 @@ void ios_process_cuts(glp_tree *T) +diff --git a/src/glpios08.c b/src/glpios08.c +index 2d2fcd5..3aad808 100644 +--- a/src/glpios08.c ++++ b/src/glpios08.c +@@ -129,6 +129,15 @@ void ios_clq_gen(glp_tree *T, void *G_) + /* add cut inequality to local cut pool */ + glp_ios_add_row(T, NULL, GLP_RF_CLQ, 0, len, ind, val, GLP_UP, + rhs); ++ ++ /** callback for a cut being added to the cut pool */ ++ if (T->parm->cb_func != NULL) ++ { xassert(T->reason == GLP_ICUTGEN); ++ T->reason = GLP_ICUTADDED; ++ T->parm->cb_func(T, T->parm->cb_info); ++ T->reason = GLP_ICUTGEN; ++ } ++ + skip: /* free working arrays */ + tfree(ind); + tfree(val); +diff --git a/src/glpios11.c b/src/glpios11.c +index c40e9a5..82d5698 100644 +--- a/src/glpios11.c ++++ b/src/glpios11.c +@@ -193,6 +193,9 @@ void ios_process_cuts(glp_tree *T) glp_set_mat_row(T->mip, i, len, ind, val); xassert(cut->type == GLP_LO || cut->type == GLP_UP); glp_set_row_bnds(T->mip, i, cut->type, cut->rhs, cut->rhs); @@ -1375,18 +1362,18 @@ index e23b97f..13978d1 100644 /* free working arrays */ xfree(info); diff --git a/src/glpk.h b/src/glpk.h -index ea79ec2..5034199 100644 +index 75c292c..e117782 100644 --- a/src/glpk.h +++ b/src/glpk.h -@@ -140,6 +140,7 @@ typedef struct - int aorn; /* option to use A or N: */ - #define GLP_USE_AT 1 /* use A matrix in row-wise format */ - #define GLP_USE_NT 2 /* use N matrix in row-wise format */ +@@ -130,6 +130,7 @@ typedef struct + int out_frq; /* spx.out_frq */ + int out_dly; /* spx.out_dly (milliseconds) */ + int presolve; /* enable/disable using LP presolver */ + int stability_lmt; /* maximum number of check stability failures before stopping */ - double foo_bar[33]; /* (reserved) */ - #endif + double foo_bar[36]; /* (reserved) */ } glp_smcp; -@@ -238,6 +239,11 @@ typedef struct + +@@ -229,6 +230,11 @@ typedef struct #define GLP_IBRANCH 0x05 /* request for branching */ #define GLP_ISELECT 0x06 /* request for subproblem selection */ #define GLP_IPREPRO 0x07 /* request for preprocessing */ @@ -1398,7 +1385,7 @@ index ea79ec2..5034199 100644 /* branch selection indicator: */ #define GLP_NO_BRNCH 0 /* select no branch */ -@@ -1164,6 +1170,54 @@ int glp_top_sort(glp_graph *G, int v_num); +@@ -1057,6 +1063,54 @@ int glp_top_sort(glp_graph *G, int v_num); int glp_wclique_exact(glp_graph *G, int v_wgt, double *sol, int v_set); /* find maximum weight clique with exact algorithm */ @@ -1453,81 +1440,89 @@ index ea79ec2..5034199 100644 #ifdef __cplusplus } #endif -%% -%% Primal simplex method was reimplemented in 4.56 -%% -diff --git a/src/simplex/spxprim.c b/src/simplex/spxprim.c -index d004197..31a1c7b 100644 ---- a/src/simplex/spxprim.c -+++ b/src/simplex/spxprim.c -@@ -182,6 +182,10 @@ struct csa - int ns_cnt, ls_cnt; - /* normal and long-step iteration counts */ - #endif +diff --git a/src/glpspx01.c b/src/glpspx01.c +index 5c17114..caaab27 100644 +--- a/src/glpspx01.c ++++ b/src/glpspx01.c +@@ -238,6 +238,9 @@ struct csa + double *work2; /* double work2[1+m]; */ + double *work3; /* double work3[1+m]; */ + double *work4; /* double work4[1+m]; */ + + /** Things Tim has added. */ + int stability_failures; -+ int stability_lmt; }; - /*********************************************************************** -@@ -1213,6 +1217,11 @@ loop: /* main loop starts here */ - if (perturb <= 0) - { if (check_feas(csa, csa->phase, tol_bnd, tol_bnd1)) - { /* excessive bound violations due to round-off errors */ -+ csa->stability_failures++; -+ if (csa->stability_failures >= csa->stability_lmt){ -+ ret = GLP_EINSTAB; -+ goto fini; -+ } - #if 1 /* 01/VII-2017 */ - if (perturb < 0) - { if (msg_lev >= GLP_MSG_ALL) -@@ -1760,6 +1769,8 @@ int spx_primal(glp_prob *P, const glp_smcp *parm) - #if 1 /* 23/VI-2017 */ - csa->ns_cnt = csa->ls_cnt = 0; - #endif -+ csa->stability_failures = 0; -+ csa->stability_lmt = parm->stability_lmt; - /* try to solve working LP */ - ret = primal_simplex(csa); - /* return basis factorization back to problem object */ -%% -%% Dual simplex method was reimplemented in 4.57 -%% -diff --git a/src/simplex/spydual.c b/src/simplex/spydual.c -index 770b621..f04afa7 100644 ---- a/src/simplex/spydual.c -+++ b/src/simplex/spydual.c -@@ -197,6 +197,10 @@ struct csa - int ns_cnt, ls_cnt; - /* normal and long-step iteration count */ - #endif + static const double kappa = 0.10; +@@ -400,6 +403,8 @@ static void init_csa(struct csa *csa, glp_prob *lp) + csa->refct = 0; + memset(&refsp[1], 0, (m+n) * sizeof(char)); + for (j = 1; j <= n; j++) gamma[j] = 1.0; + -+ /** Things Tim has added. */ ++ csa->stability_failures = 0; + return; + } + +@@ -2647,6 +2652,11 @@ loop: /* main loop starts here */ + if (check_stab(csa, parm->tol_bnd)) + { /* there are excessive bound violations due to round-off + errors */ ++ csa->stability_failures++; ++ if (csa->stability_failures >= parm->stability_lmt){ ++ ret = GLP_EINSTAB; ++ goto done; ++ } + if (parm->msg_lev >= GLP_MSG_ERR) + xprintf("Warning: numerical instability (primal simplex," + " phase %s)\n", csa->phase == 1 ? "I" : "II"); +diff --git a/src/glpspx02.c b/src/glpspx02.c +index 19152a6..de3d677 100644 +--- a/src/glpspx02.c ++++ b/src/glpspx02.c +@@ -288,6 +288,9 @@ struct csa + double *work2; /* double work2[1+m]; */ + double *work3; /* double work3[1+m]; */ + double *work4; /* double work4[1+m]; */ ++ ++ /* count the number of stability failures */ + int stability_failures; -+ int stability_lmt; }; - /*********************************************************************** -@@ -1329,6 +1333,11 @@ loop: /* main loop starts here */ - { if (check_feas(csa, tol_dj, tol_dj1, 0)) - { /* dual feasibility is broken due to excessive round-off - * errors */ -+ csa->stability_failures++; -+ if (csa->stability_failures >= csa->stability_lmt){ -+ ret = GLP_EINSTAB; -+ goto fini; -+ } - if (perturb < 0) - { if (msg_lev >= GLP_MSG_ALL) - xprintf("Perturbing LP to avoid instability [%d].." -@@ -2004,6 +2013,8 @@ int spy_dual(glp_prob *P, const glp_smcp *parm) - #if 1 /* 23/III-2016 */ - csa->ns_cnt = csa->ls_cnt = 0; - #endif + static const double kappa = 0.10; +@@ -501,6 +504,8 @@ static void init_csa(struct csa *csa, glp_prob *lp) + csa->refct = 0; + memset(&refsp[1], 0, (m+n) * sizeof(char)); + for (i = 1; i <= m; i++) gamma[i] = 1.0; ++ + csa->stability_failures = 0; -+ csa->stability_lmt = parm->stability_lmt; - /* try to solve working LP */ - ret = dual_simplex(csa); - /* return basis factorization back to problem object */ + return; + } + +@@ -2741,7 +2746,13 @@ loop: /* main loop starts here */ + /* make sure that the current basic solution remains dual + feasible */ + if (check_stab(csa, parm->tol_dj) != 0) +- { if (parm->msg_lev >= GLP_MSG_ERR) ++ { ++ csa->stability_failures++; ++ if (csa->stability_failures >= parm->stability_lmt){ ++ ret = GLP_EINSTAB; ++ goto done; ++ } ++ if (parm->msg_lev >= GLP_MSG_ERR) + xprintf("Warning: numerical instability (dual simplex, p" + "hase %s)\n", csa->phase == 1 ? "I" : "II"); + #if 1 +@@ -3023,6 +3034,10 @@ loop: /* main loop starts here */ + /* accuracy check based on the pivot element */ + { double piv1 = csa->tcol_vec[csa->p]; /* more accurate */ + double piv2 = csa->trow_vec[csa->q]; /* less accurate */ ++ if(piv1 == 0.0){ ++ ret = GLP_EFAIL; ++ goto done; ++ } + xassert(piv1 != 0.0); + if (fabs(piv1 - piv2) > 1e-8 * (1.0 + fabs(piv1)) || + !(piv1 > 0.0 && piv2 > 0.0 || piv1 < 0.0 && piv2 < 0.0)) +-- +2.26.2 diff --git a/cmake/deps-utils/gmp-test.cpp b/cmake/deps-utils/gmp-test.cpp index 05ccc2694b1..ce653601604 100644 --- a/cmake/deps-utils/gmp-test.cpp +++ b/cmake/deps-utils/gmp-test.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2025 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. diff --git a/cmake/fuzzing-murxla.cmake b/cmake/fuzzing-murxla.cmake index bc5b1a2026a..7fe8f84e6d5 100644 --- a/cmake/fuzzing-murxla.cmake +++ b/cmake/fuzzing-murxla.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. @@ -28,7 +28,7 @@ ExternalProject_Add( EXCLUDE_FROM_ALL ON ${COMMON_EP_CONFIG} URL https://github.com/murxla/murxla/archive/${Murxla_COMMIT}.tar.gz - URL_HASH SHA1=176e325344a94250c4f4f6df3a9d2d01d6529a26 + URL_HASH SHA256=b3ae1042ff9887d91db1eee990c32be5cbebe809e0350f8b3b3e334a4c6bd0d9 SOURCE_DIR ${CMAKE_BINARY_DIR}/murxla CMAKE_ARGS -DCMAKE_PREFIX_PATH=${CMAKE_BINARY_DIR}/murxla-install/usr/local/ diff --git a/cmake/install_python_wheel.cmake b/cmake/install_python_wheel.cmake new file mode 100644 index 00000000000..ce238548c0e --- /dev/null +++ b/cmake/install_python_wheel.cmake @@ -0,0 +1,53 @@ +############################################################################### +# Top contributors (to current version): +# Daniel Larraz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2025 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. +# ############################################################################# +# +# Build, repair, and install a cvc5 Python wheel +# +# This script first removes any existing wheel build directories, +# builds an initial Python wheel, repairs the wheel to include +# all required shared library dependencies, and finally prepares +# an installation command to install the repaired wheel. +# +# Input variables: +# Python_EXECUTABLE - Path to the Python executable +# Repairwheel_EXECUTABLE - Path to the repairwheel tool +# BUILD_DIR - Path to the cvc5 build directory +# DEPS_BASE - Path to the cvc5 dependencies directory +# INSTALL_CMD - Command to install the wheel +## +set(UNREPAIRED_WHEEL_DIR ${BUILD_DIR}/unrepaired-wheel) +set(REPAIRED_WHEEL_DIR ${BUILD_DIR}/repaired-wheel) + +execute_process(COMMAND + ${CMAKE_COMMAND} -E remove_directory ${UNREPAIRED_WHEEL_DIR} ${REPAIRED_WHEEL_DIR}) + +execute_process(COMMAND + ${Python_EXECUTABLE} -m pip wheel ${BUILD_DIR}/src/api/python + --wheel-dir=${BUILD_DIR}/unrepaired-wheel) + +file(GLOB WHL_FILE ${UNREPAIRED_WHEEL_DIR}/cvc5*.whl) + +execute_process(COMMAND + ${Repairwheel_EXECUTABLE} -o ${BUILD_DIR}/repaired-wheel + -l ${BUILD_DIR}/src -l ${BUILD_DIR}/src/parser + -l ${DEPS_BASE}/bin ${WHL_FILE}) + +file(GLOB WHL_FILE ${REPAIRED_WHEEL_DIR}/cvc5*.whl) + +set(INSTALL_CMD "${INSTALL_CMD} ${WHL_FILE}") +string(REPLACE "\"" "" INSTALL_CMD "${INSTALL_CMD}") +if(WIN32) + string(REPLACE "/" "\\" INSTALL_CMD "${INSTALL_CMD}") +endif() +separate_arguments(INSTALL_CMD) + +execute_process(COMMAND ${INSTALL_CMD}) diff --git a/cmake/target-graphs.cmake b/cmake/target-graphs.cmake index 471c1d23677..75a869d3dad 100644 --- a/cmake/target-graphs.cmake +++ b/cmake/target-graphs.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/cmake/update_rpath_macos.cmake b/cmake/update_rpath_macos.cmake new file mode 100644 index 00000000000..13ea30a53ff --- /dev/null +++ b/cmake/update_rpath_macos.cmake @@ -0,0 +1,81 @@ +############################################################################### +# Top contributors (to current version): +# Daniel Larraz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2025 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. +# ############################################################################# +# +# Update the RPATH of a macOS dynamic library to make it relocatable +# +# This script updates RPATH if not already set, replaces ${DEPS_BASE}/lib with +# @rpath in the install name and in the paths of all library dependencies to +# ensure the dynamic library is relocatable. +# +# Input variables: +# RPATH - The rpath to use in the dynamic library +# INSTALL_NAME_TOOL - Path to the install_name tool +# DYLIB_PATH - Path to the dynamic library +# DEPS_BASE - Path to the cvc5 dependencies directory +## +# If RPATH is provided, add it unless it already exists +if(RPATH) + # otool -l output is in the format: + # cmd LC_RPATH + # cmdsize XX + # path (offset YY) + execute_process( + COMMAND otool -l "${DYLIB_PATH}" + COMMAND grep LC_RPATH -A2 + OUTPUT_VARIABLE RPATH_OUTPUT + ) + if(NOT "${RPATH_OUTPUT}" MATCHES "${RPATH}") + execute_process( + COMMAND ${INSTALL_NAME_TOOL} -add_rpath ${RPATH} ${DYLIB_PATH} + ) + endif() +endif() + +# Get install name +execute_process( + COMMAND otool -D "${DYLIB_PATH}" + OUTPUT_VARIABLE INSTALL_NAME_OUTPUT + OUTPUT_STRIP_TRAILING_WHITESPACE +) +# otool -D output is in the format: +# libname.dylib: +# /full/path/to/libname.n.dylib +# Extract the second line which contains the actual install name +string(REPLACE "\n" ";" INSTALL_NAME_LIST "${INSTALL_NAME_OUTPUT}") +list(GET INSTALL_NAME_LIST 1 INSTALL_NAME) + +if("${INSTALL_NAME}" MATCHES "${DEPS_BASE}/lib") + # Replace ${DEPS_BASE}/lib with @rpath + string(REPLACE "${DEPS_BASE}/lib" "@rpath" NEW_INSTALL_NAME "${INSTALL_NAME}") + execute_process( + COMMAND ${INSTALL_NAME_TOOL} -id ${NEW_INSTALL_NAME} ${DYLIB_PATH} + ) +endif() + +# Get all dependencies and replace ${DEPS_BASE}/lib with @rpath +execute_process( + COMMAND otool -L ${DYLIB_PATH} + OUTPUT_VARIABLE OTOOL_OUTPUT + OUTPUT_STRIP_TRAILING_WHITESPACE +) +string(REPLACE "\n" ";" OTOOL_LINES "${OTOOL_OUTPUT}") +# Discard the first line which is the path to ${DYLIB_PATH} +list(REMOVE_AT OTOOL_LINES 0) +foreach(LINE ${OTOOL_LINES}) + if(LINE MATCHES "${DEPS_BASE}/lib/") + string(REGEX REPLACE "^[ \t]*([^ \t]+).*" "\\1" LIB_PATH "${LINE}") + string(REPLACE "${DEPS_BASE}/lib" "@rpath" LIB_RPATH "${LIB_PATH}") + execute_process( + COMMAND ${INSTALL_NAME_TOOL} -change ${LIB_PATH} ${LIB_RPATH} ${DYLIB_PATH} + ) + endif() +endforeach() \ No newline at end of file diff --git a/cmake/version-base.cmake b/cmake/version-base.cmake index c68b6b5e372..0b793c0980b 100644 --- a/cmake/version-base.cmake +++ b/cmake/version-base.cmake @@ -1,5 +1,5 @@ # These are updated when making a release -set(CVC5_LAST_RELEASE "1.1.2") +set(CVC5_LAST_RELEASE "1.2.1") set(CVC5_IS_RELEASE "false") # These are used in other places in cmake diff --git a/cmake/version.cmake b/cmake/version.cmake index 0f0cf037a22..0a46abb4da3 100644 --- a/cmake/version.cmake +++ b/cmake/version.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2025 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. diff --git a/configure.sh b/configure.sh index 784c6569dda..c52441e649c 100755 --- a/configure.sh +++ b/configure.sh @@ -9,10 +9,15 @@ Usage: $0 [] [