ci.yml

name: what4-solvers
on:
  push:
    tags: ["v?[0-9]+"]
    branches: [main, "release-**"]
  pull_request:
  workflow_dispatch:

env:
  CACHE_VERSION: 1
  LATEST_Z3_VERSION: "4.8.14"

jobs:
  build:
    runs-on: ${{ matrix.os }}
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019]
        solver: [abc, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14]
    steps:
      - uses: actions/checkout@v2
        with:
          submodules: true
          fetch-depth: 0

      - name: Install dependencies (Ubuntu)
        run: |
          sudo apt-get update
          sudo apt-get install gperf automake autoconf lzip ninja-build
        if: runner.os == 'Linux'

      - name: Install dependencies (macOS)
        run: |
          brew update
          brew install gperf automake autoconf ninja gnu-sed
          # macOS's version of sed lacks the -r option, which CVC5 requires. To
          # work around this, we install put GNU sed before macOS's sed on the
          # PATH.
          echo "PATH=/usr/local/opt/gnu-sed/libexec/gnubin:$PATH" >> $GITHUB_ENV
        if: runner.os == 'macOS'

      - name: Install dependencies (Windows)
        uses: msys2/setup-msys2@v2
        with:
          update: true
          msystem: MINGW64
          path-type: inherit
          install: |
            autoconf
            automake
            curl
            dos2unix
            git
            gperf
            lzip
            m4
            make
            mingw-w64-x86_64-cmake
            mingw-w64-x86_64-gcc
            mingw-w64-x86_64-ninja
            patch
            tar
            unzip
        if: runner.os == 'Windows'

      - name: Install Python
        uses: actions/setup-python@v4
        with:
          python-version: '3.9'

      - name: Install Python libraries
        run: |
          python -m pip install --upgrade pip
          pip install pyparsing toml tomli

      - name: Install Java
        uses: actions/setup-java@v3
        with:
          distribution: 'temurin'
          java-version: '17'

      - name: build_solver (non-Windows)
        shell: bash
        run: .github/ci.sh build_${{ matrix.solver }}
        if: runner.os != 'Windows'

      - name: build_solver (Windows)
        shell: msys2 {0}
        run: .github/ci.sh build_${{ matrix.solver }}
        if: runner.os == 'Windows'

      - uses: actions/upload-artifact@v2
        with:
          path: bin
          name: ${{ matrix.os }}-${{ runner.arch }}-${{ matrix.solver }}-bin

  package_solvers:
    runs-on: ${{ matrix.os }}
    needs: [build]
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019]
    steps:
      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-abc-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-boolector-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-cvc4-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-cvc5-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-yices-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.8-bin"
          path: bin

      - uses: actions/download-artifact@v2
        with:
          name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.14-bin"
          path: bin

        # Make a copy of z3-<LATEST_Z3_VERSION> named z3 for ease of use.
        # Unfortunately, GitHub Actions' upload-artifact action doesn't support
        # symlinks (see https://github.com/actions/upload-artifact/issues/93),
        # so we have no choice but to copy the entire binary.
      - name: Copy latest Z3 version
        shell: bash
        run: cp bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3

      - uses: actions/upload-artifact@v2
        with:
          path: bin
          name: ${{ matrix.os }}-${{ runner.arch }}-bin

  # Indicates sufficient CI success for the purposes of mergify merging the pull
  # request, see .github/mergify.yml. This is done instead of enumerating each
  # instance of each job in the mergify configuration for a number of reasons:
  # - continue-on-error is respected, won't block merge
  # - changes to jobs or job instances don't require a mergify config update
  # - dependencies through `needs:` are validated, CI will fail if it's invalid
  mergify:
    runs-on: ubuntu-20.04
    needs: [build]
    steps:
      - run: "true"