diff --git a/.github/actions/add-package/action.yml b/.github/actions/add-package/action.yml index 0a82e3f4792..dbddfa8c2dc 100644 --- a/.github/actions/add-package/action.yml +++ b/.github/actions/add-package/action.yml @@ -89,7 +89,9 @@ runs: for cnt,asset in enumerate(assets): delete = False - if cnt >= 32: + # 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 diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml index e4f2e1432e8..b4431185e50 100644 --- a/.github/actions/configure-and-build/action.yml +++ b/.github/actions/configure-and-build/action.yml @@ -5,6 +5,8 @@ inputs: default: "" configure-config: default: "" + macos-target: + default: "" build-shared: default: true type: boolean @@ -25,6 +27,11 @@ outputs: runs: using: composite steps: + - name: Set MACOSX_DEPLOYMENT_TARGET + if: runner.os == 'macOS' && inputs.macos-target + shell: ${{ inputs.shell }} + run: echo "MACOSX_DEPLOYMENT_TARGET=${{ inputs.macos-target }}" >> $GITHUB_ENV + - name: Shared build id: shared-build # Boolean inputs are actually strings: @@ -34,11 +41,14 @@ runs: run: | echo "::group::Shared build" ${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \ - --prefix=$(pwd)/build-shared/install --werror --name=build-shared + --prefix=$(pwd)/build-shared/install --werror --name=build-shared \ + -DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache - # can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10 cd build-shared/ && pwd=$(pwd) - if [[ "$RUNNER_OS" != "Windows" ]]; then + 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 @@ -56,10 +66,14 @@ 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 --no-java-bindings \ + -DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache cd build-static/ && pwd=$(pwd) - if [[ "$RUNNER_OS" != "Windows" ]]; then + 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 @@ -73,9 +87,16 @@ runs: echo "::endgroup::" - name: Reset ccache base_dir - if: runner.os != 'Windows' shell: ${{ inputs.shell }} run: | echo "::group::Reset ccache base_dir" - $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir =" $CCACHE_CONFIGPATH + 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 echo "::endgroup::" + + - name: ccache Statistics + shell: ${{ inputs.shell }} + run: ccache -s diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml index 588bde9d252..4ce474c4232 100644 --- a/.github/actions/install-dependencies/action.yml +++ b/.github/actions/install-dependencies/action.yml @@ -32,7 +32,16 @@ runs: libfl-dev echo "SED=sed" >> $GITHUB_ENV echo "CCACHE_CONFIGPATH=/home/runner/.ccache/ccache.conf" >> $GITHUB_ENV - echo "/usr/lib/ccache" >> $GITHUB_PATH + echo "::endgroup::" + + - name: Install software for cross-compiling for arm64 Linux + if: runner.os == 'Linux' + shell: ${{ inputs.shell }} + run: | + echo "::group::Install software for cross-compiling for arm64 Linux" + sudo apt-get install -y \ + gcc-aarch64-linux-gnu \ + g++-aarch64-linux-gnu echo "::endgroup::" - name: Install software for cross-compiling for Windows @@ -61,6 +70,7 @@ runs: path-type: inherit install: | make + mingw-w64-x86_64-ccache mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp @@ -85,21 +95,29 @@ runs: brew install \ ccache \ - gmp \ 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 "/usr/local/opt/ccache/libexec" >> $GITHUB_PATH + echo "::endgroup::" + + # Required by PEP-668 + - name: Set up Python virtual environment + if: runner.os == 'macOS' + shell: ${{ inputs.shell }} + run: | + echo "::group::Set up Python virtual environment" + python3 -m venv ~/.venv + echo "$HOME/.venv/bin" >> $GITHUB_PATH echo "::endgroup::" - name: Install Python modules for building and testing shell: ${{ inputs.shell }} run: | echo "::group::Install Python modules for building and testing" - python3 -m pip install --user -r contrib/requirements_build.txt - python3 -m pip install --user pexpect # For interactive shell tests + python3 -m pip install -r contrib/requirements_build.txt + python3 -m pip install pexpect # For interactive shell tests echo "::endgroup::" - name: Install software for Python bindings @@ -108,9 +126,7 @@ runs: run: | echo "::group::Install software for Python bindings" python3 -m pip install -q --upgrade pip - python3 -m pip install --user -r contrib/requirements_python_dev.txt - # Add binary path of user site-packages to PATH - echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH + python3 -m pip install -r contrib/requirements_python_dev.txt echo "::endgroup::" - name: Install software for Python packaging @@ -119,8 +135,8 @@ runs: run: | echo "::group::Install software for Python packaging" python3 -m pip install -q --upgrade pip - python3 -m pip install --user twine - python3 -m pip install --user -U urllib3 requests + python3 -m pip install twine + python3 -m pip install -U urllib3 requests echo "::endgroup::" - name: Install software for documentation @@ -129,7 +145,7 @@ runs: run: | echo "::group::Install software for documentation" sudo apt-get install -y doxygen python3-docutils python3-jinja2 - python3 -m pip install --user \ + 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 diff --git a/.github/actions/package-python-wheel-macos/action.yml b/.github/actions/package-python-wheel-macos/action.yml deleted file mode 100644 index 78edc63b10a..00000000000 --- a/.github/actions/package-python-wheel-macos/action.yml +++ /dev/null @@ -1,26 +0,0 @@ -name: Package python wheel for macOS -description: Package cvc5 into a python wheel on macOS for one python version -inputs: - python-version: - default: "" - config: - default: "" - platform: - default: "" -runs: - using: composite - steps: - - uses: actions/setup-python@v5 - if: runner.os == 'macOS' - with: - python-version: ${{ inputs.python-version }} - - - name: Build wheel - shell: bash - if: runner.os == 'macOS' - run: | - echo "::group::Build macOS wheel for ${{ inputs.python-version }}" - ./contrib/packaging_python/mk_clean_wheel.sh python "${{ inputs.config }}" ${{ inputs.platform }} - - ls *.whl - echo "::endgroup::" diff --git a/.github/actions/package-python-wheel/action.yml b/.github/actions/package-python-wheel/action.yml deleted file mode 100644 index ca6877ddbaa..00000000000 --- a/.github/actions/package-python-wheel/action.yml +++ /dev/null @@ -1,150 +0,0 @@ -name: Package python wheels -description: Package cvc5 into python wheels for all supported python versions -inputs: - upload-to-pypi: - default: false - upload-to-test-pypi: - default: false - pypi-token: - default: "" - test-pypi-token: - default: "" - config: - default: "" - platform: - default: "" -runs: - using: composite - steps: - - name: Build wheels for Linux - if: runner.os == 'Linux' - shell: bash - run: | - echo "::group::Create docker image" - if ! docker image inspect pycvc5-manylinux2014 > /dev/null 2>&1; then - echo "Need to build docker image" - docker build -q -t pycvc5-manylinux2014 contrib/packaging_python/manylinux2014 - fi - echo "::endgroup::" - - OPTS="${{ inputs.config }}" - for version in cp37 cp38 cp39 cp310 cp311 cp312 pp37 pp38 pp39 pp310 - do - echo "::group::Build extension for python $version" - docker run --rm \ - -v `pwd`:/home/pycvc5 \ - pycvc5-manylinux2014 \ - ./contrib/packaging_python/mk_clean_wheel.sh /opt/python/${version}*/bin/python "$OPTS" - echo "::endgroup::" - done - - ls *.whl - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.7' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.8' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.9' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.10' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.11' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: '3.12' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: 'pypy-3.7' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: 'pypy-3.8' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: 'pypy-3.9' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Build wheels for macOS - if: runner.os == 'macOS' - uses: ./.github/actions/package-python-wheel-macos - with: - python-version: 'pypy-3.10' - config: ${{ inputs.config }} - platform: ${{ inputs.platform }} - - - name: Upload wheels to pypi.org - if: inputs.upload-to-pypi == 'true' - shell: bash - env: - TWINE_USERNAME: __token__ - TWINE_PASSWORD: ${{ inputs.pypi-token }} - run: | - echo "::group::Upload to pypi.org" - for wheel in `ls *.whl` - do - twine upload $wheel - done - echo "::endgroup::" - - - name: Upload wheels to test.pypi.org - if: inputs.upload-to-test-pypi == 'true' - shell: bash - env: - TWINE_USERNAME: __token__ - TWINE_PASSWORD: ${{ inputs.test-pypi-token }} - run: | - echo "::group::Upload to test.pypi.org" - for wheel in `ls *.whl` - do - twine upload --repository testpypi $wheel - done - echo "::endgroup::" - diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index ae0ddb55b91..750c5310bbb 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -13,12 +13,15 @@ inputs: default: "" regressions-exclude: default: "3-4" + shell: + default: bash runs: using: composite steps: - name: Run CTest - shell: bash + shell: ${{ inputs.shell }} run: | + cd ${{ inputs.build-dir }} make -j${{ env.num_proc }} build-tests if ! ctest -j${{ env.num_proc }} --output-on-failure -LE regress[${{ inputs.regressions-exclude }}] then @@ -27,30 +30,36 @@ runs: env: CVC5_REGRESSION_ARGS: --no-early-exit RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }} - working-directory: ${{ inputs.build-dir }} - name: Install Check - shell: bash + shell: ${{ inputs.shell }} run: | if [[ "${{ inputs.check-install }}" != "true" ]]; then exit 0; fi + cd ${{ inputs.build-dir }} make -j${{ env.num_proc }} install - echo -e "#include \nint main() { cvc5::Solver s; return 0; }" > /tmp/test.cpp + echo "#include " > /tmp/test.cpp + echo "using namespace cvc5;" >> /tmp/test.cpp + echo "int main() { TermManager tm; Solver s(tm); return 0; }" >> /tmp/test.cpp g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5 - working-directory: ${{ inputs.build-dir }} - name: Python Install Check - shell: bash + 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*')))" python3 -c "import cvc5" - name: Check Examples - shell: bash + shell: ${{ inputs.shell }} run: | if [[ "${{ inputs.check-examples }}" != "true" ]]; then exit 0; fi + cd examples mkdir -p build && cd build - cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake + if [[ "$RUNNER_OS" == "Windows" ]]; then + export PATH="${{ inputs.build-dir }}/install/lib:$PATH" + export CMAKE_GENERATOR="MSYS Makefiles" + fi + cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake \ + -DPython_EXECUTABLE=$(command -v python3) make -j${{ env.num_proc }} ctest -j${{ env.num_proc }} --output-on-failure - working-directory: examples diff --git a/.github/actions/setup-cache/action.yml b/.github/actions/setup-cache/action.yml index a879a2d8934..44d58856410 100644 --- a/.github/actions/setup-cache/action.yml +++ b/.github/actions/setup-cache/action.yml @@ -35,7 +35,6 @@ runs: using: composite steps: - name: Setup ccache cache - if: runner.os != 'Windows' uses: actions/cache@v4 with: path: ccache-dir @@ -43,10 +42,9 @@ runs: restore-keys: ${{ inputs.cache-key }}-${{ runner.os }}-ccache- - name: Configure ccache - if: runner.os != 'Windows' shell: ${{ inputs.shell }} run: | - ccache --set-config=cache_dir=${{ github.workspace }}/ccache-dir + ccache --set-config=cache_dir="${{ github.workspace }}/ccache-dir" ccache --set-config=compression=true ccache --set-config=compression_level=6 ccache -M 500M @@ -56,14 +54,13 @@ runs: id: contrib-cache uses: actions/cache@v4 with: - path: deps/install + path: deps/bin key: ${{ inputs.cache-key }}-${{ runner.os }}-contrib-${{ hashFiles('contrib/get-**') }}-${{ hashFiles('.github/**') }} - name: Install contrib dependencies + if: steps.contrib-cache.outputs.cache-hit != 'true' shell: ${{ inputs.shell }} - run: | - if [[ "${{ steps.contrib-cache.outputs.cache-hit }}" == "true" ]]; then exit 0; fi - ./contrib/get-alf-checker + run: ./contrib/get-alf-checker - name: Setup dependencies cache uses: actions/cache@v4 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0b9cc7a6c5e..998987467c3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,42 +23,54 @@ jobs: 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-11 - config: production --auto-download --all-bindings --editline + 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 + 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-11 + os: macos-13 config: production --auto-download --all-bindings --editline --arm64 cache-key: production-arm64-cross strip-bin: strip python-bindings: true - package-name: cvc5-macOS-arm64 - name: win64:production - os: windows-2019 - config: production --auto-download --win64-native + os: windows-latest + config: production --auto-download cache-key: production-win64-native strip-bin: strip windows-build: true shell: 'msys2 {0}' + check-examples: true + exclude_regress: 1-4 + run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - name: win64:production-cross os: ubuntu-latest @@ -69,7 +81,7 @@ jobs: package-name: cvc5-Win64 - name: ubuntu:production-clang - os: ubuntu-latest + os: ubuntu-20.04 env: CC=clang CXX=clang++ config: production --auto-download --no-poly cache-key: productionclang @@ -78,7 +90,7 @@ jobs: run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump - name: ubuntu:production-dbg - os: ubuntu-latest + os: ubuntu-20.04 config: production --auto-download --assertions --tracing --unit-testing --all-bindings --editline --cocoa cache-key: dbg exclude_regress: 3-4 @@ -86,12 +98,12 @@ jobs: python-bindings: true - name: ubuntu:production-dbg-clang - os: ubuntu-latest + 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 base --tester model --tester synth --tester abduct --tester unsat-core --tester dump + 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 }} @@ -125,15 +137,12 @@ jobs: 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: ccache Statistics - if: runner.os != 'Windows' - run: ccache -s - - name: Run tests if: matrix.run_regression_args uses: ./.github/actions/run-tests @@ -143,6 +152,7 @@ jobs: 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 @@ -154,6 +164,7 @@ jobs: check-python-bindings: false regressions-args: ${{ matrix.run_regression_args }} regressions-exclude: 1-4 + shell: ${{ matrix.shell }} - name: Build documentation if: matrix.build-documentation @@ -188,7 +199,7 @@ jobs: group: update-pr steps: - name: Automatically update PR - uses: adRise/update-pr-branch@v0.6.0 + uses: adRise/update-pr-branch@v0.7.2 with: token: ${{ secrets.ACTION_USER_TOKEN }} base: 'main' diff --git a/.github/workflows/package_pypi.yml b/.github/workflows/package_pypi.yml index c9e38bba504..811cdfcdb9e 100644 --- a/.github/workflows/package_pypi.yml +++ b/.github/workflows/package_pypi.yml @@ -8,62 +8,133 @@ on: name: PyPi packaging jobs: - build: + 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 - config: production --auto-download - cache-key: cvc5-pypi + arch: x86_64 + shell: bash + - name: manylinux-aarch64 + os: ubuntu-latest + arch: aarch64 + shell: bash - name: macos-x86_64 - os: macos-11 - config: production --auto-download - cache-key: cvc5-pypi - platform: macosx_11_0_x86_64 + os: macos-13 + macos-target: 10.13 + shell: bash - name: macos-arm64 - os: macos-11 - config: production --auto-download --arm64 - cache-key: cvc5-pypi-arm64 - platform: macosx_11_0_arm64 - - name: ${{ matrix.name }} - runs-on: ${{ matrix.os }} - if: (github.repository == 'cvc5/cvc5') || (github.event_name != 'schedule') + 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 - - name: Install dependencies - uses: ./.github/actions/install-dependencies - if: runner.os == 'Linux' - with: - with-documentation: false - with-python-bindings: false - with-python-packaging: true - - - name: Install dependencies - uses: ./.github/actions/install-dependencies + # 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: - with-documentation: false - with-python-bindings: true - with-python-packaging: true + platforms: "linux/arm64" - - name: Setup caches - uses: ./.github/actions/setup-cache + - uses: msys2/setup-msys2@v2 + if: runner.os == 'Windows' with: - cache-key: ${{ matrix.cache-key }} + 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: Package PyPi wheel packages - uses: ./.github/actions/package-python-wheel + - name: Build wheels + uses: pypa/cibuildwheel@v2.17.0 with: - upload-to-pypi: ${{ github.event_name == 'release' }} - upload-to-test-pypi: false - test-pypi-token: ${{ secrets.PYPI_TOKEN }} - pypi-token: ${{ secrets.PYPI_TOKEN }} - config: ${{ matrix.config }} - platform: ${{ matrix.platform }} + 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\lib;${{ 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/CMakeLists.txt b/CMakeLists.txt index 312771e56c2..ea8142ec1da 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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. @@ -13,7 +13,7 @@ # The build system configuration. ## -cmake_minimum_required(VERSION 3.12) +cmake_minimum_required(VERSION 3.16) #-----------------------------------------------------------------------------# # Project configuration @@ -131,15 +131,22 @@ set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install") # Supported language bindings based on new C++ API option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ") +option(ONLY_PYTHON_EXT_SRC "Create only Python bindings source files") option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ") # Api documentation option(BUILD_DOCS "Build Api documentation") +option(BUILD_GMP "Build GMP from sources") + # Link against static system libraries cvc5_option(STATIC_BINARY "Link against static system libraries \ (enabled by default for static builds)") +option(SKIP_COMPRESS_DEBUG "Skip compression of debug symbols") +option(SKIP_SET_RPATH "Skip setting of rpath") +option(USE_DEFAULT_LINKER "Use default linker") + # Custom flags for WebAssembly compilation set(WASM_FLAGS "" CACHE STRING "Link flags for the WebAssembly binary generation") set(WASM "OFF" CACHE STRING "Use a specific extension for WebAssembly compilation") @@ -236,7 +243,7 @@ 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")) +if (NOT ("${CMAKE_GENERATOR}" STREQUAL "MSYS Makefiles") AND NOT USE_DEFAULT_LINKER) #-----------------------------------------------------------------------------# # Use ld.mold if available, otherwise use ld.gold if available @@ -306,7 +313,13 @@ endif() # # More information on RPATH in CMake: # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling -set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib") +if(NOT SKIP_SET_RPATH) + if (APPLE) + SET(CMAKE_INSTALL_RPATH "@loader_path/../${CMAKE_INSTALL_LIBDIR}") + else() + SET(CMAKE_INSTALL_RPATH "\${ORIGIN}/../${CMAKE_INSTALL_LIBDIR}") + endif() +endif() # Set visibility to default if unit tests are enabled. If unit tests are # enabled, we also check if we can execute white box unit tests (some versions @@ -356,14 +369,6 @@ else() find_package(Python COMPONENTS Interpreter REQUIRED) endif() -# Some cmake packages are not compatible with the newest version -# of FindPython, introduced in cmake 3.12. -# We define the symbols below to be backward compatible. -# FindPython Interpreter sets Python_EXECUTABLE -if(NOT DEFINED PYTHON_EXECUTABLE) - set(PYTHON_EXECUTABLE "${Python_EXECUTABLE}") -endif() - find_package(GMP 6.3 REQUIRED) if(ENABLE_ASAN) @@ -413,7 +418,9 @@ endif() if(ENABLE_DEBUG_SYMBOLS) add_check_c_cxx_flag("-ggdb3") - add_check_c_cxx_flag("-gz") + if(NOT SKIP_COMPRESS_DEBUG) + add_check_c_cxx_flag("-gz") + endif() endif() if(ENABLE_COMP_INC_TRACK) diff --git a/INSTALL.rst b/INSTALL.rst index 01d308d7828..a3d8e24c225 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -117,7 +117,7 @@ versions; more recent versions should be compatible. - `GNU C and C++ (gcc and g++, >= 7) `_ or `Clang (>= 5) `_ -- `CMake >= 3.12 `_ +- `CMake >= 3.16 `_ - `GNU Make `_ or `Ninja `_ - `Python >= 3.6 `_ @@ -259,7 +259,6 @@ Dependencies for Language Bindings - Python - `Cython `_ >= 3.0.0 - - `scikit-build `_ - `pytest `_ - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`. diff --git a/NEWS.md b/NEWS.md index 3ea6df3df88..a702b8d47b1 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,19 +1,47 @@ This file contains a summary of important user-visible changes. +cvc5 1.1.2 +========== + ## New Features -- Added support for nullable sorts and lift operator to the theory of datatypes. +- Added support for **nullable** sorts and lift operator to the theory of **datatypes**. +- Adds 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. ## Changes +- SAT clauses are no longer marked as removable in MiniSat. This change + **improves performance** overall on quantifier-free logics with arithmetic and + strings. - **API** * Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now deprecated and replaced by `std::to_string(Kind)` and `std::to_string(SortKind)`. They will be removed in the next minor release. +- Minor changes to the output format for proofs. Proofs in the AletheLF + proof format generated by cvc5 now correspond directly to their representation + in proof objects obtained in via the API (the `Proof` class). Moreover, + proofs now use SMT-LIB compliant syntax for quantified formulas and unary + arithmetic negation. +- The option `--safe-options` now disallows cases where more than one regular + option is used. +- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive + mode. +- Renamed `bag.duplicate_removal` to `bag.setof`. +- Improvements to handling of constant production rules (`Constant`) in SyGuS + grammars. cvc5 1.1.1 ========== +## New Features + +- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS** + inputs. This allows functions-to-synthesize to include previous + functions-to-synthesize in their grammars. This feature is enabled by default + for all SyGuS inputs. + ## Changes - Fixed a bug when piping input from stdin, which caused cvc5 to have degraded diff --git a/cmake/CMakeGraphVizOptions.cmake.in b/cmake/CMakeGraphVizOptions.cmake.in index 4ca946e11be..1c3e83a302f 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-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. diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index a152a87c02b..f86d0c619c4 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -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. diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 87a872bf325..ce5c35dac02 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -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. @@ -29,6 +29,6 @@ cvc5_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=optional cvc5_set_option(ENABLE_UNIT_TESTING ON) -# Reset visibility for debug builds (https://github.com/CVC4/CVC4/issues/324) +# Reset visibility for debug builds (https://github.com/cvc5/cvc5/issues/324) set(CMAKE_CXX_VISIBILITY_PRESET default) set(CMAKE_VISIBILITY_INLINES_HIDDEN 0) diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 1176f288019..5b3ccfc8c90 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -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. diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 9af2fb5d063..5f9e1c524d4 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -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. diff --git a/cmake/ConfigureCvc5.cmake b/cmake/ConfigureCvc5.cmake index bc107d8b8d3..233b03e1259 100644 --- a/cmake/ConfigureCvc5.cmake +++ b/cmake/ConfigureCvc5.cmake @@ -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. diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index 22b8ad1c015..c0484c34531 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andrew V. Jones +# Gereon Kremer, Mathias Preiner, Daniel Larraz # # 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. diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake index 5a658c0a0f0..3f34e7e6c2b 100644 --- a/cmake/FindCVC5PythonicAPI.cmake +++ b/cmake/FindCVC5PythonicAPI.cmake @@ -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. diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index 38060a3b18a..43046c52c40 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andres Noetzli +# Gereon Kremer, Andrew V. Teylu, Mathias Preiner # # 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. @@ -23,10 +23,10 @@ find_library(CaDiCaL_LIBRARIES NAMES cadical) set(CaDiCaL_FOUND_SYSTEM FALSE) if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRARIES) - # Try to compile our version file - try_run(RUN_RESULT_VAR - COMPILE_RESULT_VAR - SOURCE_FROM_CONTENT CaDiCaL_version.cpp + + # Generate our version check file in CMAKE_BINARY_DIR + set(CaDiCaL_version_src "${CMAKE_BINARY_DIR}/CaDiCaL_version.cpp") + file(WRITE ${CaDiCaL_version_src} " #include #include @@ -37,10 +37,29 @@ if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRARIES) return 0; } " + ) + + # `try_run` doesn't have a way to specify a specific include dirs, so we need + # to set (and then reset) `CMAKE_CXX_FLAGS`; our version file is a .cpp file, + # so CXX_FLAGS are the right flags + set(OLD_CXX_FLAGS ${CMAKE_CXX_FLAGS}) + + # cvc5 doesn't support MSVC, so we're fine to hard-code `-I` as the include + # flag + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I${CaDiCaL_INCLUDE_DIR}") + + # Try to compile and run our version file + try_run(RUN_RESULT_VAR + COMPILE_RESULT_VAR + ${CMAKE_BINARY_DIR} + ${CaDiCaL_version_src} LINK_LIBRARIES ${CaDiCaL_LIBRARIES} RUN_OUTPUT_VARIABLE CaDiCaL_VERSION ) + # Restore our CXX flags after checking with `try_run` + set(CMAKE_CXX_FLAGS ${OLD_CXX_FLAGS}) + # If this failed to compile or run, we have bigger issues if (NOT ${RUN_RESULT_VAR} EQUAL 0 OR NOT ${COMPILE_RESULT_VAR}) set(CaDiCaL_VERSION "") @@ -153,8 +172,4 @@ if(CaDiCaL_FOUND_SYSTEM) else() message(STATUS "Building CaDiCaL ${CaDiCaL_VERSION}: ${CaDiCaL_LIBRARIES}") add_dependencies(CaDiCaL CaDiCaL-EP) - install(FILES - ${CaDiCaL_LIBRARIES} - DESTINATION ${CMAKE_INSTALL_LIBDIR} - ) endif() diff --git a/cmake/FindCoCoA.cmake b/cmake/FindCoCoA.cmake index e24d8b4b909..5978f8cc4e6 100644 --- a/cmake/FindCoCoA.cmake +++ b/cmake/FindCoCoA.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Andres Noetzli +# Gereon Kremer, Alex Ozdemir, Sorawee Porncharoenwase # # 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. @@ -63,7 +63,7 @@ if(NOT CoCoA_FOUND_SYSTEM) PATCH_COMMAND patch -p1 -d -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CoCoALib-0.99800-trace.patch BUILD_IN_SOURCE YES - CONFIGURE_COMMAND ${SHELL} ./configure --prefix= --with-libgmp=${GMP_LIBRARY} + CONFIGURE_COMMAND ${SHELL} ./configure --prefix= --with-libgmp=${GMP_LIBRARY} --with-cxx=${CMAKE_CXX_COMPILER} BUILD_COMMAND ${make_cmd} library BUILD_BYPRODUCTS /lib/libcocoa.a ) diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index ec920966b2f..606d2093fc8 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Andrew V. Jones +# Gereon Kremer, Mathias Preiner, Andrew V. Teylu # # 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. diff --git a/cmake/FindCython.cmake b/cmake/FindCython.cmake new file mode 100644 index 00000000000..907073660e5 --- /dev/null +++ b/cmake/FindCython.cmake @@ -0,0 +1,57 @@ +############################################################################### +# Top contributors (to current version): +# Daniel Larraz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Find Cython +# Cython_FOUND - found Cython Python module +## + +execute_process( + COMMAND "${Python_EXECUTABLE}" -c "import Cython; print(Cython.__version__)" + RESULT_VARIABLE Cython_VERSION_CHECK_RESULT + OUTPUT_VARIABLE Cython_VERSION + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE +) + +if (Cython_FIND_REQUIRED) + set(Cython_FIND_MODE FATAL_ERROR) +else() + set(Cython_FIND_MODE STATUS) +endif() + +if (Cython_VERSION_CHECK_RESULT EQUAL 0) + set(Cython_FOUND TRUE) + message(STATUS "Found Cython version: ${Cython_VERSION}") + if (DEFINED Cython_FIND_VERSION) + if(Cython_FIND_VERSION_EXACT) + if (NOT (Cython_VERSION VERSION_EQUAL ${Cython_FIND_VERSION})) + message(${Cython_FIND_MODE} + "Cython version == ${Cython_FIND_VERSION} is required, " + "but found version ${Cython_VERSION}") + endif() + else() + if (Cython_VERSION VERSION_LESS ${Cython_FIND_VERSION}) + message(${Cython_FIND_MODE} + "Cython version >= ${Cython_FIND_VERSION} is required, " + "but found version ${Cython_VERSION}") + endif() + endif() + endif() +else() + set(Cython_FOUND FALSE) + message(${Cython_FIND_MODE} + "Could not find module Cython for Python " + "version ${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}. " + "Make sure to install Cython for this Python version " + "via \n`${Python_EXECUTABLE} -m pip install Cython'.\n" + "Note: You need to have pip installed for this Python version.") +endif() diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake index 353023e7a81..52b4d656c4d 100644 --- a/cmake/FindDrat2Er.cmake +++ b/cmake/FindDrat2Er.cmake @@ -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. diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake index f525d7bf74b..3aa69fe2943 100644 --- a/cmake/FindEditline.cmake +++ b/cmake/FindEditline.cmake @@ -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. @@ -25,7 +25,7 @@ pkg_check_modules(Editline REQUIRED libedit) if(Editline_INCLUDE_DIRS) # Check which standard of editline is installed on the system. - # https://github.com/CVC4/CVC4/issues/702 + # https://github.com/cvc5/cvc5/issues/702 include(CheckCXXSourceCompiles) set(CMAKE_REQUIRED_QUIET TRUE) set(CMAKE_REQUIRED_LIBRARIES ${Editline_LIBRARIES}) @@ -42,7 +42,11 @@ if(Editline_INCLUDE_DIRS) unset(CMAKE_REQUIRED_INCLUDES) if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin") - set(Editline_LIBRARIES ${Editline_LIBRARIES} bsd tinfo) + find_library(BSD_LIBRARIES NAMES bsd) + if (BSD_LIBRARIES) + set(Editline_LIBRARIES ${Editline_LIBRARIES} bsd) + endif() + set(Editline_LIBRARIES ${Editline_LIBRARIES} tinfo) endif() endif() diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index fe8213225a2..366776fdc75 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -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. diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 17e9fad96df..19d61a50c96 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Andres Noetzli, Vinícius Camillo # # 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. @@ -17,10 +17,12 @@ include(deps-helper) -find_path(GMP_INCLUDE_DIR NAMES gmp.h) -find_path(GMPXX_INCLUDE_DIR NAMES gmpxx.h) -find_library(GMP_LIBRARIES NAMES gmp) -find_library(GMPXX_LIBRARIES NAMES gmpxx) +if (NOT BUILD_GMP) + find_path(GMP_INCLUDE_DIR NAMES gmp.h) + find_path(GMPXX_INCLUDE_DIR NAMES gmpxx.h) + find_library(GMP_LIBRARIES NAMES gmp) + find_library(GMPXX_LIBRARIES NAMES gmpxx) +endif() set(GMP_FOUND_SYSTEM FALSE) if(GMP_INCLUDE_DIR AND GMPXX_INCLUDE_DIR AND GMP_LIBRARIES AND GMPXX_LIBRARIES) @@ -57,7 +59,7 @@ if(GMP_INCLUDE_DIR AND GMPXX_INCLUDE_DIR AND GMP_LIBRARIES AND GMPXX_LIBRARIES) LINK_LIBRARIES ${GMP_LIBRARIES} ${GMPXX_LIBRARIES} ) if(NOT GMP_USABLE) - message(VERBOSE "System version for GMP does not work in the selected configuration. Maybe we are cross-compiling?") + message(STATUS "System version for GMP does not work in the selected configuration. Maybe we are cross-compiling?") set(GMP_FOUND_SYSTEM FALSE) endif() endif() @@ -96,7 +98,7 @@ if(NOT GMP_FOUND_SYSTEM) # https://github.com/microsoft/vcpkg/issues/22671 # Many solution attempts have been tried, but none worked. - # Since makeinfo just builds the documentation for GMP, + # Since makeinfo just builds the documentation for GMP, # it is possible to get around this issue by just disabling it: set(CONFIGURE_ENV env "MAKEINFO=true") @@ -105,7 +107,7 @@ if(NOT GMP_FOUND_SYSTEM) --host=${TOOLCHAIN_PREFIX} --build=${CMAKE_HOST_SYSTEM_PROCESSOR}) - set(CONFIGURE_ENV ${CMAKE_COMMAND} -E + set(CONFIGURE_ENV ${CONFIGURE_ENV} ${CMAKE_COMMAND} -E env "CC_FOR_BUILD=cc") if (CMAKE_CROSSCOMPILING_MACOS) set(CONFIGURE_ENV diff --git a/cmake/FindGTest.cmake b/cmake/FindGTest.cmake index 7c8ffe964e1..01acf8aa2e4 100644 --- a/cmake/FindGTest.cmake +++ b/cmake/FindGTest.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Yoni Zohar # # 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. diff --git a/cmake/FindHamcrest.cmake b/cmake/FindHamcrest.cmake index 283633e3899..5a4820cf0e1 100644 --- a/cmake/FindHamcrest.cmake +++ b/cmake/FindHamcrest.cmake @@ -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. diff --git a/cmake/FindJUnit.cmake b/cmake/FindJUnit.cmake index f88240600bc..80283c9086a 100644 --- a/cmake/FindJUnit.cmake +++ b/cmake/FindJUnit.cmake @@ -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. diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake index 4cbcef4bcec..9cae199594f 100644 --- a/cmake/FindKissat.cmake +++ b/cmake/FindKissat.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner, Aina Niemetz +# Gereon Kremer, Aina Niemetz, Mathias Preiner # # 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. diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 757306a1e5c..aba95bb3494 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -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. diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index f8748c8c66c..a74e41deea9 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Andres Noetzli, Mathias Preiner +# Gereon Kremer, Andres Noetzli, Vinícius Camillo # # 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. diff --git a/cmake/FindSphinx.cmake b/cmake/FindSphinx.cmake index cc22438e4b0..2cb844d99e5 100644 --- a/cmake/FindSphinx.cmake +++ b/cmake/FindSphinx.cmake @@ -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. diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 91ea54edbb4..3173a659175 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -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. diff --git a/cmake/FindValgrind.cmake b/cmake/FindValgrind.cmake index ae1439fa6d5..d1481f5cf95 100644 --- a/cmake/FindValgrind.cmake +++ b/cmake/FindValgrind.cmake @@ -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. diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index ccb2e05081a..0e8e603301a 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -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. @@ -255,3 +255,13 @@ function(check_python_module module) "Note: You need to have pip installed for this Python version.") endif() endfunction() + +macro(copy_file_from_src filename) + add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${filename} + COMMAND ${CMAKE_COMMAND} -E copy + ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + ${CMAKE_CURRENT_BINARY_DIR}/${filename} + DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + ) +endmacro() diff --git a/cmake/IWYU.cmake b/cmake/IWYU.cmake index 9ff42694097..fc204a57924 100644 --- a/cmake/IWYU.cmake +++ b/cmake/IWYU.cmake @@ -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. diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake index 9e842369122..70c7702e188 100644 --- a/cmake/Toolchain-aarch64.cmake +++ b/cmake/Toolchain-aarch64.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Andres Noetzli, Gereon Kremer +# Gereon Kremer, Mathias Preiner, Andres Noetzli # # 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. @@ -15,9 +15,12 @@ # Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake ## +# Set CMAKE_SYSTEM_NAME here. CMake only sets CMAKE_CROSSCOMPILING to +# TRUE if CMAKE_SYSTEM_NAME is set _unconditionally_. +set(CMAKE_SYSTEM_NAME ${CMAKE_HOST_SYSTEM_NAME}) + if(CMAKE_SYSTEM_NAME STREQUAL "Linux") - set(CMAKE_SYSTEM_NAME Linux) set(CMAKE_SYSTEM_PROCESSOR aarch64) set(TOOLCHAIN_PREFIX aarch64-linux-gnu) @@ -37,7 +40,6 @@ if(CMAKE_SYSTEM_NAME STREQUAL "Linux") elseif(CMAKE_SYSTEM_NAME STREQUAL "Darwin") - set(CMAKE_SYSTEM_NAME Darwin) set(CMAKE_SYSTEM_PROCESSOR arm64) set(TOOLCHAIN_PREFIX arm64-apple-darwin) diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake index 6bd3443ff65..fbf554bc5d8 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-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. diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in index 7ea66e605ee..7ebec6c830c 100644 --- a/cmake/cvc5Config.cmake.in +++ b/cmake/cvc5Config.cmake.in @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mudathir Mohamed, Mathias Preiner, Aina Niemetz +# Aina Niemetz, Mudathir Mohamed, Mathias Preiner # # 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. diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake index d9717c67b08..f9ff08537f7 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. Jones +# Gereon Kremer, Mathias Preiner, Andrew V. Teylu # # 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. @@ -99,7 +99,7 @@ macro(check_system_version name) # we ignore the EXACT option and version ranges here if (${name}_FIND_VERSION) if(${name}_VERSION VERSION_LESS ${name}_FIND_VERSION) - message(VERBOSE "System version for ${name} has incompatible \ + message(STATUS "System version for ${name} has incompatible \ version: required ${${name}_FIND_VERSION} but found ${${name}_VERSION}") set(${name}_FOUND_SYSTEM FALSE) endif() diff --git a/cmake/deps-utils/gmp-test.cpp b/cmake/deps-utils/gmp-test.cpp index c845a2587ad..05ccc2694b1 100644 --- a/cmake/deps-utils/gmp-test.cpp +++ b/cmake/deps-utils/gmp-test.cpp @@ -1,3 +1,17 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for required GMP version. + */ #include #if __GNU_MP_RELEASE < 60100 diff --git a/cmake/fuzzing-murxla.cmake b/cmake/fuzzing-murxla.cmake index 061e07e2f6d..bc5b1a2026a 100644 --- a/cmake/fuzzing-murxla.cmake +++ b/cmake/fuzzing-murxla.cmake @@ -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. diff --git a/cmake/target-graphs.cmake b/cmake/target-graphs.cmake index 7ec643ea063..471c1d23677 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-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. diff --git a/cmake/version-base.cmake b/cmake/version-base.cmake index a5bb8e3ae85..c68b6b5e372 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.1") +set(CVC5_LAST_RELEASE "1.1.2") set(CVC5_IS_RELEASE "false") # These are used in other places in cmake diff --git a/cmake/version.cmake b/cmake/version.cmake index 4353ba70ffc..0f0cf037a22 100644 --- a/cmake/version.cmake +++ b/cmake/version.cmake @@ -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. diff --git a/configure.sh b/configure.sh index 326e8731975..68e62fb928c 100755 --- a/configure.sh +++ b/configure.sh @@ -45,6 +45,7 @@ The following flags enable optional features (disable with --no-