Benchmark z3 and cvc5

rems-project · Sep 26, 2024 · 0e5ded7 · 0e5ded7
1 parent 98434f0
commit 0e5ded7
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}"