Z3 MCP

🚀 Z3定理證明器與函數式編程項目

本項目基於Python實現，藉助Z3定理證明器解決複雜約束滿足問題，分析實體間關聯關係。同時，通過MCP（機器可讀配置）服務器接口將這些功能對外開放，為相關應用提供了強大的支持。

🚀 快速開始

安裝步驟

1. 克隆項目倉庫：

   git clone https://github.com/yourusername/z3_project.git
   cd z3_project
   

2. 安裝依賴項：

   pip install -r requirements.txt
   

3. 可選：安裝開發工具：

   pip install pre-commit
   

運行示例

約束求解示例

from src.solver import solve_constraints
variables = ['x', 'y']
constraints = ["x + y == 10", "x <= 5"]
solution = solve_constraints(variables, constraints)
print(solution)  # 輸出可能的解集合

關係推理示例

from src.relations import infer_relations
relations_data = [
    ("Bob", "Hanna", "sibling"),
    ("Bob", "Charlie", "sibling")
]
inferred = infer_relations(relations_data)
print(inferred)  # 輸出推導出的關係

啟動MCP服務器

uvicorn src.server:app --reload

✨ 主要特性

• 複雜約束處理：能夠解決涉及多個變量和條件的約束滿足問題。
• 關係分析：支持對實體間關係的推理與驗證。
• 函數式編程風格：採用不可變數據結構、結果類型及Maybe類型等函數式編程原則，確保代碼的簡潔性和可維護性。
• MCP服務器接口：提供標準化的機器可讀配置接口，便於外部系統的集成。

📦 安裝指南

1. 克隆項目倉庫：

   git clone https://github.com/yourusername/z3_project.git
   cd z3_project
   

2. 安裝依賴項：

   pip install -r requirements.txt
   

3. 可選：安裝開發工具：

   pip install pre-commit
   

💻 使用示例

基礎用法

約束求解示例

from src.solver import solve_constraints
variables = ['x', 'y']
constraints = ["x + y == 10", "x <= 5"]
solution = solve_constraints(variables, constraints)
print(solution)  # 輸出可能的解集合

關係推理示例

from src.relations import infer_relations
relations_data = [
    ("Bob", "Hanna", "sibling"),
    ("Bob", "Charlie", "sibling")
]
inferred = infer_relations(relations_data)
print(inferred)  # 輸出推導出的關係

高級用法

啟動MCP服務器

uvicorn src.server:app --reload

📚 詳細文檔

MCP服務器配置

簡單約束求解接口

請求格式：

{
  "variables": [
    {"name": "x", "type": "integer"},
    {"name": "y", "type": "integer"}
  ],
  "constraints": ["x + y == 10"],
  "description": "尋找滿足條件的x和y值"
}

簡單關係推理接口

請求格式：

{
  "relationships": [
    {"person1": "Bob", "person2": "Hanna", "relation": "sibling"},
    {"person1": "Bob", "person2": "Charlie", "relation": "sibling"}
  ],
  "query": "sibling(Hanna, Charlie)"
}

功能式編程方法

本項目展示了多種功能式編程技巧：

• 不可變數據結構：通過Pydantic模型實現數據的不可變性。
• 結果類型：使用returns.result.Result處理錯誤，避免異常拋出。
• Maybe類型：採用returns.maybe.Maybe處理可選值。
• Do Notation：結合生成器表達式和Result.do()實現操作序列。
• 模式匹配：利用Python的match-case結構提升代碼可讀性。

示例代碼

expr = (
    RelationshipResult(...)
    for entities in create_entities()
    if entities
)

🔧 技術細節

技術棧

📄 許可證

本項目遵循MIT License協議，允許自由使用、修改和分發。

貢獻指南

歡迎貢獻！請先閱讀CONTRIBUTING.md，瞭解如何參與開發。

📦 項目結構

z3_project/
├── README.md          # 項目文檔
├── LICENSE           # 許可證文件
├── setup.py          # 項目安裝腳本
├── requirements.txt  # 依賴管理文件
├── src/
│   ├── __init__.py    # 包初始化文件
│   ├── solver.py      # 約束求解器實現
│   ├── relations.py   # 關係推理模塊
│   └── server.py      # MCP服務器實現