{
  "markdown": "# mcp-z3-prover\n\n> MCP server exposing Z3 solver API\n\n[![PyPI](https://img.shields.io/pypi/v/mcp-z3-prover.svg)](https://pypi.org/project/mcp-z3-prover/)\n[![Python](https://img.shields.io/pypi/pyversions/mcp-z3-prover.svg)](https://pypi.org/project/mcp-z3-prover/)\n[![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)\n\n## Install\n\n```bash\npip install mcp-z3-prover\n```\n\n## Usage\n\n```python\nfrom mcp_z3_prover import mcp\n\n# Run the server\nmcp.run()\n```\n\nOr from command line:\n\n```bash\nmcp-z3-prover\n```\n\n## MCP Tools\n\nThe server exposes the following tools:\n\n- **create_bool_var** - Create a Boolean variable\n- **create_int_var** - Create an Integer variable\n- **create_real_var** - Create a Real variable\n- **create_int_constant** - Create an integer constant\n- **create_real_constant** - Create a real constant\n- **add_constraint** - Add a constraint to the solver\n- **solve** - Solve the current problem\n- **get_model_value** - Get value of a variable from the model\n- **optimize** - Solve with optimization objective\n- **reset_solver** - Reset the solver state\n- **list_variables** - List all created variables\n\n## Example\n\n```python\n# Create variables\ncreate_int_var(\"x\")\ncreate_int_var(\"y\")\n\n# Add constraints\nadd_constraint(\"int:x + int:y == 10\")\nadd_constraint(\"int:x > 0\")\nadd_constraint(\"int:y > 0\")\n\n# Solve\nresult = solve()\n# Returns: {\"status\": \"sat\", \"model\": {\"x\": \"5\", \"y\": \"5\"}}\n\n# Get specific values\nx_val = get_model_value(\"int:x\")\n```\n\n### Integer Factorization Example\n\n```python\n# Factor n = 4295229443 where n = p * q with q <= sqrt(n)\ncreate_int_var(\"p\")\ncreate_int_var(\"q\")\n\n# Add constraints\nadd_constraint(\"int:p * int:q == 4295229443\")\nadd_constraint(\"4295229443 > int:p\")\nadd_constraint(\"4295229443 > int:q\")\nadd_constraint(\"int:q <= 65537\")  # sqrt(4295229443) ≈ 65537\nadd_constraint(\"int:q > 1\")\nadd_constraint(\"int:p > 1\")\nadd_constraint(\"int:q % 2 != 0\")  # q is odd\nadd_constraint(\"int:p % 2 != 0\")  # p is odd\n\n# Solve\nresult = solve()\n# Returns: {\"status\": \"sat\", \"model\": {\"p\": \"65539\", \"q\": \"65537\"}}\n# Verification: 65537 * 65539 = 4295229443\n```\n\n## Development\n\n```bash\ngit clone https://github.com/daedalus/mcp-z3-prover.git\ncd mcp-z3-prover\npip install -e \".[test]\"\n\n# run tests\npytest\n\n# format\nruff format src/ tests/\n\n# lint\nruff check src/ tests/\n\n# type check\nmypy src/\n```\n\n## MCP Registration\n\nmcp-name: io.github.daedalus/mcp-z3-prover\n",
  "bytes": 2491,
  "sha": "e95b9f820c22114e048bcd8db5941d081dc8c05028246f7477cbaab28969d692",
  "repo_slug": "daedalus/mcp-z3-prover",
  "fonte": "repo",
  "truncated": false,
  "api": "https://agentalog.com/api/listings/mcp_io_github_daedalus_mcp_z3_prover_2cad3715/readme"
}