Benchmark z3 and cvc5

GaloisInc · Sep 25, 2024 · 114870c · 114870c
1 parent 98434f0
commit 114870c
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 10 deletions.
diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml
@@ -94,19 +94,23 @@ jobs:
         opam pin --yes --no-action add cn .
         opam install --yes cn ocamlformat.0.26.2
 
-    - name: Run benchmark
+    - name: Run benchmarks
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh
+        cd tests; SOLVER='z3' ./run-ci-benchmarks.sh; SOLVER='cvc5' ./run-ci-benchmarks.sh
         cd ..
 
     - name: Store benchmark result
-      uses: benchmark-action/github-action-benchmark@v1
+      uses: GaloisInc/github-action-benchmark@00bf34008c7b91a09ea7f1ef93330ccb7bf2d4ab
       with:
         name: CN Benchmarks
         tool: 'customSmallerIsBetter'
-        output-file-path: tests/benchmark-data.json
+        output-file-path: |
+          {
+            "z3": "tests/benchmark-data-z3.json",
+            "cvc5": "tests/benchmark-data-cvc5.json"
+          }
         # Access token to deploy GitHub Pages branch
         github-token: ${{ secrets.GITHUB_TOKEN }}
         # Push and deploy GitHub pages branch automatically

diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
@@ -2,7 +2,13 @@
 set -euo pipefail -o noclobber
 # set -xv # uncomment to debug variables
 
-JSON_FILE="benchmark-data.json"
+if [[ -z "${SOLVER+x}" ]]; then
+  JSON_FILE="benchmark-data.json"
+  SOLVER_TYPE="--solver-type=z3"
+else
+  JSON_FILE="benchmark-data-${SOLVER}.json"
+  SOLVER_TYPE="--solver-type=${SOLVER}"
+fi
 TMP_FILE=$(mktemp)
 
 echo "[" >> "${JSON_FILE}"
@@ -21,22 +27,22 @@ TOTAL=0
 for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
-  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${TEST}" || true
+  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${SOLVER_TYPE}" "${TEST}" || true
   TIME=$(cat /tmp/time)
   TOTAL="$(echo "${TOTAL} + ${TIME}" | bc -l)"
 
   # If we're last, don't print a trailing comma.
   if [[ ${INDEX} -eq ${COUNT}-1 ]]; then
     # Hack to output JSON.
-    cat << EOF >> ${TMP_FILE}
+    cat << EOF >> "${TMP_FILE}"
     {
 	"name": "${TEST}",
         "unit": "Seconds",
 	"value": ${TIME}
     }
 EOF
   else
-    cat << EOF >> ${TMP_FILE}
+    cat << EOF >> "${TMP_FILE}"
     {
 	"name": "${TEST}",
         "unit": "Seconds",
@@ -48,15 +54,15 @@ EOF
   let INDEX=${INDEX}+1
 done
 
-cat << EOF >> ${JSON_FILE}
+cat << EOF >> "${JSON_FILE}"
     {
         "name": "Total benchmark time",
         "unit": "Seconds",
         "value": ${TOTAL}
     },
 EOF
 
-cat ${TMP_FILE} >> ${JSON_FILE}
+cat "${TMP_FILE}" >> "${JSON_FILE}"
 
 echo "]" >> "${JSON_FILE}"