Metadata-Version: 2.4
Name: mcp-z3-prover
Version: 0.1.0
Summary: MCP server exposing Z3 solver API
Project-URL: Homepage, https://github.com/daedalus/mcp-z3-prover
Project-URL: Repository, https://github.com/daedalus/mcp-z3-prover
Project-URL: Issues, https://github.com/daedalus/mcp-z3-prover/issues
Author-email: Darío Clavijo <clavijodario@gmail.com>
License: MIT
License-File: LICENSE
Requires-Python: >=3.11
Requires-Dist: fastmcp>=2.0.0
Requires-Dist: z3-solver>=4.13.0
Provides-Extra: all
Requires-Dist: hatch; extra == 'all'
Requires-Dist: hypothesis; extra == 'all'
Requires-Dist: mypy; extra == 'all'
Requires-Dist: pytest; extra == 'all'
Requires-Dist: pytest-asyncio; extra == 'all'
Requires-Dist: pytest-cov; extra == 'all'
Requires-Dist: pytest-mock; extra == 'all'
Requires-Dist: ruff; extra == 'all'
Provides-Extra: dev
Requires-Dist: hatch; extra == 'dev'
Requires-Dist: mypy; extra == 'dev'
Requires-Dist: ruff; extra == 'dev'
Provides-Extra: lint
Requires-Dist: mypy; extra == 'lint'
Requires-Dist: ruff; extra == 'lint'
Provides-Extra: test
Requires-Dist: hypothesis; extra == 'test'
Requires-Dist: pytest; extra == 'test'
Requires-Dist: pytest-asyncio; extra == 'test'
Requires-Dist: pytest-cov; extra == 'test'
Requires-Dist: pytest-mock; extra == 'test'
Description-Content-Type: text/markdown

# mcp-z3-prover

> MCP server exposing Z3 solver API

[![PyPI](https://img.shields.io/pypi/v/mcp-z3-prover.svg)](https://pypi.org/project/mcp-z3-prover/)
[![Python](https://img.shields.io/pypi/pyversions/mcp-z3-prover.svg)](https://pypi.org/project/mcp-z3-prover/)
[![Ruff](https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/astral-sh/ruff/main/assets/badge/v2.json)](https://github.com/astral-sh/ruff)

## Install

```bash
pip install mcp-z3-prover
```

## Usage

```python
from mcp_z3_prover import mcp

# Run the server
mcp.run()
```

Or from command line:

```bash
mcp-z3-prover
```

## MCP Tools

The server exposes the following tools:

- **create_bool_var** - Create a Boolean variable
- **create_int_var** - Create an Integer variable
- **create_real_var** - Create a Real variable
- **create_int_constant** - Create an integer constant
- **create_real_constant** - Create a real constant
- **add_constraint** - Add a constraint to the solver
- **solve** - Solve the current problem
- **get_model_value** - Get value of a variable from the model
- **optimize** - Solve with optimization objective
- **reset_solver** - Reset the solver state
- **list_variables** - List all created variables

## Example

```python
# Create variables
create_int_var("x")
create_int_var("y")

# Add constraints
add_constraint("int:x + int:y == 10")
add_constraint("int:x > 0")
add_constraint("int:y > 0")

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

# Get specific values
x_val = get_model_value("int:x")
```

### Integer Factorization Example

```python
# Factor n = 4295229443 where n = p * q with q <= sqrt(n)
create_int_var("p")
create_int_var("q")

# Add constraints
add_constraint("int:p * int:q == 4295229443")
add_constraint("4295229443 > int:p")
add_constraint("4295229443 > int:q")
add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537
add_constraint("int:q > 1")
add_constraint("int:p > 1")
add_constraint("int:q % 2 != 0")  # q is odd
add_constraint("int:p % 2 != 0")  # p is odd

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}
# Verification: 65537 * 65539 = 4295229443
```

## Development

```bash
git clone https://github.com/daedalus/mcp-z3-prover.git
cd mcp-z3-prover
pip install -e ".[test]"

# run tests
pytest

# format
ruff format src/ tests/

# lint
ruff check src/ tests/

# type check
mypy src/
```

## MCP Registration

mcp-name: io.github.daedalus/mcp-z3-prover
