Mcp Z3 Prover

io.github.daedalus由 GitHub 账号 daedalus 发布v0.1.0更新于 Oct 28, 2026

MCP server exposing Z3 solver API

已验证STDIO仅桌面开发者工具AI 与机器学习

概览

AI 生成的概览

本地 MCP 服务器，封装 Z3 求解器，让助手创建变量与约束并进行求解或优化。

可以做什么
  • 创建布尔、整数和实数变量，以及整数或实数常量
  • 向求解器添加约束并求解当前问题
  • 从结果模型中读取变量取值
  • 带优化目标进行求解
  • 重置求解器状态并列出已创建的变量
适用场景
适合让助手判断一组逻辑或算术约束是否可满足、找出满足条件的赋值，或对目标进行优化，例如小规模因数分解或逻辑谜题类问题。
运行要求
以本地进程运行，需从 PyPI 安装 mcp-z3-prover 包（pip install mcp-z3-prover），并用 mcp-z3-prover 命令启动；仅支持桌面环境。未声明认证、环境变量或请求头。
安装前请注意
求解器在多次调用间保留状态，约束会不断累积，需重置才能清空；困难问题可能耗时较长或占用大量 CPU。未显示需要凭据、付费或向第三方发送数据。

安装

在 SourceWeft 中

  1. 打开 控制台中的 Mcp Z3 Prover，将其添加到工作区。
  2. 为需要使用其工具的对话启用该服务。

Desktop only，通过 STDIO。 STDIO 服务会启动本地进程，因此需要 SourceWeft 桌面宿主。

其他 MCP 客户端

参照 仓库 中的启动说明。

README

mcp-z3-prover

MCP server exposing Z3 solver API

[PyPI] [Python] [Ruff]

Install

bash
pip install mcp-z3-prover

Usage

python
from mcp_z3_prover import mcp
# Run the servermcp.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 variablescreate_int_var("x")create_int_var("y")
# Add constraintsadd_constraint("int:x + int:y == 10")add_constraint("int:x > 0")add_constraint("int:y > 0")
# Solveresult = solve()# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}
# Get specific valuesx_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 constraintsadd_constraint("int:p * int:q == 4295229443")add_constraint("4295229443 > int:p")add_constraint("4295229443 > int:q")add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537add_constraint("int:q > 1")add_constraint("int:p > 1")add_constraint("int:q % 2 != 0")  # q is oddadd_constraint("int:p % 2 != 0")  # p is odd
# Solveresult = solve()# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}# Verification: 65537 * 65539 = 4295229443

Development

bash
git clone https://github.com/daedalus/mcp-z3-prover.gitcd mcp-z3-proverpip install -e ".[test]"
# run testspytest
# formatruff format src/ tests/
# lintruff check src/ tests/
# type checkmypy src/

MCP Registration

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

来源：README.md，提交 12bcd34

工具

0
SourceWeft 尚未在沙箱中启动过该软件包，因此其工具未知。

版本历史

1
  1. v0.1.0最新Sep 16, 2026

评分

已满足适用检查项的 50%

该评分衡量此收录条目的完整程度，依据注册中心条目、端点与公开来源计算得出。它不是对服务器本身的评价，也不表示服务器安全或当前可用：可连通性是带日期的检查结果，评分也不包含安装量或用户评价。

  • 近 30 天内可连通25 分

    请保持端点能够响应 MCP 握手；SourceWeft 每 30 天探测一次。

  • 已声明认证方式10 分

    请在注册中心条目中声明凭据请求头，或保持端点能够响应探测，以便判定其认证方式。

  • 已列出工具15 分

    请让服务器在无凭据时响应 tools/list，或发布可在沙箱中无凭据启动的软件包。

  • 描述必需15 分
  • 图标10 分
  • 文档15 分
  • 许可证10 分