基于函数式编程的 Z3 定理证明器

这是一个使用函数式编程原则对 Z3 定理证明器功能进行抽象的 Python 实现，通过模型上下文协议 (MCP) 服务器公开。

概述

本项目演示了如何使用 Z3 定理证明器和函数式编程方法来解决复杂的约束满足问题并分析实体之间的关系。它利用 returns 库进行函数式编程抽象，并通过 MCP 服务器公开其功能。

特性

• 约束满足问题: 解决具有变量和约束的复杂问题
• 关系分析: 分析和推断实体之间的关系
• 函数式编程: 使用纯函数、不可变数据结构和单子错误处理
• MCP 服务器: 通过标准化接口公开 Z3 功能

项目结构

z3_mcp/
├── core/                  # 核心实现
│   ├── solver.py          # 约束满足问题求解
│   └── relationships.py   # 关系分析
├── models/                # 数据模型
│   ├── constraints.py     # 约束问题模型
│   └── relationships.py   # 关系分析模型
├── server/                # MCP 服务器
│   └── main.py            # 服务器实现
└── examples/              # 使用示例
    └── main.py            # 功能演示

技术栈

• Z3 Solver: Microsoft 的定理证明器，用于约束求解
• Returns: 用于单子运算和错误处理的函数式编程库
• Pydantic: 数据验证和序列化
• FastMCP: 模型上下文协议的实现

安装

本项目使用 uv 进行依赖管理。

# 克隆仓库
git clone https://github.com/javergar/z3_mcp.git
cd z3_mcp

# 安装依赖
uv pip install -e .

# 安装开发依赖（可选）
uv pip install -e ".[dev]"

使用

运行示例

该项目包含几个示例，演示了 Z3 求解器的功能：

# 运行示例
python -m z3_poc.examples.main

示例包括：

• N 皇后问题
• 家庭关系推断
• 具有因果关系的时间推理
• 密码算术难题 (SEND + MORE = MONEY)

运行 MCP 服务器

启动 MCP 服务器以通过模型上下文协议公开 Z3 功能：

# 运行服务器
python -m z3_poc.server.main

使用 Claude/Cline 设置 MCP 服务器

要通过 VSCode 中的 Cline 扩展将 Z3 求解器 MCP 服务器与 Claude 一起使用，您需要配置 settings.json 文件：

1. 配置: 将以下内容添加到设置文件中的 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"
  ]
}

2. 配置选项:

   • command: 要运行的命令（使用 uv 进行 Python 环境管理）
   • args: 命令参数，包括项目路径和服务器脚本
   • disabled: 设置为 false 以启用服务器
   • autoApprove: 可以使用的工具列表，无需显式批准

3. 重启: 更新设置后，重启 VSCode 或 Claude Desktop 应用程序以使更改生效。

配置完成后，Claude 将可以通过 MCP 服务器访问 Z3 求解器功能。

MCP 工具

服务器提供以下工具：

solve_constraint_problem

使用完整的 Problem 模型解决约束满足问题。

# 示例输入
{
  "problem": {
    "variables": [
      {"name": "x", "type": "integer"},
      {"name": "y", "type": "integer"}
    ],
    "constraints": [
      {"expression": "x + y == 10"},
      {"expression": "x >= 0"},
      {"expression": "y >= 0"}
    ],
    "description": "查找 x 和 y 的非负值，使其总和为 10"
  }
}

analyze_relationships

使用完整的 RelationshipQuery 模型分析实体之间的关系。

# 示例输入
{
  "query": {
    "relationships": [
      {"person1": "Alice", "person2": "Bob", "relation": "sibling"},
      {"person1": "Bob", "person2": "Charlie", "relation": "sibling"}
    ],
    "query": "sibling(Alice, Charlie)"
  }
}

simple_constraint_solver

一个更简单的接口，用于解决约束问题，无需完整的 Problem 模型。

# 示例输入
{
  "variables": [
    {"name": "x", "type": "integer"},
    {"name": "y", "type": "integer"}
  ],
  "constraints": [
    "x + y == 10",
    "x <= 5",
    "y <= 5"
  ],
  "description": "查找 x 和 y 的值"
}

simple_relationship_analyzer

一个更简单的接口，用于分析关系，无需完整的 RelationshipQuery 模型。

# 示例输入
{
  "relationships": [
    {"person1": "Bob", "person2": "Hanna", "relation": "sibling"},
    {"person1": "Bob", "person2": "Claudia", "relation": "sibling"}
  ],
  "query": "sibling(Hanna, Claudia)"
}

函数式编程方法

本项目演示了几个函数式编程原则：

1. 不可变数据结构: 使用 Pydantic 模型进行不可变数据表示
2. Result 类型: 使用 returns.result.Result 进行错误处理，无需异常
3. Maybe 类型: 使用 returns.maybe.Maybe 处理可空值
4. Do Notation: 使用带有 Result.do() 的生成器表达式进行顺序操作
5. 模式匹配: 使用 Python 的 match-case 处理不同的结果类型

analyze_relationships 中 do notation 的示例：

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)

贡献

欢迎贡献！请随时提交 Pull Request。

许可证

本项目根据 MIT 许可证获得许可 - 有关详细信息，请参阅 LICENSE 文件。