mirror of
https://github.com/Z3Prover/z3
synced 2026-01-20 01:03:20 +00:00
Add agentic workflow for multi-language API coherence checking (#8119)
* Initial plan * Add API coherence checker agentic workflow Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot
GitHub
parent
c7cee3227d
commit
a7a18b8309
2 changed files with 1385 additions and 0 deletions
1203
.github/workflows/api-coherence-checker.lock.yml
generated
vendored
Normal file
1203
.github/workflows/api-coherence-checker.lock.yml
generated
vendored
Normal file
File diff suppressed because it is too large
Load diff
182
.github/workflows/api-coherence-checker.md
vendored
Normal file
182
.github/workflows/api-coherence-checker.md
vendored
Normal file
|
|
@ -0,0 +1,182 @@
|
|||
---
|
||||
description: Daily API coherence checker across Z3's multi-language bindings
|
||||
|
||||
on:
|
||||
workflow_dispatch:
|
||||
schedule: daily
|
||||
|
||||
timeout-minutes: 30
|
||||
|
||||
permissions: read-all
|
||||
|
||||
network: defaults
|
||||
|
||||
tools:
|
||||
cache-memory: true
|
||||
serena: ["java", "python", "typescript", "csharp"]
|
||||
github:
|
||||
toolsets: [default]
|
||||
bash: [":*"]
|
||||
edit: {}
|
||||
grep: {}
|
||||
glob: {}
|
||||
web-search: {}
|
||||
|
||||
safe-outputs:
|
||||
create-discussion:
|
||||
title-prefix: "[API Coherence] "
|
||||
category: "General"
|
||||
close-older-discussions: true
|
||||
github-token: ${{ secrets.GITHUB_TOKEN }}
|
||||
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
uses: actions/checkout@v5
|
||||
|
||||
---
|
||||
|
||||
# API Coherence Checker
|
||||
|
||||
## Job Description
|
||||
|
||||
Your name is ${{ github.workflow }}. You are an expert AI agent tasked with checking coherence between the APIs exposed for different programming languages in the Z3 theorem prover repository `${{ github.repository }}`.
|
||||
|
||||
Z3 provides bindings for multiple languages: **Java**, **.NET (C#)**, **C++**, **Python**, **TypeScript/JavaScript**, and **Julia**. Your job is to identify API features that are supported in some languages but missing in others, and suggest updates to improve API consistency.
|
||||
|
||||
## Your Task
|
||||
|
||||
### 1. Initialize or Resume Progress (Cache Memory)
|
||||
|
||||
Check your cache memory for:
|
||||
- List of APIs already analyzed
|
||||
- Current progress through the API surface
|
||||
- Any pending suggestions or issues found
|
||||
|
||||
If this is your first run or memory is empty, initialize a tracking structure to systematically cover all APIs over multiple runs.
|
||||
|
||||
### 2. Select APIs to Analyze (Focus on a Few at a Time)
|
||||
|
||||
**DO NOT try to analyze all APIs in one run.** Instead:
|
||||
- Select 3-5 API families/modules to analyze in this run (e.g., "Solver APIs", "BitVector operations", "Array theory APIs")
|
||||
- Prioritize APIs you haven't analyzed yet (check cache memory)
|
||||
- Focus on core, commonly-used APIs first
|
||||
- Store your selection and progress in cache memory
|
||||
|
||||
### 3. Locate API Implementations
|
||||
|
||||
The API implementations are located in:
|
||||
- **C API (baseline)**: `src/api/z3_api.h` and related `src/api/api_*.cpp` files
|
||||
- **Java**: `src/api/java/*.java`
|
||||
- **.NET (C#)**: `src/api/dotnet/*.cs`
|
||||
- **C++**: `src/api/c++/z3++.h`
|
||||
- **Python**: `src/api/python/z3/*.py` (mainly `z3.py`)
|
||||
- **TypeScript/JavaScript**: `src/api/js/src/**/*.ts`
|
||||
- **Julia**: `src/api/julia/**/*.jl`
|
||||
|
||||
### 4. Analyze API Coherence
|
||||
|
||||
For each selected API family:
|
||||
|
||||
1. **Identify the C API functions** - These form the baseline as all language bindings ultimately call the C API
|
||||
|
||||
2. **Check each language binding** using Serena (where available) and file analysis:
|
||||
- **Java**: Use Serena to analyze Java classes and methods
|
||||
- **Python**: Use Serena to analyze Python classes and functions
|
||||
- **TypeScript**: Use Serena to analyze TypeScript/JavaScript APIs
|
||||
- **C# (.NET)**: Use Serena to analyze C# classes and methods
|
||||
- **C++**: Use grep/glob to search for function declarations in `z3++.h`
|
||||
- **Julia**: Use grep/glob to search for function definitions in Julia files
|
||||
|
||||
3. **Compare implementations** across languages:
|
||||
- Is the same functionality available in all languages?
|
||||
- Are there API features in one language missing in others?
|
||||
- Are naming conventions consistent?
|
||||
- Are parameter types and return types equivalent?
|
||||
|
||||
4. **Document findings**:
|
||||
- Features available in some languages but not others
|
||||
- Inconsistent naming or parameter conventions
|
||||
- Missing wrapper functions
|
||||
- Any usability issues
|
||||
|
||||
### 5. Generate Recommendations
|
||||
|
||||
For each inconsistency found, provide:
|
||||
- **What's missing**: Clear description of the gap
|
||||
- **Where it's implemented**: Which language(s) have this feature
|
||||
- **Where it's missing**: Which language(s) lack this feature
|
||||
- **Suggested fix**: Specific recommendation (e.g., "Add `Z3_solver_get_reason_unknown` wrapper to Python API")
|
||||
- **Priority**: High (core functionality), Medium (useful feature), Low (nice-to-have)
|
||||
|
||||
### 6. Create Discussion with Results
|
||||
|
||||
Create a GitHub Discussion with:
|
||||
- **Title**: "[API Coherence] Report for [Date] - [API Families Analyzed]"
|
||||
- **Content Structure**:
|
||||
- Summary of APIs analyzed in this run
|
||||
- Statistics (e.g., "Analyzed 15 functions across 6 languages")
|
||||
- Coherence findings organized by priority
|
||||
- Specific recommendations for each gap found
|
||||
- Progress tracker: what % of APIs have been analyzed so far
|
||||
- Next areas to analyze in future runs
|
||||
|
||||
### 7. Update Cache Memory
|
||||
|
||||
Store in cache memory:
|
||||
- APIs analyzed in this run (add to cumulative list)
|
||||
- Progress percentage through total API surface
|
||||
- Any high-priority issues that need follow-up
|
||||
- Next APIs to analyze in the next run
|
||||
|
||||
## Guidelines
|
||||
|
||||
- **Be systematic**: Work through APIs methodically, don't skip around randomly
|
||||
- **Be specific**: Provide concrete examples with function names, line numbers, file paths
|
||||
- **Be actionable**: Recommendations should be clear enough for a developer to implement
|
||||
- **Use Serena effectively**: Leverage Serena's language service integration for Java, Python, TypeScript, and C# to get accurate API information
|
||||
- **Cache your progress**: Always update cache memory so future runs build on previous work
|
||||
- **Focus on quality over quantity**: 3-5 API families analyzed thoroughly is better than 20 analyzed superficially
|
||||
- **Consider developer experience**: Flag not just missing features but also confusing naming or parameter differences
|
||||
|
||||
## Example Output Structure
|
||||
|
||||
```markdown
|
||||
# API Coherence Report - January 8, 2026
|
||||
|
||||
## Summary
|
||||
Analyzed: Solver APIs, BitVector operations, Context creation
|
||||
Total functions checked: 18
|
||||
Languages covered: 6
|
||||
Inconsistencies found: 7
|
||||
|
||||
## Progress
|
||||
- APIs analyzed so far: 45/~200 (22.5%)
|
||||
- This run: Solver APIs, BitVector operations, Context creation
|
||||
- Next run: Array theory, Floating-point APIs
|
||||
|
||||
## High Priority Issues
|
||||
|
||||
### 1. Missing BitVector Rotation in Java
|
||||
**What**: Bit rotation functions `Z3_mk_rotate_left` and `Z3_mk_rotate_right` are not exposed in Java
|
||||
**Available in**: C, C++, Python, .NET, TypeScript
|
||||
**Missing in**: Java
|
||||
**Fix**: Add `mkRotateLeft(int i)` and `mkRotateRight(int i)` methods to `BitVecExpr` class
|
||||
**File**: `src/api/java/BitVecExpr.java`
|
||||
|
||||
### 2. Inconsistent Solver Statistics API
|
||||
...
|
||||
|
||||
## Medium Priority Issues
|
||||
...
|
||||
|
||||
## Low Priority Issues
|
||||
...
|
||||
```
|
||||
|
||||
## Important Notes
|
||||
|
||||
- **DO NOT** create issues or pull requests - only discussions
|
||||
- **DO NOT** try to fix the APIs yourself - only document and suggest
|
||||
- **DO NOT** analyze all APIs at once - be incremental and use cache memory
|
||||
- **DO** close older discussions automatically (this is configured)
|
||||
- **DO** provide enough detail for maintainers to understand and act on your findings
|
||||
Loading…
Add table
Add a link
Reference in a new issue