Add eval

.github/workflows/eval.yml

@@ -0,0 +1,29 @@
+name: Run evaluation
+on:
+  push:
+    branches: [cav-eval]
+  workflow_dispatch:
+
+jobs:
+  eval:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install Z3
+        uses: pavpanchekha/setup-z3@1.2.2
+        with:
+          version: '4.8.7'
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "shared"
+      - run: ./eval/build.sh
+      - run: ./eval/eval.sh
+
+      - run: tar -czf data.tar.bz2 eval/data/
+      - uses: actions/upload-artifact@v4.4.3
+        with:
+          name: "data"
+          path: data.tar.bz2
+          retention-days: 30

eval/axiom-profiler/build.sh

@@ -0,0 +1,6 @@
+cd "$(dirname "$0")"
+rm -rf axiom-profiler
+wget -O axiom-profiler.tar.gz https://github.com/viperproject/axiom-profiler/releases/download/v-2025-01-07-1716/axiom-profiler-release-windows.zip
+mkdir axiom-profiler
+tar -xvf axiom-profiler.tar.gz -C axiom-profiler
+rm -f axiom-profiler.tar.gz

eval/axiom-profiler/run.sh

@@ -0,0 +1,5 @@
+SDIR="$(dirname "$0")"
+mono "$SDIR/axiom-profiler/AxiomProfiler.exe" /headless /timing /loops:2147483647 /loopsMs:10000 /showNumChecks /showQuantStatistics /findHighBranching:6 /l:$1
+EXIT_CODE=$?
+rm -f AxiomProfiler.basic AxiomProfiler.branching AxiomProfiler.loops AxiomProfiler.error
+exit $EXIT_CODE

eval/build.sh

@@ -0,0 +1,13 @@
+DIRNAME="$(realpath "$(dirname "$0")")"
+
+cd "$DIRNAME"
+rm -rf smt-logs-smt2
+wget -O smt-logs.tar.gz https://github.com/viperproject/smt-logs/archive/refs/heads/smt2.tar.gz
+tar -xvf smt-logs.tar.gz
+rm -f smt-logs.tar.gz
+
+TOOLS="axiom-profiler smt-scope"
+while read -r tool; do
+    cd "$DIRNAME/$tool"
+    ./build.sh || exit 1
+done <<< "$TOOL"