Z3 Theorem Prover with Functional Programming

使用函数式编程的 Z3 定理证明器

使用函数式编程原则，对 Z3 定理证明器的功能进行抽象的 Python 实现，并通过 Model Context Protocol（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 Solver：Microsoft 的约束求解定理证明器
• Returns：用于单子操作和错误处理的函数式编程库
• Pydantic：数据验证和序列化
• FastMCP：Model Context Protocol 的实现

安装

本项目使用 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 皇后问题
• 家庭关系推断
• 基于因果关系的时间推理
• 算术字谜（SEND + MORE = MONEY）

运行 MCP 服务

启动 MCP 服务，通过 Model Context Protocol 开放 Z3 的功能：

# Run the server
python -m z3_poc.server.main

使用 Claude/Cline 配置 MCP 服务

要通过 VSCode 中的 Cline 扩展使用 Claude 的 Z3 求解器 MCP 服务，需要配置 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 app，使更改生效。

配置完成后，Claude 即可通过 MCP 服务使用 Z3 求解器的功能。

MCP 工具

该服务提供以下工具：

solve_constraint_problem

使用完整的 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

无需完整的 Problem 模型即可求解约束问题的简化接口。

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

函数式编程方法

本项目展示了若干函数式编程原则：

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

analyze_relationships 中 do 记法的示例：

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 许可，详情请参阅 LICENSE 文件。