Add CI (#13)

* Add CI and related scripts

* Make CI parametric to solver versions

* Update solver release versions to latest

* Generalize CI conditions to pushes and prs

* Correct quoting around pwd

* Correct solver version setting and cvc5 build selection

* Get z3 url from github api vased on version

* Reset java tmp dir

* Quieten z3 wget

Author: sankalpgambhir

.github/workflows/scala-smtlib-CI.yml

@@ -0,0 +1,44 @@
+name: scala-smtlib CI
+on: [push, pull_request]
+jobs:
+  tests:
+    # the CI is small enough that we can run on draft PRs as well without issue
+    # if: github.event.pull_request.draft == false
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        java-version: [ 17, 21 ]
+    env:
+      # define Java options for both official sbt and sbt-extras
+      JAVA_OPTS: -Xss64M -Xms1024M -Xmx8G
+      JVM_OPTS:  -Xss64M -Xms1024M -Xmx8G
+      # solver versions to test against
+      Z3_VER: 4.15.1
+      CVC4_VER: 1.8
+      CVC5_VER: 1.2.1
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - name: Setup JDK
+      uses: actions/setup-java@v4
+      with:
+        distribution: temurin
+        java-version: ${{ matrix.java-version }}
+    - name: Install and unpack sbt
+      run: |
+        ./scripts/install_sbt.sh
+        echo "PATH=./sbt/bin/:$PATH" >> "$GITHUB_ENV"
+    - name: Install solvers
+      run: ./scripts/install_solvers.sh $GITHUB_WORKSPACE/.local/bin $Z3_VER $CVC4_VER $CVC5_VER
+    - name: Add solvers to PATH
+      run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
+    - name: Test solvers availability
+      run: cvc5 --version && z3 --version && cvc4 --version
+    - name: Run Tests
+      run: sbt -Dtest-parallelism=10 -batch test
+    - name: Run integration tests
+      run: sbt -Dtest-parallelism=10 -batch it:test
+    - name: Clean up
+      run: rm -rf $JAVA_OPTS_TMP_DIR

scripts/install_sbt.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env sh
+
+SBT_VER="$(grep 'sbt.version' project/build.properties | cut -d= -f2)"
+if [ -z "$SBT_VER" ]; then
+  echo "sbt.version not found in project/build.properties"
+  exit 1
+fi
+wget -c https://github.com/sbt/sbt/releases/download/v${SBT_VER}/sbt-${SBT_VER}.tgz -q
+tar xfz "sbt-${SBT_VER}.tgz"

scripts/install_solvers.sh

@@ -0,0 +1,48 @@
+#!/usr/bin/env sh
+
+TEMP_DIR="$(pwd)/temp"
+SOLVERS_DIR=${1:-"$(pwd)/solvers"}
+
+Z3_VER=${2:-"4.15.1"}
+CVC4_VER=${3:-"1.8"}
+CVC5_VER=${4:-"1.2.1"}
+
+ARCH=$(uname -m)
+# short arch name as used by z3 builds
+SHORT_ARCH=$(uname -m | sed 's/x86_64/x64/;s/aarch64/arm64/;')
+
+# libc linked against z3
+# (glibc for Linux, osx for macOS)
+LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+
+mkdir -p "$SOLVERS_DIR"
+mkdir -p "$TEMP_DIR"
+# cvc5
+wget -c "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-Linux-${ARCH}-static.zip" -O "$TEMP_DIR/cvc5.zip" -q
+unzip "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR" 
+CVC5_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*cvc5*")
+mv "$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5"
+chmod +x "$SOLVERS_DIR/cvc5"
+rm -rf "$TEMP_DIR"
+
+# # CVC4
+wget -c "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" -O "$SOLVERS_DIR/cvc4" -q
+chmod +x "$SOLVERS_DIR/cvc4"
+
+# z3
+mkdir -p "$TEMP_DIR"
+Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
+Z3_URL=$(
+  curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
+  grep "browser_download_url.*${Z3_FILE_PREFIX}" | #| # find url for the correct build
+  sed 's/^.*: //;s/^"//;s/"$//' # strip non-url
+)
+wget -c "${Z3_URL}" -O "$TEMP_DIR/z3.zip" -q
+unzip "$TEMP_DIR/z3.zip" -d "$TEMP_DIR" 
+Z3_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*z3*")
+mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
+chmod +x "$SOLVERS_DIR/z3"
+rm -rf "$TEMP_DIR"
+
+echo "************** Solvers Installed **************"
+exit 0