mcp-z3-prover
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": true
} |
| logging | {} |
| prompts | {
"listChanged": false
} |
| resources | {
"subscribe": false,
"listChanged": false
} |
| extensions | {
"io.modelcontextprotocol/ui": {}
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| create_bool_varB | Create a Boolean variable with the given name. |
| create_int_varB | Create an Integer variable with the given name. |
| create_real_varB | Create a Real (floating-point) variable with the given name. |
| create_int_constantB | Create an integer constant with the given value. |
| create_real_constantB | Create a real constant with the given value. |
| add_constraintA | Add a constraint to the solver. Use variable references like 'bool:x', 'int:y', 'real:z' in expressions. Supports standard Z3 Python API syntax. |
| solveB | Solve the current problem and return the result. Checks all added constraints for satisfiability and returns a model if the problem is SAT. |
| get_model_valueA | Get the value of a variable from the model after solving. |
| optimizeA | Solve with an optimization objective (maximize or minimize). Finds the optimal value for the given objective function subject to all added constraints. |
| reset_solverA | Reset the solver state. Clears all variables, constants, constraints, and model data. Useful when starting a new problem. Returns: A dictionary with status and a success message. Example: >>> create_int_var("x") 'int:x' >>> add_constraint("int:x > 5") {'status': 'success', 'constraint': 'int:x > 5'} >>> reset_solver() {'status': 'success', 'message': 'Solver reset successfully'} >>> list_variables() {'variables': []} |
| list_variablesA | List all created variables. Returns: A dictionary containing a list of all variable references. Example: >>> create_int_var("x") 'int:x' >>> create_bool_var("flag") 'bool:flag' >>> list_variables() {'variables': ['int:x', 'bool:flag']} |
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 11 tools
Each tool has a clear, distinct purpose: variable creation for different types (bool, int, real) with separate creation of constants and variables, constraint addition, solving, optimization, model retrieval, listing, and reset. No overlap.
All tool names follow a consistent snake_case verb_noun pattern (e.g., create_int_var, add_constraint, get_model_value). No mixing of conventions.
11 tools is well-scoped for a constraint solver. Each tool serves a necessary function without being overly granular or too sparse.
Covers the core workflow: variable creation, constraints, solving, and model retrieval. Minor gaps exist, such as no push/pop for incremental solving or constraint deletion, but the essential operations are present.