feat: solvers package (#302)

Co-authored-by: PILLIP YOUN <[email protected]>

.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

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"]

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)