From 338b8eae977b3647f8a7dbc028e96654bf14bf59 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Thu, 6 Jun 2024 14:26:43 -0700 Subject: [PATCH] feat: solvers package (#302) Co-authored-by: PILLIP YOUN --- .github/workflows/solvers-publish.yml | 52 ++++++++++++++++ packages/solvers/Dockerfile | 85 +++++++++++++++++++++++++++ packages/solvers/README.md | 50 ++++++++++++++++ 3 files changed, 187 insertions(+) create mode 100644 .github/workflows/solvers-publish.yml create mode 100644 packages/solvers/Dockerfile create mode 100644 packages/solvers/README.md diff --git a/.github/workflows/solvers-publish.yml b/.github/workflows/solvers-publish.yml new file mode 100644 index 00000000..65424faa --- /dev/null +++ b/.github/workflows/solvers-publish.yml @@ -0,0 +1,52 @@ +# based on https://docs.github.com/en/packages/managing-github-packages-using-github-actions-workflows/publishing-and-installing-a-package-with-github-actions#upgrading-a-workflow-that-accesses-a-registry-using-a-personal-access-token +name: Push solvers package + +on: + workflow_dispatch: + push: + branches: + - feat-packages + +env: + IMAGE_NAME: solvers + +jobs: + # This pushes the image to GitHub Packages. + push: + runs-on: ubuntu-latest + permissions: + packages: write + contents: read + + steps: + - uses: actions/checkout@v4 + + - name: Build image + run: docker build . --file packages/solvers/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}" + + - name: Login to GitHub Container Registry + uses: docker/login-action@v3 + with: + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + + - name: Push image + run: | + IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME + + # This changes all uppercase characters to lowercase. + IMAGE_ID=$(echo $IMAGE_ID | tr '[A-Z]' '[a-z]') + + # This strips the git ref prefix from the version. + VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,') + + # This strips the "v" prefix from the tag name. + [[ "${{ github.ref }}" == "refs/tags/"* ]] && VERSION=$(echo $VERSION | sed -e 's/^v//') + + # This uses the Docker `latest` tag convention. + [ "$VERSION" == "main" ] && VERSION=latest + echo IMAGE_ID=$IMAGE_ID + echo VERSION=$VERSION + docker tag $IMAGE_NAME $IMAGE_ID:$VERSION + docker push $IMAGE_ID:$VERSION diff --git a/packages/solvers/Dockerfile b/packages/solvers/Dockerfile new file mode 100644 index 00000000..e6e70b2a --- /dev/null +++ b/packages/solvers/Dockerfile @@ -0,0 +1,85 @@ +FROM ubuntu:24.04 as builder + +# Install necessary packages +RUN apt-get update && apt-get install --no-install-recommends -y \ + curl \ + git \ + build-essential \ + wget \ + unzip \ + autoconf \ + libffi-dev \ + cmake \ + python3 \ + python3-pip \ + python3-venv \ + ninja-build \ + software-properties-common \ + g++ zlib1g-dev libboost-all-dev flex bison + +# Install Z3 +COPY --from=ghcr.io/z3prover/z3:ubuntu-20.04-bare-z3-sha-770c51a /usr/bin/z3 /usr/local/bin/z3 + +# Install STP +COPY --from=msoos/stp /usr/local/bin/stp /usr/local/bin/stp + +# Install Yices from the release binaries +WORKDIR /yices +ARG YICES_VERSION=2.6.4 +RUN wget https://github.com/SRI-CSL/yices2/releases/download/Yices-${YICES_VERSION}/yices-${YICES_VERSION}-x86_64-pc-linux-gnu.tar.gz -O yices.tar.gz && \ + tar -xzvf yices.tar.gz --strip-components=1 && \ + mv /yices/bin/* /usr/local/bin/ && \ + mv /yices/lib/* /usr/local/lib/ && \ + mv /yices/include/* /usr/local/include/ && \ + rm -rf /yices + +# Install cvc5 from release binaries +WORKDIR /cvc5 +ARG CVC5_VERSION=1.1.2 +RUN wget https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-static.zip -O cvc5-Linux-static.zip && \ + unzip cvc5-Linux-static.zip && \ + mv cvc5-Linux-static/bin/cvc5 /usr/local/bin/cvc5 && \ + chmod +x /usr/local/bin/cvc5 && \ + rm -rf /cvc5 + +# Install Bitwuzla +WORKDIR /bitwuzla +RUN git clone --depth 1 https://github.com/bitwuzla/bitwuzla . && \ + python3 -m venv .venv && \ + . .venv/bin/activate && \ + python3 -m pip install meson && \ + ./configure.py && \ + cd build && \ + ninja install && \ + rm -rf /bitwuzla + +# Install Boolector +WORKDIR /boolector +RUN git clone --depth 1 https://github.com/boolector/boolector . && \ + ./contrib/setup-lingeling.sh && \ + ./contrib/setup-btor2tools.sh && \ + ./configure.sh && \ + cd build && \ + make && \ + mv /boolector/build/bin/* /usr/local/bin/ && \ + rm -rf /boolector + +# Create the final image +FROM ubuntu:24.04 + +# Copy installed files from builder + +COPY --from=builder \ + /usr/local/bin/z3 \ + /usr/local/bin/stp \ + /usr/local/bin/cvc5 \ + /usr/local/bin/yices \ + /usr/local/bin/yices-smt2 \ + /usr/local/bin/bitwuzla \ + /usr/local/bin/boolector \ + /usr/local/bin/ + + +# Set the default command for the container +WORKDIR /workspace +CMD ["/bin/bash"] diff --git a/packages/solvers/README.md b/packages/solvers/README.md new file mode 100644 index 00000000..76a3997c --- /dev/null +++ b/packages/solvers/README.md @@ -0,0 +1,50 @@ +# solvers package + +A minimalist Docker image containing high-performance SMT solvers. + +## Quick start + +```sh +# Step 1: Pull the image +docker pull ghcr.io/a16z/solvers:latest + +# Step 2: Tag the image with a shorter name +docker tag ghcr.io/a16z/solvers:latest solvers + +# Step 3: Run the container using the shorter name, +for solver in bitwuzla boolector cvc5 stp yices z3 ; do \ + echo --- $solver && \ + docker run --rm solvers $solver --version ; \ +done + +# Step 4: create an example smt2 file: +cat << EOF > checkSanity.smt2 +(set-logic QF_BV) +(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2))) +(check-sat) +(exit) +EOF + +# Step 5: invoke each solver on the file +# (`-v .:/workspace` mounts the current working directory under /workspace on the container, making the files available there) +for solver in bitwuzla boolector cvc5 stp yices-smt2 z3 ; do \ + echo -n "$solver: " && \ + docker run --rm -v .:/workspace solvers $solver checkSanity.smt2 ; \ +done +``` + +## Available solvers + +| Solver | Version | URL | Notes +| ------ | ------- | --- | ----- | +| Bitwuzla | 0.5.0-dev-main@50ce452 | [bitwuzla/bitwuzla](https://github.com/bitwuzla/bitwuzla) | Built from source +| Boolector | 3.2.3 | [boolector/boolector](https://github.com/boolector/boolector) | Built from source +| CVC5 | 1.1.2 | [cvc5/cvc5](https://github.com/cvc5/cvc5) | Installed from Github release binaries +| STP | 2.3.3 | [stp/stp](https://github.com/stp/stp) | Provides a great Dockerfile that shows how to do a static build. We just copy the binary from the `msoos/stp` image since releases aren't too frequent. | +| Yices | 2.6.4 | [SRI-CSL/yices2](https://github.com/SRI-CSL/yices2) | Installed from Github release binaries +| Z3 | 4.13.1 | [Z3Prover/z3](https://github.com/Z3Prover/z3) | Includes a [Dockerfile](https://github.com/Z3Prover/z3/blob/master/docker/ubuntu-20-04.Dockerfile) and a package but no `latest` tag | + + +## Credit + +Based on [EmperorOrokuSaki/solvers](https://github.com/EmperorOrokuSaki/solvers)