Расшифровка результатов Z3-решателя

★ 6.5 · data

explain is a Claude Code skill that parses and interprets Z3 solver output, translating raw solver internals into structured plain-language explanations. It accepts output from the solve, prove, optimize, or benchmark skills and handles five output types: models (`define-fun` blocks), unsat cores, performance statistics, proof terms, and error messages. The core component is `explain.py`, invoked with `--file` or `--stdin`; output type is auto-detected but can be forced via `--type`. Model explanations expand each variable's value and sort, array and function interpretations, and bitvector values in both decimal and hex; statistics break down solver time by phase (preprocessing, solving, model construction) and report memory high-water marks. The skill is aimed at anyone doing SMT-based constraint solving who needs to understand Z3 output without manually parsing its internal syntax.