Z3定理的函数规划证明
使用函数式编程原理对Z3定理证明器功能进行弃权的Python实现，通过模型上下文协议（MCP）服务器公开。
概述
该项目演示了如何使用Z3定理证明器和函数式编程方法来解决复杂的约束满足问题，并分析实体之间的关系。它利用了 returns 函数式编程抽象库，并通过MCP服务器公开其功能。
特性
- 约束满足问题：解决具有变量和约束的复杂问题
- 关系分析：分析和推断实体之间的关系
- 函数式编程：使用纯函数、不可变数据结构和一元错误处理
- MCP服务器：通过标准化接口展示Z3功能
项目结构
z3_mcp/
├── core/ # Core implementation
│ ├── solver.py # Constraint satisfaction problem solving
│ └── relationships.py # Relationship analysis
├── models/ # Data models
│ ├── constraints.py # Models for constraint problems
│ └── relationships.py # Models for relationship analysis
├── server/ # MCP server
│ └── main.py # Server implementation
└── examples/ # Example usage
└── main.py # Demonstration of capabilities技术栈
- Z3求解器：用于约束求解的Microsoft定理证明器
- 退货：用于一元运算和错误处理的函数式编程库
- 派丹蒂克：数据验证和序列化
- FastMCP：模型上下文协议的实现
安装
此项目使用 uv 用于依赖性管理。
# Clone the repository
git clone https://github.com/javergar/z3_mcp.git
cd z3_mcp
# Install dependencies
uv pip install -e .
# Install development dependencies (optional)
uv pip install -e ".[dev]"用法
运行示例
该项目包括几个示例，展示了Z3求解器的功能：
# Run the examples
python -m z3_poc.examples.main示例包括：
- N皇后问题
- 家庭关系推断
- 因果关系时态推理
- 密码谜题（发送+更多=金钱）
运行MCP服务器
启动MCP服务器，通过模型上下文协议公开Z3功能：
# Run the server
python -m z3_poc.server.main用Claude/Cline建立MCP服务器
要通过VSCode中的Cline扩展与Claude一起使用Z3求解器MCP服务器，您需要配置 settings.json 文件：
- 配置：将以下内容添加到
mcpServers设置文件中的对象：
"z3-solver": {
"command": "uv",
"args": [
"--directory",
"/path/to/your/z3_poc",
"run",
"z3_poc/server/main.py"
],
"disabled": false,
"autoApprove": [
"simple_constraint_solver",
"simple_relationship_analyzer",
"solve_constraint_problem",
"analyze_relationships"
]
}- 配置选项:
- command：要运行的命令（使用 uv Python环境管理） - args：命令参数，包括项目路径和服务器脚本 - disabled：设置为 false 启用服务器 - autoApprove：未经明确批准可使用的工具清单
- 重启：更新设置后，重新启动VSCode或Claude Desktop应用程序以使更改生效。
配置后，Claude将可以通过MCP服务器访问Z3求解器功能。
MCP工具
服务器提供以下工具：
solve_constraint_problem
使用完整的问题模型解决约束满足问题。
# Example input
{
"problem": {
"variables": [
{"name": "x", "type": "integer"},
{"name": "y", "type": "integer"}
],
"constraints": [
{"expression": "x + y == 10"},
{"expression": "x >= 0"},
{"expression": "y >= 0"}
],
"description": "Find non-negative values for x and y that sum to 10"
}
}analyze_relationships
使用完整的RelationshipQuery模型分析实体之间的关系。
# Example input
{
"query": {
"relationships": [
{"person1": "Alice", "person2": "Bob", "relation": "sibling"},
{"person1": "Bob", "person2": "Charlie", "relation": "sibling"}
],
"query": "sibling(Alice, Charlie)"
}
}simple_constraint_solver
一个更简单的界面，用于解决约束问题，而不需要完整的问题模型。
# Example input
{
"variables": [
{"name": "x", "type": "integer"},
{"name": "y", "type": "integer"}
],
"constraints": [
"x + y == 10",
"x <= 5",
"y <= 5"
],
"description": "Find values for x and y"
}simple_relationship_analyzer
一个更简单的接口，用于分析关系，而不需要完整的RelationshipQuery模型。
# Example input
{
"relationships": [
{"person1": "Bob", "person2": "Hanna", "relation": "sibling"},
{"person1": "Bob", "person2": "Claudia", "relation": "sibling"}
],
"query": "sibling(Hanna, Claudia)"
}函数式编程方法
这个项目演示了几个函数式编程原理：
- 不可变数据结构：使用Pydantic模型进行不可变数据表示
- 结果类型：使用
returns.result.Result用于无例外的错误处理 - 也许类型：使用
returns.maybe.Maybe用于处理可为null的值 - 做记号：使用生成器表达式
Result.do()用于顺序操作 - 模式匹配：使用Python的match case来处理不同的结果类型
do符号示例 analyze_relationships:
expr = (
RelationshipResult(...)
for entities in create_entities(query.relationships)
for relations in create_relations(query.relationships)
for _ in add_relationship_assertions(solver, query.relationships, entities, relations)
for query_expr in parse_query(query.query, entities, relations)
for (result, explanation, is_satisfiable) in evaluate_query(solver, query_expr)
)
return Result.do(expr)贡献
欢迎投稿！请随时提交拉取请求。
许可证
此项目根据MIT许可证获得许可-有关详细信息，请参阅许可证文件。
