Menu
Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.
Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db.
Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db.
Route gh-aw workflow create/debug/upgrade requests to the right prompts.
Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking.
Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.
Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.
| name | explain |
| description | Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations. |
Given raw Z3 output (from the solve, prove, optimize, or benchmark skills), produce a structured explanation. This skill is for cases where the solver output is large, nested, or otherwise difficult to read directly.
Action: Determine the category of Z3 output to explain: model, core, statistics, error, or proof.
Expectation: The output type maps to one of the recognized formats in the table below.
Result:
If the type is ambiguous, use --type auto and let the script detect it.
Proceed to Step 2.
| Output contains | Explanation type |
|---|---|
(define-fun ...) blocks | model explanation |
| unsat core labels | conflict explanation |
:key value statistics | performance breakdown |
(error ...) | error diagnosis |
| proof terms | proof sketch |
Action: Invoke explain.py with the output file or stdin.
Expectation: The script auto-detects the output type and produces a structured plain-language summary.
Result:
A formatted explanation is printed. If detection fails, re-run with
an explicit --type flag.
python3 scripts/explain.py --file output.txt
python3 scripts/explain.py --stdin < output.txt
python3 scripts/explain.py --file output.txt --debug
Action: Review the structured explanation for accuracy and completeness.
Expectation: Models list each variable with its value and sort. Cores list conflicting assertions. Statistics show time and memory breakdowns.
Result: Use the explanation to answer the user query or to guide the next skill invocation.
For models:
For unsat cores:
For statistics:
| Parameter | Type | Required | Default | Description |
|---|---|---|---|---|
| file | path | no | file containing Z3 output | |
| stdin | flag | no | off | read from stdin |
| type | string | no | auto | force output type: model, core, stats, error |
| debug | flag | no | off | verbose tracing |
| db | path | no | .z3-agent/z3agent.db | logging database |