mirror of
https://github.com/Z3Prover/z3
synced 2026-08-10 07:51:20 +00:00
remove stale workflows
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
9866fee194
commit
009f3c1ae6
8 changed files with 0 additions and 8112 deletions
1579
.github/workflows/ostrich-benchmark.lock.yml
generated
vendored
1579
.github/workflows/ostrich-benchmark.lock.yml
generated
vendored
File diff suppressed because one or more lines are too long
461
.github/workflows/ostrich-benchmark.md
vendored
461
.github/workflows/ostrich-benchmark.md
vendored
|
|
@ -1,461 +0,0 @@
|
|||
---
|
||||
description: Run Z3 string solver benchmarks (seq vs nseq) plus ZIPT, cvc5, and Ostrich2 on all Ostrich benchmarks from tests/ostrich.zip on the c3 branch and post results as a GitHub discussion
|
||||
|
||||
on:
|
||||
schedule:
|
||||
- cron: "0 6 * * *"
|
||||
workflow_dispatch:
|
||||
|
||||
permissions: read-all
|
||||
|
||||
network:
|
||||
allowed:
|
||||
- defaults
|
||||
- api.nuget.org
|
||||
|
||||
tools:
|
||||
bash: true
|
||||
github:
|
||||
toolsets: [default]
|
||||
|
||||
safe-outputs:
|
||||
report-failure-as-issue: false
|
||||
create-discussion:
|
||||
title-prefix: "[Ostrich Benchmark] "
|
||||
category: "Agentic Workflows"
|
||||
close-older-discussions: true
|
||||
missing-tool:
|
||||
create-issue: true
|
||||
noop:
|
||||
report-as-issue: false
|
||||
|
||||
timeout-minutes: 180
|
||||
|
||||
steps:
|
||||
- name: Checkout c3 branch
|
||||
uses: actions/checkout@v6.0.2
|
||||
with:
|
||||
ref: c3
|
||||
fetch-depth: 1
|
||||
persist-credentials: false
|
||||
|
||||
---
|
||||
|
||||
|
||||
# Ostrich Benchmark: Z3 c3 branch vs ZIPT, cvc5, and Ostrich2
|
||||
|
||||
You are an AI agent that benchmarks Z3 string solvers (`seq` and `nseq`) plus ZIPT, cvc5, and Ostrich2 on all SMT-LIB2 benchmarks from the `tests/ostrich.zip` archive on the `c3` branch, and publishes a summary report as a GitHub discussion.
|
||||
|
||||
## Context
|
||||
|
||||
- **Repository**: ${{ github.repository }}
|
||||
- **Workspace**: ${{ github.workspace }}
|
||||
- **Branch**: c3 (already checked out by the workflow setup step)
|
||||
|
||||
## Phase 1: Build Z3
|
||||
|
||||
Build Z3 from the checked-out `c3` branch using CMake + Ninja, including the .NET bindings required by ZIPT.
|
||||
|
||||
```bash
|
||||
cd ${{ github.workspace }}
|
||||
|
||||
# Install build dependencies if missing
|
||||
sudo apt-get install -y ninja-build cmake python3 zstd dotnet-sdk-8.0 unzip 2>/dev/null || true
|
||||
|
||||
# Configure the build in Release mode for better performance and lower memory usage
|
||||
# (Release mode is sufficient for benchmarking; the workflow does not use -tr: trace flags)
|
||||
mkdir -p build
|
||||
cd build
|
||||
cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_DOTNET_BINDINGS=ON 2>&1 | tail -20
|
||||
|
||||
# Build z3 binary and .NET bindings SYNCHRONOUSLY (do NOT add & to background these commands).
|
||||
# Running ninja in the background while the LLM agent is also active causes OOM and kills the
|
||||
# agent process. Wait for each build command to finish before continuing.
|
||||
# -j1 limits parallelism to reduce peak memory usage alongside the LLM agent process.
|
||||
ninja z3 2>&1 | tail -30
|
||||
ninja build_z3_dotnet_bindings 2>&1 | tail -20
|
||||
|
||||
# Verify the build succeeded
|
||||
./z3 --version
|
||||
|
||||
# Locate the Microsoft.Z3.dll produced by the build
|
||||
Z3_DOTNET_DLL=$(find . -name "Microsoft.Z3.dll" -not -path "*/obj/*" | head -1)
|
||||
if [ -z "$Z3_DOTNET_DLL" ]; then
|
||||
echo "ERROR: Microsoft.Z3.dll not found after build"
|
||||
exit 1
|
||||
fi
|
||||
echo "Found Microsoft.Z3.dll at: $Z3_DOTNET_DLL"
|
||||
```
|
||||
|
||||
If the build fails, report the error clearly and exit without proceeding.
|
||||
|
||||
Once the binary is confirmed working, call the `noop` safe-output tool with the message `"Z3 built successfully from the c3 branch. Starting ZIPT/cvc5/Ostrich2 build and benchmark — results will be posted as a GitHub Discussion once complete."` This keepalive call refreshes the safe-output MCP session before the long build and benchmark phases begin, preventing a session timeout.
|
||||
|
||||
## Phase 2a: Clone and Build ZIPT, cvc5, and Ostrich2
|
||||
|
||||
Clone and build the external solvers.
|
||||
|
||||
```bash
|
||||
cd ${{ github.workspace }}
|
||||
|
||||
# Re-locate the Microsoft.Z3.dll if needed
|
||||
Z3_DOTNET_DLL=$(find build -name "Microsoft.Z3.dll" -not -path "*/obj/*" | head -1)
|
||||
Z3_LIB_DIR=${{ github.workspace }}/build
|
||||
|
||||
# Clone ZIPT (parikh branch)
|
||||
git clone --depth=1 --branch parikh https://github.com/CEisenhofer/ZIPT.git /tmp/zipt
|
||||
|
||||
# Patch ZIPT.csproj to point at the freshly built Microsoft.Z3.dll
|
||||
# (the repo has a Windows-relative hardcoded path that won't exist here)
|
||||
sed -i "s|<HintPath>.*</HintPath>|<HintPath>$Z3_DOTNET_DLL</HintPath>|" /tmp/zipt/ZIPT/ZIPT.csproj
|
||||
|
||||
# Build ZIPT in Release mode
|
||||
cd /tmp/zipt/ZIPT
|
||||
dotnet build --configuration Release 2>&1 | tail -20
|
||||
|
||||
# Locate the built ZIPT.dll
|
||||
ZIPT_DLL=$(find /tmp/zipt/ZIPT/bin/Release -name "ZIPT.dll" | head -1)
|
||||
if [ -z "$ZIPT_DLL" ]; then
|
||||
echo "ERROR: ZIPT.dll not found after build"
|
||||
exit 1
|
||||
fi
|
||||
echo "ZIPT binary: $ZIPT_DLL"
|
||||
|
||||
# Make libz3.so visible to the .NET runtime at ZIPT startup
|
||||
ZIPT_OUT_DIR=$(dirname "$ZIPT_DLL")
|
||||
if cp "$Z3_LIB_DIR/libz3.so" "$ZIPT_OUT_DIR/" 2>/dev/null; then
|
||||
echo "Copied libz3.so to $ZIPT_OUT_DIR"
|
||||
else
|
||||
echo "WARNING: could not copy libz3.so to $ZIPT_OUT_DIR — setting LD_LIBRARY_PATH fallback"
|
||||
fi
|
||||
export LD_LIBRARY_PATH="$Z3_LIB_DIR${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}"
|
||||
echo "ZIPT build complete."
|
||||
|
||||
# Build cvc5 from source (minimal build with string support)
|
||||
git clone --depth=1 https://github.com/cvc5/cvc5.git /tmp/cvc5
|
||||
cd /tmp/cvc5
|
||||
./configure.sh --auto-download --static-binary 2>&1 | tail -30
|
||||
cd build
|
||||
make -j"$(nproc)" 2>&1 | tail -40
|
||||
|
||||
if [ -x "/tmp/cvc5/build/bin/cvc5" ]; then
|
||||
echo "cvc5 binary: /tmp/cvc5/build/bin/cvc5"
|
||||
else
|
||||
echo "WARNING: cvc5 build failed or binary missing"
|
||||
fi
|
||||
|
||||
# Build Ostrich2 from source
|
||||
cd ${{ github.workspace }}
|
||||
git clone --depth=1 https://github.com/uuverifiers/ostrich.git /tmp/ostrich2
|
||||
cd /tmp/ostrich2
|
||||
sudo apt-get install -y openjdk-17-jdk-headless sbt 2>/dev/null || true
|
||||
sbt assembly 2>&1 | tail -40
|
||||
|
||||
if [ -x "/tmp/ostrich2/ostrich" ]; then
|
||||
echo "Ostrich2 launcher: /tmp/ostrich2/ostrich"
|
||||
else
|
||||
echo "WARNING: Ostrich2 build failed or launcher missing"
|
||||
fi
|
||||
```
|
||||
|
||||
If any external solver build fails, note the error in the report and continue with the remaining solvers.
|
||||
|
||||
## Phase 2b: Extract Benchmark Files
|
||||
|
||||
Extract all SMT-LIB2 files from the `tests/ostrich.zip` archive.
|
||||
|
||||
```bash
|
||||
cd ${{ github.workspace }}
|
||||
|
||||
# Extract the zip archive
|
||||
mkdir -p /tmp/ostrich_benchmarks
|
||||
unzip -q tests/ostrich.zip -d /tmp/ostrich_benchmarks
|
||||
|
||||
# List all .smt2 files
|
||||
find /tmp/ostrich_benchmarks -name "*.smt2" -type f | sort > /tmp/all_ostrich_files.txt
|
||||
TOTAL_FILES=$(wc -l < /tmp/all_ostrich_files.txt)
|
||||
echo "Total Ostrich .smt2 files: $TOTAL_FILES"
|
||||
|
||||
if [ "$TOTAL_FILES" -eq 0 ]; then
|
||||
echo "ERROR: No .smt2 files found in tests/ostrich.zip"
|
||||
exit 1
|
||||
fi
|
||||
```
|
||||
|
||||
Once the benchmark files are confirmed, call the `noop` safe-output tool with the message `"Benchmark files ready: <TOTAL_FILES> Ostrich .smt2 files extracted. Starting benchmark run — this may take over an hour."` This second keepalive refreshes the safe-output MCP session immediately before the long per-file benchmark loop begins.
|
||||
|
||||
## Phase 3: Run Benchmarks
|
||||
|
||||
Run every file from `/tmp/all_ostrich_files.txt` with both Z3 string solvers plus ZIPT, cvc5, and Ostrich2. Use a **5-second timeout** per run.
|
||||
|
||||
For each file, run:
|
||||
1. `z3 smt.string_solver=seq -T:5 <file>` — seq solver
|
||||
2. `z3 smt.string_solver=nseq -T:5 <file>` — nseq (ZIPT) solver
|
||||
3. `dotnet <ZIPT.dll> -t:5000 <file>` — standalone ZIPT solver (milliseconds)
|
||||
4. `cvc5 --lang smt2 --tlimit-per=5000 <file>` — cvc5 (milliseconds)
|
||||
5. `ostrich -timeout=5 <file>` — Ostrich2 (seconds; fallback to outer timeout if unsupported)
|
||||
|
||||
Capture:
|
||||
- **Verdict**: `sat`, `unsat`, `unknown`, `timeout` (if exit code indicates timeout or process is killed), or `bug` (if a solver crashes / produces a non-standard result)
|
||||
- **Time** (seconds): wall-clock time for the run
|
||||
- A row is flagged `SOUNDNESS_DISAGREEMENT` when any two solvers that both produced a definitive answer (sat/unsat) disagree
|
||||
|
||||
Use a bash script to automate this:
|
||||
|
||||
```bash
|
||||
#!/usr/bin/env bash
|
||||
set -euo pipefail
|
||||
|
||||
Z3=${{ github.workspace }}/build/z3
|
||||
ZIPT_DLL=$(find /tmp/zipt/ZIPT/bin/Release -name "ZIPT.dll" 2>/dev/null | head -1)
|
||||
CVC5_BIN=/tmp/cvc5/build/bin/cvc5
|
||||
OSTRICH2_BIN=/tmp/ostrich2/ostrich
|
||||
ZIPT_AVAILABLE=false
|
||||
[ -n "$ZIPT_DLL" ] && ZIPT_AVAILABLE=true
|
||||
CVC5_AVAILABLE=false
|
||||
[ -x "$CVC5_BIN" ] && CVC5_AVAILABLE=true
|
||||
OSTRICH2_AVAILABLE=false
|
||||
[ -x "$OSTRICH2_BIN" ] && OSTRICH2_AVAILABLE=true
|
||||
|
||||
# Ensure libz3.so is on the dynamic-linker path for the .NET runtime
|
||||
export LD_LIBRARY_PATH=${{ github.workspace }}/build${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}
|
||||
|
||||
RESULTS=/tmp/benchmark_results.tsv
|
||||
mkdir -p /tmp/ostrich_run
|
||||
|
||||
echo -e "file\tseq_verdict\tseq_time\tnseq_verdict\tnseq_time\tzipt_verdict\tzipt_time\tcvc5_verdict\tcvc5_time\tostrich2_verdict\tostrich2_time\tnotes" > "$RESULTS"
|
||||
|
||||
run_and_parse() {
|
||||
local sat_pattern="$1"
|
||||
local unsat_pattern="$2"
|
||||
local unknown_pattern="$3"
|
||||
local bug_pattern="$4"
|
||||
shift 4
|
||||
local start end elapsed verdict output exit_code
|
||||
|
||||
start=$(date +%s%3N)
|
||||
set +e
|
||||
output=$("$@" 2>&1)
|
||||
exit_code=$?
|
||||
set -e
|
||||
end=$(date +%s%3N)
|
||||
elapsed=$(echo "scale=3; ($end - $start) / 1000" | bc)
|
||||
|
||||
if [ "$exit_code" -eq 124 ]; then
|
||||
verdict="timeout"
|
||||
elif echo "$output" | grep -Eqi "$unsat_pattern"; then
|
||||
verdict="unsat"
|
||||
elif echo "$output" | grep -Eqi "$sat_pattern"; then
|
||||
verdict="sat"
|
||||
elif echo "$output" | grep -Eqi "$unknown_pattern"; then
|
||||
verdict="unknown"
|
||||
elif echo "$output" | grep -Eqi "$bug_pattern"; then
|
||||
verdict="bug"
|
||||
else
|
||||
verdict="unknown"
|
||||
fi
|
||||
|
||||
echo "$verdict $elapsed"
|
||||
}
|
||||
|
||||
run_z3_seq() {
|
||||
local file="$1"
|
||||
run_and_parse "^sat$" "^unsat$" "^unknown$" "error|assertion|segfault|SIGABRT|exception" \
|
||||
timeout 7 "$Z3" "smt.string_solver=seq" -T:5 "$file"
|
||||
}
|
||||
|
||||
run_z3_nseq() {
|
||||
local file="$1"
|
||||
run_and_parse "^sat$" "^unsat$" "^unknown$" "error|assertion|segfault|SIGABRT|exception" \
|
||||
timeout 7 "$Z3" "smt.string_solver=nseq" -T:5 "$file"
|
||||
}
|
||||
|
||||
run_zipt() {
|
||||
local file="$1"
|
||||
|
||||
if [ "$ZIPT_AVAILABLE" != "true" ]; then
|
||||
echo "n/a 0.000"
|
||||
return
|
||||
fi
|
||||
|
||||
# ZIPT prints the filename on the first line, then SAT/UNSAT/UNKNOWN on subsequent lines
|
||||
run_and_parse "^SAT$" "^UNSAT$" "^UNKNOWN$" "error|crash|exception|Unsupported" \
|
||||
timeout 7 dotnet "$ZIPT_DLL" -t:5000 "$file"
|
||||
}
|
||||
|
||||
run_cvc5() {
|
||||
local file="$1"
|
||||
|
||||
if [ "$CVC5_AVAILABLE" != "true" ]; then
|
||||
echo "n/a 0.000"
|
||||
return
|
||||
fi
|
||||
|
||||
run_and_parse "^sat$" "^unsat$" "^unknown$" "error|fatal|exception|segfault|assert" \
|
||||
timeout 7 "$CVC5_BIN" --lang smt2 --tlimit-per=5000 "$file"
|
||||
}
|
||||
|
||||
run_ostrich2() {
|
||||
local file="$1"
|
||||
|
||||
if [ "$OSTRICH2_AVAILABLE" != "true" ]; then
|
||||
echo "n/a 0.000"
|
||||
return
|
||||
fi
|
||||
|
||||
run_and_parse "^sat$" "^unsat$" "^unknown$" "error|fatal|exception|segfault|assert|Unsupported" \
|
||||
timeout 7 "$OSTRICH2_BIN" -timeout=5 "$file"
|
||||
}
|
||||
|
||||
COUNTER=0
|
||||
while IFS= read -r file; do
|
||||
COUNTER=$((COUNTER + 1))
|
||||
fname=$(basename "$file")
|
||||
|
||||
seq_result=$(run_z3_seq "$file")
|
||||
nseq_result=$(run_z3_nseq "$file")
|
||||
zipt_result=$(run_zipt "$file")
|
||||
cvc5_result=$(run_cvc5 "$file")
|
||||
ostrich2_result=$(run_ostrich2 "$file")
|
||||
|
||||
seq_verdict=$(echo "$seq_result" | cut -d' ' -f1)
|
||||
seq_time=$(echo "$seq_result" | cut -d' ' -f2)
|
||||
nseq_verdict=$(echo "$nseq_result" | cut -d' ' -f1)
|
||||
nseq_time=$(echo "$nseq_result" | cut -d' ' -f2)
|
||||
zipt_verdict=$(echo "$zipt_result" | cut -d' ' -f1)
|
||||
zipt_time=$(echo "$zipt_result" | cut -d' ' -f2)
|
||||
cvc5_verdict=$(echo "$cvc5_result" | cut -d' ' -f1)
|
||||
cvc5_time=$(echo "$cvc5_result" | cut -d' ' -f2)
|
||||
ostrich2_verdict=$(echo "$ostrich2_result" | cut -d' ' -f1)
|
||||
ostrich2_time=$(echo "$ostrich2_result" | cut -d' ' -f2)
|
||||
|
||||
# Flag soundness disagreement when any two definitive verdicts disagree
|
||||
notes=""
|
||||
declare -A definitive_map
|
||||
[ "$seq_verdict" = "sat" ] || [ "$seq_verdict" = "unsat" ] && definitive_map[seq]="$seq_verdict"
|
||||
[ "$nseq_verdict" = "sat" ] || [ "$nseq_verdict" = "unsat" ] && definitive_map[nseq]="$nseq_verdict"
|
||||
[ "$zipt_verdict" = "sat" ] || [ "$zipt_verdict" = "unsat" ] && definitive_map[zipt]="$zipt_verdict"
|
||||
[ "$cvc5_verdict" = "sat" ] || [ "$cvc5_verdict" = "unsat" ] && definitive_map[cvc5]="$cvc5_verdict"
|
||||
[ "$ostrich2_verdict" = "sat" ] || [ "$ostrich2_verdict" = "unsat" ] && definitive_map[ostrich2]="$ostrich2_verdict"
|
||||
has_sat=false; has_unsat=false
|
||||
for v in "${definitive_map[@]}"; do
|
||||
[ "$v" = "sat" ] && has_sat=true
|
||||
[ "$v" = "unsat" ] && has_unsat=true
|
||||
done
|
||||
if $has_sat && $has_unsat; then
|
||||
notes="SOUNDNESS_DISAGREEMENT"
|
||||
fi
|
||||
|
||||
echo -e "$fname\t$seq_verdict\t$seq_time\t$nseq_verdict\t$nseq_time\t$zipt_verdict\t$zipt_time\t$cvc5_verdict\t$cvc5_time\t$ostrich2_verdict\t$ostrich2_time\t$notes" >> "$RESULTS"
|
||||
echo "[$COUNTER] [$fname] seq=$seq_verdict(${seq_time}s) nseq=$nseq_verdict(${nseq_time}s) zipt=$zipt_verdict(${zipt_time}s) cvc5=$cvc5_verdict(${cvc5_time}s) ostrich2=$ostrich2_verdict(${ostrich2_time}s) $notes"
|
||||
done < /tmp/all_ostrich_files.txt
|
||||
|
||||
echo "Benchmark run complete. Results saved to $RESULTS"
|
||||
```
|
||||
|
||||
Save this script to `/tmp/run_ostrich_benchmarks.sh`, make it executable, and run it. Do not skip any file.
|
||||
|
||||
## Phase 4: Generate Summary Report
|
||||
|
||||
Read `/tmp/benchmark_results.tsv` and compute statistics. Then generate a Markdown report.
|
||||
|
||||
Compute:
|
||||
- **Total benchmarks**: total number of files run
|
||||
- **Per solver (seq, nseq, ZIPT, cvc5, and Ostrich2)**: count of sat / unsat / unknown / timeout / bug verdicts
|
||||
- **Total time used**: sum of all times for each solver
|
||||
- **Average time per benchmark**: total_time / total_files
|
||||
- **Soundness disagreements**: files where any two solvers that both returned a definitive answer disagree
|
||||
- **Bugs / crashes**: files with error/crash verdicts
|
||||
|
||||
Format the report as a GitHub Discussion post (GitHub-flavored Markdown):
|
||||
|
||||
```markdown
|
||||
### Ostrich Benchmark Report — Z3 c3 branch
|
||||
|
||||
**Date**: <today's date>
|
||||
**Branch**: c3
|
||||
**Benchmark set**: Ostrich (all files from tests/ostrich.zip)
|
||||
**Timeout**: 5 seconds per benchmark (`-T:5` for Z3; `-t:5000` for ZIPT; `--tlimit-per=5000` for cvc5; `-timeout=5` for Ostrich2)
|
||||
|
||||
---
|
||||
|
||||
### Summary
|
||||
|
||||
| Metric | seq solver | nseq solver | ZIPT solver | cvc5 solver | Ostrich2 solver |
|
||||
|--------|-----------|-------------|-------------|-------------|-----------------|
|
||||
| sat | X | X | X | X | X |
|
||||
| unsat | X | X | X | X | X |
|
||||
| unknown | X | X | X | X | X |
|
||||
| timeout | X | X | X | X | X |
|
||||
| bug/crash | X | X | X | X | X |
|
||||
| **Total time (s)** | X.XXX | X.XXX | X.XXX | X.XXX | X.XXX |
|
||||
| **Avg time/benchmark (s)** | X.XXX | X.XXX | X.XXX | X.XXX | X.XXX |
|
||||
|
||||
**Soundness disagreements** (any two solvers return conflicting sat/unsat): N
|
||||
|
||||
---
|
||||
|
||||
### Per-File Results
|
||||
|
||||
<details>
|
||||
<summary>Click to expand full per-file table</summary>
|
||||
|
||||
| # | File | seq verdict | seq time (s) | nseq verdict | nseq time (s) | ZIPT verdict | ZIPT time (s) | cvc5 verdict | cvc5 time (s) | Ostrich2 verdict | Ostrich2 time (s) | Notes |
|
||||
|---|------|-------------|-------------|--------------|--------------|--------------|--------------|--------------|---------------|------------------|-------------------|-------|
|
||||
| 1 | benchmark_0001.smt2 | sat | 0.123 | sat | 0.456 | sat | 0.789 | sat | 0.111 | sat | 0.222 | |
|
||||
| ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... |
|
||||
|
||||
</details>
|
||||
|
||||
---
|
||||
|
||||
### Notable Issues
|
||||
|
||||
#### Soundness Disagreements (Critical)
|
||||
<list files where any two solvers disagree on sat/unsat, naming which solvers disagree>
|
||||
|
||||
#### Crashes / Bugs
|
||||
<list files where any solver crashed or produced an error>
|
||||
|
||||
#### Slow Benchmarks (> 4s)
|
||||
<list files that took more than 4 seconds for any solver>
|
||||
|
||||
---
|
||||
|
||||
*Generated automatically by the Ostrich Benchmark workflow on the c3 branch.*
|
||||
```
|
||||
|
||||
## Phase 5: Post to GitHub Discussion
|
||||
|
||||
Post the Markdown report as a new GitHub Discussion using the `create-discussion` safe output.
|
||||
|
||||
- **Category**: "Agentic Workflows"
|
||||
- **Title**: `[Ostrich Benchmark] Z3 c3 branch — <date>`
|
||||
- Close older discussions with the same title prefix to avoid clutter.
|
||||
|
||||
## Guidelines
|
||||
|
||||
- **Always build from c3 branch**: The workspace is already checked out on c3; don't change branches.
|
||||
- **Synchronous builds only**: Never run `ninja` (or any other build command) in the background using `&`. Running the build concurrently with LLM inference causes the agent process to be killed by the OOM killer (exit 137) because C++ compilation and the LLM together exceed available RAM. Always wait for each build command to finish before proceeding.
|
||||
- **Release build**: The build uses `CMAKE_BUILD_TYPE=Release` for lower memory footprint and faster compilation on the GitHub Actions runner. The benchmark only needs verdict and timing output; no `-tr:` trace flags are used.
|
||||
- **Run all benchmarks**: Unlike the QF_S workflow, run every file in the archive — do not randomly sample.
|
||||
- **5-second timeout**: Pass `-T:5` to Z3 (both seq and nseq), `-t:5000` to ZIPT, `--tlimit-per=5000` to cvc5, and `-timeout=5` to Ostrich2. Use `timeout 7` as the outer OS-level guard to allow solvers to exit cleanly before being killed.
|
||||
- **Be precise with timing**: Use millisecond-precision timestamps and report times in seconds with 3 decimal places.
|
||||
- **Distinguish timeout from unknown**: A timeout is different from `(unknown)` returned by a solver within its time budget.
|
||||
- **ZIPT output format**: ZIPT prints the input filename on the first line, then `SAT`, `UNSAT`, or `UNKNOWN` on subsequent lines. Parse accordingly.
|
||||
- **cvc5 and Ostrich2 availability**: If cvc5 or Ostrich2 build/setup fails, keep benchmarking with available solvers and emit `n/a` verdict/time for unavailable ones.
|
||||
- **Report soundness bugs prominently**: If any benchmark shows a conflict between any two solvers that both returned a definitive sat/unsat answer, highlight it as a critical finding and name which pair disagrees.
|
||||
- **Handle build failures gracefully**: If Z3 fails to build, report the error and create a brief discussion noting the build failure. If any external solver (ZIPT/cvc5/Ostrich2) fails to build, continue with available solver columns and note `n/a` for unavailable solvers.
|
||||
- **Large report**: Always put the per-file table in a `<details>` collapsible section since there may be many files.
|
||||
- **Progress logging**: Print a line per file as you run it (e.g., `[N] [filename] seq=...`) so the workflow log shows progress even for large benchmark sets.
|
||||
|
||||
## Safe Output Guarantee
|
||||
|
||||
You **MUST** call either `create_discussion` or `noop` before the workflow ends, regardless of what happened during execution:
|
||||
|
||||
- **Build succeeded, benchmarks ran**: Call `create_discussion` with the full report.
|
||||
- **Build succeeded, benchmarks partially ran**: Call `create_discussion` with whatever results were collected and a note about what could not be completed.
|
||||
- **Z3 build failed**: Call `noop` with a brief message describing the build error.
|
||||
- **No benchmarks could be run**: Call `noop` with a summary of what failed and why.
|
||||
|
||||
Failing to produce any safe output triggers an automatic workflow-failure issue that clutters the repository.
|
||||
1715
.github/workflows/specbot-crash-analyzer.lock.yml
generated
vendored
1715
.github/workflows/specbot-crash-analyzer.lock.yml
generated
vendored
File diff suppressed because one or more lines are too long
253
.github/workflows/specbot-crash-analyzer.md
vendored
253
.github/workflows/specbot-crash-analyzer.md
vendored
|
|
@ -1,253 +0,0 @@
|
|||
---
|
||||
description: >
|
||||
Build Z3 in debug mode from the c3 branch, compile and run the specbot tests,
|
||||
identify root causes for any crashes, and post findings as a GitHub Discussion.
|
||||
|
||||
on:
|
||||
workflow_dispatch:
|
||||
|
||||
timeout-minutes: 120
|
||||
|
||||
permissions:
|
||||
contents: read
|
||||
issues: read
|
||||
pull-requests: read
|
||||
discussions: read
|
||||
copilot-requests: write
|
||||
|
||||
network: defaults
|
||||
|
||||
tools:
|
||||
cache-memory: true
|
||||
github:
|
||||
toolsets: [default, discussions]
|
||||
bash: [":*"]
|
||||
edit: {}
|
||||
|
||||
safe-outputs:
|
||||
report-failure-as-issue: false
|
||||
create-discussion:
|
||||
title-prefix: "[Specbot] "
|
||||
category: "Agentic Workflows"
|
||||
close-older-discussions: true
|
||||
missing-tool:
|
||||
create-issue: true
|
||||
noop:
|
||||
report-as-issue: false
|
||||
|
||||
steps:
|
||||
- name: Checkout c3 branch
|
||||
uses: actions/checkout@v6.0.2
|
||||
with:
|
||||
ref: c3
|
||||
persist-credentials: false
|
||||
|
||||
- name: Install build dependencies
|
||||
run: |
|
||||
sudo apt-get update -y
|
||||
sudo apt-get install -y cmake ninja-build python3 gcc g++ 2>&1 | tail -5
|
||||
|
||||
- name: Build Z3 in debug mode
|
||||
id: build-z3
|
||||
continue-on-error: true
|
||||
run: |
|
||||
mkdir -p build/debug specbot-results
|
||||
cd build/debug
|
||||
cmake -G Ninja -DCMAKE_BUILD_TYPE=Debug ../.. 2>&1 | tee ../../specbot-results/cmake.log
|
||||
ninja 2>&1 | tee ../../specbot-results/build.log
|
||||
BUILD_EXIT=$?
|
||||
cd ../..
|
||||
echo "build_exit=${BUILD_EXIT}" >> specbot-results/build-status.txt
|
||||
ls -la build/debug/libz3* build/debug/*.so* 2>/dev/null >> specbot-results/build-status.txt || echo "Library not found" >> specbot-results/build-status.txt
|
||||
exit $BUILD_EXIT
|
||||
|
||||
- name: Compile specbot tests
|
||||
continue-on-error: true
|
||||
run: |
|
||||
mkdir -p specbot-results
|
||||
gcc -g -O0 \
|
||||
-I src/api \
|
||||
specbot/test_specbot_seq.c \
|
||||
-L build/debug \
|
||||
-lz3 \
|
||||
-Wl,-rpath,"${GITHUB_WORKSPACE}/build/debug" \
|
||||
-o specbot-results/test_specbot_seq \
|
||||
2>&1 | tee specbot-results/compile_specbot_seq.log
|
||||
echo "compile_specbot_seq_exit=$?" >> specbot-results/compile-status.txt
|
||||
|
||||
gcc -g -O0 \
|
||||
-I src/api \
|
||||
specbot/test_deeptest_seq.c \
|
||||
-L build/debug \
|
||||
-lz3 \
|
||||
-Wl,-rpath,"${GITHUB_WORKSPACE}/build/debug" \
|
||||
-o specbot-results/test_deeptest_seq \
|
||||
2>&1 | tee specbot-results/compile_deeptest_seq.log
|
||||
echo "compile_deeptest_seq_exit=$?" >> specbot-results/compile-status.txt
|
||||
|
||||
- name: Run specbot tests
|
||||
continue-on-error: true
|
||||
run: |
|
||||
mkdir -p specbot-results
|
||||
if [ -f specbot-results/test_specbot_seq ]; then
|
||||
LD_LIBRARY_PATH="${GITHUB_WORKSPACE}/build/debug" timeout 120 specbot-results/test_specbot_seq > specbot-results/test_specbot_seq.log 2>&1
|
||||
SPECBOT_EXIT=$?
|
||||
echo "specbot_seq_exit=${SPECBOT_EXIT}" >> specbot-results/test-status.txt
|
||||
else
|
||||
echo "Binary not compiled" > specbot-results/test_specbot_seq.log
|
||||
echo "specbot_seq_exit=127" >> specbot-results/test-status.txt
|
||||
fi
|
||||
|
||||
if [ -f specbot-results/test_deeptest_seq ]; then
|
||||
LD_LIBRARY_PATH="${GITHUB_WORKSPACE}/build/debug" timeout 120 specbot-results/test_deeptest_seq > specbot-results/test_deeptest_seq.log 2>&1
|
||||
DEEPTEST_EXIT=$?
|
||||
echo "deeptest_seq_exit=${DEEPTEST_EXIT}" >> specbot-results/test-status.txt
|
||||
else
|
||||
echo "Binary not compiled" > specbot-results/test_deeptest_seq.log
|
||||
echo "deeptest_seq_exit=127" >> specbot-results/test-status.txt
|
||||
fi
|
||||
|
||||
---
|
||||
|
||||
# Specbot Crash Analyzer
|
||||
|
||||
## Job Description
|
||||
|
||||
Your name is ${{ github.workflow }}. You are an expert C/C++ and SMT solver analyst for the Z3 theorem prover
|
||||
repository `${{ github.repository }}`. The pre-steps above have already built Z3 in debug mode from the `c3`
|
||||
branch, compiled and run the specbot test suite, and saved all output to the `specbot-results/` directory in
|
||||
the workspace (`${{ github.workspace }}/specbot-results/`). Your task is to analyze those results, diagnose
|
||||
any crash root causes by reading the relevant source files, and publish a structured findings report as a
|
||||
GitHub Discussion.
|
||||
|
||||
**Do not try to build Z3 or run tests yourself.** All build and test output is already in `specbot-results/`.
|
||||
|
||||
## Your Task
|
||||
|
||||
### 1. Read the Pre-Generated Results
|
||||
|
||||
All build and test outputs are in `specbot-results/` (relative to the workspace root). Read each file:
|
||||
|
||||
```bash
|
||||
# Build status
|
||||
cat specbot-results/build-status.txt 2>/dev/null || echo "No build status"
|
||||
|
||||
# Compile status
|
||||
cat specbot-results/compile-status.txt 2>/dev/null || echo "No compile status"
|
||||
|
||||
# Test status
|
||||
cat specbot-results/test-status.txt 2>/dev/null || echo "No test status"
|
||||
|
||||
# Test output from test_specbot_seq
|
||||
cat specbot-results/test_specbot_seq.log 2>/dev/null || echo "No test_specbot_seq output"
|
||||
|
||||
# Test output from test_deeptest_seq
|
||||
cat specbot-results/test_deeptest_seq.log 2>/dev/null || echo "No test_deeptest_seq output"
|
||||
|
||||
# Last 30 lines of the build log
|
||||
tail -30 specbot-results/build.log 2>/dev/null || echo "No build log"
|
||||
```
|
||||
|
||||
If `specbot-results/build-status.txt` shows `build_exit=0`, the build succeeded.
|
||||
If it shows a non-zero exit, include the last 50 lines of `specbot-results/build.log` in the report
|
||||
under a "Build Failure" section.
|
||||
|
||||
If `specbot-results/compile-status.txt` shows a non-zero exit for a test, include the compile error
|
||||
from `specbot-results/compile_specbot_seq.log` or `specbot-results/compile_deeptest_seq.log`.
|
||||
|
||||
Collect every line containing `CRASH` or `ABORT` from the test log files — these are the crashes to analyze.
|
||||
|
||||
### 2. Diagnose Each Crash
|
||||
|
||||
For each crashed test function, perform the following analysis:
|
||||
|
||||
1. **Identify the test body**: read `specbot/test_specbot_seq.c` or `specbot/test_deeptest_seq.c`
|
||||
to understand what Z3 API calls the test makes and what invariants it exercises.
|
||||
|
||||
2. **Find the likely crash site**: the test exercises the Z3 Nielsen/nseq string solver. Relevant source files are:
|
||||
- `src/smt/seq_solver.h` and `src/smt/seq_solver.cpp` (or nearby files)
|
||||
- `src/smt/seq_axioms.cpp`, `src/smt/seq_eq_solver.cpp`, `src/smt/seq_regex.cpp`
|
||||
- `src/math/lp/` for length-arithmetic paths
|
||||
- `src/api/z3_api.h` for the public API entry points
|
||||
|
||||
Use `grep` and `view` to locate assertion macros, `UNREACHABLE()`, `SASSERT`, or `throw` statements
|
||||
in the code paths exercised by the failing test. Example:
|
||||
```bash
|
||||
grep -rn "SASSERT\|UNREACHABLE\|Z3_CATCH" src/smt/seq_solver.cpp 2>/dev/null | head -30
|
||||
```
|
||||
|
||||
3. **Hypothesize root cause**: based on the Z3 API calls in the test and the assertion/throw sites in
|
||||
the solver source, state the most likely root cause. Common categories include:
|
||||
- Violated invariant (SASSERT/UNREACHABLE hit due to unexpected solver state)
|
||||
- Use-after-free or dangling reference during push/pop
|
||||
- Unhandled edge case in Nielsen graph construction
|
||||
- Missing theory-combination lemma between string length and integer arithmetic
|
||||
|
||||
4. **Suggest a fix**: propose a minimal, concrete fix — e.g., a guard condition, an additional lemma,
|
||||
a missing reference-count increment, or a missing case in a switch/match.
|
||||
|
||||
### 3. Generate the Report
|
||||
|
||||
After analyzing all crashes, produce a structured GitHub Discussion in the "Agentic Workflows" category
|
||||
using `create-discussion`.
|
||||
|
||||
The discussion body must follow this structure (use `###` and lower for headers):
|
||||
|
||||
```
|
||||
### Summary
|
||||
|
||||
- Build: Debug (CMake + Ninja, c3 branch)
|
||||
- Tests compiled: N
|
||||
- Tests run: N
|
||||
- Tests passed: N
|
||||
- Tests crashed: N
|
||||
- Tests timed out: N
|
||||
|
||||
### Crash Findings
|
||||
|
||||
For each crash, one subsection:
|
||||
|
||||
#### <test function name>
|
||||
|
||||
**Test file**: `specbot/test_specbot_seq.c` or `specbot/test_deeptest_seq.c`
|
||||
|
||||
**Observed failure**: ABORT/CRASH — one-line description of what was caught
|
||||
|
||||
**Root cause hypothesis**: explanation of which assertion or code path was hit and why
|
||||
|
||||
**Suggested fix**: concrete proposed change (file, function, what to add/change)
|
||||
|
||||
---
|
||||
|
||||
### Tests Passed
|
||||
|
||||
List of test names that passed.
|
||||
|
||||
<details>
|
||||
<summary><b>Full Test Output</b></summary>
|
||||
|
||||
Raw stdout/stderr from both test binaries.
|
||||
|
||||
</details>
|
||||
|
||||
<details>
|
||||
<summary><b>Build Log</b></summary>
|
||||
|
||||
Last 30 lines of the ninja build output.
|
||||
|
||||
</details>
|
||||
```
|
||||
|
||||
If there are no crashes at all, write a "No Crashes Found" summary celebrating that all tests passed,
|
||||
and include the full test output in a collapsible section.
|
||||
|
||||
Use `mentions: false` behavior — do not mention any GitHub usernames in the report.
|
||||
|
||||
Format workflow run references as: `[§${{ github.run_id }}](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})`.
|
||||
|
||||
## Usage
|
||||
|
||||
Trigger via **Actions → Specbot Crash Analyzer → Run workflow** on any branch. The pre-steps
|
||||
always check out the `c3` branch where `specbot/test_specbot_seq.c` and
|
||||
`specbot/test_deeptest_seq.c` live, build Z3, run the tests, and save results to `specbot-results/`.
|
||||
The agent then analyzes the results and posts a discussion to the "Agentic Workflows" category.
|
||||
1586
.github/workflows/tptp-benchmark.lock.yml
generated
vendored
1586
.github/workflows/tptp-benchmark.lock.yml
generated
vendored
File diff suppressed because one or more lines are too long
551
.github/workflows/tptp-benchmark.md
vendored
551
.github/workflows/tptp-benchmark.md
vendored
|
|
@ -1,551 +0,0 @@
|
|||
---
|
||||
description: >
|
||||
Weekly benchmark of Z3's TPTP front-end against 500 random TPTP problems.
|
||||
Downloads TPTP benchmarks from tptp.org, resolves axiom dependencies,
|
||||
skips large problems, runs each with a 5-second timeout, and posts a
|
||||
discrepancy/crash report as a GitHub discussion.
|
||||
|
||||
on:
|
||||
schedule:
|
||||
- cron: "0 6 * * 1"
|
||||
workflow_dispatch:
|
||||
|
||||
permissions:
|
||||
contents: read
|
||||
issues: read
|
||||
pull-requests: read
|
||||
copilot-requests: write
|
||||
|
||||
network:
|
||||
allowed:
|
||||
- defaults
|
||||
- tptp.org
|
||||
|
||||
tools:
|
||||
bash: true
|
||||
github:
|
||||
toolsets: [default]
|
||||
|
||||
safe-outputs:
|
||||
report-failure-as-issue: false
|
||||
create-discussion:
|
||||
title-prefix: "[TPTP Benchmark] "
|
||||
category: "Agentic Workflows"
|
||||
close-older-discussions: true
|
||||
expires: 14d
|
||||
missing-tool:
|
||||
create-issue: true
|
||||
noop:
|
||||
report-as-issue: false
|
||||
|
||||
timeout-minutes: 300
|
||||
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
uses: actions/checkout@v6.0.2
|
||||
with:
|
||||
persist-credentials: false
|
||||
|
||||
- name: Install build dependencies
|
||||
run: |
|
||||
sudo apt-get update -y -q
|
||||
sudo apt-get install -y cmake ninja-build python3 wget curl bc
|
||||
|
||||
- name: Build Z3
|
||||
run: |
|
||||
mkdir -p /tmp/z3-build
|
||||
cd /tmp/z3-build
|
||||
cmake "$GITHUB_WORKSPACE" \
|
||||
-G Ninja \
|
||||
-DCMAKE_BUILD_TYPE=Release \
|
||||
-DZ3_BUILD_TEST_EXECUTABLES=OFF
|
||||
ninja -j$(nproc) z3
|
||||
./z3 --version
|
||||
|
||||
---
|
||||
|
||||
# TPTP Front-End Benchmark
|
||||
|
||||
## Job Description
|
||||
|
||||
Your name is ${{ github.workflow }}. You are an expert testing engineer for the Z3 theorem prover. Your task is to:
|
||||
|
||||
1. Verify the Z3 binary built by the pre-flight step is available
|
||||
2. Download the TPTP benchmark library from tptp.org
|
||||
3. Select 500 random small-to-medium problems (with their axiom dependencies)
|
||||
4. Run each problem through Z3's TPTP front-end with a 5-second timeout
|
||||
5. Compare Z3's output against the expected SZS status declared in each problem file
|
||||
6. Post a detailed report as a GitHub Discussion summarising discrepancies and crashes
|
||||
|
||||
**Repository**: ${{ github.repository }}
|
||||
**Workspace**: ${{ github.workspace }}
|
||||
|
||||
## Phase 1: Verify Z3 Binary
|
||||
|
||||
Z3 was built by the workflow pre-flight step and is available at `/tmp/z3-build/z3`.
|
||||
Confirm the binary is present and functional:
|
||||
|
||||
```bash
|
||||
/tmp/z3-build/z3 --version
|
||||
```
|
||||
|
||||
If the binary is missing or returns an error, call the `noop` safe-output with a message describing the problem and stop.
|
||||
|
||||
Once confirmed, call `noop` with `"Z3 binary verified. Downloading TPTP benchmark library — this may take a few minutes."` to keep the safe-output session alive.
|
||||
|
||||
## Phase 2: Download the TPTP Problem Library
|
||||
|
||||
Find the latest TPTP release and download the full archive.
|
||||
|
||||
```bash
|
||||
# Find the latest TPTP distribution version by fetching the directory listing
|
||||
TPTP_DIST_URL="https://tptp.org/TPTP/Distribution/"
|
||||
LATEST_TGZ=$(curl -sL "$TPTP_DIST_URL" \
|
||||
| grep -oP 'TPTP-v[0-9]+\.[0-9]+\.[0-9]+\.tgz' \
|
||||
| sort -V | tail -1)
|
||||
|
||||
if [ -z "$LATEST_TGZ" ]; then
|
||||
echo "ERROR: Could not determine latest TPTP version from $TPTP_DIST_URL"
|
||||
# Fall back to a known stable version
|
||||
LATEST_TGZ="TPTP-v9.0.0.tgz"
|
||||
fi
|
||||
|
||||
echo "Downloading $LATEST_TGZ ..."
|
||||
mkdir -p /tmp/tptp_download
|
||||
wget -q --show-progress \
|
||||
"${TPTP_DIST_URL}${LATEST_TGZ}" \
|
||||
-O /tmp/tptp_download/tptp.tgz
|
||||
|
||||
echo "Extracting TPTP library..."
|
||||
mkdir -p /tmp/tptp
|
||||
tar -xzf /tmp/tptp_download/tptp.tgz -C /tmp/tptp --strip-components=1 2>&1 | tail -5
|
||||
|
||||
# Verify extraction
|
||||
if [ ! -d /tmp/tptp/Problems ] || [ ! -d /tmp/tptp/Axioms ]; then
|
||||
echo "ERROR: TPTP extraction failed — Problems/ or Axioms/ directory not found"
|
||||
ls /tmp/tptp/
|
||||
exit 1
|
||||
fi
|
||||
|
||||
TPTP_ROOT=/tmp/tptp
|
||||
echo "TPTP library extracted to $TPTP_ROOT"
|
||||
echo "Problem domains available:"
|
||||
ls "$TPTP_ROOT/Problems/" | wc -l
|
||||
echo "Axiom files available:"
|
||||
ls "$TPTP_ROOT/Axioms/" | wc -l
|
||||
```
|
||||
|
||||
If the download or extraction fails, call `noop` with the error details and stop.
|
||||
|
||||
Call `noop` with `"TPTP library downloaded and extracted. Selecting 500 benchmark problems — filtering by size."` to keep the session alive.
|
||||
|
||||
## Phase 3: Select 500 Benchmark Problems
|
||||
|
||||
Filter out large problems and problems that depend on large axiom files, then take a random sample of 500.
|
||||
|
||||
Save this script to `/tmp/select_benchmarks.py` and run it:
|
||||
|
||||
```python
|
||||
#!/usr/bin/env python3
|
||||
"""
|
||||
Select 500 random TPTP problems that:
|
||||
- Have a known, conclusive expected status (Theorem, Unsatisfiable,
|
||||
CounterSatisfiable, Satisfiable) OR Unknown/Open status.
|
||||
- Are not "large" (problem file <= 50 KB).
|
||||
- Do not include any axiom file larger than 100 KB.
|
||||
"""
|
||||
import os
|
||||
import re
|
||||
import random
|
||||
import sys
|
||||
|
||||
TPTP_ROOT = "/tmp/tptp"
|
||||
PROBLEMS_DIR = os.path.join(TPTP_ROOT, "Problems")
|
||||
AXIOMS_DIR = os.path.join(TPTP_ROOT, "Axioms")
|
||||
MAX_PROBLEM_SIZE = 50 * 1024 # 50 KB
|
||||
MAX_AXIOM_SIZE = 100 * 1024 # 100 KB
|
||||
SAMPLE_SIZE = 500
|
||||
OUTPUT_FILE = "/tmp/selected_benchmarks.txt"
|
||||
|
||||
include_re = re.compile(r"include\s*\(\s*['\"]([^'\"]+)['\"]", re.IGNORECASE)
|
||||
status_re = re.compile(r"%\s*Status\s*:\s*(\S+)", re.IGNORECASE)
|
||||
|
||||
def axiom_sizes_ok(problem_path):
|
||||
"""Return True if all included axiom files exist and are <= MAX_AXIOM_SIZE."""
|
||||
try:
|
||||
with open(problem_path, encoding="utf-8", errors="replace") as f:
|
||||
content = f.read(4096) # header is in first few KB
|
||||
except OSError:
|
||||
return False
|
||||
for m in include_re.finditer(content):
|
||||
axiom_rel = m.group(1) # e.g. "Axioms/AGT001+0.ax"
|
||||
axiom_path = os.path.join(TPTP_ROOT, axiom_rel)
|
||||
if not os.path.exists(axiom_path):
|
||||
return False # axiom missing — skip
|
||||
if os.path.getsize(axiom_path) > MAX_AXIOM_SIZE:
|
||||
return False # axiom too large — skip
|
||||
return True
|
||||
|
||||
candidates = []
|
||||
skipped_size = 0
|
||||
skipped_axiom = 0
|
||||
|
||||
for domain in sorted(os.listdir(PROBLEMS_DIR)):
|
||||
domain_dir = os.path.join(PROBLEMS_DIR, domain)
|
||||
if not os.path.isdir(domain_dir):
|
||||
continue
|
||||
for fname in os.listdir(domain_dir):
|
||||
if not fname.endswith(".p"):
|
||||
continue
|
||||
fpath = os.path.join(domain_dir, fname)
|
||||
size = os.path.getsize(fpath)
|
||||
if size > MAX_PROBLEM_SIZE:
|
||||
skipped_size += 1
|
||||
continue
|
||||
if not axiom_sizes_ok(fpath):
|
||||
skipped_axiom += 1
|
||||
continue
|
||||
candidates.append(fpath)
|
||||
|
||||
print(f"Total candidates (after filtering): {len(candidates)}", flush=True)
|
||||
print(f" Skipped — problem too large : {skipped_size}", flush=True)
|
||||
print(f" Skipped — axiom too large : {skipped_axiom}", flush=True)
|
||||
|
||||
if len(candidates) == 0:
|
||||
print("ERROR: No suitable benchmark problems found.", file=sys.stderr)
|
||||
sys.exit(1)
|
||||
|
||||
if len(candidates) > SAMPLE_SIZE:
|
||||
random.seed(42)
|
||||
selected = random.sample(candidates, SAMPLE_SIZE)
|
||||
else:
|
||||
selected = candidates
|
||||
|
||||
selected.sort()
|
||||
with open(OUTPUT_FILE, "w") as f:
|
||||
f.write("\n".join(selected) + "\n")
|
||||
|
||||
print(f"Selected {len(selected)} problems → {OUTPUT_FILE}", flush=True)
|
||||
```
|
||||
|
||||
Run the script:
|
||||
|
||||
```bash
|
||||
python3 /tmp/select_benchmarks.py
|
||||
SELECTED=$(wc -l < /tmp/selected_benchmarks.txt)
|
||||
echo "Benchmark set: $SELECTED problems"
|
||||
```
|
||||
|
||||
If no problems are found, call `noop` with an error message and stop.
|
||||
|
||||
Call `noop` with `"$SELECTED problems selected. Starting benchmark run with 5-second timeout per problem — this will take approximately $(( SELECTED * 7 / 60 )) minutes."` to keep the session alive.
|
||||
|
||||
## Phase 4: Run Benchmarks
|
||||
|
||||
Save the following script to `/tmp/run_tptp_benchmarks.sh`, make it executable, and run it.
|
||||
|
||||
```bash
|
||||
#!/usr/bin/env bash
|
||||
set -euo pipefail
|
||||
|
||||
Z3=/tmp/z3-build/z3
|
||||
TPTP_ROOT=/tmp/tptp
|
||||
TIMEOUT_HARD=8 # outer OS-level guard (seconds; 3 s beyond Z3's -T:5)
|
||||
Z3_TIMEOUT=5 # Z3 internal timeout: -T:N sets N-second limit (uppercase -T is seconds)
|
||||
|
||||
RESULTS=/tmp/tptp_results.tsv
|
||||
PROBLEM_LIST=/tmp/selected_benchmarks.txt
|
||||
|
||||
echo -e "file\texpected\tactual\ttime_s\tnotes" > "$RESULTS"
|
||||
|
||||
# Helper: extract the expected SZS status from the TPTP problem header.
|
||||
get_expected_status() {
|
||||
local file="$1"
|
||||
# Look for lines like: "% Status : Theorem"
|
||||
grep -m1 -iP '%\s*Status\s*:\s*\K\S+' "$file" 2>/dev/null || echo "Unknown"
|
||||
}
|
||||
|
||||
# Helper: run z3 on a single TPTP problem with timeout.
|
||||
run_benchmark() {
|
||||
local file="$1"
|
||||
local start end elapsed output exit_code verdict
|
||||
|
||||
start=$(date +%s%3N) # milliseconds since epoch
|
||||
output=$(TPTP="$TPTP_ROOT" timeout "$TIMEOUT_HARD" \
|
||||
"$Z3" -tptp -T:"$Z3_TIMEOUT" "$file" 2>&1) || exit_code=$?
|
||||
exit_code=${exit_code:-0}
|
||||
end=$(date +%s%3N)
|
||||
elapsed=$(echo "scale=3; ($end - $start) / 1000" | bc)
|
||||
|
||||
# Extract SZS status line from output
|
||||
szs_line=$(echo "$output" | grep -m1 "% SZS status" || true)
|
||||
|
||||
if [ -n "$szs_line" ]; then
|
||||
# Parse the status keyword (e.g. "Theorem", "CounterSatisfiable", "GaveUp")
|
||||
verdict=$(echo "$szs_line" | grep -oP '% SZS status \K\S+' || echo "Unknown")
|
||||
elif [ "$exit_code" -eq 124 ]; then
|
||||
verdict="Timeout"
|
||||
elif [ "$exit_code" -ne 0 ]; then
|
||||
verdict="Crash"
|
||||
else
|
||||
verdict="NoOutput"
|
||||
fi
|
||||
|
||||
echo "$verdict $elapsed"
|
||||
}
|
||||
|
||||
COUNTER=0
|
||||
TOTAL=$(wc -l < "$PROBLEM_LIST")
|
||||
|
||||
while IFS= read -r problem_file; do
|
||||
COUNTER=$((COUNTER + 1))
|
||||
|
||||
expected=$(get_expected_status "$problem_file")
|
||||
result_line=$(run_benchmark "$problem_file")
|
||||
actual=$(echo "$result_line" | cut -d' ' -f1)
|
||||
elapsed=$(echo "$result_line" | cut -d' ' -f2)
|
||||
fname=$(basename "$problem_file")
|
||||
|
||||
# Classify notes
|
||||
notes=""
|
||||
# Soundness discrepancy: both answers are conclusive but conflict
|
||||
conclusive_expected=false
|
||||
conclusive_actual=false
|
||||
case "$expected" in
|
||||
Theorem|Unsatisfiable) conclusive_expected=true ;;
|
||||
Satisfiable|CounterSatisfiable) conclusive_expected=true ;;
|
||||
esac
|
||||
case "$actual" in
|
||||
Theorem|Unsatisfiable) conclusive_actual=true ;;
|
||||
Satisfiable|CounterSatisfiable) conclusive_actual=true ;;
|
||||
esac
|
||||
|
||||
if $conclusive_expected && $conclusive_actual; then
|
||||
# Map expected to the Z3 output equivalents for comparison
|
||||
# Theorem (has-conjecture unsat) matches "Theorem"
|
||||
# Unsatisfiable (no-conjecture unsat) matches "Unsatisfiable"
|
||||
# Satisfiable (no-conjecture sat) matches "Satisfiable"
|
||||
# CounterSatisfiable (has-conjecture sat) matches "CounterSatisfiable"
|
||||
if [ "$expected" != "$actual" ]; then
|
||||
# Check for sat/unsat polarity conflict
|
||||
sat_expected=false; sat_actual=false
|
||||
case "$expected" in Satisfiable|CounterSatisfiable) sat_expected=true ;; esac
|
||||
case "$actual" in Satisfiable|CounterSatisfiable) sat_actual=true ;; esac
|
||||
if [ "$sat_expected" != "$sat_actual" ]; then
|
||||
notes="SOUNDNESS_ERROR"
|
||||
else
|
||||
notes="STATUS_MISMATCH"
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
|
||||
if [ "$actual" = "Crash" ]; then
|
||||
notes="CRASH"
|
||||
fi
|
||||
|
||||
echo -e "$fname\t$expected\t$actual\t$elapsed\t$notes" >> "$RESULTS"
|
||||
|
||||
if [ -n "$notes" ]; then
|
||||
echo "[$COUNTER/$TOTAL] $fname expected=$expected actual=$actual time=${elapsed}s *** $notes ***"
|
||||
elif [ $((COUNTER % 50)) -eq 0 ]; then
|
||||
echo "[$COUNTER/$TOTAL] Progress checkpoint last=$fname actual=$actual time=${elapsed}s"
|
||||
fi
|
||||
|
||||
done < "$PROBLEM_LIST"
|
||||
|
||||
echo "Benchmark run complete: $COUNTER problems processed. Results → $RESULTS"
|
||||
```
|
||||
|
||||
Run it:
|
||||
|
||||
```bash
|
||||
chmod +x /tmp/run_tptp_benchmarks.sh
|
||||
/tmp/run_tptp_benchmarks.sh
|
||||
```
|
||||
|
||||
Do not skip any file in the list.
|
||||
|
||||
## Phase 5: Analyze Results
|
||||
|
||||
Save the following script to `/tmp/analyze_tptp.py` and run it:
|
||||
|
||||
```python
|
||||
#!/usr/bin/env python3
|
||||
"""Compute summary statistics from the TPTP benchmark TSV."""
|
||||
import csv
|
||||
|
||||
RESULTS_FILE = "/tmp/tptp_results.tsv"
|
||||
|
||||
rows = []
|
||||
with open(RESULTS_FILE, newline="") as f:
|
||||
reader = csv.DictReader(f, delimiter="\t")
|
||||
for row in reader:
|
||||
rows.append(row)
|
||||
|
||||
total = len(rows)
|
||||
|
||||
# Verdict counts
|
||||
from collections import Counter, defaultdict
|
||||
actual_counts = Counter(r["actual"] for r in rows)
|
||||
expected_counts = Counter(r["expected"] for r in rows)
|
||||
|
||||
# Flagged rows
|
||||
soundness_errors = [r for r in rows if r["notes"] == "SOUNDNESS_ERROR"]
|
||||
status_mismatches = [r for r in rows if r["notes"] == "STATUS_MISMATCH"]
|
||||
crashes = [r for r in rows if r["notes"] == "CRASH"]
|
||||
timeouts = [r for r in rows if r["actual"] == "Timeout"]
|
||||
gave_up = [r for r in rows if r["actual"] == "GaveUp"]
|
||||
|
||||
# Solved correctly (expected matches actual for conclusive verdicts)
|
||||
conclusive_expected = {"Theorem", "Unsatisfiable", "Satisfiable", "CounterSatisfiable"}
|
||||
correct = [r for r in rows
|
||||
if r["expected"] in conclusive_expected
|
||||
and r["actual"] == r["expected"]]
|
||||
|
||||
print(f"TOTAL={total}")
|
||||
print(f"CORRECT={len(correct)}")
|
||||
print(f"TIMEOUTS={len(timeouts)}")
|
||||
print(f"GAVE_UP={len(gave_up)}")
|
||||
print(f"CRASHES={len(crashes)}")
|
||||
print(f"SOUNDNESS_ERRORS={len(soundness_errors)}")
|
||||
print(f"STATUS_MISMATCHES={len(status_mismatches)}")
|
||||
|
||||
print("\n--- Actual verdict breakdown ---")
|
||||
for v, c in sorted(actual_counts.items()):
|
||||
print(f" {v}: {c}")
|
||||
|
||||
print("\n--- Expected status breakdown ---")
|
||||
for v, c in sorted(expected_counts.items()):
|
||||
print(f" {v}: {c}")
|
||||
|
||||
if soundness_errors:
|
||||
print(f"\n--- SOUNDNESS ERRORS ({len(soundness_errors)}) ---")
|
||||
for r in soundness_errors:
|
||||
print(f" {r['file']} expected={r['expected']} actual={r['actual']}")
|
||||
|
||||
if crashes:
|
||||
print(f"\n--- CRASHES ({len(crashes)}) ---")
|
||||
for r in crashes:
|
||||
print(f" {r['file']} expected={r['expected']}")
|
||||
|
||||
if status_mismatches:
|
||||
print(f"\n--- STATUS MISMATCHES ({len(status_mismatches)}) ---")
|
||||
for r in status_mismatches[:20]:
|
||||
print(f" {r['file']} expected={r['expected']} actual={r['actual']}")
|
||||
```
|
||||
|
||||
Run the analysis:
|
||||
|
||||
```bash
|
||||
python3 /tmp/analyze_tptp.py
|
||||
```
|
||||
|
||||
## Phase 6: Generate and Post the Discussion Report
|
||||
|
||||
Read the TSV at `/tmp/tptp_results.tsv` and the analysis output, then compose a Markdown report and call `create_discussion`.
|
||||
|
||||
The report should use `###` or lower for all headers (never `#` or `##`). Use collapsible `<details>` sections for large tables.
|
||||
|
||||
Use this structure:
|
||||
|
||||
```markdown
|
||||
**Date**: <today's date>
|
||||
**Branch**: master
|
||||
**Commit**: `<short SHA>` (run `git rev-parse --short HEAD` in ${{ github.workspace }} to get the SHA)
|
||||
**Workflow Run**: [${{ github.run_id }}](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})
|
||||
**TPTP version**: <downloaded version>
|
||||
**Problems benchmarked**: <N> (random sample, timeout 5 s per problem)
|
||||
|
||||
---
|
||||
|
||||
### Summary
|
||||
|
||||
| Metric | Count |
|
||||
|--------|-------|
|
||||
| Total problems run | N |
|
||||
| Correct (expected = actual) | N |
|
||||
| Timeouts | N |
|
||||
| GaveUp (within time budget) | N |
|
||||
| Crashes / errors | N |
|
||||
| Soundness errors (sat↔unsat conflict) | N |
|
||||
| Status mismatches (Theorem vs Unsatisfiable etc.) | N |
|
||||
|
||||
### Expected Status Distribution
|
||||
|
||||
| Expected Status | Count |
|
||||
|----------------|-------|
|
||||
| Theorem | N |
|
||||
| Unsatisfiable | N |
|
||||
| Satisfiable | N |
|
||||
| CounterSatisfiable | N |
|
||||
| Unknown / Open | N |
|
||||
|
||||
---
|
||||
|
||||
### ⚠️ Critical: Soundness Errors
|
||||
|
||||
[List ALL files where Z3 returned a conclusive answer that contradicts the expected answer
|
||||
(e.g., expected Theorem but got CounterSatisfiable). If none, write "None detected."]
|
||||
|
||||
### 💥 Crashes
|
||||
|
||||
[List ALL files where Z3 crashed (non-zero exit, no SZS output, not a timeout).
|
||||
Include filename and expected status. If none, write "None detected."]
|
||||
|
||||
### Status Mismatches
|
||||
|
||||
[Files where both answers are conclusive but differ in Theorem vs Unsatisfiable polarity
|
||||
(e.g., expected Theorem but actual Unsatisfiable). These may indicate conjecture-handling
|
||||
differences rather than soundness bugs. If none, write "None detected."]
|
||||
|
||||
---
|
||||
|
||||
<details>
|
||||
<summary>View all Timeouts (problems where Z3 exceeded the 5-second limit)</summary>
|
||||
|
||||
| # | File | Expected Status |
|
||||
|---|------|----------------|
|
||||
[First 100 timeout rows]
|
||||
|
||||
</details>
|
||||
|
||||
<details>
|
||||
<summary>View full per-problem results table</summary>
|
||||
|
||||
| # | File | Expected | Actual | Time (s) | Notes |
|
||||
|---|------|----------|--------|----------|-------|
|
||||
[All rows, or first 500 if over limit]
|
||||
|
||||
</details>
|
||||
|
||||
---
|
||||
|
||||
### Recommendations
|
||||
|
||||
[Based on the findings, list actionable items. E.g.: investigate soundness errors,
|
||||
file crash bugs, note domains where Z3 consistently times out.]
|
||||
```
|
||||
|
||||
Post the discussion using the `create_discussion` safe output. The title should be
|
||||
`[TPTP Benchmark] master — <date>`.
|
||||
|
||||
## Safe Output Guarantee
|
||||
|
||||
You **MUST** call either `create_discussion` or `noop` before the workflow ends:
|
||||
|
||||
- **Full success**: Call `create_discussion` with the complete report.
|
||||
- **Partial results** (some problems ran): Call `create_discussion` with whatever results are available and a note about incomplete execution.
|
||||
- **Download failure**: Call `noop` with the download error details.
|
||||
- **No problems selected**: Call `noop` explaining why no problems were found.
|
||||
- **Binary missing**: If `/tmp/z3-build/z3` is unexpectedly absent, call `noop` with that detail and stop.
|
||||
|
||||
## Important Notes
|
||||
|
||||
- **Build failure handling**: Z3 was built before the agent loaded. If the binary is missing or non-functional, call `noop` with the error and stop.
|
||||
- **TPTP environment variable**: Set `TPTP=/tmp/tptp` when invoking `z3 -tptp` so that `include()` directives in problem files resolve correctly against the downloaded Axioms directory.
|
||||
- **Timeout detection**: Use `timeout 8` as the outer OS-level guard (3 seconds beyond Z3's `-T:5`) to allow Z3 to exit cleanly before the shell kills it. If the exit code from `timeout` is 124, record the verdict as `Timeout`.
|
||||
- **Crash detection**: A crash is a non-zero exit code with no `% SZS status` line in the output and no timeout. Record it separately from `GaveUp`.
|
||||
- **SZS status semantics**: Z3 outputs `Theorem` (not `Unsatisfiable`) when it proves a conjecture; `CounterSatisfiable` (not `Satisfiable`) when it finds a counterexample to a conjecture. A status mismatch between `Theorem` and `Unsatisfiable` for the same problem may be innocuous and depends on whether the problem file uses a conjecture formula.
|
||||
- **Report soundness bugs prominently**: Any case where the polarity of the answer conflicts (expected Theorem/Unsatisfiable but got CounterSatisfiable/Satisfiable, or vice versa) is a potential soundness bug and must be highlighted as critical.
|
||||
- **Keep progress log**: Print a line for every flagged result and every 50th problem so the workflow log shows progress.
|
||||
- **Close older discussions**: Configured via `close-older-discussions: true`. Only the latest weekly report remains open.
|
||||
1706
.github/workflows/zipt-code-reviewer.lock.yml
generated
vendored
1706
.github/workflows/zipt-code-reviewer.lock.yml
generated
vendored
File diff suppressed because one or more lines are too long
261
.github/workflows/zipt-code-reviewer.md
vendored
261
.github/workflows/zipt-code-reviewer.md
vendored
|
|
@ -1,261 +0,0 @@
|
|||
---
|
||||
description: Reviews Z3 string/sequence graph implementation (euf_sgraph, euf_seq_plugin, src/smt/seq) by comparing with the ZIPT reference implementation and reporting improvements as git diffs in GitHub issues
|
||||
|
||||
on:
|
||||
schedule: daily
|
||||
workflow_dispatch:
|
||||
|
||||
permissions: read-all
|
||||
|
||||
network:
|
||||
allowed:
|
||||
- defaults
|
||||
- github
|
||||
|
||||
tools:
|
||||
cache-memory: true
|
||||
github:
|
||||
toolsets: [default]
|
||||
edit: {}
|
||||
web-fetch: {}
|
||||
bash:
|
||||
- "git diff:*"
|
||||
- "git log:*"
|
||||
- "git show:*"
|
||||
- "git status"
|
||||
- "clang-format:*"
|
||||
|
||||
safe-outputs:
|
||||
report-failure-as-issue: false
|
||||
create-issue:
|
||||
title-prefix: "[zipt-review] "
|
||||
labels: [code-quality, automated, string-solver]
|
||||
max: 3
|
||||
missing-tool:
|
||||
create-issue: true
|
||||
noop:
|
||||
report-as-issue: false
|
||||
|
||||
timeout-minutes: 30
|
||||
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
uses: actions/checkout@v6.0.2
|
||||
with:
|
||||
persist-credentials: false
|
||||
|
||||
---
|
||||
|
||||
# ZIPT Code Reviewer
|
||||
|
||||
You are an expert C++ code reviewer specializing in string constraint solvers and the Z3 theorem prover. Your mission is to compare Z3's string/sequence graph implementation with the reference ZIPT implementation, identify concrete code improvements, and present them as git diffs in a GitHub issue.
|
||||
|
||||
## Current Context
|
||||
|
||||
- **Repository**: ${{ github.repository }}
|
||||
- **Workspace**: ${{ github.workspace }}
|
||||
- **ZIPT Reference**: https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT
|
||||
|
||||
## Phase 1: Read Z3 Source Files
|
||||
|
||||
Read each of the following Z3 source files in full:
|
||||
|
||||
### String Graph (euf_sgraph / euf_snode)
|
||||
- `src/ast/euf/euf_snode.h`
|
||||
- `src/ast/euf/euf_sgraph.h`
|
||||
- `src/ast/euf/euf_sgraph.cpp`
|
||||
|
||||
### Sequence Plugin (euf_seq_plugin)
|
||||
- `src/ast/euf/euf_seq_plugin.h`
|
||||
- `src/ast/euf/euf_seq_plugin.cpp`
|
||||
|
||||
### SMT Sequence Theory (src/smt/seq*)
|
||||
Use the glob tool to find all relevant files:
|
||||
```
|
||||
src/smt/seq*.h
|
||||
src/smt/seq*.cpp
|
||||
```
|
||||
Read each matched file.
|
||||
|
||||
## Phase 2: Fetch ZIPT Reference Implementation
|
||||
|
||||
The ZIPT project (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT) is the reference C# implementation that the Z3 string solver is ported from. Fetch the relevant source files to understand the reference algorithms.
|
||||
|
||||
### Step 2.1: Discover ZIPT File Structure
|
||||
|
||||
Fetch the ZIPT repository tree to understand the structure:
|
||||
|
||||
```
|
||||
https://raw.githubusercontent.com/CEisenhofer/ZIPT/parikh/ZIPT/
|
||||
```
|
||||
|
||||
Try fetching these likely ZIPT source directories and files:
|
||||
|
||||
1. Repository root listing: `https://api.github.com/repos/CEisenhofer/ZIPT/git/trees/parikh?recursive=1`
|
||||
2. Key ZIPT source files (fetch the ones you find relevant from the tree):
|
||||
- Look for files related to: string graphs, sequence plugins, Nielsen graph, Parikh constraints, polynomial hashing, substitution caching
|
||||
- The ZIPT project is written in C#; the Z3 implementation is a C++ port
|
||||
|
||||
When fetching files, use the raw content URL pattern:
|
||||
```
|
||||
https://raw.githubusercontent.com/CEisenhofer/ZIPT/parikh/ZIPT/<path>
|
||||
```
|
||||
|
||||
### Step 2.2: Identify Corresponding ZIPT Files
|
||||
|
||||
For each Z3 file you read in Phase 1, identify the ZIPT file(s) that implement the same functionality. Focus on:
|
||||
- String/sequence graph data structures (snode, sgraph equivalents)
|
||||
- Concat associativity propagation
|
||||
- Nullable computation
|
||||
- Kleene star / regex handling
|
||||
- Polynomial hash matrix computation
|
||||
- Substitution caching
|
||||
|
||||
## Phase 3: Analyze and Identify Improvements
|
||||
|
||||
Compare the Z3 C++ implementation against the ZIPT C# reference. For each file pair, look for:
|
||||
|
||||
### 3.1 Algorithmic Improvements
|
||||
- Missing algorithms or edge cases present in ZIPT but absent from Z3
|
||||
- More efficient data structures used in ZIPT
|
||||
- Better asymptotic complexity in ZIPT for key operations
|
||||
- Missing optimizations (e.g., short-circuit evaluations, caching strategies)
|
||||
|
||||
### 3.2 Correctness Issues
|
||||
- Logic discrepancies between Z3 and ZIPT for the same algorithm
|
||||
- Missing null/empty checks present in ZIPT
|
||||
- Incorrect handling of edge cases (empty strings, epsilon, absorbing elements)
|
||||
- Off-by-one errors or boundary condition mistakes
|
||||
|
||||
### 3.3 Code Quality Improvements
|
||||
- Functions in ZIPT that are cleaner or more modular than the Z3 port
|
||||
- Missing early-exit conditions
|
||||
- Redundant computations that ZIPT avoids
|
||||
- Better naming or structure in ZIPT that could improve Z3 readability
|
||||
|
||||
### 3.4 Missing Features
|
||||
- ZIPT functionality not yet ported to Z3
|
||||
- Incomplete ports where only part of the ZIPT logic was transferred
|
||||
|
||||
## Phase 4: Implement Improvements as Code Changes
|
||||
|
||||
For each improvement identified in Phase 3:
|
||||
|
||||
1. **Assess feasibility**: Only implement improvements that are:
|
||||
- Self-contained (don't require large architectural changes)
|
||||
- Verifiable (you can confirm correctness by reading the code)
|
||||
- Safe (don't change public API signatures)
|
||||
|
||||
2. **Apply the change** using the edit tool to modify the Z3 source file
|
||||
|
||||
3. **Track each change**: Note the file, line range, and rationale
|
||||
|
||||
Focus on at most **5 concrete, high-value improvements** per run to keep changes focused and reviewable.
|
||||
|
||||
## Phase 5: Generate Git Diff
|
||||
|
||||
After applying all changes:
|
||||
|
||||
```bash
|
||||
# Check what was modified
|
||||
git status
|
||||
|
||||
# Generate a unified diff of all changes
|
||||
git diff > /tmp/zipt-improvements.diff
|
||||
|
||||
# Read the diff
|
||||
cat /tmp/zipt-improvements.diff
|
||||
```
|
||||
|
||||
If no changes were made because no improvements were found or all were too risky, call the `noop` safe-output tool:
|
||||
|
||||
```
|
||||
noop: "ZIPT code review complete. No concrete improvements found in this run. Files examined: [list files]. ZIPT files compared: [list files]."
|
||||
```
|
||||
|
||||
## Phase 6: Create GitHub Issue
|
||||
|
||||
If improvements were found and changes were applied, create a GitHub issue using the safe-outputs configuration.
|
||||
|
||||
Structure the issue body as follows:
|
||||
|
||||
```markdown
|
||||
## ZIPT Code Review: Improvements from Reference Implementation
|
||||
|
||||
**Date**: [today's date]
|
||||
**Files Reviewed**: [list of Z3 files examined]
|
||||
**ZIPT Reference**: https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT
|
||||
|
||||
### Summary
|
||||
|
||||
[2-3 sentence summary of what was found and changed]
|
||||
|
||||
### Improvements Applied
|
||||
|
||||
For each improvement:
|
||||
|
||||
#### Improvement N: [Short title]
|
||||
|
||||
**File**: `path/to/z3/file.cpp`
|
||||
**Rationale**: [Why this improves the code, with reference to the ZIPT equivalent]
|
||||
**ZIPT Reference**: [URL or file path of the corresponding ZIPT code]
|
||||
|
||||
### Git Diff
|
||||
|
||||
The following diff can be applied with `git apply`:
|
||||
|
||||
```diff
|
||||
[FULL GIT DIFF OUTPUT HERE]
|
||||
```
|
||||
|
||||
To apply:
|
||||
```bash
|
||||
git apply - << 'EOF'
|
||||
[FULL GIT DIFF OUTPUT HERE]
|
||||
EOF
|
||||
```
|
||||
|
||||
### Testing
|
||||
|
||||
After applying this diff, build and test with:
|
||||
```bash
|
||||
mkdir -p build && cd build
|
||||
cmake ..
|
||||
make -j$(nproc)
|
||||
make test-z3
|
||||
./test-z3 euf_sgraph
|
||||
./test-z3 euf_seq_plugin
|
||||
```
|
||||
|
||||
---
|
||||
*Generated by ZIPT Code Reviewer agent — comparing Z3 implementation with CEisenhofer/ZIPT@parikh*
|
||||
```
|
||||
|
||||
## Important: Always Call a Safe Output Tool
|
||||
|
||||
**You MUST always call at least one safe-output tool before finishing.** Failing to do so is reported as a workflow failure.
|
||||
|
||||
- If you found and applied improvements → call `create_issue`
|
||||
- If ZIPT is unreachable, no improvements were found, or all improvements are out of scope → call `noop` with a brief explanation
|
||||
|
||||
### Scope
|
||||
- **Only** examine the files listed in Phase 1
|
||||
- **Only** compare against the ZIPT reference at https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT
|
||||
- Do **not** modify test files
|
||||
- Do **not** change public API signatures
|
||||
|
||||
### Quality Bar
|
||||
- Every change must be demonstrably better than the current code
|
||||
- Cite the specific ZIPT file and function for each improvement
|
||||
- Prefer small, surgical changes over large refactors
|
||||
|
||||
### Exit Conditions
|
||||
Call `noop` (instead of creating an issue) if:
|
||||
- ZIPT repository is unreachable
|
||||
- No concrete, safe improvements can be identified
|
||||
- All identified improvements require architectural changes beyond the scope of a single diff
|
||||
|
||||
Example noop call:
|
||||
```
|
||||
noop: "ZIPT code review complete. No improvements applied: [brief reason, e.g. ZIPT unreachable / no safe changes identified]. Files reviewed: [list]."
|
||||
```
|
||||
Loading…
Add table
Add a link
Reference in a new issue