Z3 MCP

🚀 Z3定理証明器と関数型プログラミングプロジェクト

このプロジェクトはPythonをベースに実装されており、Z3定理証明器を利用して複雑な制約充足問題を解決し、エンティティ間の関連関係を分析する方法を示すことを目的としています。さらに、MCP（機械可読設定）サーバーインターフェースを通じてこれらの機能を外部に公開しています。

✨ 主な機能

• 複雑な制約処理：複数の変数と条件を含む制約充足問題を解決できます。
• 関係分析：エンティティ間の関係の推論と検証をサポートします。
• 関数型プログラミングスタイル：不変データ構造、結果型、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
)

🔧 技術詳細

• Z3：Microsoftによって開発された高性能な定理証明ツールです。
• Pydantic：データ検証と設定構築に使用されるライブラリです。
• Returns：関数型プログラミングの拡張ライブラリで、結果型とMaybe型の処理をサポートします。
• FastMCP：軽量な機械可読設定サーバーフレームワークです。

📄 ライセンス

このプロジェクトはMIT Licenseに基づいており、自由な使用、修正、配布が許可されています。

貢献ガイド

貢献を歓迎します！開発に参加する方法については、CONTRIBUTING.mdをご覧ください。