# Z3 SMT Solver MCP Server

A Model Context Protocol (MCP) server that provides SMT (Satisfiability Modulo Theories) solving capabilities using the Z3 theorem prover. This server allows Claude and other MCP clients to solve complex constraint satisfaction problems, mathematical equations, logic puzzles, and optimization problems.

## Features

- **SMT-LIB2 Support**: Accepts problems in the standard SMT-LIB2 format
- **Z3 Integration**: Powered by Microsoft's Z3 theorem prover
- **Mathematical Problem Solving**: Handle algebra, logic, optimization, and constraint satisfaction
- **Simple Interface**: Single tool with string input/output

## Installation

### Prerequisites

- Python 3.8 or higher
- uv (recommended) or pip

### Setup

1. Clone this repository:
```bash
git clone <repository-url>
cd z3-mcp-server
```

2. Install dependencies:
```bash
uv sync
```

Or with pip:
```bash
pip install z3-solver mcp
```

3. Make the server executable:
```bash
chmod +x src/z3_mcp_server/main.py
```

## Usage

### With Claude Desktop

Add the server to your Claude Desktop configuration file:

**macOS**: `~/Library/Application Support/Claude/claude_desktop_config.json`
**Windows**: `%APPDATA%/Claude/claude_desktop_config.json`

```json
{
  "mcpServers": {
    "z3-solver": {
      "command": "uv",
      "args": ["--directory", "/path/to/z3-mcp-server", "run", "main.py"],
      "env": {}
    }
  }
}
```

### Example Problems

Once configured, you can ask Claude to solve various types of problems:

**Age Problems**:
> "Joey is 20 years younger than Becky. In two years, Becky will be twice as old as Joey. How old are they?"

**Algebra**:
> "Find integers x and y such that 2x + 3y = 17 and both are positive."

**Logic Puzzles**:
> "Three people have ages 21, 22, and 23. Alice is not 21, and Bob is older than Alice. What are their ages?"

**Optimization**:
> "A farmer has 100 feet of fencing. What rectangular dimensions maximize the enclosed area?"

## Tool Reference

### `solve_smt_lib2`

Solves constraint problems specified in SMT-LIB2 format.

**Parameters**:
- `problem` (string): The constraint problem in SMT-LIB2 syntax

**Returns**:
- String containing the solver result:
  - `sat` + model if satisfiable
  - `unsat` if no solution exists
  - `unknown` if solver cannot determine
  - Error message if parsing fails

**Example SMT-LIB2 Input**:
```smt2
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (* x y) 21))
(check-sat)
(get-model)
```

## SMT-LIB2 Quick Reference

### Basic Syntax
- `(declare-const name Type)` - Declare a variable
- `(assert condition)` - Add a constraint
- `(check-sat)` - Check if constraints are satisfiable
- `(get-model)` - Get variable assignments (if sat)

### Types
- `Int` - Integers
- `Real` - Real numbers
- `Bool` - Boolean values

### Operations
- Arithmetic: `+`, `-`, `*`, `/`, `mod`
- Comparison: `=`, `<`, `>`, `<=`, `>=`
- Logic: `and`, `or`, `not`
- Special: `distinct` (all different)

## Transport Support

Currently supports:
- **stdio**: For use with Claude Desktop and similar local clients

Planned:
- **HTTP/WebSocket**: For web-based integrations

## Troubleshooting

### Common Issues

1. **Server not starting**: Ensure Python and z3-solver are properly installed
2. **Permission denied**: Make sure the main.py file is executable
3. **Import errors**: Verify all dependencies are installed in the correct environment

### Debug Mode

Run the server directly in the Inspector:
```bash
npx @modelcontextprotocol/inspector src/z3_mcp_server/main.py uv --directory /path/to/z3-mcp-server run main.py
```

## Contributing

Contributions are welcome! Please:

1. Fork the repository
2. Create a feature branch
3. Add tests for new functionality
4. Submit a pull request