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

使用函数式编程原则实现的Python抽象层，用于Z3定理证明器的功能，并通过模型上下文协议（MCP）服务器暴露这些功能。

概述

该项目展示了如何使用函数式编程方法来解决复杂的约束满足问题并分析实体之间的关系。它利用了returns库进行函数式编程抽象，并通过一个MCP服务器暴露其功能。

特性

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

项目结构

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

技术栈

• Z3求解器：微软的约束求解定理证明器
• 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

配置MCP服务器与Claude/Cline

要在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桌面应用使更改生效。

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

MCP工具

服务器提供以下工具：

solve_constraint_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

分析带有完整关系查询模型的实体间的关系。

# 示例输入
{
  "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. 结果类型：使用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文件。