z3-solver-mcp-server
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": false
} |
| prompts | {
"listChanged": false
} |
| resources | {
"subscribe": false,
"listChanged": false
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| solve_smt_lib2B | Solve the constraint problem provided in SMT-LIB2 format |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 1 tool
With only one tool, there is no possibility of confusion or overlap. The tool's purpose is singular and clear, so disambiguation is perfect.
The tool name 'solve_smt_lib2' follows a clear verb_noun pattern, indicating the action and the input format. Consistency is trivially high with a single tool.
The server has exactly one tool, which feels minimal for a solver domain. While it covers the core solve operation, a typical solver server might offer additional tools like model extraction or incremental assertions, making the count borderline.
The single tool accepts a full SMT-LIB2 script, which allows users to express a wide range of constraint problems including assertions, checks, and models. However, the lack of incremental interaction or separate utilities (e.g., parsing or model retrieval) is a minor gap.