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 |