9d674404c8
Each step in every SKILL.md now carries labeled Action, Expectation, and Result blocks so the agent can mechanically execute, verify, and branch at each stage. Format chosen after comparing three variants (indented blocks, inline keywords, tables) on a prove-validity simulation; indented blocks scored highest on routing completeness and checkability. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2.7 KiB
| name | description |
|---|---|
| encode | Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions. |
Given a problem description (natural language, pseudocode, or a partial formulation), produce a complete, syntactically valid SMT-LIB2 encoding or Z3 Python script. The encoding should declare all variables, assert all constraints, and include the appropriate check-sat / get-model commands.
Step 1: Identify the problem class
Action: Determine the SMT theory and variable sorts required by the problem description.
Expectation: A clear mapping from the problem to one of the supported theories (LIA, LRA, QF_BV, etc.).
Result: If the theory is identified, proceed to Step 2. If the problem spans multiple theories, select the appropriate combined logic.
| Problem class | Theory | Typical sorts |
|---|---|---|
| Integer arithmetic | LIA / NIA | Int |
| Real arithmetic | LRA / NRA | Real |
| Bitvector operations | QF_BV | (_ BitVec N) |
| Arrays and maps | QF_AX | (Array Int Int) |
| Strings and regex | QF_S | String, RegLan |
| Uninterpreted functions | QF_UF | custom sorts |
| Mixed theories | AUFLIA, etc. | combination |
Step 2: Generate the encoding
Action: Invoke encode.py with the problem description and desired output format.
Expectation: The script produces a complete SMT-LIB2 file or Z3 Python script with all declarations, constraints, and check-sat commands.
Result:
For smtlib2 format: pass the output to solve.
For python format: execute the script directly.
Proceed to Step 3 for validation.
python3 scripts/encode.py --problem "Find integers x, y such that x^2 + y^2 = 25 and x > 0" --format smtlib2
python3 scripts/encode.py --problem "Schedule 4 tasks on 2 machines minimizing makespan" --format python
Step 3: Validate the encoding
Action:
The script runs a syntax check by piping the output through z3 -in
in parse-only mode.
Expectation: No parse errors. If errors occur, the offending line is reported.
Result: On success: the encoding is ready for solve, prove, or optimize. On parse error: fix the reported line and re-run.
Parameters
| Parameter | Type | Required | Default | Description |
|---|---|---|---|---|
| problem | string | yes | problem description | |
| format | string | no | smtlib2 | output format: smtlib2 or python |
| output | path | no | stdout | write to file instead of stdout |
| validate | flag | no | on | run syntax check on the output |
| debug | flag | no | off | verbose tracing |
| db | path | no | .z3-agent/z3agent.db | logging database |