// Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.
| name | encode |
| description | 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.
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 |
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
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.
| 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 |
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.
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.
Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.
Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.
Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.