From 610a3d3c5a7127e5b87018e01a0458f73f438cfe Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 03:22:56 +0000
Subject: [PATCH] Add tactic-to-simplifier comparison agentic workflow
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
.../workflows/tactic-to-simplifier.lock.yml | 1170 +++++++++++++++++
.github/workflows/tactic-to-simplifier.md | 278 ++++
2 files changed, 1448 insertions(+)
create mode 100644 .github/workflows/tactic-to-simplifier.lock.yml
create mode 100644 .github/workflows/tactic-to-simplifier.md
diff --git a/.github/workflows/tactic-to-simplifier.lock.yml b/.github/workflows/tactic-to-simplifier.lock.yml
new file mode 100644
index 000000000..eac8296e2
--- /dev/null
+++ b/.github/workflows/tactic-to-simplifier.lock.yml
@@ -0,0 +1,1170 @@
+#
+# ___ _ _
+# / _ \ | | (_)
+# | |_| | __ _ ___ _ __ | |_ _ ___
+# | _ |/ _` |/ _ \ '_ \| __| |/ __|
+# | | | | (_| | __/ | | | |_| | (__
+# \_| |_/\__, |\___|_| |_|\__|_|\___|
+# __/ |
+# _ _ |___/
+# | | | | / _| |
+# | | | | ___ _ __ _ __| |_| | _____ ____
+# | |/\| |/ _ \ '__| |/ /| _| |/ _ \ \ /\ / / ___|
+# \ /\ / (_) | | | | ( | | | | (_) \ V V /\__ \
+# \/ \/ \___/|_| |_|\_\|_| |_|\___/ \_/\_/ |___/
+#
+# This file was automatically generated by gh-aw (v0.47.6). DO NOT EDIT.
+#
+# To update this file, edit the corresponding .md file and run:
+# gh aw compile
+# Not all edits will cause changes to this file.
+#
+# For more information: https://github.github.com/gh-aw/introduction/overview/
+#
+# Compares exposed tactics and simplifiers in Z3, and creates issues for tactics that can be converted to simplifiers
+#
+# gh-aw-metadata: {"schema_version":"v1","frontmatter_hash":"50116844aa0308890a39445e2e30a0cc857b66711c75cecd175c4e064608b1aa","compiler_version":"v0.47.6"}
+
+name: "Tactic-to-Simplifier Comparison Agent"
+"on":
+ schedule:
+ - cron: "28 4 * * 6"
+ # Friendly format: weekly (scattered)
+ workflow_dispatch:
+
+permissions: {}
+
+concurrency:
+ group: "gh-aw-${{ github.workflow }}"
+
+run-name: "Tactic-to-Simplifier Comparison Agent"
+
+jobs:
+ activation:
+ runs-on: ubuntu-slim
+ permissions:
+ contents: read
+ outputs:
+ comment_id: ""
+ comment_repo: ""
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Validate context variables
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/validate_context_variables.cjs');
+ await main();
+ - name: Checkout .github and .agents folders
+ uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+ with:
+ sparse-checkout: |
+ .github
+ .agents
+ fetch-depth: 1
+ persist-credentials: false
+ - name: Check workflow file timestamps
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_WORKFLOW_FILE: "tactic-to-simplifier.lock.yml"
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/check_workflow_timestamp_api.cjs');
+ await main();
+ - name: Create prompt with built-in context
+ env:
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ GH_AW_SAFE_OUTPUTS: ${{ env.GH_AW_SAFE_OUTPUTS }}
+ GH_AW_GITHUB_ACTOR: ${{ github.actor }}
+ GH_AW_GITHUB_EVENT_COMMENT_ID: ${{ github.event.comment.id }}
+ GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER: ${{ github.event.discussion.number }}
+ GH_AW_GITHUB_EVENT_ISSUE_NUMBER: ${{ github.event.issue.number }}
+ GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER: ${{ github.event.pull_request.number }}
+ GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
+ GH_AW_GITHUB_RUN_ID: ${{ github.run_id }}
+ GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
+ run: |
+ bash /opt/gh-aw/actions/create_prompt_first.sh
+ cat << 'GH_AW_PROMPT_EOF' > "$GH_AW_PROMPT"
+
+ GH_AW_PROMPT_EOF
+ cat "/opt/gh-aw/prompts/xpia.md" >> "$GH_AW_PROMPT"
+ cat "/opt/gh-aw/prompts/temp_folder_prompt.md" >> "$GH_AW_PROMPT"
+ cat "/opt/gh-aw/prompts/markdown.md" >> "$GH_AW_PROMPT"
+ cat "/opt/gh-aw/prompts/cache_memory_prompt.md" >> "$GH_AW_PROMPT"
+ cat << 'GH_AW_PROMPT_EOF' >> "$GH_AW_PROMPT"
+
+ GitHub API Access Instructions
+
+ The gh CLI is NOT authenticated. Do NOT use gh commands for GitHub operations.
+
+
+ To create or modify GitHub resources (issues, discussions, pull requests, etc.), you MUST call the appropriate safe output tool. Simply writing content will NOT work - the workflow requires actual tool calls.
+
+ Temporary IDs: Some safe output tools support a temporary ID field (usually named temporary_id) so you can reference newly-created items elsewhere in the SAME agent output (for example, using #aw_abc1 in a later body).
+
+ **IMPORTANT - temporary_id format rules:**
+ - If you DON'T need to reference the item later, OMIT the temporary_id field entirely (it will be auto-generated if needed)
+ - If you DO need cross-references/chaining, you MUST match this EXACT validation regex: /^aw_[A-Za-z0-9]{3,8}$/i
+ - Format: aw_ prefix followed by 3 to 8 alphanumeric characters (A-Z, a-z, 0-9, case-insensitive)
+ - Valid alphanumeric characters: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789
+ - INVALID examples: aw_ab (too short), aw_123456789 (too long), aw_test-id (contains hyphen), aw_id_123 (contains underscore)
+ - VALID examples: aw_abc, aw_abc1, aw_Test123, aw_A1B2C3D4, aw_12345678
+ - To generate valid IDs: use 3-8 random alphanumeric characters or omit the field to let the system auto-generate
+
+ Do NOT invent other aw_* formats — downstream steps will reject them with validation errors matching against /^aw_[A-Za-z0-9]{3,8}$/i.
+
+ Discover available tools from the safeoutputs MCP server.
+
+ **Critical**: Tool calls write structured data that downstream jobs process. Without tool calls, follow-up actions will be skipped.
+
+ **Note**: If you made no other safe output tool calls during this workflow execution, call the "noop" tool to provide a status message indicating completion or that no actions were needed.
+
+ ---
+
+ ## Creating an Issue, Reporting Missing Tools or Functionality, Reporting Missing Data
+
+ **IMPORTANT**: To perform the actions listed above, use the **safeoutputs** tools. Do NOT use `gh`, do NOT call the GitHub API directly. You do not have write access to the GitHub repository.
+
+ **Creating an Issue**
+
+ To create an issue, use the create_issue tool from safeoutputs.
+
+ **Reporting Missing Tools or Functionality**
+
+ To report a missing tool or capability, use the missing_tool tool from safeoutputs.
+
+ **Reporting Missing Data**
+
+ To report missing data required to achieve a goal, use the missing_data tool from safeoutputs.
+
+
+
+
+ The following GitHub context information is available for this workflow:
+ {{#if __GH_AW_GITHUB_ACTOR__ }}
+ - **actor**: __GH_AW_GITHUB_ACTOR__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_REPOSITORY__ }}
+ - **repository**: __GH_AW_GITHUB_REPOSITORY__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_WORKSPACE__ }}
+ - **workspace**: __GH_AW_GITHUB_WORKSPACE__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_EVENT_ISSUE_NUMBER__ }}
+ - **issue-number**: #__GH_AW_GITHUB_EVENT_ISSUE_NUMBER__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER__ }}
+ - **discussion-number**: #__GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER__ }}
+ - **pull-request-number**: #__GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_EVENT_COMMENT_ID__ }}
+ - **comment-id**: __GH_AW_GITHUB_EVENT_COMMENT_ID__
+ {{/if}}
+ {{#if __GH_AW_GITHUB_RUN_ID__ }}
+ - **workflow-run-id**: __GH_AW_GITHUB_RUN_ID__
+ {{/if}}
+
+
+ GH_AW_PROMPT_EOF
+ cat << 'GH_AW_PROMPT_EOF' >> "$GH_AW_PROMPT"
+
+ GH_AW_PROMPT_EOF
+ cat << 'GH_AW_PROMPT_EOF' >> "$GH_AW_PROMPT"
+ {{#runtime-import .github/workflows/tactic-to-simplifier.md}}
+ GH_AW_PROMPT_EOF
+ - name: Interpolate variables and render templates
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/interpolate_prompt.cjs');
+ await main();
+ - name: Substitute placeholders
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ GH_AW_ALLOWED_EXTENSIONS: ''
+ GH_AW_CACHE_DESCRIPTION: ''
+ GH_AW_CACHE_DIR: '/tmp/gh-aw/cache-memory/'
+ GH_AW_GITHUB_ACTOR: ${{ github.actor }}
+ GH_AW_GITHUB_EVENT_COMMENT_ID: ${{ github.event.comment.id }}
+ GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER: ${{ github.event.discussion.number }}
+ GH_AW_GITHUB_EVENT_ISSUE_NUMBER: ${{ github.event.issue.number }}
+ GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER: ${{ github.event.pull_request.number }}
+ GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
+ GH_AW_GITHUB_RUN_ID: ${{ github.run_id }}
+ GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
+ GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED: ${{ needs.pre_activation.outputs.activated }}
+ GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_MATCHED_COMMAND: ${{ needs.pre_activation.outputs.matched_command }}
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+
+ const substitutePlaceholders = require('/opt/gh-aw/actions/substitute_placeholders.cjs');
+
+ // Call the substitution function
+ return await substitutePlaceholders({
+ file: process.env.GH_AW_PROMPT,
+ substitutions: {
+ GH_AW_ALLOWED_EXTENSIONS: process.env.GH_AW_ALLOWED_EXTENSIONS,
+ GH_AW_CACHE_DESCRIPTION: process.env.GH_AW_CACHE_DESCRIPTION,
+ GH_AW_CACHE_DIR: process.env.GH_AW_CACHE_DIR,
+ GH_AW_GITHUB_ACTOR: process.env.GH_AW_GITHUB_ACTOR,
+ GH_AW_GITHUB_EVENT_COMMENT_ID: process.env.GH_AW_GITHUB_EVENT_COMMENT_ID,
+ GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER: process.env.GH_AW_GITHUB_EVENT_DISCUSSION_NUMBER,
+ GH_AW_GITHUB_EVENT_ISSUE_NUMBER: process.env.GH_AW_GITHUB_EVENT_ISSUE_NUMBER,
+ GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER: process.env.GH_AW_GITHUB_EVENT_PULL_REQUEST_NUMBER,
+ GH_AW_GITHUB_REPOSITORY: process.env.GH_AW_GITHUB_REPOSITORY,
+ GH_AW_GITHUB_RUN_ID: process.env.GH_AW_GITHUB_RUN_ID,
+ GH_AW_GITHUB_WORKSPACE: process.env.GH_AW_GITHUB_WORKSPACE,
+ GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED: process.env.GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED,
+ GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_MATCHED_COMMAND: process.env.GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_MATCHED_COMMAND
+ }
+ });
+ - name: Validate prompt placeholders
+ env:
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ run: bash /opt/gh-aw/actions/validate_prompt_placeholders.sh
+ - name: Print prompt
+ env:
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ run: bash /opt/gh-aw/actions/print_prompt_summary.sh
+ - name: Upload prompt artifact
+ if: success()
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: prompt
+ path: /tmp/gh-aw/aw-prompts/prompt.txt
+ retention-days: 1
+
+ agent:
+ needs: activation
+ runs-on: ubuntu-latest
+ permissions:
+ contents: read
+ issues: read
+ pull-requests: read
+ concurrency:
+ group: "gh-aw-copilot-${{ github.workflow }}"
+ env:
+ DEFAULT_BRANCH: ${{ github.event.repository.default_branch }}
+ GH_AW_ASSETS_ALLOWED_EXTS: ""
+ GH_AW_ASSETS_BRANCH: ""
+ GH_AW_ASSETS_MAX_SIZE_KB: 0
+ GH_AW_MCP_LOG_DIR: /tmp/gh-aw/mcp-logs/safeoutputs
+ GH_AW_SAFE_OUTPUTS: /opt/gh-aw/safeoutputs/outputs.jsonl
+ GH_AW_SAFE_OUTPUTS_CONFIG_PATH: /opt/gh-aw/safeoutputs/config.json
+ GH_AW_SAFE_OUTPUTS_TOOLS_PATH: /opt/gh-aw/safeoutputs/tools.json
+ GH_AW_WORKFLOW_ID_SANITIZED: tactictosimplifier
+ outputs:
+ checkout_pr_success: ${{ steps.checkout-pr.outputs.checkout_pr_success || 'true' }}
+ has_patch: ${{ steps.collect_output.outputs.has_patch }}
+ model: ${{ steps.generate_aw_info.outputs.model }}
+ output: ${{ steps.collect_output.outputs.output }}
+ output_types: ${{ steps.collect_output.outputs.output_types }}
+ secret_verification_result: ${{ steps.validate-secret.outputs.verification_result }}
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Create gh-aw temp directory
+ run: bash /opt/gh-aw/actions/create_gh_aw_tmp_dir.sh
+ - name: Checkout repository
+ uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+ with:
+ persist-credentials: false
+
+ # Cache memory file share configuration from frontmatter processed below
+ - name: Create cache-memory directory
+ run: bash /opt/gh-aw/actions/create_cache_memory_dir.sh
+ - name: Restore cache-memory file share data
+ uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+ with:
+ key: memory-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
+ path: /tmp/gh-aw/cache-memory
+ restore-keys: |
+ memory-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-
+ - name: Configure Git credentials
+ env:
+ REPO_NAME: ${{ github.repository }}
+ SERVER_URL: ${{ github.server_url }}
+ run: |
+ git config --global user.email "github-actions[bot]@users.noreply.github.com"
+ git config --global user.name "github-actions[bot]"
+ # Re-authenticate git with GitHub token
+ SERVER_URL_STRIPPED="${SERVER_URL#https://}"
+ git remote set-url origin "https://x-access-token:${{ github.token }}@${SERVER_URL_STRIPPED}/${REPO_NAME}.git"
+ echo "Git configured with standard GitHub Actions identity"
+ - name: Checkout PR branch
+ id: checkout-pr
+ if: |
+ github.event.pull_request
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/checkout_pr_branch.cjs');
+ await main();
+ - name: Generate agentic run info
+ id: generate_aw_info
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const fs = require('fs');
+
+ const awInfo = {
+ engine_id: "copilot",
+ engine_name: "GitHub Copilot CLI",
+ model: process.env.GH_AW_MODEL_AGENT_COPILOT || "",
+ version: "",
+ agent_version: "0.0.412",
+ cli_version: "v0.47.6",
+ workflow_name: "Tactic-to-Simplifier Comparison Agent",
+ experimental: false,
+ supports_tools_allowlist: true,
+ run_id: context.runId,
+ run_number: context.runNumber,
+ run_attempt: process.env.GITHUB_RUN_ATTEMPT,
+ repository: context.repo.owner + '/' + context.repo.repo,
+ ref: context.ref,
+ sha: context.sha,
+ actor: context.actor,
+ event_name: context.eventName,
+ staged: false,
+ allowed_domains: ["defaults"],
+ firewall_enabled: true,
+ awf_version: "v0.20.2",
+ awmg_version: "v0.1.4",
+ steps: {
+ firewall: "squid"
+ },
+ created_at: new Date().toISOString()
+ };
+
+ // Write to /tmp/gh-aw directory to avoid inclusion in PR
+ const tmpPath = '/tmp/gh-aw/aw_info.json';
+ fs.writeFileSync(tmpPath, JSON.stringify(awInfo, null, 2));
+ console.log('Generated aw_info.json at:', tmpPath);
+ console.log(JSON.stringify(awInfo, null, 2));
+
+ // Set model as output for reuse in other steps/jobs
+ core.setOutput('model', awInfo.model);
+ - name: Validate COPILOT_GITHUB_TOKEN secret
+ id: validate-secret
+ run: /opt/gh-aw/actions/validate_multi_secret.sh COPILOT_GITHUB_TOKEN 'GitHub Copilot CLI' https://github.github.com/gh-aw/reference/engines/#github-copilot-default
+ env:
+ COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+ - name: Install GitHub Copilot CLI
+ run: /opt/gh-aw/actions/install_copilot_cli.sh 0.0.412
+ - name: Install awf binary
+ run: bash /opt/gh-aw/actions/install_awf_binary.sh v0.20.2
+ - name: Determine automatic lockdown mode for GitHub MCP Server
+ id: determine-automatic-lockdown
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }}
+ GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }}
+ with:
+ script: |
+ const determineAutomaticLockdown = require('/opt/gh-aw/actions/determine_automatic_lockdown.cjs');
+ await determineAutomaticLockdown(github, context, core);
+ - name: Download container images
+ run: bash /opt/gh-aw/actions/download_docker_images.sh ghcr.io/github/gh-aw-firewall/agent:0.20.2 ghcr.io/github/gh-aw-firewall/api-proxy:0.20.2 ghcr.io/github/gh-aw-firewall/squid:0.20.2 ghcr.io/github/gh-aw-mcpg:v0.1.4 ghcr.io/github/github-mcp-server:v0.31.0 node:lts-alpine
+ - name: Write Safe Outputs Config
+ run: |
+ mkdir -p /opt/gh-aw/safeoutputs
+ mkdir -p /tmp/gh-aw/safeoutputs
+ mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs
+ cat > /opt/gh-aw/safeoutputs/config.json << 'GH_AW_SAFE_OUTPUTS_CONFIG_EOF'
+ {"create_issue":{"max":3},"missing_data":{},"missing_tool":{},"noop":{"max":1}}
+ GH_AW_SAFE_OUTPUTS_CONFIG_EOF
+ cat > /opt/gh-aw/safeoutputs/tools.json << 'GH_AW_SAFE_OUTPUTS_TOOLS_EOF'
+ [
+ {
+ "description": "Create a new GitHub issue for tracking bugs, feature requests, or tasks. Use this for actionable work items that need assignment, labeling, and status tracking. For reports, announcements, or status updates that don't require task tracking, use create_discussion instead. CONSTRAINTS: Maximum 3 issue(s) can be created. Title will be prefixed with \"[tactic-to-simplifier] \". Labels [enhancement refactoring tactic-to-simplifier] will be automatically added.",
+ "inputSchema": {
+ "additionalProperties": false,
+ "properties": {
+ "body": {
+ "description": "Detailed issue description in Markdown. Do NOT repeat the title as a heading since it already appears as the issue's h1. Include context, reproduction steps, or acceptance criteria as appropriate.",
+ "type": "string"
+ },
+ "labels": {
+ "description": "Labels to categorize the issue (e.g., 'bug', 'enhancement'). Labels must exist in the repository.",
+ "items": {
+ "type": "string"
+ },
+ "type": "array"
+ },
+ "parent": {
+ "description": "Parent issue number for creating sub-issues. This is the numeric ID from the GitHub URL (e.g., 42 in github.com/owner/repo/issues/42). Can also be a temporary_id (e.g., 'aw_abc123', 'aw_Test123') from a previously created issue in the same workflow run.",
+ "type": [
+ "number",
+ "string"
+ ]
+ },
+ "temporary_id": {
+ "description": "Unique temporary identifier for referencing this issue before it's created. Format: 'aw_' followed by 3 to 8 alphanumeric characters (e.g., 'aw_abc1', 'aw_Test123'). Use '#aw_ID' in body text to reference other issues by their temporary_id; these are replaced with actual issue numbers after creation.",
+ "pattern": "^aw_[A-Za-z0-9]{3,8}$",
+ "type": "string"
+ },
+ "title": {
+ "description": "Concise issue title summarizing the bug, feature, or task. The title appears as the main heading, so keep it brief and descriptive.",
+ "type": "string"
+ }
+ },
+ "required": [
+ "title",
+ "body"
+ ],
+ "type": "object"
+ },
+ "name": "create_issue"
+ },
+ {
+ "description": "Report that a tool or capability needed to complete the task is not available, or share any information you deem important about missing functionality or limitations. Use this when you cannot accomplish what was requested because the required functionality is missing or access is restricted.",
+ "inputSchema": {
+ "additionalProperties": false,
+ "properties": {
+ "alternatives": {
+ "description": "Any workarounds, manual steps, or alternative approaches the user could take (max 256 characters).",
+ "type": "string"
+ },
+ "reason": {
+ "description": "Explanation of why this tool is needed or what information you want to share about the limitation (max 256 characters).",
+ "type": "string"
+ },
+ "tool": {
+ "description": "Optional: Name or description of the missing tool or capability (max 128 characters). Be specific about what functionality is needed.",
+ "type": "string"
+ }
+ },
+ "required": [
+ "reason"
+ ],
+ "type": "object"
+ },
+ "name": "missing_tool"
+ },
+ {
+ "description": "Log a transparency message when no significant actions are needed. Use this to confirm workflow completion and provide visibility when analysis is complete but no changes or outputs are required (e.g., 'No issues found', 'All checks passed'). This ensures the workflow produces human-visible output even when no other actions are taken.",
+ "inputSchema": {
+ "additionalProperties": false,
+ "properties": {
+ "message": {
+ "description": "Status or completion message to log. Should explain what was analyzed and the outcome (e.g., 'Code review complete - no issues found', 'Analysis complete - all tests passing').",
+ "type": "string"
+ }
+ },
+ "required": [
+ "message"
+ ],
+ "type": "object"
+ },
+ "name": "noop"
+ },
+ {
+ "description": "Report that data or information needed to complete the task is not available. Use this when you cannot accomplish what was requested because required data, context, or information is missing.",
+ "inputSchema": {
+ "additionalProperties": false,
+ "properties": {
+ "alternatives": {
+ "description": "Any workarounds, manual steps, or alternative approaches the user could take (max 256 characters).",
+ "type": "string"
+ },
+ "context": {
+ "description": "Additional context about the missing data or where it should come from (max 256 characters).",
+ "type": "string"
+ },
+ "data_type": {
+ "description": "Type or description of the missing data or information (max 128 characters). Be specific about what data is needed.",
+ "type": "string"
+ },
+ "reason": {
+ "description": "Explanation of why this data is needed to complete the task (max 256 characters).",
+ "type": "string"
+ }
+ },
+ "required": [],
+ "type": "object"
+ },
+ "name": "missing_data"
+ }
+ ]
+ GH_AW_SAFE_OUTPUTS_TOOLS_EOF
+ cat > /opt/gh-aw/safeoutputs/validation.json << 'GH_AW_SAFE_OUTPUTS_VALIDATION_EOF'
+ {
+ "create_issue": {
+ "defaultMax": 1,
+ "fields": {
+ "body": {
+ "required": true,
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 65000
+ },
+ "labels": {
+ "type": "array",
+ "itemType": "string",
+ "itemSanitize": true,
+ "itemMaxLength": 128
+ },
+ "parent": {
+ "issueOrPRNumber": true
+ },
+ "repo": {
+ "type": "string",
+ "maxLength": 256
+ },
+ "temporary_id": {
+ "type": "string"
+ },
+ "title": {
+ "required": true,
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 128
+ }
+ }
+ },
+ "missing_data": {
+ "defaultMax": 20,
+ "fields": {
+ "alternatives": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 256
+ },
+ "context": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 256
+ },
+ "data_type": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 128
+ },
+ "reason": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 256
+ }
+ }
+ },
+ "missing_tool": {
+ "defaultMax": 20,
+ "fields": {
+ "alternatives": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 512
+ },
+ "reason": {
+ "required": true,
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 256
+ },
+ "tool": {
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 128
+ }
+ }
+ },
+ "noop": {
+ "defaultMax": 1,
+ "fields": {
+ "message": {
+ "required": true,
+ "type": "string",
+ "sanitize": true,
+ "maxLength": 65000
+ }
+ }
+ }
+ }
+ GH_AW_SAFE_OUTPUTS_VALIDATION_EOF
+ - name: Generate Safe Outputs MCP Server Config
+ id: safe-outputs-config
+ run: |
+ # Generate a secure random API key (360 bits of entropy, 40+ chars)
+ # Mask immediately to prevent timing vulnerabilities
+ API_KEY=$(openssl rand -base64 45 | tr -d '/+=')
+ echo "::add-mask::${API_KEY}"
+
+ PORT=3001
+
+ # Set outputs for next steps
+ {
+ echo "safe_outputs_api_key=${API_KEY}"
+ echo "safe_outputs_port=${PORT}"
+ } >> "$GITHUB_OUTPUT"
+
+ echo "Safe Outputs MCP server will run on port ${PORT}"
+
+ - name: Start Safe Outputs MCP HTTP Server
+ id: safe-outputs-start
+ env:
+ DEBUG: '*'
+ GH_AW_SAFE_OUTPUTS_PORT: ${{ steps.safe-outputs-config.outputs.safe_outputs_port }}
+ GH_AW_SAFE_OUTPUTS_API_KEY: ${{ steps.safe-outputs-config.outputs.safe_outputs_api_key }}
+ GH_AW_SAFE_OUTPUTS_TOOLS_PATH: /opt/gh-aw/safeoutputs/tools.json
+ GH_AW_SAFE_OUTPUTS_CONFIG_PATH: /opt/gh-aw/safeoutputs/config.json
+ GH_AW_MCP_LOG_DIR: /tmp/gh-aw/mcp-logs/safeoutputs
+ run: |
+ # Environment variables are set above to prevent template injection
+ export DEBUG
+ export GH_AW_SAFE_OUTPUTS_PORT
+ export GH_AW_SAFE_OUTPUTS_API_KEY
+ export GH_AW_SAFE_OUTPUTS_TOOLS_PATH
+ export GH_AW_SAFE_OUTPUTS_CONFIG_PATH
+ export GH_AW_MCP_LOG_DIR
+
+ bash /opt/gh-aw/actions/start_safe_outputs_server.sh
+
+ - name: Start MCP Gateway
+ id: start-mcp-gateway
+ env:
+ GH_AW_SAFE_OUTPUTS: ${{ env.GH_AW_SAFE_OUTPUTS }}
+ GH_AW_SAFE_OUTPUTS_API_KEY: ${{ steps.safe-outputs-start.outputs.api_key }}
+ GH_AW_SAFE_OUTPUTS_PORT: ${{ steps.safe-outputs-start.outputs.port }}
+ GITHUB_MCP_LOCKDOWN: ${{ steps.determine-automatic-lockdown.outputs.lockdown == 'true' && '1' || '0' }}
+ GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
+ run: |
+ set -eo pipefail
+ mkdir -p /tmp/gh-aw/mcp-config
+
+ # Export gateway environment variables for MCP config and gateway script
+ export MCP_GATEWAY_PORT="80"
+ export MCP_GATEWAY_DOMAIN="host.docker.internal"
+ MCP_GATEWAY_API_KEY=$(openssl rand -base64 45 | tr -d '/+=')
+ echo "::add-mask::${MCP_GATEWAY_API_KEY}"
+ export MCP_GATEWAY_API_KEY
+ export MCP_GATEWAY_PAYLOAD_DIR="/tmp/gh-aw/mcp-payloads"
+ mkdir -p "${MCP_GATEWAY_PAYLOAD_DIR}"
+ export DEBUG="*"
+
+ export GH_AW_ENGINE="copilot"
+ export MCP_GATEWAY_DOCKER_COMMAND='docker run -i --rm --network host -v /var/run/docker.sock:/var/run/docker.sock -e MCP_GATEWAY_PORT -e MCP_GATEWAY_DOMAIN -e MCP_GATEWAY_API_KEY -e MCP_GATEWAY_PAYLOAD_DIR -e DEBUG -e MCP_GATEWAY_LOG_DIR -e GH_AW_MCP_LOG_DIR -e GH_AW_SAFE_OUTPUTS -e GH_AW_SAFE_OUTPUTS_CONFIG_PATH -e GH_AW_SAFE_OUTPUTS_TOOLS_PATH -e GH_AW_ASSETS_BRANCH -e GH_AW_ASSETS_MAX_SIZE_KB -e GH_AW_ASSETS_ALLOWED_EXTS -e DEFAULT_BRANCH -e GITHUB_MCP_SERVER_TOKEN -e GITHUB_MCP_LOCKDOWN -e GITHUB_REPOSITORY -e GITHUB_SERVER_URL -e GITHUB_SHA -e GITHUB_WORKSPACE -e GITHUB_TOKEN -e GITHUB_RUN_ID -e GITHUB_RUN_NUMBER -e GITHUB_RUN_ATTEMPT -e GITHUB_JOB -e GITHUB_ACTION -e GITHUB_EVENT_NAME -e GITHUB_EVENT_PATH -e GITHUB_ACTOR -e GITHUB_ACTOR_ID -e GITHUB_TRIGGERING_ACTOR -e GITHUB_WORKFLOW -e GITHUB_WORKFLOW_REF -e GITHUB_WORKFLOW_SHA -e GITHUB_REF -e GITHUB_REF_NAME -e GITHUB_REF_TYPE -e GITHUB_HEAD_REF -e GITHUB_BASE_REF -e GH_AW_SAFE_OUTPUTS_PORT -e GH_AW_SAFE_OUTPUTS_API_KEY -v /tmp/gh-aw/mcp-payloads:/tmp/gh-aw/mcp-payloads:rw -v /opt:/opt:ro -v /tmp:/tmp:rw -v '"${GITHUB_WORKSPACE}"':'"${GITHUB_WORKSPACE}"':rw ghcr.io/github/gh-aw-mcpg:v0.1.4'
+
+ mkdir -p /home/runner/.copilot
+ cat << GH_AW_MCP_CONFIG_EOF | bash /opt/gh-aw/actions/start_mcp_gateway.sh
+ {
+ "mcpServers": {
+ "github": {
+ "type": "stdio",
+ "container": "ghcr.io/github/github-mcp-server:v0.31.0",
+ "env": {
+ "GITHUB_LOCKDOWN_MODE": "$GITHUB_MCP_LOCKDOWN",
+ "GITHUB_PERSONAL_ACCESS_TOKEN": "\${GITHUB_MCP_SERVER_TOKEN}",
+ "GITHUB_READ_ONLY": "1",
+ "GITHUB_TOOLSETS": "context,repos,issues,pull_requests"
+ }
+ },
+ "safeoutputs": {
+ "type": "http",
+ "url": "http://host.docker.internal:$GH_AW_SAFE_OUTPUTS_PORT",
+ "headers": {
+ "Authorization": "\${GH_AW_SAFE_OUTPUTS_API_KEY}"
+ }
+ }
+ },
+ "gateway": {
+ "port": $MCP_GATEWAY_PORT,
+ "domain": "${MCP_GATEWAY_DOMAIN}",
+ "apiKey": "${MCP_GATEWAY_API_KEY}",
+ "payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}"
+ }
+ }
+ GH_AW_MCP_CONFIG_EOF
+ - name: Generate workflow overview
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const { generateWorkflowOverview } = require('/opt/gh-aw/actions/generate_workflow_overview.cjs');
+ await generateWorkflowOverview(core);
+ - name: Download prompt artifact
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ with:
+ name: prompt
+ path: /tmp/gh-aw/aw-prompts
+ - name: Clean git credentials
+ run: bash /opt/gh-aw/actions/clean_git_credentials.sh
+ - name: Execute GitHub Copilot CLI
+ id: agentic_execution
+ # Copilot CLI tool arguments (sorted):
+ timeout-minutes: 30
+ run: |
+ set -o pipefail
+ sudo -E awf --env-all --container-workdir "${GITHUB_WORKSPACE}" --allow-domains api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com --log-level info --proxy-logs-dir /tmp/gh-aw/sandbox/firewall/logs --enable-host-access --image-tag 0.20.2 --skip-pull --enable-api-proxy \
+ -- /bin/bash -c '/usr/local/bin/copilot --add-dir /tmp/gh-aw/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --add-dir "${GITHUB_WORKSPACE}" --disable-builtin-mcps --allow-all-tools --add-dir /tmp/gh-aw/cache-memory/ --allow-all-paths --prompt "$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"${GH_AW_MODEL_AGENT_COPILOT:+ --model "$GH_AW_MODEL_AGENT_COPILOT"}' 2>&1 | tee -a /tmp/gh-aw/agent-stdio.log
+ env:
+ COPILOT_AGENT_RUNNER_TYPE: STANDALONE
+ COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+ GH_AW_MCP_CONFIG: /home/runner/.copilot/mcp-config.json
+ GH_AW_MODEL_AGENT_COPILOT: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || '' }}
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ GH_AW_SAFE_OUTPUTS: ${{ env.GH_AW_SAFE_OUTPUTS }}
+ GITHUB_HEAD_REF: ${{ github.head_ref }}
+ GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
+ GITHUB_REF_NAME: ${{ github.ref_name }}
+ GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
+ GITHUB_WORKSPACE: ${{ github.workspace }}
+ XDG_CONFIG_HOME: /home/runner
+ - name: Configure Git credentials
+ env:
+ REPO_NAME: ${{ github.repository }}
+ SERVER_URL: ${{ github.server_url }}
+ run: |
+ git config --global user.email "github-actions[bot]@users.noreply.github.com"
+ git config --global user.name "github-actions[bot]"
+ # Re-authenticate git with GitHub token
+ SERVER_URL_STRIPPED="${SERVER_URL#https://}"
+ git remote set-url origin "https://x-access-token:${{ github.token }}@${SERVER_URL_STRIPPED}/${REPO_NAME}.git"
+ echo "Git configured with standard GitHub Actions identity"
+ - name: Copy Copilot session state files to logs
+ if: always()
+ continue-on-error: true
+ run: |
+ # Copy Copilot session state files to logs folder for artifact collection
+ # This ensures they are in /tmp/gh-aw/ where secret redaction can scan them
+ SESSION_STATE_DIR="$HOME/.copilot/session-state"
+ LOGS_DIR="/tmp/gh-aw/sandbox/agent/logs"
+
+ if [ -d "$SESSION_STATE_DIR" ]; then
+ echo "Copying Copilot session state files from $SESSION_STATE_DIR to $LOGS_DIR"
+ mkdir -p "$LOGS_DIR"
+ cp -v "$SESSION_STATE_DIR"/*.jsonl "$LOGS_DIR/" 2>/dev/null || true
+ echo "Session state files copied successfully"
+ else
+ echo "No session-state directory found at $SESSION_STATE_DIR"
+ fi
+ - name: Stop MCP Gateway
+ if: always()
+ continue-on-error: true
+ env:
+ MCP_GATEWAY_PORT: ${{ steps.start-mcp-gateway.outputs.gateway-port }}
+ MCP_GATEWAY_API_KEY: ${{ steps.start-mcp-gateway.outputs.gateway-api-key }}
+ GATEWAY_PID: ${{ steps.start-mcp-gateway.outputs.gateway-pid }}
+ run: |
+ bash /opt/gh-aw/actions/stop_mcp_gateway.sh "$GATEWAY_PID"
+ - name: Redact secrets in logs
+ if: always()
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/redact_secrets.cjs');
+ await main();
+ env:
+ GH_AW_SECRET_NAMES: 'COPILOT_GITHUB_TOKEN,GH_AW_GITHUB_MCP_SERVER_TOKEN,GH_AW_GITHUB_TOKEN,GITHUB_TOKEN'
+ SECRET_COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+ SECRET_GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }}
+ SECRET_GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }}
+ SECRET_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+ - name: Upload Safe Outputs
+ if: always()
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: safe-output
+ path: ${{ env.GH_AW_SAFE_OUTPUTS }}
+ if-no-files-found: warn
+ - name: Ingest agent output
+ id: collect_output
+ if: always()
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_SAFE_OUTPUTS: ${{ env.GH_AW_SAFE_OUTPUTS }}
+ GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com"
+ GITHUB_SERVER_URL: ${{ github.server_url }}
+ GITHUB_API_URL: ${{ github.api_url }}
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/collect_ndjson_output.cjs');
+ await main();
+ - name: Upload sanitized agent output
+ if: always() && env.GH_AW_AGENT_OUTPUT
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: agent-output
+ path: ${{ env.GH_AW_AGENT_OUTPUT }}
+ if-no-files-found: warn
+ - name: Upload engine output files
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: agent_outputs
+ path: |
+ /tmp/gh-aw/sandbox/agent/logs/
+ /tmp/gh-aw/redacted-urls.log
+ if-no-files-found: ignore
+ - name: Parse agent logs for step summary
+ if: always()
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: /tmp/gh-aw/sandbox/agent/logs/
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/parse_copilot_log.cjs');
+ await main();
+ - name: Parse MCP Gateway logs for step summary
+ if: always()
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/parse_mcp_gateway_log.cjs');
+ await main();
+ - name: Print firewall logs
+ if: always()
+ continue-on-error: true
+ env:
+ AWF_LOGS_DIR: /tmp/gh-aw/sandbox/firewall/logs
+ run: |
+ # Fix permissions on firewall logs so they can be uploaded as artifacts
+ # AWF runs with sudo, creating files owned by root
+ sudo chmod -R a+r /tmp/gh-aw/sandbox/firewall/logs 2>/dev/null || true
+ # Only run awf logs summary if awf command exists (it may not be installed if workflow failed before install step)
+ if command -v awf &> /dev/null; then
+ awf logs summary | tee -a "$GITHUB_STEP_SUMMARY"
+ else
+ echo 'AWF binary not installed, skipping firewall log summary'
+ fi
+ - name: Upload cache-memory data as artifact
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ if: always()
+ with:
+ name: cache-memory
+ path: /tmp/gh-aw/cache-memory
+ - name: Upload agent artifacts
+ if: always()
+ continue-on-error: true
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: agent-artifacts
+ path: |
+ /tmp/gh-aw/aw-prompts/prompt.txt
+ /tmp/gh-aw/aw_info.json
+ /tmp/gh-aw/mcp-logs/
+ /tmp/gh-aw/sandbox/firewall/logs/
+ /tmp/gh-aw/agent-stdio.log
+ /tmp/gh-aw/agent/
+ if-no-files-found: ignore
+
+ conclusion:
+ needs:
+ - activation
+ - agent
+ - detection
+ - safe_outputs
+ - update_cache_memory
+ if: (always()) && (needs.agent.result != 'skipped')
+ runs-on: ubuntu-slim
+ permissions:
+ contents: read
+ issues: write
+ outputs:
+ noop_message: ${{ steps.noop.outputs.noop_message }}
+ tools_reported: ${{ steps.missing_tool.outputs.tools_reported }}
+ total_count: ${{ steps.missing_tool.outputs.total_count }}
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Download agent output artifact
+ continue-on-error: true
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ with:
+ name: agent-output
+ path: /tmp/gh-aw/safeoutputs/
+ - name: Setup agent output environment variable
+ run: |
+ mkdir -p /tmp/gh-aw/safeoutputs/
+ find "/tmp/gh-aw/safeoutputs/" -type f -print
+ echo "GH_AW_AGENT_OUTPUT=/tmp/gh-aw/safeoutputs/agent_output.json" >> "$GITHUB_ENV"
+ - name: Process No-Op Messages
+ id: noop
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
+ GH_AW_NOOP_MAX: 1
+ GH_AW_WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/noop.cjs');
+ await main();
+ - name: Record Missing Tool
+ id: missing_tool
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
+ GH_AW_WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/missing_tool.cjs');
+ await main();
+ - name: Handle Agent Failure
+ id: handle_agent_failure
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
+ GH_AW_WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+ GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
+ GH_AW_WORKFLOW_ID: "tactic-to-simplifier"
+ GH_AW_SECRET_VERIFICATION_RESULT: ${{ needs.agent.outputs.secret_verification_result }}
+ GH_AW_CHECKOUT_PR_SUCCESS: ${{ needs.agent.outputs.checkout_pr_success }}
+ GH_AW_GROUP_REPORTS: "false"
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/handle_agent_failure.cjs');
+ await main();
+ - name: Handle No-Op Message
+ id: handle_noop_message
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
+ GH_AW_WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+ GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
+ GH_AW_NOOP_MESSAGE: ${{ steps.noop.outputs.noop_message }}
+ GH_AW_NOOP_REPORT_AS_ISSUE: "true"
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/handle_noop_message.cjs');
+ await main();
+
+ detection:
+ needs: agent
+ if: needs.agent.outputs.output_types != '' || needs.agent.outputs.has_patch == 'true'
+ runs-on: ubuntu-latest
+ permissions: {}
+ concurrency:
+ group: "gh-aw-copilot-${{ github.workflow }}"
+ timeout-minutes: 10
+ outputs:
+ success: ${{ steps.parse_results.outputs.success }}
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Download agent artifacts
+ continue-on-error: true
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ with:
+ name: agent-artifacts
+ path: /tmp/gh-aw/threat-detection/
+ - name: Download agent output artifact
+ continue-on-error: true
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ with:
+ name: agent-output
+ path: /tmp/gh-aw/threat-detection/
+ - name: Print agent output types
+ env:
+ AGENT_OUTPUT_TYPES: ${{ needs.agent.outputs.output_types }}
+ run: |
+ echo "Agent output-types: $AGENT_OUTPUT_TYPES"
+ - name: Setup threat detection
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ WORKFLOW_DESCRIPTION: "Compares exposed tactics and simplifiers in Z3, and creates issues for tactics that can be converted to simplifiers"
+ HAS_PATCH: ${{ needs.agent.outputs.has_patch }}
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/setup_threat_detection.cjs');
+ await main();
+ - name: Ensure threat-detection directory and log
+ run: |
+ mkdir -p /tmp/gh-aw/threat-detection
+ touch /tmp/gh-aw/threat-detection/detection.log
+ - name: Validate COPILOT_GITHUB_TOKEN secret
+ id: validate-secret
+ run: /opt/gh-aw/actions/validate_multi_secret.sh COPILOT_GITHUB_TOKEN 'GitHub Copilot CLI' https://github.github.com/gh-aw/reference/engines/#github-copilot-default
+ env:
+ COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+ - name: Install GitHub Copilot CLI
+ run: /opt/gh-aw/actions/install_copilot_cli.sh 0.0.412
+ - name: Execute GitHub Copilot CLI
+ id: agentic_execution
+ # Copilot CLI tool arguments (sorted):
+ # --allow-tool shell(cat)
+ # --allow-tool shell(grep)
+ # --allow-tool shell(head)
+ # --allow-tool shell(jq)
+ # --allow-tool shell(ls)
+ # --allow-tool shell(tail)
+ # --allow-tool shell(wc)
+ timeout-minutes: 20
+ run: |
+ set -o pipefail
+ COPILOT_CLI_INSTRUCTION="$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"
+ mkdir -p /tmp/
+ mkdir -p /tmp/gh-aw/
+ mkdir -p /tmp/gh-aw/agent/
+ mkdir -p /tmp/gh-aw/sandbox/agent/logs/
+ copilot --add-dir /tmp/ --add-dir /tmp/gh-aw/ --add-dir /tmp/gh-aw/agent/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --disable-builtin-mcps --allow-tool 'shell(cat)' --allow-tool 'shell(grep)' --allow-tool 'shell(head)' --allow-tool 'shell(jq)' --allow-tool 'shell(ls)' --allow-tool 'shell(tail)' --allow-tool 'shell(wc)' --prompt "$COPILOT_CLI_INSTRUCTION"${GH_AW_MODEL_DETECTION_COPILOT:+ --model "$GH_AW_MODEL_DETECTION_COPILOT"} 2>&1 | tee /tmp/gh-aw/threat-detection/detection.log
+ env:
+ COPILOT_AGENT_RUNNER_TYPE: STANDALONE
+ COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+ GH_AW_MODEL_DETECTION_COPILOT: ${{ vars.GH_AW_MODEL_DETECTION_COPILOT || '' }}
+ GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
+ GITHUB_HEAD_REF: ${{ github.head_ref }}
+ GITHUB_REF_NAME: ${{ github.ref_name }}
+ GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
+ GITHUB_WORKSPACE: ${{ github.workspace }}
+ XDG_CONFIG_HOME: /home/runner
+ - name: Parse threat detection results
+ id: parse_results
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ with:
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/parse_threat_detection_results.cjs');
+ await main();
+ - name: Upload threat detection log
+ if: always()
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: threat-detection.log
+ path: /tmp/gh-aw/threat-detection/detection.log
+ if-no-files-found: ignore
+
+ safe_outputs:
+ needs:
+ - agent
+ - detection
+ if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (needs.detection.outputs.success == 'true')
+ runs-on: ubuntu-slim
+ permissions:
+ contents: read
+ issues: write
+ timeout-minutes: 15
+ env:
+ GH_AW_ENGINE_ID: "copilot"
+ GH_AW_WORKFLOW_ID: "tactic-to-simplifier"
+ GH_AW_WORKFLOW_NAME: "Tactic-to-Simplifier Comparison Agent"
+ outputs:
+ create_discussion_error_count: ${{ steps.process_safe_outputs.outputs.create_discussion_error_count }}
+ create_discussion_errors: ${{ steps.process_safe_outputs.outputs.create_discussion_errors }}
+ process_safe_outputs_processed_count: ${{ steps.process_safe_outputs.outputs.processed_count }}
+ process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }}
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Download agent output artifact
+ continue-on-error: true
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ with:
+ name: agent-output
+ path: /tmp/gh-aw/safeoutputs/
+ - name: Setup agent output environment variable
+ run: |
+ mkdir -p /tmp/gh-aw/safeoutputs/
+ find "/tmp/gh-aw/safeoutputs/" -type f -print
+ echo "GH_AW_AGENT_OUTPUT=/tmp/gh-aw/safeoutputs/agent_output.json" >> "$GITHUB_ENV"
+ - name: Process Safe Outputs
+ id: process_safe_outputs
+ uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
+ env:
+ GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
+ GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_issue\":{\"labels\":[\"enhancement\",\"refactoring\",\"tactic-to-simplifier\"],\"max\":3,\"title_prefix\":\"[tactic-to-simplifier] \"},\"missing_data\":{},\"missing_tool\":{}}"
+ with:
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+ script: |
+ const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
+ setupGlobals(core, github, context, exec, io);
+ const { main } = require('/opt/gh-aw/actions/safe_output_handler_manager.cjs');
+ await main();
+ - name: Upload safe output items manifest
+ if: always()
+ uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6
+ with:
+ name: safe-output-items
+ path: /tmp/safe-output-items.jsonl
+ if-no-files-found: warn
+
+ update_cache_memory:
+ needs:
+ - agent
+ - detection
+ if: always() && needs.detection.outputs.success == 'true'
+ runs-on: ubuntu-latest
+ permissions: {}
+ env:
+ GH_AW_WORKFLOW_ID_SANITIZED: tactictosimplifier
+ steps:
+ - name: Setup Scripts
+ uses: github/gh-aw/actions/setup@v0.47.6
+ with:
+ destination: /opt/gh-aw/actions
+ - name: Download cache-memory artifact (default)
+ id: download_cache_default
+ uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6
+ continue-on-error: true
+ with:
+ name: cache-memory
+ path: /tmp/gh-aw/cache-memory
+ - name: Check if cache-memory folder has content (default)
+ id: check_cache_default
+ shell: bash
+ run: |
+ if [ -d "/tmp/gh-aw/cache-memory" ] && [ "$(ls -A /tmp/gh-aw/cache-memory 2>/dev/null)" ]; then
+ echo "has_content=true" >> $GITHUB_OUTPUT
+ else
+ echo "has_content=false" >> $GITHUB_OUTPUT
+ fi
+ - name: Save cache-memory to cache (default)
+ if: steps.check_cache_default.outputs.has_content == 'true'
+ uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+ with:
+ key: memory-${{ env.GH_AW_WORKFLOW_ID_SANITIZED }}-${{ github.run_id }}
+ path: /tmp/gh-aw/cache-memory
+
diff --git a/.github/workflows/tactic-to-simplifier.md b/.github/workflows/tactic-to-simplifier.md
new file mode 100644
index 000000000..994b76dac
--- /dev/null
+++ b/.github/workflows/tactic-to-simplifier.md
@@ -0,0 +1,278 @@
+---
+description: Compares exposed tactics and simplifiers in Z3, and creates issues for tactics that can be converted to simplifiers
+
+on:
+ schedule: weekly
+ workflow_dispatch:
+
+timeout-minutes: 30
+
+permissions:
+ contents: read
+ issues: read
+ pull-requests: read
+
+network: defaults
+
+tools:
+ cache-memory: true
+ github:
+ toolsets: [default]
+ bash: [":*"]
+ glob: {}
+ view: {}
+
+safe-outputs:
+ create-issue:
+ labels:
+ - enhancement
+ - refactoring
+ - tactic-to-simplifier
+ title-prefix: "[tactic-to-simplifier] "
+ max: 3
+ github-token: ${{ secrets.GITHUB_TOKEN }}
+
+steps:
+ - name: Checkout repository
+ uses: actions/checkout@v5
+ with:
+ persist-credentials: false
+
+---
+
+# Tactic-to-Simplifier Comparison Agent
+
+You are an expert Z3 theorem prover developer. Your task is to compare the tactics and simplifiers exposed in the Z3 codebase, identify tactics that could be converted into simplifiers, and create GitHub issues with the proposed code changes.
+
+## Background
+
+Z3 has two related but distinct abstraction layers:
+
+- **Tactics** (`tactic` base class in `src/tactic/tactic.h`): Operate on *goals* (sets of formulas). Registered with `ADD_TACTIC` macros.
+- **Simplifiers** (`dependent_expr_simplifier` base class in `src/ast/simplifiers/dependent_expr_state.h`): Operate on individual `dependent_expr` objects in a `dependent_expr_state`. Registered with `ADD_SIMPLIFIER` macros.
+
+The preferred modern pattern wraps a simplifier as a tactic using `dependent_expr_state_tactic` (see `src/tactic/dependent_expr_state_tactic.h`). Example from `src/tactic/core/propagate_values2_tactic.h`:
+
+```cpp
+inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+ return alloc(dependent_expr_state_tactic, m, p,
+ [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(propagate_values, m, p, s); });
+}
+
+/*
+ ADD_TACTIC("propagate-values2", "propagate constants.", "mk_propagate_values2_tactic(m, p)")
+ ADD_SIMPLIFIER("propagate-values", "propagate constants.", "alloc(propagate_values, m, p, s)")
+*/
+```
+
+## Your Task
+
+### Step 1: Collect All Tactics
+
+Scan all header files in `src/` to extract every `ADD_TACTIC` registration:
+
+```bash
+grep -rn "ADD_TACTIC(" src/ --include="*.h" | grep -v "^Binary"
+```
+
+Parse each line to extract:
+- Tactic name (first quoted string)
+- Description (second quoted string)
+- Factory expression (third quoted string)
+- File path
+
+### Step 2: Collect All Simplifiers
+
+Scan all header files to extract every `ADD_SIMPLIFIER` registration:
+
+```bash
+grep -rn "ADD_SIMPLIFIER(" src/ --include="*.h" | grep -v "^Binary"
+```
+
+Parse each line to extract:
+- Simplifier name
+- Description
+- Factory expression
+- File path
+
+### Step 3: Compare and Find Gaps
+
+Build a comparison table. For each tactic, check if there is a corresponding simplifier with the same or a closely related name.
+
+Key rules for matching:
+- Exact name match: tactic `simplify` ↔ simplifier `simplify`
+- Version suffix: tactic `propagate-values2` corresponds to simplifier `propagate-values` (the "2" suffix indicates the tactic wraps the simplifier)
+- Suffix `2`: tactics with `2` suffix (e.g., `elim-uncnstr2`, `propagate-bv-bounds2`) typically already have a simplifier counterpart
+
+Identify tactics that have **no corresponding simplifier**.
+
+### Step 4: Evaluate Convertibility
+
+For each tactic without a corresponding simplifier, assess whether it is a good candidate for conversion by examining its implementation:
+
+```bash
+# Read the tactic's header file to understand its implementation
+grep -rn "mk__tactic\|class " src/ --include="*.h" --include="*.cpp"
+```
+
+A tactic is a **good conversion candidate** if:
+1. It transforms formulas in a formula-by-formula way (no goal splitting/branching)
+2. It does not produce multiple goals from one
+3. It is a pure simplification (rewrites terms without adding new conjuncts that split the goal)
+4. It doesn't require global goal analysis beyond what `dependent_expr_state` provides
+
+A tactic is **not suitable** for conversion if:
+- It splits goals into multiple subgoals
+- It requires tight coupling to the goal infrastructure
+- It depends on features unavailable in `dependent_expr_simplifier` (e.g., `goal_num_occurs`)
+- It only makes sense in a tactic pipeline (e.g., `fail`, `skip`, `sat`, `smt`, solver tactics)
+- It is a portfolio tactic (combines multiple tactics)
+
+### Step 5: Check for Existing Issues
+
+Before creating any issue, search for existing open issues to avoid duplicates:
+
+Use GitHub tools to search: `repo:${{ github.repository }} is:issue is:open label:tactic-to-simplifier ""`
+
+Also check cache memory for previously created issues.
+
+### Step 6: Create Issues for Convertible Tactics
+
+For each convertible tactic that does not already have an open issue:
+
+1. Read the tactic's existing implementation carefully (header + cpp files)
+2. Design the corresponding `dependent_expr_simplifier` subclass
+3. Draft the code for the new simplifier
+
+Use `create-issue` to create a GitHub issue with:
+
+**Title**: `Convert tactic '' to a simplifier`
+
+**Body**:
+
+```markdown
+## Summary
+
+The `` tactic (described as: "") currently only exists as a `tactic`
+and has no corresponding `dependent_expr_simplifier`. This issue proposes converting it to
+expose it as both a tactic (via the `dependent_expr_state_tactic` wrapper) and a simplifier.
+
+## Background
+
+Z3 provides two abstraction layers for formula transformation:
+- **Tactics** (`tactic` base class): Operate on goals
+- **Simplifiers** (`dependent_expr_simplifier` base class): Operate on individual formulas in a `dependent_expr_state`
+
+The modern pattern wraps a simplifier inside a tactic using `dependent_expr_state_tactic`.
+
+## Current Implementation
+
+File: ``
+
+```cpp
+// Existing tactic registration
+ADD_TACTIC("", "", "mk__tactic(m, p)")
+```
+
+## Proposed Change
+
+### 1. Create a new simplifier class in `src/ast/simplifiers/_simplifier.h`:
+
+```cpp
+#pragma once
+#include "ast/simplifiers/dependent_expr_state.h"
+// ... other includes
+
+class _simplifier : public dependent_expr_simplifier {
+ // ... internal state
+public:
+ _simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s)
+ : dependent_expr_simplifier(m, s) { }
+
+ char const* name() const override { return ""; }
+
+ void reduce() override {
+ for (unsigned idx : indices()) {
+ auto& d = m_fmls[idx];
+ // ... transform d.fml() ...
+ expr_ref new_fml(m);
+ // apply simplification
+ m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep()));
+ }
+ }
+};
+```
+
+### 2. Update `` to add the simplifier registration and new tactic factory:
+
+```cpp
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/_simplifier.h"
+
+inline tactic* mk_2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+ return alloc(dependent_expr_state_tactic, m, p,
+ [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
+ return alloc(_simplifier, m, p, s);
+ });
+}
+
+/*
+ ADD_TACTIC("2", "", "mk_2_tactic(m, p)")
+ ADD_SIMPLIFIER("", "", "alloc(_simplifier, m, p, s)")
+*/
+```
+
+## Benefits
+
+- Enables use of `` in Z3's simplifier pipeline (used by the new solver engine)
+- Follows the established modern pattern for formula simplification in Z3
+- No behavioral change for existing tactic users
+
+## Notes
+
+- The original `mk__tactic` should remain for backward compatibility
+- The simplifier should implement `supports_proofs()` if proof generation is relevant
+```
+
+**Important instructions for issue body**:
+- Replace all placeholders (``, ``, ``, ``, etc.) with **real, specific values** from the actual source code
+- Provide **actual code** based on reading the tactic's implementation, not generic templates
+- Include the real factory expression, include paths, and class names from the existing implementation
+- If the tactic has parameters, include them in the simplifier
+- If the tactic wraps another component (rewriter, solver, etc.), include that in the simplifier too
+
+### Step 7: Update Cache Memory
+
+Store in cache memory:
+- The list of all tactics analyzed in this run
+- The list of issues created (tactic name → issue number)
+- Tactics determined to be non-convertible and why
+- Tactics with existing issues (to skip in future runs)
+
+## Conversion Criteria Reference
+
+### Likely Convertible (if no simplifier exists)
+- Pure term rewriting tactics (apply rewriting rules)
+- Bound propagation tactics
+- Variable elimination tactics that work formula-by-formula
+- Normalization tactics (NNF, SNF) that apply local transformations
+- Tactics that simplify based on syntactic structure
+
+### Not Convertible (skip these)
+- Solver-based tactics (`ctx-solver-simplify`, `sat`, `smt`, etc.) — require a solver
+- Portfolio/combinator tactics (`then`, `or-else`, `repeat`, etc.)
+- Decision procedure tactics (`qfbv`, `qflra`, etc.)
+- Tactics that split goals (`split-clause`, `tseitin-cnf`, `occf`)
+- Tactics that only make sense in goal context (`fail`, `skip`)
+- Tactics using `goal_num_occurs` for occurrence counting (the simplifier doesn't have this)
+- Tactics that produce multiple result goals
+
+## Guidelines
+
+- **Be specific**: Provide actual file paths, class names, and factory expressions — no generic placeholders
+- **Be careful**: Only create issues for tactics that are genuinely good candidates
+- **Avoid duplicates**: Always check existing issues before creating new ones
+- **One issue per tactic**: Create separate issues for each convertible tactic
+- **Read the code**: Examine the actual tactic implementation before proposing code for the simplifier
+- **Be incremental**: If there are many candidates, focus on the most impactful ones first
+- **Limit per run**: Create at most 3 new issues per run to avoid flooding the issue tracker