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.

Quality

71%

Does it follow best practices?

Run evals on this skill

Adds up to 20 points to the overall score

View guide

Securityby

Passed

No findings from the security scan

Fix and improve this skill with Tessl

tessl review fix ./.github/skills/encode/SKILL.md

Quality

Content

85%

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

The content is concise, well-structured, and has a clear validated workflow with an error-recovery loop. Its main weakness is that the documented generation commands do not match the bundled encode.py, which only validates — making the headline example misleading rather than executable.

Suggestions

Reconcile the example commands with the actual scripts/encode.py interface: the script supports only --validate, so either document validation usage accurately or extend the script to support the shown --problem/--format generation.

Clarify the division of labor between the agent (which drafts the encoding) and encode.py (which validates it), since Step 2 implies the script generates the encoding.

Show the validation invocation explicitly (e.g. "python3 scripts/encode.py --validate out.smt2") so the executable path in the examples matches the real tool.

Dimension	Reasoning	Score
Conciseness	The body is lean: a theory-mapping table, three Action/Expectation/Result steps, two example commands, and a parameter table, with no padding explaining what SMT or z3 is. Every section does work and assumes Claude's competence, matching the anchor 3 example of efficient, token-earning content.	3 / 3
Actionability	The example commands look copy-paste ready ("python3 scripts/encode.py --problem ... --format smtlib2"), but the bundled scripts/encode.py only supports --validate and cannot generate encodings from --problem, so the documented primary workflow is not actually executable against the real script — a missing key detail that matches anchor 2 rather than fully executable guidance.	2 / 3
Workflow Clarity	A clear three-step sequence (identify class, generate, validate) includes an explicit validation checkpoint in Step 3 with a feedback loop ("On parse error: fix the reported line and re-run"), matching the anchor 3 example of clear sequencing with explicit validation and error recovery.	3 / 3
Progressive Disclosure	The ~70-line body is well-organized into labeled sections and references a single real bundle file (scripts/encode.py) one level deep with no nested reference chains; for a compact, single-purpose skill this matches the rubric's allowance that well-organized sections score 3 without external reference files.	3 / 3
	Total	11 / 12 Passed

Description

57%

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

The description is concrete and occupies a distinct, low-conflict niche, but it lacks an explicit "Use when..." trigger clause and its natural-language trigger coverage is incomplete. Adding trigger guidance and broader user-facing terms would raise it across completeness and trigger_term_quality.

Suggestions

Add an explicit trigger clause, e.g. "Use when encoding scheduling, graph coloring, arithmetic puzzles, or verification conditions as SMT constraints."

Broaden natural trigger terms to include user-facing phrasings like "constraint satisfaction", "SAT/SMT solving", and "encode constraints".

Express more than one distinct concrete action (e.g. "declare variables, assert constraints, emit check-sat/get-model") rather than a single translate action across two formats.

Dimension	Reasoning	Score
Specificity	"Translate constraint problems into SMT-LIB2 or Z3 Python API code" names a concrete deliverable and enumerates problem classes (scheduling, graph coloring, arithmetic puzzles, verification conditions), but it is essentially one action across two output formats rather than the multiple distinct actions (e.g. extract, fill, merge) that anchor 3 calls for.	2 / 3
Completeness	It clearly states what the skill does (translate constraint problems into SMT-LIB2/Z3 code) but provides no "Use when..." clause or equivalent explicit trigger guidance; per the judging guidelines a missing trigger clause caps completeness at 2.	2 / 3
Trigger Term Quality	Terms like "scheduling", "graph coloring", and "arithmetic puzzles" are natural, but coverage is incomplete — common variations such as "constraint satisfaction", "SAT/SMT solving", or "encode constraints" are missing, matching the anchor 2 example of relevant keywords without common variations.	2 / 3
Distinctiveness Conflict Risk	The SMT-LIB2 / Z3 Python API niche is specialized and clearly distinguishable from other skills, with little realistic overlap, matching the anchor 3 example of a clear niche with distinct triggers.	3 / 3
	Total	9 / 12 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: Z3Prover/z3
Path: .github/skills/encode/SKILL.md
Commit: 1c89937

Reviewed: 3 days ago

Table of Contents

Discovery Implementation Validation

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.