z3/.github/workflows/zipt-code-reviewer.md

---
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:
    - cron: "0 0,6,12,18 * * *"
  workflow_dispatch:

permissions: read-all

network:
  allowed:
    - defaults
    - github

tools:
  cache-memory: true
  github:
    toolsets: [default]
  view: {}
  glob: {}
  edit: {}
  web-fetch: {}
  bash:
    - "git diff:*"
    - "git log:*"
    - "git show:*"
    - "git status"
    - "clang-format:*"

safe-outputs:
  create-issue:
    title-prefix: "[zipt-review] "
    labels: [code-quality, automated, string-solver]
    max: 3
  missing-tool:
    create-issue: true

timeout-minutes: 30

steps:
  - name: Checkout repository
    uses: actions/checkout@v5
    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, exit gracefully:

```
✅ 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 Guidelines

### 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
Exit without 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