MCP Z3 Prover

mcp-z3-prover

MCP服务器暴露Z3解算器API

  

安装

pip install mcp-z3-prover

用法

from mcp_z3_prover import mcp

# Run the server
mcp.run()

或者从命令行：

mcp-z3-prover

MCP工具

服务器公开了以下工具：

• create_bool_var -创建布尔变量
• create_int_var -创建一个Integer变量
• create_real_var -创建一个实变量
• create_int_constant -创建一个整数常量
• create_real_constant -创建一个真正的常量
• add_约束 -向求解器添加约束
• 解决 -解决当前问题
• get_model_value -从模型中获取变量的值
• 优化 -以优化目标求解
• reset_solver -重置求解器状态
• list_变量 -列出所有创建的变量

示例

# 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")

整数分解示例

# Factor n = 4295229443 where n = p * q with q  int:p")
add_constraint("4295229443 > int:q")
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

发展

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注册

mcp名称：io.github.daedalus/mcp-z3-prover